Check current receiver typestate across loops

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

@@ -0,0 +1,79 @@
+package testSuite;
+
+import liquidjava.specification.StateRefinement;
+import liquidjava.specification.StateSet;
+
+@StateSet({"open", "marked"})
+public class CorrectLoopPostState {
+    @StateRefinement(to = "open(this)")
+    CorrectLoopPostState() {}
+
+    @StateRefinement(to = "marked(this)")
+    void mark() {}
+
+    @StateRefinement(from = "marked(this)", to = "open(this)")
+    void reset() {}
+
+    @StateRefinement(from = "open(this)")
+    void use() {}
+
+    // A state-preserving call leaves the entry state available after the loop.
+    static void unchangedState(int n) {
+        CorrectLoopPostState b = new CorrectLoopPostState();
+        while (n > 0) {
+            b.use();
+            n--;
+        }
+        b.use();
+    }
+
+    // An unconditional transition after the loop establishes the required state.
+    static void establishStateAfterLoop(int n) {
+        CorrectLoopPostState b = new CorrectLoopPostState();
+        while (n > 0) {
+            b.mark();
+            n--;
+        }
+        b.mark();
+        b.reset();
+    }
+
+    @StateRefinement(from = "open(this)")
+    void unchangedThisState(int n) {
+        while (n > 0) {
+            this.use();
+            n--;
+        }
+        use();
+    }
+
+    @StateRefinement(from = "open(this)")
+    void establishThisStateAfterLoop(int n) {
+        while (n > 0) {
+            mark();
+            n--;
+        }
+        this.mark();
+        reset();
+    }
+
+    @StateRefinement(from = "open(this)")
+    void directValidTransitions() {
+        this.use();
+        mark();
+        this.reset();
+        use();
+    }
+
+    @StateRefinement(from = "open(this)")
+    @StateRefinement(from = "marked(this)")
+    void acceptEitherState() {}
+
+    // Neither alternative is known individually; the call accepts their union and preserves it.
+    @StateRefinement(from = "open(this)")
+    @StateRefinement(from = "marked(this)")
+    void wrapEitherState() {
+        acceptEitherState();
+        this.acceptEitherState();
+    }
+}

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

@@ -0,0 +1,90 @@
+package testSuite;
+
+import liquidjava.specification.StateRefinement;
+import liquidjava.specification.StateSet;
+
+@StateSet({"open", "marked"})
+public class ErrorLoopPostState {
+    @StateRefinement(to = "open(this)")
+    ErrorLoopPostState() {}
+
+    @StateRefinement(to = "marked(this)")
+    void mark() {}
+
+    @StateRefinement(from = "marked(this)", to = "open(this)")
+    void reset() {}
+
+    @StateRefinement(from = "open(this)")
+    void use() {}
+
+    // Issue #338: the loop may run zero times, leaving b open.
+    static void whileMayBeEmpty(int n) {
+        ErrorLoopPostState b = new ErrorLoopPostState();
+        int k = 0;
+        while (k < n) {
+            b.mark();
+            k++;
+        }
+        b.reset(); // Expect: State Refinement Error
+    }
+
+    static void forMayBeEmpty(int n) {
+        ErrorLoopPostState b = new ErrorLoopPostState();
+        for (int k = 0; k < n; k++) {
+            b.mark();
+        }
+        b.reset(); // Expect: State Refinement Error
+    }
+
+    static void forEachMayBeEmpty(int[] values) {
+        ErrorLoopPostState b = new ErrorLoopPostState();
+        for (int value : values) {
+            b.mark();
+        }
+        b.reset(); // Expect: State Refinement Error
+    }
+
+    @StateRefinement(from = "open(this)")
+    void explicitThisMayBeEmpty(int n) {
+        while (n > 0) {
+            this.mark();
+            n--;
+        }
+        this.reset(); // Expect: State Refinement Error
+    }
+
+    @StateRefinement(from = "open(this)")
+    void implicitThisMayBeEmpty(int n) {
+        while (n > 0) {
+            mark();
+            n--;
+        }
+        reset(); // Expect: State Refinement Error
+    }
+
+    @StateRefinement(from = "open(this)")
+    void laterIteration(int n) {
+        while (n > 0) {
+            use(); // Expect: State Refinement Error
+            mark();
+            n--;
+        }
+    }
+
+    @StateRefinement(from = "open(this)")
+    void directInvalidCall() {
+        this.reset(); // Expect: State Refinement Error
+    }
+
+    @StateRefinement(from = "open(this)")
+    void directInvalidSequence() {
+        mark();
+        use(); // Expect: State Refinement Error
+    }
+
+    @StateRefinement(from = "open(this)")
+    @StateRefinement(from = "marked(this)")
+    void unionDoesNotImplyOneState() {
+        use(); // Expect: State Refinement Error
+    }
+}

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

@@ -604,13 +604,17 @@ private void havocChangedIn(CtLoop loop) {
                 loop.getElements(new TypeFilter<CtVariableWrite<?>>(CtVariableWrite.class)));
         List<CtAbstractInvocation<?>> calls = loop
                 .getElements(new TypeFilter<CtAbstractInvocation<?>>(CtAbstractInvocation.class));
