Label errors with the kind of mistake they show

Each error now carries a category from the LiquidJava bug codebook,
printed after its hints:
- 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.

Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>

Author: CatarinaGamboa

liquidjava-example/src/main/java/testSuite/ErrorOutOfDomainArgument.java

@@ -0,0 +1,12 @@
+package testSuite;
+
+import liquidjava.specification.Refinement;
+
+public class ErrorOutOfDomainArgument {
+
+    static void take(@Refinement("_ > 0") int amount) {}
+
+    static void use() {
+        take(-1); // Expect: Refinement Error
+    }
+}

liquidjava-example/src/main/java/testSuite/ErrorPathDependentOtherStateSet.java

@@ -0,0 +1,29 @@
+package testSuite;
+
+import liquidjava.specification.StateRefinement;
+import liquidjava.specification.StateSet;
+
+@StateSet({"closed", "opened"})
+@StateSet({"unlocked", "locked"})
+public class ErrorPathDependentOtherStateSet {
+
+    @StateRefinement(to = "closed(this) && unlocked(this)")
+    public ErrorPathDependentOtherStateSet() {}
+
+    @StateRefinement(from = "closed(this)", to = "opened(this)")
+    public void open() {}
+
+    @StateRefinement(from = "unlocked(this)", to = "locked(this)")
+    public void lock() {}
+
+    @StateRefinement(from = "opened(this)")
+    public void pass() {}
+
+    // the states differ only in the lock, which pass() does not check, so the path is not what is wrong
+    public static void use(boolean secure) {
+        ErrorPathDependentOtherStateSet d = new ErrorPathDependentOtherStateSet();
+        if (secure)
+            d.lock();
+        d.pass(); // Expect: State Refinement Error
+    }
+}

liquidjava-example/src/main/java/testSuite/ErrorUnprovableArgument.java

@@ -0,0 +1,13 @@
+package testSuite;
+
+import liquidjava.specification.Refinement;
+
+public class ErrorUnprovableArgument {
+
+    static void take(@Refinement("_ > 0") int amount) {}
+
+    // nothing is known about amount, so its refinement can be neither violated nor proved
+    static void use(int amount) {
+        take(amount); // Expect: Refinement Error
+    }
+}

liquidjava-verifier/src/main/java/liquidjava/diagnostics/LJDiagnostic.java

@@ -6,8 +6,10 @@
 import java.util.Collections;
 import java.util.List;
 import java.util.Objects;
+import java.util.Optional;
 import java.util.stream.Collectors;
 
+import liquidjava.diagnostics.categories.ErrorCategory;
 import liquidjava.diagnostics.hints.Hint;
 import spoon.reflect.cu.SourcePosition;
 
