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 new file mode 100644 index 00000000..7dd614a5 --- /dev/null +++ b/liquidjava-verifier/src/main/java/liquidjava/rj_language/opt/VCBinderSimplification.java @@ -0,0 +1,118 @@ +package liquidjava.rj_language.opt; + +import java.util.ArrayList; +import java.util.List; + +import liquidjava.processor.SimplifiedVCImplication; +import liquidjava.processor.VCImplication; +import liquidjava.rj_language.Predicate; +import liquidjava.rj_language.ast.Expression; +import liquidjava.rj_language.ast.LiteralBoolean; + +/** + * Simplifies VCImplication chains by removing vacuous binder implications + */ +public class VCBinderSimplification implements VCSimplificationPass { + + /** + * Applies one binder simplification in a VC chain + */ + @Override + public VCImplication apply(VCImplication implication) { + VCImplication cloned = implication.clone(); + VCImplication simplified = simplify(cloned); + return simplified == null ? cloned : simplified; + } + + /** + * Simplifies the first applicable binder in a VC chain + */ + private VCImplication simplify(VCImplication implication) { + if (implication == null) + return null; + + if (isFalseBinder(implication)) + return collapseFalseBinder(implication); + + if (isTrueBinder(implication) && !containsVar(implication.getNext(), implication.getName())) + return removeTrueBinder(implication); + + VCImplication next = simplify(implication.getNext()); + if (next == null) + return null; + + VCImplication result = implication.copyWithRefinement(implication.getRefinement().clone()); + result.setNext(next); + return result; + } + + /** + * Removes a true binder whose name is not used in the suffix + */ + private VCImplication removeTrueBinder(VCImplication implication) { + VCImplication next = implication.getNext(); + + // ∀x. true => P -> P + if (next != null) { + VCImplication origin = new VCImplication(implication.getName(), implication.getType(), + next.getOriginRefinement()); + VCImplication result = new SimplifiedVCImplication(next, next.getRefinement().clone(), origin); + result.setNext(next.getNext() == null ? null : next.getNext().clone()); + return result; + } + + // ∀x. true -> true + Predicate truePredicate = new Predicate(new LiteralBoolean(true)); + return new SimplifiedVCImplication(new VCImplication(truePredicate), truePredicate, implication); + } + + /** + * Replaces a false binder implication with true + */ + private VCImplication collapseFalseBinder(VCImplication implication) { + // ∀x. false => P -> true + Predicate truePredicate = new Predicate(new LiteralBoolean(true)); + return new SimplifiedVCImplication(new VCImplication(truePredicate), truePredicate, implication); + } + + /** + * Checks whether a VC node is a binder refined with true + */ + private boolean isTrueBinder(VCImplication implication) { + return implication.hasBinder() && isTrue(implication.getRefinement().getExpression()); + } + + /** + * Checks whether a VC node is a binder refined with false + */ + private boolean isFalseBinder(VCImplication implication) { + return implication.hasBinder() && isFalse(implication.getRefinement().getExpression()); + } + + /** + * Checks whether an expression is true + */ + private boolean isTrue(Expression expression) { + return expression instanceof LiteralBoolean literal && literal.isBooleanTrue(); + } + + /** + * Checks whether an expression is false + */ + private boolean isFalse(Expression expression) { + return expression instanceof LiteralBoolean literal && !literal.isBooleanTrue(); + } + + /** + * Checks whether a VC suffix contains a variable name + */ + private boolean containsVar(VCImplication implication, String name) { + for (VCImplication current = implication; current != null; current = current.getNext()) { + List names = new ArrayList<>(); + current.getRefinement().getExpression().getVariableNames(names); + if (names.contains(name)) + 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 38eb7f3b..b26af0e6 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,8 @@ */ public class VCSimplification { - private static final List PASSES = List.of(new VCSubstitution(), new VCFolding(), - new VCArithmeticSimplification(), new VCLogicalSimplification()); + private static final List PASSES = List.of(new VCSubstitution(), 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/test/java/liquidjava/rj_language/opt/VCBinderSimplificationTest.java b/liquidjava-verifier/src/test/java/liquidjava/rj_language/opt/VCBinderSimplificationTest.java new file mode 100644 index 00000000..5f49bbb3 --- /dev/null +++ b/liquidjava-verifier/src/test/java/liquidjava/rj_language/opt/VCBinderSimplificationTest.java @@ -0,0 +1,69 @@ +package liquidjava.rj_language.opt; + +import static liquidjava.utils.VCTestUtils.*; +import static org.junit.jupiter.api.Assertions.assertFalse; + +import liquidjava.processor.VCImplication; +import org.junit.jupiter.api.Test; + +class VCBinderSimplificationTest { + + private final VCBinderSimplification binderSimplification = new VCBinderSimplification(); + + @Test + void removesTrueBinderWhenVariableIsUnusedDownstream() { + VCImplication implication = vc("∀x:int. true", "y > 0"); + + assertSimplificationSteps(binderSimplification::apply, implication, chain(expect("y > 0", "∀x:int. y > 0"))); + } + + @Test + void keepsTrueBinderWhenVariableIsUsedDownstream() { + VCImplication implication = vc("∀x:int. true", "x > 0"); + + assertSimplificationSteps(binderSimplification::apply, implication, + chain(expect("true", "∀x:int. true"), expect("x > 0", "x > 0"))); + } + + @Test + void collapsesFalseBinderSuffixToPlainTrue() { + VCImplication implication = vc("∀x:int. false", "x > 0", "y > 0"); + VCImplication result = binderSimplification.apply(implication); + + assertFalse(result.hasBinder()); + assertSimplifiedVC(result, expect("true", "∀x:int. false")); + } + + @Test + void simplifiesOnlyFirstApplicableBinder() { + VCImplication implication = vc("∀x:int. true", "∀y:int. true", "z > 0"); + + assertSimplificationSteps(binderSimplification::apply, implication, + chain(expect("true", "∀x:int. true"), expect("z > 0", "z > 0"))); + } + + @Test + void skipsInapplicableTrueBinderAndSimplifiesLaterBinder() { + VCImplication implication = vc("∀x:int. true", "x > 0", "∀y:int. true", "z > 0"); + + assertSimplificationSteps(binderSimplification::apply, implication, + chain(expect("true", "∀x:int. true"), expect("x > 0", "x > 0"), expect("z > 0", "∀y:int. z > 0"))); + } + + @Test + void ignoresNonBinderBooleanLiterals() { + VCImplication implication = vc("true", "false"); + + assertSimplificationSteps(binderSimplification::apply, implication, + chain(expect("true", "true"), expect("false", "false"))); + } + + @Test + void trueBinderWithoutSuffixBecomesPlainTrue() { + VCImplication implication = vc("∀x:int. true"); + VCImplication result = binderSimplification.apply(implication); + + assertFalse(result.hasBinder()); + assertSimplifiedVC(result, expect("true", "∀x:int. true")); + } +} diff --git a/liquidjava-verifier/src/test/java/liquidjava/rj_language/opt/VCImplicationGenerator.java b/liquidjava-verifier/src/test/java/liquidjava/rj_language/opt/VCImplicationGenerator.java index f3e19ff9..b7517c49 100644 --- a/liquidjava-verifier/src/test/java/liquidjava/rj_language/opt/VCImplicationGenerator.java +++ b/liquidjava-verifier/src/test/java/liquidjava/rj_language/opt/VCImplicationGenerator.java @@ -21,7 +21,7 @@ public VCImplicationGenerator() { @Override public VCImplication generate(SourceOfRandomness random, GenerationStatus status) { - return switch (random.nextInt(0, 12)) { + return switch (random.nextInt(0, 14)) { case 0 -> vc(substitution(random, "x"), comparison(random, "x")); case 1 -> vc(reverseSubstitution(random, "x"), comparison(random, "x")); case 2 -> vc(nonSubstitution(random, "x"), substitution(random, "y"), comparison(random, "y")); @@ -34,6 +34,8 @@ public VCImplication generate(SourceOfRandomness random, GenerationStatus status case 9 -> vc(arithmeticIdentity(random)); case 10 -> guardedArithmeticIdentity(random); case 11 -> vc(logicalIdentity(random)); + case 12 -> vc(unusedTrueBinder(random)); + case 13 -> vc(falseBinder(random)); default -> vc(substitution(random, "x"), substitution(random, "y"), foldableComparison(random)); }; } @@ -60,6 +62,14 @@ private static String nonSubstitution(SourceOfRandomness random, String binder) return "∀" + binder + ":int. " + binder + " == " + binder + " " + signed(random.nextInt(1, 5)); } + private static String[] unusedTrueBinder(SourceOfRandomness random) { + return new String[] { "∀x:int. true", comparison(random, "a") }; + } + + private static String[] falseBinder(SourceOfRandomness random) { + return new String[] { "∀x:int. false", comparison(random, "x") }; + } + private static String comparison(SourceOfRandomness random, String preferredVar) { String left = random.nextBoolean() ? preferredVar : arithmetic(random, preferredVar); String right = random.nextBoolean() ? intLiteral(random) 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 5565e311..7a32db0d 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 @@ -36,6 +36,31 @@ void simplifyOnceDoesNotFoldAfterSubstitutionInSameStep() { chain(expect("true", "3 == 3"))); } + @Test + void simplifyOnceAppliesSubstitutionBeforeBinderSimplification() { + VCImplication implication = vc("∀x:int. x == 3", "∀y:int. true", "x > 0"); + + assertSimplificationSteps(VCSimplification::simplifyOnce, implication, + chain(expect("true", "∀y:int. true"), expect("3 > 0", "∀x:int. x > 0")), + chain(expect("3 > 0", "∀y:int. x > 0")), chain(expect("true", "3 > 0"))); + } + + @Test + void simplifyOnceAppliesBinderSimplificationBeforeFolding() { + VCImplication implication = vc("∀x:int. true", "1 + 2 > 0"); + + assertSimplificationSteps(VCSimplification::simplifyOnce, implication, + chain(expect("1 + 2 > 0", "∀x:int. 1 + 2 > 0")), chain(expect("3 > 0", "1 + 2 > 0"))); + } + + @Test + void simplifyOnceAppliesBinderSimplificationBeforeLogicalSimplification() { + VCImplication implication = vc("∀x:int. true", "y && true"); + + assertSimplificationSteps(VCSimplification::simplifyOnce, implication, + chain(expect("y && true", "∀x:int. y && true")), chain(expect("y", "y && true"))); + } + @Test void simplifyOnceAppliesFoldingWhenNoSubstitutionIsAvailable() { VCImplication implication = vc("1 + 2 > 2"); @@ -91,6 +116,13 @@ void simplifyKeepsApplyingStepsUntilFixedPoint() { chain(expect("4 > 3", "3 + 1 > 3")), chain(expect("true", "4 > 3"))); } + @Test + void simplifyToFixedPointRemovesTrueBindersOverMultipleSteps() { + VCImplication implication = vc("∀x:int. true", "∀y:int. true", "z > 0"); + + assertSimplifiedVC(VCSimplification.simplifyToFixedPoint(implication), expect("z > 0", "∀y:int. z > 0")); + } + @Test void simplifyAppliesMultipleSubstitutionsBeforeReachingFixedPoint() { VCImplication implication = vc("∀x:int. x == 3", "∀y:int. y == x + 1", "y > x");