Point out the argument that decided a state a call does not allow

Each object now remembers the last call that changed its state, through
constructors and state-preserving calls. When a call fails, the verifier
follows that chain back to the last call that changed a state set the
failing call checks. If that call's transition depends on its arguments
or result, and the SMT solver finds values for which the failing call
would have been allowed, the error gets the "Argument picks the state"
category and a hint with those values.

Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>

Author: CatarinaGamboa

liquidjava-example/src/main/java/testSuite/ErrorArgumentCannotPickTheState.java

@@ -0,0 +1,24 @@
+package testSuite;
+
+import liquidjava.specification.StateRefinement;
+import liquidjava.specification.StateSet;
+
+@StateSet({"empty", "filled", "closed"})
+public class ErrorArgumentCannotPickTheState {
+
+    @StateRefinement(to = "empty(this)")
+    public ErrorArgumentCannotPickTheState() {}
+
+    @StateRefinement(from = "!closed(this)", to = "keep ? filled(this) : empty(this)")
+    public void reset(boolean keep) {}
+
+    @StateRefinement(from = "closed(this)")
+    public void reopen() {}
+
+    // no value of keep closes the object, so the argument is not what went wrong
+    public static void use() {
+        ErrorArgumentCannotPickTheState buffer = new ErrorArgumentCannotPickTheState();
+        buffer.reset(true);
+        buffer.reopen(); // Expect: State Refinement Error
+    }
+}

liquidjava-example/src/main/java/testSuite/ErrorArgumentPicksTheState.java

@@ -0,0 +1,23 @@
+package testSuite;
+
+import liquidjava.specification.StateRefinement;
+import liquidjava.specification.StateSet;
+
+@StateSet({"empty", "filled", "closed"})
+public class ErrorArgumentPicksTheState {
+
+    @StateRefinement(to = "empty(this)")
+    public ErrorArgumentPicksTheState() {}
+
+    @StateRefinement(from = "!closed(this)", to = "keep ? filled(this) : empty(this)")
+    public void reset(boolean keep) {}
+
+    @StateRefinement(from = "filled(this)")
+    public void read() {}
+
+    public static void use() {
+        ErrorArgumentPicksTheState buffer = new ErrorArgumentPicksTheState();
+        buffer.reset(false);
+        buffer.read(); // Expect: State Refinement Error
+    }
+}

liquidjava-example/src/main/java/testSuite/ErrorArgumentPicksTheStateEarlier.java

@@ -0,0 +1,29 @@
+package testSuite;
+
+import liquidjava.specification.StateRefinement;
+import liquidjava.specification.StateSet;
+
+@StateSet({"tilingOff", "tilingOn"})
+@StateSet({"uncompressed", "compressed"})
+public class ErrorArgumentPicksTheStateEarlier {
+
+    @StateRefinement(to = "tilingOff(this) && uncompressed(this)")
+    public ErrorArgumentPicksTheStateEarlier() {}
+
+    @StateRefinement(to = "mode == 2 ? tilingOn(this) : tilingOff(this)")
+    public void setTilingMode(int mode) {}
+
+    @StateRefinement(from = "uncompressed(this)", to = "compressed(this)")
+    public void compress() {}
+
+    @StateRefinement(from = "tilingOn(this)")
+    public void setTiling() {}
+
+    // compress() changes another state set, so the tiling mode is what decided the state
+    public static void use() {
+        ErrorArgumentPicksTheStateEarlier param = new ErrorArgumentPicksTheStateEarlier();
+        param.setTilingMode(1);
+        param.compress();
+        param.setTiling(); // Expect: State Refinement Error
+    }
+}

liquidjava-example/src/main/java/testSuite/ErrorConstructorArgumentPicksTheState.java

@@ -0,0 +1,19 @@
+package testSuite;
+
+import liquidjava.specification.StateRefinement;
+import liquidjava.specification.StateSet;
+
+@StateSet({"readOnly", "writable"})
+public class ErrorConstructorArgumentPicksTheState {
+
+    @StateRefinement(to = "write ? writable(this) : readOnly(this)")
+    public ErrorConstructorArgumentPicksTheState(boolean write) {}
+
+    @StateRefinement(from = "writable(this)")
+    public void append() {}
+
+    public static void use() {
+        ErrorConstructorArgumentPicksTheState file = new ErrorConstructorArgumentPicksTheState(false);
+        file.append(); // Expect: State Refinement Error
+    }
+}

liquidjava-verifier/src/main/java/liquidjava/diagnostics/categories/ErrorCategory.java

