From note: name an unrefined parameter as the unknown value's origin

liquidjava-verifier/src/main/java/liquidjava/diagnostics/LJDiagnostic.java

@@ -22,6 +22,7 @@ public class LJDiagnostic extends RuntimeException {
     private String file;
     private SourcePosition position;
     private final List<Hint> hints = new ArrayList<>();
+    private final List<String> messageNotes = new ArrayList<>();
     private String counterexample;
     private ErrorCategory category;
     private static final String PIPE = " | ";
@@ -72,7 +73,12 @@ public SourcePosition getDeclarationPosition() {
 
     /** Lines printed under the message that explain it, such as what the names it uses mean */
     public List<String> getMessageNotes() {
-        return List.of();
+        return Collections.unmodifiableList(messageNotes);
+    }
+
+    /** Adds a line printed under the message, such as where the value it is about comes from */
+    public void addMessageNote(String note) {
+        messageNotes.add(note);
     }
 
     /** Lines printed under the excerpt of where the refinement is declared that explain it */

liquidjava-verifier/src/main/java/liquidjava/diagnostics/errors/RefinementError.java

@@ -120,10 +120,13 @@ public List<AliasExpansion> getExpectedAliases() {
         return expectedAliases;
     }
 
-    /** A where line declaring each alias the message uses */
+    /** A where line declaring each alias the message uses, then the other notes */
     @Override
     public List<String> getMessageNotes() {
-        return aliasDeclarations.stream().map(declaration -> "where " + declaration).toList();
+        List<String> notes = new ArrayList<>(
+                aliasDeclarations.stream().map(declaration -> "where " + declaration).toList());
+        notes.addAll(super.getMessageNotes());
+        return notes;
     }
 
     // Keeps the counterexample assignments to the terms of expected and of the found facts linked to them, except

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

@@ -0,0 +1,90 @@
+package liquidjava.processor.refinement_checker;
+
+import java.util.ArrayList;
+import java.util.List;
+import java.util.Optional;
+import java.util.stream.Collectors;
+
+import liquidjava.diagnostics.categories.ErrorCategory;
+import liquidjava.diagnostics.errors.RefinementError;
+import liquidjava.processor.context.Context;
+import liquidjava.processor.context.Variable;
+import spoon.reflect.declaration.CtConstructor;
+import spoon.reflect.declaration.CtElement;
+import spoon.reflect.declaration.CtExecutable;
+import spoon.reflect.declaration.CtMethod;
+import spoon.reflect.declaration.CtParameter;
+import spoon.reflect.declaration.CtType;
+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
+ */
+final class FromNotes {
+
+    private FromNotes() {
+    }
+
+    /**
+     * When nothing is known about the values expected constrains and each is a parameter of the enclosing method that
+     * is declared with no refinement, a note per parameter saying so. Nothing is said about the callers
+     */
+    static List<String> unrefinedParameters(RefinementError error, CtElement checked, Context context) {
+        Optional<CtExecutable<?>> method = enclosingMethod(checked);
+        List<String> variables = error.getExpected().getVariableNames().stream().distinct().toList();
+        if (error.getCategory().filter(ErrorCategory.UNKNOWN::equals).isEmpty() || method.isEmpty()
+                || variables.isEmpty())
+            return List.of();
+
+        List<String> notes = new ArrayList<>();
+        for (String variable : variables) {
+            Optional<CtParameter<?>> parameter = method.get().getParameters().stream()
+                    .filter(p -> p.getSimpleName().equals(variable)).findFirst();
+            // a written parameter has an instance, which expected would name instead
+            if (parameter.isEmpty() || !parameter.get().getPosition().isValidPosition()
+                    || !(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()));
+        }
+        return notes;
+    }
+
+    /**
+     * 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
+     */
+    private static boolean isRefined(CtParameter<?> parameter, Context context) {
+        if (parameter.getAnnotations().stream()
+                .anyMatch(a -> a.getAnnotationType().getQualifiedName().equals("liquidjava.specification.Refinement")))
+            return true;
+        CtExecutable<?> method = parameter.getParent();
+        int index = method.getParameters().indexOf(parameter);
+        String owner = method.getParent(CtType.class).getQualifiedName();
+        String name = method instanceof CtConstructor<?> ? Utils.getSimpleName(owner) : method.getSimpleName();
+        List<String> types = method.getParameters().stream().map(p -> p.getType().getQualifiedName()).toList();
+        return context.getCtxFunctions().stream()
+                .filter(f -> owner.equals(f.getTargetClass()) && name.equals(Utils.getSimpleName(f.getName()))
+                        && types.equals(f.getArguments().stream()
+                                .map(a -> a.getType() == null ? null : a.getType().getQualifiedName()).toList()))
+                .anyMatch(f -> !f.getArguments().get(index).getMainRefinement().isBooleanTrue());
+    }
+
+    private static Optional<CtExecutable<?>> enclosingMethod(CtElement element) {
+        CtElement parent = element.getParent();
+        while (parent != null && !(parent instanceof CtMethod<?> || parent instanceof CtConstructor<?>))
+            parent = parent.getParent();
+        return Optional.ofNullable((CtExecutable<?>) parent);
+    }
+
+    /** The method as {@code name(ParameterType, ...)}, a constructor by its class name */
+    private static String signature(CtExecutable<?> method) {
+        String name = method instanceof CtConstructor<?> constructor ? constructor.getDeclaringType().getSimpleName()
+                : method.getSimpleName();
+        return name + method.getParameters().stream().map(p -> p.getType().getSimpleName())
+                .collect(Collectors.joining(", ", "(", ")"));
+    }
+}

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

@@ -87,9 +87,11 @@ public void processSubtyping(Predicate expectedType, List<GhostState> list, CtEl
         }
         DebugLog.smtResult(result);
         if (result.isError()) {
-            throw new RefinementError(element.getPosition(), declarationPosition, expectedType,
+            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);
+            throw error;
         }
     }
 

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

@@ -0,0 +1,31 @@
+package liquidjava.api.tests;
+
+import static org.junit.jupiter.api.Assertions.*;
+
+import java.util.List;
+
+import org.junit.jupiter.api.Test;
+
+import liquidjava.api.CommandLineLauncher;
+import liquidjava.diagnostics.Diagnostics;
+import liquidjava.diagnostics.errors.LJError;
+
+class TestFromNotes {
+
+    private static final String TEST_SUITE = "../liquidjava-example/src/main/java/testSuite/";
+
+    @Test
+    void unrefinedParameterIsNamedWithItsMethod() {
+        LJError error = verify("ErrorUnknownArgument.java");
+        assertEquals(List.of("From: amount is a parameter of use(int) (line 10) with no refinement"),
+                error.getMessageNotes());
+        assertTrue(error.toString().contains(error.getMessage() + "\n  From: amount is a parameter"));
+    }
+
+    private static LJError verify(String test) {
+        CommandLineLauncher.launch(TEST_SUITE + test);
+        List<LJError> errors = Diagnostics.getInstance().getErrors().stream().toList();
+        assertEquals(1, errors.size(), "Expected exactly one error from " + test);
+        return errors.get(0);
+    }
+}