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