diff --git a/liquidjava-example/src/main/java/testSuite/classes/found_binders_error/ArrayListRefinements.java b/liquidjava-example/src/main/java/testSuite/classes/found_binders_error/ArrayListRefinements.java new file mode 100644 index 000000000..56a182c08 --- /dev/null +++ b/liquidjava-example/src/main/java/testSuite/classes/found_binders_error/ArrayListRefinements.java @@ -0,0 +1,15 @@ +package testSuite.classes.found_binders_error; + +import liquidjava.specification.ExternalRefinementsFor; +import liquidjava.specification.Ghost; +import liquidjava.specification.Refinement; + +@ExternalRefinementsFor("java.util.ArrayList") +@Ghost("int size") +public interface ArrayListRefinements { + + public void ArrayList(); + + @Refinement("_ == size(this) && _ >= 0") + public int size(); +} 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 new file mode 100644 index 000000000..8de524557 --- /dev/null +++ b/liquidjava-example/src/main/java/testSuite/classes/found_binders_error/Basket.java @@ -0,0 +1,58 @@ +package testSuite.classes.found_binders_error; + +import java.util.ArrayList; +import java.util.Random; + +import liquidjava.specification.Refinement; + +// Found drops the true rows the error does not need and writes fields as in code (#457) +public class Basket { + static int served; + + @Refinement("_ >= 0") + int level; + + private final ArrayList items; + private final Random random = new Random(); + + Basket(ArrayList items) { + this.items = items; + } + + // the issue's reproducer: the field row only says true + String pick() { + ArrayList items = this.items; + return items.get(random.nextInt(items.size())); // Expect: Refinement Error + } + + // a static field + void serve() { + @Refinement("_ > 0") + int count = served + 1; // Expect: Refinement Error + } + + // writes to another object's field are checked as on main, and named after that object + void setOther(Basket other) { + other.level = -1; // Expect: Refinement Error + } + + void incrementOther(Basket other) { + other.level++; + } + + void addToOther(Basket other) { + other.level += 1; + } + + void decrementOther(Basket other) { + other.level--; // Expect: Refinement Error + } + + void writeThroughAlias() { + level = 7; + Basket other = this; + other.level = 3; + @Refinement("_ == 7") + int k = level; // Expect: Refinement Error + } +} diff --git a/liquidjava-example/src/main/java/testSuite/classes/found_binders_error/RandomRefinements.java b/liquidjava-example/src/main/java/testSuite/classes/found_binders_error/RandomRefinements.java new file mode 100644 index 000000000..73e6720ef --- /dev/null +++ b/liquidjava-example/src/main/java/testSuite/classes/found_binders_error/RandomRefinements.java @@ -0,0 +1,12 @@ +package testSuite.classes.found_binders_error; + +import liquidjava.specification.ExternalRefinementsFor; +import liquidjava.specification.Refinement; + +@ExternalRefinementsFor("java.util.Random") +public interface RandomRefinements { + + public void Random(); + + public int nextInt(@Refinement("bound > 0") int bound); +} diff --git a/liquidjava-verifier/src/main/java/liquidjava/api/CommandLineLauncher.java b/liquidjava-verifier/src/main/java/liquidjava/api/CommandLineLauncher.java index f10d9abef..00b0256b9 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.FieldDisplayNames; import liquidjava.specification.Refinement; import picocli.CommandLine; import spoon.Launcher; @@ -57,6 +58,7 @@ public static void launch(String... paths) { diagnostics.clear(); contextHistory.clearHistory(); + FieldDisplayNames.clear(); Launcher launcher = new Launcher(); for (String path : paths) { if (!new File(path).exists()) { diff --git a/liquidjava-verifier/src/main/java/liquidjava/processor/VCImplication.java b/liquidjava-verifier/src/main/java/liquidjava/processor/VCImplication.java index 37ea117b4..c1163152e 100644 --- a/liquidjava-verifier/src/main/java/liquidjava/processor/VCImplication.java +++ b/liquidjava-verifier/src/main/java/liquidjava/processor/VCImplication.java @@ -3,6 +3,7 @@ import java.util.Objects; import liquidjava.rj_language.Predicate; +import liquidjava.rj_language.opt.NeededVariables; import liquidjava.rj_language.opt.VCSimplification; import liquidjava.rj_language.opt.VCSimplificationResult; import liquidjava.utils.Utils; @@ -79,6 +80,10 @@ public VCSimplificationResult simplify() { return VCSimplification.simplifyToFixedPoint(this); } + public VCSimplificationResult simplify(NeededVariables needed) { + return VCSimplification.simplifyToFixedPoint(this, needed); + } + public Predicate toPredicate() { return hasBinder() || hasNext() ? toConjunctions() : refinement; } diff --git a/liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/TypeChecker.java b/liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/TypeChecker.java index fb9efd2ec..388656a1a 100644 --- a/liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/TypeChecker.java +++ b/liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/TypeChecker.java @@ -23,6 +23,7 @@ import liquidjava.processor.state_machine.StateMachineBuilder; import liquidjava.processor.state_machine.StateSolver; import liquidjava.rj_language.Predicate; +import liquidjava.rj_language.ast.formatter.FieldDisplayNames; import liquidjava.rj_language.parsing.RefinementsParser; import liquidjava.smt.SMTEvaluator; import liquidjava.smt.SMTResult; @@ -382,6 +383,8 @@ public void checkVariableRefinements(Predicate refinementFound, String simpleNam Predicate cet = cEt.substituteVariable(Keys.WILDCARD, simpleName); String newName = String.format(Formats.INSTANCE, simpleName, context.getCounter()); + Utils.untrackedWriteReceiver(usage) + .ifPresent(receiver -> FieldDisplayNames.recordWriteReceiver(newName, receiver)); Predicate correctNewRefinement = refinementFound.substituteVariable(Keys.WILDCARD, newName); correctNewRefinement = correctNewRefinement.substituteVariable(Keys.THIS, newName); cEt = cEt.substituteVariable(simpleName, newName); 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 819e4b6a2..b086c062d 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 @@ -20,6 +20,7 @@ import liquidjava.rj_language.ast.Expression; import liquidjava.rj_language.ast.Ite; import liquidjava.rj_language.ast.Var; +import liquidjava.rj_language.opt.NeededVariables; import liquidjava.smt.Counterexample; import liquidjava.smt.SMTEvaluator; import liquidjava.smt.SMTResult; @@ -83,7 +84,8 @@ public void processSubtyping(Predicate expectedType, List list, CtEl DebugLog.smtResult(result); if (result.isError()) { throw new RefinementError(element.getPosition(), declarationPosition, expectedType, - implBeforeChange.simplify(), map, result.getCounterexample(), customMessage); + implBeforeChange.simplify(NeededVariables.forRefinementError(expectedType)), map, + result.getCounterexample(), customMessage); } } @@ -442,8 +444,8 @@ protected void throwRefinementError(SourcePosition position, SourcePosition decl Predicate found, Counterexample counterexample, String customMessage) throws RefinementError { TranslationTable map = new TranslationTable(); VCImplication premises = buildPremiseChain(map, expected, found); - throw new RefinementError(position, declarationPosition, expected, premises.simplify(), map, counterexample, - customMessage); + throw new RefinementError(position, declarationPosition, expected, + premises.simplify(NeededVariables.forRefinementError(expected)), map, counterexample, customMessage); } protected void throwStateRefinementError(SourcePosition position, SourcePosition declarationPosition, @@ -451,8 +453,9 @@ protected void throwStateRefinementError(SourcePosition position, SourcePosition StateErrorContext context) throws StateRefinementError { TranslationTable map = new TranslationTable(); VCImplication foundState = buildPremiseChain(map, expected, found); - throw new StateRefinementError(position, declarationPosition, expected, foundState.simplify(), map, - customMessage, hints, category, context); + throw new StateRefinementError(position, declarationPosition, expected, + foundState.simplify(NeededVariables.forStateError(expected)), map, customMessage, hints, category, + context); } protected void throwStateConflictError(SourcePosition position, Predicate expected) throws StateConflictError { 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 b7a2ae7e4..35cdc8366 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,6 +22,9 @@ 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)) + 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/FieldDisplayNames.java b/liquidjava-verifier/src/main/java/liquidjava/rj_language/ast/formatter/FieldDisplayNames.java new file mode 100644 index 000000000..0894c3476 --- /dev/null +++ b/liquidjava-verifier/src/main/java/liquidjava/rj_language/ast/formatter/FieldDisplayNames.java @@ -0,0 +1,51 @@ +package liquidjava.rj_language.ast.formatter; + +import java.util.Map; +import java.util.Set; +import java.util.concurrent.ConcurrentHashMap; + +/** + * What a verification learns about field names that their internal form does not say, so that {@link VariableFormatter} + * can write them as in code: which fields are static, and which field instances were created by a write through another + * object. Filled during a verification and cleared when the next one starts + */ +public final class FieldDisplayNames { + private static final Set STATIC_FIELDS = ConcurrentHashMap.newKeySet(); + private static final Map WRITE_RECEIVERS = new ConcurrentHashMap<>(); + + private FieldDisplayNames() { + } + + /** + * Records that a field name ({@code this#.}) belongs to a static field, written + * {@code Class.field} + */ + public static void recordStaticField(String name) { + STATIC_FIELDS.add(name); + } + + /** + * Records that a field instance ({@code #this#._}) was created by a write through + * {@code receiver} ({@code receiver.field = v}), written {@code receiver.field}; an empty receiver writes the bare + * field name. Only the display changes + */ + public static void recordWriteReceiver(String instanceName, String receiver) { + WRITE_RECEIVERS.put(instanceName, receiver); + } + + /** + * Forgets what the previous verification recorded + */ + public static void clear() { + STATIC_FIELDS.clear(); + WRITE_RECEIVERS.clear(); + } + + static boolean isStaticField(String name) { + return STATIC_FIELDS.contains(name); + } + + static String writeReceiver(String instanceName) { + return WRITE_RECEIVERS.get(instanceName); + } +} 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 7a2571630..7ec4f1281 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 @@ -8,6 +8,8 @@ */ 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) { @@ -19,12 +21,15 @@ public static String format(String name) { Matcher matcher = INSTACE_VAR_PATTERN.matcher(name); if (!matcher.matches()) - return name; + return formatField(name); String baseName = matcher.group(1); String counter = matcher.group(2); + String receiver = FieldDisplayNames.writeReceiver(name); + if (receiver != null && isField(baseName)) + return (receiver.isEmpty() ? "" : receiver + ".") + fieldOf(baseName) + toSuperscript(counter); String prefix = isSpecialIdentifier(baseName) ? "#" : ""; - return prefix + baseName + toSuperscript(counter); + return prefix + formatField(baseName) + toSuperscript(counter); } public static String withoutInstance(String name) { @@ -32,6 +37,38 @@ public static String withoutInstance(String name) { return matcher.matches() ? matcher.group(1) : name; } + /** + * Whether a name is that of a field, {@code this#.}, possibly with an instance counter + */ + public static boolean isField(String name) { + return FIELD_PATTERN.matcher(withoutInstance(name)).matches(); + } + + /** + * Writes a field name as it is written in code: {@code this.field} for an instance field and {@code Class.field} + * for a static one, leaving any other name unchanged; the internal name keeps the declaring type to tell fields of + * different classes apart + */ + private static String formatField(String name) { + Matcher matcher = FIELD_PATTERN.matcher(name); + if (!matcher.matches()) + return name; + + if (FieldDisplayNames.isStaticField(name)) + return simpleTypeName(matcher.group(1)) + "." + matcher.group(2); + return "this." + matcher.group(2); + } + + private static String fieldOf(String name) { + Matcher matcher = FIELD_PATTERN.matcher(name); + return matcher.matches() ? matcher.group(2) : name; + } + + private static String simpleTypeName(String qualifiedName) { + int start = Math.max(qualifiedName.lastIndexOf('.'), qualifiedName.lastIndexOf('$')); + return qualifiedName.substring(start + 1); + } + private static String toSuperscript(String number) { StringBuilder sb = new StringBuilder(number.length()); for (char c : number.toCharArray()) { diff --git a/liquidjava-verifier/src/main/java/liquidjava/rj_language/opt/NeededVariables.java b/liquidjava-verifier/src/main/java/liquidjava/rj_language/opt/NeededVariables.java new file mode 100644 index 000000000..1c1680354 --- /dev/null +++ b/liquidjava-verifier/src/main/java/liquidjava/rj_language/opt/NeededVariables.java @@ -0,0 +1,103 @@ +package liquidjava.rj_language.opt; + +import static liquidjava.rj_language.opt.VCSimplificationUtils.isTrue; +import static liquidjava.rj_language.opt.VCSimplificationUtils.linkedConjuncts; +import static liquidjava.rj_language.opt.VCSimplificationUtils.splitConjuncts; +import static liquidjava.rj_language.opt.VCSimplificationUtils.termsOf; +import static liquidjava.rj_language.opt.VCSimplificationUtils.valueVariablesOf; +import static liquidjava.rj_language.opt.VCSimplificationUtils.variablesOf; + +import java.util.ArrayList; +import java.util.HashSet; +import java.util.List; +import java.util.Set; + +import liquidjava.processor.VCImplication; +import liquidjava.rj_language.Predicate; +import liquidjava.rj_language.ast.Expression; + +/** + * Decides which binders refined only by {@code true} a simplified VC chain keeps for an error. Such a binder states no + * fact, so it is kept only when a fact linked to the expected refinement (sharing a term with it, directly or through + * other facts) constrains its variable's value, or, when the error shows a counterexample, when expected itself + * constrains its value, so that the counterexample can show it + * + * @param expectedTerms + * variables and ghost applications of the expected refinement + * @param expectedValues + * variables whose value the expected refinement constrains + * @param keepExpected + * whether the binders of expectedValues are kept for that alone + */ +public record NeededVariables(Set expectedTerms, Set expectedValues, boolean keepExpected) { + + public static final NeededVariables NONE = new NeededVariables(Set.of(), Set.of(), false); + + public NeededVariables { + expectedTerms = Set.copyOf(expectedTerms); + expectedValues = Set.copyOf(expectedValues); + } + + /** + * For a refinement error, whose counterexample lists the values of the binders + */ + public static NeededVariables forRefinementError(Predicate expected) { + return of(expected, true); + } + + /** + * For a state refinement error, which has no counterexample + */ + public static NeededVariables forStateError(Predicate expected) { + return of(expected, false); + } + + private static NeededVariables of(Predicate expected, boolean keepExpected) { + Expression expression = expected.getExpression(); + return new NeededVariables(new HashSet<>(termsOf(expression)), new HashSet<>(valueVariablesOf(expression)), + keepExpected); + } + + /** + * Variables whose binder refined only by true the chain keeps: those whose own value a fact linked to expected + * constrains, and, when {@code keepExpected}, those whose value expected constrains + */ + public Set trueBindersToKeep(VCImplication chain) { + Set primitives = primitiveBinders(chain); + Set keep = new HashSet<>(); + for (Expression fact : linkedConjuncts(factsOf(chain), VCSimplificationUtils::termsOf, expectedTerms)) + for (String name : variablesOf(fact)) + if (!expectedTerms.contains(name) && hasOwnValue(name, fact, primitives)) + keep.add(name); + if (keepExpected) + for (String name : expectedTerms) + if (expectedValues.contains(name) || primitives.contains(name)) + keep.add(name); + return keep; + } + + /** + * Whether a fact constrains the variable's own value. A variable of an object type that the fact names only as the + * argument of a ghost or state application ({@code x} in {@code b == size(x)}) has no value of its own there, so + * its row would say nothing; a primitive argument ({@code k} in {@code y == f(k)}) has one + */ + private static boolean hasOwnValue(String name, Expression fact, Set primitives) { + return primitives.contains(name) || valueVariablesOf(fact).contains(name); + } + + private static List factsOf(VCImplication chain) { + List facts = new ArrayList<>(); + for (VCImplication current = chain; current != null; current = current.getNext()) + if (!isTrue(current.getRefinement().getExpression())) + facts.addAll(splitConjuncts(current.getRefinement().getExpression())); + return facts; + } + + private static Set primitiveBinders(VCImplication chain) { + Set primitives = new HashSet<>(); + for (VCImplication current = chain; current != null; current = current.getNext()) + if (current.hasBinder() && current.getType().isPrimitive()) + primitives.add(current.getName()); + return primitives; + } +} diff --git a/liquidjava-verifier/src/main/java/liquidjava/rj_language/opt/VCBinderOrdering.java b/liquidjava-verifier/src/main/java/liquidjava/rj_language/opt/VCBinderOrdering.java new file mode 100644 index 000000000..9c2a1e8c1 --- /dev/null +++ b/liquidjava-verifier/src/main/java/liquidjava/rj_language/opt/VCBinderOrdering.java @@ -0,0 +1,54 @@ +package liquidjava.rj_language.opt; + +import static liquidjava.rj_language.opt.VCSimplificationUtils.containsVar; +import static liquidjava.rj_language.opt.VCSimplificationUtils.copyWithRefinement; +import static liquidjava.rj_language.opt.VCSimplificationUtils.isTrue; + +import java.util.ArrayList; +import java.util.List; + +import liquidjava.processor.VCImplication; + +/** + * Moves a binder refined only by true that comes after an implication using its variable to just before that + * implication, so that each variable is introduced before it is used + */ +public class VCBinderOrdering implements VCSimplificationPass { + + /** + * Moves the first such binder of a VC chain + */ + @Override + public VCImplication apply(VCImplication implication) { + List nodes = new ArrayList<>(); + for (VCImplication current = implication; current != null; current = current.getNext()) + nodes.add(current); + + for (int i = 0; i < nodes.size(); i++) { + VCImplication binder = nodes.get(i); + if (!binder.hasBinder() || !isTrue(binder.getRefinement().getExpression())) + continue; + for (int j = 0; j < i; j++) { + if (containsVar(nodes.get(j).getRefinement().getExpression(), binder.getName())) { + nodes.add(j, nodes.remove(i)); + return relink(nodes); + } + } + } + return implication.clone(); + } + + private static VCImplication relink(List nodes) { + VCImplication first = null; + VCImplication last = null; + for (VCImplication node : nodes) { + VCImplication copy = copyWithRefinement(node, node.getRefinement().clone()); + if (first == null) + first = copy; + else + last.setNext(copy); + last = copy; + } + return first; + } +} diff --git a/liquidjava-verifier/src/main/java/liquidjava/rj_language/opt/VCBinderSimplification.java b/liquidjava-verifier/src/main/java/liquidjava/rj_language/opt/VCBinderSimplification.java index 6241b5b8d..3a2c42511 100644 --- a/liquidjava-verifier/src/main/java/liquidjava/rj_language/opt/VCBinderSimplification.java +++ b/liquidjava-verifier/src/main/java/liquidjava/rj_language/opt/VCBinderSimplification.java @@ -5,6 +5,8 @@ import static liquidjava.rj_language.opt.VCSimplificationUtils.isFalse; import static liquidjava.rj_language.opt.VCSimplificationUtils.isTrue; +import java.util.Set; + import liquidjava.processor.VCImplication; import liquidjava.rj_language.Predicate; import liquidjava.rj_language.ast.LiteralBoolean; @@ -18,30 +20,40 @@ public class VCBinderSimplification implements VCSimplificationPass { private static final String FRESH_PREFIX = Formats.FRESH_PREFIX; + private final NeededVariables needed; + + public VCBinderSimplification() { + this(NeededVariables.NONE); + } + + public VCBinderSimplification(NeededVariables needed) { + this.needed = needed; + } + /** * Applies one binder simplification in a VC chain */ @Override public VCImplication apply(VCImplication implication) { VCImplication cloned = implication.clone(); - VCImplication simplified = simplify(cloned); + VCImplication simplified = simplify(cloned, needed.trueBindersToKeep(cloned)); return simplified == null ? cloned : simplified; } /** * Simplifies the first applicable binder in a VC chain */ - private VCImplication simplify(VCImplication implication) { + private VCImplication simplify(VCImplication implication, Set keptTrueBinders) { if (implication == null) return null; if (isFalseBinder(implication)) return collapseFalseBinder(implication); - if (isRemovableUnusedBinder(implication)) + if (isRemovableBinder(implication, keptTrueBinders)) return removeBinder(implication); - VCImplication next = simplify(implication.getNext()); + VCImplication next = simplify(implication.getNext(), keptTrueBinders); if (next == null) return null; @@ -56,7 +68,7 @@ private VCImplication simplify(VCImplication implication) { private VCImplication removeBinder(VCImplication implication) { VCImplication next = implication.getNext(); - // ∀x. true => P -> P, and unused generated path conditions can be omitted from diagnostics + // ∀x. true => P -> P, and unneeded generated path conditions can be omitted from diagnostics if (next != null) return next.clone(); @@ -66,13 +78,17 @@ private VCImplication removeBinder(VCImplication implication) { } /** - * Checks whether a binder is unused and can be removed without changing the VC conclusion + * Checks whether a binder can be removed without changing the VC conclusion or hiding what explains the error. A + * binder refined only by true states no fact, so it is removed even when a later implication uses its variable, + * unless the error needs it */ - private boolean isRemovableUnusedBinder(VCImplication implication) { - if (!implication.hasBinder() || containsVar(implication.getNext(), implication.getName())) + private boolean isRemovableBinder(VCImplication implication, Set keptTrueBinders) { + if (!implication.hasBinder()) return false; - return isTrueBinder(implication) || isUnusedFreshPathBinder(implication); + if (isTrueBinder(implication)) + return !keptTrueBinders.contains(implication.getName()); + return !containsVar(implication.getNext(), implication.getName()) && isUnusedFreshPathBinder(implication); } /** diff --git a/liquidjava-verifier/src/main/java/liquidjava/rj_language/opt/VCSimplification.java b/liquidjava-verifier/src/main/java/liquidjava/rj_language/opt/VCSimplification.java index 70c79d575..7eb8d6dfb 100644 --- a/liquidjava-verifier/src/main/java/liquidjava/rj_language/opt/VCSimplification.java +++ b/liquidjava-verifier/src/main/java/liquidjava/rj_language/opt/VCSimplification.java @@ -10,21 +10,26 @@ */ public class VCSimplification { - private static final List PASSES = List.of(new VCSubstitution(), new VCFunctionSubstitution(), - new VCBinderSimplification(), new VCFolding(), new VCArithmeticSimplification(), - new VCLogicalSimplification(), new VCConstraintSimplification()); - /** * Applies all available simplification steps to a VC chain until a fixed point is reached */ public static VCSimplificationResult simplifyToFixedPoint(VCImplication implication) { + return simplifyToFixedPoint(implication, NeededVariables.NONE); + } + + /** + * Applies all available simplification steps to a VC chain until a fixed point is reached, keeping the binders of + * the needed variables + */ + public static VCSimplificationResult simplifyToFixedPoint(VCImplication implication, NeededVariables needed) { if (implication == null) return null; + List passes = passes(needed); DebugLog.simplificationStart(implication); VCSimplificationResult current = new VCSimplificationResult(implication); while (true) { - VCSimplificationResult simplified = simplifyOnce(current); + VCSimplificationResult simplified = simplifyOnce(current, passes); if (simplified == current) { DebugLog.simplificationEnd(current); return current; // fixed point reached @@ -37,7 +42,12 @@ public static VCSimplificationResult simplifyToFixedPoint(VCImplication implicat * Applies one simplification step to a VC chain from all available simplification passes */ public static VCSimplificationResult simplifyOnce(VCSimplificationResult implication) { - for (VCSimplificationPass pass : PASSES) { + return simplifyOnce(implication, passes(NeededVariables.NONE)); + } + + private static VCSimplificationResult simplifyOnce(VCSimplificationResult implication, + List passes) { + for (VCSimplificationPass pass : passes) { VCSimplificationResult simplified = simplifyOnce(implication, pass); if (simplified != implication) return simplified; @@ -45,6 +55,12 @@ public static VCSimplificationResult simplifyOnce(VCSimplificationResult implica return implication; } + private static List passes(NeededVariables needed) { + return List.of(new VCSubstitution(), new VCFunctionSubstitution(), new VCBinderSimplification(needed), + new VCFolding(), new VCArithmeticSimplification(), new VCLogicalSimplification(), + new VCConstraintSimplification(), new VCBinderOrdering()); + } + /** * Applies one selected simplification pass to a VC chain */ diff --git a/liquidjava-verifier/src/main/java/liquidjava/rj_language/opt/VCSimplificationUtils.java b/liquidjava-verifier/src/main/java/liquidjava/rj_language/opt/VCSimplificationUtils.java index 4ab153753..bb31fb783 100644 --- a/liquidjava-verifier/src/main/java/liquidjava/rj_language/opt/VCSimplificationUtils.java +++ b/liquidjava-verifier/src/main/java/liquidjava/rj_language/opt/VCSimplificationUtils.java @@ -1,12 +1,20 @@ package liquidjava.rj_language.opt; import java.util.ArrayList; +import java.util.Collection; +import java.util.HashSet; import java.util.List; +import java.util.Set; +import java.util.function.Function; import liquidjava.processor.VCImplication; import liquidjava.rj_language.Predicate; +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.UnaryExpression; +import liquidjava.rj_language.ast.Var; public final class VCSimplificationUtils { @@ -52,4 +60,103 @@ public static boolean isTrue(Expression expression) { public static boolean isFalse(Expression expression) { return expression instanceof LiteralBoolean literal && !literal.isBooleanTrue(); } + + /** + * Splits an expression into the facts it states together: the operands of {@code &&}, and of a negated disjunction + * {@code !(a || b)}, which states {@code !a} and {@code !b} + */ + public static List splitConjuncts(Expression expression) { + List conjuncts = new ArrayList<>(); + addConjuncts(expression, conjuncts); + return conjuncts; + } + + private static void addConjuncts(Expression expression, List conjuncts) { + Expression negated = negatedOperand(expression); + if (expression instanceof BinaryExpression binary && "&&".equals(binary.getOperator())) { + addConjuncts(binary.getFirstOperand(), conjuncts); + addConjuncts(binary.getSecondOperand(), conjuncts); + } else if (negated instanceof BinaryExpression binary && "||".equals(binary.getOperator())) { + addConjuncts(new UnaryExpression("!", binary.getFirstOperand()), conjuncts); + addConjuncts(new UnaryExpression("!", binary.getSecondOperand()), conjuncts); + } else if (negatedOperand(negated) != null) { + addConjuncts(negatedOperand(negated), conjuncts); + } else { + conjuncts.add(expression); + } + } + + // the operand of !e, or null for any other expression + private static Expression negatedOperand(Expression expression) { + return expression instanceof UnaryExpression not && "!".equals(not.getOp()) ? not.getExpression() : null; + } + + /** + * Returns the conjuncts linked to the seed terms: those sharing a term with the seed, directly or through other + * linked conjuncts. The remaining conjuncts only constrain values that the seed does not depend on + */ + public static List linkedConjuncts(List conjuncts, + Function> termsOf, Collection seed) { + Set linkedTerms = new HashSet<>(seed); + List linked = new ArrayList<>(); + List unlinked = new ArrayList<>(conjuncts); + boolean changed = true; + while (changed) { + changed = false; + for (Expression conjunct : List.copyOf(unlinked)) { + Collection terms = termsOf.apply(conjunct); + if (terms.stream().anyMatch(linkedTerms::contains)) { + linkedTerms.addAll(terms); + linked.add(conjunct); + unlinked.remove(conjunct); + changed = true; + } + } + } + return linked; + } + + /** + * Variable names of an expression + */ + public static List variablesOf(Expression expression) { + List names = new ArrayList<>(); + expression.getVariableNames(names); + return names; + } + + /** + * Terms an expression constrains: its variables and its ghost and state applications such as {@code size(x)} + */ + public static List termsOf(Expression expression) { + List terms = variablesOf(expression); + addApplications(expression, terms); + return terms; + } + + private static void addApplications(Expression expression, List terms) { + if (expression instanceof FunctionInvocation && !terms.contains(expression.toString())) + terms.add(expression.toString()); + for (Expression child : expression.getChildren()) + addApplications(child, terms); + } + + /** + * Variables whose own value an expression constrains: those outside the arguments of ghost and state applications. + * In {@code b == size(x)} that is {@code b}, while {@code x} only names the object whose size is meant + */ + public static List valueVariablesOf(Expression expression) { + List names = new ArrayList<>(); + addValueVariables(expression, names); + return names; + } + + private static void addValueVariables(Expression expression, List names) { + if (expression instanceof FunctionInvocation) + return; + if (expression instanceof Var var && !names.contains(var.getName())) + names.add(var.getName()); + for (Expression child : expression.getChildren()) + addValueVariables(child, names); + } } diff --git a/liquidjava-verifier/src/main/java/liquidjava/utils/Utils.java b/liquidjava-verifier/src/main/java/liquidjava/utils/Utils.java index 5e1d1fc43..b85809e02 100644 --- a/liquidjava-verifier/src/main/java/liquidjava/utils/Utils.java +++ b/liquidjava-verifier/src/main/java/liquidjava/utils/Utils.java @@ -3,19 +3,26 @@ import java.util.List; import java.util.Map; import java.util.Objects; +import java.util.Optional; import java.util.Scanner; import java.util.Set; import java.util.stream.Stream; +import liquidjava.rj_language.ast.formatter.FieldDisplayNames; import liquidjava.utils.constants.Types; +import spoon.reflect.code.CtAssignment; import spoon.reflect.code.CtBlock; +import spoon.reflect.code.CtExpression; import spoon.reflect.code.CtFieldAccess; +import spoon.reflect.code.CtFieldWrite; import spoon.reflect.code.CtFor; import spoon.reflect.code.CtForEach; import spoon.reflect.code.CtIf; import spoon.reflect.code.CtSuperAccess; import spoon.reflect.code.CtThisAccess; import spoon.reflect.code.CtTry; +import spoon.reflect.code.CtUnaryOperator; +import spoon.reflect.code.CtVariableRead; import spoon.reflect.code.CtWhile; import spoon.reflect.cu.SourcePosition; import spoon.reflect.declaration.CtAnnotation; @@ -55,10 +62,31 @@ public static String qualifyName(String prefix, String name) { return String.format("%s.%s", prefix, name); } + /** + * The context variable name of a field, {@code this#.}; also records a static field for + * display, since every field name of a verification is built here + */ public static String qualifyFieldName(CtFieldReference field) { if (field.getDeclaringType() == null) // declaring class not resolved: matches no known field return "this#" + field.getSimpleName(); - return "this#" + field.getDeclaringType().getQualifiedName() + "." + field.getSimpleName(); + String name = "this#" + field.getDeclaringType().getQualifiedName() + "." + field.getSimpleName(); + if (field.isStatic()) + FieldDisplayNames.recordStaticField(name); + return name; + } + + /** + * The object through which a write updates a field of another object ({@code other} in {@code other.f = v} or + * {@code other.f++}), used only to display that write; empty when the write is to a tracked field (see + * {@link #accessesTrackedField}) or not a field write, and an empty string when the object is not in a variable + */ + public static Optional untrackedWriteReceiver(CtElement usage) { + CtExpression written = usage instanceof CtAssignment assignment ? assignment.getAssigned() + : usage instanceof CtUnaryOperator unary ? unary.getOperand() : null; + if (!(written instanceof CtFieldWrite write) || accessesTrackedField(write)) + return Optional.empty(); + return Optional + .of(write.getTarget()instanceof CtVariableRead read ? read.getVariable().getSimpleName() : ""); } public static String getFile(CtElement element) { diff --git a/liquidjava-verifier/src/test/java/liquidjava/api/tests/TestFoundBinders.java b/liquidjava-verifier/src/test/java/liquidjava/api/tests/TestFoundBinders.java new file mode 100644 index 000000000..549cba700 --- /dev/null +++ b/liquidjava-verifier/src/test/java/liquidjava/api/tests/TestFoundBinders.java @@ -0,0 +1,103 @@ +package liquidjava.api.tests; + +import static org.junit.jupiter.api.Assertions.*; + +import java.util.ArrayList; +import java.util.List; +import java.util.Map; +import java.util.TreeMap; + +import org.junit.jupiter.api.BeforeAll; +import org.junit.jupiter.api.Test; + +import liquidjava.api.CommandLineLauncher; +import liquidjava.diagnostics.Diagnostics; +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.opt.VCSimplificationResult; + +/** + * Checks what Found shows for the errors of {@code classes/found_binders_error}, whose {@code // Expect:} lines also + * pin that writes to another object's field are accepted and rejected as on main + */ +class TestFoundBinders { + + private static final Map ERRORS = new TreeMap<>(); + + /** + * What the user is shown for an error, without the instance counters that depend on verification order: the + * simplified Found, the original Found the panel steps back to, the simplification of each step and the raw binder + * names of the original + */ + private record Shown(List rows, String message, String counterexample, List originalRows, + List steps, List originalBinders) { + } + + @BeforeAll + static void verify() { + // shown as the IDE gets it: right after the verification, before the next one starts + CommandLineLauncher.launch("../liquidjava-example/src/main/java/testSuite/classes/found_binders_error"); + for (LJError error : Diagnostics.getInstance().getErrors()) { + VCSimplificationResult found = assertInstanceOf(RefinementError.class, error).getFound(); + List steps = new ArrayList<>(); + VCSimplificationResult original = found; + for (; original.getOrigin() != null; original = original.getOrigin()) + 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)); + } + } + + @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()); + } + + @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("Substitution", "Binder"), shown.steps()); + assertEquals(List.of("this#testSuite.classes.found_binders_error.Basket.items", "#items_", "#bound_"), + shown.originalBinders()); + } + + @Test + void staticFieldIsWrittenWithItsClass() { + Shown shown = ERRORS.get(31); + assertEquals(List.of("∀Basket.served true", "∀count count == Basket.served + 1"), shown.rows()); + assertEquals("Counterexample: count == 0 && Basket.served == -1", shown.counterexample()); + } + + @Test + void writeToAnotherObjectsFieldIsNamedAfterThatObject() { + assertEquals("other.level == -1 is not a subtype of other.level >= 0", ERRORS.get(36).message()); + assertEquals(List.of("∀this.level this.level >= 0", "∀other.level other.level == this.level - 1"), + ERRORS.get(48).rows()); + } + + // the rows of Found as the IDE writes them: binder name, then its refinement + private static List rows(VCImplication found) { + 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)); + } + return rows; + } + + private static String plain(String text) { + return text.replaceAll("[⁰¹²³⁴⁵⁶⁷⁸⁹]", ""); + } +} 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 3fc91abea..848f70a5a 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 @@ -42,4 +42,13 @@ void keepsQualifiedNamesForDifferentInstances() { 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 + void writesFieldsAsInCodeNextToALocalOfTheSameName() { + Expression expression = Predicate + .createEquals(Predicate.createVar("#items_5"), Predicate.createVar("this#shop.Basket.items")) + .getExpression(); + + 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 f04d2c81d..508972c56 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 @@ -2,10 +2,16 @@ import static org.junit.jupiter.api.Assertions.assertEquals; +import org.junit.jupiter.api.AfterEach; import org.junit.jupiter.api.Test; class VariableFormatterTest { + @AfterEach + void forgetRecordedNames() { + FieldDisplayNames.clear(); + } + @Test void formatsVariables() { assertEquals("x", VariableFormatter.format("x")); @@ -22,4 +28,25 @@ void formatsVariables() { 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")); + } + + @Test + void writesStaticFieldsWithTheirClass() { + FieldDisplayNames.recordStaticField("this#pkg.Outer$Job.count"); + 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")); + FieldDisplayNames.clear(); + assertEquals("this.level¹", VariableFormatter.format("#this#pkg.W.level_1")); + } } diff --git a/liquidjava-verifier/src/test/java/liquidjava/rj_language/opt/VCBinderOrderingTest.java b/liquidjava-verifier/src/test/java/liquidjava/rj_language/opt/VCBinderOrderingTest.java new file mode 100644 index 000000000..adb272b0b --- /dev/null +++ b/liquidjava-verifier/src/test/java/liquidjava/rj_language/opt/VCBinderOrderingTest.java @@ -0,0 +1,18 @@ +package liquidjava.rj_language.opt; + +import static liquidjava.utils.VCTestUtils.*; +import static org.junit.jupiter.api.Assertions.assertEquals; + +import java.util.List; + +import org.junit.jupiter.api.Test; + +class VCBinderOrderingTest { + + @Test + void movesTrueBinderBeforeItsFirstUse() { + VCSimplificationResult result = assertSimplificationSteps(new VCBinderOrdering(), + vc("∀y:int. y < i", "∀i:int. true"), step("true", "y < i")); + assertEquals(List.of("i", "y"), result.getBinders()); + } +} 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 d3fbf3d04..5a0ee82a5 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 @@ -1,12 +1,28 @@ package liquidjava.rj_language.opt; import static liquidjava.utils.VCTestUtils.*; + import org.junit.jupiter.api.Test; +import liquidjava.rj_language.Predicate; +import liquidjava.rj_language.parsing.RefinementsParser; + class VCBinderSimplificationTest { private final VCBinderSimplification binderSimplification = new VCBinderSimplification(); + private static VCBinderSimplification forRefinementError(String expected) { + return new VCBinderSimplification(NeededVariables.forRefinementError(predicate(expected))); + } + + private static VCBinderSimplification forStateError(String expected) { + return new VCBinderSimplification(NeededVariables.forStateError(predicate(expected))); + } + + private static Predicate predicate(String refinement) { + return new Predicate(RefinementsParser.createAST(refinement, "")); + } + @Test void removesTrueBinderWhenVariableIsUnusedDownstream() { assertSimplificationSteps(binderSimplification, vc("∀x:int. true", "y > 0"), step("y > 0")); @@ -28,8 +44,51 @@ void keepsNonTrueTerminalBinderAsConclusion() { } @Test - void keepsTrueBinderWhenVariableIsUsedDownstream() { - assertSimplificationSteps(binderSimplification, vc("∀x:int. true", "x > 0"), step("true", "x > 0")); + void removesTrueBinderUsedDownstreamWhenNothingNeedsIt() { + assertSimplificationSteps(binderSimplification, vc("∀x:int. true", "x > 0"), step("x > 0")); + } + + @Test + void keepsTrueBinderLinkedToExpectedThroughALaterRow() { + assertSimplificationSteps(forRefinementError("y > 0"), vc("∀x:int. true", "∀y:int. y == x + 1"), + step("true", "y == x + 1")); + } + + @Test + void keepsTrueBinderLinkedToExpectedThroughSeveralRows() { + assertSimplificationSteps(forRefinementError("z > 0"), + vc("∀x:int. true", "∀y:int. y == x + 1", "∀z:int. z == y"), step("true", "y == x + 1", "z == y")); + } + + @Test + void removesTrueBindersOnlyAnUnlinkedGuardUses() { + // one guard !(p || t < 0) states !p and !(t < 0) apart, so only the second is linked to t + assertSimplificationSteps(forRefinementError("t > 0"), + vc("∀port:int. true", "∀p:boolean. true", "!(port < 0)", "!(p || t < 0)", "∀t:int. true"), + step("true", "!(port < 0)", "!(p || t < 0)", "true"), step("!(port < 0)", "!(p || t < 0)", "true")); + } + + @Test + void keepsTrueBinderOfExpectedVariableInRefinementError() { + assertSimplificationSteps(forRefinementError("x > 0"), vc("∀x:int. true", "y > 0"), step("true", "y > 0")); + } + + @Test + void removesTrueBinderOfExpectedVariableInStateError() { + assertSimplificationSteps(forStateError("x > 0"), vc("∀x:int. true", "y > 0"), step("y > 0")); + } + + @Test + void keepsPrimitiveTrueBinderThatIsTheArgumentOfAGhost() { + assertSimplificationSteps(forRefinementError("y > 0"), vc("∀k:int. true", "∀y:int. y == f(k)"), + step("true", "y == f(k)")); + } + + @Test + void linksThroughGhostApplicationsButKeepsOnlyValueVariables() { + assertSimplificationSteps(forStateError("open(f)"), + vc("∀ready:boolean. true", "∀f:Object. true", "ready ? open(f) : created(f)"), + step("true", "ready ? open(f) : created(f)")); } @Test @@ -45,7 +104,7 @@ void simplifiesOnlyFirstApplicableBinder() { @Test void skipsInapplicableTrueBinderAndSimplifiesLaterBinder() { - assertSimplificationSteps(binderSimplification, vc("∀x:int. true", "x > 0", "∀y:int. true", "z > 0"), + assertSimplificationSteps(forRefinementError("x > 0"), vc("∀x:int. true", "x > 0", "∀y:int. true", "z > 0"), step("true", "x > 0", "z > 0")); } diff --git a/liquidjava-verifier/src/test/java/liquidjava/utils/VCTestUtils.java b/liquidjava-verifier/src/test/java/liquidjava/utils/VCTestUtils.java index d952f814a..2a039e253 100644 --- a/liquidjava-verifier/src/test/java/liquidjava/utils/VCTestUtils.java +++ b/liquidjava-verifier/src/test/java/liquidjava/utils/VCTestUtils.java @@ -88,7 +88,7 @@ private static VCImplication parseImplication(String implication) { if (!implication.startsWith("∀")) return new VCImplication(new Predicate(RefinementsParser.createAST(implication, ""))); - int refinementStart = implication.indexOf('.'); + int refinementStart = implication.indexOf('.', implication.indexOf(':')); // binder names may have dots String binder = implication.substring(1, refinementStart).trim(); String refinement = implication.substring(refinementStart + 1).trim(); String[] parts = binder.split(":"); @@ -101,6 +101,8 @@ private static CtTypeReference type(String name) { return TYPE_FACTORY.INTEGER_PRIMITIVE; if ("boolean".equals(name)) return TYPE_FACTORY.BOOLEAN_PRIMITIVE; + if ("Object".equals(name)) + return TYPE_FACTORY.OBJECT; throw new IllegalArgumentException("Unsupported test type: " + name); }