Attach the receiver's states to state refinement errors

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

@@ -0,0 +1,23 @@
+package testSuite;
+
+import liquidjava.specification.StateRefinement;
+import liquidjava.specification.StateSet;
+
+@StateSet({"open", "closed"})
+public class ErrorStateContextArgumentDependent {
+
+    @StateRefinement(to = "open(this)")
+    public ErrorStateContextArgumentDependent() {}
+
+    @StateRefinement(from = "open(this)", to = "closed(this)")
+    public void close() {}
+
+    // the states that allow it depend on its argument
+    @StateRefinement(from = "closed(this) && attempts > 0", to = "open(this)")
+    public void reopen(int attempts) {}
+
+    public static void main(String[] args) {
+        ErrorStateContextArgumentDependent f = new ErrorStateContextArgumentDependent();
+        f.reopen(1); // Expect: State Refinement Error
+    }
+}

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

@@ -0,0 +1,43 @@
+package liquidjava.diagnostics.errors;
+
+import java.util.Collection;
+import java.util.List;
+import java.util.Set;
+
+import liquidjava.diagnostics.hints.StateHints;
+import liquidjava.processor.context.RefinedFunction;
+import liquidjava.processor.state_machine.State;
+import liquidjava.processor.state_machine.StateMachine;
+
+/**
+ * What the verifier knows about a call made in a state that does not allow it, for clients that show it. Each state is
+ * given by its name in each state set of the class, in the order the sets are declared.
+ *
+ * @param receiver
+ *            the receiver of the call as written in the code
+ * @param receiverClass
+ *            the qualified name of the receiver's class
+ * @param method
+ *            the called method, e.g. {@code open(int)}
+ * @param possibleStates
+ *            the states the receiver can be in before the call
+ * @param acceptedStates
+ *            the states that allow the call, or null if they depend on more than the receiver's state
+ * @param complete
+ *            whether every method that changes the receiver's state is known, so a state that no call reaches is
+ *            unreachable
+ */
+public record StateErrorContext(String receiver, String receiverClass, String method, List<List<String>> possibleStates,
+        List<List<String>> acceptedStates, boolean complete) {
+
+    public static StateErrorContext of(StateMachine machine, RefinedFunction call, Set<State> current,
+            String receiver) {
+        List<List<String>> accepted = machine.models(call) ? names(machine.statesAllowing(call)) : null;
+        return new StateErrorContext(receiver, call.getTargetClass(), StateHints.signature(call), names(current),
+                accepted, machine.complete());
+    }
+
+    private static List<List<String>> names(Collection<State> states) {
+        return states.stream().map(State::names).toList();
+    }
+}

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

