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-verifier/src/main/java/liquidjava/diagnostics/hints/Hint.java b/liquidjava-verifier/src/main/java/liquidjava/diagnostics/hints/Hint.java index a121a518..d3286253 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,13 @@ 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 } 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..dbb5d3cb 100644 --- a/liquidjava-verifier/src/main/java/liquidjava/diagnostics/hints/StateHints.java +++ b/liquidjava-verifier/src/main/java/liquidjava/diagnostics/hints/StateHints.java @@ -44,15 +44,25 @@ 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(); + return Stream.concat(hints.howToReach(current, call, goal).stream(), hints.allowedCalls(current).stream()) + .toList(); } - private List howToReach(Set current, RefinedFunction call) { + 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() && !isUnknown(current) ? 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 +74,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 +117,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/state_machine/StateMachine.java b/liquidjava-verifier/src/main/java/liquidjava/processor/state_machine/StateMachine.java index 47114cf3..a481bce2 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,11 @@ public Optional>> shortestPaths(Set current, R return Optional.of(List.of()); } + /** 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..32dc960a 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