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 784a0eeb..68dc2530 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 @@ -78,4 +78,11 @@ static int count() { int pickByCount() { return random.nextInt(count()); // Expect: Refinement Error } + + // the earlier values of a variable are written with the line they come from + void negate() { + @Refinement("_ > 0") + int b = 8; + b = -b; // Expect: Refinement Error + } } diff --git a/liquidjava-verifier/src/main/java/liquidjava/diagnostics/AliasExpansion.java b/liquidjava-verifier/src/main/java/liquidjava/diagnostics/AliasExpansion.java index 475cab70..92e49f8f 100644 --- a/liquidjava-verifier/src/main/java/liquidjava/diagnostics/AliasExpansion.java +++ b/liquidjava-verifier/src/main/java/liquidjava/diagnostics/AliasExpansion.java @@ -11,6 +11,8 @@ import liquidjava.rj_language.ast.AliasInvocation; import liquidjava.rj_language.ast.Expression; import liquidjava.rj_language.ast.Var; +import liquidjava.rj_language.ast.formatter.DisplayNames; +import liquidjava.rj_language.ast.formatter.ExpressionFormatter; import spoon.reflect.cu.SourcePosition; /** @@ -40,19 +42,19 @@ public String declaration() { /** * The expansions of the alias invocations in an expression, each invocation once in order of appearance, followed - * by those of the aliases their definitions use + * by those of the aliases their definitions use, naming the variables as the diagnostic does */ - public static List of(Expression expression, List aliases) { + public static List of(Expression expression, List aliases, DisplayNames names) { Map byName = new LinkedHashMap<>(); for (AliasWrapper alias : aliases) byName.put(alias.getName(), alias); Map expansions = new LinkedHashMap<>(); - collect(expression, byName, expansions, new HashSet<>()); + collect(expression, byName, names, expansions, new HashSet<>()); return new ArrayList<>(expansions.values()); } // Expands the invocations under expression, skipping aliases already being expanded so recursive ones end - private static void collect(Expression expression, Map aliases, + private static void collect(Expression expression, Map aliases, DisplayNames names, Map expansions, Set expanding) { List invocations = new ArrayList<>(); invocationsOf(expression, invocations); @@ -64,14 +66,16 @@ private static void collect(Expression expression, Map ali if (alias == null || expanding.contains(alias.getName()) || expansions.containsKey(key)) continue; Expression body = substituteArguments(alias, invocation.getArgs()); - expansions.put(key, new AliasExpansion(invocation.toDisplayString(), body.toDisplayString(), - alias.getName(), alias.getVarNames(), alias.getDefinition(), alias.getPosition())); + expansions.put(key, + new AliasExpansion(ExpressionFormatter.format(invocation, names), + ExpressionFormatter.format(body, names), alias.getName(), alias.getVarNames(), + alias.getDefinition(), alias.getPosition())); bodies.put(key, body); } for (Map.Entry body : bodies.entrySet()) { Set inner = new HashSet<>(expanding); inner.add(expansions.get(body.getKey()).alias()); - collect(body.getValue(), aliases, expansions, inner); + collect(body.getValue(), aliases, names, expansions, inner); } } diff --git a/liquidjava-verifier/src/main/java/liquidjava/diagnostics/errors/ErrorMessage.java b/liquidjava-verifier/src/main/java/liquidjava/diagnostics/errors/ErrorMessage.java new file mode 100644 index 00000000..bd6e2153 --- /dev/null +++ b/liquidjava-verifier/src/main/java/liquidjava/diagnostics/errors/ErrorMessage.java @@ -0,0 +1,43 @@ +package liquidjava.diagnostics.errors; + +import static liquidjava.rj_language.opt.VCSimplificationUtils.linkedToExpected; + +import java.util.ArrayList; +import java.util.List; +import java.util.function.Predicate; + +import liquidjava.diagnostics.TranslationTable; +import liquidjava.processor.context.PlacementInCode; +import liquidjava.rj_language.ast.Expression; +import liquidjava.rj_language.ast.formatter.DisplayNames; +import liquidjava.rj_language.ast.formatter.ExpressionFormatter; +import liquidjava.rj_language.opt.VCSimplificationResult; + +/** The message of an error that found does not prove expected, and the names it gives the variables of both */ +record ErrorMessage(String text, DisplayNames names) { + + /** + * Writes the facts of found about the values expected constrains and expected in frame, or only expected when + * showsFound rejects those facts; path conditions about other values stay in the derivation + */ + static ErrorMessage of(Expression expected, VCSimplificationResult found, TranslationTable translationTable, + Predicate showsFound, String frame) { + Expression shown = linkedToExpected(found.getImplication().toPredicate().getExpression(), expected); + // the names of the message first, then those only the original found has, each with the line of its value + List message = new ArrayList<>(); + shown.getVariableNames(message); + expected.getVariableNames(message); + VCSimplificationResult original = found.getOriginal(); + List others = original.getBinders(); + original.getImplication().toPredicate().getExpression().getVariableNames(others); + DisplayNames names = DisplayNames.of(message, others, name -> { + PlacementInCode placement = translationTable == null ? null : translationTable.get(name); + return placement == null ? null : placement.getLine(); + }); + String expectedText = ExpressionFormatter.format(expected, names); + String text = showsFound.test(shown) + ? String.format(frame, ExpressionFormatter.format(shown, names), expectedText) + : String.format("expected %s but could not prove it", expectedText); + return new ErrorMessage(text, names); + } +} diff --git a/liquidjava-verifier/src/main/java/liquidjava/diagnostics/errors/LJError.java b/liquidjava-verifier/src/main/java/liquidjava/diagnostics/errors/LJError.java index 66ff9fd2..21e5b3fa 100644 --- a/liquidjava-verifier/src/main/java/liquidjava/diagnostics/errors/LJError.java +++ b/liquidjava-verifier/src/main/java/liquidjava/diagnostics/errors/LJError.java @@ -3,6 +3,7 @@ import liquidjava.diagnostics.LJDiagnostic; import liquidjava.diagnostics.TranslationTable; import liquidjava.diagnostics.Colors; +import liquidjava.rj_language.ast.formatter.DisplayNames; import spoon.reflect.cu.SourcePosition; /** @@ -11,6 +12,7 @@ public abstract class LJError extends LJDiagnostic { private final TranslationTable translationTable; + private final DisplayNames displayNames; public LJError(String title, String message, SourcePosition pos, TranslationTable translationTable) { this(title, message, pos, translationTable, null); @@ -18,11 +20,22 @@ public LJError(String title, String message, SourcePosition pos, TranslationTabl public LJError(String title, String message, SourcePosition pos, TranslationTable translationTable, String customMessage) { - super(title, message, pos, Colors.BOLD_RED, customMessage); + this(title, new ErrorMessage(message, null), pos, translationTable, customMessage); + } + + LJError(String title, ErrorMessage message, SourcePosition pos, TranslationTable translationTable, + String customMessage) { + super(title, message.text(), pos, Colors.BOLD_RED, customMessage); this.translationTable = translationTable != null ? translationTable : new TranslationTable(); + this.displayNames = message.names(); } public TranslationTable getTranslationTable() { return translationTable; } + + /** The names the error gives its variables, for every view of it to show them alike, or null when it has none */ + public DisplayNames getDisplayNames() { + return displayNames; + } } 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 ab00bc95..55f5c0a6 100644 --- a/liquidjava-verifier/src/main/java/liquidjava/diagnostics/errors/RefinementError.java +++ b/liquidjava-verifier/src/main/java/liquidjava/diagnostics/errors/RefinementError.java @@ -19,7 +19,6 @@ import liquidjava.rj_language.ast.Enum; import liquidjava.rj_language.ast.Expression; import liquidjava.rj_language.ast.Var; -import liquidjava.rj_language.ast.formatter.VariableFormatter; import liquidjava.rj_language.opt.VCSimplificationResult; import liquidjava.smt.Counterexample; import liquidjava.utils.GeneratedNames; @@ -52,19 +51,20 @@ public class RefinementError extends LJError { public RefinementError(SourcePosition position, SourcePosition declarationPosition, Predicate expected, VCSimplificationResult found, TranslationTable translationTable, Counterexample counterexample, String customMessage, List aliases) { - super("Refinement Error", message(expected, found), position, translationTable, customMessage); + super("Refinement Error", ErrorMessage.of(expected.getExpression(), found, translationTable, + shown -> !isTrue(shown), "%s is not a subtype of %s"), position, translationTable, customMessage); this.expected = expected; this.found = found; Expression foundExpression = found.getImplication().toPredicate().getExpression(); - this.foundAliases = AliasExpansion.of(foundExpression, aliases); - this.expectedAliases = AliasExpansion.of(expected.getExpression(), aliases); + this.foundAliases = AliasExpansion.of(foundExpression, aliases, getDisplayNames()); + this.expectedAliases = AliasExpansion.of(expected.getExpression(), aliases, getDisplayNames()); this.aliasDeclarations = aliasDeclarations(linkedToExpected(foundExpression, expected.getExpression()), expected.getExpression(), aliases); this.counterexample = filterCounterexample(counterexample); this.declarationPosition = declarationPosition; if (!this.counterexample.isEmpty()) { String counterexampleString = this.counterexample.assignments().stream() - .map(a -> VariableFormatter.format(a.first()) + " == " + a.second()) + .map(a -> getDisplayNames().get(a.first()) + " == " + a.second()) .collect(Collectors.joining(" && ")); setCounterexampleStr("Counterexample: " + counterexampleString); } @@ -74,23 +74,11 @@ public RefinementError(SourcePosition position, SourcePosition declarationPositi "Not enough information to prove the expected refinement. Add a refinement or condition to constrain it.")); } - // Only the facts of found about the values expected constrains; path conditions about other values stay in the - // derivation - private static String message(Predicate expected, VCSimplificationResult found) { - Expression shown = linkedToExpected(found.getImplication().toPredicate().getExpression(), - expected.getExpression()); - if (isTrue(shown)) - return String.format("expected %s but could not prove it", expected.getExpression().toDisplayString()); - return String.format("%s is not a subtype of %s", shown.toDisplayString(), - expected.getExpression().toDisplayString()); - } - // Each alias the message uses once, with those their definitions use, as declared - private static List aliasDeclarations(Expression shownFound, Expression expected, - List aliases) { + private List aliasDeclarations(Expression shownFound, Expression expected, List aliases) { Map declarations = new LinkedHashMap<>(); for (Expression shown : List.of(shownFound, expected)) - for (AliasExpansion expansion : AliasExpansion.of(shown, aliases)) + for (AliasExpansion expansion : AliasExpansion.of(shown, aliases, getDisplayNames())) declarations.putIfAbsent(expansion.alias(), expansion.declaration()); return new ArrayList<>(declarations.values()); } @@ -182,10 +170,7 @@ private static boolean states(Expression term, Expression value, Pair originalBinders() { - VCSimplificationResult original = getFound(); - while (original.getOrigin() != null) - original = original.getOrigin(); - return original.getBinders(); + return getFound().getOriginal().getBinders(); } // 0 for terms of expected found says nothing about, whose values alone break it, 1 for the other terms of diff --git a/liquidjava-verifier/src/main/java/liquidjava/diagnostics/errors/StateRefinementError.java b/liquidjava-verifier/src/main/java/liquidjava/diagnostics/errors/StateRefinementError.java index e60d709a..f1e3810a 100644 --- a/liquidjava-verifier/src/main/java/liquidjava/diagnostics/errors/StateRefinementError.java +++ b/liquidjava-verifier/src/main/java/liquidjava/diagnostics/errors/StateRefinementError.java @@ -1,7 +1,6 @@ package liquidjava.diagnostics.errors; import static liquidjava.rj_language.opt.VCSimplificationUtils.isTrue; -import static liquidjava.rj_language.opt.VCSimplificationUtils.linkedToExpected; import java.util.List; @@ -30,7 +29,9 @@ public class StateRefinementError extends LJError { public StateRefinementError(SourcePosition position, SourcePosition declarationPosition, Predicate expected, VCSimplificationResult found, TranslationTable translationTable, String customMessage, List hints, ErrorCategory category, StateErrorContext context) { - super("State Refinement Error", message(expected, found), position, translationTable, customMessage); + super("State Refinement Error", ErrorMessage.of(expected.getExpression(), found, translationTable, + StateRefinementError::appliesGhost, "found %s but expected %s"), position, translationTable, + customMessage); this.declarationPosition = declarationPosition; this.expected = expected; this.found = found; @@ -44,15 +45,6 @@ public StateRefinementError(SourcePosition position, SourcePosition declarationP // Only the facts of found about the objects of expected, and only when one of them tells a state: an alias or a // guard on another value says nothing about the state expected needs - private static String message(Predicate expected, VCSimplificationResult found) { - Expression shown = linkedToExpected(found.getImplication().toPredicate().getExpression(), - expected.getExpression()); - if (!appliesGhost(shown)) - return String.format("expected %s but could not prove it", expected.getExpression().toDisplayString()); - return String.format("found %s but expected %s", shown.toDisplayString(), - expected.getExpression().toDisplayString()); - } - private static boolean appliesGhost(Expression expression) { return expression instanceof FunctionInvocation || expression.getChildren().stream().anyMatch(StateRefinementError::appliesGhost); diff --git a/liquidjava-verifier/src/main/java/liquidjava/processor/context/ContextHistory.java b/liquidjava-verifier/src/main/java/liquidjava/processor/context/ContextHistory.java index 6b9af787..2d6aef85 100644 --- a/liquidjava-verifier/src/main/java/liquidjava/processor/context/ContextHistory.java +++ b/liquidjava-verifier/src/main/java/liquidjava/processor/context/ContextHistory.java @@ -3,7 +3,9 @@ import java.util.HashMap; import java.util.HashSet; import java.util.Map; +import java.util.Objects; import java.util.Set; +import java.util.stream.Stream; import liquidjava.api.CommandLineLauncher; import liquidjava.utils.Utils; @@ -96,4 +98,11 @@ public Set getMethods() { public Map> getFileScopes() { return fileScopes; } + + /** The line where the value of a saved variable comes from, or null when unknown */ + public Integer lineOf(String name) { + return Stream.concat(localVars.stream(), globalVars.stream()).filter(v -> v.getName().equals(name)) + .map(RefinedVariable::getPlacementInCode).filter(Objects::nonNull).map(PlacementInCode::getLine) + .filter(Objects::nonNull).findFirst().orElse(null); + } } diff --git a/liquidjava-verifier/src/main/java/liquidjava/processor/context/PlacementInCode.java b/liquidjava-verifier/src/main/java/liquidjava/processor/context/PlacementInCode.java index 77eddd35..c59654d3 100644 --- a/liquidjava-verifier/src/main/java/liquidjava/processor/context/PlacementInCode.java +++ b/liquidjava-verifier/src/main/java/liquidjava/processor/context/PlacementInCode.java @@ -31,6 +31,11 @@ public SourcePosition getAnnotationPosition() { return annotationPosition; } + /** The line of this placement, or null when it is not in code */ + public Integer getLine() { + return position == null || !position.isValidPosition() ? null : position.getLine(); + } + public static PlacementInCode createPlacement(CtElement elem) { CtElement elemCopy = elem.clone(); // cleanup annotations diff --git a/liquidjava-verifier/src/main/java/liquidjava/rj_language/ast/formatter/DisplayNames.java b/liquidjava-verifier/src/main/java/liquidjava/rj_language/ast/formatter/DisplayNames.java new file mode 100644 index 00000000..8dabfbef --- /dev/null +++ b/liquidjava-verifier/src/main/java/liquidjava/rj_language/ast/formatter/DisplayNames.java @@ -0,0 +1,81 @@ +package liquidjava.rj_language.ast.formatter; + +import java.util.Collection; +import java.util.Comparator; +import java.util.HashMap; +import java.util.LinkedHashSet; +import java.util.List; +import java.util.Map; +import java.util.Set; +import java.util.function.Function; +import java.util.stream.Collectors; + +/** + * The names of the variables of one scope, such as an error or a refinement, as they are shown. A name is written as in + * code; when the scope has several variables written alike, one keeps the plain name and each other one gets the line + * its value comes from, {@code x@12}, numbered when they share a line or have none, {@code x@12#1} and {@code x@12#2}. + * The plain name goes to the declared variable, or else to its latest instance, preferring those shown first + */ +public final class DisplayNames { + private final Map tags = new HashMap<>(); + + private DisplayNames() { + } + + /** + * @param shown + * the names shown first, such as those of an error message + * @param others + * the other names of the scope + * @param lineOf + * the line where the value of a variable comes from, or null when unknown + */ + public static DisplayNames of(Collection shown, Collection others, + Function lineOf) { + DisplayNames names = new DisplayNames(); + Set all = new LinkedHashSet<>(shown); + all.addAll(others); + Map> alike = all.stream().collect(Collectors.groupingBy(VariableFormatter::format)); + for (List variables : alike.values()) { + if (variables.size() > 1) + names.tag(variables, shown, lineOf); + } + return names; + } + + /** + * The display name of a variable, or of a ghost application over variables such as {@code size(#s_2)} + */ + public String get(String name) { + return VariableFormatter.format(name, variable -> tags.getOrDefault(variable, "")); + } + + private void tag(List alike, Collection shown, Function lineOf) { + String plain = plainOf(alike, shown); + Map> byLine = alike.stream().filter(name -> !name.equals(plain)) + .sorted(Comparator.comparingInt(VariableFormatter::counterOf)) + .collect(Collectors.groupingBy(name -> lineTag(lineOf.apply(name)))); + byLine.forEach((line, variables) -> { + for (int i = 0; i < variables.size(); i++) + tags.put(variables.get(i), tagFor(line, i, variables.size())); + }); + } + + // The declared variable, or else the latest instance, preferring those shown + private static String plainOf(List alike, Collection shown) { + List candidates = alike.stream().filter(shown::contains).toList(); + return (candidates.isEmpty() ? alike : candidates).stream() + .max(Comparator.comparing((String name) -> VariableFormatter.counterOf(name) < 0) + .thenComparing(VariableFormatter::counterOf)) + .orElseThrow(); + } + + // The line alone tells apart a single value from it; values that share a line, or have none, are numbered + private static String tagFor(String line, int index, int count) { + return count == 1 && !line.isEmpty() ? line : line + "#" + (index + 1); + } + + private static String lineTag(Integer line) { + return line == null ? "" : "@" + line; + } +} diff --git a/liquidjava-verifier/src/main/java/liquidjava/rj_language/ast/formatter/ExpressionFormatter.java b/liquidjava-verifier/src/main/java/liquidjava/rj_language/ast/formatter/ExpressionFormatter.java index 7016229d..30299244 100644 --- a/liquidjava-verifier/src/main/java/liquidjava/rj_language/ast/formatter/ExpressionFormatter.java +++ b/liquidjava-verifier/src/main/java/liquidjava/rj_language/ast/formatter/ExpressionFormatter.java @@ -1,6 +1,8 @@ package liquidjava.rj_language.ast.formatter; +import java.util.ArrayList; import java.util.List; +import java.util.function.Function; import java.util.stream.Collectors; import liquidjava.rj_language.Predicate; @@ -28,8 +30,8 @@ public class ExpressionFormatter implements ExpressionVisitor { private final ExpressionNameResolver nameResolver; - private ExpressionFormatter(Expression expression) { - this.nameResolver = ExpressionNameResolver.forExpression(expression); + private ExpressionFormatter(Expression expression, DisplayNames names) { + this.nameResolver = ExpressionNameResolver.forExpression(expression, names); } public static String format(Predicate predicate) { @@ -37,7 +39,23 @@ public static String format(Predicate predicate) { } public static String format(Expression expression) { - return new ExpressionFormatter(expression).formatExpression(expression); + return format(expression, name -> null); + } + + /** + * Formats an expression on its own, telling apart its variables written alike by the line their values come from + */ + public static String format(Expression expression, Function lineOf) { + List variables = new ArrayList<>(); + expression.getVariableNames(variables); + return format(expression, DisplayNames.of(variables, List.of(), lineOf)); + } + + /** + * Formats an expression of a scope, such as an error, naming its variables as the scope does + */ + public static String format(Expression expression, DisplayNames names) { + return new ExpressionFormatter(expression, names).formatExpression(expression); } private String formatExpression(Expression expression) { 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 0c72a785..a908711d 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 @@ -13,15 +13,20 @@ final class ExpressionNameResolver { private final Set variables = new HashSet<>(); private final Set functions = new HashSet<>(); + private final DisplayNames names; - public static ExpressionNameResolver forExpression(Expression expression) { - ExpressionNameResolver resolver = new ExpressionNameResolver(); + private ExpressionNameResolver(DisplayNames names) { + this.names = names; + } + + public static ExpressionNameResolver forExpression(Expression expression, DisplayNames names) { + ExpressionNameResolver resolver = new ExpressionNameResolver(names); resolver.collect(expression); return resolver; } public String resolveVariable(String name) { - String formatted = VariableFormatter.format(name); + String formatted = names.get(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; 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 66ccca41..7afe8949 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 @@ -1,39 +1,54 @@ package liquidjava.rj_language.ast.formatter; +import java.util.function.Function; import java.util.regex.Matcher; import java.util.regex.Pattern; /** - * Formats internal variable names into a cleaner display representation using superscript notation + * Formats internal variable names as they are written in code, without the instance counter */ public final class VariableFormatter { private static final Pattern INSTACE_VAR_PATTERN = Pattern.compile("^#(.+)_([0-9]+)$"); // this#. private static final Pattern FIELD_PATTERN = Pattern.compile("^this#([\\w.$]+)\\.([\\w$]+)$"); - private static final char[] SUPERSCRIPT_CHARS = { '⁰', '¹', '²', '³', '⁴', '⁵', '⁶', '⁷', '⁸', '⁹' }; public static String format(String name) { + return format(name, instance -> ""); + } + + /** + * Formats a name, appending to each variable instance in it the tag that tells it apart from other instances + */ + static String format(String name, Function tagOf) { if (name == null) return null; if (isApplication(name)) - return formatApplication(name); + return formatApplication(name, tagOf); Matcher matcher = INSTACE_VAR_PATTERN.matcher(name); if (!matcher.matches()) return formatField(name); String baseName = matcher.group(1); - String counter = matcher.group(2); - // the counter tells apart calls written alike, which can return different values + // the tag tells apart calls written alike, which can return different values + String tag = tagOf.apply(name); String argument = ArgumentDisplayNames.argumentCode(name); if (argument != null) - return argument + toSuperscript(counter); + return argument + tag; String receiver = FieldDisplayNames.writeReceiver(name); if (receiver != null && isField(baseName)) - return (receiver.isEmpty() ? "" : receiver + ".") + fieldOf(baseName) + toSuperscript(counter); + return (receiver.isEmpty() ? "" : receiver + ".") + fieldOf(baseName) + tag; String prefix = isReturn(baseName) ? "#" : ""; - return prefix + formatField(baseName) + toSuperscript(counter); + return prefix + formatField(baseName) + tag; + } + + /** + * The instance counter of a name, or -1 for a name that is not an instance + */ + static int counterOf(String name) { + Matcher matcher = INSTACE_VAR_PATTERN.matcher(name); + return matcher.matches() ? Integer.parseInt(matcher.group(2)) : -1; } public static String withoutInstance(String name) { @@ -73,17 +88,6 @@ private static String simpleTypeName(String qualifiedName) { return qualifiedName.substring(start + 1); } - private static String toSuperscript(String number) { - StringBuilder sb = new StringBuilder(number.length()); - for (char c : number.toCharArray()) { - int index = c - '0'; - if (index < 0 || index >= SUPERSCRIPT_CHARS.length) - return number; - sb.append(SUPERSCRIPT_CHARS[index]); - } - return sb.toString(); - } - private static boolean isReturn(String id) { return id.equals("ret"); } @@ -97,7 +101,7 @@ private static boolean isApplication(String name) { * Formats the arguments of a ghost application such as {@code size(#s_2)}, splitting them only at top-level commas * so nested applications keep theirs */ - private static String formatApplication(String name) { + private static String formatApplication(String name, Function tagOf) { int open = name.indexOf('('); String args = name.substring(open + 1, name.length() - 1); StringBuilder formatted = new StringBuilder(name.substring(0, open)).append('('); @@ -112,7 +116,7 @@ else if (c == ')') else if (c == ',' && depth == 0) { if (start > 0) formatted.append(", "); - formatted.append(format(args.substring(start, i).trim())); + formatted.append(format(args.substring(start, i).trim(), tagOf)); start = i + 1; } } diff --git a/liquidjava-verifier/src/main/java/liquidjava/rj_language/opt/VCSimplificationResult.java b/liquidjava-verifier/src/main/java/liquidjava/rj_language/opt/VCSimplificationResult.java index e545b997..b1083f9a 100644 --- a/liquidjava-verifier/src/main/java/liquidjava/rj_language/opt/VCSimplificationResult.java +++ b/liquidjava-verifier/src/main/java/liquidjava/rj_language/opt/VCSimplificationResult.java @@ -40,6 +40,13 @@ public VCSimplificationResult getOrigin() { return origin; } + /** + * Returns the original VC chain this result was simplified from, or this result if it is the original + */ + public VCSimplificationResult getOriginal() { + return origin == null ? this : origin.getOriginal(); + } + /** * Returns the name of the simplification pass that produced this result or null for the original VC chain */ diff --git a/liquidjava-verifier/src/test/java/liquidjava/api/tests/TestAliasExpansions.java b/liquidjava-verifier/src/test/java/liquidjava/api/tests/TestAliasExpansions.java index 2461db4a..acb942ba 100644 --- a/liquidjava-verifier/src/test/java/liquidjava/api/tests/TestAliasExpansions.java +++ b/liquidjava-verifier/src/test/java/liquidjava/api/tests/TestAliasExpansions.java @@ -39,7 +39,6 @@ void messageDeclaresEachAliasOnceAsWritten() { private static void assertExpansion(List expansions, String invocation, String expansion) { assertEquals(1, expansions.size()); - // instance numbers of variables are shown as superscripts assertEquals(invocation, expansions.get(0).invocation().replaceAll("[⁰¹²³⁴⁵⁶⁷⁸⁹]", "")); assertEquals(expansion, expansions.get(0).expansion().replaceAll("[⁰¹²³⁴⁵⁶⁷⁸⁹]", "")); } 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 6861fffa..ae883369 100644 --- a/liquidjava-verifier/src/test/java/liquidjava/api/tests/TestFoundBinders.java +++ b/liquidjava-verifier/src/test/java/liquidjava/api/tests/TestFoundBinders.java @@ -15,7 +15,8 @@ import liquidjava.diagnostics.errors.LJError; import liquidjava.diagnostics.errors.RefinementError; import liquidjava.processor.VCImplication; -import liquidjava.rj_language.ast.formatter.VariableFormatter; +import liquidjava.rj_language.ast.formatter.DisplayNames; +import liquidjava.rj_language.ast.formatter.ExpressionFormatter; import liquidjava.rj_language.opt.VCSimplificationResult; /** @@ -47,10 +48,9 @@ static void verify() { steps.add(0, original.getSimplification()); List originalBinders = original.getBinders().stream().map(b -> b.replaceAll("[0-9]+$", "")) .toList(); - ERRORS.put(error.getPosition().getLine(), - new Shown(rows(found.getImplication()), plain(error.getMessage()), - error.getCounterexampleStr() == null ? null : plain(error.getCounterexampleStr()), - rows(original.getImplication()), steps, originalBinders)); + DisplayNames names = error.getDisplayNames(); + ERRORS.put(error.getPosition().getLine(), new Shown(rows(found.getImplication(), names), error.getMessage(), + error.getCounterexampleStr(), rows(original.getImplication(), names), steps, originalBinders)); } } @@ -105,18 +105,22 @@ void writeToAnotherObjectsFieldIsNamedAfterThatObject() { ERRORS.get(48).rows()); } - // the rows of Found as the IDE writes them: binder name, then its refinement - private static List rows(VCImplication found) { + @Test + void earlierValuesOfAVariableAreWrittenWithTheirLine() { + Shown shown = ERRORS.get(86); + assertEquals("b@86 == 8 && b@86 > 0 && b == -b@86 is not a subtype of b > 0", shown.message()); + assertEquals("Counterexample: b == -8", shown.counterexample()); + assertEquals(List.of("∀b@85 b@85 == 8", "∀b@86 b@86 == b@85 && b@86 > 0", "∀b b == -b@86"), + shown.originalRows()); + } + + // the rows of Found as the IDE writes them, with the error's names: binder name, then its refinement + private static List rows(VCImplication found, DisplayNames names) { List rows = new ArrayList<>(); for (VCImplication current = found; current != null; current = current.getNext()) { - String refinement = current.getRefinement().getExpression().toDisplayString(); - rows.add(plain(current.hasBinder() ? "∀" + VariableFormatter.format(current.getName()) + " " + refinement - : refinement)); + String refinement = ExpressionFormatter.format(current.getRefinement().getExpression(), names); + rows.add(current.hasBinder() ? "∀" + names.get(current.getName()) + " " + refinement : refinement); } return rows; } - - private static String plain(String text) { - return text.replaceAll("[⁰¹²³⁴⁵⁶⁷⁸⁹]", ""); - } } diff --git a/liquidjava-verifier/src/test/java/liquidjava/diagnostics/errors/RefinementErrorCounterexampleTest.java b/liquidjava-verifier/src/test/java/liquidjava/diagnostics/errors/RefinementErrorCounterexampleTest.java index 813da9b5..aa1d5944 100644 --- a/liquidjava-verifier/src/test/java/liquidjava/diagnostics/errors/RefinementErrorCounterexampleTest.java +++ b/liquidjava-verifier/src/test/java/liquidjava/diagnostics/errors/RefinementErrorCounterexampleTest.java @@ -65,7 +65,7 @@ void keepsGhostApplicationsOfExpectedAndFormatsTheirArguments() { RefinementError error = error("size(#s_3) > 0", vc("∀port:int. port > 0", "true"), "port=1", "size(#s_3)=0", "length(#a_1)=4"); assertEquals(List.of(pair("size(#s_3)", "0")), error.getCounterexample().assignments()); - assertEquals("Counterexample: size(s³) == 0", error.getCounterexampleStr()); + assertEquals("Counterexample: size(s) == 0", error.getCounterexampleStr()); } @Test @@ -159,7 +159,7 @@ void omitsGhostValuesWithSeveralArgumentsFoundAlreadyStates() { RefinementError error = error("at(#l_1, #i_2) > 0 && #i_2 > 0", vc("∀#i_2:int. at(#l_1, #i_2) == 0", "true"), "at(#l_1, #i_2)=0", "#i_2=0"); assertEquals(List.of(pair("#i_2", "0")), error.getCounterexample().assignments()); - assertEquals("Counterexample: i² == 0", error.getCounterexampleStr()); + assertEquals("Counterexample: i == 0", error.getCounterexampleStr()); } @Test @@ -167,7 +167,7 @@ void keepsGhostValuesWithSeveralArgumentsFoundSaysNothingAbout() { RefinementError error = error("at(#l_1, #i_2) > 0", vc("∀#i_2:int. #i_2 > 0", "true"), "at(#l_1, #i_2)=0", "#i_2=1"); assertEquals(List.of(pair("at(#l_1, #i_2)", "0"), pair("#i_2", "1")), error.getCounterexample().assignments()); - assertEquals("Counterexample: at(l¹, i²) == 0 && i² == 1", error.getCounterexampleStr()); + assertEquals("Counterexample: at(l, i) == 0 && i == 1", error.getCounterexampleStr()); } private static RefinementError error(String expected, VCImplication found, String... assignments) { diff --git a/liquidjava-verifier/src/test/java/liquidjava/processor/context/ContextHistoryTest.java b/liquidjava-verifier/src/test/java/liquidjava/processor/context/ContextHistoryTest.java new file mode 100644 index 00000000..e044b7d8 --- /dev/null +++ b/liquidjava-verifier/src/test/java/liquidjava/processor/context/ContextHistoryTest.java @@ -0,0 +1,26 @@ +package liquidjava.processor.context; + +import static org.junit.jupiter.api.Assertions.assertEquals; + +import org.junit.jupiter.api.Test; + +import liquidjava.api.CommandLineLauncher; +import liquidjava.rj_language.ast.formatter.ExpressionFormatter; + +class ContextHistoryTest { + + @Test + void refinementNamesTheVariableAndTheLineOfItsEarlierValue() { + CommandLineLauncher.cmdArgs.lspMode = true; + try { + CommandLineLauncher.launch("../liquidjava-example/src/main/java/testSuite/ErrorUnaryOperators.java"); + } finally { + CommandLineLauncher.cmdArgs.lspMode = false; + } + ContextHistory history = ContextHistory.getInstance(); + RefinedVariable b = history.getLocalVars().stream().filter(v -> v.getName().equals("b")).findFirst() + .orElseThrow(); + assertEquals("b == b@19 && b > 0", + ExpressionFormatter.format(b.getRefinement().getExpression(), history::lineOf)); + } +} diff --git a/liquidjava-verifier/src/test/java/liquidjava/rj_language/ast/ExpressionFormatterTest.java b/liquidjava-verifier/src/test/java/liquidjava/rj_language/ast/ExpressionFormatterTest.java index a7d013ec..40236922 100644 --- a/liquidjava-verifier/src/test/java/liquidjava/rj_language/ast/ExpressionFormatterTest.java +++ b/liquidjava-verifier/src/test/java/liquidjava/rj_language/ast/ExpressionFormatterTest.java @@ -50,9 +50,9 @@ void formatsGrouping() { assertEquals("a + b * c", parse("a + (b * c)").toDisplayString()); assertEquals("a && b > 0", parse("a && (b > 0)").toDisplayString()); assertEquals("a && b && c", parse("a && (b && c)").toDisplayString()); - assertEquals("size(stack²⁹⁴) > 0", parse("(size(#stack_294) > 0)").toDisplayString()); - assertEquals("size(stack²⁹⁴) > 0 && ready", parse("(size(#stack_294) > 0) && ready").toDisplayString()); - assertEquals("ready && size(stack²⁹⁴) > 0", parse("ready && (size(#stack_294) > 0)").toDisplayString()); + assertEquals("size(stack) > 0", parse("(size(#stack_294) > 0)").toDisplayString()); + assertEquals("size(stack) > 0 && ready", parse("(size(#stack_294) > 0) && ready").toDisplayString()); + assertEquals("ready && size(stack) > 0", parse("ready && (size(#stack_294) > 0)").toDisplayString()); } @Test diff --git a/liquidjava-verifier/src/test/java/liquidjava/rj_language/ast/formatter/DisplayNamesTest.java b/liquidjava-verifier/src/test/java/liquidjava/rj_language/ast/formatter/DisplayNamesTest.java new file mode 100644 index 00000000..a1981a7a --- /dev/null +++ b/liquidjava-verifier/src/test/java/liquidjava/rj_language/ast/formatter/DisplayNamesTest.java @@ -0,0 +1,33 @@ +package liquidjava.rj_language.ast.formatter; + +import static org.junit.jupiter.api.Assertions.assertEquals; + +import java.util.List; +import java.util.Map; + +import org.junit.jupiter.api.Test; + +class DisplayNamesTest { + + @Test + void tagsEarlierValuesWithTheirLineAndKeepsTheLatestShownPlain() { + Map lines = Map.of("#s_3", 12, "#s_4", 13, "#s_5", 13, "#s_6", 14); + DisplayNames names = DisplayNames.of(List.of("#s_4", "#s_5"), List.of("#s_3", "#s_6"), lines::get); + assertEquals("s", names.get("#s_5")); + assertEquals("s@13", names.get("#s_4")); + assertEquals("s@12", names.get("#s_3")); + assertEquals("s@14", names.get("#s_6")); + assertEquals("size(s@13)", names.get("size(#s_4)")); + } + + @Test + void numbersValuesFromOneLineOrNoneAndKeepsTheDeclaredVariablePlain() { + DisplayNames names = DisplayNames.of(List.of("n", "#n_1", "#n_2", "#m_1", "#m_2"), List.of(), + name -> name.startsWith("#n") ? 11 : null); + assertEquals("n", names.get("n")); + assertEquals("n@11#1", names.get("#n_1")); + assertEquals("n@11#2", names.get("#n_2")); + assertEquals("m", names.get("#m_2")); + assertEquals("m#1", names.get("#m_1")); + } +} 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..a6666915 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,8 @@ import static org.junit.jupiter.api.Assertions.assertEquals; +import java.util.List; + import org.junit.jupiter.api.Test; import liquidjava.rj_language.Predicate; @@ -15,10 +17,13 @@ private static Expression parse(String refinement, String prefix) { return RefinementsParser.createAST(refinement, prefix); } + private static ExpressionNameResolver resolver(Expression expression) { + return ExpressionNameResolver.forExpression(expression, DisplayNames.of(List.of(), List.of(), name -> null)); + } + @Test void stripsQualifiedNamesWhenUnambiguous() { - ExpressionNameResolver resolver = ExpressionNameResolver - .forExpression(parse("size(this) == size(this)", "java.util.List")); + ExpressionNameResolver resolver = resolver(parse("size(this) == size(this)", "java.util.List")); assertEquals("size", resolver.resolveFunction("java.util.List.size")); } @@ -27,7 +32,7 @@ void stripsQualifiedNamesWhenUnambiguous() { void keepsQualifiedNamesForDifferentPrefixes() { Expression expression = new BinaryExpression(parse("size(this)", "java.util.ArrayList"), "==", parse("size(this)", "java.util.ArrayDeque")); - ExpressionNameResolver resolver = ExpressionNameResolver.forExpression(expression); + ExpressionNameResolver resolver = resolver(expression); assertEquals("java.util.ArrayList.size", resolver.resolveFunction("java.util.ArrayList.size")); assertEquals("java.util.ArrayDeque.size", resolver.resolveFunction("java.util.ArrayDeque.size")); @@ -37,10 +42,10 @@ void keepsQualifiedNamesForDifferentPrefixes() { void keepsQualifiedNamesForDifferentInstances() { Predicate differentInstances = Predicate.createEquals(Predicate.createVar("#java.util.ArrayList.size_1"), Predicate.createVar("#java.util.ArrayDeque.size_2")); - ExpressionNameResolver resolver = ExpressionNameResolver.forExpression(differentInstances.getExpression()); + ExpressionNameResolver resolver = resolver(differentInstances.getExpression()); - assertEquals("java.util.ArrayList.size¹", resolver.resolveVariable("#java.util.ArrayList.size_1")); - assertEquals("java.util.ArrayDeque.size²", resolver.resolveVariable("#java.util.ArrayDeque.size_2")); + assertEquals("java.util.ArrayList.size", resolver.resolveVariable("#java.util.ArrayList.size_1")); + assertEquals("java.util.ArrayDeque.size", resolver.resolveVariable("#java.util.ArrayDeque.size_2")); } @Test @@ -49,6 +54,6 @@ void writesFieldsAsInCodeNextToALocalOfTheSameName() { .createEquals(Predicate.createVar("#items_5"), Predicate.createVar("this#shop.Basket.items")) .getExpression(); - assertEquals("items⁵ == this.items", expression.toDisplayString()); + assertEquals("items == this.items", expression.toDisplayString()); } } diff --git a/liquidjava-verifier/src/test/java/liquidjava/rj_language/ast/formatter/VariableFormatterTest.java b/liquidjava-verifier/src/test/java/liquidjava/rj_language/ast/formatter/VariableFormatterTest.java index 2ea3c9d6..d0ea02a7 100644 --- a/liquidjava-verifier/src/test/java/liquidjava/rj_language/ast/formatter/VariableFormatterTest.java +++ b/liquidjava-verifier/src/test/java/liquidjava/rj_language/ast/formatter/VariableFormatterTest.java @@ -15,40 +15,40 @@ void forgetRecordedNames() { @Test void formatsVariables() { assertEquals("x", VariableFormatter.format("x")); - assertEquals("x²", VariableFormatter.format("#x_2")); - assertEquals("#if_condition¹²", VariableFormatter.format("##if_condition_12")); - assertEquals("#size_result⁴", VariableFormatter.format("##size_result_4")); - assertEquals("size_result⁴", VariableFormatter.format("#size_result_4")); - assertEquals("#ret³", VariableFormatter.format("#ret_3")); + assertEquals("x", VariableFormatter.format("#x_2")); + assertEquals("#if_condition", VariableFormatter.format("##if_condition_12")); + assertEquals("#size_result", VariableFormatter.format("##size_result_4")); + assertEquals("size_result", VariableFormatter.format("#size_result_4")); + assertEquals("#ret", VariableFormatter.format("#ret_3")); assertEquals("this#Class", VariableFormatter.format("this#Class")); // ghost applications - assertEquals("size(s²)", VariableFormatter.format("size(#s_2)")); + assertEquals("size(s)", VariableFormatter.format("size(#s_2)")); assertEquals("size(bag)", VariableFormatter.format("size(bag)")); - assertEquals("at(list³, #get_result¹²)", VariableFormatter.format("at(#list_3, ##get_result_12)")); + assertEquals("at(list, #get_result)", VariableFormatter.format("at(#list_3, ##get_result_12)")); assertEquals("size(this)", VariableFormatter.format("size(this)")); - assertEquals("f(g(a¹, b²), c³)", VariableFormatter.format("f(g(#a_1, #b_2), #c_3)")); - assertEquals("f(g(h(a¹)), b)", VariableFormatter.format("f(g(h(#a_1)),b)")); + assertEquals("f(g(a, b), c)", VariableFormatter.format("f(g(#a_1, #b_2), #c_3)")); + assertEquals("f(g(h(a)), b)", VariableFormatter.format("f(g(h(#a_1)),b)")); assertEquals("size()", VariableFormatter.format("size()")); } @Test void writesInstanceFieldsAsInCode() { assertEquals("this.items", VariableFormatter.format("this#shop.Basket.items")); - assertEquals("this.port⁴", VariableFormatter.format("#this#pkg.Outer$Job.port_4")); + assertEquals("this.port", VariableFormatter.format("#this#pkg.Outer$Job.port_4")); } @Test void writesStaticFieldsWithTheirClass() { FieldDisplayNames.recordStaticField("this#pkg.Outer$Job.count"); - assertEquals("Job.count³", VariableFormatter.format("#this#pkg.Outer$Job.count_3")); + assertEquals("Job.count", VariableFormatter.format("#this#pkg.Outer$Job.count_3")); } @Test void writesAFieldWrittenThroughAnotherObjectWithThatObject() { FieldDisplayNames.recordWriteReceiver("#this#pkg.W.level_1", "other"); - assertEquals("other.level¹", VariableFormatter.format("#this#pkg.W.level_1")); - assertEquals("this.level²", VariableFormatter.format("#this#pkg.W.level_2")); + assertEquals("other.level", VariableFormatter.format("#this#pkg.W.level_1")); + assertEquals("this.level", VariableFormatter.format("#this#pkg.W.level_2")); FieldDisplayNames.clear(); - assertEquals("this.level¹", VariableFormatter.format("#this#pkg.W.level_1")); + assertEquals("this.level", VariableFormatter.format("#this#pkg.W.level_1")); } } diff --git a/liquidjava-verifier/src/test/java/liquidjava/rj_language/opt/VCBinderSimplificationTest.java b/liquidjava-verifier/src/test/java/liquidjava/rj_language/opt/VCBinderSimplificationTest.java index 5260c6ea..ddd3c72c 100644 --- a/liquidjava-verifier/src/test/java/liquidjava/rj_language/opt/VCBinderSimplificationTest.java +++ b/liquidjava-verifier/src/test/java/liquidjava/rj_language/opt/VCBinderSimplificationTest.java @@ -140,7 +140,7 @@ void keepsPathConditionAnotherRowMentions() { assertSimplificationSteps(forStateError("open(f)"), vc("∀##if_condition_1:boolean. p", "∀##if_condition_2:boolean. q", "∀f:Object. ##if_condition_1 ? open(f) : created(f)"), - step("p", "#if_condition¹ ? open(f) : created(f)")); + step("p", "#if_condition ? open(f) : created(f)")); } @Test diff --git a/liquidjava-verifier/src/test/java/liquidjava/rj_language/opt/VCSubstitutionTest.java b/liquidjava-verifier/src/test/java/liquidjava/rj_language/opt/VCSubstitutionTest.java index 299e7b02..e02d5581 100644 --- a/liquidjava-verifier/src/test/java/liquidjava/rj_language/opt/VCSubstitutionTest.java +++ b/liquidjava-verifier/src/test/java/liquidjava/rj_language/opt/VCSubstitutionTest.java @@ -45,7 +45,7 @@ void keepsSourceNodeWhenItIsLastInChain() { @Test void keepsReturnBinderWhenConclusionIsSeparate() { assertSimplificationSteps(substitution, vc("∀x:int. true", "∀#ret_8:int. #ret_8 == x + 1"), - step("true", "#ret⁸ == x + 1")); + step("true", "#ret == x + 1")); } @Test