@@ -8,6 +8,7 @@ public enum ErrorCategory {
 
     OUT_OF_ORDER("A1", "Out of order: the operation is legal for this object, but not right now"),
     OUT_OF_DOMAIN("A2", "Out of domain: the value is outside what is accepted"),
+    ARGUMENT_PICKS_THE_STATE("C3.1", "Argument picks the state: the value passed decides where the object lands"),
     PATH_DEPENDENT_STATE("C4.1", "Path-dependent state: the state differs depending on which branch ran"),
     UNPROVABLE("C4.2", "Unprovable: nothing is known that could prove the requirement");
 

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

@@ -13,6 +13,8 @@ public record Hint(Kind kind, String message) {
     public enum Kind {
         /** A suggestion that does not come from a specific analysis */
         GENERAL,
+        /** An earlier call whose arguments decided the state, and values that would allow the failing call */
+        DECIDING_ARGUMENT,
         /** 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 */

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

@@ -13,10 +13,12 @@
 import liquidjava.diagnostics.hints.Hint.Kind;
 import liquidjava.processor.context.RefinedFunction;
 import liquidjava.processor.context.Variable;
+import liquidjava.processor.state_machine.DecidingArgument;
 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.CtExecutableReference;
 import spoon.reflect.reference.CtTypeReference;
 
 /**
@@ -59,6 +61,18 @@ public static List<Hint> forCall(StateMachine machine, RefinedFunction call, Set
                 .toList();
     }
 
+    /** The earlier call whose arguments decided the receiver's state, and values that would allow the call */
+    public static Hint decidingArgument(DecidingArgument deciding, String receiver) {
+        RefinedFunction function = deciding.call().function();
+        String call = CtExecutableReference.CONSTRUCTOR_NAME.equals(function.getName()) ? constructor(function)
+                : receiver + "." + signature(function);
+        String values = deciding.values().isEmpty() ? "other arguments" : deciding.values().entrySet().stream()
+                .map(e -> e.getKey() + " == " + e.getValue()).collect(Collectors.joining(" and "));
+        return new Hint(Kind.DECIDING_ARGUMENT,
+                String.format("%s on line %d decides the state of %s: with %s, this call would be allowed", call,
+                        deciding.call().position().getLine(), receiver, values));
+    }
+
     /** 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<>();

liquidjava-verifier/src/main/java/liquidjava/processor/context/StateChange.java

@@ -0,0 +1,25 @@
+package liquidjava.processor.context;
+
+import java.util.Optional;
+
+import spoon.reflect.cu.SourcePosition;
+
+/**
+ * The call that put an object in its current state
+ *
+ * @param function
+ *            the method or constructor called
+ * @param change
+ *            the state refinement of {@code function} that applied
+ * @param before
+ *            the object before the call, or {@code null} for a constructor
+ * @param position
+ *            where the call is
+ */
+public record StateChange(RefinedFunction function, ObjectState change, VariableInstance before,
+        SourcePosition position) {
+
+    public Optional<VariableInstance> previous() {
+        return Optional.ofNullable(before);
+    }
+}

liquidjava-verifier/src/main/java/liquidjava/processor/context/VariableInstance.java

@@ -7,6 +7,7 @@
 public class VariableInstance extends RefinedVariable {
 
     private Variable parent;
+    private StateChange stateChange;
 
     public VariableInstance(String name, CtTypeReference<?> type, Predicate c) {
         super(name, type, c);
@@ -33,6 +34,15 @@ public void setParent(Variable p) {
         parent = p;
     }
 
+    /** The last call that changed the state of this object, if it is known */
+    public Optional<StateChange> getStateChange() {
+        return Optional.ofNullable(stateChange);
+    }
+
+    public void setStateChange(StateChange stateChange) {
+        this.stateChange = stateChange;
+    }
+
     public Optional<Variable> getParent() {
         return parent == null ? Optional.empty() : Optional.of(parent);
     }

liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/TypeChecker.java

@@ -414,9 +414,13 @@ public boolean checkStateSMT(Predicate prevState, Predicate expectedState, Sourc
 
     public boolean checkStateSMT(Predicate prevState, Predicate expectedState, SourcePosition p, boolean silent)
             throws LJError {
-        SMTResult result = vcChecker.verifySMTSubtypeStates(prevState, expectedState, context.getGhostStates(), p,
-                factory, silent);
-        return result.isOk();
+        return verifyStateSMT(prevState, expectedState, p, silent).isOk();
+    }
+
+    /** Checks that {@code prevState} implies {@code expectedState}, with a counterexample when it does not */
+    public SMTResult verifyStateSMT(Predicate prevState, Predicate expectedState, SourcePosition p, boolean silent)
+            throws LJError {
+        return vcChecker.verifySMTSubtypeStates(prevState, expectedState, context.getGhostStates(), p, factory, silent);
     }
 
     public void throwRefinementError(SourcePosition position, SourcePosition declarationPosition,