Origin note: say what a call's return refinement guarantees about an argument it gives

liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/OriginNotes.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.AliasInvocation;
+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.factsOf;
+import static liquidjava.rj_language.opt.VCSimplificationUtils.isTrue;
 
 /**
  * The origin notes of a refinement error, which say where the values its expected refinement is about come from. Each
@@ -53,6 +67,112 @@ 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 nothing else the error knows or
+     * expects mentions that ghost application: it then constrains no value, so what is left is all the refinement 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(), variable, error, context);
+            if (!namesOnlyCodeVariables(guaranteed, context))
+                continue;
+            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("Origin: %s:%d, %s %s", declared.getFile().getName(), declared.getLine(), value,
+                    says));
+        }
+        return notes;
+    }
+
+    private static Expression withoutGhostDefinitions(Expression refinement, String variable, RefinementError error,
+            Context context) {
+        List<Expression> facts = factsOf(refinement);
+        List<Expression> known = factsOf(error.getFound().getOriginal().getImplication().toPredicate().getExpression());
+        Expression kept = new LiteralBoolean(true);
+        for (Expression fact : facts) {
+            // the ghost on any arguments: an alias of its receiver may be constrained under another name
+            boolean definesGhost = ghostDefined(fact).filter(ghost -> isGhost(ghost.getName(), context))
+                    .filter(ghost -> facts.stream()
+                            .noneMatch(other -> other != fact && applies(other, ghost.getName())))
+                    .filter(ghost -> !applies(error.getExpected().getExpression(), ghost.getName()))
+                    .filter(ghost -> known.stream().noneMatch(
+                            other -> applies(other, ghost.getName()) && !definesGhostAs(other, ghost, variable)))
+                    .isPresent();
+            if (!definesGhost)
+                kept = isTrue(kept) ? fact : new BinaryExpression(kept, "&&", fact);
+        }
+        return kept;
+    }
+
+    /**
+     * Whether {@code expression} may apply the function {@code name}, to any arguments: it does, or it applies an
+     * alias, whose definition may
+     */
+    private static boolean applies(Expression expression, String name) {
+        return expression instanceof FunctionInvocation invocation && invocation.getName().equals(name)
+                || expression instanceof AliasInvocation
+                || expression.getChildren().stream().anyMatch(child -> applies(child, name));
+    }
+
+    /** Whether {@code name} is a declared ghost, unlike a built-in such as {@code length}, which may be interpreted */
+    private static boolean isGhost(String name, Context context) {
+        return !Utils.isBuiltin(name) && (context.getGhosts().stream().anyMatch(g -> g.matches(name))
+                || context.getGhostStates().stream().anyMatch(g -> g.getParent() == null && g.matches(name)));
+    }
+
+    /**
+     * Whether every variable of the refinement but the value is one the code names: an argument the verifier names
+     * after the callee's parameter, such as the {@code 0} of {@code twice(0)} for {@code _ == b * 2}, would read as
+     * that parameter
+     */
+    private static boolean namesOnlyCodeVariables(Expression refinement, Context context) {
+        List<String> variables = new ArrayList<>();
+        refinement.getVariableNames(variables);
+        return variables.stream().filter(name -> !Keys.WILDCARD.equals(name))
+                .allMatch(name -> context.getVariableByName(name) instanceof Variable
+                        || context.getVariableByName(name)instanceof VariableInstance instance
+                                && context.getVariableFromInstance(instance) != null);
+    }
+
+    /** Whether {@code fact} is {@code variable == ghost}, the argument's own definition */
+    private static boolean definesGhostAs(Expression fact, Expression ghost, String variable) {
+        return fact instanceof BinaryExpression equality && "==".equals(equality.getOperator())
+                && (equality.getFirstOperand().equals(new Var(variable)) && equality.getSecondOperand().equals(ghost)
+                        || equality.getSecondOperand().equals(new Var(variable))
+                                && equality.getFirstOperand().equals(ghost));
+    }
+
+    /** The function application {@code g(...)} of a fact {@code _ == g(...)} */
+    private static Optional<FunctionInvocation> 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 ghost)
+            return Optional.of(ghost);
+        if (isWildcard(right) && left instanceof FunctionInvocation ghost)
+            return Optional.of(ghost);
+        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());
             OriginNotes.unrefinedParameters(error, element, context).forEach(error::addMessageNote);
+            OriginNotes.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/main/java/liquidjava/utils/Utils.java

@@ -39,6 +39,11 @@ public class Utils {
     private static final Set<String> DEFAULT_NAMES = Set.of("old", "length", "addToIndex", "getFromIndex");
     private static final List<String> REFINEMENT_KEYS = List.of("value", "to", "from");
 
+    /** Whether {@code name} is a function the refinement language provides, such as {@code length} */
+    public static boolean isBuiltin(String name) {
+        return DEFAULT_NAMES.contains(name);
+    }
+
     public static CtTypeReference<?> getType(String type, Factory factory) {
         // TODO: complete with other types
         return switch (type) {

liquidjava-verifier/src/test/java/liquidjava/api/tests/TestOriginNotes.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("Origin: ArrayListRefinements.java:13, items.size() 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();