Give state hints when the state set or methods come from the receiver's supertypes

liquidjava-example/src/main/java/testSuite/ErrorStateHintInheritedStates.java

@@ -0,0 +1,30 @@
+package testSuite;
+
+import liquidjava.specification.StateRefinement;
+import liquidjava.specification.StateSet;
+
+@StateSet({"a", "b", "c"})
+public class ErrorStateHintInheritedStates {
+
+    @StateRefinement(to = "a(this)")
+    public ErrorStateHintInheritedStates() {}
+
+    @StateRefinement(from = "a(this)", to = "b(this)")
+    public void ab() {}
+
+    @StateRefinement(from = "c(this)")
+    public void useC() {}
+
+    public static void use() {
+        ErrorStateHintInheritedStatesChild s = new ErrorStateHintInheritedStatesChild();
+        s.ab();
+        s.useC(); // Expect: State Refinement Error
+    }
+}
+
+// adds a transition to the states it inherits
+class ErrorStateHintInheritedStatesChild extends ErrorStateHintInheritedStates {
+
+    @StateRefinement(from = "b(this)", to = "c(this)")
+    public void bc() {}
+}

liquidjava-example/src/main/java/testSuite/ErrorStateHintOverride.java

@@ -0,0 +1,30 @@
+package testSuite;
+
+import liquidjava.specification.StateRefinement;
+import liquidjava.specification.StateSet;
+
+@StateSet({"a", "b", "c"})
+public class ErrorStateHintOverride {
+
+    @StateRefinement(to = "a(this)")
+    public ErrorStateHintOverride() {}
+
+    @StateRefinement(from = "a(this)", to = "b(this) || c(this)")
+    public void next() {}
+
+    @StateRefinement(from = "c(this)")
+    public void useC() {}
+
+    public static void use() {
+        ErrorStateHintOverrideChild s = new ErrorStateHintOverrideChild();
+        s.useC(); // Expect: State Refinement Error
+    }
+}
+
+// the override always moves to c, which the superclass's refinement does not promise
+class ErrorStateHintOverrideChild extends ErrorStateHintOverride {
+
+    @Override
+    @StateRefinement(from = "a(this)", to = "c(this)")
+    public void next() {}
+}

liquidjava-example/src/main/java/testSuite/ErrorStateHintSubclass.java

@@ -16,7 +16,7 @@ public void ab() {}
     public void useC() {}
 
     public static void use() {
-        ErrorStateHintSubclassChild s = new ErrorStateHintSubclassChild();
+        ErrorStateHintSubclass s = new ErrorStateHintSubclassChild();
         s.ab();
         s.useC(); // Expect: State Refinement Error
     }

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

@@ -0,0 +1,19 @@
+package testSuite.classes.state_hints_generic_inherited_method_error;
+
+import liquidjava.specification.ExternalRefinementsFor;
+import liquidjava.specification.StateRefinement;
+import liquidjava.specification.StateSet;
+
+@StateSet({"empty", "nonEmpty"})
+@ExternalRefinementsFor("java.util.Stack")
+public interface StackRefinements<E> {
+    @StateRefinement(to = "empty(this)")
+    void Stack();
+
+    // Stack inherits add from Vector, and the verifier does not find this refinement for a call to it
+    @StateRefinement(to = "nonEmpty(this)")
+    boolean add(E e);
+
+    @StateRefinement(from = "nonEmpty(this)")
+    E pop();
+}

liquidjava-example/src/main/java/testSuite/classes/state_hints_generic_inherited_method_error/Use.java

@@ -0,0 +1,10 @@
+package testSuite.classes.state_hints_generic_inherited_method_error;
+
+import java.util.Stack;
+
+public class Use {
+    static void popEmpty() {
+        Stack<String> s = new Stack<>();
+        s.pop(); // Expect: State Refinement Error
+    }
+}

liquidjava-example/src/main/java/testSuite/classes/state_hints_grandchild_spec_error/Use.java

@@ -0,0 +1,12 @@
+package testSuite.classes.state_hints_grandchild_spec_error;
+
+import javax.swing.JFrame;
+
+// JFrame has no spec: its state set comes from Window's, and setUndecorated from Frame's
+public class Use {
+    static void borderless() {
+        JFrame window = new JFrame("Playfield");
+        window.pack();
+        window.setUndecorated(true); // Expect: State Refinement Error
+    }
+}

liquidjava-example/src/main/java/testSuite/classes/state_hints_grandchild_spec_error/WindowRefinements.java

