diff --git a/liquidjava-example/src/main/java/testSuite/classes/found_binders_error/Basket.java b/liquidjava-example/src/main/java/testSuite/classes/found_binders_error/Basket.java index 683d4ce5..784a0eeb 100644 --- a/liquidjava-example/src/main/java/testSuite/classes/found_binders_error/Basket.java +++ b/liquidjava-example/src/main/java/testSuite/classes/found_binders_error/Basket.java @@ -68,4 +68,14 @@ void addUp(int first, int second) { void forward(int t) { positive(t); // Expect: Refinement Error } + + @Refinement("_ >= 0") + static int count() { + return 0; + } + + // a call argument is written as the caller wrote it, not as the callee's parameter + int pickByCount() { + return random.nextInt(count()); // Expect: Refinement Error + } } diff --git a/liquidjava-verifier/src/main/java/liquidjava/api/CommandLineLauncher.java b/liquidjava-verifier/src/main/java/liquidjava/api/CommandLineLauncher.java index 00b0256b..200c42f9 100644 --- a/liquidjava-verifier/src/main/java/liquidjava/api/CommandLineLauncher.java +++ b/liquidjava-verifier/src/main/java/liquidjava/api/CommandLineLauncher.java @@ -9,6 +9,7 @@ import liquidjava.diagnostics.warnings.CustomWarning; import liquidjava.processor.RefinementProcessor; import liquidjava.processor.context.ContextHistory; +import liquidjava.rj_language.ast.formatter.ArgumentDisplayNames; import liquidjava.rj_language.ast.formatter.FieldDisplayNames; import liquidjava.specification.Refinement; import picocli.CommandLine; @@ -59,6 +60,7 @@ public static void launch(String... paths) { diagnostics.clear(); contextHistory.clearHistory(); FieldDisplayNames.clear(); + ArgumentDisplayNames.clear(); Launcher launcher = new Launcher(); for (String path : paths) { if (!new File(path).exists()) { 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 74233c3e..8c8f4ade 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 @@ -16,6 +16,7 @@ import liquidjava.processor.refinement_checker.object_checkers.AuxHierarchyRefinementsPassage; import liquidjava.processor.refinement_checker.object_checkers.AuxStateHandler; import liquidjava.rj_language.Predicate; +import liquidjava.rj_language.ast.formatter.ArgumentDisplayNames; import liquidjava.utils.GeneratedNames; import liquidjava.utils.Utils; import liquidjava.utils.constants.Formats; @@ -459,6 +460,10 @@ private String createVariableRepresentingArgument(CtExpression iArg, Variable 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); + // 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()) + ArgumentDisplayNames.recordArgument(nVar, iArg.getOriginalSourceFragment().getSourceCode()); return nVar; } diff --git a/liquidjava-verifier/src/main/java/liquidjava/rj_language/ast/formatter/ArgumentDisplayNames.java b/liquidjava-verifier/src/main/java/liquidjava/rj_language/ast/formatter/ArgumentDisplayNames.java new file mode 100644 index 00000000..832f26ae --- /dev/null +++ b/liquidjava-verifier/src/main/java/liquidjava/rj_language/ast/formatter/ArgumentDisplayNames.java @@ -0,0 +1,35 @@ +package liquidjava.rj_language.ast.formatter; + +import java.util.Map; +import java.util.concurrent.ConcurrentHashMap; + +/** + * The code of the call arguments that a verification names after the callee's parameter, so that + * {@link VariableFormatter} can write such an argument as the caller wrote it ({@code items.size()} rather than + * {@code bound}). Filled during a verification and cleared when the next one starts + */ +public final class ArgumentDisplayNames { + private static final Map ARGUMENTS = new ConcurrentHashMap<>(); + + private ArgumentDisplayNames() { + } + + /** + * Records that an argument instance ({@code #_}) stands for the argument {@code code}. Only the + * display changes + */ + public static void recordArgument(String instanceName, String code) { + ARGUMENTS.put(instanceName, code); + } + + /** + * Forgets what the previous verification recorded + */ + public static void clear() { + ARGUMENTS.clear(); + } + + static String argumentCode(String instanceName) { + return ARGUMENTS.get(instanceName); + } +} diff --git a/liquidjava-verifier/src/main/java/liquidjava/rj_language/ast/formatter/ExpressionNameResolver.java b/liquidjava-verifier/src/main/java/liquidjava/rj_language/ast/formatter/ExpressionNameResolver.java index 35cdc836..0c72a785 100644 --- a/liquidjava-verifier/src/main/java/liquidjava/rj_language/ast/formatter/ExpressionNameResolver.java +++ b/liquidjava-verifier/src/main/java/liquidjava/rj_language/ast/formatter/ExpressionNameResolver.java @@ -22,8 +22,8 @@ public static ExpressionNameResolver forExpression(Expression expression) { public String resolveVariable(String name) { String formatted = VariableFormatter.format(name); - // a field is always written as in code, as its binder and the counterexample write it - if (VariableFormatter.isField(name)) + // a field or call argument is always written as in code, as its binder and the counterexample write it + if (VariableFormatter.isField(name) || ArgumentDisplayNames.argumentCode(name) != null) return formatted; return isAmbiguous(name, variables, ExpressionNameResolver::getVariableSimpleName) ? formatted : Utils.getSimpleName(formatted); diff --git a/liquidjava-verifier/src/main/java/liquidjava/rj_language/ast/formatter/VariableFormatter.java b/liquidjava-verifier/src/main/java/liquidjava/rj_language/ast/formatter/VariableFormatter.java index 8a1d57fd..66ccca41 100644 --- a/liquidjava-verifier/src/main/java/liquidjava/rj_language/ast/formatter/VariableFormatter.java +++ b/liquidjava-verifier/src/main/java/liquidjava/rj_language/ast/formatter/VariableFormatter.java @@ -25,6 +25,10 @@ public static String format(String name) { String baseName = matcher.group(1); String counter = matcher.group(2); + // the counter tells apart calls written alike, which can return different values + String argument = ArgumentDisplayNames.argumentCode(name); + if (argument != null) + return argument + toSuperscript(counter); String receiver = FieldDisplayNames.writeReceiver(name); if (receiver != null && isField(baseName)) return (receiver.isEmpty() ? "" : receiver + ".") + fieldOf(baseName) + toSuperscript(counter); diff --git a/liquidjava-verifier/src/test/java/liquidjava/api/tests/TestFoundBinders.java b/liquidjava-verifier/src/test/java/liquidjava/api/tests/TestFoundBinders.java index 6f5d44ff..6861fffa 100644 --- a/liquidjava-verifier/src/test/java/liquidjava/api/tests/TestFoundBinders.java +++ b/liquidjava-verifier/src/test/java/liquidjava/api/tests/TestFoundBinders.java @@ -57,16 +57,21 @@ static void verify() { @Test void issueReproducerDropsTheTrueFieldRow() { Shown shown = ERRORS.get(25); - assertEquals(List.of("∀bound bound == size(this.items) && bound >= 0"), shown.rows()); - assertEquals("bound == size(this.items) && bound >= 0 is not a subtype of bound > 0", shown.message()); + assertEquals(List.of("∀items.size() items.size() == size(this.items) && items.size() >= 0"), shown.rows()); + } + + @Test + void callArgumentIsWrittenAsTheCallerWroteIt() { + Shown shown = ERRORS.get(79); + assertEquals("count() >= 0 is not a subtype of count() > 0", shown.message()); + assertEquals("Counterexample: count() == 0", shown.counterexample()); } @Test void steppingBackReachesTheOriginalWithTheDroppedRow() { Shown shown = ERRORS.get(25); - assertEquals( - List.of("∀this.items true", "∀items items == this.items", "∀bound bound == size(items) && bound >= 0"), - shown.originalRows()); + assertEquals(List.of("∀this.items true", "∀items items == this.items", + "∀items.size() items.size() == size(items) && items.size() >= 0"), shown.originalRows()); assertEquals(List.of("Substitution", "Binder"), shown.steps()); assertEquals(List.of("this#testSuite.classes.found_binders_error.Basket.items", "#items_", "#bound_"), shown.originalBinders());