diff --git a/liquidjava-example/src/main/java/testSuite/ErrorStateSetNameInSuperclass.java b/liquidjava-example/src/main/java/testSuite/ErrorStateSetNameInSuperclass.java new file mode 100644 index 00000000..1208429e --- /dev/null +++ b/liquidjava-example/src/main/java/testSuite/ErrorStateSetNameInSuperclass.java @@ -0,0 +1,29 @@ +package testSuite; + +import liquidjava.specification.StateRefinement; +import liquidjava.specification.StateSet; + +// The class and its superclass each have a set named phase: their states keep the shorthand, since phase == ready +// and phase == busy would read as two values of one set +@StateSet(name = "phase", value = {"ready", "done"}) +class ErrorStateSetNameInSuperclassBase { + @StateRefinement(to = "ready(this)") + ErrorStateSetNameInSuperclassBase() {} +} + +@StateSet(name = "phase", value = {"busy", "idle"}) +public class ErrorStateSetNameInSuperclass extends ErrorStateSetNameInSuperclassBase { + @StateRefinement(to = "ready(this) && idle(this)") + ErrorStateSetNameInSuperclass() {} + + @StateRefinement(from = "idle(this)", to = "busy(this)") + void start() {} + + @StateRefinement(from = "ready(this) && busy(this)") + void use() {} + + public static void main(String[] args) { + ErrorStateSetNameInSuperclass c = new ErrorStateSetNameInSuperclass(); + c.use(); // Expect: State Refinement Error + } +} diff --git a/liquidjava-verifier/src/main/java/liquidjava/diagnostics/LJDiagnostic.java b/liquidjava-verifier/src/main/java/liquidjava/diagnostics/LJDiagnostic.java index 6eafd068..6224bb67 100644 --- a/liquidjava-verifier/src/main/java/liquidjava/diagnostics/LJDiagnostic.java +++ b/liquidjava-verifier/src/main/java/liquidjava/diagnostics/LJDiagnostic.java @@ -75,6 +75,11 @@ public List getMessageNotes() { return List.of(); } + /** Lines printed under the excerpt of where the refinement is declared that explain it */ + public List getDeclarationNotes() { + return List.of(); + } + public void setPosition(SourcePosition pos) { if (pos == null || pos.getFile() == null) return; @@ -145,8 +150,11 @@ public String toString() { if (declPos != null && declPos.getFile() != null && !declPos.equals(position)) { sb.append(Colors.CYAN).append("\n--> Refinement declared here:\n").append(Colors.RESET); String declarationSnippet = getSnippet(declPos, 1, 1, Colors.CYAN, null, true); - if (declarationSnippet != null) + if (declarationSnippet != null) { sb.append(declarationSnippet); + for (String note : getDeclarationNotes()) + sb.append(" ").append(note).append("\n"); + } sb.append("\n").append(declPos.getFile().getPath()).append(":").append(declPos.getLine()) .append(Colors.RESET).append("\n"); 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 d1c58ed6..139ebba9 100644 --- a/liquidjava-verifier/src/main/java/liquidjava/diagnostics/errors/StateRefinementError.java +++ b/liquidjava-verifier/src/main/java/liquidjava/diagnostics/errors/StateRefinementError.java @@ -26,15 +26,19 @@ public class StateRefinementError extends LJError { private final VCSimplificationResult found; private final SourcePosition declarationPosition; private final StateErrorContext context; + private final List declarationNotes; /** * @param display * rewrites expected and found as the error shows them, here and to the IDE, after the facts to show are * chosen on them as given + * @param declarationNotes + * lines that explain the declaration, printed under its excerpt */ public StateRefinementError(SourcePosition position, SourcePosition declarationPosition, Predicate expected, VCSimplificationResult found, TranslationTable translationTable, String customMessage, List hints, - ErrorCategory category, StateErrorContext context, UnaryOperator display) { + ErrorCategory category, StateErrorContext context, UnaryOperator display, + List declarationNotes) { super("State Refinement Error", ErrorMessage.of(expected.getExpression(), found, translationTable, StateRefinementError::appliesGhost, "found %s but expected %s", display), position, translationTable, customMessage); @@ -42,6 +46,7 @@ public StateRefinementError(SourcePosition position, SourcePosition declarationP this.expected = new Predicate(display.apply(expected.getExpression())); this.found = found.map(display); this.context = context; + this.declarationNotes = declarationNotes; hints.forEach(this::addHint); setCategory(category); if (hints.isEmpty() && isTrue(found.getImplication().toPredicate().getExpression())) @@ -56,6 +61,11 @@ private static boolean appliesGhost(Expression expression) { || expression.getChildren().stream().anyMatch(StateRefinementError::appliesGhost); } + @Override + public List getDeclarationNotes() { + return declarationNotes; + } + @Override public SourcePosition getDeclarationPosition() { return declarationPosition; 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 62629559..7bd300d7 100644 --- a/liquidjava-verifier/src/main/java/liquidjava/diagnostics/hints/StateHints.java +++ b/liquidjava-verifier/src/main/java/liquidjava/diagnostics/hints/StateHints.java @@ -7,6 +7,7 @@ import java.util.Set; import java.util.TreeSet; import java.util.function.Supplier; +import java.util.function.Function; import java.util.stream.Collectors; import java.util.stream.Stream; @@ -41,10 +42,21 @@ public final class StateHints { private final List> goals; /** The state sets the failing call checks, as indexes into {@link State#names()} */ private final Set checkedSets; + /** The name of the state set a state is shown as a value of, or empty when it keeps the shorthand */ + private final Function> setNameOf; + /** + * Whether states are shown as the error's message shows them, e.g. {@code lockState(d) == locked}: when some state + * set of the class is shown by its name + */ + private final boolean asValues; - private StateHints(StateMachine machine, String receiver, RefinedFunction call) { + private StateHints(StateMachine machine, String receiver, RefinedFunction call, + Function> setNameOf) { this.machine = machine; this.receiver = receiver; + this.setNameOf = setNameOf; + this.asValues = machine.states().stream().flatMap(s -> s.names().stream()) + .anyMatch(name -> setNameOf.apply(name).isPresent()); this.goals = machine.statesAllowingByRefinement(call); this.checkedSets = goals.stream().flatMap(g -> machine.stateSetsNamed(g).stream()) .collect(Collectors.toCollection(TreeSet::new)); @@ -62,12 +74,15 @@ private StateHints(StateMachine machine, String receiver, RefinedFunction call) * @param checkedElsewhere * whether the receiver's state was checked elsewhere, though not decided, e.g. by an earlier call whose * result says which state it is in + * @param setNameOf + * the name of the state set the error's message shows a state as a value of, or empty when it shows the + * shorthand */ public static List forCall(StateMachine machine, RefinedFunction call, Set current, String receiver, - ErrorCategory category, boolean checkedElsewhere) { + ErrorCategory category, boolean checkedElsewhere, Function> setNameOf) { if (!machine.models(call) || current.isEmpty() || machine.allows(current, call)) return List.of(); // the machine cannot explain why the call failed - StateHints hints = new StateHints(machine, receiver, call); + StateHints hints = new StateHints(machine, receiver, call, setNameOf); if (hints.goals.isEmpty()) return List.of(); @@ -107,7 +122,7 @@ public static Hint decidingArgument(DecidingArgument deciding, String receiver) private List anyState(Set current, RefinedFunction call, boolean checkedElsewhere) { String known = checkedElsewhere ? "What is known here does not decide the state of " + receiver : "The state of " + receiver + " is unknown here"; - String message = known + ", and this call needs it to be " + needed(); + String message = known + ", and this call needs " + (asValues ? "" : "it to be ") + needed(); message += newObjects(call).map(c -> ". Objects created with " + c + " start in such a state").orElse(""); List hints = new ArrayList<>(); hints.add(new Hint(Kind.NEEDED_STATE, message)); @@ -161,8 +176,8 @@ private List guard(Set current, RefinedFunction call) { String check = (negated ? "!" : "") + guardCall(guard.method()); String arguments = guard.method().getArguments().isEmpty() ? "" : ", filling in the arguments of " + declaration(guard.method()); - String message = String.format("Guard this call with if (%s)%s: when it returns %s, %s is %s", check, arguments, - !negated, receiver, needed()); + String message = String.format("Guard this call with if (%s)%s: when it returns %s, %s", check, arguments, + !negated, (asValues ? "" : receiver + " is ") + needed()); return List.of(new Hint(Kind.GUARD, message)); } @@ -206,6 +221,11 @@ private Hint callSequence(Set current, List sequence, boolea } private Hint unreachable(Set current, RefinedFunction call, boolean pathDependent) { + if (pathDependent && asValues) + return new Hint(Kind.PATH_DEPENDENT_STATE, String.format( + "Depending on the path taken, %s here, and no sequence of calls moves %s from all of them to %s. " + + "Make %s reach this line in the same state on every path", + namesHere(current), receiver, needed(), receiver)); 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. " @@ -222,13 +242,15 @@ private List allowedCalls(Set current) { if (!allowed.isEmpty()) { List signatures = allowed.stream().map(StateHints::signature).toList(); String others = machine.complete() ? "" : " (and possibly others)"; - return List.of(new Hint(Kind.AVAILABLE_CALLS, String.format("In state %s, %s can call: %s%s", - namesHere(current), receiver, list(signatures), others))); + return List.of(new Hint(Kind.AVAILABLE_CALLS, String.format("%s %s, %s can call: %s%s", + asValues ? "When" : "In state", namesHere(current), receiver, list(signatures), others))); } boolean noCallsInAnyState = current.stream().allMatch(s -> machine.allowedIn(Set.of(s)).isEmpty()); if (machine.complete() && noCallsInAnyState) - return List.of(new Hint(Kind.FINAL_STATE, - String.format("%s is in state %s, where none of its methods with state refinements can be called", + return List.of(new Hint(Kind.FINAL_STATE, asValues + ? String.format("When %s, none of the methods of %s with state refinements can be called", + namesHere(current), receiver) + : String.format("%s is in state %s, where none of its methods with state refinements can be called", receiver, namesHere(current)))); return List.of(); } @@ -311,11 +333,26 @@ private String needed() { Set goal = machine.ordered(goals.stream().flatMap(Set::stream).toList()); if (goal.size() < machine.states().size()) return names(goal); - return goals.stream().map(this::names).distinct().collect(Collectors.joining(" or ")); + return join(goals.stream().flatMap(g -> machine.describe(g).stream()).distinct().toList()); } - private static String join(List> groups) { - return groups.stream().map(group -> String.join(" and ", group)).collect(Collectors.joining(" or ")); + /** The groups joined by {@code or}, each in parentheses if it has several states and there are other groups */ + private String join(List> groups) { + return groups.stream().map(group -> { + String states = group.stream().map(this::stateName).collect(Collectors.joining(" and ")); + return groups.size() > 1 && group.size() > 1 ? "(" + states + ")" : states; + }).collect(Collectors.joining(" or ")); + } + + /** + * A state as the error's message shows it, e.g. {@code lockState(d) == locked}, or {@code closed(d)} for a state + * that keeps the shorthand, or only its name if no state set of the class is shown by its name + */ + private String stateName(String state) { + if (!asValues) + return state; + return setNameOf.apply(state).map(set -> set + "(" + receiver + ") == " + state) + .orElse(state + "(" + receiver + ")"); } private static String list(List items) { diff --git a/liquidjava-verifier/src/main/java/liquidjava/processor/context/ObjectState.java b/liquidjava-verifier/src/main/java/liquidjava/processor/context/ObjectState.java index 3d03fd95..8d44fba1 100644 --- a/liquidjava-verifier/src/main/java/liquidjava/processor/context/ObjectState.java +++ b/liquidjava-verifier/src/main/java/liquidjava/processor/context/ObjectState.java @@ -7,6 +7,8 @@ public class ObjectState { Predicate from; Predicate to; + /** {@code from} as written, before states written as values of their sets are read as the shorthand */ + Predicate writtenFrom; SourcePosition fromPosition; SourcePosition toPosition; String message; @@ -33,6 +35,14 @@ public void setTo(Predicate to) { this.to = to; } + public Predicate getWrittenFrom() { + return writtenFrom; + } + + public void setWrittenFrom(Predicate writtenFrom) { + this.writtenFrom = writtenFrom; + } + public SourcePosition getFromPosition() { return fromPosition; } @@ -77,6 +87,7 @@ public ObjectState clone() { Predicate clonedFrom = from == null ? null : from.clone(); Predicate clonedTo = to == null ? null : to.clone(); ObjectState clone = new ObjectState(clonedFrom, clonedTo, message); + clone.setWrittenFrom(writtenFrom); clone.setFromPosition(fromPosition); clone.setToPosition(toPosition); return clone; 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 4bcaf9ff..f01e4f6e 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 @@ -588,14 +588,15 @@ 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, null); + throwStateRefinementError(position, declarationPosition, found, expected, customMessage, List.of(), null, null, + List.of()); } public void throwStateRefinementError(SourcePosition position, SourcePosition declarationPosition, Predicate found, Predicate expected, String customMessage, List hints, ErrorCategory category, - StateErrorContext context) throws LJError { + StateErrorContext context, List declarationNotes) throws LJError { vcChecker.throwStateRefinementError(position, declarationPosition, found, expected, customMessage, hints, - category, context); + category, context, declarationNotes); } 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 86749010..84d285e4 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 @@ -457,7 +457,7 @@ protected Predicate shownFound(Predicate found, Predicate expected) { protected void throwStateRefinementError(SourcePosition position, SourcePosition declarationPosition, Predicate found, Predicate expected, String customMessage, List hints, ErrorCategory category, - StateErrorContext context) throws StateRefinementError { + StateErrorContext context, List declarationNotes) throws StateRefinementError { TranslationTable map = new TranslationTable(); VCImplication foundState = buildPremiseChain(map, expected, found); VCSimplificationResult simplified = foundState.simplify(NeededVariables.forStateError(expected)); @@ -465,7 +465,8 @@ protected void throwStateRefinementError(SourcePosition position, SourcePosition new VCRelevantFacts(expected.getExpression(), this::ghostFunctionsOf)); throw new StateRefinementError(position, declarationPosition, expected, shown, map, customMessage, hints, category, context, - e -> StateValues.toSetForm(e, this.context.getGhostStates(), this.context.getGhosts())); + e -> StateValues.toSetForm(e, this.context.getGhostStates(), this.context.getGhosts()), + declarationNotes); } /** The ghost functions an invocation name stands for: a state's state set function, or the ghost itself */ 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 c2d00a08..6c1d7167 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 @@ -23,6 +23,9 @@ import liquidjava.processor.state_machine.StateMachineBuilder; import liquidjava.processor.state_machine.StateSolver; import liquidjava.rj_language.Predicate; +import liquidjava.rj_language.StateValues; +import liquidjava.rj_language.ast.Expression; +import liquidjava.rj_language.ast.FunctionInvocation; import liquidjava.utils.GeneratedNames; import liquidjava.utils.Utils; import liquidjava.utils.constants.Formats; @@ -411,7 +414,9 @@ private static ObjectState getStates(CtAnnotation ctAnnota // has from if (from != null) { - state.setFrom(createStatePredicate(new Predicate(from, e, prefix), from, f.getTargetClass(), tc, e, false)); + Predicate written = new Predicate(from, e, prefix); + state.setWrittenFrom(written); + state.setFrom(createStatePredicate(written, from, f.getTargetClass(), tc, e, false)); state.setFromPosition(Utils.getLJAnnotationPosition(e, from)); } @@ -791,9 +796,12 @@ private static void changeState(TypeChecker tc, VariableInstance vi, RefinedFunc // combine messages of all state changes String message = stateChanges.stream().map(ObjectState::getMessage) .filter(msg -> msg != null && !msg.isBlank()).distinct().collect(Collectors.joining("\n")); - SourcePosition declarationPosition = stateChanges.stream().filter(ObjectState::hasFrom) - .map(ObjectState::getFromPosition).filter(Objects::nonNull).findFirst() + Optional declaration = stateChanges.stream().filter(ObjectState::hasFrom) + .filter(s -> s.getFromPosition() != null).findFirst(); + SourcePosition declarationPosition = declaration.map(ObjectState::getFromPosition) .orElse(function.getPlacementInCode().getPosition()); + List declarationNotes = declaration.map(ObjectState::getWrittenFrom).filter(Objects::nonNull) + .map(written -> declarationNotes(written.getExpression(), tc.getContext())).orElse(List.of()); List ghostStates = getGhostStatesFor(function.getTargetClass(), tc); Optional deciding = decidingArgument(tc, vi, function, ghostStates, invocation); Optional states = receiverStates(tc, function, vi, prevState, invocation); @@ -805,15 +813,38 @@ private static void changeState(TypeChecker tc, VariableInstance vi, RefinedFunc .orElse(null); List hints = deciding.isPresent() ? receiverOf(invocation).map(r -> StateHints.decidingArgument(deciding.get(), r)).stream().toList() - : states.map(r -> stateHints(r, function, category, checked, invocation)).orElse(List.of()); + : states.map(r -> stateHints(tc, r, function, category, checked, 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, context); + expectedStatesDisjunction, message, hints, category, context, declarationNotes); } } + /** + * What each state of a named set that {@code written} writes as the shorthand means as the error's message shows + * it, e.g. {@code where closed(this) means doorState(this) == closed}: the declaration is shown as written + */ + private static List declarationNotes(Expression written, Context context) { + List meanings = new ArrayList<>(); + addMeanings(written, context, meanings); + return meanings.isEmpty() ? List.of() : List.of("where " + String.join(", ", meanings)); + } + + private static void addMeanings(Expression e, Context context, List meanings) { + if (e instanceof FunctionInvocation state && state.getArgs().size() == 1 + && StateValues.setNameOf(state.getName(), context.getGhostStates(), context.getGhosts()).isPresent()) { + String meaning = state.toDisplayString() + " means " + + StateValues.toSetForm(state, context.getGhostStates(), context.getGhosts()).toDisplayString(); + if (!meanings.contains(meaning)) + meanings.add(meaning); + return; + } + for (Expression child : e.getChildren()) + addMeanings(child, context, meanings); + } + /** * The state machine of the receiver's class, the states the receiver can be in before a call, and the ghost states * of the class and its supertypes @@ -883,13 +914,15 @@ private static Optional decidingArgument(TypeChecker tc, Varia * Hints on how to fix a call to {@code function} made in a state that does not allow it. Best effort, like * {@link #receiverStates}: the machine asks the solver about some calls only when a hint needs them */ - private static List stateHints(ReceiverStates states, RefinedFunction function, ErrorCategory category, - boolean checked, CtElement invocation) { + private static List stateHints(TypeChecker tc, ReceiverStates states, RefinedFunction function, + ErrorCategory category, boolean checked, CtElement invocation) { Optional receiver = receiverOf(invocation); if (receiver.isEmpty() || !StateMachineBuilder.canModel(function)) return List.of(); + Context context = tc.getContext(); try { - return StateHints.forCall(states.machine(), function, states.current(), receiver.get(), category, checked); + return StateHints.forCall(states.machine(), function, states.current(), receiver.get(), category, checked, + state -> StateValues.setNameOf(state, context.getGhostStates(), context.getGhosts())); } catch (RuntimeException e) { DebugLog.warn("Could not compute the state hints: " + e.getMessage()); return List.of(); diff --git a/liquidjava-verifier/src/main/java/liquidjava/rj_language/StateValues.java b/liquidjava-verifier/src/main/java/liquidjava/rj_language/StateValues.java index 369ac126..77862087 100644 --- a/liquidjava-verifier/src/main/java/liquidjava/rj_language/StateValues.java +++ b/liquidjava-verifier/src/main/java/liquidjava/rj_language/StateValues.java @@ -123,17 +123,31 @@ private static Expression rewriteToSetForm(Expression e, List states /** {@code set(e) op state} when {@code e} is the state {@code state(e)} of a set with one, given name */ private static Optional setValue(Expression e, String op, List states, List ghosts) { - if (!(e instanceof FunctionInvocation invocation && invocation.getArgs().size() == 1) - || ghosts.stream().anyMatch(g -> g.matches(invocation.getName())) - || states.stream().anyMatch(s -> s.getParent() == null && s.matches(invocation.getName()))) + if (!(e instanceof FunctionInvocation invocation && invocation.getArgs().size() == 1)) return Optional.empty(); - List setNames = states.stream().filter(s -> s.getParent() != null && s.matches(invocation.getName())) + return setNameOf(invocation.getName(), states, ghosts).map(setName -> new BinaryExpression( + new FunctionInvocation(qualifiedLike(invocation.getName(), setName), + List.of(invocation.getArgs().get(0).clone())), + op, new Var(Utils.getSimpleName(invocation.getName())))); + } + + /** + * The name of the state set that {@link #toSetForm} shows the state {@code state} as a value of, or empty when it + * keeps the shorthand. It also keeps it when sets of different classes have that set name, e.g. a class and its + * superclass: their values would read as values of one set + */ + public static Optional setNameOf(String state, List states, List ghosts) { + if (ghosts.stream().anyMatch(g -> g.matches(state)) + || states.stream().anyMatch(s -> s.getParent() == null && s.matches(state))) + return Optional.empty(); + List setNames = states.stream().filter(s -> s.getParent() != null && s.matches(state)) .map(s -> s.getParent().getName()).distinct().toList(); if (setNames.size() != 1 || setNames.get(0).matches(Formats.STATE_SET_NAMES)) return Optional.empty(); - FunctionInvocation set = new FunctionInvocation(qualifiedLike(invocation.getName(), setNames.get(0)), - List.of(invocation.getArgs().get(0).clone())); - return Optional.of(new BinaryExpression(set, op, new Var(Utils.getSimpleName(invocation.getName())))); + long setsWithName = states.stream().map(GhostState::getParent) + .filter(p -> p != null && p.getName().equals(setNames.get(0))).map(GhostFunction::getQualifiedName) + .distinct().count(); + return setsWithName == 1 ? Optional.of(setNames.get(0)) : Optional.empty(); } /** The states of {@code set}, or only those named {@code name} when it is not null */ diff --git a/liquidjava-verifier/src/test/java/liquidjava/api/tests/TestStateHints.java b/liquidjava-verifier/src/test/java/liquidjava/api/tests/TestStateHints.java index 9b6a9c2a..f22dc673 100644 --- a/liquidjava-verifier/src/test/java/liquidjava/api/tests/TestStateHints.java +++ b/liquidjava-verifier/src/test/java/liquidjava/api/tests/TestStateHints.java @@ -38,9 +38,10 @@ void missingCallsAreSuggestedInOrder() { @Test void callSequenceNamesOnlyTheStateSetsItChanges() { - assertHints("ErrorStateHintMultipleSets.java", - new Hint(Kind.CALL_SEQUENCE, "Call d.unlock() before this call to move d from locked to unlocked"), - new Hint(Kind.AVAILABLE_CALLS, "In state closed and locked, d can call: unlock()")); + assertHints("ErrorStateHintMultipleSets.java", new Hint(Kind.CALL_SEQUENCE, + "Call d.unlock() before this call to move d from lockState(d) == locked to lockState(d) == unlocked"), + new Hint(Kind.AVAILABLE_CALLS, + "When doorState(d) == closed and lockState(d) == locked, d can call: unlock()")); } @Test @@ -200,14 +201,14 @@ void failedCheckOfTheReceiverIsNotAnUnknownState() { void joinsAreNotTakenForAnUnknownState() { List errors = errors("ErrorStateHintJoins.java", 2); assertHints(errors.get(0), new Hint(Kind.UNREACHABLE_STATE, - "No sequence of calls moves d from closed and unlocked or closed and locked or opened and unlocked " - + "or opened and locked to closed and unlocked. " + "No sequence of calls moves d from (closed and unlocked) or (closed and locked) or (opened and unlocked) " + + "or (opened and locked) to closed and unlocked. " + "Create a new object instead with new ErrorStateHintJoins()")); assertHints(errors.get(1), new Hint(Kind.UNREACHABLE_STATE, - "No sequence of calls moves d from closed and unlocked or opened and unlocked to closed and unlocked. " + "No sequence of calls moves d from (closed and unlocked) or (opened and unlocked) to closed and unlocked. " + "Create a new object instead with new ErrorStateHintJoins()"), new Hint(Kind.AVAILABLE_CALLS, - "In state closed and unlocked or opened and unlocked, d can call: lock()")); + "In state (closed and unlocked) or (opened and unlocked), d can call: lock()")); assertEquals(Optional.empty(), errors.get(0).getCategory()); } @@ -345,13 +346,26 @@ void foundKeepsANamedStateSetByItsName() { assertEquals( "found doorState(d@26) == closed && lockState(d) == locked && doorState(d) == doorState(d@26) but expected doorState(d) == closed && lockState(d) == unlocked", error.getMessage().replaceAll("[⁰¹²³⁴⁵⁶⁷⁸⁹]", "")); + // the declaration is shown as written, with what its states mean under it + assertTrue(error.toString().contains(" where closed(this) means doorState(this) == closed, " + + "unlocked(this) means lockState(this) == unlocked\n")); + } + + @Test + void setNameOfTheClassAndOfItsSuperclassKeepsTheShorthand() { + StateRefinementError error = errors("ErrorStateSetNameInSuperclass.java", 1).get(0); + assertEquals("found ready(c) && idle(c) but expected ready(c) && busy(c)", + error.getMessage().replaceAll("[⁰¹²³⁴⁵⁶⁷⁸⁹]", "")); + assertHints(error, new Hint(Kind.CALL_SEQUENCE, "Call c.start() before this call to move c from idle to busy"), + new Hint(Kind.AVAILABLE_CALLS, "In state idle and ready, c can call: start()")); } @Test void queryWrittenWithItsStateSetIsOfferedAsAGuard() { assertHints("ErrorStateValueQuery.java", - new Hint(Kind.NEEDED_STATE, "The state of d is unknown here, and this call needs it to be unlocked"), - new Hint(Kind.GUARD, "Guard this call with if (d.isUnlocked()): when it returns true, d is unlocked")); + new Hint(Kind.NEEDED_STATE, "The state of d is unknown here, and this call needs lock(d) == unlocked"), + new Hint(Kind.GUARD, + "Guard this call with if (d.isUnlocked()): when it returns true, lock(d) == unlocked")); } @Test diff --git a/liquidjava-verifier/src/test/java/liquidjava/diagnostics/errors/RefinementErrorCounterexampleTest.java b/liquidjava-verifier/src/test/java/liquidjava/diagnostics/errors/RefinementErrorCounterexampleTest.java index 46e51d46..ffb487cc 100644 --- a/liquidjava-verifier/src/test/java/liquidjava/diagnostics/errors/RefinementErrorCounterexampleTest.java +++ b/liquidjava-verifier/src/test/java/liquidjava/diagnostics/errors/RefinementErrorCounterexampleTest.java @@ -144,7 +144,7 @@ void stateMessageKeepsAStateReachingExpectedThroughAnAlias() { new Predicate(RefinementsParser.createAST("full(box)", "")), new VCSimplificationResult( vc("∀b1:Object. empty(b1)", "∀x:int. x > 0", "∀box:Object. box == b1", "true")), - new TranslationTable(), null, List.of(), null, null, UnaryOperator.identity()); + new TranslationTable(), null, List.of(), null, null, UnaryOperator.identity(), List.of()); assertEquals("found empty(b1) && box == b1 but expected full(box)", error.getMessage()); }