@@ -0,0 +1,25 @@
+package testSuite.classes.state_hints_grandchild_spec_error;
+
+import liquidjava.specification.ExternalRefinementsFor;
+import liquidjava.specification.StateRefinement;
+import liquidjava.specification.StateSet;
+
+@StateSet({"displayable", "notDisplayable"})
+@ExternalRefinementsFor("java.awt.Window")
+public interface WindowRefinements {
+    @StateRefinement(to = "notDisplayable(this)")
+    void dispose();
+
+    @StateRefinement(to = "displayable(this)")
+    void pack();
+}
+
+// the state set is declared in the superclass's spec
+@ExternalRefinementsFor("java.awt.Frame")
+interface FrameRefinements {
+    @StateRefinement(to = "notDisplayable(this)")
+    void Frame(String title);
+
+    @StateRefinement(from = "notDisplayable(this)")
+    void setUndecorated(boolean undecorated);
+}

liquidjava-example/src/main/java/testSuite/classes/state_hints_inaccessible_inherited_error/Door.java

@@ -0,0 +1,29 @@
+package testSuite.classes.state_hints_inaccessible_inherited_error;
+
+import liquidjava.specification.StateRefinement;
+import liquidjava.specification.StateSet;
+
+@StateSet({"shut", "ajar"})
+public interface Door {
+
+    @StateRefinement(from = "shut(this)", to = "ajar(this)")
+    private void pry() {}
+
+    @StateRefinement(from = "shut(this)", to = "ajar(this)")
+    default void push() {}
+
+    @StateRefinement(from = "ajar(this)")
+    default void walkThrough() {}
+}
+
+// only push() can be called on an implementing class: pry() is private
+class FrontDoor implements Door {
+
+    @StateRefinement(to = "shut(this)")
+    FrontDoor() {}
+
+    static void walkThroughShut() {
+        FrontDoor door = new FrontDoor();
+        door.walkThrough(); // Expect: State Refinement Error
+    }
+}

liquidjava-example/src/main/java/testSuite/classes/state_hints_inaccessible_inherited_error/Hatch.java

@@ -0,0 +1,35 @@
+package testSuite.classes.state_hints_inaccessible_inherited_error;
+
+import liquidjava.specification.StateRefinement;
+import liquidjava.specification.StateSet;
+
+@StateSet({"closed", "open"})
+public class Hatch {
+
+    @StateRefinement(to = "closed(this)")
+    public Hatch() {}
+
+    @StateRefinement(from = "closed(this)", to = "open(this)")
+    private void open() {}
+
+    @StateRefinement(from = "closed(this)", to = "open(this)")
+    void openInPackage() {}
+
+    @StateRefinement(from = "closed(this)", to = "open(this)")
+    protected void openInSubclass() {}
+
+    @StateRefinement(from = "closed(this)", to = "open(this)")
+    public void openPublicly() {}
+
+    @StateRefinement(from = "open(this)")
+    public void use() {}
+}
+
+// only openPublicly() can be called on a subclass by every caller
+class SamePackageHatch extends Hatch {
+
+    static void useClosed() {
+        SamePackageHatch hatch = new SamePackageHatch();
+        hatch.use(); // Expect: State Refinement Error
+    }
+}

liquidjava-example/src/main/java/testSuite/classes/state_hints_redeclared_method_error/Use.java

@@ -0,0 +1,11 @@
+package testSuite.classes.state_hints_redeclared_method_error;
+
+import java.awt.Frame;
+
+public class Use {
+    static void borderless() {
+        Frame host = new Frame("Playfield");
+        host.pack();
+        host.setUndecorated(true); // Expect: State Refinement Error
+    }
+}

liquidjava-example/src/main/java/testSuite/classes/state_hints_redeclared_method_error/WindowRefinements.java

@@ -0,0 +1,28 @@
+package testSuite.classes.state_hints_redeclared_method_error;
+
+import liquidjava.specification.ExternalRefinementsFor;
+import liquidjava.specification.StateRefinement;
+import liquidjava.specification.StateSet;
+
+@StateSet({"displayable", "notDisplayable"})
+@ExternalRefinementsFor("java.awt.Window")
+public interface WindowRefinements {
+    @StateRefinement(to = "notDisplayable(this)")
+    void dispose();
+
+    @StateRefinement(to = "displayable(this)")
+    void pack();
+
+    // Frame redeclares addNotify, so on a Frame the verifier does not apply this refinement
+    @StateRefinement(to = "displayable(this)")
+    void addNotify();
+}
+
+@ExternalRefinementsFor("java.awt.Frame")
+interface FrameRefinements {
+    @StateRefinement(to = "notDisplayable(this)")
+    void Frame(String title);
+
+    @StateRefinement(from = "notDisplayable(this)")
+    void setUndecorated(boolean undecorated);
+}

liquidjava-example/src/main/java/testSuite/classes/state_hints_same_simple_name_error/ArrayListRefinements.java

@@ -0,0 +1,18 @@
+package testSuite.classes.state_hints_same_simple_name_error;
+
+import liquidjava.specification.ExternalRefinementsFor;
+import liquidjava.specification.StateRefinement;
+import liquidjava.specification.StateSet;
+
+@StateSet({"empty", "nonEmpty"})
+@ExternalRefinementsFor("java.util.ArrayList")
+public interface ArrayListRefinements<E> {
+    @StateRefinement(to = "empty(this)")
+    void ArrayList();
+
+    @StateRefinement(to = "nonEmpty(this)")
+    boolean add(E e);
+
+    @StateRefinement(from = "nonEmpty(this)")
+    E remove(int index);
+}

