diff --git a/liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/OriginNotes.java b/liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/OriginNotes.java index 863f09a5..a094ef3d 100644 --- a/liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/OriginNotes.java +++ b/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 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 returnedValues(RefinementError error, Context context) { + List 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 facts = factsOf(refinement); + List 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 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 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 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 d68fdd5a..25cd299b 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 @@ -91,6 +91,7 @@ public void processSubtyping(Predicate expectedType, List 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; } } diff --git a/liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/general_checkers/MethodsFunctionsChecker.java b/liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/general_checkers/MethodsFunctionsChecker.java index 598d6fc2..5da69fca 100644 --- a/liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/general_checkers/MethodsFunctionsChecker.java +++ b/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()) diff --git a/liquidjava-verifier/src/main/java/liquidjava/utils/Utils.java b/liquidjava-verifier/src/main/java/liquidjava/utils/Utils.java index b85809e0..c664fa3e 100644 --- a/liquidjava-verifier/src/main/java/liquidjava/utils/Utils.java +++ b/liquidjava-verifier/src/main/java/liquidjava/utils/Utils.java @@ -39,6 +39,11 @@ public class Utils { private static final Set DEFAULT_NAMES = Set.of("old", "length", "addToIndex", "getFromIndex"); private static final List 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) { diff --git a/liquidjava-verifier/src/test/java/liquidjava/api/tests/TestOriginNotes.java b/liquidjava-verifier/src/test/java/liquidjava/api/tests/TestOriginNotes.java index 4eaaf74b..7404045a 100644 --- a/liquidjava-verifier/src/test/java/liquidjava/api/tests/TestOriginNotes.java +++ b/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 errors = Diagnostics.getInstance().getErrors().stream().toList();