Walk to an ancestor's constructor spec through JDK bytecode delegation

liquidjava-example/src/main/java/testSuite/classes/delegated_argument_reassigned_error/HashMapRefinements.java

@@ -0,0 +1,15 @@
+package testSuite.classes.delegated_argument_reassigned_error;
+
+import liquidjava.specification.ExternalRefinementsFor;
+import liquidjava.specification.Ghost;
+import liquidjava.specification.StateRefinement;
+
+@ExternalRefinementsFor("java.util.HashMap")
+@Ghost("int capacity")
+public interface HashMapRefinements<K, V> {
+    @StateRefinement(to = "capacity(this) == initialCapacity")
+    void HashMap(int initialCapacity);
+
+    @StateRefinement(from = "capacity(this) == 5")
+    V get(Object key);
+}

liquidjava-example/src/main/java/testSuite/classes/delegated_argument_reassigned_error/Test.java

@@ -0,0 +1,34 @@
+package testSuite.classes.delegated_argument_reassigned_error;
+
+import java.util.function.IntFunction;
+import javax.print.attribute.standard.PrinterStateReasons;
+
+// PrinterStateReasons(int) runs HashMap(int): the capacity is the argument's value at the call, not a later one
+public class Test {
+    static void assignedBefore(int n) {
+        n = 5;
+        PrinterStateReasons r = new PrinterStateReasons(n);
+        r.get("k");
+    }
+
+    static void assignedAfter(int n) {
+        PrinterStateReasons r = new PrinterStateReasons(n);
+        n = 5;
+        r.get("k"); // Expect: State Refinement Error
+    }
+
+    static void assignedBeforeAndAfter(int n) {
+        n = 6;
+        PrinterStateReasons r = new PrinterStateReasons(n);
+        n = 5;
+        r.get("k"); // Expect: State Refinement Error
+    }
+
+    static IntFunction<PrinterStateReasons> lambdaParameter() {
+        return k -> {
+            PrinterStateReasons r = new PrinterStateReasons(k);
+            r.get("k"); // Expect: State Refinement Error
+            return r;
+        };
+    }
+}

liquidjava-example/src/main/java/testSuite/classes/delegated_constant_arguments_error/HashSetRefinements.java

@@ -0,0 +1,20 @@
+package testSuite.classes.delegated_constant_arguments_error;
+
+import liquidjava.specification.ExternalRefinementsFor;
+import liquidjava.specification.Ghost;
+import liquidjava.specification.StateRefinement;
+import liquidjava.specification.StateSet;
+
+@ExternalRefinementsFor("java.util.HashSet")
+@Ghost("int capacity")
+@StateSet({ "plain", "linked" })
+public interface HashSetRefinements<E> {
+    @StateRefinement(to = "capacity(this) == initialCapacity && (dummy --> linked(this)) && (!dummy --> plain(this))")
+    void HashSet(int initialCapacity, float loadFactor, boolean dummy);
+
+    @StateRefinement(from = "capacity(this) == 16 && linked(this)")
+    boolean add(E e);
+
+    @StateRefinement(from = "plain(this)")
+    void clear();
+}

liquidjava-example/src/main/java/testSuite/classes/delegated_constant_arguments_error/Test.java

@@ -0,0 +1,22 @@
+package testSuite.classes.delegated_constant_arguments_error;
+
+import java.util.LinkedHashSet;
+
+// LinkedHashSet() runs HashSet(16, .75f, true) and LinkedHashSet(int n) runs HashSet(n, .75f, true): the constants
+// passed reach the spec as literals
+public class Test {
+    static void defaultCapacity() {
+        LinkedHashSet<String> s = new LinkedHashSet<>();
+        s.add("x");
+    }
+
+    static void linked() {
+        LinkedHashSet<String> s = new LinkedHashSet<>();
+        s.clear(); // Expect: State Refinement Error
+    }
+
+    static void otherCapacity(int n) {
+        LinkedHashSet<String> s = new LinkedHashSet<>(n);
+        s.add("x"); // Expect: State Refinement Error
+    }
+}

liquidjava-example/src/main/java/testSuite/classes/delegated_spec_keeping_other_sets_correct/HashMapRefinements.java