liquidjava-example/src/main/java/testSuite/classes/state_hints_same_simple_name_error/Collection.java

@@ -0,0 +1,14 @@
+package testSuite.classes.state_hints_same_simple_name_error;
+
+import liquidjava.specification.StateRefinement;
+import liquidjava.specification.StateSet;
+
+// shares its simple name with java.util.Collection, a supertype of ArrayList, but its states are not ArrayList's
+@StateSet({"fresh", "used"})
+public class Collection {
+    @StateRefinement(to = "fresh(this)")
+    public Collection() {}
+
+    @StateRefinement(from = "fresh(this)", to = "used(this)")
+    public void use() {}
+}

liquidjava-example/src/main/java/testSuite/classes/state_hints_same_simple_name_error/Use.java

@@ -0,0 +1,10 @@
+package testSuite.classes.state_hints_same_simple_name_error;
+
+import java.util.ArrayList;
+
+public class Use {
+    static void removeFromEmpty() {
+        ArrayList<String> l = new ArrayList<>();
+        l.remove(0); // Expect: State Refinement Error
+    }
+}

liquidjava-example/src/main/java/testSuite/classes/state_hints_superclass_spec_error/Use.java

@@ -0,0 +1,11 @@
+package testSuite.classes.state_hints_superclass_spec_error;
+
+import java.awt.Frame;
+
+public class Use {
+    static void borderless() {
+        Frame host = new Frame("Playfield");
+        host.pack();
+        host.setUndecorated(true); // Expect: State Refinement Error
+    }
+}

liquidjava-example/src/main/java/testSuite/classes/state_hints_superclass_spec_error/WindowRefinements.java

@@ -0,0 +1,25 @@
+package testSuite.classes.state_hints_superclass_spec_error;
+
+import liquidjava.specification.ExternalRefinementsFor;
+import liquidjava.specification.StateRefinement;
+import liquidjava.specification.StateSet;
+
+@StateSet({"displayable", "notDisplayable"})
+@ExternalRefinementsFor("java.awt.Window")
+public interface WindowRefinements {
+    @StateRefinement(to = "notDisplayable(this)")
+    void dispose();
+
+    @StateRefinement(to = "displayable(this)")
+    void pack();
+}
+
+// the state set is declared in the superclass's spec
+@ExternalRefinementsFor("java.awt.Frame")
+interface FrameRefinements {
+    @StateRefinement(to = "notDisplayable(this)")
+    void Frame(String title);
+
+    @StateRefinement(from = "notDisplayable(this)")
+    void setUndecorated(boolean undecorated);
+}

liquidjava-verifier/src/main/java/liquidjava/diagnostics/hints/StateHints.java

@@ -170,7 +170,8 @@ private List<Hint> allowedCalls(Set<State> current) {
     private Optional<String> newObjects(RefinedFunction call) {
         if (receiver.equals(Keys.THIS))
             return Optional.empty();
-        List<String> constructors = machine.constructorsEnabling(call).stream().map(StateHints::constructor).toList();
+        List<String> constructors = machine.constructorsEnabling(call).stream().map(StateHints::constructor).distinct()
+                .toList();
         return constructors.isEmpty() ? Optional.empty() : Optional.of(String.join(" or ", constructors));
     }
 

liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/object_checkers/AuxHierarchyRefinementsPassage.java

@@ -139,7 +139,7 @@ private static void transferStateRefinements(RefinedFunction superFunction, Refi
                     ObjectState subState = subStates.get(i);
 
                     String thisName = String.format(Formats.FRESH, tc.getContext().getCounter());
-                    createVariableInContext(thisName, tc, subFunction, superFunction, method.getParameters().get(i));
+                    createVariableInContext(thisName, tc, subFunction, superFunction, method);
 
                     Predicate superConst = matchVariableNames(thisName, superState.getFrom());
                     Predicate subConst = matchVariableNames(thisName, superFunction, subFunction, subState.getFrom());
@@ -164,9 +164,9 @@ private static void transferStateRefinements(RefinedFunction superFunction, Refi
     }
 
     private static void createVariableInContext(String thisName, TypeChecker tc, RefinedFunction subFunction,
-            RefinedFunction superFunction, CtParameter<?> ctParameter) {
+            RefinedFunction superFunction, CtMethod<?> method) {
         RefinedVariable rv = tc.getContext().addVarToContext(thisName,
-                Utils.getType(subFunction.getTargetClass(), tc.getFactory()), new Predicate(), ctParameter);
+                Utils.getType(subFunction.getTargetClass(), tc.getFactory()), new Predicate(), method);
         rv.addSuperType(Utils.getType(superFunction.getTargetClass(), tc.getFactory())); // TODO: change: this only
         // works for one superclass
     }