@@ -22,10 +22,11 @@ public class StateRefinementError extends LJError {
     private final Predicate expected;
     private final VCSimplificationResult found;
     private final SourcePosition declarationPosition;
+    private final StateErrorContext context;
 
     public StateRefinementError(SourcePosition position, SourcePosition declarationPosition, Predicate expected,
             VCSimplificationResult found, TranslationTable translationTable, String customMessage, List<Hint> hints,
-            ErrorCategory category) {
+            ErrorCategory category, StateErrorContext context) {
         super("State Refinement Error",
                 String.format("found %s but expected %s",
                         found.getImplication().toPredicate().getExpression().toDisplayString(),
@@ -34,6 +35,7 @@ public StateRefinementError(SourcePosition position, SourcePosition declarationP
         this.declarationPosition = declarationPosition;
         this.expected = expected;
         this.found = found;
+        this.context = context;
         hints.forEach(this::addHint);
         setCategory(category);
         if (hints.isEmpty() && isTrue(found.getImplication().toPredicate().getExpression()))
@@ -57,4 +59,9 @@ public VCImplication getFound() {
     public VCSimplificationResult getFoundSimplification() {
         return found;
     }
+
+    /** What is known about the receiver's states, or null if they could not be computed */
+    public StateErrorContext getContext() {
+        return context;
+    }
 }

liquidjava-verifier/src/main/java/liquidjava/diagnostics/hints/StateHints.java

@@ -149,7 +149,8 @@ private String call(RefinedFunction method) {
         return receiver + "." + signature(method);
     }
 
-    private static String signature(RefinedFunction method) {
+    /** A method as shown in hints, e.g. {@code open(int)} */
+    public static String signature(RefinedFunction method) {
         return Utils.getSimpleName(method.getName()) + parameters(method);
     }
 

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

@@ -430,13 +430,14 @@ 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(), null);
+        throwStateRefinementError(position, declarationPosition, found, expected, customMessage, List.of(), null, null);
     }
 
     public void throwStateRefinementError(SourcePosition position, SourcePosition declarationPosition, Predicate found,
-            Predicate expected, String customMessage, List<Hint> hints, ErrorCategory category) throws LJError {
+            Predicate expected, String customMessage, List<Hint> hints, ErrorCategory category,
+            StateErrorContext context) throws LJError {
         vcChecker.throwStateRefinementError(position, declarationPosition, found, expected, customMessage, hints,
-                category);
+                category, context);
     }
 
     public void throwStateConflictError(SourcePosition position, Predicate expectedType) throws LJError {

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

@@ -438,12 +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, ErrorCategory category)
-            throws StateRefinementError {
+            Predicate found, Predicate expected, String customMessage, List<Hint> hints, ErrorCategory category,
+            StateErrorContext context) throws StateRefinementError {
         TranslationTable map = new TranslationTable();
         VCImplication foundState = buildPremiseChain(map, expected, found);
         throw new StateRefinementError(position, declarationPosition, expected, foundState.simplify(), map,
-                customMessage, hints, category);
+                customMessage, hints, category, context);
     }
 
     protected void throwStateConflictError(SourcePosition position, Predicate expected) throws StateConflictError {

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

@@ -10,6 +10,7 @@
 import liquidjava.diagnostics.errors.InvalidRefinementError;
 import liquidjava.diagnostics.errors.LJError;
 import liquidjava.diagnostics.errors.SMTUnknownError;
+import liquidjava.diagnostics.errors.StateErrorContext;
 import liquidjava.diagnostics.hints.Hint;
 import liquidjava.diagnostics.hints.StateHints;
 import liquidjava.processor.context.*;
@@ -661,8 +662,11 @@ private static void changeState(TypeChecker tc, VariableInstance vi, RefinedFunc
             List<Hint> hints = deciding.isPresent()
                     ? receiverOf(invocation).map(r -> StateHints.decidingArgument(deciding.get(), r)).stream().toList()
                     : states.map(r -> stateHints(r, function, category, invocation)).orElse(List.of());
+            StateErrorContext context = states
+                    .map(r -> StateErrorContext.of(r.machine(), function, r.current(), writtenReceiver(invocation)))
+                    .orElse(null);
             tc.throwStateRefinementError(invocation.getPosition(), declarationPosition, prevState,
-                    expectedStatesDisjunction, message, hints, category);
+                    expectedStatesDisjunction, message, hints, category, context);
         }
     }
 
@@ -718,13 +722,18 @@ private static Optional<String> receiverOf(CtElement invocation) {
         if (!(invocation instanceof CtInvocation<?> call))
             return Optional.empty();
         CtExpression<?> target = call.getTarget();
-        if (target == null || target.isImplicit())
-            return Optional.of(Keys.THIS);
-        if (target instanceof CtVariableRead<?> || target instanceof CtThisAccess<?>)
-            return Optional.of(target.toString());
+        if (target == null || target.isImplicit() || target instanceof CtVariableRead<?>
+                || target instanceof CtThisAccess<?>)
+            return Optional.of(writtenReceiver(invocation));
         return Optional.empty();
     }
 
+    /** The receiver of {@code invocation} as written in the code, {@code this} if it is implicit */
+    private static String writtenReceiver(CtElement invocation) {
+        CtExpression<?> target = invocation instanceof CtInvocation<?> call ? call.getTarget() : null;
+        return target == null || target.isImplicit() ? Keys.THIS : target.toString();
+    }
+
     private static Predicate checkOldMentions(Predicate transitionedState, String instanceName,
             String newInstanceName) {
         return transitionedState.changeOldMentions(instanceName, newInstanceName);

liquidjava-verifier/src/main/java/liquidjava/processor/state_machine/State.java

@@ -1,14 +1,25 @@
 package liquidjava.processor.state_machine;
 
+import java.util.List;
+
 import liquidjava.rj_language.Predicate;
 
 /**
  * A state of a class's typestate: one state from each of its state sets
  *
- * @param name
- *            the state names, e.g. {@code open} or {@code open and locked} for a class with two state sets
+ * @param names
+ *            the name of the state in each state set, in the order the sets are declared
  * @param predicate
  *            the predicate that holds for {@code this} in this state
  */
-public record State(String name, Predicate predicate) {
+public record State(List<String> names, Predicate predicate) {
+
+    public State {
+        names = List.copyOf(names);
+    }
+
+    /** The state names, e.g. {@code open} or {@code open and locked} for a class with two state sets */
+    public String name() {
+        return String.join(" and ", names);
+    }
 }

liquidjava-verifier/src/main/java/liquidjava/processor/state_machine/StateMachineBuilder.java

@@ -90,16 +90,17 @@ private static List<State> statesOf(Context context, String className) {
         if (stateSets.isEmpty())
             return List.of();
 
-        List<State> combinations = List.of(new State("", new Predicate()));
+        List<State> combinations = List.of(new State(List.of(), new Predicate()));
         for (List<GhostState> stateSet : stateSets.values())
             combinations = combinations.stream().flatMap(s -> stateSet.stream().map(g -> combine(s, g))).toList();
         return combinations;
     }
 
     private static State combine(State state, GhostState ghostState) {
-        String name = state.name().isEmpty() ? ghostState.getName() : state.name() + " and " + ghostState.getName();
+        List<String> names = new ArrayList<>(state.names());
+        names.add(ghostState.getName());
         Predicate holds = Predicate.createInvocation(ghostState.getQualifiedName(), Predicate.createVar(Keys.THIS));
-        return new State(name, Predicate.createConjunction(state.predicate(), holds));
+        return new State(names, Predicate.createConjunction(state.predicate(), holds));
     }
 
     private StateMachine build(String className, CtTypeReference<?> type) throws LJError {

liquidjava-verifier/src/test/java/liquidjava/api/tests/TestStateErrorContext.java

@@ -0,0 +1,59 @@
+package liquidjava.api.tests;
+
+import static org.junit.jupiter.api.Assertions.*;
+
+import java.util.List;
+
+import org.junit.jupiter.api.Test;
+
+import liquidjava.api.CommandLineLauncher;
+import liquidjava.diagnostics.Diagnostics;
+import liquidjava.diagnostics.errors.LJError;
+import liquidjava.diagnostics.errors.StateErrorContext;
+import liquidjava.diagnostics.errors.StateRefinementError;
+
+class TestStateErrorContext {
+
+    private static final String TEST_SUITE = "../liquidjava-example/src/main/java/testSuite/";
+
+    @Test
+    void callInTheWrongStateHasThePossibleAndAcceptedStates() {
+        assertEquals(
+                new StateErrorContext("f", "testSuite.ErrorStateHintCallSequence", "read()",
+                        List.of(List.of("created")), List.of(List.of("open")), true),
+                contextOf("ErrorStateHintCallSequence.java"));
+    }
+
+    @Test
+    void statesAreNamedInEachStateSet() {
+        assertEquals(
+                new StateErrorContext("d", "testSuite.ErrorStateHintMultipleSets", "open()",
+                        List.of(List.of("closed", "locked")), List.of(List.of("closed", "unlocked")), true),
+                contextOf("ErrorStateHintMultipleSets.java"));
+    }
+
+    @Test
+    void stateDependingOnThePathHasEveryPossibleState() {
+        assertEquals(List.of(List.of("created"), List.of("open")),
+                contextOf("ErrorStateHintPathDependent.java").possibleStates());
+    }
+
+    @Test
+    void transitionDependingOnArgumentsLeavesTheAcceptedStatesUnknown() {
+        StateErrorContext context = contextOf("ErrorStateContextArgumentDependent.java");
+        assertNull(context.acceptedStates());
+        assertFalse(context.complete());
+    }
+
+    @Test
+    void classWithoutStateSetHasNoContext() {
+        assertNull(contextOf("ErrorUnconstrainedStateRefinement.java"));
+    }
+
+    private static StateErrorContext contextOf(String test) {
+        CommandLineLauncher.launch(TEST_SUITE + test);
+        List<LJError> errors = Diagnostics.getInstance().getErrors().stream().toList();
+        assertEquals(1, errors.size(), "Expected exactly one error from " + test);
+        return assertInstanceOf(StateRefinementError.class, errors.get(0)).getContext();
+    }
+}