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 272c1e83..0e925fb8 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,10 @@ 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.BinaryExpression; +import liquidjava.rj_language.ast.Expression; +import liquidjava.rj_language.ast.Var; +import liquidjava.rj_language.ast.formatter.ArgumentDisplayNames; import liquidjava.utils.Utils; import liquidjava.utils.constants.Formats; import liquidjava.utils.constants.Keys; @@ -458,9 +462,29 @@ 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); + if (describesCallResult(iArg, met)) + ArgumentDisplayNames.recordArgument(nVar, Utils.getSourceCode(iArg)); return nVar; } + /** + * Whether an argument is a call whose refinement states facts about its result, so that it reads best written as + * the call. Any other argument is refined as equal to its expression, and a call refined only as equal to the + * variable holding its result already reads well; named after their code, both would read as tautologies + */ + private static boolean describesCallResult(CtExpression argument, Predicate refinement) { + return argument instanceof CtInvocation && !isEqualityToVariable(refinement.getExpression()); + } + + /** + * Whether a refinement is {@code _ == x} for a variable {@code x} + */ + private static boolean isEqualityToVariable(Expression refinement) { + return refinement instanceof BinaryExpression equality && equality.getOperator().equals("==") + && equality.getFirstOperand()instanceof Var wildcard && wildcard.getName().equals(Keys.WILDCARD) + && equality.getSecondOperand() instanceof Var; + } + private void checkParameters(CtElement invocation, List> arguments, RefinedFunction f, Map map) throws LJError { List functionParams = f.getArguments(); 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..5c3cf23f 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.isWrittenAsInCode(name)) 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..83cebd2c 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); @@ -37,6 +41,13 @@ public static String withoutInstance(String name) { return matcher.matches() ? matcher.group(1) : name; } + /** + * Whether a name is written as in code, qualifier included: a field or a call argument + */ + public static boolean isWrittenAsInCode(String name) { + return isField(name) || ArgumentDisplayNames.argumentCode(name) != null; + } + /** * Whether a name is that of a field, {@code this#.}, possibly with an instance counter */ diff --git a/liquidjava-verifier/src/main/java/liquidjava/utils/Utils.java b/liquidjava-verifier/src/main/java/liquidjava/utils/Utils.java index b85809e0..91ea2f81 100644 --- a/liquidjava-verifier/src/main/java/liquidjava/utils/Utils.java +++ b/liquidjava-verifier/src/main/java/liquidjava/utils/Utils.java @@ -178,6 +178,17 @@ public static String getExpressionFromPosition(SourcePosition position) { return null; } + /** + * The code of an element as written in the source, its lines joined; its printed form when the source is unknown + */ + public static String getSourceCode(CtElement element) { + SourcePosition position = element.getPosition(); + if (position == null || !position.isValidPosition() || position.getCompilationUnit() == null) + return element.toString(); + String source = position.getCompilationUnit().getOriginalSourceCode(); + return source.substring(position.getSourceStart(), position.getSourceEnd() + 1).replaceAll("\\s*\\R\\s*", " "); + } + /** * Whether the context variable {@link #qualifyFieldName} names the field accessed here: a static field, or a field * of the current object ({@code f}, {@code this.f}, {@code super.f}, {@code Outer.this.f}). A field of another 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..6a839e0e 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,22 @@ 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(25); + assertEquals("items.size() == size(this.items) && items.size() >= 0 is not a subtype of items.size() > 0", + shown.message()); + assertEquals("Counterexample: items.size() == 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()); diff --git a/liquidjava-verifier/src/test/java/liquidjava/rj_language/ast/formatter/ExpressionNameResolverTest.java b/liquidjava-verifier/src/test/java/liquidjava/rj_language/ast/formatter/ExpressionNameResolverTest.java index 848f70a5..1d58f282 100644 --- a/liquidjava-verifier/src/test/java/liquidjava/rj_language/ast/formatter/ExpressionNameResolverTest.java +++ b/liquidjava-verifier/src/test/java/liquidjava/rj_language/ast/formatter/ExpressionNameResolverTest.java @@ -2,6 +2,7 @@ import static org.junit.jupiter.api.Assertions.assertEquals; +import org.junit.jupiter.api.AfterEach; import org.junit.jupiter.api.Test; import liquidjava.rj_language.Predicate; @@ -11,6 +12,11 @@ class ExpressionNameResolverTest { + @AfterEach + void forgetRecordedNames() { + ArgumentDisplayNames.clear(); + } + private static Expression parse(String refinement, String prefix) { return RefinementsParser.createAST(refinement, prefix); } @@ -51,4 +57,13 @@ void writesFieldsAsInCodeNextToALocalOfTheSameName() { assertEquals("items⁵ == this.items", expression.toDisplayString()); } + + @Test + void writesACallArgumentAsTheCallerWroteIt() { + ArgumentDisplayNames.recordArgument("#bound_83", "failures.size()"); + Expression expression = Predicate + .createEquals(Predicate.createVar("#bound_83"), Predicate.createLit("0", "int")).getExpression(); + + assertEquals("failures.size()⁸³ == 0", expression.toDisplayString()); + } }