From 0b5259e878fd065041a0bef465bb07e8db1ba3d3 Mon Sep 17 00:00:00 2001 From: Catarina Gamboa Date: Thu, 22 Oct 2026 00:17:25 +0100 Subject: [PATCH 1/3] Explain dead ends in failing state transitions When no sequence of calls leads to a state that allows the failing call, the error says so and suggests the constructors that create the object in such a state, or, if the object can be in several states depending on the path taken, asks for the same state on every path. When no call is allowed in the object's state, the error says it is a final state. These claims are only made when the state machine models every state-changing method of the class and of its super and subclasses. Co-Authored-By: Claude Opus 5.5 --- .../testSuite/ErrorStateHintFinalState.java | 23 ++++++++ .../testSuite/ErrorStateHintIncomplete.java | 27 +++++++++ .../ErrorStateHintPathDependent.java | 27 +++++++++ .../testSuite/ErrorStateHintSubclass.java | 30 ++++++++++ .../liquidjava/diagnostics/hints/Hint.java | 8 ++- .../diagnostics/hints/StateHints.java | 59 +++++++++++++++---- .../processor/state_machine/StateMachine.java | 16 ++++- .../state_machine/StateMachineBuilder.java | 21 ++++++- .../liquidjava/api/tests/TestStateHints.java | 29 ++++++++- 9 files changed, 224 insertions(+), 16 deletions(-) create mode 100644 liquidjava-example/src/main/java/testSuite/ErrorStateHintFinalState.java create mode 100644 liquidjava-example/src/main/java/testSuite/ErrorStateHintIncomplete.java create mode 100644 liquidjava-example/src/main/java/testSuite/ErrorStateHintPathDependent.java create mode 100644 liquidjava-example/src/main/java/testSuite/ErrorStateHintSubclass.java 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 From c1f53c54661936fd451fd950928bd949595c98b1 Mon Sep 17 00:00:00 2001 From: Catarina Gamboa Date: Thu, 22 Oct 2026 00:20:27 +0100 Subject: [PATCH 2/3] List the calls that reach an allowed state when the state is unknown When nothing is known about the receiver's state, the error lists the constructors and the calls, with the states they are made from, that lead to a state allowing the failing call. Co-Authored-By: Claude Opus 5.5 --- .../testSuite/ErrorStateHintUnknownState.java | 24 +++++++++++++++++++ .../liquidjava/diagnostics/hints/Hint.java | 4 +++- .../diagnostics/hints/StateHints.java | 23 +++++++++++++++++- .../processor/state_machine/StateMachine.java | 5 ++++ .../liquidjava/api/tests/TestStateHints.java | 6 +++++ 5 files changed, 60 insertions(+), 2 deletions(-) create mode 100644 liquidjava-example/src/main/java/testSuite/ErrorStateHintUnknownState.java 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( From dc4ef436041831047be25797203afd39bc470e41 Mon Sep 17 00:00:00 2001 From: Catarina Gamboa <52540187+CatarinaGamboa@users.noreply.github.com> Date: Sat, 24 Oct 2026 02:06:39 +0200 Subject: [PATCH 3/3] Build each class's state machine once per checker (#414) MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Stacked on #413. ## Description Building a state machine takes about 25 SMT checks for a small class, and each check creates its own Z3 context. The machine only depends on specifications, which are all registered in the first pass, so `TypeChecker` now builds it on the first state error and reuses it for every later error in the same checker. Finding the receiver's current states still runs at each error. Other options considered: - **Eagerly, after the first pass, for every class with `@StateSet`:** correct programs would pay the SMT cost too. Only worth it once something needs machines without an error, e.g. the fsm diagram. - **Once per run, cached in `Context`:** `Context` would depend on `state_machine`, which depends on `context` (a package cycle). The other way is a static cache that tracks when specifications change. Neither seemed worth it for the extra hits across classes. ## Cost Extra time of `TestExamples` on the 269 cases that exist on `main` (summed per case, one run each; `main` takes 80.3 s): - #413, without the cache: +29.5 s - with this PR: +10.6 s, spread over the 54 files with state errors ## Type of change - [x] Code refactoring ## Checklist - [x] `mvn test` passes locally 🤖 Generated with [Claude Code](https://claude.com/claude-code) Co-authored-by: Claude Opus 5.5 --- .../refinement_checker/TypeChecker.java | 17 +++++++++++++++++ .../object_checkers/AuxStateHandler.java | 7 +++---- 2 files changed, 20 insertions(+), 4 deletions(-) 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