@@ -0,0 +1,16 @@
+package testSuite.classes.delegated_spec_keeping_other_sets_correct;
+
+import liquidjava.specification.ExternalRefinementsFor;
+import liquidjava.specification.StateRefinement;
+import liquidjava.specification.StateSet;
+
+@ExternalRefinementsFor("java.util.HashMap")
+@StateSet({ "a1", "a2" })
+@StateSet({ "b1", "b2" })
+public interface HashMapRefinements<K, V> {
+    @StateRefinement(to = "a2(this)")
+    void HashMap(int initialCapacity);
+
+    @StateRefinement(from = "b1(this)")
+    V get(Object key);
+}

liquidjava-example/src/main/java/testSuite/classes/delegated_spec_keeping_other_sets_correct/Test.java

@@ -0,0 +1,12 @@
+package testSuite.classes.delegated_spec_keeping_other_sets_correct;
+
+import javax.print.attribute.standard.PrinterStateReasons;
+
+// HashMap(int)'s spec leaves the b set unchanged, which refers to the old object: a new object has none, so the
+// delegated call gets the default state (b1) instead of that spec
+public class Test {
+    static void get() {
+        PrinterStateReasons r = new PrinterStateReasons(5);
+        r.get("k");
+    }
+}

liquidjava-example/src/main/java/testSuite/classes/delegated_subclass_sets_error/StackRefinements.java

@@ -0,0 +1,15 @@
+package testSuite.classes.delegated_subclass_sets_error;
+
+import liquidjava.specification.ExternalRefinementsFor;
+import liquidjava.specification.StateRefinement;
+import liquidjava.specification.StateSet;
+
+@ExternalRefinementsFor("java.util.Stack")
+@StateSet({ "empty", "nonEmpty" })
+public interface StackRefinements<E> {
+    @StateRefinement(from = "empty(this)", to = "nonEmpty(this)")
+    E push(E item);
+
+    @StateRefinement(from = "nonEmpty(this)")
+    E peek();
+}

liquidjava-example/src/main/java/testSuite/classes/delegated_subclass_sets_error/Test.java

@@ -0,0 +1,17 @@
+package testSuite.classes.delegated_subclass_sets_error;
+
+import java.util.Stack;
+
+// Stack() runs Vector(), whose spec sets only Vector's ghost: Stack's own state set starts at its default (empty)
+public class Test {
+    static void pushThenPeek() {
+        Stack<String> s = new Stack<>();
+        s.push("a");
+        s.peek();
+    }
+
+    static void peekEmpty() {
+        Stack<String> s = new Stack<>();
+        s.peek(); // Expect: State Refinement Error
+    }
+}

liquidjava-example/src/main/java/testSuite/classes/delegated_subclass_sets_error/VectorRefinements.java

@@ -0,0 +1,12 @@
+package testSuite.classes.delegated_subclass_sets_error;
+
+import liquidjava.specification.ExternalRefinementsFor;
+import liquidjava.specification.Ghost;
+import liquidjava.specification.StateRefinement;
+
+@ExternalRefinementsFor("java.util.Vector")
+@Ghost("int elements")
+public interface VectorRefinements<E> {
+    @StateRefinement(to = "elements(this) == 0")
+    void Vector();
+}

liquidjava-example/src/main/java/testSuite/classes/super_swapped_arguments_correct/Base.java

@@ -0,0 +1,13 @@
+package testSuite.classes.super_swapped_arguments_correct;
+
+import liquidjava.specification.StateRefinement;
+import liquidjava.specification.StateSet;
+
+@StateSet({"open", "closed"})
+public class Base {
+    @StateRefinement(to = "(x && !y && open(this)) || (!(x && !y) && closed(this))")
+    public Base(boolean x, boolean y) {}
+
+    @StateRefinement(from = "open(this)", to = "closed(this)")
+    public void close() {}
+}

liquidjava-example/src/main/java/testSuite/classes/super_swapped_arguments_correct/Sub.java

@@ -0,0 +1,14 @@
+package testSuite.classes.super_swapped_arguments_correct;
+
+// The parameters of Sub are named like those of Base, in the other order: each Base parameter is replaced by the Sub
+// parameter passed for it, all at once, so a name is not replaced twice
+public class Sub extends Base {
+    public Sub(boolean y, boolean x) {
+        super(y, x);
+    }
+
+    static void test() {
+        Sub s = new Sub(true, false); // Base(true, false): open
+        s.close();
+    }
+}

