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) {