From 6f55e1c265f01a4177b10f59a544b49ef2c707e2 Mon Sep 17 00:00:00 2001 From: Ricardo Costa Date: Wed, 24 Jun 2026 16:01:57 +0100 Subject: [PATCH 1/2] Fix VC Function Substitution --- .../opt/VCFunctionSubstitution.java | 70 ++++++++++--------- .../rj_language/opt/VCSimplification.java | 5 +- .../opt/VCSimplificationUtils.java | 17 +++++ .../opt/VCFunctionSubstitutionTest.java | 21 ++++-- .../VCSimplificationPropertyBasedTest.java | 20 ++++++ 5 files changed, 91 insertions(+), 42 deletions(-) diff --git a/liquidjava-verifier/src/main/java/liquidjava/rj_language/opt/VCFunctionSubstitution.java b/liquidjava-verifier/src/main/java/liquidjava/rj_language/opt/VCFunctionSubstitution.java index c9a4a702..bbf75cbc 100644 --- a/liquidjava-verifier/src/main/java/liquidjava/rj_language/opt/VCFunctionSubstitution.java +++ b/liquidjava-verifier/src/main/java/liquidjava/rj_language/opt/VCFunctionSubstitution.java @@ -1,7 +1,10 @@ package liquidjava.rj_language.opt; import static liquidjava.rj_language.opt.VCSimplificationUtils.copyWithRefinement; +import static liquidjava.rj_language.opt.VCSimplificationUtils.containsExpression; +import java.util.ArrayList; +import java.util.List; import java.util.Optional; import liquidjava.processor.VCImplication; @@ -18,7 +21,8 @@ public class VCFunctionSubstitution implements VCSimplificationPass { /** * A substitution discovered from a function invocation equality */ - private record Substitution(VCImplication node, FunctionInvocation invocation, Expression replacement) { + private record Substitution(VCImplication node, FunctionInvocation invocation, Expression replacement, + Expression sourceEquality) { } /** @@ -31,32 +35,52 @@ public VCImplication apply(VCImplication implication) { if (substitutionOpt.isPresent()) { Substitution substitution = substitutionOpt.get(); - result = substitute(result, substitution.node(), substitution.invocation(), substitution.replacement()); + result = substitute(result, substitution.node(), substitution.invocation(), substitution.replacement(), + substitution.sourceEquality()); } return result; } /** - * Preserves nodes before the source equality and starts rewriting at the source suffix + * Rewrites one VC chain with a single substitution and removes its source equality */ private VCImplication substitute(VCImplication implication, VCImplication node, FunctionInvocation invocation, - Expression replacement) { + Expression replacement, Expression sourceEquality) { if (implication == null) return null; - // skip the source node to remove it from the chain and start substitution from the next node + // consume the source equality and start substitution from the next node if (implication == node) { - VCImplication result = copyWithRefinement(implication, implication.getRefinement().clone()); - result.setNext(substituteSuffix(implication.getNext(), invocation, replacement)); - return result; + VCImplication suffix = substituteSuffix(implication.getNext(), invocation, replacement); + VCImplication source = removeSourceEquality(implication, sourceEquality); + if (source == null) + return suffix; + source.setNext(suffix); + return source; } // preserve the current node and continue rewriting the suffix VCImplication result = copyWithRefinement(implication, implication.getRefinement().clone()); - result.setNext(substitute(implication.getNext(), node, invocation, replacement)); + result.setNext(substitute(implication.getNext(), node, invocation, replacement, sourceEquality)); return result; } + /** + * Removes the equality conjunct that supplied the substitution, preserving any sibling conjuncts + */ + private VCImplication removeSourceEquality(VCImplication implication, Expression sourceEquality) { + List remaining = new ArrayList<>(implication.getRefinement().getExpression().getConjuncts()); + if (!remaining.remove(sourceEquality)) + return copyWithRefinement(implication, implication.getRefinement().clone()); + if (remaining.isEmpty()) + return null; + + Predicate refinement = new Predicate(); + for (Expression conjunct : remaining) + refinement = Predicate.createConjunction(refinement, new Predicate(conjunct.clone())); + return copyWithRefinement(implication, refinement); + } + /** * Rewrites every node after the source equality with one function substitution */ @@ -121,33 +145,13 @@ private Optional getSubstitution(VCImplication implication, Expres Expression left = binary.getFirstOperand(); Expression right = binary.getSecondOperand(); if (left instanceof FunctionInvocation invocation && !containsExpression(right, left)) - return Optional.of(new Substitution(implication, (FunctionInvocation) invocation.clone(), right.clone())); + return Optional.of(new Substitution(implication, (FunctionInvocation) invocation.clone(), right.clone(), + binary.clone())); if (right instanceof FunctionInvocation invocation && !containsExpression(left, right)) - return Optional.of(new Substitution(implication, (FunctionInvocation) invocation.clone(), left.clone())); + return Optional.of(new Substitution(implication, (FunctionInvocation) invocation.clone(), left.clone(), + binary.clone())); return Optional.empty(); } - /** - * Checks whether an expression contains another expression - */ - private boolean containsExpression(Expression expression, Expression target) { - if (expression.equals(target)) - return true; - - for (Expression child : expression.getChildren()) - if (containsExpression(child, target)) - return true; - return false; - } - - /** - * Checks whether a VC suffix contains an expression - */ - private boolean containsExpression(VCImplication implication, Expression target) { - for (VCImplication current = implication; current != null; current = current.getNext()) - if (containsExpression(current.getRefinement().getExpression(), target)) - return true; - return false; - } } 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 2b52a957..33727021 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 @@ -9,8 +9,9 @@ */ public class VCSimplification { - private static final List PASSES = List.of(new VCSubstitution(), new VCBinderSimplification(), - new VCFolding(), new VCArithmeticSimplification(), new VCLogicalSimplification()); + private static final List PASSES = List.of(new VCSubstitution(), new VCFunctionSubstitution(), + new VCBinderSimplification(), new VCFolding(), new VCArithmeticSimplification(), + new VCLogicalSimplification()); /** * Applies all available simplification steps to a VC chain until a fixed point is reached 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 042aa413..4ab15375 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 @@ -28,6 +28,23 @@ public static boolean containsVar(VCImplication implication, String name) { return false; } + public static boolean containsExpression(Expression expression, Expression target) { + if (expression.equals(target)) + return true; + + for (Expression child : expression.getChildren()) + if (containsExpression(child, target)) + return true; + return false; + } + + public static boolean containsExpression(VCImplication implication, Expression target) { + for (VCImplication current = implication; current != null; current = current.getNext()) + if (containsExpression(current.getRefinement().getExpression(), target)) + return true; + return false; + } + public static boolean isTrue(Expression expression) { return expression instanceof LiteralBoolean literal && literal.isBooleanTrue(); } diff --git a/liquidjava-verifier/src/test/java/liquidjava/rj_language/opt/VCFunctionSubstitutionTest.java b/liquidjava-verifier/src/test/java/liquidjava/rj_language/opt/VCFunctionSubstitutionTest.java index 91ea9468..a9304bcb 100644 --- a/liquidjava-verifier/src/test/java/liquidjava/rj_language/opt/VCFunctionSubstitutionTest.java +++ b/liquidjava-verifier/src/test/java/liquidjava/rj_language/opt/VCFunctionSubstitutionTest.java @@ -13,21 +13,21 @@ class VCFunctionSubstitutionTest { void substitutesExactFunctionInvocationIntoSuffix() { VCImplication implication = vc("f(x) == 0", "f(y) == f(x) + 1"); - assertSimplificationSteps(substitution::apply, implication, step("f(x) == 0", "f(y) == 0 + 1")); + assertSimplificationSteps(substitution::apply, implication, step("f(y) == 0 + 1")); } @Test void substitutesReverseFunctionEquality() { VCImplication implication = vc("0 == f(x)", "f(y) == f(x) + 1"); - assertSimplificationSteps(substitution::apply, implication, step("0 == f(x)", "f(y) == 0 + 1")); + assertSimplificationSteps(substitution::apply, implication, step("f(y) == 0 + 1")); } @Test - void preservesSourceNode() { + void consumesSourceNodeWhenSubstitutedInvocationIsGoneFromSuffix() { VCImplication implication = vc("f(x) == 0", "f(x) > -1"); - assertSimplificationSteps(substitution::apply, implication, step("f(x) == 0", "0 > -1")); + assertSimplificationSteps(substitution::apply, implication, step("0 > -1")); } @Test @@ -41,8 +41,8 @@ void doesNotRewriteEarlierNodesFromLaterEquality() { void skipsUsedUpEqualityAndUsesNextAvailableEquality() { VCImplication implication = vc("f(x) == 0", "f(y) == f(x) + 1", "f(y) == 1"); - assertSimplificationSteps(substitution::apply, implication, step("f(x) == 0", "f(y) == 0 + 1", "f(y) == 1"), - step("f(x) == 0", "f(y) == 0 + 1", "0 + 1 == 1")); + assertSimplificationSteps(substitution::apply, implication, step("f(y) == 0 + 1", "f(y) == 1"), + step("0 + 1 == 1")); } @Test @@ -63,6 +63,13 @@ void ignoresRecursiveFunctionEquality() { void extractsEqualityFromTopLevelConjunction() { VCImplication implication = vc("ok && f(x) == 0", "f(y) == f(x) + 1"); - assertSimplificationSteps(substitution::apply, implication, step("ok && f(x) == 0", "f(y) == 0 + 1")); + assertSimplificationSteps(substitution::apply, implication, step("ok", "f(y) == 0 + 1")); + } + + @Test + void removesOnlySourceEqualityConjunct() { + VCImplication implication = vc("ok && f(x) == 0 && ready", "f(y) == f(x) + 1"); + + assertSimplificationSteps(substitution::apply, implication, step("ok && ready", "f(y) == 0 + 1")); } } diff --git a/liquidjava-verifier/src/test/java/liquidjava/rj_language/opt/VCSimplificationPropertyBasedTest.java b/liquidjava-verifier/src/test/java/liquidjava/rj_language/opt/VCSimplificationPropertyBasedTest.java index 9d97a1c5..39d69a67 100644 --- a/liquidjava-verifier/src/test/java/liquidjava/rj_language/opt/VCSimplificationPropertyBasedTest.java +++ b/liquidjava-verifier/src/test/java/liquidjava/rj_language/opt/VCSimplificationPropertyBasedTest.java @@ -2,6 +2,7 @@ import static org.junit.jupiter.api.Assertions.assertTrue; import static org.junit.jupiter.api.Assertions.fail; +import static liquidjava.rj_language.opt.VCSimplificationUtils.containsExpression; import java.util.ArrayList; import java.util.List; @@ -15,6 +16,7 @@ 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.Var; import liquidjava.smt.SMTEvaluator; import liquidjava.smt.SMTResult; @@ -81,10 +83,28 @@ private static Predicate substitutionPremises(VCImplication implication) { for (VCImplication current = implication; current != null; current = current.getNext()) { if (isSubstitution(current)) premises = Predicate.createConjunction(premises, current.getRefinement()); + for (Expression conjunct : current.getRefinement().getExpression().getConjuncts()) { + if (!isFunctionSubstitution(conjunct, current.getNext())) + continue; + premises = Predicate.createConjunction(premises, new Predicate(conjunct.clone())); + } } return premises; } + private static boolean isFunctionSubstitution(Expression expression, VCImplication suffix) { + if (!(expression instanceof BinaryExpression binary) || !"==".equals(binary.getOperator())) + return false; + + Expression left = binary.getFirstOperand(); + Expression right = binary.getSecondOperand(); + if (left instanceof FunctionInvocation && !containsExpression(right, left)) + return containsExpression(suffix, left); + if (right instanceof FunctionInvocation && !containsExpression(left, right)) + return containsExpression(suffix, right); + return false; + } + private static boolean isSubstitution(VCImplication implication) { if (!implication.hasBinder()) return false; From 2d2db905bdee472b9d61857eb06686f372dc4c91 Mon Sep 17 00:00:00 2001 From: Ricardo Costa Date: Wed, 24 Jun 2026 17:46:35 +0100 Subject: [PATCH 2/2] Function Invocation Simple Name Workaround --- .../liquidjava/rj_language/ast/FunctionInvocation.java | 7 +++++-- 1 file changed, 5 insertions(+), 2 deletions(-) diff --git a/liquidjava-verifier/src/main/java/liquidjava/rj_language/ast/FunctionInvocation.java b/liquidjava-verifier/src/main/java/liquidjava/rj_language/ast/FunctionInvocation.java index d9d53731..85af21b4 100644 --- a/liquidjava-verifier/src/main/java/liquidjava/rj_language/ast/FunctionInvocation.java +++ b/liquidjava-verifier/src/main/java/liquidjava/rj_language/ast/FunctionInvocation.java @@ -93,7 +93,7 @@ public int hashCode() { final int prime = 31; int result = 1; result = prime * result + ((getArgs() == null) ? 0 : getArgs().hashCode()); - result = prime * result + ((name == null) ? 0 : name.hashCode()); + result = prime * result + ((name == null) ? 0 : Utils.getSimpleName(name).hashCode()); // same here return result; } @@ -114,7 +114,10 @@ public boolean equals(Object obj) { if (name == null) { return other.name == null; } else { - return name.equals(other.name); + // prefixes are inconsistent for refined class ghost calls: some use the + // original class prefix, others use the caller class prefix + // for now we compare simple names, but prefix handling should be fixed instead of having this workaround + return other.name != null && Utils.getSimpleName(name).equals(Utils.getSimpleName(other.name)); } } }