Skip to content

Drop path conditions that expected does not depend on from Found #487

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Merged
CatarinaGamboa merged 1 commit into from
Nov 5, 2026
Merged

Drop path conditions that expected does not depend on from Found #487

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
1 commit
Select commit
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
93 changes: 5 additions & 88 deletions liquidjava-verifier/src/main/java/liquidjava/diagnostics/errors/RefinementError.java
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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;
Expand All @@ -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;
Expand All @@ -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
Expand Down Expand Up @@ -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<Expression> facts = factsOf(found);
Set<String> linked = linkedTerms(facts, termsOf(expected));
List<Expression> 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<String> foundVariables = found.getImplication().toPredicate().getVariableNames();
Expand Down Expand Up @@ -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<Expression> factsOf(Expression expression) {
List<Expression> 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<String> linkedTerms(List<Expression> facts, List<String> expectedTerms) {
Set<String> linked = new HashSet<>(expectedTerms);
List<List<String>> unlinked = facts.stream().map(RefinementError::termsOf)
.collect(Collectors.toCollection(ArrayList::new));
boolean changed = true;
while (changed) {
changed = false;
for (Iterator<List<String>> it = unlinked.iterator(); it.hasNext();) {
List<String> 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<String, String> assignment, List<Expression> facts) {
return facts.stream()
Expand Down Expand Up @@ -209,32 +154,4 @@ private static int relevance(String term, List<String> expectedTerms, List<Strin
return foundTerms.contains(term) ? 1 : 0;
return GeneratedNames.isGenerated(term) ? 3 : 2;
}

// Variables and ghost applications of an expression, named as in the SMT model
private static List<String> termsOf(Expression expression) {
List<String> terms = new ArrayList<>();
expression.getVariableNames(terms);
addGhostApplications(expression, terms);
return terms;
}

private static void addGhostApplications(Expression expression, List<String> 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;
}
}
3 changes: 2 additions & 1 deletion liquidjava-verifier/src/main/java/liquidjava/diagnostics/errors/StateRefinementError.java
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -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;

Expand Down Expand Up @@ -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());
Expand Down
35 changes: 34 additions & 1 deletion liquidjava-verifier/src/main/java/liquidjava/rj_language/opt/NeededVariables.java
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -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;
Expand All @@ -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
Expand Down Expand Up @@ -68,6 +72,35 @@ public Set<String> 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<String> unlinkedBinders(VCImplication chain) {
Set<String> unlinked = new HashSet<>();
if (expectedTerms.isEmpty())
return unlinked;
List<Expression> facts = factsOf(chain.toPredicate().getExpression());
Set<String> 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<String> 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<String> primitiveBinders(VCImplication chain) {
Set<String> primitives = new HashSet<>();
for (VCImplication current = chain; current != null; current = current.getNext())
Expand Down
27 changes: 19 additions & 8 deletions liquidjava-verifier/src/main/java/liquidjava/rj_language/opt/VCBinderSimplification.java
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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<String> keptTrueBinders) {
private VCImplication simplify(VCImplication implication, Set<String> keptTrueBinders,
Set<String> 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;

Expand Down Expand Up @@ -87,29 +88,39 @@ 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<String> keptTrueBinders) {
private boolean isRemovableBinder(VCImplication implication, Set<String> keptTrueBinders,
Set<String> 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);
}

/**
* 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
*/
Expand Down
Loading
Loading