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(); + } +}