liquidjava-example/src/main/java/testSuite/classes/super_swapped_arguments_error/Base.java

@@ -0,0 +1,13 @@
+package testSuite.classes.super_swapped_arguments_error;
+
+import liquidjava.specification.StateRefinement;
+import liquidjava.specification.StateSet;
+
+@StateSet({"open", "closed"})
+public class Base {
+    @StateRefinement(to = "(x && !y && open(this)) || (!(x && !y) && closed(this))")
+    public Base(boolean x, boolean y) {}
+
+    @StateRefinement(from = "open(this)", to = "closed(this)")
+    public void close() {}
+}

liquidjava-example/src/main/java/testSuite/classes/super_swapped_arguments_error/Sub.java

@@ -0,0 +1,14 @@
+package testSuite.classes.super_swapped_arguments_error;
+
+// The parameters of Sub are named like those of Base, in the other order: each Base parameter is replaced by the Sub
+// parameter passed for it, all at once, so a name is not replaced twice
+public class Sub extends Base {
+    public Sub(boolean y, boolean x) {
+        super(y, x);
+    }
+
+    static void test() {
+        Sub s = new Sub(false, true); // Base(false, true): closed
+        s.close(); // Expect: State Refinement Error
+    }
+}

liquidjava-example/src/main/java/testSuite/classes/throwable_jdk_subclass_correct/MyException.java

@@ -0,0 +1,10 @@
+package testSuite.classes.throwable_jdk_subclass_correct;
+
+import java.io.IOException;
+
+// super(message) runs IOException(String), Exception(String) and then Throwable(String): no cause.
+public class MyException extends IOException {
+    public MyException(String message) {
+        super(message);
+    }
+}

liquidjava-example/src/main/java/testSuite/classes/throwable_jdk_subclass_correct/Test.java

@@ -0,0 +1,29 @@
+package testSuite.classes.throwable_jdk_subclass_correct;
+
+// JDK exceptions whose constructors only pass their arguments up to Throwable(String) or Throwable() are created
+// without a cause, so one initCause is allowed.
+public class Test {
+    static RuntimeException wrap(Throwable t) {
+        RuntimeException e = new RuntimeException("failed");
+        e.initCause(t);
+        return e;
+    }
+
+    static IllegalStateException illegalState(Throwable t) {
+        IllegalStateException e = new IllegalStateException("failed");
+        e.initCause(t);
+        return e;
+    }
+
+    static Exception noMessage(Throwable t) {
+        Exception e = new Exception();
+        e.initCause(t);
+        return e;
+    }
+
+    static MyException mine(Throwable t) {
+        MyException e = new MyException("failed");
+        e.initCause(t);
+        return e;
+    }
+}

liquidjava-example/src/main/java/testSuite/classes/throwable_jdk_subclass_correct/ThrowableRefinements.java

@@ -0,0 +1,24 @@
+package testSuite.classes.throwable_jdk_subclass_correct;
+
+import liquidjava.specification.ExternalRefinementsFor;
+import liquidjava.specification.StateRefinement;
+import liquidjava.specification.StateSet;
+
+@ExternalRefinementsFor("java.lang.Throwable")
+@StateSet({ "noThrowable", "withThrowable" })
+public interface ThrowableRefinements {
+    @StateRefinement(to = "noThrowable(this)")
+    public void Throwable();
+
+    @StateRefinement(to = "noThrowable(this)")
+    public void Throwable(String message);
+
+    @StateRefinement(to = "withThrowable(this)")
+    public void Throwable(String message, Throwable cause);
+
+    @StateRefinement(to = "withThrowable(this)")
+    public void Throwable(Throwable cause);
+
+    @StateRefinement(from = "noThrowable(this)", to = "withThrowable(this)")
+    public Throwable initCause(Throwable cause);
+}

liquidjava-example/src/main/java/testSuite/classes/throwable_jdk_subclass_error/NotFound.java

@@ -0,0 +1,7 @@
+package testSuite.classes.throwable_jdk_subclass_error;
+
+public class NotFound extends ClassNotFoundException {
+    public NotFound(String message) {
+        super(message);
+    }
+}

liquidjava-example/src/main/java/testSuite/classes/throwable_jdk_subclass_error/Test.java

