[CatarinaGamboa]

After a loop, an object whose class has an external spec keeps the state set inside the loop body, so a real bug passes (#427). The same loops over a class specified in the file have the opposite problem: their state is forgotten, so valid calls inside the loop are refused.

Problem

// @ExternalRefinementsFor("java.io.BufferedReader"), states open / marked / closed
BufferedReader br = new BufferedReader(in);
while (k < n) { br.mark(100); k++; }
br.reset();                 // may run with br unmarked: n == 0

for (int i = 0; i < n; i++) {
    br.readLine();          // closed from the second iteration on
    br.close();
}

Correct! Passed Verification.

The same shape is a real bug in tabu-timetabling's InputReader ("Stream not marked", fixed in 5ea97d1): the inner loop that marks may stop at once, and then reset() runs.

With a class specified in the file, a call that every iteration allows is refused:

for (int i = 0; i < n; i++) { b.read(); b.mark(); }   // read needs open or marked
// State Refinement Error: found i < n but expected open(b) || marked(b)

Cause

A loop was checked for one iteration, after havocking what it may change. An object was havocked only if the loop called a method of that name with a state change, looked up by simple name. Methods from @ExternalRefinementsFor are registered under their qualified name (java.io.BufferedReader.mark), so the lookup missed them and the state set in the body was kept, after the loop and in the next iteration. When the lookup did find them, the object's state was unknown in the whole body, hence the false error above. Fixing only the lookup would move external specs to that false error too (br.mark(100) above would be refused).

Fix

Eight commits: the first two are the change, the third is a refactoring, the next four follow review, and the last simplifies the code.

1. A state-changing call from a union of its entry states. mark() (from open to marked, or from marked) was refused on an object that is open or marked, since each entry state was checked alone. Now, when only their union is provable, the call is allowed and the object takes the state of any alternative whose entry state it may be in.
2. The typestate at the loop head as a fixpoint. For each local object the loop may change, the verifier keeps a set of states of its class: the states before the loop, plus the states at the end of each checked iteration (the end of the body and each continue), until the set stops changing. The body is then checked from those states, and after the loop the object is in a state it may be in where the loop exits (the condition is false, or a break). For while, do-while, for and for-each, with break and continue (labelled or not) to a loop or out of a switch; a loop with any other jump falls back to havoc (below).
   • Same facts in every check: every check starts from the facts before the loop, with what the loop changes havocked; only the states at the head differ. Each check runs in its own context scope (the instances it gives to variables and the variables it declares are dropped after 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, but nothing refers to them any more.
   • Termination: a class has finitely many states and the set only grows, so a loop is checked at most once per state, plus once. For nested loops, the counts multiply.
   • Errors reported once: an earlier check starts from the same facts and fewer states, so an error that stops it is also an error of the final states. Errors recorded without stopping (in a lambda) are dropped, except those from the last check.
   • Jumps: a loop with a jump whose state would not be recorded where it lands is not tracked, and its objects are havocked as on main. That covers a break to a labelled block, or one that runs a finally or closes resources on its way out.
   • If-join fix (also wrong on main): a statement that a labelled break leaves now completes normally. Before, if (c) { done: { b.close(); break done; } } b.read(); passed, because the join after the if dropped the then branch.
   • Guard: an object with no state where the loop exits (the solver proves the loop never exits, or its states were not followed) is havocked, so the code after the loop never passes because of that.
   • No state of a set: an object may be in none of the states of a set, e.g. after @StateRefinement(to = "!open(this) && !closed(this)"). Each set has a none alternative in the fixpoint, so such an object is tracked like one in a named state (before, its body was checked from false, and a wrong call in it passed).
   • Values and fields are havocked as before. The lookup now also finds externally specified methods.

Now:

br.reset()   -> State Refinement Error: found open(br) || marked(br) but expected marked(br)
br.readLine() -> State Refinement Error: found i + 1 < n && (open(br) || closed(br)) but expected open(br) || marked(br)

Tests

• classes/loop_state_external_error: the two reproducers of Soundness: after a loop, an object with an external spec keeps the state set inside the loop body #427, do-while, for-each, continue, break, nested loops, and the tabu-timetabling shape (a mark only in the inner loop).
• classes/loop_state_external_correct: mark and reset in the body, open or marked in every iteration, do-while, for-each, continue/break, nested loops, and the fix of the tabu-timetabling bug. This one also passes on main; it guards against a fix of the lookup alone, which would refuse it.
• CorrectLoopStateFixpoint (in-file class): the false error above and the same loop kinds. ErrorLoopStateFixpoint: a state reached only in the third iteration, and an error in a lambda in the loop reported once.
• ErrorLoopStatePasses: values from an earlier check must not leak into the next (a loop never entered, and a lambda error in the first iteration). CorrectLoopFreshReceivers / ErrorLoopFreshReceivers: a receiver created in an earlier check, e.g. () -> new T().close(), must not be reused (it gave a Not Found Error).
• ErrorLoopStateJumps: pins the havoc fallback for a break to a labelled block (inside the body or around the loop) and through a finally. ErrorLabelledBlockInIf: the if-join fix (main accepts this program, so the test fails there).
• CorrectStateChangeFromUnion / ErrorStateChangeFromUnion: the first commit.
• CorrectLoopStateNone / ErrorLoopStateNone: an object in no state of its set before the loop, and one that reaches it in the body (both fail without the last commit).
• ErrorLoopPostState (Soundness: after a loop, the state is taken from the loop body as if it ran at least once #338) is still reported, and CorrectLoopPostState still passes.
• mvn test: 545 tests, 0 failures (rebased on main at f7f366c).

Results

• tabu-timetabling InputReader: br is a static field there, and LiquidJava does not track the state of static fields, even without loops. So the original file still passes. With br and fr as locals and the method otherwise unchanged, the bug is reported at br.reset(), and the fixed version passes.
• 53 exercises built from real OSS bugs (74 runs, buggy and fixed), main (4a89df6) vs this branch: the same results on every run (same error titles and lines, same 20 crashes from unrelated causes). Only a Z3 counterexample value and some stack frames differ.
• Time: a loop is checked again only when the states at its head grow. The machine was shared with other jobs, so wall-clock times are noisy. CPU time for the 74 runs was 1153 s on main and 1121 s on this branch. mvn test took 202 s of CPU on main and 178 s on this branch. Both differences are within the noise.

Closes #427.

🤖 Generated with Claude Code

[CatarinaGamboa]

[Codex review — blocking] A reachable loop body can be checked under an impossible state and its invalid call is accepted.

I reproduced this on this PR head with a class that has @StateSet({"open", "closed"}), a constructor with @StateRefinement(to = "!open(this) && !closed(this)"), and read() with @StateRefinement(from = "open(this)", to = "!open(this) && !closed(this)"). A direct value.read() correctly reports a State Refinement Error. The same call inside while (count > 0) { value.read(); count--; } reports no error. The CLI output contains only the direct-call diagnostic.

StateMachineBuilder.statesOf enumerates only named states. LoopTypestates.currentStates therefore returns an empty set for this valid unnamed state. startIteration turns that into the predicate false, so the body is verified vacuously. finishLoop havocs an empty exit set, but that happens after the missed check. Please represent the unnamed/default state in the fixpoint or fall back to havoc before checking the loop when its current state set is empty, and add this case to the tests.

[CatarinaGamboa]

[Claude] Fixed in 63600f8. The loop fixpoint now gives each state set a none alternative (!open(this) && !closed(this) here), so an object in no named state is tracked instead of being checked from false. This also covers an object that reaches no state inside the body, e.g. open() before the loop and read() in it: the second iteration was missed in the same way.

Your reproducer now reports the error in the loop. ErrorLoopStateNone covers both cases, and CorrectLoopStateNone covers a loop that starts and ends in no state. Both fail without the commit (the correct one gave a false error after the loop, since its exit set was empty). mvn test: 509 tests, 0 failures.

[CatarinaGamboa]

[Codex re-review] The blocker I reported is fixed at cb1a49d1. I reran my original reproducer: the verifier now reports the invalid direct call and the invalid call inside while (count > 0). ErrorLoopStateNone also covers reaching none on a later iteration, and CorrectLoopStateNone covers a valid loop through that state. The none predicate is formed per state set, so the loop fixpoint now has an alternative for values outside the named states; the state machine used for hints still uses its prior named-state list.

I reviewed the subsequent simplification of the loop's next-iteration recording, method lookup, and state disjunction and found no new correctness issue. The full local verifier suite passes: 545 test cases, 0 failures or errors (./mvnw -q -pl liquidjava-verifier -am test). The previous blocking comment is resolved from my review.

Small documentation follow-up: StateSet's Javadoc says an object is always in exactly one named state per set, while this change explicitly supports none.