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