Say what a call's return refinement guarantees about an argument it gives

A refinement error whose Expected is about a call argument that is a
call to a refined method now has the note "From: <call> (<File>:<line>)
guarantees only <refinement>", instantiated as the error writes it. An
equality _ == g(...) defining a ghost is left out when the ghost is
nowhere else in the refinement: then it constrains no value, so what is
left is exactly what the refinement says about the value.

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

Author: CatarinaGamboa

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

@@ -16,6 +16,20 @@
 import spoon.reflect.declaration.CtParameter;
 import spoon.reflect.declaration.CtType;
 import liquidjava.utils.Utils;
+import liquidjava.utils.constants.Keys;
+import liquidjava.processor.context.CallResult;
+import liquidjava.processor.context.VariableInstance;
+import liquidjava.rj_language.ast.BinaryExpression;
+import liquidjava.rj_language.ast.Expression;
+import liquidjava.rj_language.ast.FunctionInvocation;
+import liquidjava.rj_language.ast.LiteralBoolean;
+import liquidjava.rj_language.ast.Var;
+import liquidjava.rj_language.ast.formatter.ExpressionFormatter;
+import spoon.reflect.cu.SourcePosition;
+
+import static liquidjava.rj_language.opt.VCSimplificationUtils.containsExpression;
+import static liquidjava.rj_language.opt.VCSimplificationUtils.factsOf;
+import static liquidjava.rj_language.opt.VCSimplificationUtils.isTrue;
 
 /**
  * The notes of a refinement error that say where the values its expected refinement is about come from. Each is given
@@ -53,6 +67,64 @@ static List<String> unrefinedParameters(RefinementError error, CtElement checked
         return notes;
     }
 
+    /**
+     * For each argument of expected that is a call to a refined method, what the method's return refinement guarantees
+     * about it. An equality defining a ghost, {@code _ == size(this)}, is left out when the ghost is nowhere else in
+     * the refinement: it then constrains no value, so what is left is all it says about the value
+     */
+    static List<String> returnedValues(RefinementError error, Context context) {
+        List<String> notes = new ArrayList<>();
+        for (String variable : error.getExpected().getVariableNames().stream().distinct().toList()) {
+            // a call argument, which has no variable of its own and is shown as the call
+            if (!(context.getVariableByName(variable)instanceof VariableInstance instance)
+                    || instance.getReturnedBy().isEmpty() || context.getVariableFromInstance(instance) != null)
+                continue;
+            CallResult call = instance.getReturnedBy().get();
+            SourcePosition declared = call.function().getPlacementInCode() == null ? null
+                    : call.function().getPlacementInCode().getAnnotationPosition();
+            if (declared == null || !declared.isValidPosition() || declared.getFile() == null)
+                continue;
+            Expression guaranteed = withoutGhostDefinitions(call.returned().getExpression());
+            String value = ExpressionFormatter.format(new Var(variable), error.getDisplayNames());
+            String says = isTrue(guaranteed) ? "guarantees nothing about " + value
+                    : "guarantees only " + ExpressionFormatter.format(
+                            guaranteed.substitute(new Var(Keys.WILDCARD), new Var(variable)), error.getDisplayNames());
+            notes.add(String.format("From: %s (%s:%d) %s", value, declared.getFile().getName(), declared.getLine(),
+                    says));
+        }
+        return notes;
+    }
+
+    private static Expression withoutGhostDefinitions(Expression refinement) {
+        List<Expression> facts = factsOf(refinement);
+        Expression kept = new LiteralBoolean(true);
+        for (Expression fact : facts) {
+            boolean definesGhost = ghostDefined(fact).filter(
+                    ghost -> facts.stream().noneMatch(other -> other != fact && containsExpression(other, ghost)))
+                    .isPresent();
+            if (!definesGhost)
+                kept = isTrue(kept) ? fact : new BinaryExpression(kept, "&&", fact);
+        }
+        return kept;
+    }
+
+    /** The ghost application {@code g(...)} of a fact {@code _ == g(...)} */
+    private static Optional<Expression> ghostDefined(Expression fact) {
+        if (!(fact instanceof BinaryExpression equality) || !"==".equals(equality.getOperator()))
+            return Optional.empty();
+        Expression left = equality.getFirstOperand();
+        Expression right = equality.getSecondOperand();
+        if (isWildcard(left) && right instanceof FunctionInvocation)
+            return Optional.of(right);
+        if (isWildcard(right) && left instanceof FunctionInvocation)
+            return Optional.of(left);
+        return Optional.empty();
+    }
+
+    private static boolean isWildcard(Expression expression) {
+        return expression instanceof Var var && Keys.WILDCARD.equals(var.getName());
+    }
+
     /**
      * Whether the parameter is written with a refinement, even {@code true}, or a specification of its method refines
      * it, such as an external one, which the method's body is not checked against

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

@@ -91,6 +91,7 @@ public void processSubtyping(Predicate expectedType, List<GhostState> list, CtEl
                     implBeforeChange.simplify(NeededVariables.forRefinementError(expectedType)), map,
                     result.getCounterexample(), customMessage, context.getAliases());
             FromNotes.unrefinedParameters(error, element, context).forEach(error::addMessageNote);
+            FromNotes.returnedValues(error, context).forEach(error::addMessageNote);
             throw error;
         }
     }

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

@@ -472,7 +472,11 @@ private String createVariableRepresentingArgument(CtExpression<?> iArg, Variable
         if (!unknown && !met.getVariableNames().contains(Keys.WILDCARD))
             met = Predicate.createEquals(Predicate.createVar(Keys.WILDCARD), met);
         String nVar = String.format(Formats.INSTANCE, fArg.getName(), rtc.getContext().getCounter());
-        rtc.getContext().addInstanceToContext(nVar, fArg.getType(), met.substituteVariable(Keys.WILDCARD, nVar), iArg);
+        RefinedVariable argument = rtc.getContext().addInstanceToContext(nVar, fArg.getType(),
+                met.substituteVariable(Keys.WILDCARD, nVar), iArg);
+        if (argument instanceof VariableInstance instance
+                && iArg.getMetadata(Keys.CALL_RESULT)instanceof CallResult call)
+            instance.setReturnedBy(call);
         // a call in the source reads as written; any other argument is refined as equal to its code, which would read
         // as a tautology
         if (iArg instanceof CtInvocation && iArg.getPosition().isValidPosition())

liquidjava-verifier/src/test/java/liquidjava/api/tests/TestFromNotes.java

@@ -42,6 +42,15 @@ void stateOfAReceiverAnotherNameMayHoldIsNotTraced() {
         assertEquals(List.of(), captured.getMessageNotes());
     }
 
+    @Test
+    void callArgumentIsTracedToWhatItsReturnRefinementGuaranteesAboutIt() {
+        CommandLineLauncher.launch(TEST_SUITE + "classes/found_binders_error");
+        LJError pick = Diagnostics.getInstance().getErrors().stream().filter(e -> e.getPosition().getLine() == 25)
+                .findFirst().orElseThrow();
+        assertEquals(List.of("From: items.size() (ArrayListRefinements.java:13) guarantees only items.size() >= 0"),
+                pick.getMessageNotes());
+    }
+
     private static LJError verify(String test) {
         CommandLineLauncher.launch(TEST_SUITE + test);
         List<LJError> errors = Diagnostics.getInstance().getErrors().stream().toList();