@@ -0,0 +1,34 @@
+package testSuite.classes.throwable_jdk_subclass_error;
+
+import java.util.MissingResourceException;
+
+public class Test {
+    // ClassNotFoundException() runs Throwable(Throwable) with a null cause, so initCause throws
+    // IllegalStateException("Can't overwrite cause") (scijava-common CommandInfo, fixed in a6fd9cf)
+    static ClassNotFoundException notFound(Throwable exc) throws ClassNotFoundException {
+        final ClassNotFoundException cnfe = new ClassNotFoundException();
+        cnfe.initCause(exc); // Expect: State Refinement Error
+        throw cnfe;
+    }
+
+    static RuntimeException causeTwice(Throwable cause, Throwable other) {
+        RuntimeException e = new RuntimeException("failed", cause);
+        e.initCause(other); // Expect: State Refinement Error
+        return e;
+    }
+
+    // super(message) runs ClassNotFoundException(String), which passes a null cause on to Throwable(String, Throwable)
+    static NotFound notFoundSubclass(Throwable exc) {
+        NotFound e = new NotFound("missing");
+        e.initCause(exc); // Expect: State Refinement Error
+        return e;
+    }
+
+    // MissingResourceException(String, String, String) also writes fields after super(message), so it is not known to
+    // delegate and gets the default state, in which initCause cannot be shown to be allowed (#367)
+    static MissingResourceException notDelegating(Throwable exc) {
+        MissingResourceException e = new MissingResourceException("missing", "Bundle", "key");
+        e.initCause(exc); // Expect: State Refinement Error
+        return e;
+    }
+}

liquidjava-example/src/main/java/testSuite/classes/throwable_jdk_subclass_error/ThrowableRefinements.java

@@ -0,0 +1,24 @@
+package testSuite.classes.throwable_jdk_subclass_error;
+
+import liquidjava.specification.ExternalRefinementsFor;
+import liquidjava.specification.StateRefinement;
+import liquidjava.specification.StateSet;
+
+@ExternalRefinementsFor("java.lang.Throwable")
+@StateSet({ "noThrowable", "withThrowable" })
+public interface ThrowableRefinements {
+    @StateRefinement(to = "noThrowable(this)")
+    public void Throwable();
+
+    @StateRefinement(to = "noThrowable(this)")
+    public void Throwable(String message);
+
+    @StateRefinement(to = "withThrowable(this)")
+    public void Throwable(String message, Throwable cause);
+
+    @StateRefinement(to = "withThrowable(this)")
+    public void Throwable(Throwable cause);
+
+    @StateRefinement(from = "noThrowable(this)", to = "withThrowable(this)")
+    public Throwable initCause(Throwable cause);
+}

liquidjava-example/src/main/java/testSuite/classes/throwable_subclass_more_than_super_error/CauseAfterImplicitSuper.java

@@ -0,0 +1,16 @@
+package testSuite.classes.throwable_subclass_more_than_super_error;
+
+import java.io.IOException;
+
+// the implicit super() leaves no cause, but the constructor then sets one
+public class CauseAfterImplicitSuper extends IOException {
+    public CauseAfterImplicitSuper(Throwable cause) {
+        initCause(cause);
+    }
+
+    static CauseAfterImplicitSuper wrap(Throwable cause, Throwable other) {
+        CauseAfterImplicitSuper e = new CauseAfterImplicitSuper(cause);
+        e.initCause(other); // Expect: State Refinement Error
+        return e;
+    }
+}

liquidjava-example/src/main/java/testSuite/classes/throwable_subclass_more_than_super_error/CauseAfterSuper.java

@@ -0,0 +1,16 @@
+package testSuite.classes.throwable_subclass_more_than_super_error;
+
+// super(message) leaves no cause, but the constructor then sets one, so it gets the default state, not
+// Throwable(String)'s, and a second initCause is reported
+public class CauseAfterSuper extends RuntimeException {
+    public CauseAfterSuper(String message, Throwable cause) {
+        super(message);
+        initCause(cause);
+    }
+
+    static CauseAfterSuper wrap(Throwable cause, Throwable other) {
+        CauseAfterSuper e = new CauseAfterSuper("failed", cause);
+        e.initCause(other); // Expect: State Refinement Error
+        return e;
+    }
+}