Origin note: say where the wrong state of a receiver comes from

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

@@ -0,0 +1,30 @@
+package testSuite;
+
+import liquidjava.specification.Refinement;
+import liquidjava.specification.StateRefinement;
+import liquidjava.specification.StateSet;
+
+// The state of an object assigned the value of a call comes from the call's return refinement
+@StateSet(name = "phase", value = {"idle", "running"})
+class FromReturnedTask {
+    @StateRefinement(to = "idle(this)")
+    FromReturnedTask() {}
+
+    @StateRefinement(from = "idle(this)", to = "running(this)")
+    void start() {}
+
+    @StateRefinement(from = "running(this)")
+    void await() {}
+
+    @Refinement("idle(_)")
+    static FromReturnedTask create() {
+        return new FromReturnedTask();
+    }
+}
+
+public class ErrorStateFromReturnedValue {
+    static void use() {
+        FromReturnedTask task = FromReturnedTask.create();
+        task.await(); // Expect: State Refinement Error
+    }
+}

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

@@ -0,0 +1,18 @@
+package liquidjava.processor.context;
+
+import liquidjava.rj_language.Predicate;
+import spoon.reflect.cu.SourcePosition;
+
+/**
+ * The value a call to a refined method returned
+ *
+ * @param function
+ *            the method called
+ * @param returned
+ *            the method's return refinement at this call, with its arguments and receiver substituted and {@code _} for
+ *            the value
+ * @param position
+ *            where the call is
+ */
+public record CallResult(RefinedFunction function, Predicate returned, SourcePosition position) {
+}

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

