From bc2ad0c2ffea7e8fa9d0beca7d87dfec80115ece Mon Sep 17 00:00:00 2001 From: Catarina Gamboa Date: Wed, 4 Nov 2026 12:04:44 +0000 Subject: [PATCH] Ask the solver only about the state sets a refinement names The verifier keeps the state of every set a refinement's to does not name, and the states of different sets are different ghost functions. So: - whether a from holds is asked once per state of the sets it names; - the states a call can lead to are only those that keep the other sets, and are asked once per state of the sets its to names for old(this); - a guard whose refinements name no state of the sets the failing call checks is not tried when the receiver can be in any combination of states. On the study's UndoManager this takes 1419 queries to 258, with the same hints. Co-Authored-By: Claude Opus 5.5 --- .../diagnostics/hints/StateHints.java | 31 ++++++++++ .../state_machine/SolverEffects.java | 53 ++++++++++++---- .../processor/state_machine/StateMachine.java | 60 +++++++++++++++++++ .../state_machine/StateMachineBuilder.java | 54 ++++++++++++++--- .../state_machine/StateMachineTest.java | 40 +++++++++++++ 5 files changed, 219 insertions(+), 19 deletions(-) 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 67828934..aeb931ae 100644 --- a/liquidjava-verifier/src/main/java/liquidjava/diagnostics/hints/StateHints.java +++ b/liquidjava-verifier/src/main/java/liquidjava/diagnostics/hints/StateHints.java @@ -18,6 +18,7 @@ import liquidjava.processor.state_machine.DecidingArgument; import liquidjava.processor.state_machine.State; import liquidjava.processor.state_machine.StateMachine; +import liquidjava.rj_language.Predicate; import liquidjava.utils.Utils; import liquidjava.utils.constants.Keys; import spoon.reflect.reference.CtExecutableReference; @@ -143,7 +144,10 @@ private List howToReach(Set current, RefinedFunction call, String f */ private List guard(Set current, RefinedFunction call) { List guards = new ArrayList<>(); + boolean anyCombination = anyCombination(current); for (CallVariant guard : machine.guards()) { + if (anyCombination && !namesCheckedState(guard.method())) + continue; if (!machine.allows(current, guard)) continue; Set reached = machine.after(current, guard); @@ -162,6 +166,33 @@ private List guard(Set current, RefinedFunction call) { return List.of(new Hint(Kind.GUARD, message)); } + /** + * Whether the receiver can be in any combination of the states {@code current} has in each state set. Then a call + * that names no state of the sets the failing call checks leaves them as they were, whatever it returns, so the + * failing call stays disallowed after it + */ + private boolean anyCombination(Set current) { + long combinations = 1; + for (int set = 0; set < current.iterator().next().names().size(); set++) { + int index = set; + combinations *= current.stream().map(s -> s.names().get(index)).distinct().count(); + } + return combinations == current.size(); + } + + /** + * Whether a state refinement or the return refinement of {@code method} names a state of a set the failing call + * checks, or an alias + */ + private boolean namesCheckedState(RefinedFunction method) { + Set checked = machine.states().stream().flatMap(s -> checkedSets.stream().map(s.names()::get)) + .collect(Collectors.toSet()); + Stream refinements = Stream.concat( + method.getAllStates().stream().flatMap(o -> Stream.of(o.getFrom(), o.getTo())), + Stream.ofNullable(method.getRefReturn())); + return refinements.anyMatch(p -> StateMachine.mayName(p, checked)); + } + private Hint callSequence(Set current, List sequence, String from) { Set reached = current; for (CallVariant step : sequence) diff --git a/liquidjava-verifier/src/main/java/liquidjava/processor/state_machine/SolverEffects.java b/liquidjava-verifier/src/main/java/liquidjava/processor/state_machine/SolverEffects.java index 26225b97..620e5290 100644 --- a/liquidjava-verifier/src/main/java/liquidjava/processor/state_machine/SolverEffects.java +++ b/liquidjava-verifier/src/main/java/liquidjava/processor/state_machine/SolverEffects.java @@ -2,6 +2,8 @@ import java.util.ArrayList; import java.util.HashMap; +import java.util.HashSet; +import java.util.LinkedHashSet; import java.util.List; import java.util.Map; import java.util.Optional; @@ -56,8 +58,14 @@ record Scope(TypeChecker tc, StateSolver solver, List states, List> entries = new HashMap<>(); + /** By state refinement, then by the states before the call in the state sets its {@code from} names */ + private final Map, CallVariant.Entry>> entries = new HashMap<>(); private final Map>>> afters = new HashMap<>(); + /** + * By state refinement, then by the states before the call in the sets its {@code to} names for {@code old(this)}: + * the states it can lead to in the sets it names + */ + private final Map, Set>>> reachedBefore = new HashMap<>(); /** * @param changes @@ -99,13 +107,17 @@ public CallVariant.Entry entry(int index, State state) { return CallVariant.Entry.HOLDS; // no state refinement: allowed in every state if (onResult && any != null) return any.entry(index, state); // the result is not known before the call - return entries.computeIfAbsent(index, i -> new HashMap<>()).computeIfAbsent(state, s -> { + // the states of the other sets are about other ghost functions, so they cannot change the answer + Predicate from = changes.get(index).getFrom(); + List named = namedSets(from).stream().map(state.names()::get).toList(); + return entries.computeIfAbsent(index, i -> new HashMap<>()).computeIfAbsent(named, n -> { Optional entry = withScope(() -> { - Predicate before = before(s); - Predicate from = changes.get(index).getFrom().substituteVariable(Keys.THIS, BEFORE); - if (scope.solver().implies(before, from)) + Predicate before = before(state); + Predicate fromBefore = from.substituteVariable(Keys.THIS, BEFORE); + if (scope.solver().implies(before, fromBefore)) return CallVariant.Entry.HOLDS; - return scope.solver().compatible(before, from) ? CallVariant.Entry.UNDECIDED : CallVariant.Entry.FAILS; + return scope.solver().compatible(before, fromBefore) ? CallVariant.Entry.UNDECIDED + : CallVariant.Entry.FAILS; }); return entry.orElse(CallVariant.Entry.UNDECIDED); }); @@ -132,11 +144,23 @@ private Optional> computeAfter(int index, State state, Set can ObjectState change = changes.get(index); if (!change.hasTo()) return Set.of(state); - Predicate to = change.getTo().substituteVariable(Keys.THIS, AFTER).changeOldMentions(BEFORE, AFTER); - Predicate known = Predicate.createConjunction(before(state), to); - if (onResult) - known = Predicate.createConjunction(known, condition); - Set next = possibleStates(candidates, known, AFTER); + List named = namedSets(change.getTo()).stream().sorted().toList(); + Set kept = Set.copyOf(StateMachine.keeping(candidates, state, Set.copyOf(named))); + // where it leads in the sets it names depends only on the state before in those it names for old(this) + List before = StateMachine.namedSetsBefore(change.getTo(), scope.stateSets()).stream().sorted() + .map(state.names()::get).toList(); + Map, Set>> reached = reachedBefore.computeIfAbsent(index, i -> new HashMap<>()); + if (!reached.containsKey(before)) { + Predicate to = change.getTo().substituteVariable(Keys.THIS, AFTER).changeOldMentions(BEFORE, AFTER); + Predicate known = Predicate.createConjunction(before(state), to); + if (onResult) + known = Predicate.createConjunction(known, condition); + reached.put(before, possibleStates(kept, known, AFTER).stream() + .map(c -> named.stream().map(c.names()::get).toList()).collect(Collectors.toSet())); + } + Set next = scope.states().stream().filter(kept::contains) + .filter(c -> reached.get(before).contains(named.stream().map(c.names()::get).toList())) + .collect(Collectors.toCollection(LinkedHashSet::new)); // no state at all: the condition contradicts the refinement here, so nothing can be claimed return next.isEmpty() && !onResult ? null : next; }); @@ -170,6 +194,13 @@ private Set possibleStates(Set candidates, Predicate known, String return scope.solver().possibleStates(combined, known, variable); } + /** The state sets that {@code predicate} or this variant's condition may name a state of */ + private Set namedSets(Predicate predicate) { + Set named = new HashSet<>(StateMachine.namedSets(predicate, scope.stateSets())); + named.addAll(StateMachine.namedSets(condition, scope.stateSets())); + return named; + } + /** What is known before the call in {@code state} */ private Predicate before(State state) { Predicate before = state.predicate().substituteVariable(Keys.THIS, BEFORE); 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 4fa637c7..db045cfc 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 @@ -12,10 +12,16 @@ import java.util.Optional; import java.util.Set; import java.util.stream.Collectors; +import java.util.stream.IntStream; import liquidjava.processor.context.ObjectState; import liquidjava.processor.context.RefinedFunction; import liquidjava.rj_language.Predicate; +import liquidjava.rj_language.ast.AliasInvocation; +import liquidjava.rj_language.ast.Expression; +import liquidjava.rj_language.ast.FunctionInvocation; +import liquidjava.utils.Utils; +import liquidjava.utils.constants.Keys; /** * The typestate of a class as a finite state machine, built by {@link StateMachineBuilder} @@ -258,6 +264,60 @@ public Set ordered(Collection subset) { return states.stream().filter(subset::contains).collect(Collectors.toCollection(LinkedHashSet::new)); } + /** + * Whether {@code predicate} names one of {@code states}, by its simple name, or calls an alias, which may name one + * that cannot be seen without expanding it + */ + public static boolean mayName(Predicate predicate, Set states) { + return mayName(predicate.getExpression(), states, false); + } + + /** + * The state sets, as indexes into {@link State#names()}, that {@code predicate} {@link #mayName may name} a state + * of + * + * @param stateSets + * the states of each state set on its own, in the order the sets are declared + */ + static Set namedSets(Predicate predicate, List> stateSets) { + return namedSets(predicate, stateSets, false); + } + + /** Like {@link #namedSets}, but only the sets it may name a state of for {@code old(this)} */ + static Set namedSetsBefore(Predicate predicate, List> stateSets) { + return namedSets(predicate, stateSets, true); + } + + private static Set namedSets(Predicate predicate, List> stateSets, boolean onOld) { + return IntStream.range(0, stateSets.size()) + .filter(k -> mayName(predicate.getExpression(), + stateSets.get(k).stream().map(s -> s.names().get(0)).collect(Collectors.toSet()), onOld)) + .boxed().collect(Collectors.toSet()); + } + + /** + * The {@code candidates} in the same state as {@code before} in every state set but those in {@code changed}: the + * verifier keeps the state of a set that a state refinement's {@code to} does not name + */ + static List keeping(Collection candidates, State before, Set changed) { + return candidates.stream().filter(c -> IntStream.range(0, before.names().size()) + .allMatch(k -> changed.contains(k) || c.names().get(k).equals(before.names().get(k)))).toList(); + } + + private static boolean mayName(Expression expression, Set states, boolean onOld) { + if (expression instanceof AliasInvocation) + return true; + if (expression instanceof FunctionInvocation f && states.contains(Utils.getSimpleName(f.getName())) + && (!onOld || invokesOld(f))) + return true; + return expression.getChildren().stream().anyMatch(e -> mayName(e, states, onOld)); + } + + private static boolean invokesOld(Expression expression) { + return expression instanceof FunctionInvocation f && Keys.OLD.equals(f.getName()) + || expression.getChildren().stream().anyMatch(StateMachine::invokesOld); + } + private Optional transition(State from, RefinedFunction method) { return transitions.stream().filter(t -> t.from().equals(from) && t.method().equals(method)).findFirst(); } 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 e77cc5bf..92ba7c3b 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 @@ -3,8 +3,10 @@ import java.util.ArrayDeque; import java.util.ArrayList; import java.util.Deque; +import java.util.HashMap; import java.util.HashSet; import java.util.LinkedHashMap; +import java.util.LinkedHashSet; import java.util.List; import java.util.Map; import java.util.Objects; @@ -509,32 +511,68 @@ private Optional> transitionsOf(RefinedFunction method) throws if (!canModel(method)) return Optional.empty(); List transitions = new ArrayList<>(); + List> sets = stateSets(); + List changes = method.getAllStates(); + // whether a from holds depends only on the state sets it names: the others are other ghost functions + List, CallVariant.Entry>> entries = changes.stream() + .map(c -> new HashMap, CallVariant.Entry>()).collect(Collectors.toList()); + List, Set>>> afters = changes.stream() + .map(c -> new HashMap, Set>>()).collect(Collectors.toList()); for (State state : states) { Predicate current = state.predicate().substituteVariable(Keys.THIS, BEFORE); - for (ObjectState change : method.getAllStates()) { + for (int i = 0; i < changes.size(); i++) { + ObjectState change = changes.get(i); if (!change.hasFrom()) continue; - Predicate from = change.getFrom().substituteVariable(Keys.THIS, BEFORE); - if (solver.implies(current, from)) { + List named = StateMachine.namedSets(change.getFrom(), sets).stream().map(state.names()::get) + .toList(); + CallVariant.Entry entry = entries.get(i).get(named); + if (entry == null) { + entry = entry(current, change.getFrom().substituteVariable(Keys.THIS, BEFORE)); + entries.get(i).put(named, entry); + } + if (entry == CallVariant.Entry.HOLDS) { // like the verifier, the first state change whose precondition holds is the one applied - Set next = statesAfter(change, state, current); + Set next = statesAfter(change, state, current, sets, afters.get(i)); if (next.isEmpty()) return Optional.empty(); transitions.add(new Transition(state, method, change, next)); break; } - if (solver.compatible(current, from)) + if (entry == CallVariant.Entry.UNDECIDED) return Optional.empty(); // allowed only sometimes in this state } } return Optional.of(transitions); } - private Set statesAfter(ObjectState change, State state, Predicate current) throws LJError { + private CallVariant.Entry entry(Predicate current, Predicate from) throws LJError { + if (solver.implies(current, from)) + return CallVariant.Entry.HOLDS; + return solver.compatible(current, from) ? CallVariant.Entry.UNDECIDED : CallVariant.Entry.FAILS; + } + + /** + * The states {@code change} can lead to from {@code state}. The verifier keeps the state of the sets its {@code to} + * does not name, and the states it can lead to in the others depend only on the state before in the sets it names + * for {@code old(this)}, so they are asked once for each and kept in {@code known} + */ + private Set statesAfter(ObjectState change, State state, Predicate current, List> sets, + Map, Set>> known) 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); + List named = StateMachine.namedSets(change.getTo(), sets).stream().sorted().toList(); + List candidates = StateMachine.keeping(states, state, Set.copyOf(named)); + List before = StateMachine.namedSetsBefore(change.getTo(), sets).stream().sorted() + .map(state.names()::get).toList(); + if (!known.containsKey(before)) { + Predicate to = change.getTo().substituteVariable(Keys.THIS, AFTER).changeOldMentions(BEFORE, AFTER); + known.put(before, solver.possibleStates(candidates, Predicate.createConjunction(current, to), AFTER) + .stream().map(s -> named.stream().map(s.names()::get).toList()).collect(Collectors.toSet())); + } + Set> after = known.get(before); + return candidates.stream().filter(c -> after.contains(named.stream().map(c.names()::get).toList())) + .collect(Collectors.toCollection(LinkedHashSet::new)); } /** The states {@code constructor} can create the object in, or nothing if they depend on its arguments */ diff --git a/liquidjava-verifier/src/test/java/liquidjava/processor/state_machine/StateMachineTest.java b/liquidjava-verifier/src/test/java/liquidjava/processor/state_machine/StateMachineTest.java index 3d2d25e1..7c5ebf7e 100644 --- a/liquidjava-verifier/src/test/java/liquidjava/processor/state_machine/StateMachineTest.java +++ b/liquidjava-verifier/src/test/java/liquidjava/processor/state_machine/StateMachineTest.java @@ -15,6 +15,8 @@ import liquidjava.processor.context.RefinedFunction; import liquidjava.rj_language.Predicate; +import liquidjava.rj_language.ast.AliasInvocation; +import liquidjava.utils.constants.Keys; class StateMachineTest { @@ -23,6 +25,9 @@ class StateMachineTest { private static final State OPEN_UNLOCKED = state("open", "unlocked"); private static final State CLOSED_LOCKED = state("closed", "locked"); private static final State CLOSED_UNLOCKED = state("closed", "unlocked"); + private static final List> SETS = List.of(List.of(state("open"), state("closed")), + List.of(state("locked"), state("unlocked"))); + private static final Predicate THIS = Predicate.createVar(Keys.THIS); private static final StateMachine MACHINE = machine( List.of(OPEN_LOCKED, OPEN_UNLOCKED, CLOSED_LOCKED, CLOSED_UNLOCKED)); @@ -139,6 +144,41 @@ void callWhoseStatesAfterAreUnknownIsNotAllowed() { assertFalse(machine(ABC, call).allows(Set.of(A), call)); } + @Test + void setsNamedAreThoseWithAStateInThePredicate() { + Predicate openAndPositive = Predicate.createConjunction(inState("open", THIS), + Predicate.createInvocation("size", THIS)); + assertEquals(Set.of(0), StateMachine.namedSets(openAndPositive, SETS)); + assertEquals(Set.of(), StateMachine.namedSets(new Predicate(), SETS)); + } + + @Test + void aliasMayNameEverySet() { + Predicate alias = new Predicate(new AliasInvocation("Ready", List.of(THIS.getExpression()))); + assertEquals(Set.of(0, 1), StateMachine.namedSets(alias, SETS)); + assertEquals(Set.of(0, 1), StateMachine.namedSetsBefore(alias, SETS)); + } + + @Test + void setsNamedBeforeAreThoseNamedForOld() { + // locked(this) && open(old(this)) + Predicate to = Predicate.createConjunction(inState("locked", THIS), + inState("open", Predicate.createInvocation(Keys.OLD, THIS))); + assertEquals(Set.of(0, 1), StateMachine.namedSets(to, SETS)); + assertEquals(Set.of(0), StateMachine.namedSetsBefore(to, SETS)); + } + + @Test + void candidatesKeepTheStateOfSetsNotChanged() { + assertEquals(List.of(OPEN_LOCKED, OPEN_UNLOCKED), + StateMachine.keeping(MACHINE.states(), OPEN_LOCKED, Set.of(1))); + assertEquals(List.of(OPEN_LOCKED), StateMachine.keeping(MACHINE.states(), OPEN_LOCKED, Set.of())); + } + + private static Predicate inState(String state, Predicate object) { + return Predicate.createInvocation(state, object); + } + /** Effects given by hand: the states where each refinement's from holds, and the states after the call from each */ private record Effects(boolean changesState, Map> after, Set undecided) { Effects(boolean changesState, Map> after) {