Skip to content

Ask the solver only about the state sets a refinement names #475

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Merged
CatarinaGamboa merged 1 commit into from
Nov 4, 2026
Merged

Ask the solver only about the state sets a refinement names #475

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
1 commit
Select commit
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
31 changes: 31 additions & 0 deletions liquidjava-verifier/src/main/java/liquidjava/diagnostics/hints/StateHints.java
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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;
Expand Down Expand Up @@ -143,7 +144,10 @@ private List<Hint> howToReach(Set<State> current, RefinedFunction call, String f
*/
private List<Hint> guard(Set<State> current, RefinedFunction call) {
List<CallVariant> 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<State> reached = machine.after(current, guard);
Expand All @@ -162,6 +166,33 @@ private List<Hint> guard(Set<State> 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<State> 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<String> checked = machine.states().stream().flatMap(s -> checkedSets.stream().map(s.names()::get))
.collect(Collectors.toSet());
Stream<Predicate> 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<State> current, List<CallVariant> sequence, String from) {
Set<State> reached = current;
for (CallVariant step : sequence)
Expand Down
53 changes: 42 additions & 11 deletions liquidjava-verifier/src/main/java/liquidjava/processor/state_machine/SolverEffects.java
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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;
Expand Down Expand Up @@ -56,8 +58,14 @@ record Scope(TypeChecker tc, StateSolver solver, List<State> states, List<List<S
/** The effects with any arguments, whose entries a condition on the result does not change, or null */
private final CallVariant.Effects any;

private final Map<Integer, Map<State, CallVariant.Entry>> entries = new HashMap<>();
/** By state refinement, then by the states before the call in the state sets its {@code from} names */
private final Map<Integer, Map<List<String>, CallVariant.Entry>> entries = new HashMap<>();
private final Map<Integer, Map<State, Optional<Set<State>>>> 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<Integer, Map<List<String>, Set<List<String>>>> reachedBefore = new HashMap<>();

/**
* @param changes
Expand Down Expand Up @@ -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<String> named = namedSets(from).stream().map(state.names()::get).toList();
return entries.computeIfAbsent(index, i -> new HashMap<>()).computeIfAbsent(named, n -> {
Optional<CallVariant.Entry> 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);
});
Expand All @@ -132,11 +144,23 @@ private Optional<Set<State>> computeAfter(int index, State state, Set<State> 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<State> next = possibleStates(candidates, known, AFTER);
List<Integer> named = namedSets(change.getTo()).stream().sorted().toList();
Set<State> 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<String> before = StateMachine.namedSetsBefore(change.getTo(), scope.stateSets()).stream().sorted()
.map(state.names()::get).toList();
Map<List<String>, Set<List<String>>> 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<State> 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;
});
Expand Down Expand Up @@ -170,6 +194,13 @@ private Set<State> possibleStates(Set<State> 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<Integer> namedSets(Predicate predicate) {
Set<Integer> 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);
Expand Down
60 changes: 60 additions & 0 deletions liquidjava-verifier/src/main/java/liquidjava/processor/state_machine/StateMachine.java
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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}
Expand Down Expand Up @@ -258,6 +264,60 @@ public Set<State> ordered(Collection<State> 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<String> 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<Integer> namedSets(Predicate predicate, List<List<State>> 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<Integer> namedSetsBefore(Predicate predicate, List<List<State>> stateSets) {
return namedSets(predicate, stateSets, true);
}

private static Set<Integer> namedSets(Predicate predicate, List<List<State>> 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<State> keeping(Collection<State> candidates, State before, Set<Integer> 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<String> 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> transition(State from, RefinedFunction method) {
return transitions.stream().filter(t -> t.from().equals(from) && t.method().equals(method)).findFirst();
}
Expand Down
54 changes: 46 additions & 8 deletions ...idjava-verifier/src/main/java/liquidjava/processor/state_machine/StateMachineBuilder.java
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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;
Expand Down Expand Up @@ -509,32 +511,68 @@ private Optional<List<Transition>> transitionsOf(RefinedFunction method) throws
if (!canModel(method))
return Optional.empty();
List<Transition> transitions = new ArrayList<>();
List<List<State>> sets = stateSets();
List<ObjectState> changes = method.getAllStates();
// whether a from holds depends only on the state sets it names: the others are other ghost functions
List<Map<List<String>, CallVariant.Entry>> entries = changes.stream()
.map(c -> new HashMap<List<String>, CallVariant.Entry>()).collect(Collectors.toList());
List<Map<List<String>, Set<List<String>>>> afters = changes.stream()
.map(c -> new HashMap<List<String>, Set<List<String>>>()).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<String> 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<State> next = statesAfter(change, state, current);
Set<State> 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<State> 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<State> statesAfter(ObjectState change, State state, Predicate current, List<List<State>> sets,
Map<List<String>, Set<List<String>>> 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<Integer> named = StateMachine.namedSets(change.getTo(), sets).stream().sorted().toList();
List<State> candidates = StateMachine.keeping(states, state, Set.copyOf(named));
List<String> 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<List<String>> 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 */
Expand Down
40 changes: 40 additions & 0 deletions liquidjava-verifier/src/test/java/liquidjava/processor/state_machine/StateMachineTest.java
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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 {

Expand All @@ -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<List<State>> 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));

Expand Down Expand Up @@ -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<State, Set<State>> after, Set<State> undecided) {
Effects(boolean changesState, Map<State, Set<State>> after) {
Expand Down
Loading