diff --git a/liquidjava-example/src/main/java/testSuite/ErrorStateHintFinalState.java b/liquidjava-example/src/main/java/testSuite/ErrorStateHintFinalState.java new file mode 100644 index 00000000..b7f6b643 --- /dev/null +++ b/liquidjava-example/src/main/java/testSuite/ErrorStateHintFinalState.java @@ -0,0 +1,23 @@ +package testSuite; + +import liquidjava.specification.StateRefinement; +import liquidjava.specification.StateSet; + +@StateSet({"open", "closed"}) +public class ErrorStateHintFinalState { + + @StateRefinement(to = "open(this)") + public ErrorStateHintFinalState() {} + + @StateRefinement(from = "open(this)") + public void read() {} + + @StateRefinement(from = "open(this)", to = "closed(this)") + public void close() {} + + public static void main(String[] args) { + ErrorStateHintFinalState f = new ErrorStateHintFinalState(); + f.close(); + f.read(); // Expect: State Refinement Error + } +} diff --git a/liquidjava-example/src/main/java/testSuite/ErrorStateHintIncomplete.java b/liquidjava-example/src/main/java/testSuite/ErrorStateHintIncomplete.java new file mode 100644 index 00000000..aa0b75c3 --- /dev/null +++ b/liquidjava-example/src/main/java/testSuite/ErrorStateHintIncomplete.java @@ -0,0 +1,27 @@ +package testSuite; + +import liquidjava.specification.StateRefinement; +import liquidjava.specification.StateSet; + +@StateSet({"open", "closed"}) +public class ErrorStateHintIncomplete { + + @StateRefinement(to = "open(this)") + public ErrorStateHintIncomplete() {} + + @StateRefinement(from = "open(this)") + public void read() {} + + @StateRefinement(from = "open(this)", to = "closed(this)") + public void close() {} + + // depends on its argument, so the hints cannot claim that closed is a final state + @StateRefinement(from = "closed(this) && attempts > 0", to = "open(this)") + public void reopen(int attempts) {} + + public static void main(String[] args) { + ErrorStateHintIncomplete f = new ErrorStateHintIncomplete(); + f.close(); + f.read(); // Expect: State Refinement Error + } +} diff --git a/liquidjava-example/src/main/java/testSuite/ErrorStateHintPathDependent.java b/liquidjava-example/src/main/java/testSuite/ErrorStateHintPathDependent.java new file mode 100644 index 00000000..a6bd7470 --- /dev/null +++ b/liquidjava-example/src/main/java/testSuite/ErrorStateHintPathDependent.java @@ -0,0 +1,27 @@ +package testSuite; + +import liquidjava.specification.StateRefinement; +import liquidjava.specification.StateSet; + +@StateSet({"created", "open", "closed"}) +public class ErrorStateHintPathDependent { + + @StateRefinement(to = "created(this)") + public ErrorStateHintPathDependent() {} + + @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 use(boolean ready) { + ErrorStateHintPathDependent f = new ErrorStateHintPathDependent(); + if (ready) + f.open(); + f.read(); // Expect: State Refinement Error + } +} diff --git a/liquidjava-example/src/main/java/testSuite/ErrorStateHintSubclass.java b/liquidjava-example/src/main/java/testSuite/ErrorStateHintSubclass.java new file mode 100644 index 00000000..b8fa2cde --- /dev/null +++ b/liquidjava-example/src/main/java/testSuite/ErrorStateHintSubclass.java @@ -0,0 +1,30 @@ +package testSuite; + +import liquidjava.specification.StateRefinement; +import liquidjava.specification.StateSet; + +@StateSet({"a", "b", "c"}) +public class ErrorStateHintSubclass { + + @StateRefinement(to = "a(this)") + public ErrorStateHintSubclass() {} + + @StateRefinement(from = "a(this)", to = "b(this)") + public void ab() {} + + @StateRefinement(from = "c(this)") + public void useC() {} + + public static void use() { + ErrorStateHintSubclassChild s = new ErrorStateHintSubclassChild(); + s.ab(); + s.useC(); // Expect: State Refinement Error + } +} + +// adds a transition the superclass does not know about, so the hints cannot claim that c is unreachable +class ErrorStateHintSubclassChild extends ErrorStateHintSubclass { + + @StateRefinement(from = "b(this)", to = "c(this)") + public void bc() {} +} diff --git a/liquidjava-example/src/main/java/testSuite/ErrorStateHintUnknownState.java b/liquidjava-example/src/main/java/testSuite/ErrorStateHintUnknownState.java new file mode 100644 index 00000000..dd7b10e5 --- /dev/null +++ b/liquidjava-example/src/main/java/testSuite/ErrorStateHintUnknownState.java @@ -0,0 +1,24 @@ +package testSuite; + +import liquidjava.specification.StateRefinement; +import liquidjava.specification.StateSet; + +@StateSet({"created", "open", "closed"}) +public class ErrorStateHintUnknownState { + + @StateRefinement(to = "created(this)") + public ErrorStateHintUnknownState() {} + + @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 use(ErrorStateHintUnknownState f) { + f.read(); // Expect: State Refinement Error + } +} 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 a121a518..625922ed 100644 --- a/liquidjava-verifier/src/main/java/liquidjava/diagnostics/hints/Hint.java +++ b/liquidjava-verifier/src/main/java/liquidjava/diagnostics/hints/Hint.java @@ -16,7 +16,15 @@ public enum Kind { /** 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 + AVAILABLE_CALLS, + /** No sequence of calls brings the object to a state that allows the failing call */ + UNREACHABLE_STATE, + /** The object's state depends on the path taken, and no sequence of calls works for all of them */ + PATH_DEPENDENT_STATE, + /** The object is in a state where no call with a state refinement is allowed */ + FINAL_STATE, + /** The object's state is unknown, so these are the calls that lead to a state that allows the failing call */ + REACHING_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 index e98c6fd7..a706e39d 100644 --- a/liquidjava-verifier/src/main/java/liquidjava/diagnostics/hints/StateHints.java +++ b/liquidjava-verifier/src/main/java/liquidjava/diagnostics/hints/StateHints.java @@ -1,7 +1,10 @@ package liquidjava.diagnostics.hints; +import java.util.ArrayList; import java.util.Collection; +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; @@ -12,6 +15,7 @@ import liquidjava.processor.context.Variable; import liquidjava.processor.state_machine.State; import liquidjava.processor.state_machine.StateMachine; +import liquidjava.processor.state_machine.Transition; import liquidjava.utils.Utils; import spoon.reflect.reference.CtTypeReference; @@ -44,15 +48,42 @@ private StateHints(StateMachine machine, String receiver) { 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 + Set goal = machine.statesAllowing(call); + if (goal.isEmpty()) + return List.of(); + StateHints hints = new StateHints(machine, receiver); - return Stream.concat(hints.howToReach(current, call).stream(), hints.allowedCalls(current).stream()).toList(); + if (hints.isUnknown(current)) + return hints.reachingCalls(call, goal); + return Stream.concat(hints.howToReach(current, call, goal).stream(), hints.allowedCalls(current).stream()) + .toList(); } - private List howToReach(Set current, RefinedFunction call) { + /** Nothing is known about the receiver's state: list what leads to a state where {@code call} is allowed */ + private List reachingCalls(RefinedFunction call, Set goal) { + Map> sources = new LinkedHashMap<>(); + for (Transition t : machine.transitionsEnabling(call)) + sources.computeIfAbsent(t.method(), m -> new ArrayList<>()).add(t.from()); + Stream constructors = machine.constructorsEnabling(call).stream().map(StateHints::constructor); + Stream calls = sources.entrySet().stream() + .map(e -> call(e.getKey()) + " (from " + names(e.getValue()) + ")"); + List ways = Stream.concat(constructors, calls).toList(); + if (ways.isEmpty()) + return List.of(); + return List.of(new Hint(Kind.REACHING_CALLS, String.format( + "The state of %s is unknown here. To get it to %s, use: %s", receiver, names(goal), list(ways)))); + } + + private List howToReach(Set current, RefinedFunction call, Set goal) { Optional>> search = machine.shortestPaths(current, call, MAX_SEQUENCES); - if (search.isEmpty() || search.get().isEmpty() || search.get().get(0).size() > MAX_SEQUENCE_LENGTH) + if (search.isEmpty()) + return List.of(); + List> sequences = search.get(); + if (sequences.isEmpty()) + return machine.complete() ? List.of(unreachable(current, call, goal)) : List.of(); + if (sequences.get(0).size() > MAX_SEQUENCE_LENGTH) return List.of(); - return search.get().stream().map(sequence -> callSequence(current, sequence)).toList(); + return sequences.stream().map(sequence -> callSequence(current, sequence)).toList(); } private Hint callSequence(Set current, List sequence) { @@ -64,14 +95,39 @@ private Hint callSequence(Set current, List sequence) { receiver, names(current), names(reached))); } + private Hint unreachable(Set current, RefinedFunction call, Set goal) { + if (current.size() > 1) + 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. " + + "Make %s reach this line in the same state on every path", + receiver, names(current), names(goal), receiver)); + String message = String.format("No sequence of calls moves %s from %s to %s", receiver, names(current), + names(goal)); + List constructors = machine.constructorsEnabling(call).stream().map(StateHints::constructor).toList(); + if (!constructors.isEmpty()) + message += ". Create a new object instead with " + String.join(" or ", constructors); + return new Hint(Kind.UNREACHABLE_STATE, message); + } + 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))); + 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", + names(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", + receiver, names(current)))); + return List.of(); + } + + /** Whether nothing is known about the state of the receiver */ + private boolean isUnknown(Set current) { + return current.size() == machine.states().size(); } private String call(RefinedFunction method) { @@ -82,6 +138,10 @@ private static String signature(RefinedFunction method) { return Utils.getSimpleName(method.getName()) + parameters(method); } + private static String constructor(RefinedFunction constructor) { + return "new " + Utils.getSimpleName(constructor.getTargetClass()) + parameters(constructor); + } + private static String parameters(RefinedFunction function) { return function.getArguments().stream().map(Variable::getType).map(CtTypeReference::getSimpleName) .collect(Collectors.joining(", ", "(", ")")); 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 776367d8..f0c51e18 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 @@ -2,6 +2,7 @@ import java.lang.annotation.Annotation; import java.util.Collections; +import java.util.HashMap; import java.util.List; import java.util.Map; import java.util.Optional; @@ -17,6 +18,9 @@ import liquidjava.processor.context.RefinedVariable; import liquidjava.processor.facade.AliasDTO; import liquidjava.processor.facade.GhostDTO; +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.rj_language.parsing.RefinementsParser; import liquidjava.smt.SMTEvaluator; @@ -49,6 +53,7 @@ public abstract class TypeChecker extends CtScanner { protected final Factory factory; protected final VCChecker vcChecker; private final Diagnostics diagnostics = Diagnostics.getInstance(); + private final Map> stateMachines = new HashMap<>(); public TypeChecker(Context context, Factory factory) { this.context = context; @@ -64,6 +69,18 @@ public Factory getFactory() { return factory; } + /** + * The state machine of {@code className}, built once per checker: the specifications it is built from are all known + * before a checker starts + */ + public Optional getStateMachine(String className, CtElement element) throws LJError { + if (!stateMachines.containsKey(className)) { + StateSolver solver = new StateSolver(this, element.getPosition()); + stateMachines.put(className, StateMachineBuilder.build(this, solver, className, element)); + } + return stateMachines.get(className); + } + @Override public void scan(CtElement element) { try { 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 18555583..69eb89ff 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 @@ -659,12 +659,11 @@ private static List stateHints(TypeChecker tc, RefinedFunction function, S 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); + Optional machine = tc.getStateMachine(function.getTargetClass(), invocation); if (machine.isEmpty()) return List.of(); - Set current = solver.possibleStates(machine.get().states(), state, instanceName); + Set current = new StateSolver(tc, invocation.getPosition()).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 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 index 47114cf3..1bfa1926 100644 --- a/liquidjava-verifier/src/main/java/liquidjava/processor/state_machine/StateMachine.java +++ b/liquidjava-verifier/src/main/java/liquidjava/processor/state_machine/StateMachine.java @@ -2,6 +2,7 @@ import java.util.ArrayList; import java.util.Collection; +import java.util.Collections; import java.util.HashSet; import java.util.LinkedHashMap; import java.util.LinkedHashSet; @@ -23,12 +24,14 @@ * the methods whose transitions are all known, in declaration order * @param transitions * the transitions of those methods + * @param constructors + * the states each constructor can create the object in * @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) { + Map> constructors, boolean complete) { /** How many sets of states a search visits before giving up */ private static final int MAX_SEARCHED = 1000; @@ -37,6 +40,7 @@ public record StateMachine(List states, List methods, Li states = List.copyOf(states); methods = List.copyOf(methods); transitions = List.copyOf(transitions); + constructors = Collections.unmodifiableMap(new LinkedHashMap<>(constructors)); } public boolean models(RefinedFunction method) { @@ -60,6 +64,11 @@ public List allowedIn(Set current) { return methods.stream().filter(m -> allows(current, m)).toList(); } + /** The states where {@code method} can be called */ + public Set statesAllowing(RefinedFunction method) { + return ordered(transitions.stream().filter(t -> t.method().equals(method)).map(Transition::from).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()); @@ -98,6 +107,16 @@ public Optional>> shortestPaths(Set current, R return Optional.of(List.of()); } + /** The transitions from a state where {@code call} is not allowed to states where it is */ + public List transitionsEnabling(RefinedFunction call) { + return transitions.stream().filter(t -> !allows(Set.of(t.from()), call) && allows(t.to(), call)).toList(); + } + + /** The constructors that create the object in a state where {@code call} is allowed */ + public List constructorsEnabling(RefinedFunction call) { + return constructors.entrySet().stream().filter(e -> allows(e.getValue(), call)).map(Map.Entry::getKey).toList(); + } + /** {@code subset} in declaration order */ public Set ordered(Collection subset) { return states.stream().filter(subset::contains).collect(Collectors.toCollection(LinkedHashSet::new)); diff --git a/liquidjava-verifier/src/main/java/liquidjava/processor/state_machine/StateMachineBuilder.java b/liquidjava-verifier/src/main/java/liquidjava/processor/state_machine/StateMachineBuilder.java index 087bda81..613ec0e9 100644 --- a/liquidjava-verifier/src/main/java/liquidjava/processor/state_machine/StateMachineBuilder.java +++ b/liquidjava-verifier/src/main/java/liquidjava/processor/state_machine/StateMachineBuilder.java @@ -105,11 +105,16 @@ private static State combine(State state, GhostState ghostState) { private StateMachine build(String className, CtTypeReference type) throws LJError { List methods = new ArrayList<>(); List transitions = new ArrayList<>(); + Map> constructors = new LinkedHashMap<>(); boolean complete = !relatedClassChangesState(className, type); for (RefinedFunction function : tc.getContext().getCtxFunctions()) { - if (!className.equals(function.getTargetClass()) || !function.hasStateChange() - || CtExecutableReference.CONSTRUCTOR_NAME.equals(function.getName())) + if (!className.equals(function.getTargetClass()) || !function.hasStateChange()) continue; + if (CtExecutableReference.CONSTRUCTOR_NAME.equals(function.getName())) { + Optional> created = createdStates(function); + created.ifPresent(s -> constructors.put(function, s)); + continue; + } Optional> calls = transitionsOf(function); if (calls.isPresent()) { methods.add(function); @@ -118,7 +123,7 @@ private StateMachine build(String className, CtTypeReference type) throws LJE complete = false; } } - return new StateMachine(states, methods, transitions, complete); + return new StateMachine(states, methods, transitions, constructors, complete); } /** Whether a superclass or subclass has state refinements of its own, which the machine does not include */ @@ -161,4 +166,14 @@ private Set statesAfter(ObjectState change, State state, Predicate curren Predicate to = change.getTo().substituteVariable(Keys.THIS, AFTER).changeOldMentions(BEFORE, AFTER); return solver.possibleStates(states, Predicate.createConjunction(current, to), AFTER); } + + /** The states {@code constructor} can create the object in, or nothing if they depend on its arguments */ + private Optional> createdStates(RefinedFunction constructor) throws LJError { + List toStates = constructor.getToStates(); + if (!canModel(constructor) || toStates.isEmpty()) + return Optional.empty(); + Predicate to = toStates.get(0).substituteVariable(Keys.THIS, AFTER); + Set created = solver.possibleStates(states, to, AFTER); + return created.isEmpty() ? Optional.empty() : Optional.of(created); + } } 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 58126dc4..0521fbfd 100644 --- a/liquidjava-verifier/src/test/java/liquidjava/api/tests/TestStateHints.java +++ b/liquidjava-verifier/src/test/java/liquidjava/api/tests/TestStateHints.java @@ -40,9 +40,36 @@ void statesOfMultipleStateSetsAreCombined() { new Hint(Kind.AVAILABLE_CALLS, "In state closed and locked, d can call: unlock()")); } + @Test + void finalStateSuggestsCreatingANewObject() { + assertHints("ErrorStateHintFinalState.java", new Hint(Kind.UNREACHABLE_STATE, + "No sequence of calls moves f from closed to open. Create a new object instead with new ErrorStateHintFinalState()"), + new Hint(Kind.FINAL_STATE, + "f is in state closed, where none of its methods with state refinements can be called")); + } + + @Test + void transitionDependingOnArgumentsPreventsClaimingStateIsFinal() { + assertHints("ErrorStateHintIncomplete.java"); + } + + @Test + void subclassTransitionsPreventClaimingStateIsUnreachable() { + assertHints("ErrorStateHintSubclass.java"); + } + + @Test + void stateDependingOnThePathAsksForTheSameStateOnEveryPath() { + assertHints("ErrorStateHintPathDependent.java", new Hint(Kind.PATH_DEPENDENT_STATE, + "f can be in created or open here, depending on the path taken, and no sequence of calls moves all of them to open. " + + "Make f reach this line in the same state on every path")); + } + @Test void callAllowedByDifferentRefinementsInEachStateIsNotSuggested() { - assertHints("ErrorStateHintSeveralRefinements.java"); + assertHints("ErrorStateHintSeveralRefinements.java", new Hint(Kind.PATH_DEPENDENT_STATE, + "f can be in created or open here, depending on the path taken, and no sequence of calls moves all of them to open. " + + "Make f reach this line in the same state on every path")); } @Test @@ -50,6 +77,12 @@ void receiverThatIsNotAVariableGetsNoHints() { assertHints("ErrorStateHintMethodCallReceiver.java"); } + @Test + void unknownStateListsTheCallsThatLeadToTheExpectedState() { + assertHints("ErrorStateHintUnknownState.java", new Hint(Kind.REACHING_CALLS, + "The state of f is unknown here. To get it to open, use: f.open() (from created)")); + } + @Test void classWithoutStateSetKeepsTheGeneralHint() { assertHints("ErrorUnconstrainedStateRefinement.java", Hint.general(