+        Set<String> names = new LinkedHashSet<>();
         for (CtAbstractInvocation<?> call : calls) {
-            if (call instanceof CtInvocation<?> inv && inv.getTarget()instanceof CtVariableAccess<?> target
+            if (call instanceof CtInvocation<?> inv
                     && context.getAllMethodsWithNameSize(inv.getExecutable().getSimpleName(), inv.getArguments().size())
-                            .stream().anyMatch(f -> f.getAllStates().stream().anyMatch(ObjectState::hasTo)))
-                changed.add(target);
+                            .stream().anyMatch(f -> f.getAllStates().stream().anyMatch(ObjectState::hasTo))) {
+                if (inv.getTarget()instanceof CtVariableAccess<?> target)
+                    changed.add(target);
+                else if (inv.getTarget() != null && AuxStateHandler.isCurrentReceiver(inv.getTarget()))
+                    names.add(Keys.THIS);
+            }
         }
-        Set<String> names = new LinkedHashSet<>();
         for (CtVariableAccess<?> access : changed) {
             CtVariable<?> declaration = access.getVariable().getDeclaration();
             if (declaration != null && declaration.hasParent(loop.getBody()))

liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/general_checkers/MethodsFunctionsChecker.java

@@ -19,6 +19,7 @@
 import liquidjava.utils.Utils;
 import liquidjava.utils.constants.Formats;
 import liquidjava.utils.constants.Keys;
+import liquidjava.utils.constants.Types;
 import spoon.reflect.code.CtConstructorCall;
 import spoon.reflect.code.CtExpression;
 import spoon.reflect.code.CtFieldRead;
@@ -446,6 +447,19 @@ public void loadFunctionInfo(CtExecutable<?> method) {
                 for (Variable v : lv)
                     rtc.getContext().addVarToContext(v);
             }
+            if (method instanceof CtMethod<?> instanceMethod && !instanceMethod.isStatic()) {
+                // The contract describes the entry state, not an invariant of every intermediate receiver state.
+                Predicate entry = fi == null || fi.getAllStates().isEmpty() ? new Predicate() : fi.getFromStates()
+                        .stream().reduce(Predicate.createLit("false", Types.BOOLEAN), Predicate::createDisjunction);
+                CtTypeReference<?> receiverType = rtc.getFactory().Type().createReference(className);
+                RefinedVariable receiver = rtc.getContext().addVarToContext(Keys.THIS, receiverType, new Predicate(),
+                        method);
+                receiver.addSuperTypes(receiverType.getSuperclass(), receiverType.getSuperInterfaces());
+                String instanceName = String.format(Formats.INSTANCE, Keys.THIS, rtc.getContext().getCounter());
+                rtc.getContext().addInstanceToContext(instanceName, receiverType,
+                        entry.substituteVariable(Keys.THIS, instanceName), method);
+                rtc.getContext().addRefinementInstanceToVariable(Keys.THIS, instanceName);
+            }
         }
     }
 }

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

@@ -564,8 +564,28 @@ private static void changeState(TypeChecker tc, VariableInstance vi, RefinedFunc
                 .substituteVariable(name, instanceName);
 
         boolean found = false;
+        boolean preservesState = stateChanges.stream().noneMatch(ObjectState::hasTo);
+        if (preservesState) {
+            // A state-preserving call accepts any of its entry states, including a disjunction of them.
+            Predicate expected = stateChanges.stream().filter(ObjectState::hasFrom).map(ObjectState::getFrom)
+                    .reduce(Predicate.createLit("false", Types.BOOLEAN), Predicate::createDisjunction)
+                    .substituteVariable(Keys.THIS, instanceName);
+            Predicate previous = prevState;
+            for (String parameter : map.keySet()) {
+                previous = previous.substituteVariable(parameter, map.get(parameter));
+                expected = expected.substituteVariable(parameter, map.get(parameter));
+            }
+            expected = expected.changeOldMentions(vi.getName(), instanceName);
+            try {
+                found = tc.checkStateSMT(previous, expected, invocation.getPosition());
+            } catch (SMTUnknownError error) {
+                error.setDeclarationPosition(stateChanges.stream().map(ObjectState::getFromPosition)
+                        .filter(Objects::nonNull).findFirst().orElse(function.getPlacementInCode().getPosition()));
+                throw error;
+            }
+        }
         for (ObjectState stateChange : stateChanges) { // TODO: only working for 1 state annotation
-            if (found)
+            if (found || preservesState)
                 break;
             if (!stateChange.hasFrom())
                 continue;
@@ -679,6 +699,18 @@ private static void addInstanceWithState(TypeChecker tc, String superName, Strin
         invocation.putMetadata(Keys.TARGET, vi2);
     }
 
+    /** 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);
+        if (owner == null)
+            return false;
+        if (target instanceof CtThisAccess<?> self)
+            return self.getType() != null && self.getType().getQualifiedName().equals(owner.getQualifiedName());
+        if (target instanceof CtSuperAccess<?> parent)
+            return parent.getTarget() == null || parent.getTarget().isImplicit();
+        return false;
+    }
+
     /**
      * Gets the name of the parent target and adds the closest target to the elem TARGET metadata
      *
@@ -687,10 +719,10 @@ private static void addInstanceWithState(TypeChecker tc, String superName, Strin
      * @return the name of the parent target
      */
     public static String prepareInvocationTarget(TypeChecker tc, CtElement target2, CtElement invocation) {
-        if (target2 instanceof CtVariableRead<?> v) {
+        if (target2 instanceof CtVariableRead<?> || isCurrentReceiver(target2)) {
             // v--------- field read
             // means invocation is in a form of `t.method(args)`
-            String name = v.getVariable().getSimpleName();
+            String name = target2 instanceof CtVariableRead<?> v ? v.getVariable().getSimpleName() : Keys.THIS;
             if (target2 instanceof CtFieldRead<?> fieldRead && fieldRead.getTarget() instanceof CtThisAccess<?>) {
                 String fieldName = Utils.qualifyFieldName(fieldRead.getVariable());
                 if (tc.getContext().hasVariable(fieldName))