From 8cdac3115ff9255fdbc1c7214aa31bfd440f0e60 Mon Sep 17 00:00:00 2001 From: Ricardo Costa Date: Wed, 5 Aug 2026 15:31:38 +0100 Subject: [PATCH 1/2] Remove Unused Binders In Simplification --- .../opt/VCBinderSimplification.java | 20 ++++++++++++++----- .../opt/VCSimplificationResult.java | 2 -- .../opt/VCBinderSimplificationTest.java | 10 ++++++++++ .../rj_language/opt/VCSimplificationTest.java | 9 ++++----- 4 files changed, 29 insertions(+), 12 deletions(-) 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 3b5f2866..39b37cca 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,8 +34,8 @@ private VCImplication simplify(VCImplication implication) { if (isFalseBinder(implication)) return collapseFalseBinder(implication); - if (isTrueBinder(implication) && !containsVar(implication.getNext(), implication.getName())) - return removeTrueBinder(implication); + if (isRemovableUnusedBinder(implication)) + return removeBinder(implication); VCImplication next = simplify(implication.getNext()); if (next == null) @@ -47,12 +47,12 @@ private VCImplication simplify(VCImplication implication) { } /** - * Removes a true binder whose name is not used in the suffix + * Removes a binder whose name is not used in the suffix */ - private VCImplication removeTrueBinder(VCImplication implication) { + private VCImplication removeBinder(VCImplication implication) { VCImplication next = implication.getNext(); - // ∀x. true => P -> P + // ∀x. R => P -> P when x is not used in P if (next != null) return next.clone(); @@ -61,6 +61,16 @@ private VCImplication removeTrueBinder(VCImplication implication) { return new VCImplication(truePredicate); } + /** + * Checks whether a binder is unused and can be removed + */ + private boolean isRemovableUnusedBinder(VCImplication implication) { + if (!implication.hasBinder() || containsVar(implication.getNext(), implication.getName())) + return false; + + return implication.hasNext() || isTrueBinder(implication); + } + /** * Replaces a false binder implication with true */ diff --git a/liquidjava-verifier/src/main/java/liquidjava/rj_language/opt/VCSimplificationResult.java b/liquidjava-verifier/src/main/java/liquidjava/rj_language/opt/VCSimplificationResult.java index 6f35822d..d70b2a77 100644 --- a/liquidjava-verifier/src/main/java/liquidjava/rj_language/opt/VCSimplificationResult.java +++ b/liquidjava-verifier/src/main/java/liquidjava/rj_language/opt/VCSimplificationResult.java @@ -1,7 +1,5 @@ package liquidjava.rj_language.opt; -import java.util.Objects; - import liquidjava.processor.VCImplication; /** 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 581688dd..b21eb77a 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 @@ -12,6 +12,16 @@ void removesTrueBinderWhenVariableIsUnusedDownstream() { assertSimplificationSteps(binderSimplification, vc("∀x:int. true", "y > 0"), step("y > 0")); } + @Test + void removesNonTrueBinderWhenVariableIsUnusedDownstream() { + assertSimplificationSteps(binderSimplification, vc("∀x:int. x > 0", "y > 0"), step("y > 0")); + } + + @Test + void keepsNonTrueTerminalBinderAsConclusion() { + assertSimplificationSteps(binderSimplification, vc("∀x:int. x > 0"), step("x > 0")); + } + @Test void keepsTrueBinderWhenVariableIsUsedDownstream() { assertSimplificationSteps(binderSimplification, vc("∀x:int. true", "x > 0"), step("true", "x > 0")); diff --git a/liquidjava-verifier/src/test/java/liquidjava/rj_language/opt/VCSimplificationTest.java b/liquidjava-verifier/src/test/java/liquidjava/rj_language/opt/VCSimplificationTest.java index 1ec9ebc6..2e44255e 100644 --- a/liquidjava-verifier/src/test/java/liquidjava/rj_language/opt/VCSimplificationTest.java +++ b/liquidjava-verifier/src/test/java/liquidjava/rj_language/opt/VCSimplificationTest.java @@ -108,14 +108,13 @@ void simplifyUsesLogicalSimplificationToEnableSubstitutionOnNextStep() { } @Test - void simplifyUsesFoldingToEnableBinderSimplificationOnNextStep() { - assertSimplificationSteps(vc("∀x:int. 1 > 2", "y > 0"), step("false", "y > 0"), step("true")); + void simplifyRemovesUnusedBinderBeforeFolding() { + assertSimplificationSteps(vc("∀x:int. 1 > 2", "y > 0"), step("y > 0")); } @Test - void simplifyUsesArithmeticAndLogicalSimplificationToEnableBinderRemoval() { - assertSimplificationSteps(vc("∀x:int. x + 0 == x", "y > 0"), step("x == x", "y > 0"), step("true", "y > 0"), - step("y > 0")); + void simplifyRemovesUnusedBinderBeforeArithmeticAndLogicalSimplification() { + assertSimplificationSteps(vc("∀x:int. x + 0 == x", "y > 0"), step("y > 0")); } @Test From acebb012500d8d266c0f94c61c7cc28aa9117e18 Mon Sep 17 00:00:00 2001 From: Ricardo Costa Date: Wed, 5 Aug 2026 15:56:50 +0100 Subject: [PATCH 2/2] Remove Unused Fresh Path Binders In Simplification --- .../opt/VCBinderSimplification.java | 23 +++++++++++++++---- .../opt/VCBinderSimplificationTest.java | 9 ++++++-- .../rj_language/opt/VCSimplificationTest.java | 9 ++++---- .../java/liquidjava/utils/VCTestUtils.java | 7 ++++-- 4 files changed, 36 insertions(+), 12 deletions(-) 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 39b37cca..58dc1f17 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 @@ -8,12 +8,15 @@ import liquidjava.processor.VCImplication; import liquidjava.rj_language.Predicate; import liquidjava.rj_language.ast.LiteralBoolean; +import liquidjava.rj_language.ast.Var; /** * Simplifies VCImplication chains by removing vacuous binder implications */ public class VCBinderSimplification implements VCSimplificationPass { + private static final String FRESH_PREFIX = "#fresh_"; + /** * Applies one binder simplification in a VC chain */ @@ -47,12 +50,12 @@ private VCImplication simplify(VCImplication implication) { } /** - * Removes a binder whose name is not used in the suffix + * Removes a binder that can be omitted from the suffix */ private VCImplication removeBinder(VCImplication implication) { VCImplication next = implication.getNext(); - // ∀x. R => P -> P when x is not used in P + // ∀x. true => P -> P, and unused generated path conditions can be omitted from diagnostics if (next != null) return next.clone(); @@ -62,13 +65,25 @@ private VCImplication removeBinder(VCImplication implication) { } /** - * Checks whether a binder is unused and can be removed + * Checks whether a binder is unused and can be removed without changing the VC conclusion */ private boolean isRemovableUnusedBinder(VCImplication implication) { if (!implication.hasBinder() || containsVar(implication.getNext(), implication.getName())) return false; - return implication.hasNext() || isTrueBinder(implication); + return isTrueBinder(implication) || isUnusedFreshPathBinder(implication); + } + + /** + * Checks for a generated boolean path binder refined exactly by itself + */ + private boolean isUnusedFreshPathBinder(VCImplication implication) { + if (!implication.hasNext() || !implication.getName().startsWith(FRESH_PREFIX) + || !"boolean".equals(implication.getType().getQualifiedName())) + return false; + + return implication.getRefinement().getExpression()instanceof Var var + && implication.getName().equals(var.getName()); } /** 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 b21eb77a..d3fbf3d0 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 @@ -13,8 +13,13 @@ void removesTrueBinderWhenVariableIsUnusedDownstream() { } @Test - void removesNonTrueBinderWhenVariableIsUnusedDownstream() { - assertSimplificationSteps(binderSimplification, vc("∀x:int. x > 0", "y > 0"), step("y > 0")); + void removesFreshPathBinderWhenVariableIsUnusedDownstream() { + assertSimplificationSteps(binderSimplification, vc("∀#fresh_1:boolean. #fresh_1", "y > 0"), step("y > 0")); + } + + @Test + void keepsNonTrueBinderWhenVariableIsUnusedDownstream() { + assertSimplificationSteps(binderSimplification, vc("∀x:int. x > 0", "y > 0"), step("x > 0", "y > 0")); } @Test diff --git a/liquidjava-verifier/src/test/java/liquidjava/rj_language/opt/VCSimplificationTest.java b/liquidjava-verifier/src/test/java/liquidjava/rj_language/opt/VCSimplificationTest.java index 2e44255e..1ec9ebc6 100644 --- a/liquidjava-verifier/src/test/java/liquidjava/rj_language/opt/VCSimplificationTest.java +++ b/liquidjava-verifier/src/test/java/liquidjava/rj_language/opt/VCSimplificationTest.java @@ -108,13 +108,14 @@ void simplifyUsesLogicalSimplificationToEnableSubstitutionOnNextStep() { } @Test - void simplifyRemovesUnusedBinderBeforeFolding() { - assertSimplificationSteps(vc("∀x:int. 1 > 2", "y > 0"), step("y > 0")); + void simplifyUsesFoldingToEnableBinderSimplificationOnNextStep() { + assertSimplificationSteps(vc("∀x:int. 1 > 2", "y > 0"), step("false", "y > 0"), step("true")); } @Test - void simplifyRemovesUnusedBinderBeforeArithmeticAndLogicalSimplification() { - assertSimplificationSteps(vc("∀x:int. x + 0 == x", "y > 0"), step("y > 0")); + void simplifyUsesArithmeticAndLogicalSimplificationToEnableBinderRemoval() { + assertSimplificationSteps(vc("∀x:int. x + 0 == x", "y > 0"), step("x == x", "y > 0"), step("true", "y > 0"), + step("y > 0")); } @Test diff --git a/liquidjava-verifier/src/test/java/liquidjava/utils/VCTestUtils.java b/liquidjava-verifier/src/test/java/liquidjava/utils/VCTestUtils.java index a3e1aa3c..d952f814 100644 --- a/liquidjava-verifier/src/test/java/liquidjava/utils/VCTestUtils.java +++ b/liquidjava-verifier/src/test/java/liquidjava/utils/VCTestUtils.java @@ -13,11 +13,12 @@ import liquidjava.rj_language.opt.VCSimplificationResult; import liquidjava.rj_language.parsing.RefinementsParser; import spoon.Launcher; +import spoon.reflect.factory.TypeFactory; import spoon.reflect.reference.CtTypeReference; public class VCTestUtils { - private static final CtTypeReference INT = new Launcher().getFactory().Type().INTEGER_PRIMITIVE; + private static final TypeFactory TYPE_FACTORY = new Launcher().getFactory().Type(); public static VCImplication vc(String... implications) { VCImplication first = null; @@ -97,7 +98,9 @@ private static VCImplication parseImplication(String implication) { private static CtTypeReference type(String name) { if ("int".equals(name)) - return INT; + return TYPE_FACTORY.INTEGER_PRIMITIVE; + if ("boolean".equals(name)) + return TYPE_FACTORY.BOOLEAN_PRIMITIVE; throw new IllegalArgumentException("Unsupported test type: " + name); }