From c3df13c8f347ce3f50be74e239fbf3ce448de20a Mon Sep 17 00:00:00 2001 From: Catarina Gamboa Date: Mon, 2 Nov 2026 17:24:02 +0000 Subject: [PATCH 1/5] Drop true binders that the error does not need and write fields as in code A binder refined only by true now stays in Found only when Expected mentions its variable, or a later row uses it and the counterexample gives it a value. Field variables this#pkg.Class.field are displayed as this.field (Class.field when static) in messages, Found rows and counterexamples; their internal names are unchanged. Fixes #457 Co-Authored-By: Claude Opus 5.5 --- .../InterruptManager.java | 16 ++ .../VectorRefinements.java | 21 +++ .../ArrayListRefinements.java | 15 ++ .../found_true_binders_error/Basket.java | 99 +++++++++++ .../RandomRefinements.java | 12 ++ .../liquidjava/api/CommandLineLauncher.java | 2 + .../liquidjava/processor/VCImplication.java | 5 + .../refinement_checker/VCChecker.java | 12 +- .../ast/formatter/ExpressionNameResolver.java | 4 + .../ast/formatter/VariableFormatter.java | 65 ++++++- .../rj_language/opt/NeededVariables.java | 38 +++++ .../opt/VCBinderSimplification.java | 27 ++- .../rj_language/opt/VCSimplification.java | 28 ++- .../src/main/java/liquidjava/utils/Utils.java | 6 +- .../api/tests/TestFoundBinders.java | 159 ++++++++++++++++++ .../formatter/ExpressionNameResolverTest.java | 26 +++ .../ast/formatter/VariableFormatterTest.java | 51 ++++++ .../opt/VCBinderSimplificationTest.java | 75 ++++++++- .../java/liquidjava/utils/VCTestUtils.java | 2 +- 19 files changed, 638 insertions(+), 25 deletions(-) create mode 100644 liquidjava-example/src/main/java/testSuite/classes/found_field_state_error/InterruptManager.java create mode 100644 liquidjava-example/src/main/java/testSuite/classes/found_field_state_error/VectorRefinements.java create mode 100644 liquidjava-example/src/main/java/testSuite/classes/found_true_binders_error/ArrayListRefinements.java create mode 100644 liquidjava-example/src/main/java/testSuite/classes/found_true_binders_error/Basket.java create mode 100644 liquidjava-example/src/main/java/testSuite/classes/found_true_binders_error/RandomRefinements.java create mode 100644 liquidjava-verifier/src/main/java/liquidjava/rj_language/opt/NeededVariables.java create mode 100644 liquidjava-verifier/src/test/java/liquidjava/api/tests/TestFoundBinders.java diff --git a/liquidjava-example/src/main/java/testSuite/classes/found_field_state_error/InterruptManager.java b/liquidjava-example/src/main/java/testSuite/classes/found_field_state_error/InterruptManager.java new file mode 100644 index 000000000..45ac9ffe7 --- /dev/null +++ b/liquidjava-example/src/main/java/testSuite/classes/found_field_state_error/InterruptManager.java @@ -0,0 +1,16 @@ +package testSuite.classes.found_field_state_error; + +import java.util.Vector; + +// the field's row holds its state, so Found keeps it under its source name (#457) +public class InterruptManager { + private Vector interrupts; + + public void initialize(int intrNumber) { + interrupts = new Vector(67); + if (intrNumber < 0 || intrNumber >= 67) { + return; + } + String handlers = interrupts.get(intrNumber); // Expect: State Refinement Error + } +} diff --git a/liquidjava-example/src/main/java/testSuite/classes/found_field_state_error/VectorRefinements.java b/liquidjava-example/src/main/java/testSuite/classes/found_field_state_error/VectorRefinements.java new file mode 100644 index 000000000..5029cee43 --- /dev/null +++ b/liquidjava-example/src/main/java/testSuite/classes/found_field_state_error/VectorRefinements.java @@ -0,0 +1,21 @@ +package testSuite.classes.found_field_state_error; + +import liquidjava.specification.ExternalRefinementsFor; +import liquidjava.specification.Refinement; +import liquidjava.specification.StateRefinement; +import liquidjava.specification.StateSet; + +@ExternalRefinementsFor("java.util.Vector") +@StateSet({"empty", "maybeElements"}) +public interface VectorRefinements { + + @StateRefinement(to = "empty(this)") + public void Vector(@Refinement("_ >= 0") int initialCapacity); + + @StateRefinement(from = "empty(this)", to = "maybeElements(this)") + @StateRefinement(from = "maybeElements(this)") + public boolean add(E e); + + @StateRefinement(from = "maybeElements(this)") + public E get(@Refinement("_ >= 0") int index); +} diff --git a/liquidjava-example/src/main/java/testSuite/classes/found_true_binders_error/ArrayListRefinements.java b/liquidjava-example/src/main/java/testSuite/classes/found_true_binders_error/ArrayListRefinements.java new file mode 100644 index 000000000..b3b969708 --- /dev/null +++ b/liquidjava-example/src/main/java/testSuite/classes/found_true_binders_error/ArrayListRefinements.java @@ -0,0 +1,15 @@ +package testSuite.classes.found_true_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_true_binders_error/Basket.java b/liquidjava-example/src/main/java/testSuite/classes/found_true_binders_error/Basket.java new file mode 100644 index 000000000..24fbb357c --- /dev/null +++ b/liquidjava-example/src/main/java/testSuite/classes/found_true_binders_error/Basket.java @@ -0,0 +1,99 @@ +package testSuite.classes.found_true_binders_error; + +import java.util.ArrayList; +import java.util.Random; + +import liquidjava.specification.Refinement; + +// Found keeps a binder refined only by true when the error needs it (#457) +public class Basket { + static int served; + + private final ArrayList items; + private final ArrayList extras; + private final Random random = new Random(); + int amount; + + Basket(ArrayList items, ArrayList extras) { + this.items = items; + this.extras = extras; + } + + // 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 parameter refined only by true + String pickFrom(ArrayList list) { + return list.get(random.nextInt(list.size())); // Expect: Refinement Error + } + + // a call result refined only by true + String pickCopy() { + ArrayList copy = copyItems(); + return copy.get(random.nextInt(copy.size())); // Expect: Refinement Error + } + + ArrayList copyItems() { + return new ArrayList<>(items); + } + + // a local refined only by true: the loop may have reassigned it + String pickLocal(ArrayList list) { + ArrayList local = list; + for (String name : list) { + local = list; + } + return local.get(random.nextInt(local.size())); // Expect: Refinement Error + } + + // several fields, read with and without this + int pickAny() { + int first = this.items.size(); + int second = extras.size(); + return random.nextInt(first + second); // Expect: Refinement Error + } + + // a later row uses the parameter and the counterexample has a value for it + void next(int x) { + @Refinement("_ > 0") + int y = x + 1; // Expect: Refinement Error + } + + // the expected refinement is about the parameter + void forward(int x, int unrelated) { + positive(x); // Expect: Refinement Error + } + + void positive(@Refinement("_ > 0") int v) { + } + + // a static field + void serve() { + @Refinement("_ > 0") + int count = served + 1; // Expect: Refinement Error + } + + // an instance field read with this + void withThis() { + @Refinement("_ > 0") + int a = this.amount; // Expect: Refinement Error + } + + // the same field read without this + void withoutThis() { + @Refinement("_ > 0") + int a = amount; // Expect: Refinement Error + } + + class Shelf { + ArrayList names; + + // a field of an inner class + String pick() { + return names.get(new Random().nextInt(names.size())); // Expect: Refinement Error + } + } +} diff --git a/liquidjava-example/src/main/java/testSuite/classes/found_true_binders_error/RandomRefinements.java b/liquidjava-example/src/main/java/testSuite/classes/found_true_binders_error/RandomRefinements.java new file mode 100644 index 000000000..b9be38c8d --- /dev/null +++ b/liquidjava-example/src/main/java/testSuite/classes/found_true_binders_error/RandomRefinements.java @@ -0,0 +1,12 @@ +package testSuite.classes.found_true_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..5590ae65f 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.VariableFormatter; import liquidjava.specification.Refinement; import picocli.CommandLine; import spoon.Launcher; @@ -57,6 +58,7 @@ public static void launch(String... paths) { diagnostics.clear(); contextHistory.clearHistory(); + VariableFormatter.clearStaticFields(); 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/VCChecker.java b/liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/VCChecker.java index 819e4b6a2..43f8c5ba3 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.of(expectedType, result.getCounterexample())), 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.of(expected, counterexample)), map, counterexample, customMessage); } protected void throwStateRefinementError(SourcePosition position, SourcePosition declarationPosition, @@ -451,8 +453,8 @@ 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.of(expected, null)), 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..77fb6990b 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,10 @@ public static ExpressionNameResolver forExpression(Expression expression) { public String resolveVariable(String name) { String formatted = VariableFormatter.format(name); + // a field is always written as in code, and with its class only when another field is written the same way + if (VariableFormatter.isField(name)) + return isAmbiguous(name, variables, VariableFormatter::format) ? VariableFormatter.formatWithOwner(name) + : formatted; return isAmbiguous(name, variables, ExpressionNameResolver::getVariableSimpleName) ? formatted : Utils.getSimpleName(formatted); } diff --git a/liquidjava-verifier/src/main/java/liquidjava/rj_language/ast/formatter/VariableFormatter.java b/liquidjava-verifier/src/main/java/liquidjava/rj_language/ast/formatter/VariableFormatter.java index 7a2571630..3cc1cdb64 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,5 +1,7 @@ package liquidjava.rj_language.ast.formatter; +import java.util.Set; +import java.util.concurrent.ConcurrentHashMap; import java.util.regex.Matcher; import java.util.regex.Pattern; @@ -9,8 +11,22 @@ public final class VariableFormatter { private static final Pattern INSTACE_VAR_PATTERN = Pattern.compile("^#(.+)_([0-9]+)$"); private static final char[] SUPERSCRIPT_CHARS = { '⁰', '¹', '²', '³', '⁴', '⁵', '⁶', '⁷', '⁸', '⁹' }; + private static final String FIELD_PREFIX = "this#"; + private static final Set STATIC_FIELDS = ConcurrentHashMap.newKeySet(); public static String format(String name) { + return format(name, false); + } + + /** + * Formats a name like {@link #format(String)}, but writes an instance field with its declaring class + * ({@code Basket.this.items}) to tell it apart from a field with the same name in another class + */ + public static String formatWithOwner(String name) { + return format(name, true); + } + + private static String format(String name, boolean withOwner) { if (name == null) return null; @@ -19,12 +35,12 @@ public static String format(String name) { Matcher matcher = INSTACE_VAR_PATTERN.matcher(name); if (!matcher.matches()) - return name; + return formatField(name, withOwner); String baseName = matcher.group(1); String counter = matcher.group(2); String prefix = isSpecialIdentifier(baseName) ? "#" : ""; - return prefix + baseName + toSuperscript(counter); + return prefix + formatField(baseName, withOwner) + toSuperscript(counter); } public static String withoutInstance(String name) { @@ -32,6 +48,51 @@ 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) { + String baseName = withoutInstance(name); + return baseName.startsWith(FIELD_PREFIX) && baseName.indexOf('.', FIELD_PREFIX.length()) > 0; + } + + /** + * Records that a field name ({@code this#.}) belongs to a static field, which is then + * displayed as {@code Class.field} instead of {@code this.field} + */ + public static void registerStaticField(String name) { + STATIC_FIELDS.add(name); + } + + /** + * Forgets the static fields recorded by the previous verification + */ + public static void clearStaticFields() { + STATIC_FIELDS.clear(); + } + + /** + * 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, boolean withOwner) { + if (!isField(name)) + return name; + + int fieldStart = name.lastIndexOf('.'); + String field = name.substring(fieldStart + 1); + String owner = simpleTypeName(name.substring(FIELD_PREFIX.length(), fieldStart)); + if (STATIC_FIELDS.contains(name)) + return owner + "." + field; + return (withOwner ? owner + ".this." : "this.") + field; + } + + 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..95073fc57 --- /dev/null +++ b/liquidjava-verifier/src/main/java/liquidjava/rj_language/opt/NeededVariables.java @@ -0,0 +1,38 @@ +package liquidjava.rj_language.opt; + +import java.util.HashSet; +import java.util.Set; + +import liquidjava.rj_language.Predicate; +import liquidjava.smt.Counterexample; +import liquidjava.utils.Pair; + +/** + * Variables that a simplified VC chain must keep a binder for even when the binder only says {@code true}: those of the + * expected refinement, and those that the counterexample gives a value + */ +public record NeededVariables(Set expected, Set assigned) { + + public static final NeededVariables NONE = new NeededVariables(Set.of(), Set.of()); + + public NeededVariables { + expected = Set.copyOf(expected); + assigned = Set.copyOf(assigned); + } + + public static NeededVariables of(Predicate expected, Counterexample counterexample) { + Set expectedNames = expected == null ? Set.of() : new HashSet<>(expected.getVariableNames()); + Set assignedNames = new HashSet<>(); + if (counterexample != null) + counterexample.assignments().stream().map(Pair::first).forEach(assignedNames::add); + return new NeededVariables(expectedNames, assignedNames); + } + + /** + * Whether a binder refined only by {@code true} must stay: the expected refinement is about its variable, or a + * later implication uses it and the counterexample has a value for it + */ + public boolean needsTrueBinder(String name, boolean usedDownstream) { + return expected.contains(name) || usedDownstream && assigned.contains(name); + } +} 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..f28120dbb 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 @@ -18,6 +18,16 @@ 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 */ @@ -38,7 +48,7 @@ private VCImplication simplify(VCImplication implication) { if (isFalseBinder(implication)) return collapseFalseBinder(implication); - if (isRemovableUnusedBinder(implication)) + if (isRemovableBinder(implication)) return removeBinder(implication); VCImplication next = simplify(implication.getNext()); @@ -56,7 +66,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 +76,18 @@ 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) { + if (!implication.hasBinder()) return false; - return isTrueBinder(implication) || isUnusedFreshPathBinder(implication); + boolean usedDownstream = containsVar(implication.getNext(), implication.getName()); + if (isTrueBinder(implication)) + return !needed.needsTrueBinder(implication.getName(), usedDownstream); + return !usedDownstream && 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..82705505e 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()); + } + /** * Applies one selected simplification pass to a VC chain */ diff --git a/liquidjava-verifier/src/main/java/liquidjava/utils/Utils.java b/liquidjava-verifier/src/main/java/liquidjava/utils/Utils.java index 5e1d1fc43..8d94b584d 100644 --- a/liquidjava-verifier/src/main/java/liquidjava/utils/Utils.java +++ b/liquidjava-verifier/src/main/java/liquidjava/utils/Utils.java @@ -7,6 +7,7 @@ import java.util.Set; import java.util.stream.Stream; +import liquidjava.rj_language.ast.formatter.VariableFormatter; import liquidjava.utils.constants.Types; import spoon.reflect.code.CtBlock; import spoon.reflect.code.CtFieldAccess; @@ -58,7 +59,10 @@ public static String qualifyName(String prefix, String name) { 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()) + VariableFormatter.registerStaticField(name); + return name; } 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..472a8f1d7 --- /dev/null +++ b/liquidjava-verifier/src/test/java/liquidjava/api/tests/TestFoundBinders.java @@ -0,0 +1,159 @@ +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.diagnostics.errors.StateRefinementError; +import liquidjava.processor.VCImplication; +import liquidjava.rj_language.ast.formatter.VariableFormatter; + +/** + * Checks the rows of Found: a binder refined only by true is shown only when the error needs it, and fields are written + * as in code + */ +class TestFoundBinders { + + private static final String TEST_SUITE = "../liquidjava-example/src/main/java/testSuite/"; + + private static Map basket; + private static Map fieldState; + + /** What the user is shown for an error, without the instance counters that depend on verification order */ + private record Shown(List rows, String message, String counterexample) { + } + + @BeforeAll + static void verify() { + // shown as the IDE gets it: right after the verification, before the next one starts + basket = verify("classes/found_true_binders_error"); + fieldState = verify("classes/found_field_state_error"); + } + + @Test + void basketHasOneErrorPerCase() { + assertEquals(List.of(25, 30, 36, 49, 56, 62, 67, 76, 82, 88, 96), new ArrayList<>(basket.keySet())); + } + + @Test + void trueFieldRowOfTheIssueIsDropped() { + Shown shown = basket.get(25); + assertEquals(List.of("∀bound bound == size(this.items) && bound >= 0"), shown.rows()); + assertEquals("bound == size(this.items) && bound >= 0 is not a subtype of bound > 0", shown.message()); + assertEquals("Counterexample: bound == 0", shown.counterexample()); + } + + @Test + void trueParameterRowIsDropped() { + assertEquals(List.of("∀bound bound == size(list) && bound >= 0"), basket.get(30).rows()); + } + + @Test + void trueCallResultRowIsDropped() { + assertEquals(List.of("∀bound bound == size(copyItems) && bound >= 0"), basket.get(36).rows()); + } + + @Test + void trueLocalRowIsDropped() { + assertEquals(List.of("∀bound bound == size(local) && bound >= 0"), basket.get(49).rows()); + } + + @Test + void severalTrueFieldRowsAreDroppedAndReadWithOrWithoutThisAlike() { + assertEquals( + List.of("∀first first == size(this.items) && first >= 0", + "∀second second == size(this.extras) && second >= 0", "∀bound bound == first + second"), + basket.get(56).rows()); + } + + @Test + void trueRowUsedLaterIsKeptWhenTheCounterexampleHasItsValue() { + Shown shown = basket.get(62); + assertEquals(List.of("∀x true", "∀y y == x + 1"), shown.rows()); + assertEquals("Counterexample: x == -1 && y == 0", shown.counterexample()); + } + + @Test + void trueRowOfTheExpectedVariableIsKept() { + Shown shown = basket.get(67); + assertEquals(List.of("∀x true"), shown.rows()); + assertEquals("true is not a subtype of x > 0", shown.message()); + } + + @Test + void staticFieldIsWrittenWithItsClass() { + Shown shown = basket.get(76); + assertEquals(List.of("∀Basket.served true", "∀count count == Basket.served + 1"), shown.rows()); + assertEquals("count == Basket.served + 1 is not a subtype of count > 0", shown.message()); + assertEquals("Counterexample: Basket.served == -1 && count == 0", shown.counterexample()); + } + + @Test + void fieldReadWithThisIsWrittenAsInCode() { + Shown shown = basket.get(82); + assertEquals(List.of("∀this.amount true", "∀a a == this.amount"), shown.rows()); + assertEquals("a == this.amount is not a subtype of a > 0", shown.message()); + assertEquals("Counterexample: this.amount == 0 && a == 0", shown.counterexample()); + } + + @Test + void fieldReadWithoutThisIsWrittenTheSameWay() { + assertEquals(basket.get(82), basket.get(88)); + } + + @Test + void fieldOfAnInnerClassIsWrittenAsInCode() { + assertEquals(List.of("∀bound bound == size(this.names) && bound >= 0"), basket.get(96).rows()); + } + + @Test + void fieldRowHoldingAStateIsKept() { + assertEquals(List.of(14), new ArrayList<>(fieldState.keySet())); + Shown shown = fieldState.get(14); + assertEquals( + List.of("∀#fresh !(intrNumber < 0 || intrNumber >= 67)", "∀this.interrupts empty(this.interrupts)"), + shown.rows()); + assertEquals("found !(intrNumber < 0 || intrNumber >= 67) && empty(this.interrupts) but expected " + + "maybeElements(this.interrupts)", shown.message()); + } + + private static Map verify(String test) { + CommandLineLauncher.launch(TEST_SUITE + test); + Map shown = new TreeMap<>(); + for (LJError error : Diagnostics.getInstance().getErrors()) + shown.put(error.getPosition().getLine(), new Shown(rows(error), plain(error.getMessage()), + error.getCounterexampleStr() == null ? null : plain(error.getCounterexampleStr()))); + return shown; + } + + // the rows of Found as the IDE writes them: binder name, then its refinement + private static List rows(LJError error) { + VCImplication found; + if (error instanceof RefinementError refinementError) + found = refinementError.getFound().getImplication(); + else + found = assertInstanceOf(StateRefinementError.class, error).getFound(); + + 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..e2c907775 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,30 @@ 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()); + } + + @Test + void writesFieldsAsInCodeInsideFunctionArguments() { + Predicate size = Predicate.createInvocation("java.util.ArrayList.size", + Predicate.createVar("this#shop.Basket.items")); + Expression expression = Predicate.createEquals(Predicate.createVar("#bound_6"), size).getExpression(); + + assertEquals("bound⁶ == size(this.items)", expression.toDisplayString()); + } + + @Test + void writesTheClassOfFieldsWithTheSameName() { + Expression expression = Predicate.createEquals(Predicate.createVar("this#shop.Basket.count"), + Predicate.createVar("this#shop.Shelf.count")).getExpression(); + + assertEquals("Basket.this.count == Shelf.this.count", 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..78a7537e0 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 @@ -1,11 +1,19 @@ package liquidjava.rj_language.ast.formatter; import static org.junit.jupiter.api.Assertions.assertEquals; +import static org.junit.jupiter.api.Assertions.assertFalse; +import static org.junit.jupiter.api.Assertions.assertTrue; +import org.junit.jupiter.api.AfterEach; import org.junit.jupiter.api.Test; class VariableFormatterTest { + @AfterEach + void forgetStaticFields() { + VariableFormatter.clearStaticFields(); + } + @Test void formatsVariables() { assertEquals("x", VariableFormatter.format("x")); @@ -22,4 +30,47 @@ 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.items", VariableFormatter.format("this#Basket.items")); + assertEquals("this.interrupts⁴⁷⁵", VariableFormatter + .format("#this#x_e_oss_a1_17_interruptmanager.E_OSS_A1_17_InterruptManager.interrupts_475")); + assertEquals("this.port", VariableFormatter.format("this#pkg.Outer$Job.port")); + } + + @Test + void writesStaticFieldsWithTheirClass() { + VariableFormatter.registerStaticField("this#shop.Basket.served"); + VariableFormatter.registerStaticField("this#pkg.Outer$Job.count"); + assertEquals("Basket.served", VariableFormatter.format("this#shop.Basket.served")); + assertEquals("Basket.served³", VariableFormatter.format("#this#shop.Basket.served_3")); + assertEquals("Job.count", VariableFormatter.format("this#pkg.Outer$Job.count")); + assertEquals("this.items", VariableFormatter.format("this#shop.Basket.items")); + } + + @Test + void forgetsStaticFieldsOfThePreviousVerification() { + VariableFormatter.registerStaticField("this#shop.Basket.served"); + VariableFormatter.clearStaticFields(); + assertEquals("this.served", VariableFormatter.format("this#shop.Basket.served")); + } + + @Test + void writesFieldsWithTheirOwnerOnRequest() { + assertEquals("Basket.this.items", VariableFormatter.formatWithOwner("this#shop.Basket.items")); + assertEquals("Job.this.port²", VariableFormatter.formatWithOwner("#this#pkg.Outer$Job.port_2")); + assertEquals("x²", VariableFormatter.formatWithOwner("#x_2")); + } + + @Test + void recognisesFieldNames() { + assertTrue(VariableFormatter.isField("this#shop.Basket.items")); + assertTrue(VariableFormatter.isField("#this#shop.Basket.items_4")); + assertFalse(VariableFormatter.isField("this#Basket")); + assertFalse(VariableFormatter.isField("#this_4")); + assertFalse(VariableFormatter.isField("items")); + assertFalse(VariableFormatter.isField("java.util.ArrayList.size")); + } } 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..e8d1ca56b 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,31 @@ package liquidjava.rj_language.opt; import static liquidjava.utils.VCTestUtils.*; +import static org.junit.jupiter.api.Assertions.assertEquals; + +import java.util.List; +import java.util.Set; + import org.junit.jupiter.api.Test; +import liquidjava.processor.VCImplication; +import liquidjava.rj_language.Predicate; +import liquidjava.rj_language.parsing.RefinementsParser; +import liquidjava.smt.Counterexample; +import liquidjava.utils.Pair; +import spoon.Launcher; +import spoon.reflect.factory.TypeFactory; + class VCBinderSimplificationTest { private final VCBinderSimplification binderSimplification = new VCBinderSimplification(); + private static final TypeFactory TYPES = new Launcher().getFactory().Type(); + + private static VCBinderSimplification binderWithNeeds(Set expected, Set assigned) { + return new VCBinderSimplification(new NeededVariables(expected, assigned)); + } + @Test void removesTrueBinderWhenVariableIsUnusedDownstream() { assertSimplificationSteps(binderSimplification, vc("∀x:int. true", "y > 0"), step("y > 0")); @@ -28,8 +47,56 @@ 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 removesTrueFieldBinderUsedDownstreamWhenNothingNeedsIt() { + VCImplication field = new VCImplication("this#shop.Basket.items", TYPES.INTEGER_PRIMITIVE, new Predicate()); + field.setNext(new VCImplication("#bound_6", TYPES.INTEGER_PRIMITIVE, + Predicate.createEquals(Predicate.createVar("#bound_6"), Predicate.createOperation( + Predicate.createVar("this#shop.Basket.items"), "+", Predicate.createLit("1", "int"))))); + assertSimplificationSteps(binderSimplification, field, step("bound⁶ == this.items + 1")); + } + + @Test + void keepsTrueBinderUsedDownstreamWhenCounterexampleAssignsIt() { + assertSimplificationSteps(binderWithNeeds(Set.of(), Set.of("x")), vc("∀x:int. true", "x > 0"), + step("true", "x > 0")); + } + + @Test + void removesTrueBinderAssignedByCounterexampleWhenUnusedDownstream() { + assertSimplificationSteps(binderWithNeeds(Set.of(), Set.of("x")), vc("∀x:int. true", "y > 0"), step("y > 0")); + } + + @Test + void keepsTrueBinderOfExpectedVariable() { + assertSimplificationSteps(binderWithNeeds(Set.of("x"), Set.of()), vc("∀x:int. true", "y > 0"), + step("true", "y > 0")); + } + + @Test + void keepsTerminalTrueBinderOfExpectedVariable() { + VCSimplificationResult result = assertSimplificationSteps(binderWithNeeds(Set.of("x"), Set.of()), + vc("∀x:int. true"), step("true")); + assertEquals(List.of("x"), result.getBinders()); + } + + @Test + void removesOnlyTheTrueBindersNothingNeeds() { + assertSimplificationSteps(binderWithNeeds(Set.of("e"), Set.of("c")), + vc("∀a:int. true", "∀c:int. true", "∀e:int. true", "∀y:int. y == a + c", "y > e"), + step("true", "true", "y == a + c", "y > e")); + } + + @Test + void neededVariablesComeFromExpectedAndCounterexample() { + NeededVariables needed = NeededVariables.of(new Predicate(RefinementsParser.createAST("x > y", "")), + new Counterexample(List.of(new Pair<>("z", "0")))); + assertEquals(Set.of("x", "y"), needed.expected()); + assertEquals(Set.of("z"), needed.assigned()); } @Test @@ -45,8 +112,8 @@ void simplifiesOnlyFirstApplicableBinder() { @Test void skipsInapplicableTrueBinderAndSimplifiesLaterBinder() { - assertSimplificationSteps(binderSimplification, vc("∀x:int. true", "x > 0", "∀y:int. true", "z > 0"), - step("true", "x > 0", "z > 0")); + assertSimplificationSteps(binderWithNeeds(Set.of(), Set.of("x")), + vc("∀x:int. true", "x > 0", "∀y:int. true", "z > 0"), step("true", "x > 0", "z > 0")); } @Test diff --git a/liquidjava-verifier/src/test/java/liquidjava/utils/VCTestUtils.java b/liquidjava-verifier/src/test/java/liquidjava/utils/VCTestUtils.java index d952f814a..019dd76cb 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(":"); From 01590749144e7acc0c3d6f2ec3c3e14ea6234e7f Mon Sep 17 00:00:00 2001 From: Catarina Gamboa Date: Tue, 3 Nov 2026 12:49:54 +0000 Subject: [PATCH 2/5] Keep a true binder only when it is linked to Expected, and name writes to other objects' fields after them A binder refined only by true now stays in Found when a fact linked to Expected (sharing a variable or ghost application, directly or through other facts, with negated disjunctions split first) constrains its value, or, in a refinement error, when Expected constrains it. The rule no longer depends on the counterexample, so it is the same for refinement and state errors. A kept true binder moves before the first row that uses it. A write to another object's field is checked under that object's name (other.level) instead of this.level. The class-based disambiguation of fields is removed. Co-Authored-By: Claude Opus 5.5 --- .../testSuite/ErrorOtherObjectFieldWrite.java | 21 ++++ .../found_true_binders_error/Basket.java | 21 ++++ .../RefinementTypeChecker.java | 2 +- .../refinement_checker/VCChecker.java | 7 +- .../general_checkers/OperationsChecker.java | 4 +- .../object_checkers/AuxStateHandler.java | 2 +- .../ast/formatter/ExpressionNameResolver.java | 5 +- .../ast/formatter/VariableFormatter.java | 47 +++----- .../rj_language/opt/NeededVariables.java | 77 ++++++++++--- .../opt/VCBinderSimplification.java | 59 ++++++++-- .../opt/VCSimplificationUtils.java | 103 ++++++++++++++++++ .../src/main/java/liquidjava/utils/Utils.java | 15 +++ .../api/tests/TestFoundBinders.java | 93 +++++++++++++--- .../formatter/ExpressionNameResolverTest.java | 8 -- .../ast/formatter/VariableFormatterTest.java | 8 +- .../opt/VCBinderSimplificationTest.java | 97 ++++++++++++----- .../opt/VCSimplificationUtilsTest.java | 46 ++++++++ 17 files changed, 498 insertions(+), 117 deletions(-) create mode 100644 liquidjava-example/src/main/java/testSuite/ErrorOtherObjectFieldWrite.java create mode 100644 liquidjava-verifier/src/test/java/liquidjava/rj_language/opt/VCSimplificationUtilsTest.java diff --git a/liquidjava-example/src/main/java/testSuite/ErrorOtherObjectFieldWrite.java b/liquidjava-example/src/main/java/testSuite/ErrorOtherObjectFieldWrite.java new file mode 100644 index 000000000..997e92c5e --- /dev/null +++ b/liquidjava-example/src/main/java/testSuite/ErrorOtherObjectFieldWrite.java @@ -0,0 +1,21 @@ +package testSuite; + +import liquidjava.specification.Refinement; + +// a write to another object's field is checked against the field's refinement under that object's name (#457) +public class ErrorOtherObjectFieldWrite { + @Refinement("_ >= 0") + int level; + + void setOther(ErrorOtherObjectFieldWrite other) { + other.level = -1; // Expect: Refinement Error + } + + void decrementOther(ErrorOtherObjectFieldWrite other) { + other.level--; // Expect: Refinement Error + } + + void setOwn() { + this.level = -1; // Expect: Refinement Error + } +} diff --git a/liquidjava-example/src/main/java/testSuite/classes/found_true_binders_error/Basket.java b/liquidjava-example/src/main/java/testSuite/classes/found_true_binders_error/Basket.java index 24fbb357c..3efd9e99a 100644 --- a/liquidjava-example/src/main/java/testSuite/classes/found_true_binders_error/Basket.java +++ b/liquidjava-example/src/main/java/testSuite/classes/found_true_binders_error/Basket.java @@ -96,4 +96,25 @@ String pick() { return names.get(new Random().nextInt(names.size())); // Expect: Refinement Error } } + + // a guard on a parameter unrelated to the expected one + void guarded(int port, int t) { + if (port < 0) + return; + positive(t); // Expect: Refinement Error + } + + // one guard on two flags unrelated to the expected parameter + void flags(boolean p, boolean q, int t) { + if (p || q) + return; + positive(t); // Expect: Refinement Error + } + + // the guard of a loop uses its variable before the variable's row + void count(int start) { + for (int i = start; i < served; i++) { + positive(i); // Expect: Refinement Error + } + } } diff --git a/liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/RefinementTypeChecker.java b/liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/RefinementTypeChecker.java index 1891a38d4..230f1e913 100644 --- a/liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/RefinementTypeChecker.java +++ b/liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/RefinementTypeChecker.java @@ -267,7 +267,7 @@ private void visitAssignment(CtAssignment assignment) thr } else if (ex instanceof CtFieldWrite fw) { CtFieldReference cr = fw.getVariable(); CtField f = fw.getVariable().getDeclaration(); - String updatedVarName = Utils.qualifyFieldName(cr); + String updatedVarName = Utils.writtenFieldName(fw); // a field declared outside the analyzed sources (e.g. a library field) has no declared refinement: the // write stands in for its declaration checkAssignment(updatedVarName, cr.getType(), ex, assignment.getAssignment(), assignment, 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 43f8c5ba3..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 @@ -84,7 +84,7 @@ public void processSubtyping(Predicate expectedType, List list, CtEl DebugLog.smtResult(result); if (result.isError()) { throw new RefinementError(element.getPosition(), declarationPosition, expectedType, - implBeforeChange.simplify(NeededVariables.of(expectedType, result.getCounterexample())), map, + implBeforeChange.simplify(NeededVariables.forRefinementError(expectedType)), map, result.getCounterexample(), customMessage); } } @@ -445,7 +445,7 @@ protected void throwRefinementError(SourcePosition position, SourcePosition decl TranslationTable map = new TranslationTable(); VCImplication premises = buildPremiseChain(map, expected, found); throw new RefinementError(position, declarationPosition, expected, - premises.simplify(NeededVariables.of(expected, counterexample)), map, counterexample, customMessage); + premises.simplify(NeededVariables.forRefinementError(expected)), map, counterexample, customMessage); } protected void throwStateRefinementError(SourcePosition position, SourcePosition declarationPosition, @@ -454,7 +454,8 @@ protected void throwStateRefinementError(SourcePosition position, SourcePosition TranslationTable map = new TranslationTable(); VCImplication foundState = buildPremiseChain(map, expected, found); throw new StateRefinementError(position, declarationPosition, expected, - foundState.simplify(NeededVariables.of(expected, null)), map, customMessage, hints, category, context); + 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/processor/refinement_checker/general_checkers/OperationsChecker.java b/liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/general_checkers/OperationsChecker.java index a739148f9..ec215806e 100644 --- a/liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/general_checkers/OperationsChecker.java +++ b/liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/general_checkers/OperationsChecker.java @@ -179,7 +179,7 @@ public void getUnaryOpRefinements(CtUnaryOperator operator) throws LJErro if (ex instanceof CtVariableWrite w) { name = w.getVariable().getSimpleName(); if (w instanceof CtFieldWrite fieldWrite) - name = Utils.qualifyFieldName(fieldWrite.getVariable()); + name = Utils.writtenFieldName(fieldWrite); all = getRefinementUnaryVariableWrite(ex, operator, w, name); rtc.checkVariableRefinements(all, name, w.getType(), operator, w.getVariable().getDeclaration()); return; @@ -498,6 +498,8 @@ private Predicate getRefinementUnaryVariableWrite(CtExpression ex, CtUnar String newName = String.format(Formats.INSTANCE, name, rtc.getContext().getCounter()); Predicate metadada = rtc.getContext().getVariableRefinements(name); + if (metadada == null) // a field of another object, whose current value is not tracked + metadada = new Predicate(); metadada = metadada.substituteVariable(Keys.WILDCARD, newName); metadada = metadada.substituteVariable(name, newName); diff --git a/liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/object_checkers/AuxStateHandler.java b/liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/object_checkers/AuxStateHandler.java index 38fe52cd9..f0bb9d4e8 100644 --- a/liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/object_checkers/AuxStateHandler.java +++ b/liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/object_checkers/AuxStateHandler.java @@ -635,7 +635,7 @@ public static void checkTargetChanges(TypeChecker tc, RefinedFunction f, CtExpre */ public static void updateGhostField(CtFieldWrite fw, TypeChecker tc) throws LJError { CtField field = fw.getVariable().getDeclaration(); - String updatedVarName = Utils.qualifyFieldName(fw.getVariable()); + String updatedVarName = Utils.writtenFieldName(fw); String targetClass = field.getDeclaringType().getQualifiedName(); // state transition annotation construction 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 77fb6990b..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,10 +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, and with its class only when another field is written the same way + // a field is always written as in code, as its binder and the counterexample write it if (VariableFormatter.isField(name)) - return isAmbiguous(name, variables, VariableFormatter::format) ? VariableFormatter.formatWithOwner(name) - : formatted; + return formatted; return isAmbiguous(name, variables, ExpressionNameResolver::getVariableSimpleName) ? formatted : Utils.getSimpleName(formatted); } diff --git a/liquidjava-verifier/src/main/java/liquidjava/rj_language/ast/formatter/VariableFormatter.java b/liquidjava-verifier/src/main/java/liquidjava/rj_language/ast/formatter/VariableFormatter.java index 3cc1cdb64..a0e932d8b 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 @@ -10,23 +10,13 @@ */ public final class VariableFormatter { private static final Pattern INSTACE_VAR_PATTERN = Pattern.compile("^#(.+)_([0-9]+)$"); + // #.: a field of the current object (this) or of the object in a local variable + private static final Pattern FIELD_PATTERN = Pattern.compile("^([A-Za-z_$][\\w$]*)#([\\w.$]+)\\.([\\w$]+)$"); private static final char[] SUPERSCRIPT_CHARS = { '⁰', '¹', '²', '³', '⁴', '⁵', '⁶', '⁷', '⁸', '⁹' }; - private static final String FIELD_PREFIX = "this#"; + private static final String THIS = "this"; private static final Set STATIC_FIELDS = ConcurrentHashMap.newKeySet(); public static String format(String name) { - return format(name, false); - } - - /** - * Formats a name like {@link #format(String)}, but writes an instance field with its declaring class - * ({@code Basket.this.items}) to tell it apart from a field with the same name in another class - */ - public static String formatWithOwner(String name) { - return format(name, true); - } - - private static String format(String name, boolean withOwner) { if (name == null) return null; @@ -35,12 +25,12 @@ private static String format(String name, boolean withOwner) { Matcher matcher = INSTACE_VAR_PATTERN.matcher(name); if (!matcher.matches()) - return formatField(name, withOwner); + return formatField(name); String baseName = matcher.group(1); String counter = matcher.group(2); String prefix = isSpecialIdentifier(baseName) ? "#" : ""; - return prefix + formatField(baseName, withOwner) + toSuperscript(counter); + return prefix + formatField(baseName) + toSuperscript(counter); } public static String withoutInstance(String name) { @@ -49,11 +39,10 @@ public static String withoutInstance(String name) { } /** - * Whether a name is that of a field, {@code this#.}, possibly with an instance counter + * Whether a name is that of a field, {@code #.}, possibly with an instance counter */ public static boolean isField(String name) { - String baseName = withoutInstance(name); - return baseName.startsWith(FIELD_PREFIX) && baseName.indexOf('.', FIELD_PREFIX.length()) > 0; + return FIELD_PATTERN.matcher(withoutInstance(name)).matches(); } /** @@ -72,20 +61,20 @@ public static void clearStaticFields() { } /** - * 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 + * Writes a field name as it is written in code: {@code this.field} or {@code other.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, boolean withOwner) { - if (!isField(name)) + private static String formatField(String name) { + Matcher matcher = FIELD_PATTERN.matcher(name); + if (!matcher.matches()) return name; - int fieldStart = name.lastIndexOf('.'); - String field = name.substring(fieldStart + 1); - String owner = simpleTypeName(name.substring(FIELD_PREFIX.length(), fieldStart)); - if (STATIC_FIELDS.contains(name)) - return owner + "." + field; - return (withOwner ? owner + ".this." : "this.") + field; + String object = matcher.group(1); + String field = matcher.group(3); + if (object.equals(THIS) && STATIC_FIELDS.contains(name)) + return simpleTypeName(matcher.group(2)) + "." + field; + return object + "." + field; } private static String simpleTypeName(String qualifiedName) { 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 index 95073fc57..094e5ad24 100644 --- a/liquidjava-verifier/src/main/java/liquidjava/rj_language/opt/NeededVariables.java +++ b/liquidjava-verifier/src/main/java/liquidjava/rj_language/opt/NeededVariables.java @@ -1,38 +1,79 @@ 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 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.smt.Counterexample; -import liquidjava.utils.Pair; +import liquidjava.rj_language.ast.Expression; /** - * Variables that a simplified VC chain must keep a binder for even when the binder only says {@code true}: those of the - * expected refinement, and those that the counterexample gives a value + * 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 expected, Set assigned) { +public record NeededVariables(Set expectedTerms, Set expectedValues, boolean keepExpected) { - public static final NeededVariables NONE = new NeededVariables(Set.of(), Set.of()); + public static final NeededVariables NONE = new NeededVariables(Set.of(), Set.of(), false); public NeededVariables { - expected = Set.copyOf(expected); - assigned = Set.copyOf(assigned); + 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); } - public static NeededVariables of(Predicate expected, Counterexample counterexample) { - Set expectedNames = expected == null ? Set.of() : new HashSet<>(expected.getVariableNames()); - Set assignedNames = new HashSet<>(); - if (counterexample != null) - counterexample.assignments().stream().map(Pair::first).forEach(assignedNames::add); - return new NeededVariables(expectedNames, assignedNames); + /** + * 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) { + if (expected == null) + return new NeededVariables(Set.of(), Set.of(), keepExpected); + return new NeededVariables(new HashSet<>(termsOf(expected.getExpression())), + new HashSet<>(valueVariablesOf(expected.getExpression())), keepExpected); } /** - * Whether a binder refined only by {@code true} must stay: the expected refinement is about its variable, or a - * later implication uses it and the counterexample has a value for it + * Variables whose binder refined only by true the chain keeps: those whose own value a fact linked to expected + * constrains. A variable named only as the object 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 */ - public boolean needsTrueBinder(String name, boolean usedDownstream) { - return expected.contains(name) || usedDownstream && assigned.contains(name); + public Set trueBindersToKeep(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())); + + Set keep = new HashSet<>(keepExpected ? expectedValues : Set.of()); + for (Expression fact : linkedConjuncts(facts, VCSimplificationUtils::termsOf, expectedTerms)) + for (String name : valueVariablesOf(fact)) + if (!expectedTerms.contains(name)) + keep.add(name); + return keep; } } 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 f28120dbb..4c0439911 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,10 @@ import static liquidjava.rj_language.opt.VCSimplificationUtils.isFalse; import static liquidjava.rj_language.opt.VCSimplificationUtils.isTrue; +import java.util.ArrayList; +import java.util.List; +import java.util.Set; + import liquidjava.processor.VCImplication; import liquidjava.rj_language.Predicate; import liquidjava.rj_language.ast.LiteralBoolean; @@ -34,24 +38,27 @@ public VCBinderSimplification(NeededVariables needed) { @Override public VCImplication apply(VCImplication implication) { VCImplication cloned = implication.clone(); - VCImplication simplified = simplify(cloned); + Set keptTrueBinders = needed.trueBindersToKeep(cloned); + VCImplication simplified = simplify(cloned, keptTrueBinders); + if (simplified == null) + simplified = moveTrueBinderBeforeFirstUse(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 (isRemovableBinder(implication)) + if (isRemovableBinder(implication, keptTrueBinders)) return removeBinder(implication); - VCImplication next = simplify(implication.getNext()); + VCImplication next = simplify(implication.getNext(), keptTrueBinders); if (next == null) return null; @@ -80,14 +87,50 @@ private VCImplication removeBinder(VCImplication implication) { * 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 isRemovableBinder(VCImplication implication) { + private boolean isRemovableBinder(VCImplication implication, Set keptTrueBinders) { if (!implication.hasBinder()) return false; - boolean usedDownstream = containsVar(implication.getNext(), implication.getName()); if (isTrueBinder(implication)) - return !needed.needsTrueBinder(implication.getName(), usedDownstream); - return !usedDownstream && isUnusedFreshPathBinder(implication); + return !keptTrueBinders.contains(implication.getName()); + return !containsVar(implication.getNext(), implication.getName()) && isUnusedFreshPathBinder(implication); + } + + /** + * Moves the first 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 + */ + private VCImplication moveTrueBinderBeforeFirstUse(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 (!isTrueBinder(binder)) + 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 null; + } + + private 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/VCSimplificationUtils.java b/liquidjava-verifier/src/main/java/liquidjava/rj_language/opt/VCSimplificationUtils.java index 4ab153753..00f65f224 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,99 @@ 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) { + if (expression instanceof BinaryExpression binary && "&&".equals(binary.getOperator())) { + addConjuncts(binary.getFirstOperand(), conjuncts); + addConjuncts(binary.getSecondOperand(), conjuncts); + } else if (expression instanceof UnaryExpression not && "!".equals(not.getOp()) + && not.getExpression()instanceof BinaryExpression binary && "||".equals(binary.getOperator())) { + addConjuncts(new UnaryExpression("!", binary.getFirstOperand()), conjuncts); + addConjuncts(new UnaryExpression("!", binary.getSecondOperand()), conjuncts); + } else if (expression instanceof UnaryExpression not && "!".equals(not.getOp()) + && not.getExpression()instanceof UnaryExpression inner && "!".equals(inner.getOp())) { + addConjuncts(inner.getExpression(), conjuncts); + } else { + conjuncts.add(expression); + } + } + + /** + * 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 8d94b584d..1bc1b8751 100644 --- a/liquidjava-verifier/src/main/java/liquidjava/utils/Utils.java +++ b/liquidjava-verifier/src/main/java/liquidjava/utils/Utils.java @@ -17,6 +17,7 @@ import spoon.reflect.code.CtSuperAccess; import spoon.reflect.code.CtThisAccess; import spoon.reflect.code.CtTry; +import spoon.reflect.code.CtVariableRead; import spoon.reflect.code.CtWhile; import spoon.reflect.cu.SourcePosition; import spoon.reflect.declaration.CtAnnotation; @@ -65,6 +66,20 @@ public static String qualifyFieldName(CtFieldReference field) { return name; } + /** + * Name of the context variable that a field write updates: the tracked field ({@link #qualifyFieldName}) for a + * static field or a field of the current object, and otherwise a variable of its own for that field of the other + * object, {@code #.}, named after the variable holding the object when there is one + */ + public static String writtenFieldName(CtFieldAccess access) { + String name = qualifyFieldName(access.getVariable()); + if (accessesTrackedField(access)) + return name; + String object = access.getTarget()instanceof CtVariableRead read ? read.getVariable().getSimpleName() + : "other"; + return object + name.substring("this".length()); + } + public static String getFile(CtElement element) { SourcePosition pos = element.getPosition(); if (pos == null || pos.getFile() == null) 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 472a8f1d7..779a82b97 100644 --- a/liquidjava-verifier/src/test/java/liquidjava/api/tests/TestFoundBinders.java +++ b/liquidjava-verifier/src/test/java/liquidjava/api/tests/TestFoundBinders.java @@ -17,6 +17,7 @@ import liquidjava.diagnostics.errors.StateRefinementError; import liquidjava.processor.VCImplication; import liquidjava.rj_language.ast.formatter.VariableFormatter; +import liquidjava.rj_language.opt.VCSimplificationResult; /** * Checks the rows of Found: a binder refined only by true is shown only when the error needs it, and fields are written @@ -28,9 +29,16 @@ class TestFoundBinders { private static Map basket; private static Map fieldState; + private static Map pathDependentState; + private static Map otherObjectWrite; - /** What the user is shown for an error, without the instance counters that depend on verification order */ - private record Shown(List rows, String message, String counterexample) { + /** + * 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 @@ -38,11 +46,14 @@ static void verify() { // shown as the IDE gets it: right after the verification, before the next one starts basket = verify("classes/found_true_binders_error"); fieldState = verify("classes/found_field_state_error"); + pathDependentState = verify("ErrorStateHintPathDependent.java"); + otherObjectWrite = verify("ErrorOtherObjectFieldWrite.java"); } @Test void basketHasOneErrorPerCase() { - assertEquals(List.of(25, 30, 36, 49, 56, 62, 67, 76, 82, 88, 96), new ArrayList<>(basket.keySet())); + assertEquals(List.of(25, 30, 36, 49, 56, 62, 67, 76, 82, 88, 96, 104, 111, 117), + new ArrayList<>(basket.keySet())); } @Test @@ -53,6 +64,17 @@ void trueFieldRowOfTheIssueIsDropped() { assertEquals("Counterexample: bound == 0", shown.counterexample()); } + @Test + void steppingBackReachesTheOriginalWithTheDroppedRow() { + Shown shown = basket.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_true_binders_error.Basket.items", "#items_", "#bound_"), + shown.originalBinders()); + } + @Test void trueParameterRowIsDropped() { assertEquals(List.of("∀bound bound == size(list) && bound >= 0"), basket.get(30).rows()); @@ -77,7 +99,7 @@ void severalTrueFieldRowsAreDroppedAndReadWithOrWithoutThisAlike() { } @Test - void trueRowUsedLaterIsKeptWhenTheCounterexampleHasItsValue() { + void trueRowLinkedToExpectedThroughALaterRowIsKept() { Shown shown = basket.get(62); assertEquals(List.of("∀x true", "∀y y == x + 1"), shown.rows()); assertEquals("Counterexample: x == -1 && y == 0", shown.counterexample()); @@ -108,7 +130,11 @@ void fieldReadWithThisIsWrittenAsInCode() { @Test void fieldReadWithoutThisIsWrittenTheSameWay() { - assertEquals(basket.get(82), basket.get(88)); + Shown withThis = basket.get(82); + Shown withoutThis = basket.get(88); + assertEquals(withThis.rows(), withoutThis.rows()); + assertEquals(withThis.message(), withoutThis.message()); + assertEquals(withThis.counterexample(), withoutThis.counterexample()); } @Test @@ -116,6 +142,38 @@ void fieldOfAnInnerClassIsWrittenAsInCode() { assertEquals(List.of("∀bound bound == size(this.names) && bound >= 0"), basket.get(96).rows()); } + @Test + void trueRowUsedOnlyByAnUnrelatedGuardIsDropped() { + Shown shown = basket.get(104); + assertEquals(List.of("∀#fresh !(port < 0)", "∀t true"), shown.rows()); + assertEquals(List.of("∀port true", "∀#fresh !(port < 0)", "∀t true"), shown.originalRows()); + } + + @Test + void trueRowsOfACombinedGuardAreNotLinkedToExpected() { + assertEquals(List.of("∀#fresh !(p || q)", "∀t true"), basket.get(111).rows()); + } + + @Test + void keptTrueRowComesBeforeTheRowUsingIt() { + assertEquals(List.of("∀Basket.served true", "∀i true", "∀#fresh i < Basket.served"), basket.get(117).rows()); + } + + @Test + void trueRowDecidingAPathDependentStateIsKept() { + Shown shown = pathDependentState.get(25); + assertEquals(List.of("∀ready true", "∀f ready ? open(f) : created(f)"), shown.rows()); + } + + @Test + void writeToAnotherObjectsFieldIsWrittenWithThatObject() { + assertEquals(List.of(11, 15, 19), new ArrayList<>(otherObjectWrite.keySet())); + assertEquals("other.level == -1 is not a subtype of other.level >= 0", otherObjectWrite.get(11).message()); + assertEquals(List.of("∀other.level true", "∀other.level other.level == other.level - 1"), + otherObjectWrite.get(15).rows()); + assertEquals("this.level == -1 is not a subtype of this.level >= 0", otherObjectWrite.get(19).message()); + } + @Test void fieldRowHoldingAStateIsKept() { assertEquals(List.of(14), new ArrayList<>(fieldState.keySet())); @@ -130,20 +188,25 @@ void fieldRowHoldingAStateIsKept() { private static Map verify(String test) { CommandLineLauncher.launch(TEST_SUITE + test); Map shown = new TreeMap<>(); - for (LJError error : Diagnostics.getInstance().getErrors()) - shown.put(error.getPosition().getLine(), new Shown(rows(error), plain(error.getMessage()), - error.getCounterexampleStr() == null ? null : plain(error.getCounterexampleStr()))); + for (LJError error : Diagnostics.getInstance().getErrors()) { + VCSimplificationResult found = error instanceof RefinementError refinementError ? refinementError.getFound() + : assertInstanceOf(StateRefinementError.class, error).getFoundSimplification(); + 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(); + shown.put(error.getPosition().getLine(), + new Shown(rows(found.getImplication()), plain(error.getMessage()), + error.getCounterexampleStr() == null ? null : plain(error.getCounterexampleStr()), + rows(original.getImplication()), steps, originalBinders)); + } return shown; } // the rows of Found as the IDE writes them: binder name, then its refinement - private static List rows(LJError error) { - VCImplication found; - if (error instanceof RefinementError refinementError) - found = refinementError.getFound().getImplication(); - else - found = assertInstanceOf(StateRefinementError.class, error).getFound(); - + 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(); 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 e2c907775..f5c630eab 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 @@ -60,12 +60,4 @@ void writesFieldsAsInCodeInsideFunctionArguments() { assertEquals("bound⁶ == size(this.items)", expression.toDisplayString()); } - - @Test - void writesTheClassOfFieldsWithTheSameName() { - Expression expression = Predicate.createEquals(Predicate.createVar("this#shop.Basket.count"), - Predicate.createVar("this#shop.Shelf.count")).getExpression(); - - assertEquals("Basket.this.count == Shelf.this.count", 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 78a7537e0..8cf30490c 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 @@ -58,16 +58,16 @@ void forgetsStaticFieldsOfThePreviousVerification() { } @Test - void writesFieldsWithTheirOwnerOnRequest() { - assertEquals("Basket.this.items", VariableFormatter.formatWithOwner("this#shop.Basket.items")); - assertEquals("Job.this.port²", VariableFormatter.formatWithOwner("#this#pkg.Outer$Job.port_2")); - assertEquals("x²", VariableFormatter.formatWithOwner("#x_2")); + void writesFieldsOfAnotherObjectWithThatObject() { + assertEquals("other.level", VariableFormatter.format("other#otherwrite.W.level")); + assertEquals("other.level¹", VariableFormatter.format("#other#otherwrite.W.level_1")); } @Test void recognisesFieldNames() { assertTrue(VariableFormatter.isField("this#shop.Basket.items")); assertTrue(VariableFormatter.isField("#this#shop.Basket.items_4")); + assertTrue(VariableFormatter.isField("other#otherwrite.W.level")); assertFalse(VariableFormatter.isField("this#Basket")); assertFalse(VariableFormatter.isField("#this_4")); assertFalse(VariableFormatter.isField("items")); 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 e8d1ca56b..f6b8f0c3e 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 @@ -11,8 +11,6 @@ import liquidjava.processor.VCImplication; import liquidjava.rj_language.Predicate; import liquidjava.rj_language.parsing.RefinementsParser; -import liquidjava.smt.Counterexample; -import liquidjava.utils.Pair; import spoon.Launcher; import spoon.reflect.factory.TypeFactory; @@ -22,8 +20,12 @@ class VCBinderSimplificationTest { private static final TypeFactory TYPES = new Launcher().getFactory().Type(); - private static VCBinderSimplification binderWithNeeds(Set expected, Set assigned) { - return new VCBinderSimplification(new NeededVariables(expected, assigned)); + private static VCBinderSimplification forRefinementError(String... expected) { + return new VCBinderSimplification(new NeededVariables(Set.of(expected), Set.of(expected), true)); + } + + private static VCBinderSimplification forStateError(String... expected) { + return new VCBinderSimplification(new NeededVariables(Set.of(expected), Set.of(expected), false)); } @Test @@ -61,42 +63,85 @@ void removesTrueFieldBinderUsedDownstreamWhenNothingNeedsIt() { } @Test - void keepsTrueBinderUsedDownstreamWhenCounterexampleAssignsIt() { - assertSimplificationSteps(binderWithNeeds(Set.of(), Set.of("x")), vc("∀x:int. true", "x > 0"), - step("true", "x > 0")); + void keepsTrueBinderLinkedToExpectedThroughALaterRow() { + assertSimplificationSteps(forRefinementError("y"), vc("∀x:int. true", "∀y:int. y == x + 1"), + step("true", "y == x + 1")); + } + + @Test + void keepsTrueBinderLinkedToExpectedThroughSeveralRows() { + assertSimplificationSteps(forRefinementError("z"), vc("∀x:int. true", "∀y:int. y == x + 1", "∀z:int. z == y"), + step("true", "y == x + 1", "z == y")); + } + + @Test + void removesTrueBinderUsedOnlyByARowUnlinkedToExpected() { + assertSimplificationSteps(forRefinementError("t"), vc("∀port:int. true", "!(port < 0)", "∀t:int. true"), + step("!(port < 0)", "true")); } @Test - void removesTrueBinderAssignedByCounterexampleWhenUnusedDownstream() { - assertSimplificationSteps(binderWithNeeds(Set.of(), Set.of("x")), vc("∀x:int. true", "y > 0"), step("y > 0")); + void splitsANegatedDisjunctionSoOneGuardDoesNotLinkItsParts() { + assertSimplificationSteps(forRefinementError("t"), vc("∀p:boolean. true", "∀t:int. true", "!(p || t < 0)"), + step("true", "!(p || t < 0)")); } @Test - void keepsTrueBinderOfExpectedVariable() { - assertSimplificationSteps(binderWithNeeds(Set.of("x"), Set.of()), vc("∀x:int. true", "y > 0"), - step("true", "y > 0")); + void keepsTrueBinderOfExpectedVariableInRefinementError() { + assertSimplificationSteps(forRefinementError("x"), vc("∀x:int. true", "y > 0"), step("true", "y > 0")); } @Test - void keepsTerminalTrueBinderOfExpectedVariable() { - VCSimplificationResult result = assertSimplificationSteps(binderWithNeeds(Set.of("x"), Set.of()), - vc("∀x:int. true"), step("true")); + void keepsTerminalTrueBinderOfExpectedVariableInRefinementError() { + VCSimplificationResult result = assertSimplificationSteps(forRefinementError("x"), vc("∀x:int. true"), + step("true")); assertEquals(List.of("x"), result.getBinders()); } @Test - void removesOnlyTheTrueBindersNothingNeeds() { - assertSimplificationSteps(binderWithNeeds(Set.of("e"), Set.of("c")), - vc("∀a:int. true", "∀c:int. true", "∀e:int. true", "∀y:int. y == a + c", "y > e"), - step("true", "true", "y == a + c", "y > e")); + void removesTrueBinderOfExpectedVariableInStateError() { + assertSimplificationSteps(forStateError("x"), vc("∀x:int. true", "y > 0"), step("y > 0")); + } + + @Test + void keepsTrueBinderLinkedToExpectedInStateError() { + assertSimplificationSteps(forStateError("f"), vc("∀ready:boolean. true", "∀f:int. ready ? f > 0 : f < 0"), + step("true", "ready ? f > 0 : f < 0")); + } + + @Test + void removesOnlyTheTrueBindersNothingLinks() { + assertSimplificationSteps(forRefinementError("y"), + vc("∀a:int. true", "∀c:int. true", "∀w:int. w > a", "∀y:int. y == c"), step("true", "w > a", "y == c")); + } + + @Test + void movesKeptTrueBinderBeforeItsFirstUse() { + VCSimplificationResult result = assertSimplificationSteps(forRefinementError("i"), + vc("∀y:int. y < i", "∀i:int. true"), step("true", "y < i")); + assertEquals(List.of("i", "y"), result.getBinders()); + } + + @Test + void removesTrueBinderNamedOnlyAsTheObjectOfAGhost() { + assertSimplificationSteps(forRefinementError("b"), vc("∀x:int. true", "∀b:int. b == size(x) && b >= 0"), + step("b == size(x) && b >= 0")); + } + + @Test + void linksThroughGhostApplicationsButKeepsOnlyValueVariables() { + assertSimplificationSteps(forStateError("open(f)", "f"), + vc("∀ready:boolean. true", "∀f:int. true", "ready ? open(f) : created(f)"), + step("true", "ready ? open(f) : created(f)")); } @Test - void neededVariablesComeFromExpectedAndCounterexample() { - NeededVariables needed = NeededVariables.of(new Predicate(RefinementsParser.createAST("x > y", "")), - new Counterexample(List.of(new Pair<>("z", "0")))); - assertEquals(Set.of("x", "y"), needed.expected()); - assertEquals(Set.of("z"), needed.assigned()); + void neededVariablesComeFromExpected() { + Predicate expected = new Predicate(RefinementsParser.createAST("x > size(y)", "")); + assertEquals(new NeededVariables(Set.of("x", "y", "size(y)"), Set.of("x"), true), + NeededVariables.forRefinementError(expected)); + assertEquals(new NeededVariables(Set.of("x", "y", "size(y)"), Set.of("x"), false), + NeededVariables.forStateError(expected)); } @Test @@ -112,8 +157,8 @@ void simplifiesOnlyFirstApplicableBinder() { @Test void skipsInapplicableTrueBinderAndSimplifiesLaterBinder() { - assertSimplificationSteps(binderWithNeeds(Set.of(), Set.of("x")), - vc("∀x:int. true", "x > 0", "∀y:int. true", "z > 0"), step("true", "x > 0", "z > 0")); + assertSimplificationSteps(forRefinementError("x"), vc("∀x:int. true", "x > 0", "∀y:int. true", "z > 0"), + step("true", "x > 0", "z > 0")); } @Test diff --git a/liquidjava-verifier/src/test/java/liquidjava/rj_language/opt/VCSimplificationUtilsTest.java b/liquidjava-verifier/src/test/java/liquidjava/rj_language/opt/VCSimplificationUtilsTest.java new file mode 100644 index 000000000..dc5c781cd --- /dev/null +++ b/liquidjava-verifier/src/test/java/liquidjava/rj_language/opt/VCSimplificationUtilsTest.java @@ -0,0 +1,46 @@ +package liquidjava.rj_language.opt; + +import static org.junit.jupiter.api.Assertions.assertEquals; + +import java.util.List; + +import org.junit.jupiter.api.Test; + +import liquidjava.rj_language.ast.Expression; +import liquidjava.rj_language.parsing.RefinementsParser; + +class VCSimplificationUtilsTest { + + private static Expression parse(String refinement) { + return RefinementsParser.createAST(refinement, ""); + } + + private static List display(List expressions) { + return expressions.stream().map(Expression::toDisplayString).toList(); + } + + @Test + void splitsConjunctionsAndNegatedDisjunctions() { + assertEquals(List.of("!a", "!(b > 0)", "c", "d"), + display(VCSimplificationUtils.splitConjuncts(parse("!(a || b > 0) && c && !!d")))); + } + + @Test + void keepsDisjunctionsAndNegatedConjunctionsWhole() { + assertEquals(List.of("a || b", "!(c && d)"), + display(VCSimplificationUtils.splitConjuncts(parse("(a || b) && !(c && d)")))); + } + + @Test + void linksConjunctsSharingVariablesWithTheSeedTransitively() { + List conjuncts = List.of(parse("y == x + 1"), parse("p"), parse("x > z"), parse("q == p")); + assertEquals(List.of("y == x + 1", "x > z"), display( + VCSimplificationUtils.linkedConjuncts(conjuncts, VCSimplificationUtils::variablesOf, List.of("y")))); + } + + @Test + void linksNothingWithoutASharedVariable() { + assertEquals(List.of(), VCSimplificationUtils.linkedConjuncts(List.of(parse("p && q")), + VCSimplificationUtils::variablesOf, List.of("t"))); + } +} From a725a573f2b59d21bca4bac24130ecd86e0393ba Mon Sep 17 00:00:00 2001 From: Catarina Gamboa Date: Tue, 3 Nov 2026 14:02:42 +0000 Subject: [PATCH 3/5] Keep writes to another object's field as on main and only name the object in their display Writes through another object are checked and tracked exactly as on main again; the new instance they create is only displayed with the receiver's name. A true binder that is a primitive ghost argument is kept like any other value variable. Co-Authored-By: Claude Opus 5.5 --- .../testSuite/ErrorOtherObjectFieldWrite.java | 18 +++++++- .../RefinementTypeChecker.java | 2 +- .../refinement_checker/TypeChecker.java | 3 ++ .../general_checkers/OperationsChecker.java | 4 +- .../object_checkers/AuxStateHandler.java | 2 +- .../ast/formatter/VariableFormatter.java | 43 +++++++++++++------ .../rj_language/opt/NeededVariables.java | 28 +++++++++--- .../src/main/java/liquidjava/utils/Utils.java | 25 ++++++----- .../api/tests/TestFoundBinders.java | 14 ++++-- .../ast/formatter/VariableFormatterTest.java | 14 ++++-- .../opt/VCBinderSimplificationTest.java | 8 +++- .../java/liquidjava/utils/VCTestUtils.java | 2 + 12 files changed, 118 insertions(+), 45 deletions(-) diff --git a/liquidjava-example/src/main/java/testSuite/ErrorOtherObjectFieldWrite.java b/liquidjava-example/src/main/java/testSuite/ErrorOtherObjectFieldWrite.java index 997e92c5e..3a934b566 100644 --- a/liquidjava-example/src/main/java/testSuite/ErrorOtherObjectFieldWrite.java +++ b/liquidjava-example/src/main/java/testSuite/ErrorOtherObjectFieldWrite.java @@ -2,7 +2,7 @@ import liquidjava.specification.Refinement; -// a write to another object's field is checked against the field's refinement under that object's name (#457) +// writes to another object's field are checked as on main; only their display names the object (#457) public class ErrorOtherObjectFieldWrite { @Refinement("_ >= 0") int level; @@ -11,10 +11,26 @@ void setOther(ErrorOtherObjectFieldWrite other) { other.level = -1; // Expect: Refinement Error } + void incrementOther(ErrorOtherObjectFieldWrite other) { + other.level++; + } + + void addToOther(ErrorOtherObjectFieldWrite other) { + other.level += 1; + } + void decrementOther(ErrorOtherObjectFieldWrite other) { other.level--; // Expect: Refinement Error } + void writeThroughAlias() { + level = 7; + ErrorOtherObjectFieldWrite other = this; + other.level = 3; + @Refinement("_ == 7") + int k = level; // Expect: Refinement Error + } + void setOwn() { this.level = -1; // Expect: Refinement Error } diff --git a/liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/RefinementTypeChecker.java b/liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/RefinementTypeChecker.java index 230f1e913..1891a38d4 100644 --- a/liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/RefinementTypeChecker.java +++ b/liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/RefinementTypeChecker.java @@ -267,7 +267,7 @@ private void visitAssignment(CtAssignment assignment) thr } else if (ex instanceof CtFieldWrite fw) { CtFieldReference cr = fw.getVariable(); CtField f = fw.getVariable().getDeclaration(); - String updatedVarName = Utils.writtenFieldName(fw); + String updatedVarName = Utils.qualifyFieldName(cr); // a field declared outside the analyzed sources (e.g. a library field) has no declared refinement: the // write stands in for its declaration checkAssignment(updatedVarName, cr.getType(), ex, assignment.getAssignment(), assignment, 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..05340dfa7 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.VariableFormatter; 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 -> VariableFormatter.registerReceiver(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/general_checkers/OperationsChecker.java b/liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/general_checkers/OperationsChecker.java index ec215806e..a739148f9 100644 --- a/liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/general_checkers/OperationsChecker.java +++ b/liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/general_checkers/OperationsChecker.java @@ -179,7 +179,7 @@ public void getUnaryOpRefinements(CtUnaryOperator operator) throws LJErro if (ex instanceof CtVariableWrite w) { name = w.getVariable().getSimpleName(); if (w instanceof CtFieldWrite fieldWrite) - name = Utils.writtenFieldName(fieldWrite); + name = Utils.qualifyFieldName(fieldWrite.getVariable()); all = getRefinementUnaryVariableWrite(ex, operator, w, name); rtc.checkVariableRefinements(all, name, w.getType(), operator, w.getVariable().getDeclaration()); return; @@ -498,8 +498,6 @@ private Predicate getRefinementUnaryVariableWrite(CtExpression ex, CtUnar String newName = String.format(Formats.INSTANCE, name, rtc.getContext().getCounter()); Predicate metadada = rtc.getContext().getVariableRefinements(name); - if (metadada == null) // a field of another object, whose current value is not tracked - metadada = new Predicate(); metadada = metadada.substituteVariable(Keys.WILDCARD, newName); metadada = metadada.substituteVariable(name, newName); diff --git a/liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/object_checkers/AuxStateHandler.java b/liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/object_checkers/AuxStateHandler.java index f0bb9d4e8..38fe52cd9 100644 --- a/liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/object_checkers/AuxStateHandler.java +++ b/liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/object_checkers/AuxStateHandler.java @@ -635,7 +635,7 @@ public static void checkTargetChanges(TypeChecker tc, RefinedFunction f, CtExpre */ public static void updateGhostField(CtFieldWrite fw, TypeChecker tc) throws LJError { CtField field = fw.getVariable().getDeclaration(); - String updatedVarName = Utils.writtenFieldName(fw); + String updatedVarName = Utils.qualifyFieldName(fw.getVariable()); String targetClass = field.getDeclaringType().getQualifiedName(); // state transition annotation construction 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 a0e932d8b..4b63c55bd 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,5 +1,6 @@ package liquidjava.rj_language.ast.formatter; +import java.util.Map; import java.util.Set; import java.util.concurrent.ConcurrentHashMap; import java.util.regex.Matcher; @@ -10,11 +11,11 @@ */ public final class VariableFormatter { private static final Pattern INSTACE_VAR_PATTERN = Pattern.compile("^#(.+)_([0-9]+)$"); - // #.: a field of the current object (this) or of the object in a local variable - private static final Pattern FIELD_PATTERN = Pattern.compile("^([A-Za-z_$][\\w$]*)#([\\w.$]+)\\.([\\w$]+)$"); + // this#. + private static final Pattern FIELD_PATTERN = Pattern.compile("^this#([\\w.$]+)\\.([\\w$]+)$"); private static final char[] SUPERSCRIPT_CHARS = { '⁰', '¹', '²', '³', '⁴', '⁵', '⁶', '⁷', '⁸', '⁹' }; - private static final String THIS = "this"; private static final Set STATIC_FIELDS = ConcurrentHashMap.newKeySet(); + private static final Map WRITE_RECEIVERS = new ConcurrentHashMap<>(); public static String format(String name) { if (name == null) @@ -29,6 +30,9 @@ public static String format(String name) { String baseName = matcher.group(1); String counter = matcher.group(2); + String receiver = WRITE_RECEIVERS.get(name); + if (receiver != null && isField(baseName)) + return (receiver.isEmpty() ? "" : receiver + ".") + fieldOf(baseName) + toSuperscript(counter); String prefix = isSpecialIdentifier(baseName) ? "#" : ""; return prefix + formatField(baseName) + toSuperscript(counter); } @@ -39,7 +43,7 @@ public static String withoutInstance(String name) { } /** - * Whether a name is that of a field, {@code #.}, possibly with an instance counter + * 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(); @@ -54,27 +58,40 @@ public static void registerStaticField(String name) { } /** - * Forgets the static fields recorded by the previous verification + * Records that an instance of a field ({@code #this#._}) was created by a write through + * another object ({@code receiver.field = v}), so that it is displayed as {@code receiver.field} instead of + * {@code this.field}; an empty receiver displays the bare field name. Only the display changes + */ + public static void registerReceiver(String instanceName, String receiver) { + WRITE_RECEIVERS.put(instanceName, receiver); + } + + /** + * Forgets the static fields and write receivers recorded by the previous verification */ public static void clearStaticFields() { STATIC_FIELDS.clear(); + WRITE_RECEIVERS.clear(); } /** - * Writes a field name as it is written in code: {@code this.field} or {@code other.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 + * 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; - String object = matcher.group(1); - String field = matcher.group(3); - if (object.equals(THIS) && STATIC_FIELDS.contains(name)) - return simpleTypeName(matcher.group(2)) + "." + field; - return object + "." + field; + if (STATIC_FIELDS.contains(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) { 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 index 094e5ad24..cabb7dbb6 100644 --- a/liquidjava-verifier/src/main/java/liquidjava/rj_language/opt/NeededVariables.java +++ b/liquidjava-verifier/src/main/java/liquidjava/rj_language/opt/NeededVariables.java @@ -5,6 +5,7 @@ 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; @@ -60,19 +61,32 @@ private static NeededVariables of(Predicate expected, boolean keepExpected) { /** * Variables whose binder refined only by true the chain keeps: those whose own value a fact linked to expected - * constrains. A variable named only as the object 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 + * constrains. A variable of an object type that a 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 */ public Set trueBindersToKeep(VCImplication chain) { List facts = new ArrayList<>(); - for (VCImplication current = chain; current != null; current = current.getNext()) + Set primitives = new HashSet<>(); + for (VCImplication current = chain; current != null; current = current.getNext()) { + if (current.hasBinder() && current.getType().isPrimitive()) + primitives.add(current.getName()); if (!isTrue(current.getRefinement().getExpression())) facts.addAll(splitConjuncts(current.getRefinement().getExpression())); + } - Set keep = new HashSet<>(keepExpected ? expectedValues : Set.of()); - for (Expression fact : linkedConjuncts(facts, VCSimplificationUtils::termsOf, expectedTerms)) - for (String name : valueVariablesOf(fact)) - if (!expectedTerms.contains(name)) + Set keep = new HashSet<>(); + if (keepExpected) + keep.addAll(expectedValues); + for (Expression fact : linkedConjuncts(facts, VCSimplificationUtils::termsOf, expectedTerms)) { + List values = valueVariablesOf(fact); + for (String name : variablesOf(fact)) + if ((values.contains(name) || primitives.contains(name)) && !expectedTerms.contains(name)) + keep.add(name); + } + if (keepExpected) + for (String name : expectedTerms) + if (primitives.contains(name)) keep.add(name); return keep; } diff --git a/liquidjava-verifier/src/main/java/liquidjava/utils/Utils.java b/liquidjava-verifier/src/main/java/liquidjava/utils/Utils.java index 1bc1b8751..94b973f0a 100644 --- a/liquidjava-verifier/src/main/java/liquidjava/utils/Utils.java +++ b/liquidjava-verifier/src/main/java/liquidjava/utils/Utils.java @@ -3,20 +3,25 @@ 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.VariableFormatter; 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; @@ -67,17 +72,17 @@ public static String qualifyFieldName(CtFieldReference field) { } /** - * Name of the context variable that a field write updates: the tracked field ({@link #qualifyFieldName}) for a - * static field or a field of the current object, and otherwise a variable of its own for that field of the other - * object, {@code #.}, named after the variable holding the object when there is one + * 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 String writtenFieldName(CtFieldAccess access) { - String name = qualifyFieldName(access.getVariable()); - if (accessesTrackedField(access)) - return name; - String object = access.getTarget()instanceof CtVariableRead read ? read.getVariable().getSimpleName() - : "other"; - return object + name.substring("this".length()); + 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 index 779a82b97..8c955e457 100644 --- a/liquidjava-verifier/src/test/java/liquidjava/api/tests/TestFoundBinders.java +++ b/liquidjava-verifier/src/test/java/liquidjava/api/tests/TestFoundBinders.java @@ -165,13 +165,19 @@ void trueRowDecidingAPathDependentStateIsKept() { assertEquals(List.of("∀ready true", "∀f ready ? open(f) : created(f)"), shown.rows()); } + @Test + void writesToAnotherObjectsFieldAreCheckedAsOnMain() { + // other.level++ and other.level += 1 verify, other.level-- and the write through an alias of this are reported + assertEquals(List.of(11, 23, 31, 35), new ArrayList<>(otherObjectWrite.keySet())); + assertEquals("k == 7", otherObjectWrite.get(31).message().replaceAll(".* is not a subtype of ", "")); + } + @Test void writeToAnotherObjectsFieldIsWrittenWithThatObject() { - assertEquals(List.of(11, 15, 19), new ArrayList<>(otherObjectWrite.keySet())); assertEquals("other.level == -1 is not a subtype of other.level >= 0", otherObjectWrite.get(11).message()); - assertEquals(List.of("∀other.level true", "∀other.level other.level == other.level - 1"), - otherObjectWrite.get(15).rows()); - assertEquals("this.level == -1 is not a subtype of this.level >= 0", otherObjectWrite.get(19).message()); + assertEquals(List.of("∀this.level this.level >= 0", "∀other.level other.level == this.level - 1"), + otherObjectWrite.get(23).rows()); + assertEquals("this.level == -1 is not a subtype of this.level >= 0", otherObjectWrite.get(35).message()); } @Test 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 8cf30490c..2d8028ebe 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 @@ -58,16 +58,22 @@ void forgetsStaticFieldsOfThePreviousVerification() { } @Test - void writesFieldsOfAnotherObjectWithThatObject() { - assertEquals("other.level", VariableFormatter.format("other#otherwrite.W.level")); - assertEquals("other.level¹", VariableFormatter.format("#other#otherwrite.W.level_1")); + void writesAnInstanceCreatedByAWriteThroughAnotherObjectWithThatObject() { + VariableFormatter.registerReceiver("#this#otherwrite.W.level_1", "other"); + VariableFormatter.registerReceiver("#this#otherwrite.W.level_2", ""); + assertEquals("other.level¹", VariableFormatter.format("#this#otherwrite.W.level_1")); + assertEquals("level²", VariableFormatter.format("#this#otherwrite.W.level_2")); + assertEquals("this.level³", VariableFormatter.format("#this#otherwrite.W.level_3")); + assertEquals("this.level", VariableFormatter.format("this#otherwrite.W.level")); + VariableFormatter.clearStaticFields(); + assertEquals("this.level¹", VariableFormatter.format("#this#otherwrite.W.level_1")); } @Test void recognisesFieldNames() { assertTrue(VariableFormatter.isField("this#shop.Basket.items")); assertTrue(VariableFormatter.isField("#this#shop.Basket.items_4")); - assertTrue(VariableFormatter.isField("other#otherwrite.W.level")); + assertFalse(VariableFormatter.isField("other#otherwrite.W.level")); assertFalse(VariableFormatter.isField("this#Basket")); assertFalse(VariableFormatter.isField("#this_4")); assertFalse(VariableFormatter.isField("items")); 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 f6b8f0c3e..12eba8c89 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 @@ -124,10 +124,16 @@ void movesKeptTrueBinderBeforeItsFirstUse() { @Test void removesTrueBinderNamedOnlyAsTheObjectOfAGhost() { - assertSimplificationSteps(forRefinementError("b"), vc("∀x:int. true", "∀b:int. b == size(x) && b >= 0"), + assertSimplificationSteps(forRefinementError("b"), vc("∀x:Object. true", "∀b:int. b == size(x) && b >= 0"), step("b == size(x) && b >= 0")); } + @Test + void keepsPrimitiveTrueBinderThatIsTheArgumentOfAGhost() { + assertSimplificationSteps(forRefinementError("y"), vc("∀k:int. true", "∀y:int. y == f(k)"), + step("true", "y == f(k)")); + } + @Test void linksThroughGhostApplicationsButKeepsOnlyValueVariables() { assertSimplificationSteps(forStateError("open(f)", "f"), diff --git a/liquidjava-verifier/src/test/java/liquidjava/utils/VCTestUtils.java b/liquidjava-verifier/src/test/java/liquidjava/utils/VCTestUtils.java index 019dd76cb..2a039e253 100644 --- a/liquidjava-verifier/src/test/java/liquidjava/utils/VCTestUtils.java +++ b/liquidjava-verifier/src/test/java/liquidjava/utils/VCTestUtils.java @@ -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); } From 46ffb1767db001820581a171bac1e0220e6c84d2 Mon Sep 17 00:00:00 2001 From: Catarina Gamboa Date: Tue, 3 Nov 2026 18:51:01 +0000 Subject: [PATCH 4/5] Give field display records and binder ordering their own classes, and keep only the tests that pin distinct behaviour FieldDisplayNames now owns the static-field and write-receiver records that VariableFormatter reads, moving binders before their first use is its own Binder Ordering pass, and NeededVariables is split into small functions. The fixtures for #457 are merged into one directory and the tests cut to one per behaviour. Co-Authored-By: Claude Opus 5.5 --- .../testSuite/ErrorOtherObjectFieldWrite.java | 37 ---- .../ArrayListRefinements.java | 2 +- .../classes/found_binders_error/Basket.java | 58 ++++++ .../RandomRefinements.java | 2 +- .../InterruptManager.java | 16 -- .../VectorRefinements.java | 21 --- .../found_true_binders_error/Basket.java | 120 ------------ .../liquidjava/api/CommandLineLauncher.java | 4 +- .../refinement_checker/TypeChecker.java | 4 +- .../ast/formatter/FieldDisplayNames.java | 51 +++++ .../ast/formatter/VariableFormatter.java | 34 +--- .../rj_language/opt/NeededVariables.java | 56 +++--- .../rj_language/opt/VCBinderOrdering.java | 54 ++++++ .../opt/VCBinderSimplification.java | 44 +---- .../rj_language/opt/VCSimplification.java | 2 +- .../opt/VCSimplificationUtils.java | 14 +- .../src/main/java/liquidjava/utils/Utils.java | 8 +- .../api/tests/TestFoundBinders.java | 175 +++--------------- .../formatter/ExpressionNameResolverTest.java | 9 - .../ast/formatter/VariableFormatterTest.java | 52 ++---- .../rj_language/opt/VCBinderOrderingTest.java | 18 ++ .../opt/VCBinderSimplificationTest.java | 101 +++------- .../opt/VCSimplificationUtilsTest.java | 46 ----- 23 files changed, 296 insertions(+), 632 deletions(-) delete mode 100644 liquidjava-example/src/main/java/testSuite/ErrorOtherObjectFieldWrite.java rename liquidjava-example/src/main/java/testSuite/classes/{found_true_binders_error => found_binders_error}/ArrayListRefinements.java (87%) create mode 100644 liquidjava-example/src/main/java/testSuite/classes/found_binders_error/Basket.java rename liquidjava-example/src/main/java/testSuite/classes/{found_true_binders_error => found_binders_error}/RandomRefinements.java (84%) delete mode 100644 liquidjava-example/src/main/java/testSuite/classes/found_field_state_error/InterruptManager.java delete mode 100644 liquidjava-example/src/main/java/testSuite/classes/found_field_state_error/VectorRefinements.java delete mode 100644 liquidjava-example/src/main/java/testSuite/classes/found_true_binders_error/Basket.java create mode 100644 liquidjava-verifier/src/main/java/liquidjava/rj_language/ast/formatter/FieldDisplayNames.java create mode 100644 liquidjava-verifier/src/main/java/liquidjava/rj_language/opt/VCBinderOrdering.java create mode 100644 liquidjava-verifier/src/test/java/liquidjava/rj_language/opt/VCBinderOrderingTest.java delete mode 100644 liquidjava-verifier/src/test/java/liquidjava/rj_language/opt/VCSimplificationUtilsTest.java diff --git a/liquidjava-example/src/main/java/testSuite/ErrorOtherObjectFieldWrite.java b/liquidjava-example/src/main/java/testSuite/ErrorOtherObjectFieldWrite.java deleted file mode 100644 index 3a934b566..000000000 --- a/liquidjava-example/src/main/java/testSuite/ErrorOtherObjectFieldWrite.java +++ /dev/null @@ -1,37 +0,0 @@ -package testSuite; - -import liquidjava.specification.Refinement; - -// writes to another object's field are checked as on main; only their display names the object (#457) -public class ErrorOtherObjectFieldWrite { - @Refinement("_ >= 0") - int level; - - void setOther(ErrorOtherObjectFieldWrite other) { - other.level = -1; // Expect: Refinement Error - } - - void incrementOther(ErrorOtherObjectFieldWrite other) { - other.level++; - } - - void addToOther(ErrorOtherObjectFieldWrite other) { - other.level += 1; - } - - void decrementOther(ErrorOtherObjectFieldWrite other) { - other.level--; // Expect: Refinement Error - } - - void writeThroughAlias() { - level = 7; - ErrorOtherObjectFieldWrite other = this; - other.level = 3; - @Refinement("_ == 7") - int k = level; // Expect: Refinement Error - } - - void setOwn() { - this.level = -1; // Expect: Refinement Error - } -} diff --git a/liquidjava-example/src/main/java/testSuite/classes/found_true_binders_error/ArrayListRefinements.java b/liquidjava-example/src/main/java/testSuite/classes/found_binders_error/ArrayListRefinements.java similarity index 87% rename from liquidjava-example/src/main/java/testSuite/classes/found_true_binders_error/ArrayListRefinements.java rename to liquidjava-example/src/main/java/testSuite/classes/found_binders_error/ArrayListRefinements.java index b3b969708..56a182c08 100644 --- a/liquidjava-example/src/main/java/testSuite/classes/found_true_binders_error/ArrayListRefinements.java +++ b/liquidjava-example/src/main/java/testSuite/classes/found_binders_error/ArrayListRefinements.java @@ -1,4 +1,4 @@ -package testSuite.classes.found_true_binders_error; +package testSuite.classes.found_binders_error; import liquidjava.specification.ExternalRefinementsFor; import liquidjava.specification.Ghost; 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_true_binders_error/RandomRefinements.java b/liquidjava-example/src/main/java/testSuite/classes/found_binders_error/RandomRefinements.java similarity index 84% rename from liquidjava-example/src/main/java/testSuite/classes/found_true_binders_error/RandomRefinements.java rename to liquidjava-example/src/main/java/testSuite/classes/found_binders_error/RandomRefinements.java index b9be38c8d..73e6720ef 100644 --- a/liquidjava-example/src/main/java/testSuite/classes/found_true_binders_error/RandomRefinements.java +++ b/liquidjava-example/src/main/java/testSuite/classes/found_binders_error/RandomRefinements.java @@ -1,4 +1,4 @@ -package testSuite.classes.found_true_binders_error; +package testSuite.classes.found_binders_error; import liquidjava.specification.ExternalRefinementsFor; import liquidjava.specification.Refinement; diff --git a/liquidjava-example/src/main/java/testSuite/classes/found_field_state_error/InterruptManager.java b/liquidjava-example/src/main/java/testSuite/classes/found_field_state_error/InterruptManager.java deleted file mode 100644 index 45ac9ffe7..000000000 --- a/liquidjava-example/src/main/java/testSuite/classes/found_field_state_error/InterruptManager.java +++ /dev/null @@ -1,16 +0,0 @@ -package testSuite.classes.found_field_state_error; - -import java.util.Vector; - -// the field's row holds its state, so Found keeps it under its source name (#457) -public class InterruptManager { - private Vector interrupts; - - public void initialize(int intrNumber) { - interrupts = new Vector(67); - if (intrNumber < 0 || intrNumber >= 67) { - return; - } - String handlers = interrupts.get(intrNumber); // Expect: State Refinement Error - } -} diff --git a/liquidjava-example/src/main/java/testSuite/classes/found_field_state_error/VectorRefinements.java b/liquidjava-example/src/main/java/testSuite/classes/found_field_state_error/VectorRefinements.java deleted file mode 100644 index 5029cee43..000000000 --- a/liquidjava-example/src/main/java/testSuite/classes/found_field_state_error/VectorRefinements.java +++ /dev/null @@ -1,21 +0,0 @@ -package testSuite.classes.found_field_state_error; - -import liquidjava.specification.ExternalRefinementsFor; -import liquidjava.specification.Refinement; -import liquidjava.specification.StateRefinement; -import liquidjava.specification.StateSet; - -@ExternalRefinementsFor("java.util.Vector") -@StateSet({"empty", "maybeElements"}) -public interface VectorRefinements { - - @StateRefinement(to = "empty(this)") - public void Vector(@Refinement("_ >= 0") int initialCapacity); - - @StateRefinement(from = "empty(this)", to = "maybeElements(this)") - @StateRefinement(from = "maybeElements(this)") - public boolean add(E e); - - @StateRefinement(from = "maybeElements(this)") - public E get(@Refinement("_ >= 0") int index); -} diff --git a/liquidjava-example/src/main/java/testSuite/classes/found_true_binders_error/Basket.java b/liquidjava-example/src/main/java/testSuite/classes/found_true_binders_error/Basket.java deleted file mode 100644 index 3efd9e99a..000000000 --- a/liquidjava-example/src/main/java/testSuite/classes/found_true_binders_error/Basket.java +++ /dev/null @@ -1,120 +0,0 @@ -package testSuite.classes.found_true_binders_error; - -import java.util.ArrayList; -import java.util.Random; - -import liquidjava.specification.Refinement; - -// Found keeps a binder refined only by true when the error needs it (#457) -public class Basket { - static int served; - - private final ArrayList items; - private final ArrayList extras; - private final Random random = new Random(); - int amount; - - Basket(ArrayList items, ArrayList extras) { - this.items = items; - this.extras = extras; - } - - // 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 parameter refined only by true - String pickFrom(ArrayList list) { - return list.get(random.nextInt(list.size())); // Expect: Refinement Error - } - - // a call result refined only by true - String pickCopy() { - ArrayList copy = copyItems(); - return copy.get(random.nextInt(copy.size())); // Expect: Refinement Error - } - - ArrayList copyItems() { - return new ArrayList<>(items); - } - - // a local refined only by true: the loop may have reassigned it - String pickLocal(ArrayList list) { - ArrayList local = list; - for (String name : list) { - local = list; - } - return local.get(random.nextInt(local.size())); // Expect: Refinement Error - } - - // several fields, read with and without this - int pickAny() { - int first = this.items.size(); - int second = extras.size(); - return random.nextInt(first + second); // Expect: Refinement Error - } - - // a later row uses the parameter and the counterexample has a value for it - void next(int x) { - @Refinement("_ > 0") - int y = x + 1; // Expect: Refinement Error - } - - // the expected refinement is about the parameter - void forward(int x, int unrelated) { - positive(x); // Expect: Refinement Error - } - - void positive(@Refinement("_ > 0") int v) { - } - - // a static field - void serve() { - @Refinement("_ > 0") - int count = served + 1; // Expect: Refinement Error - } - - // an instance field read with this - void withThis() { - @Refinement("_ > 0") - int a = this.amount; // Expect: Refinement Error - } - - // the same field read without this - void withoutThis() { - @Refinement("_ > 0") - int a = amount; // Expect: Refinement Error - } - - class Shelf { - ArrayList names; - - // a field of an inner class - String pick() { - return names.get(new Random().nextInt(names.size())); // Expect: Refinement Error - } - } - - // a guard on a parameter unrelated to the expected one - void guarded(int port, int t) { - if (port < 0) - return; - positive(t); // Expect: Refinement Error - } - - // one guard on two flags unrelated to the expected parameter - void flags(boolean p, boolean q, int t) { - if (p || q) - return; - positive(t); // Expect: Refinement Error - } - - // the guard of a loop uses its variable before the variable's row - void count(int start) { - for (int i = start; i < served; i++) { - positive(i); // Expect: Refinement Error - } - } -} diff --git a/liquidjava-verifier/src/main/java/liquidjava/api/CommandLineLauncher.java b/liquidjava-verifier/src/main/java/liquidjava/api/CommandLineLauncher.java index 5590ae65f..00b0256b9 100644 --- a/liquidjava-verifier/src/main/java/liquidjava/api/CommandLineLauncher.java +++ b/liquidjava-verifier/src/main/java/liquidjava/api/CommandLineLauncher.java @@ -9,7 +9,7 @@ import liquidjava.diagnostics.warnings.CustomWarning; import liquidjava.processor.RefinementProcessor; import liquidjava.processor.context.ContextHistory; -import liquidjava.rj_language.ast.formatter.VariableFormatter; +import liquidjava.rj_language.ast.formatter.FieldDisplayNames; import liquidjava.specification.Refinement; import picocli.CommandLine; import spoon.Launcher; @@ -58,7 +58,7 @@ public static void launch(String... paths) { diagnostics.clear(); contextHistory.clearHistory(); - VariableFormatter.clearStaticFields(); + 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/refinement_checker/TypeChecker.java b/liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/TypeChecker.java index 05340dfa7..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,7 +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.VariableFormatter; +import liquidjava.rj_language.ast.formatter.FieldDisplayNames; import liquidjava.rj_language.parsing.RefinementsParser; import liquidjava.smt.SMTEvaluator; import liquidjava.smt.SMTResult; @@ -384,7 +384,7 @@ public void checkVariableRefinements(Predicate refinementFound, String simpleNam String newName = String.format(Formats.INSTANCE, simpleName, context.getCounter()); Utils.untrackedWriteReceiver(usage) - .ifPresent(receiver -> VariableFormatter.registerReceiver(newName, receiver)); + .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/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 4b63c55bd..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 @@ -1,8 +1,5 @@ package liquidjava.rj_language.ast.formatter; -import java.util.Map; -import java.util.Set; -import java.util.concurrent.ConcurrentHashMap; import java.util.regex.Matcher; import java.util.regex.Pattern; @@ -14,8 +11,6 @@ public final class VariableFormatter { // this#. private static final Pattern FIELD_PATTERN = Pattern.compile("^this#([\\w.$]+)\\.([\\w$]+)$"); private static final char[] SUPERSCRIPT_CHARS = { '⁰', '¹', '²', '³', '⁴', '⁵', '⁶', '⁷', '⁸', '⁹' }; - private static final Set STATIC_FIELDS = ConcurrentHashMap.newKeySet(); - private static final Map WRITE_RECEIVERS = new ConcurrentHashMap<>(); public static String format(String name) { if (name == null) @@ -30,7 +25,7 @@ public static String format(String name) { String baseName = matcher.group(1); String counter = matcher.group(2); - String receiver = WRITE_RECEIVERS.get(name); + String receiver = FieldDisplayNames.writeReceiver(name); if (receiver != null && isField(baseName)) return (receiver.isEmpty() ? "" : receiver + ".") + fieldOf(baseName) + toSuperscript(counter); String prefix = isSpecialIdentifier(baseName) ? "#" : ""; @@ -49,31 +44,6 @@ public static boolean isField(String name) { return FIELD_PATTERN.matcher(withoutInstance(name)).matches(); } - /** - * Records that a field name ({@code this#.}) belongs to a static field, which is then - * displayed as {@code Class.field} instead of {@code this.field} - */ - public static void registerStaticField(String name) { - STATIC_FIELDS.add(name); - } - - /** - * Records that an instance of a field ({@code #this#._}) was created by a write through - * another object ({@code receiver.field = v}), so that it is displayed as {@code receiver.field} instead of - * {@code this.field}; an empty receiver displays the bare field name. Only the display changes - */ - public static void registerReceiver(String instanceName, String receiver) { - WRITE_RECEIVERS.put(instanceName, receiver); - } - - /** - * Forgets the static fields and write receivers recorded by the previous verification - */ - public static void clearStaticFields() { - STATIC_FIELDS.clear(); - WRITE_RECEIVERS.clear(); - } - /** * 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 @@ -84,7 +54,7 @@ private static String formatField(String name) { if (!matcher.matches()) return name; - if (STATIC_FIELDS.contains(name)) + if (FieldDisplayNames.isStaticField(name)) return simpleTypeName(matcher.group(1)) + "." + matcher.group(2); return "this." + matcher.group(2); } 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 index cabb7dbb6..1c1680354 100644 --- a/liquidjava-verifier/src/main/java/liquidjava/rj_language/opt/NeededVariables.java +++ b/liquidjava-verifier/src/main/java/liquidjava/rj_language/opt/NeededVariables.java @@ -53,41 +53,51 @@ public static NeededVariables forStateError(Predicate expected) { } private static NeededVariables of(Predicate expected, boolean keepExpected) { - if (expected == null) - return new NeededVariables(Set.of(), Set.of(), keepExpected); - return new NeededVariables(new HashSet<>(termsOf(expected.getExpression())), - new HashSet<>(valueVariablesOf(expected.getExpression())), 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. A variable of an object type that a 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 + * constrains, and, when {@code keepExpected}, those whose value expected constrains */ public Set trueBindersToKeep(VCImplication chain) { - List facts = new ArrayList<>(); - Set primitives = new HashSet<>(); - for (VCImplication current = chain; current != null; current = current.getNext()) { - if (current.hasBinder() && current.getType().isPrimitive()) - primitives.add(current.getName()); - if (!isTrue(current.getRefinement().getExpression())) - facts.addAll(splitConjuncts(current.getRefinement().getExpression())); - } - + Set primitives = primitiveBinders(chain); Set keep = new HashSet<>(); - if (keepExpected) - keep.addAll(expectedValues); - for (Expression fact : linkedConjuncts(facts, VCSimplificationUtils::termsOf, expectedTerms)) { - List values = valueVariablesOf(fact); + for (Expression fact : linkedConjuncts(factsOf(chain), VCSimplificationUtils::termsOf, expectedTerms)) for (String name : variablesOf(fact)) - if ((values.contains(name) || primitives.contains(name)) && !expectedTerms.contains(name)) + if (!expectedTerms.contains(name) && hasOwnValue(name, fact, primitives)) keep.add(name); - } if (keepExpected) for (String name : expectedTerms) - if (primitives.contains(name)) + 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 4c0439911..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,8 +5,6 @@ import static liquidjava.rj_language.opt.VCSimplificationUtils.isFalse; import static liquidjava.rj_language.opt.VCSimplificationUtils.isTrue; -import java.util.ArrayList; -import java.util.List; import java.util.Set; import liquidjava.processor.VCImplication; @@ -38,10 +36,7 @@ public VCBinderSimplification(NeededVariables needed) { @Override public VCImplication apply(VCImplication implication) { VCImplication cloned = implication.clone(); - Set keptTrueBinders = needed.trueBindersToKeep(cloned); - VCImplication simplified = simplify(cloned, keptTrueBinders); - if (simplified == null) - simplified = moveTrueBinderBeforeFirstUse(cloned); + VCImplication simplified = simplify(cloned, needed.trueBindersToKeep(cloned)); return simplified == null ? cloned : simplified; } @@ -96,43 +91,6 @@ private boolean isRemovableBinder(VCImplication implication, Set keptTru return !containsVar(implication.getNext(), implication.getName()) && isUnusedFreshPathBinder(implication); } - /** - * Moves the first 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 - */ - private VCImplication moveTrueBinderBeforeFirstUse(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 (!isTrueBinder(binder)) - 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 null; - } - - private 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; - } - /** * Checks for a generated boolean path binder refined exactly by itself */ 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 82705505e..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 @@ -58,7 +58,7 @@ private static VCSimplificationResult simplifyOnce(VCSimplificationResult implic 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 VCConstraintSimplification(), new VCBinderOrdering()); } /** 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 00f65f224..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 @@ -72,21 +72,25 @@ public static List splitConjuncts(Expression expression) { } 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 (expression instanceof UnaryExpression not && "!".equals(not.getOp()) - && not.getExpression()instanceof BinaryExpression binary && "||".equals(binary.getOperator())) { + } else if (negated instanceof BinaryExpression binary && "||".equals(binary.getOperator())) { addConjuncts(new UnaryExpression("!", binary.getFirstOperand()), conjuncts); addConjuncts(new UnaryExpression("!", binary.getSecondOperand()), conjuncts); - } else if (expression instanceof UnaryExpression not && "!".equals(not.getOp()) - && not.getExpression()instanceof UnaryExpression inner && "!".equals(inner.getOp())) { - addConjuncts(inner.getExpression(), 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 diff --git a/liquidjava-verifier/src/main/java/liquidjava/utils/Utils.java b/liquidjava-verifier/src/main/java/liquidjava/utils/Utils.java index 94b973f0a..b85809e02 100644 --- a/liquidjava-verifier/src/main/java/liquidjava/utils/Utils.java +++ b/liquidjava-verifier/src/main/java/liquidjava/utils/Utils.java @@ -8,7 +8,7 @@ import java.util.Set; import java.util.stream.Stream; -import liquidjava.rj_language.ast.formatter.VariableFormatter; +import liquidjava.rj_language.ast.formatter.FieldDisplayNames; import liquidjava.utils.constants.Types; import spoon.reflect.code.CtAssignment; import spoon.reflect.code.CtBlock; @@ -62,12 +62,16 @@ 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(); String name = "this#" + field.getDeclaringType().getQualifiedName() + "." + field.getSimpleName(); if (field.isStatic()) - VariableFormatter.registerStaticField(name); + FieldDisplayNames.recordStaticField(name); return name; } 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 8c955e457..3cf797062 100644 --- a/liquidjava-verifier/src/test/java/liquidjava/api/tests/TestFoundBinders.java +++ b/liquidjava-verifier/src/test/java/liquidjava/api/tests/TestFoundBinders.java @@ -14,23 +14,17 @@ import liquidjava.diagnostics.Diagnostics; import liquidjava.diagnostics.errors.LJError; import liquidjava.diagnostics.errors.RefinementError; -import liquidjava.diagnostics.errors.StateRefinementError; import liquidjava.processor.VCImplication; import liquidjava.rj_language.ast.formatter.VariableFormatter; import liquidjava.rj_language.opt.VCSimplificationResult; /** - * Checks the rows of Found: a binder refined only by true is shown only when the error needs it, and fields are written - * as in code + * 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 String TEST_SUITE = "../liquidjava-example/src/main/java/testSuite/"; - - private static Map basket; - private static Map fieldState; - private static Map pathDependentState; - private static Map otherObjectWrite; + 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 @@ -44,171 +38,52 @@ private record Shown(List rows, String message, String counterexample, L @BeforeAll static void verify() { // shown as the IDE gets it: right after the verification, before the next one starts - basket = verify("classes/found_true_binders_error"); - fieldState = verify("classes/found_field_state_error"); - pathDependentState = verify("ErrorStateHintPathDependent.java"); - otherObjectWrite = verify("ErrorOtherObjectFieldWrite.java"); - } - - @Test - void basketHasOneErrorPerCase() { - assertEquals(List.of(25, 30, 36, 49, 56, 62, 67, 76, 82, 88, 96, 104, 111, 117), - new ArrayList<>(basket.keySet())); + 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 trueFieldRowOfTheIssueIsDropped() { - Shown shown = basket.get(25); + void issueReproducerDropsTheTrueFieldRow() { + Shown shown = ERRORS.get(25); assertEquals(List.of("∀bound bound == size(this.items) && bound >= 0"), shown.rows()); assertEquals("bound == size(this.items) && bound >= 0 is not a subtype of bound > 0", shown.message()); - assertEquals("Counterexample: bound == 0", shown.counterexample()); } @Test void steppingBackReachesTheOriginalWithTheDroppedRow() { - Shown shown = basket.get(25); + 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_true_binders_error.Basket.items", "#items_", "#bound_"), + assertEquals(List.of("this#testSuite.classes.found_binders_error.Basket.items", "#items_", "#bound_"), shown.originalBinders()); } - @Test - void trueParameterRowIsDropped() { - assertEquals(List.of("∀bound bound == size(list) && bound >= 0"), basket.get(30).rows()); - } - - @Test - void trueCallResultRowIsDropped() { - assertEquals(List.of("∀bound bound == size(copyItems) && bound >= 0"), basket.get(36).rows()); - } - - @Test - void trueLocalRowIsDropped() { - assertEquals(List.of("∀bound bound == size(local) && bound >= 0"), basket.get(49).rows()); - } - - @Test - void severalTrueFieldRowsAreDroppedAndReadWithOrWithoutThisAlike() { - assertEquals( - List.of("∀first first == size(this.items) && first >= 0", - "∀second second == size(this.extras) && second >= 0", "∀bound bound == first + second"), - basket.get(56).rows()); - } - - @Test - void trueRowLinkedToExpectedThroughALaterRowIsKept() { - Shown shown = basket.get(62); - assertEquals(List.of("∀x true", "∀y y == x + 1"), shown.rows()); - assertEquals("Counterexample: x == -1 && y == 0", shown.counterexample()); - } - - @Test - void trueRowOfTheExpectedVariableIsKept() { - Shown shown = basket.get(67); - assertEquals(List.of("∀x true"), shown.rows()); - assertEquals("true is not a subtype of x > 0", shown.message()); - } - @Test void staticFieldIsWrittenWithItsClass() { - Shown shown = basket.get(76); + Shown shown = ERRORS.get(31); assertEquals(List.of("∀Basket.served true", "∀count count == Basket.served + 1"), shown.rows()); - assertEquals("count == Basket.served + 1 is not a subtype of count > 0", shown.message()); assertEquals("Counterexample: Basket.served == -1 && count == 0", shown.counterexample()); } @Test - void fieldReadWithThisIsWrittenAsInCode() { - Shown shown = basket.get(82); - assertEquals(List.of("∀this.amount true", "∀a a == this.amount"), shown.rows()); - assertEquals("a == this.amount is not a subtype of a > 0", shown.message()); - assertEquals("Counterexample: this.amount == 0 && a == 0", shown.counterexample()); - } - - @Test - void fieldReadWithoutThisIsWrittenTheSameWay() { - Shown withThis = basket.get(82); - Shown withoutThis = basket.get(88); - assertEquals(withThis.rows(), withoutThis.rows()); - assertEquals(withThis.message(), withoutThis.message()); - assertEquals(withThis.counterexample(), withoutThis.counterexample()); - } - - @Test - void fieldOfAnInnerClassIsWrittenAsInCode() { - assertEquals(List.of("∀bound bound == size(this.names) && bound >= 0"), basket.get(96).rows()); - } - - @Test - void trueRowUsedOnlyByAnUnrelatedGuardIsDropped() { - Shown shown = basket.get(104); - assertEquals(List.of("∀#fresh !(port < 0)", "∀t true"), shown.rows()); - assertEquals(List.of("∀port true", "∀#fresh !(port < 0)", "∀t true"), shown.originalRows()); - } - - @Test - void trueRowsOfACombinedGuardAreNotLinkedToExpected() { - assertEquals(List.of("∀#fresh !(p || q)", "∀t true"), basket.get(111).rows()); - } - - @Test - void keptTrueRowComesBeforeTheRowUsingIt() { - assertEquals(List.of("∀Basket.served true", "∀i true", "∀#fresh i < Basket.served"), basket.get(117).rows()); - } - - @Test - void trueRowDecidingAPathDependentStateIsKept() { - Shown shown = pathDependentState.get(25); - assertEquals(List.of("∀ready true", "∀f ready ? open(f) : created(f)"), shown.rows()); - } - - @Test - void writesToAnotherObjectsFieldAreCheckedAsOnMain() { - // other.level++ and other.level += 1 verify, other.level-- and the write through an alias of this are reported - assertEquals(List.of(11, 23, 31, 35), new ArrayList<>(otherObjectWrite.keySet())); - assertEquals("k == 7", otherObjectWrite.get(31).message().replaceAll(".* is not a subtype of ", "")); - } - - @Test - void writeToAnotherObjectsFieldIsWrittenWithThatObject() { - assertEquals("other.level == -1 is not a subtype of other.level >= 0", otherObjectWrite.get(11).message()); + 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"), - otherObjectWrite.get(23).rows()); - assertEquals("this.level == -1 is not a subtype of this.level >= 0", otherObjectWrite.get(35).message()); - } - - @Test - void fieldRowHoldingAStateIsKept() { - assertEquals(List.of(14), new ArrayList<>(fieldState.keySet())); - Shown shown = fieldState.get(14); - assertEquals( - List.of("∀#fresh !(intrNumber < 0 || intrNumber >= 67)", "∀this.interrupts empty(this.interrupts)"), - shown.rows()); - assertEquals("found !(intrNumber < 0 || intrNumber >= 67) && empty(this.interrupts) but expected " - + "maybeElements(this.interrupts)", shown.message()); - } - - private static Map verify(String test) { - CommandLineLauncher.launch(TEST_SUITE + test); - Map shown = new TreeMap<>(); - for (LJError error : Diagnostics.getInstance().getErrors()) { - VCSimplificationResult found = error instanceof RefinementError refinementError ? refinementError.getFound() - : assertInstanceOf(StateRefinementError.class, error).getFoundSimplification(); - 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(); - shown.put(error.getPosition().getLine(), - new Shown(rows(found.getImplication()), plain(error.getMessage()), - error.getCounterexampleStr() == null ? null : plain(error.getCounterexampleStr()), - rows(original.getImplication()), steps, originalBinders)); - } - return shown; + ERRORS.get(48).rows()); } // the rows of Found as the IDE writes them: binder name, then its refinement 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 f5c630eab..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 @@ -51,13 +51,4 @@ void writesFieldsAsInCodeNextToALocalOfTheSameName() { assertEquals("items⁵ == this.items", expression.toDisplayString()); } - - @Test - void writesFieldsAsInCodeInsideFunctionArguments() { - Predicate size = Predicate.createInvocation("java.util.ArrayList.size", - Predicate.createVar("this#shop.Basket.items")); - Expression expression = Predicate.createEquals(Predicate.createVar("#bound_6"), size).getExpression(); - - assertEquals("bound⁶ == size(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 2d8028ebe..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 @@ -1,8 +1,6 @@ package liquidjava.rj_language.ast.formatter; import static org.junit.jupiter.api.Assertions.assertEquals; -import static org.junit.jupiter.api.Assertions.assertFalse; -import static org.junit.jupiter.api.Assertions.assertTrue; import org.junit.jupiter.api.AfterEach; import org.junit.jupiter.api.Test; @@ -10,8 +8,8 @@ class VariableFormatterTest { @AfterEach - void forgetStaticFields() { - VariableFormatter.clearStaticFields(); + void forgetRecordedNames() { + FieldDisplayNames.clear(); } @Test @@ -34,49 +32,21 @@ void formatsVariables() { @Test void writesInstanceFieldsAsInCode() { assertEquals("this.items", VariableFormatter.format("this#shop.Basket.items")); - assertEquals("this.items", VariableFormatter.format("this#Basket.items")); - assertEquals("this.interrupts⁴⁷⁵", VariableFormatter - .format("#this#x_e_oss_a1_17_interruptmanager.E_OSS_A1_17_InterruptManager.interrupts_475")); - assertEquals("this.port", VariableFormatter.format("this#pkg.Outer$Job.port")); + assertEquals("this.port⁴", VariableFormatter.format("#this#pkg.Outer$Job.port_4")); } @Test void writesStaticFieldsWithTheirClass() { - VariableFormatter.registerStaticField("this#shop.Basket.served"); - VariableFormatter.registerStaticField("this#pkg.Outer$Job.count"); - assertEquals("Basket.served", VariableFormatter.format("this#shop.Basket.served")); - assertEquals("Basket.served³", VariableFormatter.format("#this#shop.Basket.served_3")); - assertEquals("Job.count", VariableFormatter.format("this#pkg.Outer$Job.count")); - assertEquals("this.items", VariableFormatter.format("this#shop.Basket.items")); - } - - @Test - void forgetsStaticFieldsOfThePreviousVerification() { - VariableFormatter.registerStaticField("this#shop.Basket.served"); - VariableFormatter.clearStaticFields(); - assertEquals("this.served", VariableFormatter.format("this#shop.Basket.served")); - } - - @Test - void writesAnInstanceCreatedByAWriteThroughAnotherObjectWithThatObject() { - VariableFormatter.registerReceiver("#this#otherwrite.W.level_1", "other"); - VariableFormatter.registerReceiver("#this#otherwrite.W.level_2", ""); - assertEquals("other.level¹", VariableFormatter.format("#this#otherwrite.W.level_1")); - assertEquals("level²", VariableFormatter.format("#this#otherwrite.W.level_2")); - assertEquals("this.level³", VariableFormatter.format("#this#otherwrite.W.level_3")); - assertEquals("this.level", VariableFormatter.format("this#otherwrite.W.level")); - VariableFormatter.clearStaticFields(); - assertEquals("this.level¹", VariableFormatter.format("#this#otherwrite.W.level_1")); + FieldDisplayNames.recordStaticField("this#pkg.Outer$Job.count"); + assertEquals("Job.count³", VariableFormatter.format("#this#pkg.Outer$Job.count_3")); } @Test - void recognisesFieldNames() { - assertTrue(VariableFormatter.isField("this#shop.Basket.items")); - assertTrue(VariableFormatter.isField("#this#shop.Basket.items_4")); - assertFalse(VariableFormatter.isField("other#otherwrite.W.level")); - assertFalse(VariableFormatter.isField("this#Basket")); - assertFalse(VariableFormatter.isField("#this_4")); - assertFalse(VariableFormatter.isField("items")); - assertFalse(VariableFormatter.isField("java.util.ArrayList.size")); + 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 12eba8c89..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,31 +1,26 @@ package liquidjava.rj_language.opt; import static liquidjava.utils.VCTestUtils.*; -import static org.junit.jupiter.api.Assertions.assertEquals; - -import java.util.List; -import java.util.Set; import org.junit.jupiter.api.Test; -import liquidjava.processor.VCImplication; import liquidjava.rj_language.Predicate; import liquidjava.rj_language.parsing.RefinementsParser; -import spoon.Launcher; -import spoon.reflect.factory.TypeFactory; class VCBinderSimplificationTest { private final VCBinderSimplification binderSimplification = new VCBinderSimplification(); - private static final TypeFactory TYPES = new Launcher().getFactory().Type(); + private static VCBinderSimplification forRefinementError(String expected) { + return new VCBinderSimplification(NeededVariables.forRefinementError(predicate(expected))); + } - private static VCBinderSimplification forRefinementError(String... expected) { - return new VCBinderSimplification(new NeededVariables(Set.of(expected), Set.of(expected), true)); + private static VCBinderSimplification forStateError(String expected) { + return new VCBinderSimplification(NeededVariables.forStateError(predicate(expected))); } - private static VCBinderSimplification forStateError(String... expected) { - return new VCBinderSimplification(new NeededVariables(Set.of(expected), Set.of(expected), false)); + private static Predicate predicate(String refinement) { + return new Predicate(RefinementsParser.createAST(refinement, "")); } @Test @@ -53,103 +48,49 @@ void removesTrueBinderUsedDownstreamWhenNothingNeedsIt() { assertSimplificationSteps(binderSimplification, vc("∀x:int. true", "x > 0"), step("x > 0")); } - @Test - void removesTrueFieldBinderUsedDownstreamWhenNothingNeedsIt() { - VCImplication field = new VCImplication("this#shop.Basket.items", TYPES.INTEGER_PRIMITIVE, new Predicate()); - field.setNext(new VCImplication("#bound_6", TYPES.INTEGER_PRIMITIVE, - Predicate.createEquals(Predicate.createVar("#bound_6"), Predicate.createOperation( - Predicate.createVar("this#shop.Basket.items"), "+", Predicate.createLit("1", "int"))))); - assertSimplificationSteps(binderSimplification, field, step("bound⁶ == this.items + 1")); - } - @Test void keepsTrueBinderLinkedToExpectedThroughALaterRow() { - assertSimplificationSteps(forRefinementError("y"), vc("∀x:int. true", "∀y:int. y == x + 1"), + assertSimplificationSteps(forRefinementError("y > 0"), vc("∀x:int. true", "∀y:int. y == x + 1"), step("true", "y == x + 1")); } @Test void keepsTrueBinderLinkedToExpectedThroughSeveralRows() { - assertSimplificationSteps(forRefinementError("z"), vc("∀x:int. true", "∀y:int. y == x + 1", "∀z:int. z == y"), - step("true", "y == x + 1", "z == y")); + 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 removesTrueBinderUsedOnlyByARowUnlinkedToExpected() { - assertSimplificationSteps(forRefinementError("t"), vc("∀port:int. true", "!(port < 0)", "∀t:int. true"), - step("!(port < 0)", "true")); - } - - @Test - void splitsANegatedDisjunctionSoOneGuardDoesNotLinkItsParts() { - assertSimplificationSteps(forRefinementError("t"), vc("∀p:boolean. true", "∀t:int. true", "!(p || t < 0)"), - step("true", "!(p || t < 0)")); + 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"), vc("∀x:int. true", "y > 0"), step("true", "y > 0")); - } - - @Test - void keepsTerminalTrueBinderOfExpectedVariableInRefinementError() { - VCSimplificationResult result = assertSimplificationSteps(forRefinementError("x"), vc("∀x:int. true"), - step("true")); - assertEquals(List.of("x"), result.getBinders()); + assertSimplificationSteps(forRefinementError("x > 0"), vc("∀x:int. true", "y > 0"), step("true", "y > 0")); } @Test void removesTrueBinderOfExpectedVariableInStateError() { - assertSimplificationSteps(forStateError("x"), vc("∀x:int. true", "y > 0"), step("y > 0")); - } - - @Test - void keepsTrueBinderLinkedToExpectedInStateError() { - assertSimplificationSteps(forStateError("f"), vc("∀ready:boolean. true", "∀f:int. ready ? f > 0 : f < 0"), - step("true", "ready ? f > 0 : f < 0")); - } - - @Test - void removesOnlyTheTrueBindersNothingLinks() { - assertSimplificationSteps(forRefinementError("y"), - vc("∀a:int. true", "∀c:int. true", "∀w:int. w > a", "∀y:int. y == c"), step("true", "w > a", "y == c")); - } - - @Test - void movesKeptTrueBinderBeforeItsFirstUse() { - VCSimplificationResult result = assertSimplificationSteps(forRefinementError("i"), - vc("∀y:int. y < i", "∀i:int. true"), step("true", "y < i")); - assertEquals(List.of("i", "y"), result.getBinders()); - } - - @Test - void removesTrueBinderNamedOnlyAsTheObjectOfAGhost() { - assertSimplificationSteps(forRefinementError("b"), vc("∀x:Object. true", "∀b:int. b == size(x) && b >= 0"), - step("b == size(x) && b >= 0")); + assertSimplificationSteps(forStateError("x > 0"), vc("∀x:int. true", "y > 0"), step("y > 0")); } @Test void keepsPrimitiveTrueBinderThatIsTheArgumentOfAGhost() { - assertSimplificationSteps(forRefinementError("y"), vc("∀k:int. true", "∀y:int. y == f(k)"), + 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)", "f"), - vc("∀ready:boolean. true", "∀f:int. true", "ready ? open(f) : created(f)"), + assertSimplificationSteps(forStateError("open(f)"), + vc("∀ready:boolean. true", "∀f:Object. true", "ready ? open(f) : created(f)"), step("true", "ready ? open(f) : created(f)")); } - @Test - void neededVariablesComeFromExpected() { - Predicate expected = new Predicate(RefinementsParser.createAST("x > size(y)", "")); - assertEquals(new NeededVariables(Set.of("x", "y", "size(y)"), Set.of("x"), true), - NeededVariables.forRefinementError(expected)); - assertEquals(new NeededVariables(Set.of("x", "y", "size(y)"), Set.of("x"), false), - NeededVariables.forStateError(expected)); - } - @Test void collapsesFalseBinderSuffixToPlainTrue() { assertSimplificationSteps(binderSimplification, vc("∀x:int. false", "y > 0"), step("true")); @@ -163,7 +104,7 @@ void simplifiesOnlyFirstApplicableBinder() { @Test void skipsInapplicableTrueBinderAndSimplifiesLaterBinder() { - assertSimplificationSteps(forRefinementError("x"), 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/rj_language/opt/VCSimplificationUtilsTest.java b/liquidjava-verifier/src/test/java/liquidjava/rj_language/opt/VCSimplificationUtilsTest.java deleted file mode 100644 index dc5c781cd..000000000 --- a/liquidjava-verifier/src/test/java/liquidjava/rj_language/opt/VCSimplificationUtilsTest.java +++ /dev/null @@ -1,46 +0,0 @@ -package liquidjava.rj_language.opt; - -import static org.junit.jupiter.api.Assertions.assertEquals; - -import java.util.List; - -import org.junit.jupiter.api.Test; - -import liquidjava.rj_language.ast.Expression; -import liquidjava.rj_language.parsing.RefinementsParser; - -class VCSimplificationUtilsTest { - - private static Expression parse(String refinement) { - return RefinementsParser.createAST(refinement, ""); - } - - private static List display(List expressions) { - return expressions.stream().map(Expression::toDisplayString).toList(); - } - - @Test - void splitsConjunctionsAndNegatedDisjunctions() { - assertEquals(List.of("!a", "!(b > 0)", "c", "d"), - display(VCSimplificationUtils.splitConjuncts(parse("!(a || b > 0) && c && !!d")))); - } - - @Test - void keepsDisjunctionsAndNegatedConjunctionsWhole() { - assertEquals(List.of("a || b", "!(c && d)"), - display(VCSimplificationUtils.splitConjuncts(parse("(a || b) && !(c && d)")))); - } - - @Test - void linksConjunctsSharingVariablesWithTheSeedTransitively() { - List conjuncts = List.of(parse("y == x + 1"), parse("p"), parse("x > z"), parse("q == p")); - assertEquals(List.of("y == x + 1", "x > z"), display( - VCSimplificationUtils.linkedConjuncts(conjuncts, VCSimplificationUtils::variablesOf, List.of("y")))); - } - - @Test - void linksNothingWithoutASharedVariable() { - assertEquals(List.of(), VCSimplificationUtils.linkedConjuncts(List.of(parse("p && q")), - VCSimplificationUtils::variablesOf, List.of("t"))); - } -} From a56f0d11a9c306a6e9c0aeb40ef75137d18fe490 Mon Sep 17 00:00:00 2001 From: Catarina Gamboa Date: Tue, 3 Nov 2026 19:12:21 +0000 Subject: [PATCH 5/5] List expected's values first in the static field counterexample, as main now does Co-Authored-By: Claude Opus 5.5 --- .../src/test/java/liquidjava/api/tests/TestFoundBinders.java | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) 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 3cf797062..549cba700 100644 --- a/liquidjava-verifier/src/test/java/liquidjava/api/tests/TestFoundBinders.java +++ b/liquidjava-verifier/src/test/java/liquidjava/api/tests/TestFoundBinders.java @@ -76,7 +76,7 @@ void steppingBackReachesTheOriginalWithTheDroppedRow() { void staticFieldIsWrittenWithItsClass() { Shown shown = ERRORS.get(31); assertEquals(List.of("∀Basket.served true", "∀count count == Basket.served + 1"), shown.rows()); - assertEquals("Counterexample: Basket.served == -1 && count == 0", shown.counterexample()); + assertEquals("Counterexample: count == 0 && Basket.served == -1", shown.counterexample()); } @Test