See state changes through aliases and forget mutable field initializers across methods

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

@@ -20,7 +20,8 @@ class CorrectDeferredCallbackState {
     UndoManager manager = new UndoManager();
     Runnable listener = () -> { manager.addEdit(null); };
 
-    void fieldCallbackMayNeverRun() {
+    CorrectDeferredCallbackState() {
+        // the field callback may never run: the initializer state still holds in the constructor
         manager.discardAllEdits();
     }
 

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

@@ -0,0 +1,39 @@
+package testSuite;
+
+import liquidjava.specification.Refinement;
+
+public class CorrectMutableFieldInitializer {
+    private final float fixed = 0.75f;
+
+    @Refinement("_ >= 0.0 && _ <= 1.0")
+    private float refined = 0.75f;
+
+    private float local = 0.75f;
+
+    public CorrectMutableFieldInitializer() {
+        use(local);
+    }
+
+    public void setRefined(@Refinement("_ >= 0.0 && _ <= 1.0") float v) {
+        this.refined = v;
+    }
+
+    public void setLocal(float v) {
+        this.local = v;
+    }
+
+    static void use(@Refinement("_ >= 0.0 && _ <= 1.0") float quality) {}
+
+    void writeFixed() {
+        use(fixed);
+    }
+
+    void writeRefined() {
+        use(refined);
+    }
+
+    void writeAfterAssignment() {
+        local = 0.5f;
+        use(local);
+    }
+}

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

@@ -0,0 +1,53 @@
+package testSuite;
+
+import liquidjava.specification.StateRefinement;
+import liquidjava.specification.StateSet;
+
+@StateSet({"open", "closed"})
+class SeparateResource {
+    @StateRefinement(to = "open(this)")
+    public SeparateResource() {}
+
+    @StateRefinement(from = "open(this)")
+    public void read() {}
+
+    @StateRefinement(from = "open(this)", to = "closed(this)")
+    public void close() {}
+}
+
+public class CorrectStateChangeThroughAlias {
+    static void distinctObjects() {
+        SeparateResource a = new SeparateResource();
+        SeparateResource b = new SeparateResource();
+        b.close();
+        a.read();
+    }
+
+    static void reassignmentBreaksAlias() {
+        SeparateResource a = new SeparateResource();
+        SeparateResource b = a;
+        b = new SeparateResource();
+        b.close();
+        a.read();
+    }
+
+    static void aliasSeesOpenState() {
+        SeparateResource a = new SeparateResource();
+        SeparateResource b = a;
+        b.read();
+        a.read();
+        a.close();
+    }
+
+    static void aliasClosedInBothBranches(boolean done) {
+        SeparateResource a = new SeparateResource();
+        SeparateResource b = a;
+        if (done) {
+            b.close();
+        } else {
+            a.close();
+        }
+        SeparateResource c = new SeparateResource();
+        c.read();
+    }
+}

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

@@ -23,9 +23,6 @@ class ErrorAnonymousCallbackState {
         Runnable listener = new Runnable() {
             public void run() { manager.addEdit(null); }
         };
-    }
-
-    void undo() {
         manager.undo(); // Expect: State Refinement Error
     }
 }
@@ -42,7 +39,7 @@ class ErrorFieldLambdaCallbackState {
     UndoManager manager = new UndoManager();
     Runnable listener = () -> { manager.addEdit(null); };
 
-    void undo() {
+    ErrorFieldLambdaCallbackState() {
         manager.undo(); // Expect: State Refinement Error
     }
 }

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

@@ -0,0 +1,55 @@
+package testSuite;
+
+import liquidjava.specification.Refinement;
+import liquidjava.specification.StateRefinement;
+import liquidjava.specification.StateSet;
+
+@StateSet({"open", "closed"})
+class FieldResource {
+    @StateRefinement(to = "open(this)")
+    public FieldResource() {}
+
+    @StateRefinement(from = "open(this)")
+    public void read() {}
+
+    @StateRefinement(from = "open(this)", to = "closed(this)")
+    public void close() {}
+}
+
+public class ErrorMutableFieldInitializer {
+    private float q = 0.75f;
+    private static int count = 1;
+    private FieldResource resource = new FieldResource();
+
+    public void setQ(float v) {
+        this.q = v;
+    }
+
+    public static void setCount(int c) {
+        count = c;
+    }
+
+    static void use(@Refinement("_ >= 0.0 && _ <= 1.0") float quality) {}
+
+    static void positive(@Refinement("_ > 0") int n) {}
+
+    void write() {
+        use(q); // Expect: Refinement Error
+    }
+
+    void writeThis() {
+        use(this.q); // Expect: Refinement Error
+    }
+
+    static void report() {
+        positive(count); // Expect: Refinement Error
+    }
+
+    void closeResource() {
+        resource.close(); // Expect: State Refinement Error
+    }
+
+    void readResource() {
+        resource.read(); // Expect: State Refinement Error
+    }
+}

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

@@ -0,0 +1,50 @@
+package testSuite;
+
+import liquidjava.specification.StateRefinement;
+import liquidjava.specification.StateSet;
+
+@StateSet({"open", "closed"})
+class AliasedResource {
+    @StateRefinement(to = "open(this)")
+    public AliasedResource() {}
+
+    @StateRefinement(from = "open(this)")
+    public void read() {}
+
+    @StateRefinement(from = "open(this)", to = "closed(this)")
+    public void close() {}
+}
+
+public class ErrorStateChangeThroughAlias {
+    static void localAlias() {
+        AliasedResource a = new AliasedResource();
+        AliasedResource b = a;
+        b.close();
+        a.read(); // Expect: State Refinement Error
+    }
+
+    static void aliasOfAlias() {
+        AliasedResource a = new AliasedResource();
+        AliasedResource b = a;
+        AliasedResource c = b;
+        a.close();
+        c.read(); // Expect: State Refinement Error
+    }
+
+    static void aliasAssignedLater() {
+        AliasedResource a = new AliasedResource();
+        AliasedResource b = new AliasedResource();
+        b = a;
+        b.close();
+        a.read(); // Expect: State Refinement Error
+    }
+
+    static void aliasClosedInBranch(boolean done) {
+        AliasedResource a = new AliasedResource();
+        AliasedResource b = a;
+        if (done) {
+            b.close();
+        }
+        a.read(); // Expect: State Refinement Error
+    }
+}

liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/RefinementTypeChecker.java

@@ -142,6 +142,7 @@ public <R> void visitCtMethod(CtMethod<R> method) {
         context.clearInstanceVariables();
         context.enterContext();
         context.restoreInstanceVariables();
+        forgetMutableFieldValues(method.getDeclaringType());
         if (!method.getSignature().equals("main(java.lang.String[])")) {
             mfc.loadFunctionInfo(method);
         }
@@ -155,6 +156,25 @@ public <R> void visitCtMethod(CtMethod<R> method) {
         vcChecker.clearPathVariables();
     }
 
+    /**
+     * Any method may have reassigned a non-final field before this one runs, so inside a method a non-final field
+     * carries only its declared refinement, not the value of its initializer. Final fields keep their value.
+     */
+    private void forgetMutableFieldValues(CtType<?> type) {
+        if (type == null)
+            return;
+        for (CtField<?> f : type.getFields()) {
+            String name = Utils.qualifyFieldName(f.getReference());
+            if (f.isFinal() || !(context.getVariableByName(name)instanceof Variable field)
+                    || field.getLastInstance().isEmpty())
+                continue;
+            String instanceName = String.format(Formats.INSTANCE, name, context.getCounter());
+            context.addInstanceToContext(instanceName, field.getType(),
+                    field.getMainRefinement().substituteVariable(name, instanceName), f);
+            context.addRefinementInstanceToVariable(name, instanceName);
+        }
+    }
+
     @Override
     public <T> void visitCtLocalVariable(CtLocalVariable<T> localVariable) {
         super.visitCtLocalVariable(localVariable);

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

@@ -618,6 +618,7 @@ private static void changeState(TypeChecker tc, VariableInstance vi, RefinedFunc
                 transitionedState = checkOldMentions(transitionedState, instanceName, newInstanceName);
                 // update of state of new instance of this#n#(whatever it was + 1)
                 addInstanceWithState(tc, name, newInstanceName, vi, transitionedState, invocation);
+                updateAliases(tc, name, vi, newInstanceName, invocation);
             }
         }
         if (!found) { // Reaches the end of stateChange no matching states
@@ -699,6 +700,54 @@ private static void addInstanceWithState(TypeChecker tc, String superName, Strin
         invocation.putMetadata(Keys.TARGET, vi2);
     }
 
+    /**
+     * A state change made through one reference changes the state of the object, so every other variable that must
+     * refer to the same object (e.g. {@code b} after {@code Res b = a;}) gets a new instance equal to the transitioned
+     * one. Variables that may, but need not, alias the target keep their state.
+     *
+     * @param tc
+     * @param name
+     *            the variable the state change was made through
+     * @param previous
+     *            the target instance before the state change
+     * @param transitioned
+     *            the name of the target instance after the state change
+     * @param invocation
+     */
+    private static void updateAliases(TypeChecker tc, String name, VariableInstance previous, String transitioned,
+            CtElement invocation) {
+        Context ctx = tc.getContext();
+        for (RefinedVariable rv : ctx.getCtxVars()) {
+            if (!(rv instanceof Variable alias) || alias.getName().equals(name) || !relatedTypes(alias, previous))
+                continue;
+            String current = alias.getLastInstance().map(Refined::getName).orElse(alias.getName());
+            Predicate identity = Predicate.createEquals(Predicate.createVar(current),
+                    Predicate.createVar(previous.getName()));
+            try {
+                if (!tc.checkStateSMT(new Predicate(), identity, invocation.getPosition(), true))
+                    continue;
+            } catch (LJError e) {
+                continue; // identity not provable: not a must-alias
+            }
+            String aliasInstanceName = String.format(Formats.INSTANCE, alias.getName(), ctx.getCounter());
+            RefinedVariable aliasInstance = ctx.addInstanceToContext(aliasInstanceName, alias.getType(),
+                    Predicate.createEquals(Predicate.createVar(aliasInstanceName), Predicate.createVar(transitioned)),
+                    invocation);
+            alias.getSuperTypes().forEach(aliasInstance::addSuperType);
+            ctx.addRefinementInstanceToVariable(alias.getName(), aliasInstanceName);
+        }
+    }
+
+    /** Whether one variable's type is the other's type or one of its recorded supertypes. */
+    private static boolean relatedTypes(RefinedVariable v1, RefinedVariable v2) {
+        if (v1.getType() == null || v2.getType() == null || v1.getType().isPrimitive() || v2.getType().isPrimitive())
+            return false;
+        String t1 = v1.getType().getQualifiedName();
+        String t2 = v2.getType().getQualifiedName();
+        return t1.equals(t2) || v1.getSuperTypes().stream().anyMatch(t -> t.getQualifiedName().equals(t2))
+                || v2.getSuperTypes().stream().anyMatch(t -> t.getQualifiedName().equals(t1));
+    }
+
     /** Whether the access denotes the receiver of the enclosing type, including unqualified super. */
     public static boolean isCurrentReceiver(CtElement target) {
         CtType<?> owner = target.getParent(CtType.class);