Land the rest of the state hints stack (#412, #413, #414)

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
+    }
+}

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
+    }
+}

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
+    }
+}

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() {}
+}

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
+    }
+}

liquidjava-verifier/src/main/java/liquidjava/diagnostics/hints/Hint.java

@@ -16,7 +16,15 @@ 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,
+        /** 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) {

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;
 
@@ -44,15 +48,42 @@ private StateHints(StateMachine machine, String receiver) {
     public static List<Hint> forCall(StateMachine machine, RefinedFunction call, Set<State> 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<State> 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();
+        if (hints.isUnknown(current))
+            return hints.reachingCalls(call, goal);
+        return Stream.concat(hints.howToReach(current, call, goal).stream(), hints.allowedCalls(current).stream())
+                .toList();
     }
 
-    private List<Hint> howToReach(Set<State> current, RefinedFunction call) {
+    /** Nothing is known about the receiver's state: list what leads to a state where {@code call} is allowed */
+    private List<Hint> reachingCalls(RefinedFunction call, Set<State> goal) {
+        Map<RefinedFunction, List<State>> sources = new LinkedHashMap<>();
+        for (Transition t : machine.transitionsEnabling(call))
+            sources.computeIfAbsent(t.method(), m -> new ArrayList<>()).add(t.from());
+        Stream<String> constructors = machine.constructorsEnabling(call).stream().map(StateHints::constructor);
+        Stream<String> calls = sources.entrySet().stream()
+                .map(e -> call(e.getKey()) + " (from " + names(e.getValue()) + ")");
+        List<String> 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<Hint> howToReach(Set<State> current, RefinedFunction call, Set<State> goal) {
         Optional<List<List<RefinedFunction>>> 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<List<RefinedFunction>> sequences = search.get();
+        if (sequences.isEmpty())
+            return machine.complete() ? 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<State> current, List<RefinedFunction> sequence) {
@@ -64,14 +95,39 @@ private Hint callSequence(Set<State> current, List<RefinedFunction> sequence) {
                 receiver, names(current), names(reached)));
     }
 
+    private Hint unreachable(Set<State> current, RefinedFunction call, Set<State> 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<String> 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<Hint> allowedCalls(Set<State> current) {
         List<RefinedFunction> allowed = machine.allowedIn(current);
-        if (allowed.isEmpty())
-            return List.of();
-        List<String> 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<String> 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<State> current) {
+        return current.size() == machine.states().size();
     }
 
     private String call(RefinedFunction method) {
@@ -82,6 +138,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(", ", "(", ")"));

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<String, Optional<StateMachine>> 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<StateMachine> 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 {

liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/object_checkers/AuxStateHandler.java

@@ -659,12 +659,11 @@ private static List<Hint> stateHints(TypeChecker tc, RefinedFunction function, S
         if (receiver.isEmpty() || !StateMachineBuilder.canModel(function))
             return List.of();
         try {
-            StateSolver solver = new StateSolver(tc, invocation.getPosition());
-            Optional<StateMachine> machine = StateMachineBuilder.build(tc, solver, function.getTargetClass(),
-                    invocation);
+            Optional<StateMachine> machine = tc.getStateMachine(function.getTargetClass(), invocation);
             if (machine.isEmpty())
                 return List.of();
-            Set<State> current = solver.possibleStates(machine.get().states(), state, instanceName);
+            Set<State> 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

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<State> states, List<RefinedFunction> methods, List<Transition> transitions,
-        boolean complete) {
+        Map<RefinedFunction, Set<State>> 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<State> states, List<RefinedFunction> 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<RefinedFunction> allowedIn(Set<State> current) {
         return methods.stream().filter(m -> allows(current, m)).toList();
     }
 
+    /** The states where {@code method} can be called */
+    public Set<State> 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<State> after(Set<State> current, RefinedFunction method) {
         return ordered(current.stream().flatMap(s -> transition(s, method).orElseThrow().to().stream()).toList());
@@ -98,6 +107,16 @@ public Optional<List<List<RefinedFunction>>> shortestPaths(Set<State> 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<Transition> 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<RefinedFunction> 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<State> ordered(Collection<State> subset) {
         return states.stream().filter(subset::contains).collect(Collectors.toCollection(LinkedHashSet::new));