Adding Glacier and ReImInfer test cases

src/test/java/pico/ImmutabilityReImInferenceTest.java

@@ -0,0 +1,42 @@
+package pico;
+
+import checkers.inference.test.CFInferenceTest;
+import org.checkerframework.framework.test.TestUtilities;
+import org.checkerframework.javacutil.Pair;
+import org.junit.Ignore;
+import org.junit.runners.Parameterized.Parameters;
+import pico.inference.PICOInferenceChecker;
+import pico.inference.solver.PICOSolverEngine;
+
+import java.io.File;
+import java.util.ArrayList;
+import java.util.Arrays;
+import java.util.List;
+
+@SuppressWarnings("initialization")
+public class ImmutabilityReImInferenceTest extends CFInferenceTest {
+
+    public ImmutabilityReImInferenceTest(File testFile) {
+        super(testFile, PICOInferenceChecker.class, "",
+              "-Anomsgtext",
+                "-Astubs=src/main/java/pico/inference/jdk.astub",
+                "-d", "testdata/reiminfer");
+    }
+
+    @Override
+    public Pair<String, List<String>> getSolverNameAndOptions() {
+        return Pair.of(PICOSolverEngine.class.getCanonicalName(),
+                new ArrayList<>(Arrays.asList("useGraph=false", "collectStatistic=true")));
+    }
+
+    @Override
+    public boolean useHacks() {
+        return true;
+    }
+
+    @Parameters
+    public static List<File> getTestFiles(){
+        //InferenceTestUtilities.findAllSystemTests();
+        return new ArrayList<>(TestUtilities.findRelativeNestedJavaFiles("testinput", "reiminfer"));
+    }
+}

src/test/java/pico/ImmutabilityTypecheckGlacierTest.java

@@ -0,0 +1,23 @@
+package pico;
+
+import org.checkerframework.framework.test.CheckerFrameworkPerFileTest;
+import org.checkerframework.framework.test.TestUtilities;
+import org.junit.Ignore;
+import org.junit.runners.Parameterized.Parameters;
+import pico.typecheck.PICOChecker;
+
+import java.io.File;
+import java.util.ArrayList;
+import java.util.List;
+
+public class ImmutabilityTypecheckGlacierTest extends CheckerFrameworkPerFileTest {
+    public ImmutabilityTypecheckGlacierTest(File testFile) {
+        super(testFile, PICOChecker.class, "", "-Anomsgtext",
+                "-Anocheckjdk", "-d", "testTmp/glacier");
+    }
+
+    @Parameters
+    public static List<File> getTestFiles(){
+        return new ArrayList<>(TestUtilities.findRelativeNestedJavaFiles("testinput", "glacier"));
+    }
+}

testinput/glacier/ArrayClone.java

@@ -0,0 +1,7 @@
+// Change to PICO; array clone adaption.
+import qual.*;
+
+public class ArrayClone {
+    @Immutable Object @Immutable [] array = new @Immutable Object  @Immutable [0];
+    @Immutable Object @Immutable [] arrayClone = array.clone();
+}

testinput/glacier/ArrayCopy.java

@@ -0,0 +1,18 @@
+// @skip-test
+// Typecheck: Failed
+// Cause: checker cannot get clone() decl from stub! Decl receiver and return type get defaulted to mutable.
+// strange enough, seems other signatures are got from stubs.
+import qual.Immutable;
+
+
+public class ArrayCopy {
+    public void takeArray(@Immutable Object @Immutable [] array) {
+    }
+
+    public void passArray() {
+        @Immutable Object array[] = new @Immutable Object[5];
+
+        takeArray(array.clone());
+    }
+
+}

testinput/glacier/ArrayParameter.java

@@ -0,0 +1,22 @@
+import qual.*;
+import java.util.Arrays;
+
+
+class Array {
+    public static <T> T[] add(final T @Readonly[] array, final T entry) {
+        final int s = array.length;
+        final T[] t = Arrays.copyOf(array, s + 1);
+        t[s] = entry;
+        return t;
+    }
+}
+
+
+public class ArrayParameter {
+    final @Immutable Object @Immutable [] keys = new @Immutable Object @Immutable [0];
+
+
+    public void passArray(@Immutable Object k) {
+        Array.add(keys, k);
+    }
+}

testinput/glacier/Arrays.java

@@ -0,0 +1,21 @@
+package glacier;
+
+public class Arrays {
+    int [] intArray;
+
+    public Arrays() {
+
+    }
+
+    public int[] getData() {
+        return intArray;
+    }
+
+    public byte[] getByteData() {
+        return new byte[0];
+    }
+
+    public void setData() {
+        intArray[0] = 42;
+    }
+}

testinput/glacier/BooleanSubtyping.java

@@ -0,0 +1,16 @@
+public class BooleanSubtyping {
+    public enum CellType {
+        BLANK(3),
+        NUMBER(0);
+
+        private int value;
+        private CellType(int value) {
+            this.value = value;
+        }
+    }
+
+    public boolean foo() {
+        CellType cellType = CellType.BLANK;
+        return cellType == CellType.NUMBER;
+    }
+}

testinput/glacier/ClassGetName.java

@@ -0,0 +1,6 @@
+public class ClassGetName {
+    public String foo() {
+        Number num = null;
+        return num.getClass().getName();
+    }
+}

testinput/glacier/ClassReturn.java

@@ -0,0 +1,9 @@
+// typecheck: OK
+
+
+public class ClassReturn {
+    public ClassReturn getInstance() {
+        return new ClassReturn();
+    }
+
+}

testinput/glacier/ColorImpl.java

