Check current receiver typestate across loops (#384)

A state change inside a loop must not establish the receiver state after
a loop that can run zero times. Main already havocs local receivers, but
calls on explicit and implicit `this` skipped receiver state checking
entirely. For example, `while (n > 0) { this.mark(); n--; }
this.reset();` incorrectly passed.

Initialize each instance method's receiver from its declared entry
states, resolve current `this` and unqualified `super` through the same
receiver predicate, and include that receiver in loop havoc. Qualified
outer receivers retain their existing handling. State-preserving methods
with multiple entry alternatives check the union of those preconditions,
so a wrapper accepting either state can call another method accepting
either state.

Add passing and failing regressions for local receivers in
while/for/foreach loops, explicit and implicit `this`, later iterations,
direct receiver calls, unconditional transitions after loops, and
multiple state-preserving entry alternatives.

Validation: `mvn -pl liquidjava-verifier test` — 389 tests, zero
failures or errors.

Precision remains conservative: loops forget changed receiver state, and
methods with alternative transitions that change state still require one
applicable alternative to be provable. This change does not initialize
constructor receivers or expand instance methods named `main`.

Closes #338.

Author: CatarinaGamboa

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

@@ -585,13 +585,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))