@@ -8,6 +8,7 @@ public class VariableInstance extends RefinedVariable {
 
     private Variable parent;
     private StateChange stateChange;
+    private CallResult returnedBy;
 
     public VariableInstance(String name, CtTypeReference<?> type, Predicate c) {
         super(name, type, c);
@@ -43,6 +44,15 @@ public void setStateChange(StateChange stateChange) {
         this.stateChange = stateChange;
     }
 
+    /** The call whose value this instance was assigned, if it was assigned one and its state has not changed since */
+    public Optional<CallResult> getReturnedBy() {
+        return Optional.ofNullable(returnedBy);
+    }
+
+    public void setReturnedBy(CallResult returnedBy) {
+        this.returnedBy = returnedBy;
+    }
+
     public Optional<Variable> getParent() {
         return parent == null ? Optional.empty() : Optional.of(parent);
     }

liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/FromNotes.java → liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/OriginNotes.java

@@ -18,12 +18,12 @@
 import liquidjava.utils.Utils;
 
 /**
- * The notes of a refinement error that say where the values its expected refinement is about come from. Each is given
- * only when it restates what the verifier used, and is left out otherwise
+ * The origin notes of a refinement error, which say where the values its expected refinement is about come from. Each
+ * is given only when it restates what the verifier used, and is left out otherwise
  */
-final class FromNotes {
+final class OriginNotes {
 
-    private FromNotes() {
+    private OriginNotes() {
     }
 
     /**
@@ -46,9 +46,9 @@ static List<String> unrefinedParameters(RefinementError error, CtElement checked
                     || !(context.getVariableByName(variable)instanceof Variable declared)
                     || !declared.getMainRefinement().isBooleanTrue() || isRefined(parameter.get(), context))
                 return List.of();
-            notes.add(String.format("From: %s is a parameter of %s (line %d) with no refinement",
-                    error.getDisplayNames().get(variable), signature(method.get()),
-                    parameter.get().getPosition().getLine()));
+            notes.add(String.format("Origin: line %d, %s is a parameter of %s with no refinement",
+                    parameter.get().getPosition().getLine(), error.getDisplayNames().get(variable),
+                    signature(method.get())));
         }
         return notes;
     }

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

@@ -99,7 +99,7 @@ public class RefinementTypeChecker extends TypeChecker {
     ContextHistory contextHistory = ContextHistory.getInstance();
     // the metadata that checking an element puts on it
     private static final List<String> CHECK_METADATA = List.of(Keys.REFINEMENT, Keys.TARGET, Keys.RECEIVER,
-            Keys.RETURN_VAR_NAME, Keys.STATE_CHANGE);
+            Keys.RETURN_VAR_NAME, Keys.STATE_CHANGE, Keys.CALL_RESULT);
     // the loops being checked, innermost first
     private final Deque<LoopTypestates> loops = new ArrayDeque<>();
 
@@ -195,9 +195,16 @@ public <T> void visitCtLocalVariable(CtLocalVariable<T> localVariable) {
             context.addVarToContext(varName, localVariable.getType(), new Predicate(), e);
             checkVariableRefinements(refinementFound, varName, localVariable.getType(), localVariable, localVariable);
             AuxStateHandler.addStateRefinements(this, varName, e);
+            recordReturnedValue(varName, e);
         }
     }
 
+    /** Records on the new instance of a local variable the call whose value it was assigned, if any */
+    private void recordReturnedValue(String name, CtExpression<?> value) {
+        if (value != null && value.getMetadata(Keys.CALL_RESULT)instanceof CallResult result)
+            context.getLastVariableInstance(name).ifPresent(instance -> instance.setReturnedBy(result));
+    }
+
     @Override
     public <T> void visitCtCatchVariable(CtCatchVariable<T> catchVariable) {
         super.visitCtCatchVariable(catchVariable);
@@ -271,6 +278,8 @@ private <T, A extends T> void visitAssignment(CtAssignment<T, A> assignment) thr
             CtVariable<T> varDecl = (CtVariable<T>) var.getDeclaration();
             String name = var.getSimpleName();
             checkAssignment(name, varDecl.getType(), ex, assignment.getAssignment(), assignment, varDecl);
+            if (varDecl instanceof CtLocalVariable<?> && !(assignment instanceof CtOperatorAssignment<?, ?>))
+                recordReturnedValue(name, assignment.getAssignment());
 
         } else if (ex instanceof CtFieldWrite<?> fw) {
             CtFieldReference<?> cr = fw.getVariable();

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

@@ -614,14 +614,14 @@ public void throwRefinementError(SourcePosition position, SourcePosition declara
     public void throwStateRefinementError(SourcePosition position, SourcePosition declarationPosition, Predicate found,
             Predicate expected, String customMessage) throws LJError {
         throwStateRefinementError(position, List.of(declarationPosition), found, expected, customMessage, List.of(),
-                null, null, List.of());
+                null, null, List.of(), List.of());
     }
 
     public void throwStateRefinementError(SourcePosition position, List<SourcePosition> declarationPositions,
             Predicate found, Predicate expected, String customMessage, List<Hint> hints, ErrorCategory category,
-            StateErrorContext context, List<String> declarationNotes) throws LJError {
+            StateErrorContext context, List<String> declarationNotes, List<String> messageNotes) throws LJError {
         vcChecker.throwStateRefinementError(position, declarationPositions, found, expected, customMessage, hints,
-                category, context, declarationNotes);
+                category, context, declarationNotes, messageNotes);
     }
 
     public void throwStateConflictError(SourcePosition position, Predicate expectedType) throws LJError {

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

@@ -90,7 +90,7 @@ public void processSubtyping(Predicate expectedType, List<GhostState> list, CtEl
             RefinementError error = new RefinementError(element.getPosition(), declarationPosition, expectedType,
                     implBeforeChange.simplify(NeededVariables.forRefinementError(expectedType)), map,
                     result.getCounterexample(), customMessage, context.getAliases());
-            FromNotes.unrefinedParameters(error, element, context).forEach(error::addMessageNote);
+            OriginNotes.unrefinedParameters(error, element, context).forEach(error::addMessageNote);
             throw error;
         }
     }
@@ -459,16 +459,19 @@ protected Predicate shownFound(Predicate found, Predicate expected) {
 
     protected void throwStateRefinementError(SourcePosition position, List<SourcePosition> declarationPositions,
             Predicate found, Predicate expected, String customMessage, List<Hint> hints, ErrorCategory category,
-            StateErrorContext context, List<String> declarationNotes) throws StateRefinementError {
+            StateErrorContext context, List<String> declarationNotes, List<String> messageNotes)
+            throws StateRefinementError {
         TranslationTable map = new TranslationTable();
         VCImplication foundState = buildPremiseChain(map, expected, found);
         VCSimplificationResult simplified = foundState.simplify(NeededVariables.forStateError(expected));
         VCSimplificationResult shown = VCSimplification.simplifyOnce(simplified,
                 new VCRelevantFacts(expected.getExpression(), this::ghostFunctionsOf));
-        throw new StateRefinementError(position, declarationPositions, expected, shown, map, customMessage, hints,
-                category, context,
+        StateRefinementError error = new StateRefinementError(position, declarationPositions, expected, shown, map,
+                customMessage, hints, category, context,
                 e -> StateValues.toSetForm(e, this.context.getGhostStates(), this.context.getGhosts()),
                 declarationNotes);
+        messageNotes.forEach(error::addMessageNote);
+        throw error;
     }
 
     /** The ghost functions an invocation name stands for: a state's state set function, or the ghost itself */

liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/general_checkers/MethodsFunctionsChecker.java

@@ -7,6 +7,7 @@
 import java.util.Optional;
 
 import liquidjava.diagnostics.errors.LJError;
+import liquidjava.processor.context.CallResult;
 import liquidjava.processor.context.Refined;
 import liquidjava.processor.context.RefinedFunction;
 import liquidjava.processor.context.RefinedVariable;
@@ -358,6 +359,7 @@ private Map<String, String> checkInvocationRefinements(CtExpression<?> invocatio
                     ? Predicate.createEquals(Predicate.createVar(Keys.WILDCARD), Predicate.createVar(returnViName))
                     : new Predicate();
             invocation.putMetadata(Keys.REFINEMENT, returnRef);
+            recordCallResult(invocation, f, new Predicate());
             return map;
         }
 
@@ -371,6 +373,12 @@ private Map<String, String> checkInvocationRefinements(CtExpression<?> invocatio
         return map;
     }
 
+    /** Records on a call written in the source what it returns, for the variable it is assigned to */
+    private static void recordCallResult(CtExpression<?> invocation, RefinedFunction f, Predicate returned) {
+        if (invocation instanceof CtInvocation<?> && invocation.getPosition().isValidPosition())
+            invocation.putMetadata(Keys.CALL_RESULT, new CallResult(f, returned, invocation.getPosition()));
+    }
+
     /**
      * Computes a stable return-value instance name so {@code _}/{@code return} in a {@code @StateRefinement to=} clause
      * matches the post-call VariableInstance. Returns {@code null} for void methods. When the function has no
@@ -412,6 +420,7 @@ private void applyReturnRefinement(CtExpression<?> invocation, RefinedFunction f
                 varName = v.getName();
         }
 
+        recordCallResult(invocation, f, methodRef);
         String viName = returnViName != null ? returnViName
                 : GeneratedNames.valueOf(invocation, rtc.getContext().getCounter());
         VariableInstance vi = (VariableInstance) rtc.getContext().addInstanceToContext(viName, f.getType(),

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

@@ -827,8 +827,25 @@ private static void changeState(TypeChecker tc, VariableInstance vi, RefinedFunc
             StateErrorContext context = states
                     .map(r -> StateErrorContext.of(r.machine(), function, r.current(), writtenReceiver(invocation)))
                     .orElse(null);
+            List<String> messageNotes = receiverOf(invocation)
+                    .flatMap(r -> fromNote(tc, vi, r, function, ghostStates, states, prevState, expected, invocation))
+                    .stream().toList();
             tc.throwStateRefinementError(invocation.getPosition(), declarationPositions, prevState,
-                    expectedStatesDisjunction, message, hints, category, context, declarationNotes);
+                    expectedStatesDisjunction, message, hints, category, context, declarationNotes, messageNotes);
+        }
+    }
+
+    /** Best effort, like {@link #receiverStates}: see {@link StateOrigin} */
+    private static Optional<String> fromNote(TypeChecker tc, VariableInstance receiver, String written,
+            RefinedFunction function, List<GhostState> ghostStates, Optional<ReceiverStates> states, Predicate found,
+            Predicate expected, CtElement invocation) {
+        try {
+            return StateOrigin.note(tc, receiver, written, function, ghostStates, states.map(ReceiverStates::machine),
+                    states.map(ReceiverStates::current).orElse(Set.of()), found, expected, invocation);
+        } catch (RuntimeException e) {
+            // also an LJError, such as an unknown solver result: the note is left out, the error is still reported
+            DebugLog.warn("Could not tell where the receiver's state comes from: " + e.getMessage());
+            return Optional.empty();
         }
     }
 
@@ -1042,8 +1059,9 @@ private static void sameState(TypeChecker tc, VariableInstance variableInstance,
             Predicate c = variableInstance.getRefinement().substituteVariable(Keys.WILDCARD, newInstanceName)
                     .substituteVariable(variableInstance.getName(), newInstanceName);
 
-            addInstanceWithState(tc, name, newInstanceName, variableInstance, c, invocation)
-                    .setStateChange(variableInstance.getStateChange().orElse(null));
+            VariableInstance same = addInstanceWithState(tc, name, newInstanceName, variableInstance, c, invocation);
+            same.setStateChange(variableInstance.getStateChange().orElse(null));
+            same.setReturnedBy(variableInstance.getReturnedBy().orElse(null));
         }
     }