Drop true rows for variables that another row of Found already shows

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
+    }
 }

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<String> expectedTerms, Set<String> expectedValues, boolean keepExpected) {
 
@@ -39,7 +34,7 @@ public record NeededVariables(Set<String> expectedTerms, Set<String> 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<String> trueBindersToKeep(VCImplication chain) {
-        Set<String> primitives = primitiveBinders(chain);
         Set<String> 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<String> 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<String> primitives) {
-        return primitives.contains(name) || valueVariablesOf(fact).contains(name);
-    }
-
-    private static List<Expression> factsOf(VCImplication chain) {
-        List<Expression> 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<String> primitiveBinders(VCImplication chain) {
         Set<String> primitives = new HashSet<>();
         for (VCImplication current = chain; current != null; current = current.getNext())

liquidjava-verifier/src/main/java/liquidjava/rj_language/opt/VCSimplification.java

@@ -58,7 +58,7 @@ private static VCSimplificationResult simplifyOnce(VCSimplificationResult implic
     private static List<VCSimplificationPass> 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());
     }
 
     /**

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<Expression> splitConjuncts(Expression expression) {
-        List<Expression> conjuncts = new ArrayList<>();
-        addConjuncts(expression, conjuncts);
-        return conjuncts;
-    }
-
-    private static void addConjuncts(Expression expression, List<Expression> 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<Expression> linkedConjuncts(List<Expression> conjuncts,
-            Function<Expression, ? extends Collection<String>> termsOf, Collection<String> seed) {
-        Set<String> linkedTerms = new HashSet<>(seed);
-        List<Expression> linked = new ArrayList<>();
-        List<Expression> unlinked = new ArrayList<>(conjuncts);
-        boolean changed = true;
-        while (changed) {
-            changed = false;
-            for (Expression conjunct : List.copyOf(unlinked)) {
-                Collection<String> 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
      */

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());

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