From 77a1d4eb5f0e91ee2c8294a91dfa692121806c20 Mon Sep 17 00:00:00 2001 From: Catarina Gamboa Date: Sat, 24 Oct 2026 23:58:57 +0100 Subject: [PATCH] Attach the receiver's states to state refinement errors StateRefinementError now carries a StateErrorContext with the receiver, its class, the called method, the states the receiver can be in, the states that allow the call (per state set) and whether the state machine is complete, so clients can show the verifier's answer instead of re-deriving it from the predicates' text. Co-Authored-By: Claude Opus 5.5 --- .../ErrorStateContextArgumentDependent.java | 23 ++++++++ .../diagnostics/errors/StateErrorContext.java | 43 ++++++++++++++ .../errors/StateRefinementError.java | 9 ++- .../diagnostics/hints/StateHints.java | 3 +- .../refinement_checker/TypeChecker.java | 7 ++- .../refinement_checker/VCChecker.java | 6 +- .../object_checkers/AuxStateHandler.java | 19 ++++-- .../processor/state_machine/State.java | 17 +++++- .../state_machine/StateMachineBuilder.java | 7 ++- .../api/tests/TestStateErrorContext.java | 59 +++++++++++++++++++ 10 files changed, 174 insertions(+), 19 deletions(-) create mode 100644 liquidjava-example/src/main/java/testSuite/ErrorStateContextArgumentDependent.java create mode 100644 liquidjava-verifier/src/main/java/liquidjava/diagnostics/errors/StateErrorContext.java create mode 100644 liquidjava-verifier/src/test/java/liquidjava/api/tests/TestStateErrorContext.java diff --git a/liquidjava-example/src/main/java/testSuite/ErrorStateContextArgumentDependent.java b/liquidjava-example/src/main/java/testSuite/ErrorStateContextArgumentDependent.java new file mode 100644 index 00000000..eecf07da --- /dev/null +++ b/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 + } +} diff --git a/liquidjava-verifier/src/main/java/liquidjava/diagnostics/errors/StateErrorContext.java b/liquidjava-verifier/src/main/java/liquidjava/diagnostics/errors/StateErrorContext.java new file mode 100644 index 00000000..716157aa --- /dev/null +++ b/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> possibleStates, + List> acceptedStates, boolean complete) { + + public static StateErrorContext of(StateMachine machine, RefinedFunction call, Set current, + String receiver) { + List> 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> names(Collection states) { + return states.stream().map(State::names).toList(); + } +} diff --git a/liquidjava-verifier/src/main/java/liquidjava/diagnostics/errors/StateRefinementError.java b/liquidjava-verifier/src/main/java/liquidjava/diagnostics/errors/StateRefinementError.java index 27068ab8..4bc2994e 100644 --- a/liquidjava-verifier/src/main/java/liquidjava/diagnostics/errors/StateRefinementError.java +++ b/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 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; + } } diff --git a/liquidjava-verifier/src/main/java/liquidjava/diagnostics/hints/StateHints.java b/liquidjava-verifier/src/main/java/liquidjava/diagnostics/hints/StateHints.java index ef9e1ba9..c3645ef4 100644 --- a/liquidjava-verifier/src/main/java/liquidjava/diagnostics/hints/StateHints.java +++ b/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); } diff --git a/liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/TypeChecker.java b/liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/TypeChecker.java index d88a4a45..8a6886ce 100644 --- a/liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/TypeChecker.java +++ b/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 hints, ErrorCategory category) throws LJError { + Predicate expected, String customMessage, List 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 { diff --git a/liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/VCChecker.java b/liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/VCChecker.java index a3bf1819..0c2f4b9d 100644 --- a/liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/VCChecker.java +++ b/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 hints, ErrorCategory category) - throws StateRefinementError { + Predicate found, Predicate expected, String customMessage, List 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 { diff --git a/liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/object_checkers/AuxStateHandler.java b/liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/object_checkers/AuxStateHandler.java index bbaec9af..11a1f7e4 100644 --- a/liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/object_checkers/AuxStateHandler.java +++ b/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 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 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); diff --git a/liquidjava-verifier/src/main/java/liquidjava/processor/state_machine/State.java b/liquidjava-verifier/src/main/java/liquidjava/processor/state_machine/State.java index d99a36bd..df7d0184 100644 --- a/liquidjava-verifier/src/main/java/liquidjava/processor/state_machine/State.java +++ b/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 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); + } } diff --git a/liquidjava-verifier/src/main/java/liquidjava/processor/state_machine/StateMachineBuilder.java b/liquidjava-verifier/src/main/java/liquidjava/processor/state_machine/StateMachineBuilder.java index 613ec0e9..3713e034 100644 --- a/liquidjava-verifier/src/main/java/liquidjava/processor/state_machine/StateMachineBuilder.java +++ b/liquidjava-verifier/src/main/java/liquidjava/processor/state_machine/StateMachineBuilder.java @@ -90,16 +90,17 @@ private static List statesOf(Context context, String className) { if (stateSets.isEmpty()) return List.of(); - List combinations = List.of(new State("", new Predicate())); + List combinations = List.of(new State(List.of(), new Predicate())); for (List 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 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 { diff --git a/liquidjava-verifier/src/test/java/liquidjava/api/tests/TestStateErrorContext.java b/liquidjava-verifier/src/test/java/liquidjava/api/tests/TestStateErrorContext.java new file mode 100644 index 00000000..880c233e --- /dev/null +++ b/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 errors = Diagnostics.getInstance().getErrors().stream().toList(); + assertEquals(1, errors.size(), "Expected exactly one error from " + test); + return assertInstanceOf(StateRefinementError.class, errors.get(0)).getContext(); + } +}