GeezerVison is showing github.com — Say where the wrong state or value comes from (From note), and counterexamples for state errors · Issue #522 · liquid-java/liquidjava
Say where the wrong state or value comes from (From note), and counterexamples for state errors #522DescriptionNo error message in the study tasks says where the wrong state or value comes from:
- A1_38: line 134,
new BufferedInputStream(stream), reported at 157;
- A1_01: line 130,
getDefaultWriteParam(), reported at 136;
- A1_56: line 69,
frame.getUndoManager();
- A2_04:
timeout is an unrefined parameter.
That cause is what the study's rubric (rule / cause / fix) and H4/H6 measure.
Proposal: a "From" note under the headline
It goes in the CLI, the hover and the panel. It is printed only when it can be shown soundly; otherwise it is left out.
-
F1, state set by a call. Walk the receiver's StateChange chain back to the first change whose to names a checked set. Print markState(buffered) == unmarked, last set at line 134: new BufferedInputStream(stream) only if all of these hold:
- the walk crosses no join or instance of unknown origin;
- the change provably gives the Found;
- every change crossed on the way touches only sets that are not checked.
If the walk stops at a join, print the creation fact instead.
-
F2, state from a returned value. The receiver is bound to #m_result. Print the callee's return refinement projected on the checked sets, or …which says nothing about redoState(undoManager).
-
F3, unconstrained parameter (category UNKNOWN): timeout is a parameter of checkCimReachable(String, int) (line 94) with no refinement. Nothing is said about callers.
-
F4, value returned by a call: failures.size() (ArrayListRefinements.java:162) guarantees only failures.size() >= 0, instantiated and with the ghost conjunct dropped.
Also
- Counterexample for state errors, restricted to the variables of the shown Found, and never showing ghost or state values. For A1_09 it gives
previousMode == BORDERLESS.
- A1_09's nested if-then-else Found, folded under the shown path condition. An arm is dropped only when it folds to false (or one SMT check shows it is infeasible), and it is shown as one row per path.
Mock-ups and soundness conditions per task are in the joint pre-study review. ActivityCatarinaGamboa commented 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
CatarinaGamboa commented 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
- 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?
- 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?
- 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?
added 3 commits that reference this issue on Nov 11, 2026This issue will close once commit 070fb75 is merged into the 'main' branch.070fb75 This issue will close once commit 590268e is merged into the 'main' branch.590268e This issue will close once commit 7886955 is merged into the 'main' branch.7886955
MetadataMetadataDevelopmentNo branches or pull requestsIssue actions
|