From 28cc19ce2ccfd46693df64486500b2d4d8a57b1f Mon Sep 17 00:00:00 2001 From: Catarina Gamboa Date: Tue, 27 Oct 2026 17:54:07 +0000 Subject: [PATCH 1/9] Allow a state-changing call from a union of its entry states A method with several state refinements, such as `mark()` from open to marked or from marked, was refused on an object that is open or marked: each entry state was checked on its own, and neither is provable. Only state-preserving calls accepted the union. When no single entry state is provable but their union is, allow the call and give the object the state of any alternative whose entry state it may be in: the target state of an alternative with one, and the unchanged object for an alternative without. This is needed for objects whose state after a loop is the union of the states the loop may leave them in. Co-Authored-By: Claude Opus 5.5 --- .../CorrectStateChangeFromUnion.java | 38 ++++++++++ .../testSuite/ErrorStateChangeFromUnion.java | 36 +++++++++ .../object_checkers/AuxStateHandler.java | 76 ++++++++++++++++--- 3 files changed, 141 insertions(+), 9 deletions(-) create mode 100644 liquidjava-example/src/main/java/testSuite/CorrectStateChangeFromUnion.java create mode 100644 liquidjava-example/src/main/java/testSuite/ErrorStateChangeFromUnion.java diff --git a/liquidjava-example/src/main/java/testSuite/CorrectStateChangeFromUnion.java b/liquidjava-example/src/main/java/testSuite/CorrectStateChangeFromUnion.java new file mode 100644 index 00000000..804fc951 --- /dev/null +++ b/liquidjava-example/src/main/java/testSuite/CorrectStateChangeFromUnion.java @@ -0,0 +1,38 @@ +package testSuite; + +import liquidjava.specification.StateRefinement; +import liquidjava.specification.StateSet; + +// A call whose entry states are each unprovable but whose union is provable is allowed, and the object ends up in a +// state given by any alternative whose entry state it may be in +@StateSet({"open", "marked", "closed"}) +public class CorrectStateChangeFromUnion { + @StateRefinement(to = "open(this)") + CorrectStateChangeFromUnion() {} + + @StateRefinement(from = "open(this)", to = "marked(this)") + @StateRefinement(from = "marked(this)") + void mark() {} + + @StateRefinement(from = "marked(this)", to = "open(this)") + void reset() {} + + @StateRefinement(from = "open(this)", to = "closed(this)") + @StateRefinement(from = "marked(this)", to = "closed(this)") + void close() {} + + // open goes to marked, marked stays marked + @StateRefinement(from = "open(this)") + @StateRefinement(from = "marked(this)") + void markFromEither() { + mark(); + reset(); + } + + // both alternatives go to closed + @StateRefinement(from = "open(this)") + @StateRefinement(from = "marked(this)") + void closeFromEither() { + close(); + } +} diff --git a/liquidjava-example/src/main/java/testSuite/ErrorStateChangeFromUnion.java b/liquidjava-example/src/main/java/testSuite/ErrorStateChangeFromUnion.java new file mode 100644 index 00000000..4d518247 --- /dev/null +++ b/liquidjava-example/src/main/java/testSuite/ErrorStateChangeFromUnion.java @@ -0,0 +1,36 @@ +package testSuite; + +import liquidjava.specification.StateRefinement; +import liquidjava.specification.StateSet; + +@StateSet({"open", "marked", "closed"}) +public class ErrorStateChangeFromUnion { + @StateRefinement(to = "open(this)") + ErrorStateChangeFromUnion() {} + + @StateRefinement(from = "open(this)", to = "marked(this)") + @StateRefinement(from = "marked(this)") + void mark() {} + + @StateRefinement(from = "marked(this)", to = "open(this)") + void reset() {} + + @StateRefinement(from = "open(this)", to = "closed(this)") + @StateRefinement(from = "marked(this)") + void closeIfOpen() {} + + // closed is in no entry state of mark + @StateRefinement(from = "open(this)") + @StateRefinement(from = "closed(this)") + void markFromOpenOrClosed() { + mark(); // Expect: State Refinement Error + } + + // after closeIfOpen, the object is closed or still marked, so reset is not allowed + @StateRefinement(from = "open(this)") + @StateRefinement(from = "marked(this)") + void resetAfterEither() { + closeIfOpen(); + reset(); // Expect: State Refinement Error + } +} diff --git a/liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/object_checkers/AuxStateHandler.java b/liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/object_checkers/AuxStateHandler.java index 5b951912..2815c2e8 100644 --- a/liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/object_checkers/AuxStateHandler.java +++ b/liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/object_checkers/AuxStateHandler.java @@ -778,20 +778,15 @@ private static void changeState(TypeChecker tc, VariableInstance vi, RefinedFunc } if (found && stateChange.hasTo()) { String newInstanceName = String.format(Formats.INSTANCE, name, tc.getContext().getCounter()); - // Non-void: `_` is the return value; void: legacy alias for the new instance. - String returnViName = (String) invocation.getMetadata(Keys.RETURN_VAR_NAME); - String wildcardTarget = returnViName != null ? returnViName : newInstanceName; - Predicate transitionedState = stateChange.getTo().substituteVariable(Keys.WILDCARD, wildcardTarget) - .substituteVariable(Keys.THIS, newInstanceName); - for (String s : map.keySet()) { - transitionedState = transitionedState.substituteVariable(s, map.get(s)); - } - transitionedState = checkOldMentions(transitionedState, instanceName, newInstanceName); + Predicate transitionedState = transitionedState(stateChange, instanceName, newInstanceName, map, + invocation); // update of state of new instance of this#n#(whatever it was + 1) addInstanceWithState(tc, name, newInstanceName, vi, transitionedState, invocation) .setStateChange(new StateChange(function, stateChange, vi, invocation.getPosition())); } } + if (!found && !preservesState) + found = changeToStateOfAnyEntryState(tc, vi, function, name, map, invocation, prevState); if (!found) { // Reaches the end of stateChange no matching states Predicate expectedStatesDisjunction = stateChanges.stream().filter(ObjectState::hasFrom) .map(ObjectState::getFrom) @@ -890,6 +885,69 @@ private static String writtenReceiver(CtElement invocation) { return target == null || target.isImplicit() ? Keys.THIS : target.toString(); } + /** The state that {@code stateChange} gives the object after the call, as the instance {@code newInstanceName} */ + private static Predicate transitionedState(ObjectState stateChange, String instanceName, String newInstanceName, + Map map, CtElement invocation) { + // Non-void: `_` is the return value; void: legacy alias for the new instance. + String returnViName = (String) invocation.getMetadata(Keys.RETURN_VAR_NAME); + String wildcardTarget = returnViName != null ? returnViName : newInstanceName; + Predicate transitionedState = stateChange.getTo().substituteVariable(Keys.WILDCARD, wildcardTarget) + .substituteVariable(Keys.THIS, newInstanceName); + for (String s : map.keySet()) { + transitionedState = transitionedState.substituteVariable(s, map.get(s)); + } + return checkOldMentions(transitionedState, instanceName, newInstanceName); + } + + /** + * A call whose entry states are each unprovable but whose union is provable, e.g. on an object that is in one of + * two states after a loop. The call is allowed, and the object ends up in the state given by any alternative whose + * entry state it may be in: an alternative without a target state leaves the object as it was. + * + * @return whether the call is allowed + */ + private static boolean changeToStateOfAnyEntryState(TypeChecker tc, VariableInstance vi, RefinedFunction function, + String name, Map map, CtElement invocation, Predicate prevState) throws LJError { + List alternatives = function.getAllStates().stream().filter(ObjectState::hasFrom).toList(); + if (alternatives.size() < 2) + return false; + String instanceName = vi.getName(); + Predicate previous = prevState; + for (String parameter : map.keySet()) + previous = previous.substituteVariable(parameter, map.get(parameter)); + Predicate anyEntry = Predicate.createLit("false", Types.BOOLEAN); + for (ObjectState alternative : alternatives) + anyEntry = Predicate.createDisjunction(anyEntry, entryState(alternative, instanceName, map)); + try { + if (!tc.checkStateSMT(previous, anyEntry, invocation.getPosition())) + return false; + } catch (SMTUnknownError error) { + error.setDeclarationPosition(alternatives.get(0).getFromPosition()); + throw error; + } + + String newInstanceName = String.format(Formats.INSTANCE, name, tc.getContext().getCounter()); + Predicate unchanged = previous.substituteVariable(instanceName, newInstanceName); + Predicate after = Predicate.createLit("false", Types.BOOLEAN); + for (ObjectState alternative : alternatives) { + Predicate entry = entryState(alternative, instanceName, map); + Predicate exit = alternative.hasTo() + ? transitionedState(alternative, instanceName, newInstanceName, map, invocation) + : Predicate.createConjunction(entry.substituteVariable(instanceName, newInstanceName), unchanged); + after = Predicate.createDisjunction(after, Predicate.createConjunction(entry, exit)); + } + addInstanceWithState(tc, name, newInstanceName, vi, after, invocation); + return true; + } + + /** The entry state of {@code stateChange}, for the object {@code instanceName} */ + private static Predicate entryState(ObjectState stateChange, String instanceName, Map map) { + Predicate entry = stateChange.getFrom().substituteVariable(Keys.THIS, instanceName); + for (String parameter : map.keySet()) + entry = entry.substituteVariable(parameter, map.get(parameter)); + return entry.changeOldMentions(instanceName, instanceName); + } + private static Predicate checkOldMentions(Predicate transitionedState, String instanceName, String newInstanceName) { return transitionedState.changeOldMentions(instanceName, newInstanceName); From 11fc155d82890bf17f270b8c0ae9c38e308ec7fd Mon Sep 17 00:00:00 2001 From: Catarina Gamboa Date: Tue, 27 Oct 2026 17:54:07 +0000 Subject: [PATCH 2/9] Compute the typestate at a loop head as a fixpoint over its iterations A loop checked one iteration from havocked receivers, so a state set inside the body was either forgotten or kept after the loop, depending on whether a method of that name with a state change was found: - Methods specified with @ExternalRefinementsFor are registered under their qualified name, so the lookup missed them and the state set in the body was kept after the loop and in later iterations (a reset after a loop that marks may find the reader unmarked; a read after a close in the previous iteration passed). - When found, the object's state was unknown in the body and after the loop, so a call valid in every iteration was refused (a read in a loop that reads and marks). Now the states of each local object the loop may change, among the finitely many states of its class, start as the states before the loop and grow with the states at the end of each checked iteration (the end of the body and the continues) until they stop changing. The body is checked from them, and after the loop the object is in a state it may be in where the loop exits (its condition is false, or a break). Earlier iterations start from fewer states, so their errors are errors of the last one too; the errors they record without stopping (e.g. in a lambda) are dropped, so each is reported once. Fields are still havocked, since a call may change them. The method lookup now also matches externally specified methods. Closes #427. Co-Authored-By: Claude Opus 5.5 --- .../testSuite/CorrectLoopStateFixpoint.java | 113 ++++++++++ .../testSuite/ErrorLoopStateFixpoint.java | 53 +++++ .../BufferedReaderRefinements.java | 26 +++ .../loop_state_external_correct/Test.java | 106 ++++++++++ .../BufferedReaderRefinements.java | 26 +++ .../loop_state_external_error/Test.java | 98 +++++++++ .../refinement_checker/LoopTypestates.java | 160 ++++++++++++++ .../RefinementTypeChecker.java | 195 ++++++++++++++---- .../state_machine/StateMachineBuilder.java | 2 +- 9 files changed, 739 insertions(+), 40 deletions(-) create mode 100644 liquidjava-example/src/main/java/testSuite/CorrectLoopStateFixpoint.java create mode 100644 liquidjava-example/src/main/java/testSuite/ErrorLoopStateFixpoint.java create mode 100644 liquidjava-example/src/main/java/testSuite/classes/loop_state_external_correct/BufferedReaderRefinements.java create mode 100644 liquidjava-example/src/main/java/testSuite/classes/loop_state_external_correct/Test.java create mode 100644 liquidjava-example/src/main/java/testSuite/classes/loop_state_external_error/BufferedReaderRefinements.java create mode 100644 liquidjava-example/src/main/java/testSuite/classes/loop_state_external_error/Test.java create mode 100644 liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/LoopTypestates.java diff --git a/liquidjava-example/src/main/java/testSuite/CorrectLoopStateFixpoint.java b/liquidjava-example/src/main/java/testSuite/CorrectLoopStateFixpoint.java new file mode 100644 index 00000000..ed5bcff5 --- /dev/null +++ b/liquidjava-example/src/main/java/testSuite/CorrectLoopStateFixpoint.java @@ -0,0 +1,113 @@ +package testSuite; + +import liquidjava.specification.StateRefinement; +import liquidjava.specification.StateSet; + +// The states of an object at the start of every iteration of a loop are those before the loop and those at the end of +// any iteration, computed until they stop changing +@StateSet({"open", "marked", "closed"}) +public class CorrectLoopStateFixpoint { + @StateRefinement(to = "open(this)") + CorrectLoopStateFixpoint() {} + + @StateRefinement(from = "open(this)") + @StateRefinement(from = "marked(this)") + void read() {} + + @StateRefinement(from = "open(this)", to = "marked(this)") + @StateRefinement(from = "marked(this)") + void mark() {} + + @StateRefinement(from = "marked(this)", to = "open(this)") + void reset() {} + + @StateRefinement(from = "!closed(this)", to = "closed(this)") + void close() {} + + // b is open or marked in every iteration: both allow read and mark + static void openOrMarked(int n) { + CorrectLoopStateFixpoint b = new CorrectLoopStateFixpoint(); + for (int i = 0; i < n; i++) { + b.read(); + b.mark(); + } + b.read(); + b.close(); + } + + // the body restores the state it starts from + static void restoredInBody(int n) { + CorrectLoopStateFixpoint b = new CorrectLoopStateFixpoint(); + while (n > 0) { + b.mark(); + b.reset(); + n--; + } + b.mark(); + b.reset(); + } + + static void nestedLoops(int n) { + CorrectLoopStateFixpoint b = new CorrectLoopStateFixpoint(); + for (int i = 0; i < n; i++) { + for (int j = 0; j < i; j++) + b.mark(); + b.read(); + } + b.close(); + } + + static void doWhile(int n) { + CorrectLoopStateFixpoint b = new CorrectLoopStateFixpoint(); + do { + b.mark(); + n--; + } while (n > 0); + b.reset(); + } + + static void forEach(int[] values) { + CorrectLoopStateFixpoint b = new CorrectLoopStateFixpoint(); + for (int value : values) { + b.mark(); + b.read(); + } + b.read(); + } + + // the only exit is the break, with b marked + static void exitOnlyThroughBreak(int n) { + CorrectLoopStateFixpoint b = new CorrectLoopStateFixpoint(); + for (;;) { + b.mark(); + if (n > 3) + break; + b.reset(); + n++; + } + b.reset(); + } + + // a continue skips the close, which ends the loop with a return + static void continueOrClose(int n) { + CorrectLoopStateFixpoint b = new CorrectLoopStateFixpoint(); + for (int i = 0; i < n; i++) { + b.read(); + if (i < 5) + continue; + b.close(); + return; + } + b.close(); + } + + @StateRefinement(from = "open(this)") + void thisOpenOrMarked(int n) { + while (n > 0) { + read(); + this.mark(); + n--; + } + read(); + } +} diff --git a/liquidjava-example/src/main/java/testSuite/ErrorLoopStateFixpoint.java b/liquidjava-example/src/main/java/testSuite/ErrorLoopStateFixpoint.java new file mode 100644 index 00000000..8e3e520e --- /dev/null +++ b/liquidjava-example/src/main/java/testSuite/ErrorLoopStateFixpoint.java @@ -0,0 +1,53 @@ +package testSuite; + +import liquidjava.specification.StateRefinement; +import liquidjava.specification.StateSet; + +// The states of an object at the start of every iteration of a loop are those before the loop and those at the end of +// any iteration, computed until they stop changing +@StateSet({"first", "second", "third"}) +public class ErrorLoopStateFixpoint { + @StateRefinement(to = "first(this)") + ErrorLoopStateFixpoint() {} + + @StateRefinement(from = "first(this)", to = "second(this)") + @StateRefinement(from = "second(this)", to = "third(this)") + @StateRefinement(from = "third(this)") + void step() {} + + @StateRefinement(from = "first(this)") + @StateRefinement(from = "second(this)") + void early() {} + + @StateRefinement(from = "third(this)") + void last() {} + + // third is reached in the third iteration only, after the states grow twice + static void thirdIteration(int n) { + ErrorLoopStateFixpoint o = new ErrorLoopStateFixpoint(); + for (int i = 0; i < n; i++) { + o.early(); // Expect: State Refinement Error + o.step(); + } + } + + // after two steps in the loop, o may still be first or second + static void notEnoughIterations(int n) { + ErrorLoopStateFixpoint o = new ErrorLoopStateFixpoint(); + while (n > 0) { + o.step(); + o.step(); + n--; + } + o.last(); // Expect: State Refinement Error + } + + // the error in the lambda is reported once, although the loop body is checked from more than one set of states + static void errorInLambdaInLoop(int n) { + ErrorLoopStateFixpoint o = new ErrorLoopStateFixpoint(); + for (int i = 0; i < n; i++) { + o.step(); + Runnable r = () -> o.last(); // Expect: State Refinement Error + } + } +} diff --git a/liquidjava-example/src/main/java/testSuite/classes/loop_state_external_correct/BufferedReaderRefinements.java b/liquidjava-example/src/main/java/testSuite/classes/loop_state_external_correct/BufferedReaderRefinements.java new file mode 100644 index 00000000..4e0b9fcf --- /dev/null +++ b/liquidjava-example/src/main/java/testSuite/classes/loop_state_external_correct/BufferedReaderRefinements.java @@ -0,0 +1,26 @@ +package testSuite.classes.loop_state_external_correct; + +import liquidjava.specification.ExternalRefinementsFor; +import liquidjava.specification.StateRefinement; +import liquidjava.specification.StateSet; + +@ExternalRefinementsFor("java.io.BufferedReader") +@StateSet({"open", "marked", "closed"}) +public interface BufferedReaderRefinements { + @StateRefinement(to = "open(this)") + void BufferedReader(java.io.Reader in); + + @StateRefinement(from = "open(this)") + @StateRefinement(from = "marked(this)") + String readLine(); + + @StateRefinement(from = "open(this)", to = "marked(this)") + @StateRefinement(from = "marked(this)") + void mark(int readAheadLimit); + + @StateRefinement(from = "marked(this)", to = "open(this)") + void reset(); + + @StateRefinement(from = "!closed(this)", to = "closed(this)") + void close(); +} diff --git a/liquidjava-example/src/main/java/testSuite/classes/loop_state_external_correct/Test.java b/liquidjava-example/src/main/java/testSuite/classes/loop_state_external_correct/Test.java new file mode 100644 index 00000000..b3bed7f8 --- /dev/null +++ b/liquidjava-example/src/main/java/testSuite/classes/loop_state_external_correct/Test.java @@ -0,0 +1,106 @@ +package testSuite.classes.loop_state_external_correct; + +import java.io.BufferedReader; +import java.io.IOException; +import java.io.Reader; + +// Issue #427: the states of an object whose class has an external spec, computed over the iterations of a loop +public class Test { + // the body restores the state it starts from + static void markAndResetInLoop(Reader in, int n) throws IOException { + BufferedReader br = new BufferedReader(in); + int k = 0; + while (k < n) { + br.mark(100); + br.readLine(); + br.reset(); + k++; + } + br.mark(100); + br.reset(); + br.close(); + } + + // br is open or marked at the start of every iteration and after the loop + static void openOrMarked(Reader in, int n) throws IOException { + BufferedReader br = new BufferedReader(in); + for (int i = 0; i < n; i++) { + br.readLine(); + br.mark(100); + } + br.readLine(); + br.close(); + } + + static void doWhile(Reader in, int n) throws IOException { + BufferedReader br = new BufferedReader(in); + int k = 0; + do { + br.mark(100); + br.reset(); + k++; + } while (k < n); + br.close(); + } + + static void forEach(Reader in, int[] values) throws IOException { + BufferedReader br = new BufferedReader(in); + for (int value : values) { + br.mark(value); + br.readLine(); + } + br.readLine(); + br.close(); + } + + // marked on every path to the next iteration and to the exit + static void markBeforeContinueAndBreak(Reader in, int n) throws IOException { + BufferedReader br = new BufferedReader(in); + br.mark(100); + for (int i = 0; i < n; i++) { + br.reset(); + br.mark(100); + if (i > 2) + continue; + if (i > 5) + break; + } + br.reset(); + br.close(); + } + + // the inner loop leaves br open or marked, which the outer loop allows + static void nestedLoops(Reader in, int n) throws IOException { + BufferedReader br = new BufferedReader(in); + for (int i = 0; i < n; i++) { + br.readLine(); + for (int j = 0; j < i; j++) + br.mark(100); + } + br.close(); + } + + // the fix of the tabu-timetabling bug: mark before the inner loop + static void markBeforeInnerLoop(Reader in) throws IOException { + BufferedReader br = new BufferedReader(in); + String currentLine; + while ((currentLine = br.readLine()) != null) { + br.mark(10000); + String nextLine; + while ((nextLine = br.readLine()) != null && currentLine.equals(nextLine)) { + br.mark(10000); + } + br.reset(); + } + br.close(); + } + + // closed only when the loop ends + static void closeAfterLoop(Reader in) throws IOException { + BufferedReader br = new BufferedReader(in); + while (br.readLine() != null) { + br.readLine(); + } + br.close(); + } +} diff --git a/liquidjava-example/src/main/java/testSuite/classes/loop_state_external_error/BufferedReaderRefinements.java b/liquidjava-example/src/main/java/testSuite/classes/loop_state_external_error/BufferedReaderRefinements.java new file mode 100644 index 00000000..d2344617 --- /dev/null +++ b/liquidjava-example/src/main/java/testSuite/classes/loop_state_external_error/BufferedReaderRefinements.java @@ -0,0 +1,26 @@ +package testSuite.classes.loop_state_external_error; + +import liquidjava.specification.ExternalRefinementsFor; +import liquidjava.specification.StateRefinement; +import liquidjava.specification.StateSet; + +@ExternalRefinementsFor("java.io.BufferedReader") +@StateSet({"open", "marked", "closed"}) +public interface BufferedReaderRefinements { + @StateRefinement(to = "open(this)") + void BufferedReader(java.io.Reader in); + + @StateRefinement(from = "open(this)") + @StateRefinement(from = "marked(this)") + String readLine(); + + @StateRefinement(from = "open(this)", to = "marked(this)") + @StateRefinement(from = "marked(this)") + void mark(int readAheadLimit); + + @StateRefinement(from = "marked(this)", to = "open(this)") + void reset(); + + @StateRefinement(from = "!closed(this)", to = "closed(this)") + void close(); +} diff --git a/liquidjava-example/src/main/java/testSuite/classes/loop_state_external_error/Test.java b/liquidjava-example/src/main/java/testSuite/classes/loop_state_external_error/Test.java new file mode 100644 index 00000000..ae7a9d09 --- /dev/null +++ b/liquidjava-example/src/main/java/testSuite/classes/loop_state_external_error/Test.java @@ -0,0 +1,98 @@ +package testSuite.classes.loop_state_external_error; + +import java.io.BufferedReader; +import java.io.IOException; +import java.io.Reader; + +// Issue #427: the state after a loop, and at the start of every iteration, of an object whose class has an external +// spec +public class Test { + // the loop may run zero times, leaving br open + static void zeroIterations(Reader in, int n) throws IOException { + BufferedReader br = new BufferedReader(in); + int k = 0; + while (k < n) { + br.mark(100); + k++; + } + br.reset(); // Expect: State Refinement Error + } + + // from the second iteration on, br is closed + static void laterIteration(Reader in, int n) throws IOException { + BufferedReader br = new BufferedReader(in); + for (int i = 0; i < n; i++) { + br.readLine(); // Expect: State Refinement Error + br.close(); + } + } + + static void doWhileLaterIteration(Reader in, int n) throws IOException { + BufferedReader br = new BufferedReader(in); + int k = 0; + do { + br.readLine(); // Expect: State Refinement Error + br.close(); + k++; + } while (k < n); + } + + static void forEachMayBeEmpty(Reader in, int[] values) throws IOException { + BufferedReader br = new BufferedReader(in); + for (int value : values) { + br.mark(value); + } + br.reset(); // Expect: State Refinement Error + } + + // a continue goes on to the next iteration with br closed + static void closedBeforeContinue(Reader in, int n) throws IOException { + BufferedReader br = new BufferedReader(in); + for (int i = 0; i < n; i++) { + br.readLine(); // Expect: State Refinement Error + if (i > 2) { + br.close(); + continue; + } + } + } + + // the loop exits through its condition with br open, or through the break with br marked + static void breakOrCondition(Reader in, int n) throws IOException { + BufferedReader br = new BufferedReader(in); + int k = 0; + while (k < n) { + br.mark(100); + if (k > 2) + break; + br.reset(); + k++; + } + br.reset(); // Expect: State Refinement Error + } + + // marked by an inner loop, which may run zero times, in the second iteration of the outer one + static void nestedLoops(Reader in, int n) throws IOException { + BufferedReader br = new BufferedReader(in); + for (int i = 0; i < n; i++) { + br.reset(); // Expect: State Refinement Error + for (int j = 0; j < i; j++) + br.mark(100); + } + } + + // tabu-timetabling InputReader: the inner loop may stop at once, when the next line belongs to another student, + // and then reset runs without a mark ("Stream not marked") + static void markOnlyInInnerLoop(Reader in) throws IOException { + BufferedReader br = new BufferedReader(in); + String currentLine; + while ((currentLine = br.readLine()) != null) { + String nextLine; + while ((nextLine = br.readLine()) != null && currentLine.equals(nextLine)) { + br.mark(10000); + } + br.reset(); // Expect: State Refinement Error + } + br.close(); + } +} diff --git a/liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/LoopTypestates.java b/liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/LoopTypestates.java new file mode 100644 index 00000000..6b885fcc --- /dev/null +++ b/liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/LoopTypestates.java @@ -0,0 +1,160 @@ +package liquidjava.processor.refinement_checker; + +import java.util.LinkedHashMap; +import java.util.LinkedHashSet; +import java.util.List; +import java.util.Map; +import java.util.Optional; +import java.util.Set; + +import liquidjava.diagnostics.errors.LJError; +import liquidjava.processor.context.RefinedVariable; +import liquidjava.processor.context.Variable; +import liquidjava.processor.context.VariableInstance; +import liquidjava.processor.state_machine.State; +import liquidjava.processor.state_machine.StateMachineBuilder; +import liquidjava.processor.state_machine.StateSolver; +import liquidjava.rj_language.Predicate; +import liquidjava.utils.constants.Keys; +import liquidjava.utils.constants.Types; +import spoon.reflect.code.CtLoop; + +/** + * The typestates of the objects a loop may change, as sets of the states of their class. The states at the loop head + * start as the states before the loop and grow with the states at the end of each checked iteration until they stop + * changing. A class has finitely many states, so they stop changing after at most one growth per state. + * + *

