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