@@ -21,6 +23,7 @@ public class LJDiagnostic extends RuntimeException {
     private SourcePosition position;
     private final List<Hint> hints = new ArrayList<>();
     private String counterexample;
+    private ErrorCategory category;
     private static final String PIPE = " | ";
 
     public LJDiagnostic(String title, String message, SourcePosition pos, String accentColor, String customMessage) {
@@ -86,6 +89,14 @@ public void addHint(Hint hint) {
         hints.add(hint);
     }
 
+    public Optional<ErrorCategory> getCategory() {
+        return Optional.ofNullable(category);
+    }
+
+    public void setCategory(ErrorCategory category) {
+        this.category = category;
+    }
+
     public void setCounterexampleStr(String counterexample) {
         this.counterexample = counterexample;
     }
@@ -116,6 +127,10 @@ public String toString() {
             sb.append(" --> ").append(String.join("\n     ", hint.split("\n"))).append("\n");
         }
 
+        // category
+        if (category != null)
+            sb.append(" --> Category: ").append(category.title()).append("\n");
+
         // location
         if (file != null && position != null) {
             sb.append("\n").append(file).append(":").append(position.getLine()).append(Colors.RESET).append("\n");

liquidjava-verifier/src/main/java/liquidjava/diagnostics/categories/ErrorCategory.java

@@ -0,0 +1,30 @@
+package liquidjava.diagnostics.categories;
+
+/**
+ * The kind of mistake an error shows, named after the categories of the LiquidJava bug codebook. A category describes
+ * the program according to its specification, so it cannot tell whether the specification itself is wrong.
+ */
+public enum ErrorCategory {
+
+    OUT_OF_ORDER("A1", "Out of order: the operation is legal for this object, but not right now"),
+    OUT_OF_DOMAIN("A2", "Out of domain: the value is outside what is accepted"),
+    PATH_DEPENDENT_STATE("C4.1", "Path-dependent state: the state differs depending on which branch ran"),
+    UNPROVABLE("C4.2", "Unprovable: nothing is known that could prove the requirement");
+
+    private final String id;
+    private final String title;
+
+    ErrorCategory(String id, String title) {
+        this.id = id;
+        this.title = title;
+    }
+
+    /** The id of the category in the codebook */
+    public String id() {
+        return id;
+    }
+
+    public String title() {
+        return title;
+    }
+}

liquidjava-verifier/src/main/java/liquidjava/diagnostics/errors/RefinementError.java

@@ -5,6 +5,7 @@
 import java.util.stream.Collectors;
 
 import liquidjava.diagnostics.TranslationTable;
+import liquidjava.diagnostics.categories.ErrorCategory;
 import liquidjava.diagnostics.hints.Hint;
 import liquidjava.rj_language.Predicate;
 import liquidjava.rj_language.ast.Expression;
@@ -46,11 +47,19 @@ public RefinementError(SourcePosition position, SourcePosition declarationPositi
                     .collect(Collectors.joining(" && "));
             setCounterexampleStr("Counterexample: " + counterexampleString);
         }
+        setCategory(categoryOf(expected, found));
         if (isTrue(found.getImplication().toPredicate().getExpression()))
             addHint(Hint.general(
                     "Not enough information to prove the expected refinement. Add a refinement or condition to constrain it."));
     }
 
+    /** Unprovable when what was found says nothing about the values the expected refinement constrains */
+    private static ErrorCategory categoryOf(Predicate expected, VCSimplificationResult found) {
+        List<String> foundVariables = found.getImplication().toPredicate().getVariableNames();
+        boolean constrained = expected.getVariableNames().stream().anyMatch(foundVariables::contains);
+        return constrained ? ErrorCategory.OUT_OF_DOMAIN : ErrorCategory.UNPROVABLE;
+    }
+
     @Override
     public SourcePosition getDeclarationPosition() {
         return declarationPosition;

liquidjava-verifier/src/main/java/liquidjava/diagnostics/errors/StateRefinementError.java

@@ -5,6 +5,7 @@
 import java.util.List;
 
 import liquidjava.diagnostics.TranslationTable;
+import liquidjava.diagnostics.categories.ErrorCategory;
 import liquidjava.diagnostics.hints.Hint;
 import liquidjava.processor.VCImplication;
 import liquidjava.rj_language.Predicate;
@@ -23,7 +24,8 @@ public class StateRefinementError extends LJError {
     private final SourcePosition declarationPosition;
 
     public StateRefinementError(SourcePosition position, SourcePosition declarationPosition, Predicate expected,
-            VCSimplificationResult found, TranslationTable translationTable, String customMessage, List<Hint> hints) {
+            VCSimplificationResult found, TranslationTable translationTable, String customMessage, List<Hint> hints,
+            ErrorCategory category) {
         super("State Refinement Error",
                 String.format("found %s but expected %s",
                         found.getImplication().toPredicate().getExpression().toDisplayString(),
@@ -33,6 +35,7 @@ public StateRefinementError(SourcePosition position, SourcePosition declarationP
         this.expected = expected;
         this.found = found;
         hints.forEach(this::addHint);
+        setCategory(category);
         if (hints.isEmpty() && isTrue(found.getImplication().toPredicate().getExpression()))
             addHint(Hint.general(
                     "No state information is known for this object. Make sure its state is initialized and available at this point."));

liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/TypeChecker.java

@@ -9,6 +9,7 @@
 
 import liquidjava.diagnostics.Diagnostics;
 import liquidjava.diagnostics.errors.*;
+import liquidjava.diagnostics.categories.ErrorCategory;
 import liquidjava.diagnostics.hints.Hint;
 import liquidjava.diagnostics.warnings.UnsatisfiableRefinementWarning;
 import liquidjava.processor.context.AliasWrapper;
@@ -425,12 +426,13 @@ public void throwRefinementError(SourcePosition position, SourcePosition declara
 
     public void throwStateRefinementError(SourcePosition position, SourcePosition declarationPosition, Predicate found,
             Predicate expected, String customMessage) throws LJError {
-        throwStateRefinementError(position, declarationPosition, found, expected, customMessage, List.of());
+        throwStateRefinementError(position, declarationPosition, found, expected, customMessage, List.of(), null);
     }
 
     public void throwStateRefinementError(SourcePosition position, SourcePosition declarationPosition, Predicate found,
-            Predicate expected, String customMessage, List<Hint> hints) throws LJError {
-        vcChecker.throwStateRefinementError(position, declarationPosition, found, expected, customMessage, hints);
+            Predicate expected, String customMessage, List<Hint> hints, ErrorCategory category) throws LJError {
+        vcChecker.throwStateRefinementError(position, declarationPosition, found, expected, customMessage, hints,
+                category);
     }
 
     public void throwStateConflictError(SourcePosition position, Predicate expectedType) throws LJError {

liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/VCChecker.java

@@ -12,6 +12,7 @@
 import liquidjava.diagnostics.errors.*;
 import liquidjava.diagnostics.DebugLog;
 import liquidjava.diagnostics.TranslationTable;
+import liquidjava.diagnostics.categories.ErrorCategory;
 import liquidjava.diagnostics.hints.Hint;
 import liquidjava.processor.VCImplication;
 import liquidjava.processor.context.*;
@@ -437,11 +438,12 @@ protected void throwRefinementError(SourcePosition position, SourcePosition decl
     }
 
     protected void throwStateRefinementError(SourcePosition position, SourcePosition declarationPosition,
-            Predicate found, Predicate expected, String customMessage, List<Hint> hints) throws StateRefinementError {
+            Predicate found, Predicate expected, String customMessage, List<Hint> hints, ErrorCategory category)
+            throws StateRefinementError {
         TranslationTable map = new TranslationTable();
         VCImplication foundState = buildPremiseChain(map, expected, found);
         throw new StateRefinementError(position, declarationPosition, expected, foundState.simplify(), map,
-                customMessage, hints);
+                customMessage, hints, category);
     }
 
     protected void throwStateConflictError(SourcePosition position, Predicate expected) throws StateConflictError {

liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/object_checkers/AuxStateHandler.java

@@ -5,6 +5,7 @@
 import java.util.stream.Collectors;
 
 import liquidjava.diagnostics.DebugLog;
+import liquidjava.diagnostics.categories.ErrorCategory;
 import liquidjava.diagnostics.errors.IllegalConstructorTransitionError;
 import liquidjava.diagnostics.errors.InvalidRefinementError;
 import liquidjava.diagnostics.errors.LJError;
@@ -15,6 +16,7 @@
 import liquidjava.processor.refinement_checker.TypeChecker;
 import liquidjava.processor.refinement_checker.TypeCheckingUtils;
 import liquidjava.processor.state_machine.State;
+import liquidjava.processor.state_machine.StateErrorCategories;
 import liquidjava.processor.state_machine.StateMachine;
 import liquidjava.processor.state_machine.StateMachineBuilder;
 import liquidjava.processor.state_machine.StateSolver;
@@ -643,35 +645,47 @@ private static void changeState(TypeChecker tc, VariableInstance vi, RefinedFunc
             SourcePosition declarationPosition = stateChanges.stream().filter(ObjectState::hasFrom)
                     .map(ObjectState::getFromPosition).filter(Objects::nonNull).findFirst()
                     .orElse(function.getPlacementInCode().getPosition());
-            List<Hint> hints = stateHints(tc, function, instanceName, prevState, invocation);
+            Optional<ReceiverStates> states = receiverStates(tc, function, instanceName, prevState, invocation);
+            List<Hint> hints = states.map(r -> stateHints(r, function, invocation)).orElse(List.of());
+            ErrorCategory category = states.flatMap(r -> StateErrorCategories.categorize(r.machine(), r.current(),
+                    prevState, getGhostStatesFor(function.getTargetClass(), tc))).orElse(null);
             tc.throwStateRefinementError(invocation.getPosition(), declarationPosition, prevState,
-                    expectedStatesDisjunction, message, hints);
+                    expectedStatesDisjunction, message, hints, category);
         }
     }
 
+    /** The state machine of the receiver's class and the states the receiver can be in before a call */
+    private record ReceiverStates(StateMachine machine, Set<State> current) {
+    }
+
     /**
-     * Hints on how to fix a call to {@code function} made in a state that does not allow it. They are best effort: if
-     * they cannot be computed, the error is reported without them
+     * The receiver's states before a call to {@code function} that its state does not allow. Best effort: if they
+     * cannot be computed, the error is reported without hints or category
      */
-    private static List<Hint> stateHints(TypeChecker tc, RefinedFunction function, String instanceName, Predicate state,
-            CtElement invocation) {
-        Optional<String> receiver = receiverOf(invocation);
-        if (receiver.isEmpty() || !StateMachineBuilder.canModel(function))
-            return List.of();
+    private static Optional<ReceiverStates> receiverStates(TypeChecker tc, RefinedFunction function,
+            String instanceName, Predicate state, CtElement invocation) {
         try {
             Optional<StateMachine> machine = tc.getStateMachine(function.getTargetClass(), invocation);
             if (machine.isEmpty())
-                return List.of();
+                return Optional.empty();
             Set<State> current = new StateSolver(tc, invocation.getPosition()).possibleStates(machine.get().states(),
                     state, instanceName);
-            return StateHints.forCall(machine.get(), function, current, receiver.get());
+            return Optional.of(new ReceiverStates(machine.get(), current));
         } catch (RuntimeException e) {
-            // a failure to compute hints must not replace the error being reported
-            DebugLog.warn("Could not compute state hints: " + e.getMessage());
-            return List.of();
+            // a failure to analyse the states must not replace the error being reported
+            DebugLog.warn("Could not compute the receiver's states: " + e.getMessage());
+            return Optional.empty();
         }
     }
 
+    /** Hints on how to fix a call to {@code function} made in a state that does not allow it */
+    private static List<Hint> stateHints(ReceiverStates states, RefinedFunction function, CtElement invocation) {
+        Optional<String> receiver = receiverOf(invocation);
+        if (receiver.isEmpty() || !StateMachineBuilder.canModel(function))
+            return List.of();
+        return StateHints.forCall(states.machine(), function, states.current(), receiver.get());
+    }
+
     /**
      * The receiver of {@code invocation} as written in the code, if it names an object that calls can be added to: a
      * variable, a field or {@code this}