From c95bb86a2e608523d6619a622913a090cec647ed Mon Sep 17 00:00:00 2001 From: Catarina Gamboa Date: Thu, 5 Nov 2026 12:59:53 +0000 Subject: [PATCH] Drop path conditions that expected does not depend on from Found A generated boolean binder (a path condition such as #if_condition) whose variable and refinement share no term with Expected, directly or through other facts, and that no other row mentions, is removed as a step of the Binder pass. The original chain the panel steps back to keeps it. The linking helpers (factsOf, linkedTerms, termsOf, termName, linkedToExpected) move from RefinementError to VCSimplificationUtils, so the simplified chain, the message and the counterexample link facts the same way. Co-Authored-By: Claude Opus 5.5 --- .../diagnostics/errors/RefinementError.java | 93 +------------------ .../errors/StateRefinementError.java | 3 +- .../rj_language/opt/NeededVariables.java | 35 ++++++- .../opt/VCBinderSimplification.java | 27 ++++-- .../opt/VCSimplificationUtils.java | 92 +++++++++++++++++- .../api/tests/TestGeneratedNames.java | 22 +++-- .../opt/VCBinderSimplificationTest.java | 28 ++++++ 7 files changed, 192 insertions(+), 108 deletions(-) diff --git a/liquidjava-verifier/src/main/java/liquidjava/diagnostics/errors/RefinementError.java b/liquidjava-verifier/src/main/java/liquidjava/diagnostics/errors/RefinementError.java index 22e275b8..36a2458a 100644 --- a/liquidjava-verifier/src/main/java/liquidjava/diagnostics/errors/RefinementError.java +++ b/liquidjava-verifier/src/main/java/liquidjava/diagnostics/errors/RefinementError.java @@ -3,7 +3,6 @@ import java.util.ArrayList; import java.util.Comparator; import java.util.HashSet; -import java.util.Iterator; import java.util.List; import java.util.Set; import java.util.stream.Collectors; @@ -15,9 +14,6 @@ import liquidjava.rj_language.ast.BinaryExpression; import liquidjava.rj_language.ast.Enum; 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; import liquidjava.rj_language.ast.formatter.VariableFormatter; import liquidjava.rj_language.opt.VCSimplificationResult; @@ -27,7 +23,12 @@ import liquidjava.utils.Utils; import spoon.reflect.cu.SourcePosition; +import static liquidjava.rj_language.opt.VCSimplificationUtils.factsOf; import static liquidjava.rj_language.opt.VCSimplificationUtils.isTrue; +import static liquidjava.rj_language.opt.VCSimplificationUtils.linkedTerms; +import static liquidjava.rj_language.opt.VCSimplificationUtils.linkedToExpected; +import static liquidjava.rj_language.opt.VCSimplificationUtils.termName; +import static liquidjava.rj_language.opt.VCSimplificationUtils.termsOf; /** * Error indicating that a refinement constraint either was violated or cannot be proven @@ -72,21 +73,6 @@ private static String message(Predicate expected, VCSimplificationResult found) expected.getExpression().toDisplayString()); } - /** - * The facts of found linked to the terms of expected, as a conjunction, or true when there are none; found as - * written when every fact is linked - */ - static Expression linkedToExpected(Expression found, Expression expected) { - List facts = factsOf(found); - Set linked = linkedTerms(facts, termsOf(expected)); - List linkedFacts = facts.stream().filter(fact -> termsOf(fact).stream().anyMatch(linked::contains)) - .toList(); - if (linkedFacts.size() == facts.size()) - return found; - return linkedFacts.stream().reduce((first, second) -> new BinaryExpression(first, "&&", second)) - .orElse(new LiteralBoolean(true)); - } - /** Unknown when what was found says nothing about the values the expected refinement constrains */ private static ErrorCategory categoryOf(Predicate expected, VCSimplificationResult found) { List foundVariables = found.getImplication().toPredicate().getVariableNames(); @@ -138,47 +124,6 @@ private Counterexample filterCounterexample(Counterexample counterexample) { .toList()); } - // Conjuncts of found, also splitting negated disjunctions (!(a || b) is !a && !b) and dropping double negations, so - // each fact links only the terms it relates - private static List factsOf(Expression expression) { - List facts = new ArrayList<>(); - if (expression instanceof BinaryExpression binary && "&&".equals(binary.getOperator())) { - facts.addAll(factsOf(binary.getFirstOperand())); - facts.addAll(factsOf(binary.getSecondOperand())); - } else if (expression instanceof UnaryExpression not && "!".equals(not.getOp()) - && not.getExpression()instanceof BinaryExpression binary && "||".equals(binary.getOperator())) { - facts.addAll(factsOf(new UnaryExpression("!", binary.getFirstOperand()))); - facts.addAll(factsOf(new UnaryExpression("!", binary.getSecondOperand()))); - } else if (expression instanceof UnaryExpression not && "!".equals(not.getOp()) - && not.getExpression()instanceof UnaryExpression inner && "!".equals(inner.getOp())) { - facts.addAll(factsOf(inner.getExpression())); - } else { - facts.add(expression); - } - return facts; - } - - // Terms of expected plus those of every fact sharing a term with them, directly or through other facts. The - // remaining facts constrain other values only, so any values satisfying them make the same counterexample - private static Set linkedTerms(List facts, List expectedTerms) { - Set linked = new HashSet<>(expectedTerms); - List> unlinked = facts.stream().map(RefinementError::termsOf) - .collect(Collectors.toCollection(ArrayList::new)); - boolean changed = true; - while (changed) { - changed = false; - for (Iterator> it = unlinked.iterator(); it.hasNext();) { - List terms = it.next(); - if (terms.stream().anyMatch(linked::contains)) { - linked.addAll(terms); - it.remove(); - changed = true; - } - } - } - return linked; - } - // Whether a fact of found is term == value, which the counterexample would only repeat private static boolean isKnown(Pair assignment, List facts) { return facts.stream() @@ -209,32 +154,4 @@ private static int relevance(String term, List expectedTerms, List termsOf(Expression expression) { - List terms = new ArrayList<>(); - expression.getVariableNames(terms); - addGhostApplications(expression, terms); - return terms; - } - - private static void addGhostApplications(Expression expression, List terms) { - String term = expression instanceof FunctionInvocation ? termName(expression) : null; - if (term != null && !terms.contains(term)) - terms.add(term); - for (Expression child : expression.getChildren()) - addGhostApplications(child, terms); - } - - // Name of a variable, or of a ghost application over variables, as in the SMT model; null for other expressions - private static String termName(Expression expression) { - if (expression instanceof Var var) - return var.getName(); - if (expression instanceof FunctionInvocation invocation - && invocation.getArgs().stream().allMatch(Var.class::isInstance)) { - String args = invocation.getArgs().stream().map(Expression::toString).collect(Collectors.joining(", ")); - return Utils.getSimpleName(invocation.getName()) + "(" + args + ")"; - } - return null; - } } diff --git a/liquidjava-verifier/src/main/java/liquidjava/diagnostics/errors/StateRefinementError.java b/liquidjava-verifier/src/main/java/liquidjava/diagnostics/errors/StateRefinementError.java index c0ff6bcb..e60d709a 100644 --- a/liquidjava-verifier/src/main/java/liquidjava/diagnostics/errors/StateRefinementError.java +++ b/liquidjava-verifier/src/main/java/liquidjava/diagnostics/errors/StateRefinementError.java @@ -1,6 +1,7 @@ package liquidjava.diagnostics.errors; import static liquidjava.rj_language.opt.VCSimplificationUtils.isTrue; +import static liquidjava.rj_language.opt.VCSimplificationUtils.linkedToExpected; import java.util.List; @@ -44,7 +45,7 @@ public StateRefinementError(SourcePosition position, SourcePosition declarationP // Only the facts of found about the objects of expected, and only when one of them tells a state: an alias or a // guard on another value says nothing about the state expected needs private static String message(Predicate expected, VCSimplificationResult found) { - Expression shown = RefinementError.linkedToExpected(found.getImplication().toPredicate().getExpression(), + Expression shown = linkedToExpected(found.getImplication().toPredicate().getExpression(), expected.getExpression()); if (!appliesGhost(shown)) return String.format("expected %s but could not prove it", expected.getExpression().toDisplayString()); 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 eb0c7d9a..a729e14b 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,10 +1,13 @@ package liquidjava.rj_language.opt; import static liquidjava.rj_language.opt.VCSimplificationUtils.containsVar; +import static liquidjava.rj_language.opt.VCSimplificationUtils.factsOf; +import static liquidjava.rj_language.opt.VCSimplificationUtils.linkedTerms; import static liquidjava.rj_language.opt.VCSimplificationUtils.termsOf; import static liquidjava.rj_language.opt.VCSimplificationUtils.valueVariablesOf; import java.util.HashSet; +import java.util.List; import java.util.Set; import liquidjava.processor.VCImplication; @@ -15,7 +18,8 @@ * Decides which binders refined only by {@code true} a simplified VC chain keeps for an error. Such a binder states no * 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 + * other row mentions it: the row then shows that nothing is known about a value the error depends on. It also tells + * which binders expected does not depend on, such as path conditions over other values * * @param expectedTerms * variables and ghost applications of the expected refinement @@ -68,6 +72,35 @@ public Set trueBindersToKeep(VCImplication chain) { return keep; } + /** + * Binders that share no term with expected, neither their variable nor a term of their refinement, directly or + * through other facts of the chain, and whose variable no other row mentions: expected does not depend on them. + * None without expected terms + */ + public Set unlinkedBinders(VCImplication chain) { + Set unlinked = new HashSet<>(); + if (expectedTerms.isEmpty()) + return unlinked; + List facts = factsOf(chain.toPredicate().getExpression()); + Set linked = linkedTerms(facts, expectedTerms); + for (VCImplication row = chain; row != null; row = row.getNext()) + if (row.hasBinder() && !isLinked(row, linked) && !mentionedByOtherRows(chain, row)) + unlinked.add(row.getName()); + return unlinked; + } + + private static boolean isLinked(VCImplication row, Set linked) { + return linked.contains(row.getName()) + || termsOf(row.getRefinement().getExpression()).stream().anyMatch(linked::contains); + } + + private static boolean mentionedByOtherRows(VCImplication chain, VCImplication row) { + for (VCImplication other = chain; other != null; other = other.getNext()) + if (other != row && containsVar(other.getRefinement().getExpression(), row.getName())) + return true; + return false; + } + 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/VCBinderSimplification.java b/liquidjava-verifier/src/main/java/liquidjava/rj_language/opt/VCBinderSimplification.java index da979e56..0ea323aa 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 @@ -34,24 +34,25 @@ public VCBinderSimplification(NeededVariables needed) { @Override public VCImplication apply(VCImplication implication) { VCImplication cloned = implication.clone(); - VCImplication simplified = simplify(cloned, needed.trueBindersToKeep(cloned)); + VCImplication simplified = simplify(cloned, needed.trueBindersToKeep(cloned), needed.unlinkedBinders(cloned)); return simplified == null ? cloned : simplified; } /** * Simplifies the first applicable binder in a VC chain */ - private VCImplication simplify(VCImplication implication, Set keptTrueBinders) { + private VCImplication simplify(VCImplication implication, Set keptTrueBinders, + Set unlinkedBinders) { if (implication == null) return null; if (isFalseBinder(implication)) return collapseFalseBinder(implication); - if (isRemovableBinder(implication, keptTrueBinders)) + if (isRemovableBinder(implication, keptTrueBinders, unlinkedBinders)) return removeBinder(implication); - VCImplication next = simplify(implication.getNext(), keptTrueBinders); + VCImplication next = simplify(implication.getNext(), keptTrueBinders, unlinkedBinders); if (next == null) return null; @@ -87,14 +88,17 @@ private VCImplication removeBinder(VCImplication implication) { /** * 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 + * unless the error needs it. A generated path condition that expected does not depend on is removed too */ - private boolean isRemovableBinder(VCImplication implication, Set keptTrueBinders) { + private boolean isRemovableBinder(VCImplication implication, Set keptTrueBinders, + Set unlinkedBinders) { if (!implication.hasBinder()) return false; if (isTrueBinder(implication)) return !keptTrueBinders.contains(implication.getName()); + if (isGeneratedBooleanBinder(implication) && unlinkedBinders.contains(implication.getName())) + return true; return !containsVar(implication.getNext(), implication.getName()) && isUnusedFreshPathBinder(implication); } @@ -102,14 +106,21 @@ private boolean isRemovableBinder(VCImplication implication, Set keptTru * Checks for a generated boolean path binder refined exactly by itself */ private boolean isUnusedFreshPathBinder(VCImplication implication) { - if (!implication.hasNext() || !GeneratedNames.isGenerated(implication.getName()) - || !"boolean".equals(implication.getType().getQualifiedName())) + if (!implication.hasNext() || !isGeneratedBooleanBinder(implication)) return false; return implication.getRefinement().getExpression()instanceof Var var && implication.getName().equals(var.getName()); } + /** + * Checks for a binder of a generated boolean, such as a path condition + */ + private boolean isGeneratedBooleanBinder(VCImplication implication) { + return GeneratedNames.isGenerated(implication.getName()) + && "boolean".equals(implication.getType().getQualifiedName()); + } + /** * Replaces a false binder implication with true */ 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 5f0be3bf..fd1762b7 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,14 +1,22 @@ package liquidjava.rj_language.opt; import java.util.ArrayList; +import java.util.Collection; +import java.util.HashSet; +import java.util.Iterator; import java.util.List; +import java.util.Set; +import java.util.stream.Collectors; 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; +import liquidjava.utils.Utils; public final class VCSimplificationUtils { @@ -65,7 +73,8 @@ public static List variablesOf(Expression expression) { } /** - * Terms an expression constrains: its variables and its ghost and state applications such as {@code size(x)} + * Terms an expression constrains: its variables and its ghost and state applications, those over variables named as + * in the SMT model such as {@code size(x)} and the others as written */ public static List termsOf(Expression expression) { List terms = variablesOf(expression); @@ -74,12 +83,29 @@ public static List termsOf(Expression expression) { } private static void addApplications(Expression expression, List terms) { - if (expression instanceof FunctionInvocation && !terms.contains(expression.toString())) - terms.add(expression.toString()); + if (expression instanceof FunctionInvocation) { + String term = termName(expression) != null ? termName(expression) : expression.toString(); + if (!terms.contains(term)) + terms.add(term); + } for (Expression child : expression.getChildren()) addApplications(child, terms); } + /** + * Name of a variable, or of a ghost application over variables, as in the SMT model; null for other expressions + */ + public static String termName(Expression expression) { + if (expression instanceof Var var) + return var.getName(); + if (expression instanceof FunctionInvocation invocation + && invocation.getArgs().stream().allMatch(Var.class::isInstance)) { + String args = invocation.getArgs().stream().map(Expression::toString).collect(Collectors.joining(", ")); + return Utils.getSimpleName(invocation.getName()) + "(" + args + ")"; + } + return null; + } + /** * 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 @@ -98,4 +124,64 @@ private static void addValueVariables(Expression expression, List names) for (Expression child : expression.getChildren()) addValueVariables(child, names); } + + /** + * Conjuncts of an expression, also splitting negated disjunctions ({@code !(a || b)} is {@code !a && !b}) and + * dropping double negations, so each fact links only the terms it relates + */ + public static List factsOf(Expression expression) { + List facts = new ArrayList<>(); + if (expression instanceof BinaryExpression binary && "&&".equals(binary.getOperator())) { + facts.addAll(factsOf(binary.getFirstOperand())); + facts.addAll(factsOf(binary.getSecondOperand())); + } else if (expression instanceof UnaryExpression not && "!".equals(not.getOp()) + && not.getExpression()instanceof BinaryExpression binary && "||".equals(binary.getOperator())) { + facts.addAll(factsOf(new UnaryExpression("!", binary.getFirstOperand()))); + facts.addAll(factsOf(new UnaryExpression("!", binary.getSecondOperand()))); + } else if (expression instanceof UnaryExpression not && "!".equals(not.getOp()) + && not.getExpression()instanceof UnaryExpression inner && "!".equals(inner.getOp())) { + facts.addAll(factsOf(inner.getExpression())); + } else { + facts.add(expression); + } + return facts; + } + + /** + * The seed terms plus those of every fact sharing a term with them, directly or through other facts. The remaining + * facts constrain other values only + */ + public static Set linkedTerms(List facts, Collection seed) { + Set linked = new HashSet<>(seed); + List> unlinked = facts.stream().map(VCSimplificationUtils::termsOf) + .collect(Collectors.toCollection(ArrayList::new)); + boolean changed = true; + while (changed) { + changed = false; + for (Iterator> it = unlinked.iterator(); it.hasNext();) { + List terms = it.next(); + if (terms.stream().anyMatch(linked::contains)) { + linked.addAll(terms); + it.remove(); + changed = true; + } + } + } + return linked; + } + + /** + * The facts of found linked to the terms of expected, as a conjunction, or true when there are none; found as + * written when every fact is linked + */ + public static Expression linkedToExpected(Expression found, Expression expected) { + List facts = factsOf(found); + Set linked = linkedTerms(facts, termsOf(expected)); + List linkedFacts = facts.stream().filter(fact -> termsOf(fact).stream().anyMatch(linked::contains)) + .toList(); + if (linkedFacts.size() == facts.size()) + return found; + return linkedFacts.stream().reduce((first, second) -> new BinaryExpression(first, "&&", second)) + .orElse(new LiteralBoolean(true)); + } } diff --git a/liquidjava-verifier/src/test/java/liquidjava/api/tests/TestGeneratedNames.java b/liquidjava-verifier/src/test/java/liquidjava/api/tests/TestGeneratedNames.java index ade19e64..0acd3489 100644 --- a/liquidjava-verifier/src/test/java/liquidjava/api/tests/TestGeneratedNames.java +++ b/liquidjava-verifier/src/test/java/liquidjava/api/tests/TestGeneratedNames.java @@ -10,6 +10,7 @@ import liquidjava.api.CommandLineLauncher; import liquidjava.diagnostics.Diagnostics; import liquidjava.diagnostics.errors.RefinementError; +import liquidjava.rj_language.opt.VCSimplificationResult; /** * Checks that the messages for {@code classes/generated_names_error} name each value the verifier introduces after what @@ -20,18 +21,25 @@ class TestGeneratedNames { @Test void namesEachGeneratedValueAfterWhatItIs() { CommandLineLauncher.launch("../liquidjava-example/src/main/java/testSuite/classes/generated_names_error"); - // the whole Found of a refinement error, as the message keeps only the facts about the expected values - Map messages = Diagnostics.getInstance().getErrors().stream() - .collect(Collectors.toMap(error -> error.getPosition().getLine(), - error -> (error instanceof RefinementError refinement - ? refinement.getFound().getImplication().toPredicate().getExpression().toDisplayString() - : error.getMessage()).replaceAll("[⁰¹²³⁴⁵⁶⁷⁸⁹]", ""))); + // the original Found of a refinement error, as the message and the simplified Found keep only the facts about + // the expected values + Map messages = Diagnostics.getInstance().getErrors().stream().collect(Collectors.toMap( + error -> error.getPosition().getLine(), + error -> (error instanceof RefinementError refinement ? originalFound(refinement) : error.getMessage()) + .replaceAll("[⁰¹²³⁴⁵⁶⁷⁸⁹]", ""))); assertEquals(Map.of(25, "#if_condition == #ready_result && #if_condition", 30, "#loop_condition == #ready_result && #loop_condition == true", 34, "#ternary_condition == #ready_result && #ternary_condition == true", 43, "!#try_branch && !#catch_branch", 48, "x == #read_result - 1", 54, - "#if_condition == #operation_result && #if_condition && x == 0", 58, + "isNull == #operation_result && #if_condition == isNull && #if_condition && x == 0", 58, "found closed(#new_Door) but expected opened(#new_Door)"), messages); } + + private static String originalFound(RefinementError error) { + VCSimplificationResult found = error.getFound(); + while (found.getOrigin() != null) + found = found.getOrigin(); + return found.getImplication().toPredicate().getExpression().toDisplayString(); + } } 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 484bec1a..5260c6ea 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 @@ -121,6 +121,34 @@ void collapsedFalseBinderLeavesNoTrueAfterAnotherRow() { assertSimplificationSteps(binderSimplification, vc("∀x:int. x > 0", "∀y:int. false", "z > 0"), step("x > 0")); } + @Test + void removesPathConditionsExpectedDoesNotDependOn() { + assertSimplificationSteps(forStateError("redoable(u)"), + vc("∀##if_condition_1:boolean. !a", "∀##if_condition_2:boolean. !(b || c)", "∀u:Object. u == g"), + step("!(b || c)", "u == g"), step("u == g")); + } + + @Test + void keepsPathConditionExpectedDependsOnThroughAnotherRow() { + assertSimplificationSteps(forRefinementError("y > 0"), + vc("∀##if_condition_1:boolean. x > 5", "∀##if_condition_2:boolean. !c", "∀y:int. y == x - 10"), + step("x > 5", "y == x - 10")); + } + + @Test + void keepsPathConditionAnotherRowMentions() { + assertSimplificationSteps(forStateError("open(f)"), + vc("∀##if_condition_1:boolean. p", "∀##if_condition_2:boolean. q", + "∀f:Object. ##if_condition_1 ? open(f) : created(f)"), + step("p", "#if_condition¹ ? open(f) : created(f)")); + } + + @Test + void keepsPathConditionsExpectedNames() { + assertSimplificationSteps(forRefinementError("##if_condition_1 || f(1) > 1"), vc("∀##if_condition_1:boolean. p", + "∀##if_condition_2:boolean. f(1) > 0", "∀##if_condition_3:boolean. q"), step("p", "f(1) > 0")); + } + @Test void trueBinderWithoutSuffixBecomesPlainTrue() { assertSimplificationSteps(binderSimplification, vc("∀x:int. true"), step("true"));