diff --git a/liquidjava-verifier/src/main/java/liquidjava/diagnostics/LJDiagnostic.java b/liquidjava-verifier/src/main/java/liquidjava/diagnostics/LJDiagnostic.java index 6224bb67..eb5b5951 100644 --- a/liquidjava-verifier/src/main/java/liquidjava/diagnostics/LJDiagnostic.java +++ b/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 hints = new ArrayList<>(); + private final List 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 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 */ diff --git a/liquidjava-verifier/src/main/java/liquidjava/diagnostics/errors/RefinementError.java b/liquidjava-verifier/src/main/java/liquidjava/diagnostics/errors/RefinementError.java index 775c740b..9ca40925 100644 --- a/liquidjava-verifier/src/main/java/liquidjava/diagnostics/errors/RefinementError.java +++ b/liquidjava-verifier/src/main/java/liquidjava/diagnostics/errors/RefinementError.java @@ -120,10 +120,13 @@ public List 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 getMessageNotes() { - return aliasDeclarations.stream().map(declaration -> "where " + declaration).toList(); + List 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 diff --git a/liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/FromNotes.java b/liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/FromNotes.java new file mode 100644 index 00000000..f0a1aed2 --- /dev/null +++ b/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 unrefinedParameters(RefinementError error, CtElement checked, Context context) { + Optional> method = enclosingMethod(checked); + List variables = error.getExpected().getVariableNames().stream().distinct().toList(); + if (error.getCategory().filter(ErrorCategory.UNKNOWN::equals).isEmpty() || method.isEmpty() + || variables.isEmpty()) + return List.of(); + + List notes = new ArrayList<>(); + for (String variable : variables) { + Optional> 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 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> 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(", ", "(", ")")); + } +} diff --git a/liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/VCChecker.java b/liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/VCChecker.java index 84d285e4..23243571 100644 --- a/liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/VCChecker.java +++ b/liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/VCChecker.java @@ -87,9 +87,11 @@ public void processSubtyping(Predicate expectedType, List 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; } } diff --git a/liquidjava-verifier/src/test/java/liquidjava/api/tests/TestFromNotes.java b/liquidjava-verifier/src/test/java/liquidjava/api/tests/TestFromNotes.java new file mode 100644 index 00000000..48c55373 --- /dev/null +++ b/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 errors = Diagnostics.getInstance().getErrors().stream().toList(); + assertEquals(1, errors.size(), "Expected exactly one error from " + test); + return errors.get(0); + } +}