From c99ef2404a88b7e42c9d617bdb7c0a80fd82eb8d Mon Sep 17 00:00:00 2001 From: Catarina Gamboa Date: Tue, 3 Nov 2026 21:43:57 +0000 Subject: [PATCH] Drop true binders that another row already shows A binder refined only by true states no fact. When another row of Found mentions its variable, the variable is already shown there and the true row only reads as if its value were true. Keep such a row only in a refinement error, for a variable whose value expected constrains and that no other row mentions: it then shows that nothing is known about a value the error depends on. This removes the linking to expected that kept getUndoManager, the parameters of a conditional state and enum constants, and the binder ordering pass that only moved those kept rows. Co-Authored-By: Claude Opus 5.5 --- .../classes/found_binders_error/Basket.java | 15 ++++- .../rj_language/opt/NeededVariables.java | 53 +++++----------- .../rj_language/opt/VCBinderOrdering.java | 54 ---------------- .../rj_language/opt/VCSimplification.java | 2 +- .../opt/VCSimplificationUtils.java | 61 ------------------- .../api/tests/TestFoundBinders.java | 16 ++++- .../rj_language/opt/VCBinderOrderingTest.java | 18 ------ .../opt/VCBinderSimplificationTest.java | 31 ++++------ 8 files changed, 55 insertions(+), 195 deletions(-) delete mode 100644 liquidjava-verifier/src/main/java/liquidjava/rj_language/opt/VCBinderOrdering.java delete mode 100644 liquidjava-verifier/src/test/java/liquidjava/rj_language/opt/VCBinderOrderingTest.java diff --git a/liquidjava-example/src/main/java/testSuite/classes/found_binders_error/Basket.java b/liquidjava-example/src/main/java/testSuite/classes/found_binders_error/Basket.java index 8de52455..683d4ce5 100644 --- a/liquidjava-example/src/main/java/testSuite/classes/found_binders_error/Basket.java +++ b/liquidjava-example/src/main/java/testSuite/classes/found_binders_error/Basket.java @@ -5,7 +5,7 @@ import liquidjava.specification.Refinement; -// Found drops the true rows the error does not need and writes fields as in code (#457) +// Found drops the true rows the error does not need and writes fields as in code (#457, #375) public class Basket { static int served; @@ -55,4 +55,17 @@ void writeThroughAlias() { @Refinement("_ == 7") int k = level; // Expect: Refinement Error } + + static void positive(@Refinement("_ > 0") int t) {} + + // parameters that another row already shows get no true row + void addUp(int first, int second) { + @Refinement("_ > 0") + int sum = first + second; // Expect: Refinement Error + } + + // a variable only expected names keeps its true row: nothing is known about it + void forward(int t) { + positive(t); // Expect: Refinement Error + } } 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 1c168035..eb0c7d9a 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,15 +1,10 @@ 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.containsVar; import static liquidjava.rj_language.opt.VCSimplificationUtils.termsOf; import static liquidjava.rj_language.opt.VCSimplificationUtils.valueVariablesOf; -import static liquidjava.rj_language.opt.VCSimplificationUtils.variablesOf; -import java.util.ArrayList; import java.util.HashSet; -import java.util.List; import java.util.Set; import liquidjava.processor.VCImplication; @@ -18,16 +13,16 @@ /** * 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 + * fact, and a variable that another row mentions is already shown there, so its row would only read as if its value + * were true. It is kept only when the error shows a counterexample, expected constrains the variable's value and no + * other row mentions it: the row then shows that nothing is known about a value the error depends on * * @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 + * whether the binders of expectedValues that no other row mentions are kept */ public record NeededVariables(Set expectedTerms, Set expectedValues, boolean keepExpected) { @@ -39,7 +34,7 @@ public record NeededVariables(Set expectedTerms, Set expectedVal } /** - * For a refinement error, whose counterexample lists the values of the binders + * For a refinement error, which shows a counterexample */ public static NeededVariables forRefinementError(Predicate expected) { return of(expected, true); @@ -59,40 +54,20 @@ 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, and, when {@code keepExpected}, those whose value expected constrains + * Variables whose binder refined only by true the chain keeps: when {@code keepExpected}, those whose value + * expected constrains and that no other row of the chain mentions */ public Set trueBindersToKeep(VCImplication chain) { - Set primitives = primitiveBinders(chain); Set keep = new HashSet<>(); - for (Expression fact : linkedConjuncts(factsOf(chain), VCSimplificationUtils::termsOf, expectedTerms)) - for (String name : variablesOf(fact)) - if (!expectedTerms.contains(name) && hasOwnValue(name, fact, primitives)) - keep.add(name); - if (keepExpected) - for (String name : expectedTerms) - if (expectedValues.contains(name) || primitives.contains(name)) - keep.add(name); + if (!keepExpected) + return keep; + Set primitives = primitiveBinders(chain); + for (String name : expectedTerms) + if ((expectedValues.contains(name) || primitives.contains(name)) && !containsVar(chain, 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()) 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 deleted file mode 100644 index 9c2a1e8c..00000000 --- a/liquidjava-verifier/src/main/java/liquidjava/rj_language/opt/VCBinderOrdering.java +++ /dev/null @@ -1,54 +0,0 @@ -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/VCSimplification.java b/liquidjava-verifier/src/main/java/liquidjava/rj_language/opt/VCSimplification.java index 7eb8d6df..82705505 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 VCBinderOrdering()); + new VCConstraintSimplification()); } /** 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 bb31fb78..5f0be3bf 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,19 +1,13 @@ 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 { @@ -61,61 +55,6 @@ public static boolean isFalse(Expression expression) { return expression instanceof LiteralBoolean literal && !literal.isBooleanTrue(); } - /** - * Splits an expression into the facts it states together: the operands of {@code &&}, and of a negated disjunction - * {@code !(a || b)}, which states {@code !a} and {@code !b} - */ - public static List splitConjuncts(Expression expression) { - List conjuncts = new ArrayList<>(); - addConjuncts(expression, conjuncts); - return conjuncts; - } - - private static void addConjuncts(Expression expression, List conjuncts) { - Expression negated = negatedOperand(expression); - if (expression instanceof BinaryExpression binary && "&&".equals(binary.getOperator())) { - addConjuncts(binary.getFirstOperand(), conjuncts); - addConjuncts(binary.getSecondOperand(), conjuncts); - } else if (negated instanceof BinaryExpression binary && "||".equals(binary.getOperator())) { - addConjuncts(new UnaryExpression("!", binary.getFirstOperand()), conjuncts); - addConjuncts(new UnaryExpression("!", binary.getSecondOperand()), conjuncts); - } else if (negatedOperand(negated) != null) { - addConjuncts(negatedOperand(negated), conjuncts); - } else { - conjuncts.add(expression); - } - } - - // the operand of !e, or null for any other expression - private static Expression negatedOperand(Expression expression) { - return expression instanceof UnaryExpression not && "!".equals(not.getOp()) ? not.getExpression() : null; - } - - /** - * Returns the conjuncts linked to the seed terms: those sharing a term with the seed, directly or through other - * linked conjuncts. The remaining conjuncts only constrain values that the seed does not depend on - */ - public static List linkedConjuncts(List conjuncts, - Function> termsOf, Collection seed) { - Set linkedTerms = new HashSet<>(seed); - List linked = new ArrayList<>(); - List unlinked = new ArrayList<>(conjuncts); - boolean changed = true; - while (changed) { - changed = false; - for (Expression conjunct : List.copyOf(unlinked)) { - Collection terms = termsOf.apply(conjunct); - if (terms.stream().anyMatch(linkedTerms::contains)) { - linkedTerms.addAll(terms); - linked.add(conjunct); - unlinked.remove(conjunct); - changed = true; - } - } - } - return linked; - } - /** * Variable names of an expression */ 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 549cba70..6f5d44ff 100644 --- a/liquidjava-verifier/src/test/java/liquidjava/api/tests/TestFoundBinders.java +++ b/liquidjava-verifier/src/test/java/liquidjava/api/tests/TestFoundBinders.java @@ -75,10 +75,24 @@ void steppingBackReachesTheOriginalWithTheDroppedRow() { @Test void staticFieldIsWrittenWithItsClass() { Shown shown = ERRORS.get(31); - assertEquals(List.of("∀Basket.served true", "∀count count == Basket.served + 1"), shown.rows()); + assertEquals(List.of("∀count count == Basket.served + 1"), shown.rows()); assertEquals("Counterexample: count == 0 && Basket.served == -1", shown.counterexample()); } + @Test + void variablesAnotherRowShowsGetNoTrueRow() { + Shown shown = ERRORS.get(64); + assertEquals(List.of("∀sum sum == first + second"), shown.rows()); + assertEquals("Counterexample: sum == 0 && first == 0 && second == 0", shown.counterexample()); + } + + @Test + void variableOnlyExpectedNamesKeepsItsTrueRow() { + Shown shown = ERRORS.get(69); + assertEquals(List.of("∀t true"), shown.rows()); + assertEquals("Counterexample: t == 0", shown.counterexample()); + } + @Test void writeToAnotherObjectsFieldIsNamedAfterThatObject() { assertEquals("other.level == -1 is not a subtype of other.level >= 0", ERRORS.get(36).message()); 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 deleted file mode 100644 index adb272b0..00000000 --- a/liquidjava-verifier/src/test/java/liquidjava/rj_language/opt/VCBinderOrderingTest.java +++ /dev/null @@ -1,18 +0,0 @@ -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 5a0ee82a..417fe864 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 @@ -49,27 +49,18 @@ void removesTrueBinderUsedDownstreamWhenNothingNeedsIt() { } @Test - void keepsTrueBinderLinkedToExpectedThroughALaterRow() { + void removesTrueBinderThatALaterRowShows() { assertSimplificationSteps(forRefinementError("y > 0"), vc("∀x:int. true", "∀y:int. y == x + 1"), - step("true", "y == x + 1")); + step("y == x + 1")); } @Test - void keepsTrueBinderLinkedToExpectedThroughSeveralRows() { - assertSimplificationSteps(forRefinementError("z > 0"), - vc("∀x:int. true", "∀y:int. y == x + 1", "∀z:int. z == y"), step("true", "y == x + 1", "z == y")); + void removesTrueBinderOfExpectedVariableThatAnotherRowShows() { + assertSimplificationSteps(forRefinementError("x > 0"), vc("∀x:int. true", "x != 0"), step("x != 0")); } @Test - void removesTrueBindersOnlyAnUnlinkedGuardUses() { - // one guard !(p || t < 0) states !p and !(t < 0) apart, so only the second is linked to t - assertSimplificationSteps(forRefinementError("t > 0"), - vc("∀port:int. true", "∀p:boolean. true", "!(port < 0)", "!(p || t < 0)", "∀t:int. true"), - step("true", "!(port < 0)", "!(p || t < 0)", "true"), step("!(port < 0)", "!(p || t < 0)", "true")); - } - - @Test - void keepsTrueBinderOfExpectedVariableInRefinementError() { + void keepsTrueBinderOfExpectedVariableNoOtherRowMentions() { assertSimplificationSteps(forRefinementError("x > 0"), vc("∀x:int. true", "y > 0"), step("true", "y > 0")); } @@ -79,16 +70,16 @@ void removesTrueBinderOfExpectedVariableInStateError() { } @Test - void keepsPrimitiveTrueBinderThatIsTheArgumentOfAGhost() { + void removesTrueBinderThatIsTheArgumentOfAGhost() { assertSimplificationSteps(forRefinementError("y > 0"), vc("∀k:int. true", "∀y:int. y == f(k)"), - step("true", "y == f(k)")); + step("y == f(k)")); } @Test - void linksThroughGhostApplicationsButKeepsOnlyValueVariables() { + void removesTrueBindersThatAConditionalStateShows() { assertSimplificationSteps(forStateError("open(f)"), vc("∀ready:boolean. true", "∀f:Object. true", "ready ? open(f) : created(f)"), - step("true", "ready ? open(f) : created(f)")); + step("true", "ready ? open(f) : created(f)"), step("ready ? open(f) : created(f)")); } @Test @@ -104,8 +95,8 @@ void simplifiesOnlyFirstApplicableBinder() { @Test void skipsInapplicableTrueBinderAndSimplifiesLaterBinder() { - assertSimplificationSteps(forRefinementError("x > 0"), vc("∀x:int. true", "x > 0", "∀y:int. true", "z > 0"), - step("true", "x > 0", "z > 0")); + assertSimplificationSteps(forRefinementError("x > 0"), vc("∀x:int. true", "w > 0", "∀y:int. true", "z > 0"), + step("true", "w > 0", "z > 0")); } @Test