Repository navigation
Label errors with the kind of mistake they show - #418
Merged
Merged
Conversation
3 tasks done
CatarinaGamboa
force-pushed
the
feat/error-categories
branch
from
October 24, 2026 21:19
c1673bb to
91055a1
Compare
Each error now carries a category from the LiquidJava bug codebook, kept internal for now (not printed): - Out of order: a call in a single state that does not allow it - Out of domain: a value outside its refinement - Path-dependent state: a state that differs between branches, when the class has one state set - Unprovable: nothing is known about the object's state or the value Errors the rules cannot decide get no category. The category picks the kind of state hints, so a hint never contradicts it: a join of every state is now path-dependent rather than unknown. The error message now lists its hints in a Hints section. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>
CatarinaGamboa
force-pushed
the
feat/error-categories
branch
from
October 24, 2026 21:41
91055a1 to
40e993a
Compare
CatarinaGamboa
added a commit
that referenced
this pull request
Oct 24, 2026
## Description Adds the **Argument picks the state** category (codebook C3.1) and a hint for it. These errors had no useful hint before: a transition that depends on an argument isn't part of the state machine, so the existing hints can't explain it. - Each object instance now records the last call that changed its state (`StateChange`). Method calls and constructors record their own call, and state-preserving calls keep the previous record. A join of branches records nothing, which ends the search below. - `DecidingArgument` follows that chain back to the last call that changed a state set the failing call checks. If that call's transition depends on its arguments or result, the SMT solver looks for values that would have allowed the failing call: the state before the call, the call's `to` with its parameters left free, and the failing call's `from`. The model gives the values for the hint. - When such values exist, the category comes before the other state categories. The error then gets only the deciding hint. If none exist, the error keeps its other category (for example `ErrorArgumentCannotPickTheState`). ## Example ``` State Refinement Error: found empty(buffer) but expected filled(buffer) Hints: - buffer.reset(boolean) on line 20 decides the state of buffer: with keep == true, this call would be allowed ``` Category: Argument picks the state (C3.1). ## Measured against the codebook Same runs as #418: - **Corpus:** 94 of 99 right (91 before), 1 wrong, 4 with no category. - **Exercises:** 42 of 52 right (34 before), 6 wrong, 4 with no category. The category now finds 12 of the 15 C3.1 cases. The ones it misses: - a guard in `from` that changes no state; - an earlier value that is the real cause; - a returned value at a join. ## Type of change - [x] New feature ## Checklist - [x] Added tests: - `ErrorArgumentPicksTheState`, `ErrorConstructorArgumentPicksTheState` and `ErrorArgumentPicksTheStateEarlier` (the decider is found past a call on another state set); - `ErrorArgumentCannotPickTheState` (no value helps, so no category change); - cases in `TestErrorCategories` and `TestStateHints`. - [x] `mvn test` passes locally 🤖 Generated with [Claude Code](https://claude.com/claude-code) Co-authored-by: Claude Opus 5.5 <noreply@anthropic.com>
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
Description
Each error now carries a category, taken from the LiquidJava bug codebook, so explanations and visualizations can be targeted to the kind of mistake. It stays internal for now (not printed); clients get it through
LJDiagnostic.getCategory().Errors the rules can't decide get no category:
A category describes the program according to its specification, so it can't tell whether the specification itself is wrong.
Example
Category: Out of order (A1).
The error message now also lists its hints in a
Hints:section, one per line.Hints follow the category
The category is decided first and picks the kind of state hints, so they can't disagree:
Before, the hints made their own decision, so a join of every state (
ErrorStateHintJoinOfAllStates) was reported as path-dependent but hinted as unknown.Measured against the codebook
Run on the codebook's corpus bugs and exercises, counting only errors reported at the recorded line:
15 of the 18 wrong labels are "Argument picks the state" bugs (C3.1), which come out as "Out of order"; a follow-up PR adds that category. The other 3 are exercises whose receiver's state is really unknown to the verifier, so they get "Unprovable".
Type of change
Checklist
TestErrorCategories, plusErrorOutOfDomainArgument,ErrorUnprovableArgumentandErrorPathDependentOtherStateSetmvn testpasses locally🤖 Generated with Claude Code