From fb438f1f537e7bf6d7105c2b342df259eedb521b Mon Sep 17 00:00:00 2001 From: Catarina Gamboa Date: Thu, 22 Oct 2026 00:13:17 +0100 Subject: [PATCH] Suggest the calls that make a failing state transition verify When a call is made in a state that does not allow it, the verifier builds the class's state machine from its state sets and state refinements, proving each transition with the SMT solver, and searches it for the shortest sequences of calls that lead to a state allowing the call. The error then suggests those calls and lists the calls allowed in the current state. Only transitions that depend on nothing but the state of the object are modeled, and a call is suggested only when a single state refinement allows it in every state the object can be in, as in the verifier, so every suggestion makes the failing call verify. Co-Authored-By: Claude Opus 5.5 --- .../testSuite/ErrorStateHintCallSequence.java | 25 +++ .../ErrorStateHintMethodCallReceiver.java | 22 +++ .../testSuite/ErrorStateHintMultipleSets.java | 30 ++++ .../ErrorStateHintSeveralRefinements.java | 29 ++++ .../testSuite/ErrorStateHintTwoCalls.java | 25 +++ .../errors/StateRefinementError.java | 7 +- .../liquidjava/diagnostics/hints/Hint.java | 6 +- .../diagnostics/hints/StateHints.java | 99 +++++++++++ .../refinement_checker/TypeChecker.java | 8 +- .../refinement_checker/VCChecker.java | 5 +- .../object_checkers/AuxStateHandler.java | 49 +++++- .../processor/state_machine/State.java | 14 ++ .../processor/state_machine/StateMachine.java | 115 ++++++++++++ .../state_machine/StateMachineBuilder.java | 164 ++++++++++++++++++ .../processor/state_machine/StateSolver.java | 48 +++++ .../processor/state_machine/Transition.java | 22 +++ .../liquidjava/api/tests/TestStateHints.java | 66 +++++++ 17 files changed, 727 insertions(+), 7 deletions(-) create mode 100644 liquidjava-example/src/main/java/testSuite/ErrorStateHintCallSequence.java create mode 100644 liquidjava-example/src/main/java/testSuite/ErrorStateHintMethodCallReceiver.java create mode 100644 liquidjava-example/src/main/java/testSuite/ErrorStateHintMultipleSets.java create mode 100644 liquidjava-example/src/main/java/testSuite/ErrorStateHintSeveralRefinements.java create mode 100644 liquidjava-example/src/main/java/testSuite/ErrorStateHintTwoCalls.java create mode 100644 liquidjava-verifier/src/main/java/liquidjava/diagnostics/hints/StateHints.java create mode 100644 liquidjava-verifier/src/main/java/liquidjava/processor/state_machine/State.java create mode 100644 liquidjava-verifier/src/main/java/liquidjava/processor/state_machine/StateMachine.java create mode 100644 liquidjava-verifier/src/main/java/liquidjava/processor/state_machine/StateMachineBuilder.java create mode 100644 liquidjava-verifier/src/main/java/liquidjava/processor/state_machine/StateSolver.java create mode 100644 liquidjava-verifier/src/main/java/liquidjava/processor/state_machine/Transition.java create mode 100644 liquidjava-verifier/src/test/java/liquidjava/api/tests/TestStateHints.java diff --git a/liquidjava-example/src/main/java/testSuite/ErrorStateHintCallSequence.java b/liquidjava-example/src/main/java/testSuite/ErrorStateHintCallSequence.java new file mode 100644 index 00000000..e765a070 --- /dev/null +++ b/liquidjava-example/src/main/java/testSuite/ErrorStateHintCallSequence.java @@ -0,0 +1,25 @@ +package testSuite; + +import liquidjava.specification.StateRefinement; +import liquidjava.specification.StateSet; + +@StateSet({"created", "open", "closed"}) +public class ErrorStateHintCallSequence { + + @StateRefinement(to = "created(this)") + public ErrorStateHintCallSequence() {} + + @StateRefinement(from = "created(this)", to = "open(this)") + public void open() {} + + @StateRefinement(from = "open(this)") + public void read() {} + + @StateRefinement(from = "open(this)", to = "closed(this)") + public void close() {} + + public static void main(String[] args) { + ErrorStateHintCallSequence f = new ErrorStateHintCallSequence(); + f.read(); // Expect: State Refinement Error + } +} diff --git a/liquidjava-example/src/main/java/testSuite/ErrorStateHintMethodCallReceiver.java b/liquidjava-example/src/main/java/testSuite/ErrorStateHintMethodCallReceiver.java new file mode 100644 index 00000000..67cf999e --- /dev/null +++ b/liquidjava-example/src/main/java/testSuite/ErrorStateHintMethodCallReceiver.java @@ -0,0 +1,22 @@ +package testSuite; + +import liquidjava.specification.StateRefinement; +import liquidjava.specification.StateSet; + +@StateSet({"created", "open"}) +public class ErrorStateHintMethodCallReceiver { + + @StateRefinement(to = "created(this)") + public ErrorStateHintMethodCallReceiver() {} + + @StateRefinement(from = "created(this)", to = "open(this)") + public void open() {} + + @StateRefinement(from = "open(this)") + public void read() {} + + // a call added before the line would act on a different object than the one returned here + public static void use() { + new ErrorStateHintMethodCallReceiver().read(); // Expect: State Refinement Error + } +} diff --git a/liquidjava-example/src/main/java/testSuite/ErrorStateHintMultipleSets.java b/liquidjava-example/src/main/java/testSuite/ErrorStateHintMultipleSets.java new file mode 100644 index 00000000..f3bc2ce1 --- /dev/null +++ b/liquidjava-example/src/main/java/testSuite/ErrorStateHintMultipleSets.java @@ -0,0 +1,30 @@ +package testSuite; + +import liquidjava.specification.StateRefinement; +import liquidjava.specification.StateSet; + +@StateSet({"closed", "opened"}) +@StateSet({"unlocked", "locked"}) +public class ErrorStateHintMultipleSets { + + @StateRefinement(to = "closed(this) && unlocked(this)") + public ErrorStateHintMultipleSets() {} + + @StateRefinement(from = "closed(this) && unlocked(this)", to = "opened(this)") + public void open() {} + + @StateRefinement(from = "opened(this)", to = "closed(this)") + public void close() {} + + @StateRefinement(from = "closed(this) && unlocked(this)", to = "locked(this)") + public void lock() {} + + @StateRefinement(from = "locked(this)", to = "unlocked(this)") + public void unlock() {} + + public static void main(String[] args) { + ErrorStateHintMultipleSets d = new ErrorStateHintMultipleSets(); + d.lock(); + d.open(); // Expect: State Refinement Error + } +} diff --git a/liquidjava-example/src/main/java/testSuite/ErrorStateHintSeveralRefinements.java b/liquidjava-example/src/main/java/testSuite/ErrorStateHintSeveralRefinements.java new file mode 100644 index 00000000..ce853437 --- /dev/null +++ b/liquidjava-example/src/main/java/testSuite/ErrorStateHintSeveralRefinements.java @@ -0,0 +1,29 @@ +package testSuite; + +import liquidjava.specification.StateRefinement; +import liquidjava.specification.StateSet; + +@StateSet({"created", "open", "closed"}) +public class ErrorStateHintSeveralRefinements { + + @StateRefinement(to = "created(this)") + public ErrorStateHintSeveralRefinements() {} + + @StateRefinement(from = "created(this)", to = "open(this)") + public void open() {} + + // allowed in created and in open, but by different refinements, so not when the object can be in either + @StateRefinement(from = "created(this)", to = "open(this)") + @StateRefinement(from = "open(this)", to = "open(this)") + public void ensureOpen() {} + + @StateRefinement(from = "open(this)") + public void read() {} + + public static void use(boolean ready) { + ErrorStateHintSeveralRefinements f = new ErrorStateHintSeveralRefinements(); + if (ready) + f.open(); + f.read(); // Expect: State Refinement Error + } +} diff --git a/liquidjava-example/src/main/java/testSuite/ErrorStateHintTwoCalls.java b/liquidjava-example/src/main/java/testSuite/ErrorStateHintTwoCalls.java new file mode 100644 index 00000000..b02e7376 --- /dev/null +++ b/liquidjava-example/src/main/java/testSuite/ErrorStateHintTwoCalls.java @@ -0,0 +1,25 @@ +package testSuite; + +import liquidjava.specification.StateRefinement; +import liquidjava.specification.StateSet; + +@StateSet({"idle", "ready", "running"}) +public class ErrorStateHintTwoCalls { + + @StateRefinement(to = "idle(this)") + public ErrorStateHintTwoCalls() {} + + @StateRefinement(from = "idle(this)", to = "ready(this)") + public void prepare() {} + + @StateRefinement(from = "ready(this)", to = "running(this)") + public void start() {} + + @StateRefinement(from = "running(this)") + public void step() {} + + public static void main(String[] args) { + ErrorStateHintTwoCalls r = new ErrorStateHintTwoCalls(); + r.step(); // Expect: State Refinement Error + } +} 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 fdadc6aa..d034618b 100644 --- a/liquidjava-verifier/src/main/java/liquidjava/diagnostics/errors/StateRefinementError.java +++ b/liquidjava-verifier/src/main/java/liquidjava/diagnostics/errors/StateRefinementError.java @@ -2,6 +2,8 @@ import static liquidjava.rj_language.opt.VCSimplificationUtils.isTrue; +import java.util.List; + import liquidjava.diagnostics.TranslationTable; import liquidjava.diagnostics.hints.Hint; import liquidjava.processor.VCImplication; @@ -21,7 +23,7 @@ public class StateRefinementError extends LJError { private final SourcePosition declarationPosition; public StateRefinementError(SourcePosition position, SourcePosition declarationPosition, Predicate expected, - VCSimplificationResult found, TranslationTable translationTable, String customMessage) { + VCSimplificationResult found, TranslationTable translationTable, String customMessage, List hints) { super("State Refinement Error", String.format("found %s but expected %s", found.getImplication().toPredicate().getExpression().toDisplayString(), @@ -30,7 +32,8 @@ public StateRefinementError(SourcePosition position, SourcePosition declarationP this.declarationPosition = declarationPosition; this.expected = expected; this.found = found; - if (isTrue(found.getImplication().toPredicate().getExpression())) + hints.forEach(this::addHint); + 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.")); } diff --git a/liquidjava-verifier/src/main/java/liquidjava/diagnostics/hints/Hint.java b/liquidjava-verifier/src/main/java/liquidjava/diagnostics/hints/Hint.java index 2d2ad3a2..a121a518 100644 --- a/liquidjava-verifier/src/main/java/liquidjava/diagnostics/hints/Hint.java +++ b/liquidjava-verifier/src/main/java/liquidjava/diagnostics/hints/Hint.java @@ -12,7 +12,11 @@ public record Hint(Kind kind, String message) { public enum Kind { /** A suggestion that does not come from a specific analysis */ - GENERAL + GENERAL, + /** Calls to add before the failing call so the object reaches a state that allows it */ + CALL_SEQUENCE, + /** The calls allowed in the object's current state */ + AVAILABLE_CALLS } public static Hint general(String message) { diff --git a/liquidjava-verifier/src/main/java/liquidjava/diagnostics/hints/StateHints.java b/liquidjava-verifier/src/main/java/liquidjava/diagnostics/hints/StateHints.java new file mode 100644 index 00000000..e98c6fd7 --- /dev/null +++ b/liquidjava-verifier/src/main/java/liquidjava/diagnostics/hints/StateHints.java @@ -0,0 +1,99 @@ +package liquidjava.diagnostics.hints; + +import java.util.Collection; +import java.util.List; +import java.util.Optional; +import java.util.Set; +import java.util.stream.Collectors; +import java.util.stream.Stream; + +import liquidjava.diagnostics.hints.Hint.Kind; +import liquidjava.processor.context.RefinedFunction; +import liquidjava.processor.context.Variable; +import liquidjava.processor.state_machine.State; +import liquidjava.processor.state_machine.StateMachine; +import liquidjava.utils.Utils; +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. + */ +public final class StateHints { + + private static final int MAX_SEQUENCE_LENGTH = 3; + private static final int MAX_SEQUENCES = 3; + private static final int MAX_LISTED_CALLS = 5; + + private final StateMachine machine; + private final String receiver; + + private StateHints(StateMachine machine, String receiver) { + this.machine = machine; + this.receiver = receiver; + } + + /** + * @param call + * the method that cannot be called + * @param current + * the states the receiver can be in before the call + * @param receiver + * the receiver as written in the code + */ + public static List forCall(StateMachine machine, RefinedFunction call, Set current, String receiver) { + 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); + return Stream.concat(hints.howToReach(current, call).stream(), hints.allowedCalls(current).stream()).toList(); + } + + private List howToReach(Set current, RefinedFunction call) { + Optional>> search = machine.shortestPaths(current, call, MAX_SEQUENCES); + if (search.isEmpty() || search.get().isEmpty() || search.get().get(0).size() > MAX_SEQUENCE_LENGTH) + return List.of(); + return search.get().stream().map(sequence -> callSequence(current, sequence)).toList(); + } + + private Hint callSequence(Set current, List sequence) { + Set reached = current; + for (RefinedFunction method : sequence) + reached = machine.after(reached, method); + String calls = sequence.stream().map(this::call).collect(Collectors.joining(", then ")); + return new Hint(Kind.CALL_SEQUENCE, String.format("Call %s before this call to move %s from %s to %s", calls, + receiver, names(current), names(reached))); + } + + private List allowedCalls(Set current) { + List allowed = machine.allowedIn(current); + if (allowed.isEmpty()) + return List.of(); + 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", names(current), receiver, list(signatures), others))); + } + + private String call(RefinedFunction method) { + return receiver + "." + signature(method); + } + + private static String signature(RefinedFunction method) { + return Utils.getSimpleName(method.getName()) + parameters(method); + } + + private static String parameters(RefinedFunction function) { + return function.getArguments().stream().map(Variable::getType).map(CtTypeReference::getSimpleName) + .collect(Collectors.joining(", ", "(", ")")); + } + + private static String names(Collection states) { + return states.stream().map(State::name).collect(Collectors.joining(" or ")); + } + + private static String list(List items) { + if (items.size() <= MAX_LISTED_CALLS) + return String.join(", ", items); + return String.join(", ", items.subList(0, MAX_LISTED_CALLS)) + ", ..."; + } +} 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 ea73e64b..776367d8 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 @@ -8,6 +8,7 @@ import liquidjava.diagnostics.Diagnostics; import liquidjava.diagnostics.errors.*; +import liquidjava.diagnostics.hints.Hint; import liquidjava.diagnostics.warnings.UnsatisfiableRefinementWarning; import liquidjava.processor.context.AliasWrapper; import liquidjava.processor.context.Context; @@ -407,7 +408,12 @@ public void throwRefinementError(SourcePosition position, SourcePosition declara public void throwStateRefinementError(SourcePosition position, SourcePosition declarationPosition, Predicate found, Predicate expected, String customMessage) throws LJError { - vcChecker.throwStateRefinementError(position, declarationPosition, found, expected, customMessage); + throwStateRefinementError(position, declarationPosition, found, expected, customMessage, List.of()); + } + + public void throwStateRefinementError(SourcePosition position, SourcePosition declarationPosition, Predicate found, + Predicate expected, String customMessage, List hints) throws LJError { + vcChecker.throwStateRefinementError(position, declarationPosition, found, expected, customMessage, hints); } 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 ddca3506..cc5aebe8 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 @@ -12,6 +12,7 @@ import liquidjava.diagnostics.errors.*; import liquidjava.diagnostics.DebugLog; import liquidjava.diagnostics.TranslationTable; +import liquidjava.diagnostics.hints.Hint; import liquidjava.processor.VCImplication; import liquidjava.processor.context.*; import liquidjava.rj_language.Predicate; @@ -436,11 +437,11 @@ protected void throwRefinementError(SourcePosition position, SourcePosition decl } protected void throwStateRefinementError(SourcePosition position, SourcePosition declarationPosition, - Predicate found, Predicate expected, String customMessage) throws StateRefinementError { + Predicate found, Predicate expected, String customMessage, List hints) throws StateRefinementError { TranslationTable map = new TranslationTable(); VCImplication foundState = buildPremiseChain(map, expected, found); throw new StateRefinementError(position, declarationPosition, expected, foundState.simplify(), map, - customMessage); + customMessage, hints); } 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 9ae78045..18555583 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 @@ -4,13 +4,20 @@ import java.util.*; import java.util.stream.Collectors; +import liquidjava.diagnostics.DebugLog; import liquidjava.diagnostics.errors.IllegalConstructorTransitionError; import liquidjava.diagnostics.errors.InvalidRefinementError; import liquidjava.diagnostics.errors.LJError; import liquidjava.diagnostics.errors.SMTUnknownError; +import liquidjava.diagnostics.hints.Hint; +import liquidjava.diagnostics.hints.StateHints; import liquidjava.processor.context.*; import liquidjava.processor.refinement_checker.TypeChecker; import liquidjava.processor.refinement_checker.TypeCheckingUtils; +import liquidjava.processor.state_machine.State; +import liquidjava.processor.state_machine.StateMachine; +import liquidjava.processor.state_machine.StateMachineBuilder; +import liquidjava.processor.state_machine.StateSolver; import liquidjava.rj_language.Predicate; import liquidjava.utils.Utils; import liquidjava.utils.constants.Formats; @@ -636,11 +643,51 @@ private static void changeState(TypeChecker tc, VariableInstance vi, RefinedFunc SourcePosition declarationPosition = stateChanges.stream().filter(ObjectState::hasFrom) .map(ObjectState::getFromPosition).filter(Objects::nonNull).findFirst() .orElse(function.getPlacementInCode().getPosition()); + List hints = stateHints(tc, function, instanceName, prevState, invocation); tc.throwStateRefinementError(invocation.getPosition(), declarationPosition, prevState, - expectedStatesDisjunction, message); + expectedStatesDisjunction, message, hints); } } + /** + * Hints on how to fix a call to {@code function} made in a state that does not allow it. They are best effort: if + * they cannot be computed, the error is reported without them + */ + private static List stateHints(TypeChecker tc, RefinedFunction function, String instanceName, Predicate state, + CtElement invocation) { + Optional receiver = receiverOf(invocation); + if (receiver.isEmpty() || !StateMachineBuilder.canModel(function)) + return List.of(); + try { + StateSolver solver = new StateSolver(tc, invocation.getPosition()); + Optional machine = StateMachineBuilder.build(tc, solver, function.getTargetClass(), + invocation); + if (machine.isEmpty()) + return List.of(); + Set current = solver.possibleStates(machine.get().states(), state, instanceName); + return StateHints.forCall(machine.get(), function, current, receiver.get()); + } catch (RuntimeException e) { + // a failure to compute hints must not replace the error being reported + DebugLog.warn("Could not compute state hints: " + e.getMessage()); + return List.of(); + } + } + + /** + * The receiver of {@code invocation} as written in the code, if it names an object that calls can be added to: a + * variable, a field or {@code this} + */ + 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()); + return Optional.empty(); + } + 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 new file mode 100644 index 00000000..d99a36bd --- /dev/null +++ b/liquidjava-verifier/src/main/java/liquidjava/processor/state_machine/State.java @@ -0,0 +1,14 @@ +package liquidjava.processor.state_machine; + +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 predicate + * the predicate that holds for {@code this} in this state + */ +public record State(String name, Predicate predicate) { +} diff --git a/liquidjava-verifier/src/main/java/liquidjava/processor/state_machine/StateMachine.java b/liquidjava-verifier/src/main/java/liquidjava/processor/state_machine/StateMachine.java new file mode 100644 index 00000000..47114cf3 --- /dev/null +++ b/liquidjava-verifier/src/main/java/liquidjava/processor/state_machine/StateMachine.java @@ -0,0 +1,115 @@ +package liquidjava.processor.state_machine; + +import java.util.ArrayList; +import java.util.Collection; +import java.util.HashSet; +import java.util.LinkedHashMap; +import java.util.LinkedHashSet; +import java.util.List; +import java.util.Map; +import java.util.Optional; +import java.util.Set; +import java.util.stream.Collectors; + +import liquidjava.processor.context.ObjectState; +import liquidjava.processor.context.RefinedFunction; + +/** + * The typestate of a class as a finite state machine, built by {@link StateMachineBuilder} + * + * @param states + * all states of the class, in declaration order + * @param methods + * the methods whose transitions are all known, in declaration order + * @param transitions + * the transitions of those methods + * @param complete + * whether every method that can change the state of the object is in {@code methods}; only then can the + * machine tell that a state cannot be reached or that no call is allowed + */ +public record StateMachine(List states, List methods, List transitions, + boolean complete) { + + /** How many sets of states a search visits before giving up */ + private static final int MAX_SEARCHED = 1000; + + public StateMachine { + states = List.copyOf(states); + methods = List.copyOf(methods); + transitions = List.copyOf(transitions); + } + + public boolean models(RefinedFunction method) { + return methods.contains(method); + } + + /** + * Whether {@code method} can be called when the object can be in any of {@code current}. Like in the verifier, a + * method that changes the state needs a single one of its state refinements to allow all of them. + */ + public boolean allows(Set current, RefinedFunction method) { + List calls = current.stream().map(s -> transition(s, method)).flatMap(Optional::stream).toList(); + if (calls.size() != current.size()) + return false; + boolean preservesState = method.getAllStates().stream().noneMatch(ObjectState::hasTo); + return preservesState || calls.stream().map(Transition::change).distinct().count() <= 1; + } + + /** The methods that can be called when the object can be in any of {@code current} */ + public List allowedIn(Set current) { + return methods.stream().filter(m -> allows(current, m)).toList(); + } + + /** The states the object can be in after calling {@code method}, which must be allowed in all of {@code current} */ + public Set after(Set current, RefinedFunction method) { + return ordered(current.stream().flatMap(s -> transition(s, method).orElseThrow().to().stream()).toList()); + } + + /** + * The shortest sequences of calls that take an object in any of {@code current} to where {@code call} is allowed + * + * @return at most {@code limit} sequences, all of the same length; none if there is no such sequence; nothing if + * the search gave up + */ + public Optional>> shortestPaths(Set current, RefinedFunction call, int limit) { + Map, List>> level = Map.of(current, List.of(List.of())); + Set> visited = new HashSet<>(level.keySet()); + while (!level.isEmpty()) { + Map, List>> next = new LinkedHashMap<>(); + level.forEach((states, paths) -> { + for (RefinedFunction method : allowedIn(states)) { + Set reached = after(states, method); + if (visited.contains(reached)) + continue; + List> reachedPaths = next.computeIfAbsent(reached, k -> new ArrayList<>()); + paths.stream().limit(limit - reachedPaths.size()).map(path -> append(path, method)) + .forEach(reachedPaths::add); + } + }); + List> found = next.entrySet().stream().filter(e -> allows(e.getKey(), call)) + .flatMap(e -> e.getValue().stream()).limit(limit).toList(); + if (!found.isEmpty()) + return Optional.of(found); + visited.addAll(next.keySet()); + if (visited.size() > MAX_SEARCHED) + return Optional.empty(); + level = next; + } + return Optional.of(List.of()); + } + + /** {@code subset} in declaration order */ + public Set ordered(Collection subset) { + return states.stream().filter(subset::contains).collect(Collectors.toCollection(LinkedHashSet::new)); + } + + private Optional transition(State from, RefinedFunction method) { + return transitions.stream().filter(t -> t.from().equals(from) && t.method().equals(method)).findFirst(); + } + + private static List append(List path, RefinedFunction method) { + List extended = new ArrayList<>(path); + extended.add(method); + return extended; + } +} 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 new file mode 100644 index 00000000..087bda81 --- /dev/null +++ b/liquidjava-verifier/src/main/java/liquidjava/processor/state_machine/StateMachineBuilder.java @@ -0,0 +1,164 @@ +package liquidjava.processor.state_machine; + +import java.util.ArrayList; +import java.util.LinkedHashMap; +import java.util.List; +import java.util.Map; +import java.util.Optional; +import java.util.Set; +import java.util.stream.Collectors; +import java.util.stream.Stream; + +import liquidjava.diagnostics.errors.LJError; +import liquidjava.processor.context.Context; +import liquidjava.processor.context.GhostFunction; +import liquidjava.processor.context.GhostState; +import liquidjava.processor.context.ObjectState; +import liquidjava.processor.context.RefinedFunction; +import liquidjava.processor.refinement_checker.TypeChecker; +import liquidjava.rj_language.Predicate; +import liquidjava.utils.Utils; +import liquidjava.utils.constants.Keys; +import spoon.reflect.declaration.CtElement; +import spoon.reflect.reference.CtExecutableReference; +import spoon.reflect.reference.CtTypeReference; + +/** + * Builds the {@link StateMachine} of a class from its {@code @StateSet}s and {@code @StateRefinement}s. Every + * transition is proven by the SMT solver, so the machine never contains a call that would not verify. Methods whose + * state refinements mention anything besides the states of {@code this} (parameters, return values, other ghosts) are + * left out, and the machine is then marked incomplete, as it is when a superclass or subclass has state refinements of + * its own. + */ +public class StateMachineBuilder { + + /** Classes with more states than this get no machine, as building it would take too many solver calls */ + private static final int MAX_STATES = 16; + + // two objects of the class, before and after a call, that the rest of the program knows nothing about + private static final String BEFORE = "#state_before"; + private static final String AFTER = "#state_after"; + + private final TypeChecker tc; + private final StateSolver solver; + private final List states; + + private StateMachineBuilder(TypeChecker tc, StateSolver solver, List states) { + this.tc = tc; + this.solver = solver; + this.states = states; + } + + /** Whether the transitions of {@code function} can be part of a machine: they only depend on the state of this */ + public static boolean canModel(RefinedFunction function) { + return function.getAllStates().stream().flatMap(change -> Stream.of(change.getFrom(), change.getTo())) + .flatMap(p -> p.getVariableNames().stream()).allMatch(Keys.THIS::equals); + } + + /** + * Builds the state machine of {@code className} + * + * @param element + * the element being verified, where the fresh objects are declared + * + * @return the machine, or nothing if the class has no state sets or too many states + */ + public static Optional build(TypeChecker tc, StateSolver solver, String className, CtElement element) + throws LJError { + List states = statesOf(tc.getContext(), className); + if (states.isEmpty() || states.size() > MAX_STATES) + return Optional.empty(); + Context context = tc.getContext(); + context.enterContext(); + try { + CtTypeReference type = tc.getFactory().Type().createReference(className); + context.addVarToContext(BEFORE, type, new Predicate(), element); + context.addVarToContext(AFTER, type, new Predicate(), element); + return Optional.of(new StateMachineBuilder(tc, solver, states).build(className, type)); + } finally { + context.exitContext(); + } + } + + /** Every combination of one state from each state set of the class */ + private static List statesOf(Context context, String className) { + List ghostStates = context.getGhostState(Utils.getSimpleName(className)); + if (ghostStates == null) + return List.of(); + Map> stateSets = ghostStates.stream().filter(g -> g.getParent() != null) + .collect(Collectors.groupingBy(GhostState::getParent, LinkedHashMap::new, Collectors.toList())); + if (stateSets.isEmpty()) + return List.of(); + + List combinations = List.of(new State("", 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(); + Predicate holds = Predicate.createInvocation(ghostState.getQualifiedName(), Predicate.createVar(Keys.THIS)); + return new State(name, Predicate.createConjunction(state.predicate(), holds)); + } + + private StateMachine build(String className, CtTypeReference type) throws LJError { + List methods = new ArrayList<>(); + List transitions = new ArrayList<>(); + boolean complete = !relatedClassChangesState(className, type); + for (RefinedFunction function : tc.getContext().getCtxFunctions()) { + if (!className.equals(function.getTargetClass()) || !function.hasStateChange() + || CtExecutableReference.CONSTRUCTOR_NAME.equals(function.getName())) + continue; + Optional> calls = transitionsOf(function); + if (calls.isPresent()) { + methods.add(function); + transitions.addAll(calls.get()); + } else { + complete = false; + } + } + return new StateMachine(states, methods, transitions, complete); + } + + /** Whether a superclass or subclass has state refinements of its own, which the machine does not include */ + private boolean relatedClassChangesState(String className, CtTypeReference type) { + return tc.getContext().getCtxFunctions().stream().filter(RefinedFunction::hasStateChange) + .map(RefinedFunction::getTargetClass).filter(c -> c != null && !c.equals(className)).distinct() + .map(c -> tc.getFactory().Type().createReference(c)) + .anyMatch(other -> other.isSubtypeOf(type) || type.isSubtypeOf(other)); + } + + /** The transitions of {@code method}, or nothing if they depend on more than the state of {@code this} */ + private Optional> transitionsOf(RefinedFunction method) throws LJError { + if (!canModel(method)) + return Optional.empty(); + List transitions = new ArrayList<>(); + for (State state : states) { + Predicate current = state.predicate().substituteVariable(Keys.THIS, BEFORE); + for (ObjectState change : method.getAllStates()) { + if (!change.hasFrom()) + continue; + Predicate from = change.getFrom().substituteVariable(Keys.THIS, BEFORE); + if (solver.implies(current, from)) { + // like the verifier, the first state change whose precondition holds is the one applied + Set next = statesAfter(change, state, current); + if (next.isEmpty()) + return Optional.empty(); + transitions.add(new Transition(state, method, change, next)); + break; + } + if (solver.compatible(current, from)) + return Optional.empty(); // allowed only sometimes in this state + } + } + return Optional.of(transitions); + } + + private Set statesAfter(ObjectState change, State state, Predicate current) throws LJError { + if (!change.hasTo()) + return Set.of(state); + Predicate to = change.getTo().substituteVariable(Keys.THIS, AFTER).changeOldMentions(BEFORE, AFTER); + return solver.possibleStates(states, Predicate.createConjunction(current, to), AFTER); + } +} diff --git a/liquidjava-verifier/src/main/java/liquidjava/processor/state_machine/StateSolver.java b/liquidjava-verifier/src/main/java/liquidjava/processor/state_machine/StateSolver.java new file mode 100644 index 00000000..0281058a --- /dev/null +++ b/liquidjava-verifier/src/main/java/liquidjava/processor/state_machine/StateSolver.java @@ -0,0 +1,48 @@ +package liquidjava.processor.state_machine; + +import java.util.LinkedHashSet; +import java.util.List; +import java.util.Set; + +import liquidjava.diagnostics.errors.LJError; +import liquidjava.processor.refinement_checker.TypeChecker; +import liquidjava.rj_language.Predicate; +import liquidjava.utils.constants.Keys; +import spoon.reflect.cu.SourcePosition; + +/** + * Asks the SMT solver about states, in the current verification context + */ +public class StateSolver { + + private final TypeChecker tc; + private final SourcePosition position; + + /** + * @param position + * where the questions come from, reported if the solver fails + */ + public StateSolver(TypeChecker tc, SourcePosition position) { + this.tc = tc; + this.position = position; + } + + /** Whether {@code conclusion} holds whenever {@code premise} holds */ + public boolean implies(Predicate premise, Predicate conclusion) throws LJError { + return tc.checkStateSMT(premise, conclusion, position, true); + } + + /** Whether {@code first} and {@code second} can hold at the same time */ + public boolean compatible(Predicate first, Predicate second) throws LJError { + return !implies(first, second.negate()); + } + + /** The {@code states} that {@code variable} can be in when {@code known} holds, in the order given */ + public Set possibleStates(List states, Predicate known, String variable) throws LJError { + Set possible = new LinkedHashSet<>(); + for (State state : states) + if (compatible(known, state.predicate().substituteVariable(Keys.THIS, variable))) + possible.add(state); + return possible; + } +} diff --git a/liquidjava-verifier/src/main/java/liquidjava/processor/state_machine/Transition.java b/liquidjava-verifier/src/main/java/liquidjava/processor/state_machine/Transition.java new file mode 100644 index 00000000..9725984d --- /dev/null +++ b/liquidjava-verifier/src/main/java/liquidjava/processor/state_machine/Transition.java @@ -0,0 +1,22 @@ +package liquidjava.processor.state_machine; + +import java.util.Set; + +import liquidjava.processor.context.ObjectState; +import liquidjava.processor.context.RefinedFunction; + +/** + * A call that is allowed in state {@code from} and leaves the object in one of the states {@code to} + * + * @param from + * the state the call is made in + * @param method + * the method called + * @param change + * the state refinement of {@code method} that applies in {@code from} + * @param to + * the states the object can be in after the call (more than one when the state after the call is not + * determined by the state before it) + */ +public record Transition(State from, RefinedFunction method, ObjectState change, Set to) { +} diff --git a/liquidjava-verifier/src/test/java/liquidjava/api/tests/TestStateHints.java b/liquidjava-verifier/src/test/java/liquidjava/api/tests/TestStateHints.java new file mode 100644 index 00000000..58126dc4 --- /dev/null +++ b/liquidjava-verifier/src/test/java/liquidjava/api/tests/TestStateHints.java @@ -0,0 +1,66 @@ +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.StateRefinementError; +import liquidjava.diagnostics.hints.Hint; +import liquidjava.diagnostics.hints.Hint.Kind; + +class TestStateHints { + + private static final String TEST_SUITE = "../liquidjava-example/src/main/java/testSuite/"; + + @Test + void missingCallIsSuggestedWithTheCallsAllowedNow() { + assertHints("ErrorStateHintCallSequence.java", + new Hint(Kind.CALL_SEQUENCE, "Call f.open() before this call to move f from created to open"), + new Hint(Kind.AVAILABLE_CALLS, "In state created, f can call: open()")); + } + + @Test + void missingCallsAreSuggestedInOrder() { + assertHints("ErrorStateHintTwoCalls.java", + new Hint(Kind.CALL_SEQUENCE, + "Call r.prepare(), then r.start() before this call to move r from idle to running"), + new Hint(Kind.AVAILABLE_CALLS, "In state idle, r can call: prepare()")); + } + + @Test + void statesOfMultipleStateSetsAreCombined() { + assertHints("ErrorStateHintMultipleSets.java", + new Hint(Kind.CALL_SEQUENCE, + "Call d.unlock() before this call to move d from closed and locked to closed and unlocked"), + new Hint(Kind.AVAILABLE_CALLS, "In state closed and locked, d can call: unlock()")); + } + + @Test + void callAllowedByDifferentRefinementsInEachStateIsNotSuggested() { + assertHints("ErrorStateHintSeveralRefinements.java"); + } + + @Test + void receiverThatIsNotAVariableGetsNoHints() { + assertHints("ErrorStateHintMethodCallReceiver.java"); + } + + @Test + void classWithoutStateSetKeepsTheGeneralHint() { + assertHints("ErrorUnconstrainedStateRefinement.java", Hint.general( + "No state information is known for this object. Make sure its state is initialized and available at this point.")); + } + + private static void assertHints(String test, Hint... expected) { + CommandLineLauncher.launch(TEST_SUITE + test); + List errors = Diagnostics.getInstance().getErrors().stream().toList(); + assertEquals(1, errors.size(), "Expected exactly one error from " + test); + StateRefinementError error = assertInstanceOf(StateRefinementError.class, errors.get(0)); + assertEquals(List.of(expected), error.getHints()); + } +}