The Immutability Benchmark is released under the MIT license and can be cited under the original DOI number 10.5281/zenodo.203085 or the most recent release version shown below.

Basic Assignment Test Cases

We create a basic set of assignment test cases that are: (a) systematic: the test cases are generated by starting from the assignments allowed by the language model, and (b) exhaustive: every possible assignment within the Java language is tested. Since an object can be mutated only through field assignments, and aliasing is not considered, any immutability analysis tool should be expected to pass these test cases.

To ensure systematic, exhaustive coverage of basic assignment cases, it is important to note that all mutations occur as a result of an update (assignment after initialization) to a field. Let us first consider updates to class variables, instance variables, and array components of fields. Array fields must be given special attention because there is no language mechanism to enforce the immutability of array components and updates to array components mutate the object containing the array field. Fields can be categorized into three groups, class variables, instance variables of another object instance, and instance variables of “this” object instance. Finally, we consider assignments involving stack variables, i.e. parameters passed and returned values. The high level assignment patterns can be represented succinctly as an assignment graph as shown in the figure below. Each node in the assignment graph corresponds to a set of program artifacts that can be on the left hand side or right hand side of an assignment. Each edge in the assignment graph can be instantiated multiple times, one for each pair of program artifacts in the source and destination node to generate a valid Java assignment. For instance, the downward edge to the right side of the assignment graph generates assignments from a final object, an Enum, a this reference, a primitive (byte, char, short, int, long, float, double, boolean), null or a String literal to a parameter. We enumerate all possible assignment pairs from the assignment graph to produce a total of 250 test cases.

Aliasing Test Cases

In the basic assignment test cases we defined a reference test that was explicitly mutated in the code and the analysis question was to correctly detect that test is mutated. In contrast, in the aliasing test cases, we create an alias to a reference test, and mutate the alias. The analysis question is to detect that test is indirectly mutated via the alias. In this category, there are four distinct aliasing patterns we test for, which can be explained using the concept of an aliasing chain. An aliasing chain is a sequence of explicit assignments of one reference to another, e.g., the statements b = a;, c = b; create the aliasing chain c → b → a. The four patterns of tests we perform are: (a) test case contains the aliasing chain a → test; (b) test case contains the aliasing chain test → a; (c) test case contains the aliasing chain a → b → test; and (d) test case contains the aliasing chain test → b → a. In all the above cases, the test case contains an explicit mutation to a, and analysis question asks whether test is mutable. The first two patterns (a) and (b) test whether mutations to an alias are propagated in either direction of the aliasing chain, while (c) and (d) test whether the analysis is also robust enough to detect mutations to aliases are propagated over levels of the aliasing chain.

Supplemental Test Cases

More details coming soon.