From 563dfb6b2e5e35c8e209cb93c17708f0f2a13fd8 Mon Sep 17 00:00:00 2001 From: Catarina Gamboa Date: Tue, 10 Nov 2026 16:30:20 +0000 Subject: [PATCH 1/7] 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: (:) guarantees only ", 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 --- .../refinement_checker/OriginNotes.java | 72 +++++++++++++++++++ .../refinement_checker/VCChecker.java | 1 + .../MethodsFunctionsChecker.java | 6 +- .../liquidjava/api/tests/TestOriginNotes.java | 9 +++ 4 files changed, 87 insertions(+), 1 deletion(-) 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..c3f1930f 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.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 origin notes of a refinement error, which say where the values its expected refinement is about come from. Each @@ -53,6 +67,64 @@ 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 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 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()); + 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 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 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 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/test/java/liquidjava/api/tests/TestOriginNotes.java b/liquidjava-verifier/src/test/java/liquidjava/api/tests/TestOriginNotes.java index 4eaaf74b..929aea5a 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("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 errors = Diagnostics.getInstance().getErrors().stream().toList(); From 4c1890c99e9d6df4f84754e2e371cc17802fdd25 Mon Sep 17 00:00:00 2001 From: Catarina Gamboa Date: Tue, 10 Nov 2026 17:31:59 +0000 Subject: [PATCH 2/7] Drop a ghost definition only when nothing else constrains that ghost The conjunct _ == g(...) is left out only when g is a declared ghost (a built-in such as length may be interpreted), g(...) is in no other conjunct and not in Expected, and every fact of Found that mentions it is the argument's own equality with it. Co-Authored-By: Claude Opus 5.5 --- .../refinement_checker/OriginNotes.java | 45 ++++++++++++++----- 1 file changed, 33 insertions(+), 12 deletions(-) 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 c3f1930f..ae0cc90c 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 @@ -69,8 +69,9 @@ static List unrefinedParameters(RefinementError error, CtElement checked /** * 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 + * 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<>(); @@ -84,7 +85,7 @@ static List returnedValues(RefinementError error, Context context) { : call.function().getPlacementInCode().getAnnotationPosition(); if (declared == null || !declared.isValidPosition() || declared.getFile() == null) continue; - Expression guaranteed = withoutGhostDefinitions(call.returned().getExpression()); + Expression guaranteed = withoutGhostDefinitions(call.returned().getExpression(), variable, error, context); String value = ExpressionFormatter.format(new Var(variable), error.getDisplayNames()); String says = isTrue(guaranteed) ? "guarantees nothing about " + value : "guarantees only " + ExpressionFormatter.format( @@ -95,12 +96,18 @@ static List returnedValues(RefinementError error, Context context) { return notes; } - private static Expression withoutGhostDefinitions(Expression refinement) { + 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) { - boolean definesGhost = ghostDefined(fact).filter( - ghost -> facts.stream().noneMatch(other -> other != fact && containsExpression(other, ghost))) + boolean definesGhost = ghostDefined(fact).filter(ghost -> isGhost(ghost.getName(), context)) + .filter(ghost -> facts.stream() + .noneMatch(other -> other != fact && containsExpression(other, ghost))) + .filter(ghost -> !containsExpression(error.getExpected().getExpression(), ghost)) + .filter(ghost -> known.stream().noneMatch( + other -> containsExpression(other, ghost) && !definesGhostAs(other, ghost, variable))) .isPresent(); if (!definesGhost) kept = isTrue(kept) ? fact : new BinaryExpression(kept, "&&", fact); @@ -108,16 +115,30 @@ private static Expression withoutGhostDefinitions(Expression refinement) { return kept; } - /** The ghost application {@code g(...)} of a fact {@code _ == g(...)} */ - private static Optional ghostDefined(Expression fact) { + /** 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 context.getGhosts().stream().anyMatch(g -> g.matches(name)) + || context.getGhostStates().stream().anyMatch(g -> g.getParent() == null && g.matches(name)); + } + + /** 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) - return Optional.of(right); - if (isWildcard(right) && left instanceof FunctionInvocation) - return Optional.of(left); + 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(); } From 9d2d9e772741d4fc338aa1712b1ed28ac6541d6a Mon Sep 17 00:00:00 2001 From: Catarina Gamboa Date: Tue, 10 Nov 2026 17:44:08 +0000 Subject: [PATCH 3/7] Keep a ghost definition when the ghost is applied anywhere else Co-Authored-By: Claude Opus 5.5 --- .../processor/refinement_checker/OriginNotes.java | 14 ++++++++++---- 1 file changed, 10 insertions(+), 4 deletions(-) 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 ae0cc90c..f23b8d50 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 @@ -27,7 +27,6 @@ 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; @@ -102,12 +101,13 @@ private static Expression withoutGhostDefinitions(Expression refinement, String 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 && containsExpression(other, ghost))) - .filter(ghost -> !containsExpression(error.getExpected().getExpression(), ghost)) + .noneMatch(other -> other != fact && applies(other, ghost.getName()))) + .filter(ghost -> !applies(error.getExpected().getExpression(), ghost.getName())) .filter(ghost -> known.stream().noneMatch( - other -> containsExpression(other, ghost) && !definesGhostAs(other, ghost, variable))) + other -> applies(other, ghost.getName()) && !definesGhostAs(other, ghost, variable))) .isPresent(); if (!definesGhost) kept = isTrue(kept) ? fact : new BinaryExpression(kept, "&&", fact); @@ -115,6 +115,12 @@ private static Expression withoutGhostDefinitions(Expression refinement, String return kept; } + /** Whether {@code expression} applies the function {@code name}, to any arguments */ + private static boolean applies(Expression expression, String name) { + return expression instanceof FunctionInvocation invocation && invocation.getName().equals(name) + || 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 context.getGhosts().stream().anyMatch(g -> g.matches(name)) From edaba46ac7c729217bccc7880a5bb9a7719bad9f Mon Sep 17 00:00:00 2001 From: Catarina Gamboa Date: Tue, 10 Nov 2026 17:51:10 +0000 Subject: [PATCH 4/7] Keep a ghost definition when an alias may apply the ghost Co-Authored-By: Claude Opus 5.5 --- .../processor/refinement_checker/OriginNotes.java | 7 ++++++- 1 file changed, 6 insertions(+), 1 deletion(-) 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 f23b8d50..c09b1285 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 @@ -19,6 +19,7 @@ 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; @@ -115,9 +116,13 @@ private static Expression withoutGhostDefinitions(Expression refinement, String return kept; } - /** Whether {@code expression} applies the function {@code name}, to any arguments */ + /** + * 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)); } From b7df71654f3fb749c9a72e24112dab77899c0868 Mon Sep 17 00:00:00 2001 From: Catarina Gamboa Date: Tue, 10 Nov 2026 18:04:35 +0000 Subject: [PATCH 5/7] Never take a built-in function for a ghost of the same name Co-Authored-By: Claude Opus 5.5 --- .../liquidjava/processor/refinement_checker/OriginNotes.java | 4 ++-- .../src/main/java/liquidjava/utils/Utils.java | 5 +++++ 2 files changed, 7 insertions(+), 2 deletions(-) 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 c09b1285..4d0485fe 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 @@ -128,8 +128,8 @@ private static boolean applies(Expression expression, String 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 context.getGhosts().stream().anyMatch(g -> g.matches(name)) - || context.getGhostStates().stream().anyMatch(g -> g.getParent() == null && g.matches(name)); + return !Utils.isBuiltin(name) && (context.getGhosts().stream().anyMatch(g -> g.matches(name)) + || context.getGhostStates().stream().anyMatch(g -> g.getParent() == null && g.matches(name))); } /** Whether {@code fact} is {@code variable == ghost}, the argument's own definition */ 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) { From 7b0cf52d3ba91ae8f410b8d528d3120ccf39ca6c Mon Sep 17 00:00:00 2001 From: Catarina Gamboa Date: Tue, 10 Nov 2026 19:58:06 +0000 Subject: [PATCH 6/7] Write the returned-value note as Origin: :, guarantees ... Co-Authored-By: Claude Opus 5.5 --- .../liquidjava/processor/refinement_checker/OriginNotes.java | 2 +- .../src/test/java/liquidjava/api/tests/TestOriginNotes.java | 2 +- 2 files changed, 2 insertions(+), 2 deletions(-) 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 4d0485fe..c6b88b98 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 @@ -90,7 +90,7 @@ static List returnedValues(RefinementError error, Context context) { 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(), + notes.add(String.format("Origin: %s:%d, %s %s", declared.getFile().getName(), declared.getLine(), value, says)); } return notes; 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 929aea5a..7404045a 100644 --- a/liquidjava-verifier/src/test/java/liquidjava/api/tests/TestOriginNotes.java +++ b/liquidjava-verifier/src/test/java/liquidjava/api/tests/TestOriginNotes.java @@ -47,7 +47,7 @@ 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"), + assertEquals(List.of("Origin: ArrayListRefinements.java:13, items.size() guarantees only items.size() >= 0"), pick.getMessageNotes()); } From fa846409c5e81a35672297c8aa9ed090b4c7d7cd Mon Sep 17 00:00:00 2001 From: Catarina Gamboa Date: Tue, 10 Nov 2026 20:17:36 +0000 Subject: [PATCH 7/7] Leave out the returned-value note when it names an argument by its parameter Co-Authored-By: Claude Opus 5.5 --- .../refinement_checker/OriginNotes.java | 16 ++++++++++++++++ 1 file changed, 16 insertions(+) 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 c6b88b98..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 @@ -86,6 +86,8 @@ static List returnedValues(RefinementError error, Context context) { 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( @@ -132,6 +134,20 @@ private static boolean isGhost(String name, Context context) { || 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())