+ * While the body is checked, the states where control leaves the iteration are recorded: where it may exit the loop + * (the condition, a break), and where it goes on to the next iteration (the end of the body, a continue). + */ +class LoopTypestates { + + private final RefinementTypeChecker checker; + private final CtLoop loop; + private final Map> classStates = new LinkedHashMap<>(); + private final Map> head = new LinkedHashMap<>(); + private Map> exit; + private Map> continued; + private Map> nextIteration; + // whether the point of the iteration being checked can be reached + private boolean reachable; + + /** + * @param changed + * the variables the loop may change, of which those whose class has states are tracked + */ + LoopTypestates(RefinementTypeChecker checker, CtLoop loop, Set changed) throws LJError { + this.checker = checker; + this.loop = loop; + for (String name : changed) { + if (!(checker.getContext().getVariableByName(name)instanceof Variable variable) + || variable.getType() == null) + continue; + List states = StateMachineBuilder.statesOf(checker.getContext(), + variable.getType().getQualifiedName()); + if (states.isEmpty()) + continue; + classStates.put(name, states); + head.put(name, currentStates(name)); + } + } + + /** The variables whose typestate is tracked, which must not be havocked */ + Set tracked() { + return classStates.keySet(); + } + + CtLoop loop() { + return loop; + } + + /** Starts checking an iteration: each tracked object is in one of the states at the loop head */ + void startIteration() { + head.forEach(this::setStates); + exit = emptyStates(); + continued = emptyStates(); + nextIteration = emptyStates(); + reachable = true; + } + + /** The loop may exit here, if this point is reachable (the condition of a do-while is not, after a return) */ + void recordExit() throws LJError { + if (reachable) + addCurrentStates(exit); + } + + void recordBreak() throws LJError { + addCurrentStates(exit); + } + + void recordContinue() throws LJError { + addCurrentStates(continued); + } + + /** + * Where the body ends, a continue joins the end of the body: from here, each object is in a state it may be in at + * either + * + * @param completes + * whether the end of the body can be reached without a continue + */ + void endBody(boolean completes) throws LJError { + if (continued.values().stream().allMatch(Set::isEmpty)) { + reachable = completes; + return; + } + if (completes) + recordContinue(); + continued.forEach(this::setStates); + reachable = true; + } + + /** The next iteration starts here, if this point is reachable */ + void recordNextIteration() throws LJError { + if (reachable) + addCurrentStates(nextIteration); + } + + /** + * Adds the states at the start of the next iteration to the states at the loop head + * + * @return whether they were already there, so the iteration just checked is the last one to check + */ + boolean reachedFixpoint() { + boolean grown = false; + for (String name : tracked()) + grown |= head.get(name).addAll(nextIteration.get(name)); + return !grown; + } + + /** After the loop, each tracked object is in a state it may be in where the loop exits */ + void finishLoop() { + exit.forEach(this::setStates); + } + + private Map> emptyStates() { + Map> states = new LinkedHashMap<>(); + tracked().forEach(name -> states.put(name, new LinkedHashSet<>())); + return states; + } + + private void addCurrentStates(Map> states) throws LJError { + for (String name : tracked()) + states.get(name).addAll(currentStates(name)); + } + + private Set currentStates(String name) throws LJError { + Optional instance = checker.getContext().getLastVariableInstance(name); + String current = instance.map(RefinedVariable::getName).orElse(name); + return new StateSolver(checker, loop.getPosition()).possibleStates(classStates.get(name), new Predicate(), + current); + } + + /** Gives the object a new instance, known only to be in one of {@code states} */ + private void setStates(String name, Set states) { + Predicate inAnyState = states.stream().map(State::predicate).reduce(Predicate::createDisjunction) + .orElseGet(() -> Predicate.createLit("false", Types.BOOLEAN)); + checker.forgetChanges(name, inAnyState, loop); + } +} diff --git a/liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/RefinementTypeChecker.java b/liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/RefinementTypeChecker.java index 3b6e3ac8..32434b0d 100644 --- a/liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/RefinementTypeChecker.java +++ b/liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/RefinementTypeChecker.java @@ -1,12 +1,16 @@ package liquidjava.processor.refinement_checker; import java.lang.annotation.Annotation; +import java.util.ArrayDeque; import java.util.ArrayList; import java.util.Arrays; +import java.util.Deque; import java.util.LinkedHashSet; import java.util.List; import java.util.Optional; import java.util.Set; +import java.util.function.Consumer; +import java.util.stream.Collectors; import liquidjava.diagnostics.Diagnostics; import liquidjava.diagnostics.errors.LJError; @@ -43,6 +47,7 @@ import spoon.reflect.code.CtFor; import spoon.reflect.code.CtForEach; import spoon.reflect.code.CtIf; +import spoon.reflect.code.CtLabelledFlowBreak; import spoon.reflect.code.CtInvocation; import spoon.reflect.code.CtLambda; import spoon.reflect.code.CtLiteral; @@ -54,6 +59,8 @@ import spoon.reflect.code.CtReturn; import spoon.reflect.code.CtStatement; import spoon.reflect.code.CtSuperAccess; +import spoon.reflect.code.CtSwitch; +import spoon.reflect.code.CtSwitchExpression; import spoon.reflect.code.CtThisAccess; import spoon.reflect.code.CtThrow; import spoon.reflect.code.CtTry; @@ -82,6 +89,8 @@ public class RefinementTypeChecker extends TypeChecker { TryChecker tryChecker; Diagnostics diagnostics = Diagnostics.getInstance(); ContextHistory contextHistory = ContextHistory.getInstance(); + // the loops being checked, innermost first + private final Deque loops = new ArrayDeque<>(); public RefinementTypeChecker(Context context, Factory factory) { super(context, factory); @@ -664,71 +673,171 @@ public void visitCtTryWithResource(CtTryWithResource tryWithResource) { @Override public void visitCtWhile(CtWhile whileLoop) { - visitLoop(whileLoop, () -> { + visitLoop(whileLoop, states -> { scan(whileLoop.getLoopingExpression()); + recordExit(states, whileLoop.getLoopingExpression()); assumeLoopCondition(whileLoop.getLoopingExpression()); - scan(whileLoop.getBody()); + scanBody(whileLoop, states); + states.recordNextIteration(); }); } @Override public void visitCtFor(CtFor forLoop) { scan(forLoop.getForInit()); - visitLoop(forLoop, () -> { + visitLoop(forLoop, states -> { scan(forLoop.getExpression()); + recordExit(states, forLoop.getExpression()); assumeLoopCondition(forLoop.getExpression()); - List pathVariables = vcChecker.getPathVariables(); - CtStatement body = forLoop.getBody(); // null for an empty statement body, as in for (...); - scan(body); - if (body != null && !body.getElements(new TypeFilter<>(CtContinue.class)).isEmpty()) { - // a continue reaches the update from any point of the body, skipping its facts and assignments - vcChecker.restorePathVariables(pathVariables); - havocChangedIn(forLoop); - } + scanBody(forLoop, states); // the update runs after the body, so the body sees the values the condition was checked on scan(forLoop.getForUpdate()); + states.recordNextIteration(); }); } @Override public void visitCtDo(CtDo doLoop) { - // the condition is not checked before the first iteration, so it is not assumed in the body - visitLoop(doLoop, () -> super.visitCtDo(doLoop)); + visitLoop(doLoop, states -> { + // the condition is not checked before the first iteration, so it is not assumed in the body + scanBody(doLoop, states); + scan(doLoop.getLoopingExpression()); + recordExit(states, doLoop.getLoopingExpression()); + states.recordNextIteration(); + }); } @Override public void visitCtForEach(CtForEach forEach) { - visitLoop(forEach, () -> super.visitCtForEach(forEach)); + // the iterable is evaluated once, before the first iteration + scan(forEach.getExpression()); + visitLoop(forEach, states -> { + states.recordExit(); + scan(forEach.getVariable()); + scanBody(forEach, states); + states.recordNextIteration(); + }); + } + + @Override + public void visitCtBreak(CtBreak breakStatement) { + super.visitCtBreak(breakStatement); + loopLeftBy(breakStatement).ifPresent(LoopTypestates::recordBreak); + } + + @Override + public void visitCtContinue(CtContinue continueStatement) { + super.visitCtContinue(continueStatement); + loopLeftBy(continueStatement).ifPresent(LoopTypestates::recordContinue); } /** - * Checks one arbitrary iteration of a loop: what the loop may change is havocked (keeps only its declared - * refinement, which every assignment re-checks) before it and again after it, since the loop may run any number of - * times. Path conditions added inside the loop (e.g. the loop condition, or an {@code if (...) break;}) are dropped - * after it. + * Checks a loop for any number of iterations. What the loop may change is havocked (keeps only its declared + * refinement, which every assignment re-checks) before it and again after it, except the typestates of the local + * objects it may change, which are computed over its iterations (see {@link LoopTypestates}). Path conditions added + * inside the loop (e.g. the loop condition, or an {@code if (...) break;}) are dropped after it. */ - private void visitLoop(CtLoop loop, Runnable iteration) { + private void visitLoop(CtLoop loop, Consumer iteration) { List pathVariables = vcChecker.getPathVariables(); - havocChangedIn(loop); - iteration.run(); + // a field may also change in a method the loop calls, out of sight here, so fields are only havocked + Set locals = changedIn(loop).stream().filter(name -> !isField(name)) + .collect(Collectors.toCollection(LinkedHashSet::new)); + LoopTypestates states = new LoopTypestates(this, loop, locals); + havocChangedIn(loop, states.tracked()); + loops.push(states); + try { + checkUntilFixpoint(states, iteration); + } finally { + loops.pop(); + } vcChecker.restorePathVariables(pathVariables); - havocChangedIn(loop); + havocChangedIn(loop, states.tracked()); + states.finishLoop(); } /** - * Havocs what the loop may change: the variables it writes, the objects it calls state-changing methods on, and the - * fields if it calls any method or constructor (which may write them) + * Checks iterations of a loop from the typestates at its head until they stop changing. Only the last iteration + * checked keeps its diagnostics: an earlier one starts from fewer states, so an error it throws, which stops the + * check, is also an error from the final states. */ - private void havocChangedIn(CtLoop loop) { + private void checkUntilFixpoint(LoopTypestates states, Consumer iteration) { + List pathVariables = vcChecker.getPathVariables(); + while (true) { + Set errors = new LinkedHashSet<>(diagnostics.getErrors()); + states.startIteration(); + iteration.accept(states); + if (states.reachedFixpoint()) + return; + diagnostics.getErrors().retainAll(errors); + vcChecker.replacePathVariables(pathVariables); + } + } + + /** The loop exits where its condition is false: never if it has none, or if it is {@code true} */ + private void recordExit(LoopTypestates states, CtExpression condition) { + if (condition == null) + return; + RefinedVariable conditionIsFalse = assumeCondition(condition, false); + states.recordExit(); + if (conditionIsFalse != null) + vcChecker.removePathVariable(conditionIsFalse); + } + + /** Checks the body of a loop, up to the point after it where its continues join */ + private void scanBody(CtLoop loop, LoopTypestates states) { + List pathVariables = vcChecker.getPathVariables(); + CtStatement body = loop.getBody(); // null for an empty statement body, as in for (...); + scan(body); + if (body != null && !body.getElements(new TypeFilter<>(CtContinue.class)).isEmpty()) { + // a continue reaches the end of the body from any point of it, skipping its facts and assignments + vcChecker.restorePathVariables(pathVariables); + havocChangedIn(loop, states.tracked()); + } + states.endBody(canCompleteNormally(body)); + } + + /** The loop being checked that {@code jump} leaves, if any (an unlabeled break in a switch leaves the switch) */ + private Optional loopLeftBy(CtLabelledFlowBreak jump) { + CtElement target = jump.getTargetLabel() != null ? jump.getLabelledStatement() + : jump.getParent(e -> e instanceof CtLoop || jump instanceof CtBreak + && (e instanceof CtSwitch || e instanceof CtSwitchExpression)); + return loops.stream().filter(states -> states.loop() == target).findFirst(); + } + + /** Havocs what the loop may change, except the {@code tracked} typestates */ + private void havocChangedIn(CtLoop loop, Set tracked) { + for (String name : changedIn(loop)) + if (!tracked.contains(name)) + forgetChanges(name, new Predicate(), loop); + } + + /** + * Gives a variable a new instance that keeps only its declared refinement and {@code known}, since the facts on its + * previous instances may no longer hold + */ + void forgetChanges(String name, Predicate known, CtElement element) { + if (!(context.getVariableByName(name)instanceof Variable variable)) + return; + vcChecker.removePathVariableThatIncludes(name); + String instanceName = String.format(Formats.INSTANCE, name, context.getCounter()); + Predicate declared = variable.getMainRefinement().substituteVariable(name, instanceName); + context.addInstanceToContext(instanceName, variable.getType(), + Predicate.createConjunction(declared, known.substituteVariable(Keys.THIS, instanceName)), element); + context.addRefinementInstanceToVariable(name, instanceName); + } + + /** + * What the loop may change: the variables it writes, the objects it calls state-changing methods on, and the fields + * if it calls any method or constructor (which may write them) + */ + private Set changedIn(CtLoop loop) { List> changed = new ArrayList<>( loop.getElements(new TypeFilter>(CtVariableWrite.class))); List> calls = loop .getElements(new TypeFilter>(CtAbstractInvocation.class)); Set names = new LinkedHashSet<>(); for (CtAbstractInvocation call : calls) { - if (call instanceof CtInvocation inv - && context.getAllMethodsWithNameSize(inv.getExecutable().getSimpleName(), inv.getArguments().size()) - .stream().anyMatch(f -> f.getAllStates().stream().anyMatch(ObjectState::hasTo))) { + if (call instanceof CtInvocation inv && mayChangeState(inv)) { if (inv.getTarget()instanceof CtVariableAccess target) changed.add(target); else if (inv.getTarget() != null && AuxStateHandler.isCurrentReceiver(inv.getTarget())) @@ -743,17 +852,25 @@ else if (inv.getTarget() != null && AuxStateHandler.isCurrentReceiver(inv.getTar names.add(access instanceof CtFieldAccess ? String.format(Formats.THIS, name) : name); } if (!calls.isEmpty()) - context.getCtxVars().stream().map(RefinedVariable::getName) - .filter(n -> n.startsWith(String.format(Formats.THIS, ""))).forEach(names::add); - for (String name : names) { - if (!(context.getVariableByName(name)instanceof Variable variable)) - continue; - vcChecker.removePathVariableThatIncludes(name); - String instanceName = String.format(Formats.INSTANCE, name, context.getCounter()); - Predicate declared = variable.getMainRefinement().substituteVariable(name, instanceName); - context.addInstanceToContext(instanceName, variable.getType(), declared, loop); - context.addRefinementInstanceToVariable(name, instanceName); - } + context.getCtxVars().stream().map(RefinedVariable::getName).filter(RefinementTypeChecker::isField) + .forEach(names::add); + return names; + } + + /** Whether a name in the context is that of a field of this */ + private static boolean isField(String name) { + return name.startsWith(String.format(Formats.THIS, "")); + } + + /** + * Whether some method with the name and arity of the invoked one changes the state of its receiver. Methods + * specified externally are registered under their qualified name. + */ + private boolean mayChangeState(CtInvocation invocation) { + String name = invocation.getExecutable().getSimpleName(); + int arity = invocation.getArguments().size(); + return context.getCtxFunctions().stream().anyMatch(f -> Utils.getSimpleName(f.getName()).equals(name) + && f.getArguments().size() == arity && f.getAllStates().stream().anyMatch(ObjectState::hasTo)); } /** diff --git a/liquidjava-verifier/src/main/java/liquidjava/processor/state_machine/StateMachineBuilder.java b/liquidjava-verifier/src/main/java/liquidjava/processor/state_machine/StateMachineBuilder.java index 3713e034..173a05ae 100644 --- a/liquidjava-verifier/src/main/java/liquidjava/processor/state_machine/StateMachineBuilder.java +++ b/liquidjava-verifier/src/main/java/liquidjava/processor/state_machine/StateMachineBuilder.java @@ -81,7 +81,7 @@ public static Optional build(TypeChecker tc, StateSolver solver, S } /** Every combination of one state from each state set of the class */ - private static List statesOf(Context context, String className) { + public static List statesOf(Context context, String className) { List ghostStates = context.getGhostState(Utils.getSimpleName(className)); if (ghostStates == null) return List.of(); From 5ea9c035214a247f8e883ecd1ab14a98c44529f1 Mon Sep 17 00:00:00 2001 From: Catarina Gamboa Date: Tue, 27 Oct 2026 21:23:02 +0000 Subject: [PATCH 3/9] Substitute call arguments in state predicates in one place The entry, target and union checks of a state-changing call each substituted the arguments for the parameters in their own loop. Co-Authored-By: Claude Opus 5.5 --- .../object_checkers/AuxStateHandler.java | 44 +++++++------------ 1 file changed, 16 insertions(+), 28 deletions(-) diff --git a/liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/object_checkers/AuxStateHandler.java b/liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/object_checkers/AuxStateHandler.java index 2815c2e8..32b31203 100644 --- a/liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/object_checkers/AuxStateHandler.java +++ b/liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/object_checkers/AuxStateHandler.java @@ -741,12 +741,8 @@ private static void changeState(TypeChecker tc, VariableInstance vi, RefinedFunc 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); + Predicate previous = substituteArguments(prevState, map); + expected = substituteArguments(expected, map).changeOldMentions(vi.getName(), instanceName); try { found = tc.checkStateSMT(previous, expected, invocation.getPosition()); } catch (SMTUnknownError error) { @@ -761,14 +757,8 @@ private static void changeState(TypeChecker tc, VariableInstance vi, RefinedFunc if (!stateChange.hasFrom()) continue; - // replace "state(this)" to "state(whatever method is called from) and so on" - Predicate expectState = stateChange.getFrom().substituteVariable(Keys.THIS, instanceName); - Predicate prevCheck = prevState; - for (String s : map.keySet()) { // substituting function variables into annotation if there are any - prevCheck = prevCheck.substituteVariable(s, map.get(s)); - expectState = expectState.substituteVariable(s, map.get(s)); - } - expectState = expectState.changeOldMentions(vi.getName(), instanceName); + Predicate expectState = entryState(stateChange, instanceName, map); + Predicate prevCheck = substituteArguments(prevState, map); try { found = tc.checkStateSMT(prevCheck, expectState, invocation.getPosition()); @@ -791,11 +781,9 @@ private static void changeState(TypeChecker tc, VariableInstance vi, RefinedFunc Predicate expectedStatesDisjunction = stateChanges.stream().filter(ObjectState::hasFrom) .map(ObjectState::getFrom) .reduce(Predicate.createLit("false", Types.BOOLEAN), Predicate::createDisjunction); - expectedStatesDisjunction = expectedStatesDisjunction.substituteVariable(Keys.THIS, instanceName); - for (String s : map.keySet()) { - expectedStatesDisjunction = expectedStatesDisjunction.substituteVariable(s, map.get(s)); - } - expectedStatesDisjunction = expectedStatesDisjunction.changeOldMentions(vi.getName(), instanceName); + expectedStatesDisjunction = substituteArguments( + expectedStatesDisjunction.substituteVariable(Keys.THIS, instanceName), map) + .changeOldMentions(vi.getName(), instanceName); // combine messages of all state changes String message = stateChanges.stream().map(ObjectState::getMessage) @@ -893,10 +881,7 @@ private static Predicate transitionedState(ObjectState stateChange, String insta String wildcardTarget = returnViName != null ? returnViName : newInstanceName; Predicate transitionedState = stateChange.getTo().substituteVariable(Keys.WILDCARD, wildcardTarget) .substituteVariable(Keys.THIS, newInstanceName); - for (String s : map.keySet()) { - transitionedState = transitionedState.substituteVariable(s, map.get(s)); - } - return checkOldMentions(transitionedState, instanceName, newInstanceName); + return checkOldMentions(substituteArguments(transitionedState, map), instanceName, newInstanceName); } /** @@ -912,9 +897,7 @@ private static boolean changeToStateOfAnyEntryState(TypeChecker tc, VariableInst if (alternatives.size() < 2) return false; String instanceName = vi.getName(); - Predicate previous = prevState; - for (String parameter : map.keySet()) - previous = previous.substituteVariable(parameter, map.get(parameter)); + Predicate previous = substituteArguments(prevState, map); Predicate anyEntry = Predicate.createLit("false", Types.BOOLEAN); for (ObjectState alternative : alternatives) anyEntry = Predicate.createDisjunction(anyEntry, entryState(alternative, instanceName, map)); @@ -943,9 +926,14 @@ private static boolean changeToStateOfAnyEntryState(TypeChecker tc, VariableInst /** The entry state of {@code stateChange}, for the object {@code instanceName} */ private static Predicate entryState(ObjectState stateChange, String instanceName, Map map) { Predicate entry = stateChange.getFrom().substituteVariable(Keys.THIS, instanceName); + return substituteArguments(entry, map).changeOldMentions(instanceName, instanceName); + } + + /** Replaces the parameters of the called method with the arguments of the call, as given by {@code map} */ + private static Predicate substituteArguments(Predicate predicate, Map map) { for (String parameter : map.keySet()) - entry = entry.substituteVariable(parameter, map.get(parameter)); - return entry.changeOldMentions(instanceName, instanceName); + predicate = predicate.substituteVariable(parameter, map.get(parameter)); + return predicate; } private static Predicate checkOldMentions(Predicate transitionedState, String instanceName, From f1fd0f588f6974006653a38b5058c88285f7143d Mon Sep 17 00:00:00 2001 From: Catarina Gamboa Date: Tue, 27 Oct 2026 21:23:02 +0000 Subject: [PATCH 4/9] Check each loop iteration from the same facts, and follow only recorded jumps Review of the loop typestate fixpoint found programs it accepted and main rejected: - An iteration started from the values the previous one left: in `int x = 100; while (x < 10) { b.close(); x = 0; }` the last check had x == 0, so the loop could not exit through its condition, no state was possible after it, and every later check passed. A lambda error in the first iteration was lost the same way. Each iteration is now checked in its own context scope, so what it adds (instances, variables, path conditions) is dropped after it, and all iterations start from the facts before the loop with what it changes havocked. - A labelled block ending the body (`done: { break done; }`) was taken as never completing, hiding the next iteration. A statement that a labelled break leaves now completes normally. - A break to a labelled block around the loop, or through a finally or try-with-resources, recorded its state nowhere or before the cleanup ran. Loops with such jumps havoc their objects' typestates, as main. As a guard, an object with no state where the loop exits is havocked, since Java rejects code after a loop that never exits. Also: the simple-name lookup of functions is indexed in the context, and jump targets are resolved in one helper. Co-Authored-By: Claude Opus 5.5 --- .../java/testSuite/ErrorLoopStateJumps.java | 76 ++++++++++++++++ .../java/testSuite/ErrorLoopStatePasses.java | 49 +++++++++++ .../liquidjava/processor/context/Context.java | 13 ++- .../refinement_checker/LoopTypestates.java | 22 +++-- .../RefinementTypeChecker.java | 87 +++++++++++++++---- 5 files changed, 222 insertions(+), 25 deletions(-) create mode 100644 liquidjava-example/src/main/java/testSuite/ErrorLoopStateJumps.java create mode 100644 liquidjava-example/src/main/java/testSuite/ErrorLoopStatePasses.java diff --git a/liquidjava-example/src/main/java/testSuite/ErrorLoopStateJumps.java b/liquidjava-example/src/main/java/testSuite/ErrorLoopStateJumps.java new file mode 100644 index 00000000..9743901f --- /dev/null +++ b/liquidjava-example/src/main/java/testSuite/ErrorLoopStateJumps.java @@ -0,0 +1,76 @@ +package testSuite; + +import liquidjava.specification.StateRefinement; +import liquidjava.specification.StateSet; + +// Typestates through the jumps in a loop body +@StateSet({"open", "marked", "closed"}) +public class ErrorLoopStateJumps { + @StateRefinement(to = "open(this)") + ErrorLoopStateJumps() {} + + @StateRefinement(from = "open(this)", to = "marked(this)") + @StateRefinement(from = "marked(this)") + void mark() {} + + @StateRefinement(from = "marked(this)", to = "open(this)") + void reset() {} + + @StateRefinement(from = "!closed(this)", to = "closed(this)") + void close() {} + + @StateRefinement(from = "open(this)") + void needOpen() {} + + // a break out of a labelled block at the end of the body still goes on to the next iteration + static void labelledBlockEndsBody(int n) { + ErrorLoopStateJumps b = new ErrorLoopStateJumps(); + while (n > 0) { + b.close(); // Expect: State Refinement Error + n--; + done: { + break done; + } + } + } + + static void labelledBlockEndsDoWhileBody(int n) { + ErrorLoopStateJumps b = new ErrorLoopStateJumps(); + do { + b.close(); // Expect: State Refinement Error + n--; + done: { + break done; + } + } while (n > 0); + } + + // the break leaves the loop and the enclosing labelled block with b marked + static void breakOutOfEnclosingBlock(int n) { + ErrorLoopStateJumps b = new ErrorLoopStateJumps(); + out: { + while (n > 0) { + b.mark(); // Expect: State Refinement Error + if (n == 3) + break out; + b.reset(); + n--; + } + } + b.needOpen(); + } + + // the finally closes b after the break, so b is closed after the loop + static void breakThroughFinally() { + ErrorLoopStateJumps b = new ErrorLoopStateJumps(); + while (true) { + try { + b.mark(); // Expect: State Refinement Error + break; + } finally { + b.close(); + } + } + b.reset(); + } +} diff --git a/liquidjava-example/src/main/java/testSuite/ErrorLoopStatePasses.java b/liquidjava-example/src/main/java/testSuite/ErrorLoopStatePasses.java new file mode 100644 index 00000000..4d07a1f5 --- /dev/null +++ b/liquidjava-example/src/main/java/testSuite/ErrorLoopStatePasses.java @@ -0,0 +1,49 @@ +package testSuite; + +import liquidjava.specification.Refinement; +import liquidjava.specification.StateRefinement; +import liquidjava.specification.StateSet; + +// Each check of a loop body starts from the same facts: the values left by an earlier check must not leak into it +@StateSet({"open", "closed"}) +public class ErrorLoopStatePasses { + @StateRefinement(to = "open(this)") + ErrorLoopStatePasses() {} + + @StateRefinement(to = "closed(this)") + void close() {} + + @StateRefinement(from = "closed(this)", to = "open(this)") + void reopen() {} + + @StateRefinement(from = "open(this)", to = "closed(this)") + @StateRefinement(from = "closed(this)", to = "open(this)") + void toggle() {} + + // the loop is never entered, so b is still open; x == 0 from the previous check must not make the exit impossible + static void neverEntered() { + ErrorLoopStatePasses b = new ErrorLoopStatePasses(); + int x = 100; + while (x < 10) { + b.close(); + x = 0; + } + b.reopen(); // Expect: State Refinement Error + } + + // in the first iteration y == 0; x == 7 from the previous check must not hide the error in the lambda + static void lambdaInFirstIteration(int n) { + ErrorLoopStatePasses t = new ErrorLoopStatePasses(); + int x = 0; + while (n > 0) { + t.toggle(); + final int y = x; + Runnable r = () -> { + @Refinement("_ == 7") + int z = y; // Expect: Refinement Error + }; + x = 7; + n--; + } + } +} diff --git a/liquidjava-verifier/src/main/java/liquidjava/processor/context/Context.java b/liquidjava-verifier/src/main/java/liquidjava/processor/context/Context.java index 11fc653c..a5d1da5f 100644 --- a/liquidjava-verifier/src/main/java/liquidjava/processor/context/Context.java +++ b/liquidjava-verifier/src/main/java/liquidjava/processor/context/Context.java @@ -2,12 +2,14 @@ import java.util.*; import liquidjava.rj_language.Predicate; +import liquidjava.utils.Utils; import spoon.reflect.declaration.CtElement; import spoon.reflect.reference.CtTypeReference; public class Context { private Stack> ctxVars; private List ctxFunctions; + private Map> functionsBySimpleName; private List ctxInstanceVars; private final List ctxGlobalVars; @@ -24,6 +26,7 @@ private Context() { ctxVars = new Stack<>(); ctxVars.add(new ArrayList<>()); ctxFunctions = new ArrayList<>(); + functionsBySimpleName = new HashMap<>(); ctxInstanceVars = new ArrayList<>(); ctxGlobalVars = new ArrayList<>(); @@ -129,6 +132,7 @@ public void restoreInstanceVariables() { public void reinitializeAllContext() { reinitializeContext(); ctxFunctions = new ArrayList<>(); + functionsBySimpleName = new HashMap<>(); aliases = new ArrayList<>(); ghosts = new ArrayList<>(); classStates = new HashMap<>(); @@ -381,8 +385,15 @@ public void variablesCombineFromIf(Predicate cond) { // ---------------------- Functions ---------------------- public void addFunctionToContext(RefinedFunction f) { - if (!ctxFunctions.contains(f)) + if (!ctxFunctions.contains(f)) { ctxFunctions.add(f); + functionsBySimpleName.computeIfAbsent(Utils.getSimpleName(f.getName()), n -> new ArrayList<>()).add(f); + } + } + + /** The functions with this simple name, whether registered under it or, if specified externally, qualified */ + public List getFunctionsWithSimpleName(String simpleName) { + return functionsBySimpleName.getOrDefault(simpleName, List.of()); } public RefinedFunction getFunction(String name, String target, int size) { diff --git a/liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/LoopTypestates.java b/liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/LoopTypestates.java index 6b885fcc..f14a5f7e 100644 --- a/liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/LoopTypestates.java +++ b/liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/LoopTypestates.java @@ -78,7 +78,10 @@ void startIteration() { reachable = true; } - /** The loop may exit here, if this point is reachable (the condition of a do-while is not, after a return) */ + /** + * The loop may exit here, through its condition, if this point is reachable (the condition of a do-while is not + * when every path through the body returns) + */ void recordExit() throws LJError { if (reachable) addCurrentStates(exit); @@ -93,8 +96,8 @@ void recordContinue() throws LJError { } /** - * Where the body ends, a continue joins the end of the body: from here, each object is in a state it may be in at - * either + * Marks the end of the body, where the paths through its continues join the path through its last statement: from + * here on, each object is in a state it may be in at the end of the body or at any of the continues * * @param completes * whether the end of the body can be reached without a continue @@ -128,9 +131,18 @@ boolean reachedFixpoint() { return !grown; } - /** After the loop, each tracked object is in a state it may be in where the loop exits */ + /** + * After the loop, each tracked object is in a state it may be in where the loop exits. Java rejects code after a + * loop that never exits, so no exit state means the states were not followed: the object is havocked instead, so + * that this can never make the code after the loop pass + */ void finishLoop() { - exit.forEach(this::setStates); + exit.forEach((name, states) -> { + if (states.isEmpty()) + checker.forgetChanges(name, new Predicate(), loop); + else + setStates(name, states); + }); } private Map> emptyStates() { diff --git a/liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/RefinementTypeChecker.java b/liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/RefinementTypeChecker.java index 32434b0d..61b54bea 100644 --- a/liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/RefinementTypeChecker.java +++ b/liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/RefinementTypeChecker.java @@ -637,12 +637,15 @@ private boolean isUninformativeCondition(Predicate conditionRefinement, CtExpres * must be discarded at the join. * *

+ * A statement that a labelled {@code break} leaves completes normally, since execution goes on after it. + * + *

* Not currently handled (treated conservatively as completing normally): {@code switch} where every case exits, - * labeled {@code break}/{@code continue} targets, {@code try}/{@code catch}/{@code finally} flow, and infinite - * loops such as {@code while (true)}. Extending this list only tightens precision. + * {@code try}/{@code catch}/{@code finally} flow, and infinite loops such as {@code while (true)}. Extending this + * list only tightens precision. */ boolean canCompleteNormally(CtStatement statement) { - if (statement == null) + if (statement == null || isLeftByLabelledBreak(statement)) return true; if (statement instanceof CtReturn || statement instanceof CtThrow || statement instanceof CtBreak || statement instanceof CtContinue) @@ -661,6 +664,11 @@ boolean canCompleteNormally(CtStatement statement) { return true; } + private static boolean isLeftByLabelledBreak(CtStatement statement) { + return statement.getLabel() != null && statement.getElements(new TypeFilter<>(CtBreak.class)).stream() + .anyMatch(jump -> jump.getTargetLabel() != null && jump.getLabelledStatement() == statement); + } + @Override public void visitCtTry(CtTry tryBlock) { tryChecker.visitTry(tryBlock); @@ -739,9 +747,10 @@ public void visitCtContinue(CtContinue continueStatement) { */ private void visitLoop(CtLoop loop, Consumer iteration) { List pathVariables = vcChecker.getPathVariables(); - // a field may also change in a method the loop calls, out of sight here, so fields are only havocked - Set locals = changedIn(loop).stream().filter(name -> !isField(name)) - .collect(Collectors.toCollection(LinkedHashSet::new)); + // a field may also change in a method the loop calls, out of sight here, so fields are only havocked; and + // typestates are only followed through jumps whose states are recorded, else they are havocked too + Set locals = followsJumps(loop) ? changedIn(loop).stream().filter(name -> !isField(name)) + .collect(Collectors.toCollection(LinkedHashSet::new)) : Set.of(); LoopTypestates states = new LoopTypestates(this, loop, locals); havocChangedIn(loop, states.tracked()); loops.push(states); @@ -756,24 +765,35 @@ private void visitLoop(CtLoop loop, Consumer iteration) { } /** - * Checks iterations of a loop from the typestates at its head until they stop changing. Only the last iteration - * checked keeps its diagnostics: an earlier one starts from fewer states, so an error it throws, which stops the - * check, is also an error from the final states. + * Checks iterations of a loop from the typestates at its head until they stop changing. Every iteration starts from + * the same facts: those before it, with what the loop changes havocked, and only the head typestates differ, since + * what an iteration adds to the context is dropped after it (its variables and instances are scoped to it, and its + * path conditions are restored). So an earlier iteration starts from fewer states than the last one, and an error + * it throws, which stops the check, is also an error from the final states. Only the last iteration keeps the + * errors recorded without stopping it (e.g. in a lambda). */ private void checkUntilFixpoint(LoopTypestates states, Consumer iteration) { List pathVariables = vcChecker.getPathVariables(); while (true) { Set errors = new LinkedHashSet<>(diagnostics.getErrors()); - states.startIteration(); - iteration.accept(states); + context.enterContext(); + try { + states.startIteration(); + iteration.accept(states); + } finally { + context.exitContext(); + vcChecker.replacePathVariables(pathVariables); + } if (states.reachedFixpoint()) return; diagnostics.getErrors().retainAll(errors); - vcChecker.replacePathVariables(pathVariables); } } - /** The loop exits where its condition is false: never if it has none, or if it is {@code true} */ + /** + * Records the states where the loop exits through its condition, which are those where the condition is false: none + * if there is no condition or it is {@code true} + */ private void recordExit(LoopTypestates states, CtExpression condition) { if (condition == null) return; @@ -796,14 +816,43 @@ private void scanBody(CtLoop loop, LoopTypestates states) { states.endBody(canCompleteNormally(body)); } - /** The loop being checked that {@code jump} leaves, if any (an unlabeled break in a switch leaves the switch) */ + /** The loop being checked that {@code jump} leaves, if any */ private Optional loopLeftBy(CtLabelledFlowBreak jump) { - CtElement target = jump.getTargetLabel() != null ? jump.getLabelledStatement() - : jump.getParent(e -> e instanceof CtLoop || jump instanceof CtBreak - && (e instanceof CtSwitch || e instanceof CtSwitchExpression)); + CtElement target = jumpTarget(jump); return loops.stream().filter(states -> states.loop() == target).findFirst(); } + /** The statement a break or continue leaves: its label's, else the innermost loop, or switch for a break */ + private static CtElement jumpTarget(CtLabelledFlowBreak jump) { + if (jump.getTargetLabel() != null) + return jump.getLabelledStatement(); + return jump.getParent(e -> e instanceof CtLoop || (jump instanceof CtBreak && isSwitch(e))); + } + + private static boolean isSwitch(CtElement element) { + return element instanceof CtSwitch || element instanceof CtSwitchExpression; + } + + /** + * Whether the states at every jump in the loop are recorded where it goes: each jump goes to a loop or leaves a + * switch (not a labelled block, which joins no states), and runs no finally block or resource closing on its way, + * which could change states after they are recorded + */ + private static boolean followsJumps(CtLoop loop) { + return loop.getElements(new TypeFilter<>(CtLabelledFlowBreak.class)).stream().allMatch(jump -> { + CtElement target = jumpTarget(jump); + return (target instanceof CtLoop || isSwitch(target)) && !leavesTryWithCleanup(jump, target); + }); + } + + private static boolean leavesTryWithCleanup(CtLabelledFlowBreak jump, CtElement target) { + for (CtTry left = jump.getParent(CtTry.class); left != null + && left.hasParent(target); left = left.getParent(CtTry.class)) + if (left.getFinalizer() != null || left instanceof CtTryWithResource) + return true; + return false; + } + /** Havocs what the loop may change, except the {@code tracked} typestates */ private void havocChangedIn(CtLoop loop, Set tracked) { for (String name : changedIn(loop)) @@ -869,8 +918,8 @@ private static boolean isField(String name) { private boolean mayChangeState(CtInvocation invocation) { String name = invocation.getExecutable().getSimpleName(); int arity = invocation.getArguments().size(); - return context.getCtxFunctions().stream().anyMatch(f -> Utils.getSimpleName(f.getName()).equals(name) - && f.getArguments().size() == arity && f.getAllStates().stream().anyMatch(ObjectState::hasTo)); + return context.getFunctionsWithSimpleName(name).stream().anyMatch( + f -> f.getArguments().size() == arity && f.getAllStates().stream().anyMatch(ObjectState::hasTo)); } /** From 014928537c2f95d5cdd1b3df023f07bef644212a Mon Sep 17 00:00:00 2001 From: Catarina Gamboa Date: Wed, 28 Oct 2026 13:49:42 +0000 Subject: [PATCH 5/9] Recompute the metadata of a loop's elements in each check Checking an element puts metadata on it (its refinement, target, receiver), and the receiver of `new T().m()` is reused when present. Unlike the context, metadata is not scoped, so a later check of a loop body reused a receiver that an earlier check had created in a lambda and dropped since, and reported `Not Found Error: Variable '#fresh_40'` instead of checking the call. Remove that metadata from the loop's elements before each check, so each computes it afresh as the first one does. The parts checked once before the loop, and the declarations of local classes, keep theirs. Also: the readable loop in leavesTryWithCleanup. Co-Authored-By: Claude Opus 5.5 --- .../testSuite/CorrectLoopFreshReceivers.java | 32 ++++++++++++ .../testSuite/ErrorLoopFreshReceivers.java | 31 ++++++++++++ .../RefinementTypeChecker.java | 50 ++++++++++++++++--- 3 files changed, 105 insertions(+), 8 deletions(-) create mode 100644 liquidjava-example/src/main/java/testSuite/CorrectLoopFreshReceivers.java create mode 100644 liquidjava-example/src/main/java/testSuite/ErrorLoopFreshReceivers.java diff --git a/liquidjava-example/src/main/java/testSuite/CorrectLoopFreshReceivers.java b/liquidjava-example/src/main/java/testSuite/CorrectLoopFreshReceivers.java new file mode 100644 index 00000000..e1f1b9c6 --- /dev/null +++ b/liquidjava-example/src/main/java/testSuite/CorrectLoopFreshReceivers.java @@ -0,0 +1,32 @@ +package testSuite; + +import liquidjava.specification.StateRefinement; +import liquidjava.specification.StateSet; + +// A loop body checked more than once creates fresh receivers in each check, not reusing one of an earlier check +@StateSet({"open", "marked", "closed"}) +public class CorrectLoopFreshReceivers { + @StateRefinement(to = "open(this)") + CorrectLoopFreshReceivers() {} + + @StateRefinement(from = "open(this)", to = "marked(this)") + @StateRefinement(from = "marked(this)") + void mark() {} + + @StateRefinement(from = "marked(this)", to = "open(this)") + void reset() {} + + @StateRefinement(from = "!closed(this)", to = "closed(this)") + void close() {} + + static void freshReceivers(int n) { + CorrectLoopFreshReceivers b = new CorrectLoopFreshReceivers(); + while (n > 0) { + b.mark(); // the body is checked from open, then from open or marked + new CorrectLoopFreshReceivers().close(); + new CorrectLoopFreshReceivers().mark(); + Runnable r = () -> new CorrectLoopFreshReceivers().close(); + n--; + } + } +} diff --git a/liquidjava-example/src/main/java/testSuite/ErrorLoopFreshReceivers.java b/liquidjava-example/src/main/java/testSuite/ErrorLoopFreshReceivers.java new file mode 100644 index 00000000..baa585ff --- /dev/null +++ b/liquidjava-example/src/main/java/testSuite/ErrorLoopFreshReceivers.java @@ -0,0 +1,31 @@ +package testSuite; + +import liquidjava.specification.StateRefinement; +import liquidjava.specification.StateSet; + +// A loop body checked more than once creates fresh receivers in each check, not reusing one of an earlier check +@StateSet({"open", "marked", "closed"}) +public class ErrorLoopFreshReceivers { + @StateRefinement(to = "open(this)") + ErrorLoopFreshReceivers() {} + + @StateRefinement(from = "open(this)", to = "marked(this)") + @StateRefinement(from = "marked(this)") + void mark() {} + + @StateRefinement(from = "marked(this)", to = "open(this)") + void reset() {} + + @StateRefinement(from = "!closed(this)", to = "closed(this)") + void close() {} + + // a fresh object is open, and reset needs it marked + static void freshReceiverInLambda(int n) { + ErrorLoopFreshReceivers b = new ErrorLoopFreshReceivers(); + while (n > 0) { + b.mark(); // the body is checked from open, then from open or marked + Runnable r = () -> new ErrorLoopFreshReceivers().reset(); // Expect: State Refinement Error + n--; + } + } +} diff --git a/liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/RefinementTypeChecker.java b/liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/RefinementTypeChecker.java index 61b54bea..76a071d7 100644 --- a/liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/RefinementTypeChecker.java +++ b/liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/RefinementTypeChecker.java @@ -89,6 +89,9 @@ public class RefinementTypeChecker extends TypeChecker { TryChecker tryChecker; Diagnostics diagnostics = Diagnostics.getInstance(); ContextHistory contextHistory = ContextHistory.getInstance(); + // the metadata that checking an element puts on it + private static final List CHECK_METADATA = List.of(Keys.REFINEMENT, Keys.TARGET, Keys.RECEIVER, + Keys.RETURN_VAR_NAME, Keys.STATE_CHANGE); // the loops being checked, innermost first private final Deque loops = new ArrayDeque<>(); @@ -766,16 +769,22 @@ private void visitLoop(CtLoop loop, Consumer iteration) { /** * Checks iterations of a loop from the typestates at its head until they stop changing. Every iteration starts from - * the same facts: those before it, with what the loop changes havocked, and only the head typestates differ, since - * what an iteration adds to the context is dropped after it (its variables and instances are scoped to it, and its - * path conditions are restored). So an earlier iteration starts from fewer states than the last one, and an error - * it throws, which stops the check, is also an error from the final states. Only the last iteration keeps the - * errors recorded without stopping it (e.g. in a lambda). + * the same facts: those before the loop, with what it changes havocked, and only the head typestates differ. What + * an iteration adds is dropped after it: the variables it declares and the instances it gives to variables are + * scoped to it, its path conditions are restored, and the metadata it puts on the loop's elements is removed before + * the next one. The instances it created stay in the context's list of instances, but no variable or path condition + * refers to them any more, so no later check includes their refinements. + * + *

+ * So an earlier iteration starts from fewer states than the last one, and an error it throws, which stops the + * check, is also an error from the final states. Only the last iteration keeps the errors recorded without stopping + * it (e.g. in a lambda). */ private void checkUntilFixpoint(LoopTypestates states, Consumer iteration) { List pathVariables = vcChecker.getPathVariables(); while (true) { Set errors = new LinkedHashSet<>(diagnostics.getErrors()); + removeCheckMetadata(states.loop()); context.enterContext(); try { states.startIteration(); @@ -790,6 +799,29 @@ private void checkUntilFixpoint(LoopTypestates states, Consumer } } + /** + * Removes the metadata that checking the elements of a loop puts on them, which each iteration must compute afresh, + * as the first one does: unlike the context, it is not scoped, so it could refer to what an earlier iteration + * created and dropped (e.g. the receiver of a call in a lambda). The parts checked once before the loop (the + * initialization of a for, the iterable of a for-each) and the declarations in local classes and their parameters, + * which carry their contracts, keep theirs. + */ + private static void removeCheckMetadata(CtLoop loop) { + List checkedBefore = new ArrayList<>(); + if (loop instanceof CtFor forLoop) + checkedBefore.addAll(forLoop.getForInit()); + if (loop instanceof CtForEach forEach) + checkedBefore.add(forEach.getExpression()); + for (CtElement element : loop.getElements((CtElement e) -> true)) { + if (element instanceof CtTypeMember + || (element instanceof CtParameter && element.getParent() instanceof CtTypeMember) + || checkedBefore.stream().anyMatch(before -> element == before || element.hasParent(before))) + continue; + for (String key : CHECK_METADATA) + element.putMetadata(key, null); + } + } + /** * Records the states where the loop exits through its condition, which are those where the condition is false: none * if there is no condition or it is {@code true} @@ -846,10 +878,12 @@ private static boolean followsJumps(CtLoop loop) { } private static boolean leavesTryWithCleanup(CtLabelledFlowBreak jump, CtElement target) { - for (CtTry left = jump.getParent(CtTry.class); left != null - && left.hasParent(target); left = left.getParent(CtTry.class)) - if (left.getFinalizer() != null || left instanceof CtTryWithResource) + CtTry enclosing = jump.getParent(CtTry.class); + while (enclosing != null && enclosing.hasParent(target)) { + if (enclosing.getFinalizer() != null || enclosing instanceof CtTryWithResource) return true; + enclosing = enclosing.getParent(CtTry.class); + } return false; } From de8e96cfbe4c02267ccf578d7c9e60a965489af8 Mon Sep 17 00:00:00 2001 From: Catarina Gamboa Date: Wed, 28 Oct 2026 13:49:42 +0000 Subject: [PATCH 6/9] Test the labelled-block if-join, and pin the loop jump fallback A block left by a labelled break completes normally (since f9941cec), which fixes a join after an if that also passed on main: `if (c) { done: { b.close(); break done; } } b.read();`. The tests of loops with a break to a labelled block or through a finally pass through the havoc fallback, not the fixpoint: say so. Also: an unmodifiable list from the simple-name lookup, and the reason for the empty-exit guard, which does not rely on Java rejecting code after a loop that never exits. Co-Authored-By: Claude Opus 5.5 --- .../testSuite/ErrorLabelledBlockInIf.java | 28 +++++++++++++++++++ .../java/testSuite/ErrorLoopStateJumps.java | 9 +++--- .../liquidjava/processor/context/Context.java | 2 +- .../refinement_checker/LoopTypestates.java | 6 ++-- 4 files changed, 37 insertions(+), 8 deletions(-) create mode 100644 liquidjava-example/src/main/java/testSuite/ErrorLabelledBlockInIf.java diff --git a/liquidjava-example/src/main/java/testSuite/ErrorLabelledBlockInIf.java b/liquidjava-example/src/main/java/testSuite/ErrorLabelledBlockInIf.java new file mode 100644 index 00000000..0eca519d --- /dev/null +++ b/liquidjava-example/src/main/java/testSuite/ErrorLabelledBlockInIf.java @@ -0,0 +1,28 @@ +package testSuite; + +import liquidjava.specification.StateRefinement; +import liquidjava.specification.StateSet; + +// A block left by a labelled break completes normally: the state it leaves reaches the code after the if +@StateSet({"open", "closed"}) +public class ErrorLabelledBlockInIf { + @StateRefinement(to = "open(this)") + ErrorLabelledBlockInIf() {} + + @StateRefinement(from = "open(this)", to = "closed(this)") + void close() {} + + @StateRefinement(from = "open(this)") + void read() {} + + static void closedInLabelledBlock(boolean c) { + ErrorLabelledBlockInIf b = new ErrorLabelledBlockInIf(); + if (c) { + done: { + b.close(); + break done; + } + } + b.read(); // Expect: State Refinement Error + } +} diff --git a/liquidjava-example/src/main/java/testSuite/ErrorLoopStateJumps.java b/liquidjava-example/src/main/java/testSuite/ErrorLoopStateJumps.java index 9743901f..dd82fb1f 100644 --- a/liquidjava-example/src/main/java/testSuite/ErrorLoopStateJumps.java +++ b/liquidjava-example/src/main/java/testSuite/ErrorLoopStateJumps.java @@ -3,7 +3,8 @@ import liquidjava.specification.StateRefinement; import liquidjava.specification.StateSet; -// Typestates through the jumps in a loop body +// Loops with jumps whose states are not followed (a break to a labelled block, or through a finally) havoc the +// typestates of the objects they change, as before the fixpoint: these tests pin that fallback @StateSet({"open", "marked", "closed"}) public class ErrorLoopStateJumps { @StateRefinement(to = "open(this)") @@ -22,7 +23,7 @@ void close() {} @StateRefinement(from = "open(this)") void needOpen() {} - // a break out of a labelled block at the end of the body still goes on to the next iteration + // break done: the state of b is unknown in the body (the fixpoint would find it closed in the second iteration) static void labelledBlockEndsBody(int n) { ErrorLoopStateJumps b = new ErrorLoopStateJumps(); while (n > 0) { @@ -45,7 +46,7 @@ static void labelledBlockEndsDoWhileBody(int n) { } while (n > 0); } - // the break leaves the loop and the enclosing labelled block with b marked + // break out: the state of b is unknown in the body (the fixpoint would miss the marked state at the break) static void breakOutOfEnclosingBlock(int n) { ErrorLoopStateJumps b = new ErrorLoopStateJumps(); out: { @@ -60,7 +61,7 @@ static void breakOutOfEnclosingBlock(int n) { b.needOpen(); } - // the finally closes b after the break, so b is closed after the loop + // a break through a finally: the state of b is unknown in the body (the finally closes b after the break) static void breakThroughFinally() { ErrorLoopStateJumps b = new ErrorLoopStateJumps(); while (true) { diff --git a/liquidjava-verifier/src/main/java/liquidjava/processor/context/Context.java b/liquidjava-verifier/src/main/java/liquidjava/processor/context/Context.java index a5d1da5f..77d5c390 100644 --- a/liquidjava-verifier/src/main/java/liquidjava/processor/context/Context.java +++ b/liquidjava-verifier/src/main/java/liquidjava/processor/context/Context.java @@ -393,7 +393,7 @@ public void addFunctionToContext(RefinedFunction f) { /** The functions with this simple name, whether registered under it or, if specified externally, qualified */ public List getFunctionsWithSimpleName(String simpleName) { - return functionsBySimpleName.getOrDefault(simpleName, List.of()); + return Collections.unmodifiableList(functionsBySimpleName.getOrDefault(simpleName, List.of())); } public RefinedFunction getFunction(String name, String target, int size) { diff --git a/liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/LoopTypestates.java b/liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/LoopTypestates.java index f14a5f7e..cdd06f1a 100644 --- a/liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/LoopTypestates.java +++ b/liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/LoopTypestates.java @@ -132,9 +132,9 @@ boolean reachedFixpoint() { } /** - * After the loop, each tracked object is in a state it may be in where the loop exits. Java rejects code after a - * loop that never exits, so no exit state means the states were not followed: the object is havocked instead, so - * that this can never make the code after the loop pass + * After the loop, each tracked object is in a state it may be in where the loop exits. With no exit state (the + * solver proves the loop never exits, or its states were not followed), the object is havocked instead: an object + * in no state would make every check after the loop pass, which must not depend on that proof */ void finishLoop() { exit.forEach((name, states) -> { From 606839dd6d39e1b320272edf534cbfa6b6905f55 Mon Sep 17 00:00:00 2001 From: Catarina Gamboa Date: Wed, 28 Oct 2026 17:54:23 +0000 Subject: [PATCH 7/9] Track the state of an object in none of the states of a set in loops An object after @StateRefinement(to = "!open(this) && !closed(this)") is in no named state, so the loop head had no state for it and the body was checked from false. Each state set now has a none alternative in the loop fixpoint. Co-Authored-By: Claude Opus 5.5 --- .../java/testSuite/CorrectLoopStateNone.java | 31 +++++++++++++++ .../java/testSuite/ErrorLoopStateNone.java | 35 +++++++++++++++++ .../refinement_checker/LoopTypestates.java | 2 +- .../state_machine/StateMachineBuilder.java | 39 ++++++++++++++++--- 4 files changed, 100 insertions(+), 7 deletions(-) create mode 100644 liquidjava-example/src/main/java/testSuite/CorrectLoopStateNone.java create mode 100644 liquidjava-example/src/main/java/testSuite/ErrorLoopStateNone.java diff --git a/liquidjava-example/src/main/java/testSuite/CorrectLoopStateNone.java b/liquidjava-example/src/main/java/testSuite/CorrectLoopStateNone.java new file mode 100644 index 00000000..8f8698b4 --- /dev/null +++ b/liquidjava-example/src/main/java/testSuite/CorrectLoopStateNone.java @@ -0,0 +1,31 @@ +package testSuite; + +import liquidjava.specification.StateRefinement; +import liquidjava.specification.StateSet; + +// An object may be in none of the states of a set, before the loop or after a call in its body +@StateSet({"open", "closed"}) +public class CorrectLoopStateNone { + @StateRefinement(to = "!open(this) && !closed(this)") + CorrectLoopStateNone() {} + + @StateRefinement(from = "!open(this) && !closed(this)", to = "open(this)") + void open() {} + + @StateRefinement(from = "open(this)", to = "!open(this) && !closed(this)") + void read() {} + + @StateRefinement(from = "!closed(this)", to = "closed(this)") + void close() {} + + // every iteration starts and ends in no state + static void openAndRead(int n) { + CorrectLoopStateNone value = new CorrectLoopStateNone(); + for (int i = 0; i < n; i++) { + value.open(); + value.read(); + } + value.open(); + value.close(); + } +} diff --git a/liquidjava-example/src/main/java/testSuite/ErrorLoopStateNone.java b/liquidjava-example/src/main/java/testSuite/ErrorLoopStateNone.java new file mode 100644 index 00000000..dc699592 --- /dev/null +++ b/liquidjava-example/src/main/java/testSuite/ErrorLoopStateNone.java @@ -0,0 +1,35 @@ +package testSuite; + +import liquidjava.specification.StateRefinement; +import liquidjava.specification.StateSet; + +// An object may be in none of the states of a set, before the loop or after a call in its body +@StateSet({"open", "closed"}) +public class ErrorLoopStateNone { + @StateRefinement(to = "!open(this) && !closed(this)") + ErrorLoopStateNone() {} + + @StateRefinement(from = "!open(this) && !closed(this)", to = "open(this)") + void open() {} + + @StateRefinement(from = "open(this)", to = "!open(this) && !closed(this)") + void read() {} + + // value is in no state before the loop, as after the constructor + static void noneBeforeLoop(int count) { + ErrorLoopStateNone value = new ErrorLoopStateNone(); + while (count > 0) { + value.read(); // Expect: State Refinement Error + count--; + } + } + + // read leaves value in no state, so the second iteration cannot read + static void noneInSecondIteration(int n) { + ErrorLoopStateNone value = new ErrorLoopStateNone(); + value.open(); + for (int i = 0; i < n; i++) { + value.read(); // Expect: State Refinement Error + } + } +} diff --git a/liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/LoopTypestates.java b/liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/LoopTypestates.java index cdd06f1a..d9aae5a5 100644 --- a/liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/LoopTypestates.java +++ b/liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/LoopTypestates.java @@ -51,7 +51,7 @@ class LoopTypestates { if (!(checker.getContext().getVariableByName(name)instanceof Variable variable) || variable.getType() == null) continue; - List states = StateMachineBuilder.statesOf(checker.getContext(), + List states = StateMachineBuilder.statesOrNoneOf(checker.getContext(), variable.getType().getQualifiedName()); if (states.isEmpty()) continue; diff --git a/liquidjava-verifier/src/main/java/liquidjava/processor/state_machine/StateMachineBuilder.java b/liquidjava-verifier/src/main/java/liquidjava/processor/state_machine/StateMachineBuilder.java index 173a05ae..4787728c 100644 --- a/liquidjava-verifier/src/main/java/liquidjava/processor/state_machine/StateMachineBuilder.java +++ b/liquidjava-verifier/src/main/java/liquidjava/processor/state_machine/StateMachineBuilder.java @@ -82,6 +82,18 @@ public static Optional build(TypeChecker tc, StateSolver solver, S /** Every combination of one state from each state set of the class */ public static List statesOf(Context context, String className) { + return statesOf(context, className, false); + } + + /** + * Every combination of one state from each state set of the class, where an object may also be in none of the + * states of a set (e.g. after {@code @StateRefinement(to = "!open(this) && !closed(this)")}), named {@code none} + */ + public static List statesOrNoneOf(Context context, String className) { + return statesOf(context, className, true); + } + + private static List statesOf(Context context, String className, boolean withNone) { List ghostStates = context.getGhostState(Utils.getSimpleName(className)); if (ghostStates == null) return List.of(); @@ -91,16 +103,31 @@ public static List statesOf(Context context, String className) { return List.of(); List combinations = List.of(new State(List.of(), new Predicate())); - for (List stateSet : stateSets.values()) - combinations = combinations.stream().flatMap(s -> stateSet.stream().map(g -> combine(s, g))).toList(); + for (List stateSet : stateSets.values()) { + List alternatives = stateSet.stream().map(StateMachineBuilder::inState).toList(); + if (withNone) + alternatives = Stream.concat(alternatives.stream(), Stream.of(inNone(stateSet))).toList(); + List inSet = alternatives; + combinations = combinations.stream().flatMap(s -> inSet.stream().map(a -> combine(s, a))).toList(); + } return combinations; } - private static State combine(State state, GhostState ghostState) { + private static State inState(GhostState ghostState) { + return new State(List.of(ghostState.getName()), + Predicate.createInvocation(ghostState.getQualifiedName(), Predicate.createVar(Keys.THIS))); + } + + private static State inNone(List stateSet) { + Predicate none = stateSet.stream().map(g -> inState(g).predicate().negate()) + .reduce(Predicate::createConjunction).orElseThrow(); + return new State(List.of("none"), none); + } + + private static State combine(State state, State inSet) { List names = new ArrayList<>(state.names()); - names.add(ghostState.getName()); - Predicate holds = Predicate.createInvocation(ghostState.getQualifiedName(), Predicate.createVar(Keys.THIS)); - return new State(names, Predicate.createConjunction(state.predicate(), holds)); + names.addAll(inSet.names()); + return new State(names, Predicate.createConjunction(state.predicate(), inSet.predicate())); } private StateMachine build(String className, CtTypeReference type) throws LJError { From cb1a49d1ff801c56925584ccf82749d56417b1f8 Mon Sep 17 00:00:00 2001 From: Catarina Gamboa Date: Thu, 29 Oct 2026 14:17:30 +0000 Subject: [PATCH 8/9] Simplify the loop typestate code - Find state-changing methods by simple name in the function list, without a second index in Context to keep in sync. - One statesOf with a withNone flag instead of three methods. - Record the next iteration's states in the fixpoint loop, not in each loop kind. - Compute each entry state once for a call from a union of entry states. - Shorter comments on the fixpoint and metadata removal. Co-Authored-By: Claude Opus 5.5 --- .../liquidjava/processor/context/Context.java | 13 +------- .../refinement_checker/LoopTypestates.java | 4 +-- .../RefinementTypeChecker.java | 32 +++++++------------ .../object_checkers/AuxStateHandler.java | 12 +++---- .../state_machine/StateMachineBuilder.java | 26 ++++++--------- 5 files changed, 30 insertions(+), 57 deletions(-) diff --git a/liquidjava-verifier/src/main/java/liquidjava/processor/context/Context.java b/liquidjava-verifier/src/main/java/liquidjava/processor/context/Context.java index 77d5c390..11fc653c 100644 --- a/liquidjava-verifier/src/main/java/liquidjava/processor/context/Context.java +++ b/liquidjava-verifier/src/main/java/liquidjava/processor/context/Context.java @@ -2,14 +2,12 @@ import java.util.*; import liquidjava.rj_language.Predicate; -import liquidjava.utils.Utils; import spoon.reflect.declaration.CtElement; import spoon.reflect.reference.CtTypeReference; public class Context { private Stack> ctxVars; private List ctxFunctions; - private Map> functionsBySimpleName; private List ctxInstanceVars; private final List ctxGlobalVars; @@ -26,7 +24,6 @@ private Context() { ctxVars = new Stack<>(); ctxVars.add(new ArrayList<>()); ctxFunctions = new ArrayList<>(); - functionsBySimpleName = new HashMap<>(); ctxInstanceVars = new ArrayList<>(); ctxGlobalVars = new ArrayList<>(); @@ -132,7 +129,6 @@ public void restoreInstanceVariables() { public void reinitializeAllContext() { reinitializeContext(); ctxFunctions = new ArrayList<>(); - functionsBySimpleName = new HashMap<>(); aliases = new ArrayList<>(); ghosts = new ArrayList<>(); classStates = new HashMap<>(); @@ -385,15 +381,8 @@ public void variablesCombineFromIf(Predicate cond) { // ---------------------- Functions ---------------------- public void addFunctionToContext(RefinedFunction f) { - if (!ctxFunctions.contains(f)) { + if (!ctxFunctions.contains(f)) ctxFunctions.add(f); - functionsBySimpleName.computeIfAbsent(Utils.getSimpleName(f.getName()), n -> new ArrayList<>()).add(f); - } - } - - /** The functions with this simple name, whether registered under it or, if specified externally, qualified */ - public List getFunctionsWithSimpleName(String simpleName) { - return Collections.unmodifiableList(functionsBySimpleName.getOrDefault(simpleName, List.of())); } public RefinedFunction getFunction(String name, String target, int size) { diff --git a/liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/LoopTypestates.java b/liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/LoopTypestates.java index d9aae5a5..96d20235 100644 --- a/liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/LoopTypestates.java +++ b/liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/LoopTypestates.java @@ -51,8 +51,8 @@ class LoopTypestates { if (!(checker.getContext().getVariableByName(name)instanceof Variable variable) || variable.getType() == null) continue; - List states = StateMachineBuilder.statesOrNoneOf(checker.getContext(), - variable.getType().getQualifiedName()); + List states = StateMachineBuilder.statesOf(checker.getContext(), + variable.getType().getQualifiedName(), true); if (states.isEmpty()) continue; classStates.put(name, states); diff --git a/liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/RefinementTypeChecker.java b/liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/RefinementTypeChecker.java index 76a071d7..8d2388e1 100644 --- a/liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/RefinementTypeChecker.java +++ b/liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/RefinementTypeChecker.java @@ -689,7 +689,6 @@ public void visitCtWhile(CtWhile whileLoop) { recordExit(states, whileLoop.getLoopingExpression()); assumeLoopCondition(whileLoop.getLoopingExpression()); scanBody(whileLoop, states); - states.recordNextIteration(); }); } @@ -703,7 +702,6 @@ public void visitCtFor(CtFor forLoop) { scanBody(forLoop, states); // the update runs after the body, so the body sees the values the condition was checked on scan(forLoop.getForUpdate()); - states.recordNextIteration(); }); } @@ -714,7 +712,6 @@ public void visitCtDo(CtDo doLoop) { scanBody(doLoop, states); scan(doLoop.getLoopingExpression()); recordExit(states, doLoop.getLoopingExpression()); - states.recordNextIteration(); }); } @@ -726,7 +723,6 @@ public void visitCtForEach(CtForEach forEach) { states.recordExit(); scan(forEach.getVariable()); scanBody(forEach, states); - states.recordNextIteration(); }); } @@ -768,17 +764,13 @@ private void visitLoop(CtLoop loop, Consumer iteration) { } /** - * Checks iterations of a loop from the typestates at its head until they stop changing. Every iteration starts from - * the same facts: those before the loop, with what it changes havocked, and only the head typestates differ. What - * an iteration adds is dropped after it: the variables it declares and the instances it gives to variables are - * scoped to it, its path conditions are restored, and the metadata it puts on the loop's elements is removed before - * the next one. The instances it created stay in the context's list of instances, but no variable or path condition - * refers to them any more, so no later check includes their refinements. + * Checks iterations of a loop from the typestates at its head until they stop changing. Every check starts from the + * facts before the loop, with what it changes havocked; only the head typestates differ. What a check adds + * (variables, instances, path conditions, metadata) is dropped before the next one. * *

- * So an earlier iteration starts from fewer states than the last one, and an error it throws, which stops the - * check, is also an error from the final states. Only the last iteration keeps the errors recorded without stopping - * it (e.g. in a lambda). + * An earlier check starts from fewer states than the last one, so an error that stops it is also an error of the + * last one. Only the last check keeps the errors recorded without stopping it (e.g. in a lambda). */ private void checkUntilFixpoint(LoopTypestates states, Consumer iteration) { List pathVariables = vcChecker.getPathVariables(); @@ -789,6 +781,7 @@ private void checkUntilFixpoint(LoopTypestates states, Consumer try { states.startIteration(); iteration.accept(states); + states.recordNextIteration(); } finally { context.exitContext(); vcChecker.replacePathVariables(pathVariables); @@ -800,11 +793,10 @@ private void checkUntilFixpoint(LoopTypestates states, Consumer } /** - * Removes the metadata that checking the elements of a loop puts on them, which each iteration must compute afresh, - * as the first one does: unlike the context, it is not scoped, so it could refer to what an earlier iteration - * created and dropped (e.g. the receiver of a call in a lambda). The parts checked once before the loop (the - * initialization of a for, the iterable of a for-each) and the declarations in local classes and their parameters, - * which carry their contracts, keep theirs. + * Removes the metadata that checking a loop puts on its elements: unlike the context it is not scoped, so it could + * refer to what an earlier check dropped (e.g. the receiver of a call in a lambda). The parts checked once before + * the loop (a for's initialization, a for-each's iterable) and local class members, which carry their contracts, + * keep theirs. */ private static void removeCheckMetadata(CtLoop loop) { List checkedBefore = new ArrayList<>(); @@ -952,8 +944,8 @@ private static boolean isField(String name) { private boolean mayChangeState(CtInvocation invocation) { String name = invocation.getExecutable().getSimpleName(); int arity = invocation.getArguments().size(); - return context.getFunctionsWithSimpleName(name).stream().anyMatch( - f -> f.getArguments().size() == arity && f.getAllStates().stream().anyMatch(ObjectState::hasTo)); + return context.getCtxFunctions().stream().anyMatch(f -> Utils.getSimpleName(f.getName()).equals(name) + && f.getArguments().size() == arity && f.getAllStates().stream().anyMatch(ObjectState::hasTo)); } /** diff --git a/liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/object_checkers/AuxStateHandler.java b/liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/object_checkers/AuxStateHandler.java index 32b31203..38fe52cd 100644 --- a/liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/object_checkers/AuxStateHandler.java +++ b/liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/object_checkers/AuxStateHandler.java @@ -898,11 +898,10 @@ private static boolean changeToStateOfAnyEntryState(TypeChecker tc, VariableInst return false; String instanceName = vi.getName(); Predicate previous = substituteArguments(prevState, map); - Predicate anyEntry = Predicate.createLit("false", Types.BOOLEAN); - for (ObjectState alternative : alternatives) - anyEntry = Predicate.createDisjunction(anyEntry, entryState(alternative, instanceName, map)); + List entries = alternatives.stream().map(a -> entryState(a, instanceName, map)).toList(); try { - if (!tc.checkStateSMT(previous, anyEntry, invocation.getPosition())) + if (!tc.checkStateSMT(previous, entries.stream().reduce(Predicate::createDisjunction).orElseThrow(), + invocation.getPosition())) return false; } catch (SMTUnknownError error) { error.setDeclarationPosition(alternatives.get(0).getFromPosition()); @@ -912,8 +911,9 @@ private static boolean changeToStateOfAnyEntryState(TypeChecker tc, VariableInst String newInstanceName = String.format(Formats.INSTANCE, name, tc.getContext().getCounter()); Predicate unchanged = previous.substituteVariable(instanceName, newInstanceName); Predicate after = Predicate.createLit("false", Types.BOOLEAN); - for (ObjectState alternative : alternatives) { - Predicate entry = entryState(alternative, instanceName, map); + for (int i = 0; i < alternatives.size(); i++) { + ObjectState alternative = alternatives.get(i); + Predicate entry = entries.get(i); Predicate exit = alternative.hasTo() ? transitionedState(alternative, instanceName, newInstanceName, map, invocation) : Predicate.createConjunction(entry.substituteVariable(instanceName, newInstanceName), unchanged); diff --git a/liquidjava-verifier/src/main/java/liquidjava/processor/state_machine/StateMachineBuilder.java b/liquidjava-verifier/src/main/java/liquidjava/processor/state_machine/StateMachineBuilder.java index 4787728c..617c4c4a 100644 --- a/liquidjava-verifier/src/main/java/liquidjava/processor/state_machine/StateMachineBuilder.java +++ b/liquidjava-verifier/src/main/java/liquidjava/processor/state_machine/StateMachineBuilder.java @@ -65,7 +65,7 @@ public static boolean canModel(RefinedFunction function) { */ public static Optional build(TypeChecker tc, StateSolver solver, String className, CtElement element) throws LJError { - List states = statesOf(tc.getContext(), className); + List states = statesOf(tc.getContext(), className, false); if (states.isEmpty() || states.size() > MAX_STATES) return Optional.empty(); Context context = tc.getContext(); @@ -80,20 +80,14 @@ public static Optional build(TypeChecker tc, StateSolver solver, S } } - /** Every combination of one state from each state set of the class */ - public static List statesOf(Context context, String className) { - return statesOf(context, className, false); - } - /** - * Every combination of one state from each state set of the class, where an object may also be in none of the - * states of a set (e.g. after {@code @StateRefinement(to = "!open(this) && !closed(this)")}), named {@code none} + * Every combination of one state from each state set of the class + * + * @param withNone + * whether an object may also be in none of the states of a set, named {@code none} (e.g. after + * {@code @StateRefinement(to = "!open(this) && !closed(this)")}) */ - public static List statesOrNoneOf(Context context, String className) { - return statesOf(context, className, true); - } - - private static List statesOf(Context context, String className, boolean withNone) { + public static List statesOf(Context context, String className, boolean withNone) { List ghostStates = context.getGhostState(Utils.getSimpleName(className)); if (ghostStates == null) return List.of(); @@ -104,10 +98,8 @@ private static List statesOf(Context context, String className, boolean w List combinations = List.of(new State(List.of(), new Predicate())); for (List stateSet : stateSets.values()) { - List alternatives = stateSet.stream().map(StateMachineBuilder::inState).toList(); - if (withNone) - alternatives = Stream.concat(alternatives.stream(), Stream.of(inNone(stateSet))).toList(); - List inSet = alternatives; + List inSet = Stream.concat(stateSet.stream().map(StateMachineBuilder::inState), + withNone ? Stream.of(inNone(stateSet)) : Stream.empty()).toList(); combinations = combinations.stream().flatMap(s -> inSet.stream().map(a -> combine(s, a))).toList(); } return combinations; From a06f3c40c864e8a2988a39e6f5fb2c2abc7ff406 Mon Sep 17 00:00:00 2001 From: Catarina Gamboa Date: Fri, 30 Oct 2026 14:31:23 +0000 Subject: [PATCH 9/9] Say in the StateSet Javadoc that an object may be in no state of a set Also close the {@code} block of the class example. Co-Authored-By: Claude Opus 5.5 --- .../src/main/java/liquidjava/specification/StateSet.java | 8 +++++--- 1 file changed, 5 insertions(+), 3 deletions(-) diff --git a/liquidjava-api/src/main/java/liquidjava/specification/StateSet.java b/liquidjava-api/src/main/java/liquidjava/specification/StateSet.java index 376c071b..ad074c48 100644 --- a/liquidjava-api/src/main/java/liquidjava/specification/StateSet.java +++ b/liquidjava-api/src/main/java/liquidjava/specification/StateSet.java @@ -9,9 +9,10 @@ /** * Annotation to create a set of disjoint states in which class objects can be. *

- * An object will always be in exactly one state from each state set at any given time, - * and cannot be in more than one state from the same state set (e.g., {@code open} and {@code closed} simultaneously). - * To allow an object to be in multiple states at once, they must be from different state sets. + * An object cannot be in more than one state from the same state set at a time (e.g., {@code open} and + * {@code closed} simultaneously). To allow an object to be in multiple states at once, they must be from different + * state sets. An object may also be in none of the states of a set, e.g. after + * {@code @StateRefinement(to = "!open(this) && !closed(this)")}. *

* Example: * 

@@ -21,6 +22,7 @@
  * public class File {
  *    // ...
  * }
+ * }
  *
* * @see StateRefinement