Say where the wrong state or value comes from (From note), and counterexamples for state errors #522

Activity

1. CatarinaGamboa

   added

   studyNeeded before the error-message user studyNeeded before the error-message user study

   on Nov 10, 2026
2. CatarinaGamboa commented on Nov 10, 2026

   

   CatarinaGamboa

   on Nov 10, 2026

   CollaboratorAuthor

   More actions

   Design (before coding)

   Every From line is a message note (LJDiagnostic.getMessageNotes()), so the CLI prints it under the headline and the extension can show it in the hover (vscode-liquidjava#188). When a condition below fails, no note is printed.

   I plan five small PRs, in this order. 2 and 3 are stacked on 1, which adds addMessageNote.

   1. F3, unrefined parameter (A2_04)

   Data:

   • the error's category (UNKNOWN);
   • the variables of Expected;
   • the enclosing CtExecutable of the checked element;
   • the context Variable of each name.

   Printed when the category is UNKNOWN and every variable of Expected is:

   • a parameter of the enclosing method, by name (so not an instance, which a reassignment would create);
   • with a declared refinement of true in the context.

   Text: From: timeout is a parameter of checkCimReachable(String, int) (line 94) with no refinement

   Why it is sound: the note restates a declaration. It says nothing about callers, and it adds no fact to Found.

   2. F1 and F2, the state of the receiver (A1_38, A1_01, A1_56)

   Data:

   • the receiver instance at the failing call, and its StateChange chain;
   • the sets the call's from checks. The note names only the sets where no possible state is accepted, which only selects what is shown (S1);
   • new: the call result an instance holds. It is set when a local variable is declared or assigned from a call to a specified method, and a state-preserving call copies it as it copies the StateChange. It holds the method, the call's code and position, and the return refinement instantiated at the call.

   F1, a state set by a call. Walk back from the receiver to the first change whose to names a shown set. Printed only if:

   • every instance on the way has a StateChange, so the walk crosses no join, loop havoc or unknown origin;
   • every change crossed names none of the shown sets;
   • StateSolver.implies(<the instance after that change>, <Found on those sets>) holds.

   Text: From: markState(buffered) == unmarked, last set at line 134: new BufferedInputStream(stream)

   F1 fallback. If the walk reaches an instance with no StateChange, and the receiver is a local variable whose only write is its initializer, a constructor call, then the note gives the creation fact: From: buffered is created at line 134 by new BufferedInputStream(stream), which makes it markState(buffered) == unmarked. This is the constructor's to on the shown sets. It is a fact about the constructor, and it does not claim the state is still the same.

   F2, a state from a returned value. Printed only if the receiver instance has no StateChange and holds a call result, so nothing changed it since the assignment.

   • Text: From: wParam = writer.getDefaultWriteParam(), line 130, which returns compression(wParam) == compressionNotExplicit. These are the conjuncts of the instantiated return refinement that name a shown set. Dropping conjuncts only weakens it.
   • Or …, which says nothing about redoState(undoManager), only if the return refinement names no state of those sets and mentions no variable but _. Aliases are expanded first. This rules out _ == this-style returns that carry a state.

   A1_09's receiver is a join (ITE), so it gets no From note.

   DebugLog check (A1_38). Before coding F1 I will confirm with DebugLog whether the loops at lines 136/150 give buffered a new instance. reset() has no to, and read(byte[])/markSupported() are unspecified, so the code says they should not. I will log the walk under -d.

   3. F4, value returned by a call (A2_10)

   Data: the same call result, recorded on the argument instance that createVariableRepresentingArgument creates for a call argument.

   Printed for each variable of Expected that holds a call result.

   Text: From: failures.size() (ArrayListRefinements.java:162) guarantees only failures.size() >= 0. It is instantiated, and a conjunct _ == g(…) is dropped when the ghost term g(…) appears nowhere else in the refinement.

   Why "only" is sound: ∃g. (_ == g ∧ Q()) ≡ Q() when g is not in Q. So the remaining conjuncts are exactly what the refinement says about the value. If nothing remains, the note says it guarantees nothing about the value.

   4. Counterexample for state errors

   Data: one extra StateSolver.witness(Found, ¬Expected) call when a state error is reported. This is the same VC, with the same context gathering.

   Shown: the assignments to plain variables of the shown Found, except:

   • ghost and state applications (S2);
   • generated names;
   • values that a Found fact x == c already states.

   The result is a sub-assignment of a model of Found ∧ ¬Expected.

   Expected:

   • A1_09: previousMode == BORDERLESS (newMode is dropped as known);
   • A1_38, A1_01, A1_56: none.

   5. A1_09's nested ITE folded under the shown path condition

   Data: the shown Found's top-level facts x == c, where c is an enum constant or a literal.

   Fold: substitute them into the conditions of the ITEs in the other facts, then run the existing VCFolding/VCLogicalSimplification. An arm is dropped only when its condition folds to false (or true for the else arm). The ITE semantics are kept exactly, and the substituted fact stays in Found, so the folded Found is equivalent to the shown one. If constant folding does not settle a condition, I will use no SMT check in this PR: the ITE is just kept.

   Expected A1_09 headline: found newMode == BORDERLESS && (previousMode != BORDERLESS ? display(host) == notDisplayable : display(host) == displayable) but expected display(host) == notDisplayable

   Conflicts

   • With One headline frame: found … but expected … for refinement errors #520/Drop the general UNKNOWN hint and show every from in declared-here #521 (RefinementError headline, general hint; AuxStateHandler declared-here): one call site in AuxStateHandler.changeState and the getMessageNotes override.
   • With Drop the guard hint when a call-sequence hint exists, and reword it #518/State hints: name only the state the call leads to #519 (StateHints): none expected.
3. CatarinaGamboa commented on Nov 10, 2026

   

   CatarinaGamboa

   on Nov 10, 2026

   CollaboratorAuthor

   More actions

   Status: five PRs, none merged

   Part	PR	Base	Codex
   F3, unrefined parameter (A2_04)	#526	main	3 rounds, clean
   F1/F2, where the state comes from (A1_38, A1_01, A1_56)	#528	#526	5 rounds (the limit)
   F4, value returned by a call (A2_10)	#530	#528	5 rounds (the limit)
   Counterexample for state errors (A1_09)	#527	main	2 rounds, clean
   A1_09's ITE folded under the path condition	#529	main	2 rounds, clean

   #526 → #528 → #530 are stacked. Retarget each child to main before merging its parent with --delete-branch. #527 and #529 are independent of each other and of the stack. They add a parameter next to #528's in throwStateRefinementError, so whichever merges second needs a one-line rebase.

   All five together (checked on a local merge; 737 tests pass). Each task still gives one error, on its reportedLine:

   A2_10  Refinement Error: failures.size() == size(this.failures) && failures.size() >= 0 is not a subtype of failures.size() > 0
            From: failures.size() (ArrayListRefinements.java:162) guarantees only failures.size() >= 0
   A1_38  State Refinement Error: found stream(buffered) == open && markState(buffered) == unmarked but expected markState(buffered) == marked && stream(buffered) == open
            From: markState(buffered) == unmarked, last set at line 134: new BufferedInputStream(stream)
   A1_01  State Refinement Error: found compression(wParam) == compressionNotExplicit but expected compression(wParam) == compressionExplicit || compression(wParam) == compressionTypeSet
            From: wParam = writer.getDefaultWriteParam(), line 130, which returns compression(wParam) == compressionNotExplicit
   A2_04  Refinement Error: expected timeout >= 0 but could not prove it
            From: timeout is a parameter of checkCimReachable(String, int) (line 94) with no refinement
   A1_56  State Refinement Error: expected redoState(undoManager) == redoable but could not prove it
            From: undoManager = frame.getUndoManager(), line 69, which says nothing about redoState(undoManager)
   A1_09  State Refinement Error: found newMode == BORDERLESS && (previousMode != BORDERLESS ? display(host) == notDisplayable : display(host) == displayable) but expected display(host) == notDisplayable
             --> Counterexample: previousMode == BORDERLESS
   

   practice and practice2 are unchanged. The headlines of A2_10 and the practice tasks are still main's: the "found … but expected" headline is #520's job.

   The Codex rounds mostly tightened #528. A From note is now left out whenever the receiver may change state out of the verifier's sight before the call: it is aliased, passed as an argument, captured, bound in a method reference, a field, or given an unspecified source method call. The PR comments list each case.

   Questions for the PM

   1. Bodies that break their declared state contract. A constructor annotated to = "idle(this)" that calls start(), or a from-only method that calls reset(): the verifier trusts the contract and does not check the body. Its Found, and the From note quoting the contract, are then wrong about the program. That is a verifier issue, not a message issue. Should it get its own issue?
   2. A local assigned from a call, in a refinement error. n = read(); write(n) could say From: n = read(), line 44, which guarantees only n >= -1. Origin note: say what a call's return refinement guarantees about an argument it gives #530 deliberately covers only call arguments (the F4 scope). Do you want the local form too?
   3. A fully settled branch (Fold a state error's Found under the constants its path conditions state #529). When a fold settles every branch on x, the headline would drop the fact x == c that chose it, so Fold a state error's Found under the constants its path conditions state #529 shows the unfolded Found instead. Keeping that fact visible needs ErrorMessage's fact selection (shared, touched by One headline frame: found … but expected … for refinement errors #520). A follow-up?
4. CatarinaGamboa

   closed this as completedin #526on Nov 10, 2026
5. CatarinaGamboa

   added a commit that references this issue on Nov 11, 2026

   Origin note: say where the wrong state of a receiver comes from (#528)

   ...

   This issue will close once commit 070fb75 is merged into the 'main' branch.

   070fb75