@@ -0,0 +1,18 @@
+// @skip-test
+// Typecheck, Inference-TC: Failed
+// Cause: checker cannot get clone() decl from stub! Decl receiver and return type get defaulted to mutable.
+// strange enough, seems other signatures are got from stubs.
+import java.util.Arrays;
+import qual.Immutable;
+
+public class ColorImpl {
+    private byte @Immutable [] _rgb;
+    private byte [] _mutableRgb;
+
+    public int hashCode() {
+        // This should be OK, but will be an error until we have a @ReadOnly annotation.
+        Arrays.hashCode(_mutableRgb);
+
+        return Arrays.hashCode(_rgb);
+    }
+}

testinput/glacier/CompareTo.java

@@ -0,0 +1,11 @@
+package glacier;
+
+public class CompareTo {
+
+    public void foo() {
+        Object val1 = null;
+        Object val2 = null;
+        // Shouldn't give an error.
+        ((Boolean)val1).compareTo((Boolean)val2);
+    }
+}

testinput/glacier/ConflictingAnnotations.java

@@ -0,0 +1,33 @@
+import qual.*;
+
+@Immutable class ImmutClass {
+}
+
+@Mutable class MutableClass {
+}
+
+class DefaultMutableClass {
+}
+
+@Immutable interface ImmutInterface {
+}
+
+interface MutableInterface {
+}
+
+public class ConflictingAnnotations {
+    // ::error: (type.invalid.annotations.on.use)
+    @Mutable ImmutClass o1;
+
+    // ::error: (type.invalid.annotations.on.use)
+    @Immutable MutableClass o2;
+
+    // ::error: (type.invalid.annotations.on.use)
+    @Immutable DefaultMutableClass o3;
+
+    // ::error: (type.invalid.annotations.on.use)
+    @Mutable ImmutInterface i1;
+
+    // ::error: (type.invalid.annotations.on.use)
+    @Immutable MutableInterface i2;
+}

testinput/glacier/ConstructorAssignment.java

@@ -0,0 +1,24 @@
+package glacier;
+
+import qual.Immutable;
+
+public @Immutable class ConstructorAssignment {
+    public int x = 3; // static assignment is OK
+
+    ConstructorAssignment() {
+        x = 4; // constructor assignment is OK
+    }
+
+    void setX() {
+        // ::error: (illegal.field.write)
+        x = 5;
+    }
+}
+
+class OtherClass {
+    OtherClass() {
+        ConstructorAssignment c = new ConstructorAssignment();
+        // ::error: (illegal.field.write)
+        c.x = 6;
+    }
+}

testinput/glacier/EnumTest.java

@@ -0,0 +1,19 @@
+package glacier;
+
+import qual.Immutable;
+
+@Immutable enum Underline{
+    NONE,
+    SINGLE,
+    DOUBLE,
+    SINGLE_ACCOUNTING,
+    DOUBLE_ACCOUNTING
+}
+
+public class EnumTest {
+    Underline u;
+
+    public void foo() {
+        u.ordinal();
+    }
+}

testinput/glacier/EqualsTest.java

@@ -0,0 +1,23 @@
+// @skip-test
+package glacier;
+
+import qual.*;
+
+@Immutable public class EqualsTest {
+    @Override
+    public boolean equals(Object obj) {
+        if (this == obj)
+            return true;
+        return false;
+    }
+}
+
+class EqualsTest2 {
+    @Override
+    // ::error: (override.param.invalid)
+    public boolean equals(@Immutable Object obj) {
+        if (this == obj)
+            return true;
+        return false;
+    }
+}

testinput/glacier/FontImpl.java

@@ -0,0 +1,34 @@
+// Note: PICO defaults the class decal to RDM. Removing errors on line 26 and 30.
+
+import qual.*;
+
+@Immutable  interface SColor {
+}
+
+@Immutable abstract class AbstractColorAdv implements SColor {
+}
+
+// ::error: (type.invalid.annotations.on.use)
+class FI_ColorImpl extends AbstractColorAdv {
+    // Arguably it would be preferable for this to not be an error.
+    // ::error: (type.invalid.annotations.on.use)
+    public static final AbstractColorAdv BLACK = new FI_ColorImpl("#000000");
+
+    // PICO Note: adding this error.
+    // ::error: (super.invocation.invalid)
+    FI_ColorImpl(String fontColor) {
+
+    }
+}
+
+public class FontImpl {
+    FontImpl(String fontColor) {
+        // Arguably it would be preferable for this to not be an error.
+        // Removing error. PICO chose the preferable path.
+        SColor a = new FI_ColorImpl(fontColor);
+
+        // Arguably it would be preferable for this to not be an error either.
+        // Removing error. PICO chose the preferable path.
+        SColor c = fontColor != null ? new FI_ColorImpl(fontColor) : null;
+    }
+}

testinput/glacier/ImmutableArray.java

@@ -0,0 +1,16 @@
+import qual.Immutable;
+
+@SuppressWarnings("initialization")
+@Immutable class ImmutableArray {
+    private byte @Immutable [] _rgb;
+
+    private String @Immutable [] _strings;
+
+    // Immutable array of mutable objects is mutable.
+    // PICO allows shallow immutable array.
+    private java.util.Date @Immutable [] _dates;
+
+    // MaybeMutable array of primitives is mutable.
+    // PICO allows shallow immutable array.
+    private int [] _ints;
+}

testinput/glacier/ImmutableClassMutableInterface.java

@@ -0,0 +1,14 @@
+import qual.*;
+
+@ReceiverDependantMutable
+interface ICMI_MutableInterface {};
+
+@Immutable public class ImmutableClassMutableInterface implements ICMI_MutableInterface {
+    public static void bar(ICMI_MutableInterface m) { };
+
+    public static void foo() {
+        ImmutableClassMutableInterface x = null;
+        bar(x);
+    }
+
+};