Label errors with the kind of mistake they show

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/ErrorStateHintJoinOfAllStates.java

@@ -0,0 +1,24 @@
+package testSuite;
+
+import liquidjava.specification.StateRefinement;
+import liquidjava.specification.StateSet;
+
+@StateSet({"created", "open"})
+public class ErrorStateHintJoinOfAllStates {
+
+    @StateRefinement(to = "created(this)")
+    public ErrorStateHintJoinOfAllStates() {}
+
+    @StateRefinement(from = "created(this)", to = "open(this)")
+    public void open() {}
+
+    @StateRefinement(from = "open(this)")
+    public void read() {}
+
+    public static void use(boolean ready) {
+        ErrorStateHintJoinOfAllStates f = new ErrorStateHintJoinOfAllStates();
+        if (ready)
+            f.open();
+        f.read(); // 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;
     }
@@ -110,10 +121,11 @@ public String toString() {
             sb.append(" --> ").append(String.join("\n     ", counterexample.split("\n"))).append("\n");
         }
 
-        // hint
-        String hint = getHint();
-        if (hint != null && !hint.isBlank()) {
-            sb.append(" --> ").append(String.join("\n     ", hint.split("\n"))).append("\n");
+        // hints
+        if (!hints.isEmpty()) {
+            sb.append("\nHints:\n");
+            for (Hint hint : hints)
+                sb.append("  - ").append(String.join("\n    ", hint.message().split("\n"))).append("\n");
         }
 
         // location

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/diagnostics/hints/StateHints.java

@@ -10,6 +10,7 @@
 import java.util.stream.Collectors;
 import java.util.stream.Stream;
 
+import liquidjava.diagnostics.categories.ErrorCategory;
 import liquidjava.diagnostics.hints.Hint.Kind;
 import liquidjava.processor.context.RefinedFunction;
 import liquidjava.processor.context.Variable;
@@ -20,8 +21,9 @@
 import spoon.reflect.reference.CtTypeReference;
 
 /**
- * Hints for a call made in a state that does not allow it, read from the class's {@link StateMachine}. Each hint only
- * states what the machine proves, so a suggested sequence of calls always makes the failing call verify.
+ * Hints for a call made in a state that does not allow it, read from the class's {@link StateMachine}. The error's
+ * category decides which kinds of hints are given, and each hint only states what the machine proves, so a suggested
+ * sequence of calls always makes the failing call verify.
  */
 public final class StateHints {
 
@@ -44,19 +46,23 @@ private StateHints(StateMachine machine, String receiver) {
      *            the states the receiver can be in before the call
      * @param receiver
      *            the receiver as written in the code
+     * @param category
+     *            the error's category, or {@code null} if it has none
      */
-    public static List<Hint> forCall(StateMachine machine, RefinedFunction call, Set<State> current, String receiver) {
+    public static List<Hint> forCall(StateMachine machine, RefinedFunction call, Set<State> current, String receiver,
+            ErrorCategory category) {
         if (!machine.models(call) || current.isEmpty() || machine.allows(current, call))
             return List.of(); // the machine cannot explain why the call failed
         Set<State> goal = machine.statesAllowing(call);
         if (goal.isEmpty())
             return List.of();
 
         StateHints hints = new StateHints(machine, receiver);
-        if (hints.isUnknown(current))
+        if (category == ErrorCategory.UNPROVABLE)
             return hints.reachingCalls(call, goal);
-        return Stream.concat(hints.howToReach(current, call, goal).stream(), hints.allowedCalls(current).stream())
-                .toList();
+        boolean pathDependent = category == ErrorCategory.PATH_DEPENDENT_STATE;
+        return Stream.concat(hints.howToReach(current, call, goal, pathDependent).stream(),
+                hints.allowedCalls(current).stream()).toList();
     }
 
     /** Nothing is known about the receiver's state: list what leads to a state where {@code call} is allowed */
@@ -74,13 +80,13 @@ private List<Hint> reachingCalls(RefinedFunction call, Set<State> goal) {
                 "The state of %s is unknown here. To get it to %s, use: %s", receiver, names(goal), list(ways))));
     }
 
-    private List<Hint> howToReach(Set<State> current, RefinedFunction call, Set<State> goal) {
+    private List<Hint> howToReach(Set<State> current, RefinedFunction call, Set<State> goal, boolean pathDependent) {
         Optional<List<List<RefinedFunction>>> search = machine.shortestPaths(current, call, MAX_SEQUENCES);
         if (search.isEmpty())
             return List.of();
         List<List<RefinedFunction>> sequences = search.get();
         if (sequences.isEmpty())
-            return machine.complete() ? List.of(unreachable(current, call, goal)) : List.of();
+            return machine.complete() ? List.of(unreachable(current, call, goal, pathDependent)) : List.of();
         if (sequences.get(0).size() > MAX_SEQUENCE_LENGTH)
             return List.of();
         return sequences.stream().map(sequence -> callSequence(current, sequence)).toList();
@@ -95,8 +101,8 @@ private Hint callSequence(Set<State> current, List<RefinedFunction> sequence) {
                 receiver, names(current), names(reached)));
     }
 
-    private Hint unreachable(Set<State> current, RefinedFunction call, Set<State> goal) {
-        if (current.size() > 1)
+    private Hint unreachable(Set<State> current, RefinedFunction call, Set<State> goal, boolean pathDependent) {
+        if (pathDependent)
             return new Hint(Kind.PATH_DEPENDENT_STATE, String.format(
                     "%s can be in %s here, depending on the path taken, and no sequence of calls moves all of them to %s. "
                             + "Make %s reach this line in the same state on every path",
@@ -125,11 +131,6 @@ private List<Hint> allowedCalls(Set<State> current) {
         return List.of();
     }
 
-    /** Whether nothing is known about the state of the receiver */
-    private boolean isUnknown(Set<State> current) {
-        return current.size() == machine.states().size();
-    }
-
     private String call(RefinedFunction method) {
         return receiver + "." + signature(method);
     }

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 {