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 d3286253..625922ed 100644 --- a/liquidjava-verifier/src/main/java/liquidjava/diagnostics/hints/Hint.java +++ b/liquidjava-verifier/src/main/java/liquidjava/diagnostics/hints/Hint.java @@ -22,7 +22,9 @@ public enum Kind { /** 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 + 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 dbb5d3cb..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; @@ -49,17 +53,34 @@ public static List forCall(StateMachine machine, RefinedFunction call, Set return List.of(); StateHints hints = new StateHints(machine, receiver); + if (hints.isUnknown(current)) + return hints.reachingCalls(call, goal); return Stream.concat(hints.howToReach(current, call, goal).stream(), hints.allowedCalls(current).stream()) .toList(); } + /** 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()) return List.of(); List> sequences = search.get(); if (sequences.isEmpty()) - return machine.complete() && !isUnknown(current) ? List.of(unreachable(current, call, goal)) : List.of(); + return machine.complete() ? List.of(unreachable(current, call, goal)) : List.of(); if (sequences.get(0).size() > MAX_SEQUENCE_LENGTH) return List.of(); return sequences.stream().map(sequence -> callSequence(current, sequence)).toList(); 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 a481bce2..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 @@ -107,6 +107,11 @@ 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(); 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 32dc960a..0521fbfd 100644 --- a/liquidjava-verifier/src/test/java/liquidjava/api/tests/TestStateHints.java +++ b/liquidjava-verifier/src/test/java/liquidjava/api/tests/TestStateHints.java @@ -77,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(