From ea7ad09cb0d68e5c64fc61e3c8f6f1d1ba7b13d5 Mon Sep 17 00:00:00 2001 From: Ricardo Costa Date: Thu, 18 Jun 2026 15:13:44 +0100 Subject: [PATCH 1/5] Track Simplification Origins by Full VC Implication --- .../diagnostics/errors/RefinementError.java | 15 ++-- .../errors/StateRefinementError.java | 11 ++- .../processor/SimplifiedVCImplication.java | 53 -------------- .../liquidjava/processor/VCImplication.java | 18 +---- .../liquidjava/rj_language/Predicate.java | 7 +- .../opt/VCBinderSimplification.java | 17 ++--- .../opt/VCExpressionSimplificationPass.java | 7 +- .../rj_language/opt/VCSimplification.java | 24 ++++--- .../opt/VCSimplificationResult.java | 44 ++++++++++++ .../opt/VCSimplificationUtils.java | 5 ++ .../rj_language/opt/VCSubstitution.java | 9 ++- .../opt/VCArithmeticSimplificationTest.java | 9 +-- .../rj_language/opt/VCFoldingTest.java | 15 +--- .../opt/VCLogicalSimplificationTest.java | 9 +-- .../VCSimplificationPropertyBasedTest.java | 4 +- .../rj_language/opt/VCSimplificationTest.java | 71 ++++++++++++++----- .../rj_language/opt/VCSubstitutionTest.java | 3 +- .../java/liquidjava/utils/VCTestUtils.java | 43 ++++++----- 18 files changed, 182 insertions(+), 182 deletions(-) delete mode 100644 liquidjava-verifier/src/main/java/liquidjava/processor/SimplifiedVCImplication.java create mode 100644 liquidjava-verifier/src/main/java/liquidjava/rj_language/opt/VCSimplificationResult.java 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 e56ce3c8..78b5e0aa 100644 --- a/liquidjava-verifier/src/main/java/liquidjava/diagnostics/errors/RefinementError.java +++ b/liquidjava-verifier/src/main/java/liquidjava/diagnostics/errors/RefinementError.java @@ -9,6 +9,7 @@ import liquidjava.rj_language.Predicate; import liquidjava.rj_language.ast.Expression; import liquidjava.rj_language.ast.formatter.VariableFormatter; +import liquidjava.rj_language.opt.VCSimplificationResult; import liquidjava.smt.Counterexample; import spoon.reflect.cu.SourcePosition; @@ -20,13 +21,15 @@ public class RefinementError extends LJError { private final Predicate expected; - private final VCImplication found; + private final VCSimplificationResult found; private final Counterexample counterexample; - public RefinementError(SourcePosition position, Predicate expected, VCImplication found, + public RefinementError(SourcePosition position, Predicate expected, VCSimplificationResult found, TranslationTable translationTable, Counterexample counterexample, String customMessage) { - super("Refinement Error", String.format("%s is not a subtype of %s", - found.toPredicate().getExpression().toDisplayString(), expected.getExpression().toDisplayString()), + super("Refinement Error", + String.format("%s is not a subtype of %s", + found.getImplication().toPredicate().getExpression().toDisplayString(), + expected.getExpression().toDisplayString()), position, translationTable, customMessage); this.expected = expected; this.found = found; @@ -46,7 +49,7 @@ public String getCounterExampleString() { return null; List foundVarNames = new ArrayList<>(); - Expression foundExpression = found.toPredicate().getExpression(); + Expression foundExpression = getFound().getImplication().toPredicate().getExpression(); Expression expectedExpression = expected.getExpression(); foundExpression.getVariableNames(foundVarNames); // also keep resolved static-final constants (e.g. Integer.MAX_VALUE) referenced by either side of the @@ -77,7 +80,7 @@ public Predicate getExpected() { return expected; } - public VCImplication getFound() { + public VCSimplificationResult getFound() { return found; } } 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 874ccd92..763c8579 100644 --- a/liquidjava-verifier/src/main/java/liquidjava/diagnostics/errors/StateRefinementError.java +++ b/liquidjava-verifier/src/main/java/liquidjava/diagnostics/errors/StateRefinementError.java @@ -3,6 +3,7 @@ import liquidjava.diagnostics.TranslationTable; import liquidjava.processor.VCImplication; import liquidjava.rj_language.Predicate; +import liquidjava.rj_language.opt.VCSimplificationResult; import spoon.reflect.cu.SourcePosition; /** @@ -13,13 +14,13 @@ public class StateRefinementError extends LJError { private final Predicate expected; - private final VCImplication found; + private final VCSimplificationResult found; - public StateRefinementError(SourcePosition position, Predicate expected, VCImplication found, + public StateRefinementError(SourcePosition position, Predicate expected, VCSimplificationResult found, TranslationTable translationTable, String customMessage) { super("State Refinement Error", String.format("Expected state %s but found %s", expected.getExpression().toDisplayString(), - found.toPredicate().getExpression().toDisplayString()), + found.getImplication().toPredicate().getExpression().toDisplayString()), position, translationTable, customMessage); this.expected = expected; this.found = found; @@ -30,6 +31,10 @@ public Predicate getExpected() { } public VCImplication getFound() { + return found.getImplication(); + } + + public VCSimplificationResult getFoundSimplification() { return found; } } diff --git a/liquidjava-verifier/src/main/java/liquidjava/processor/SimplifiedVCImplication.java b/liquidjava-verifier/src/main/java/liquidjava/processor/SimplifiedVCImplication.java deleted file mode 100644 index 7c741cde..00000000 --- a/liquidjava-verifier/src/main/java/liquidjava/processor/SimplifiedVCImplication.java +++ /dev/null @@ -1,53 +0,0 @@ -package liquidjava.processor; - -import java.util.Objects; - -import liquidjava.rj_language.Predicate; - -/** - * Represents a VC implication node whose refinement was simplified from another quantified VC shape. - */ -public class SimplifiedVCImplication extends VCImplication { - - private final VCImplication origin; - - public SimplifiedVCImplication(VCImplication implication, Predicate refinement, VCImplication origin) { - super(implication, refinement); - this.origin = origin.clone(); - } - - @Override - public VCImplication getOrigin() { - return origin; - } - - @Override - public VCImplication copyWithRefinement(Predicate refinement) { - return new SimplifiedVCImplication(this, refinement, origin); - } - - @Override - public SimplifiedVCImplication clone() { - SimplifiedVCImplication vc = new SimplifiedVCImplication(this, this.refinement.clone(), origin); - if (this.next != null) - vc.next = this.next.clone(); - return vc; - } - - @Override - public int hashCode() { - return Objects.hash(super.hashCode(), origin); - } - - @Override - public boolean equals(Object obj) { - if (this == obj) - return true; - if (!(obj instanceof SimplifiedVCImplication)) - return false; - if (!super.equals(obj)) - return false; - SimplifiedVCImplication other = (SimplifiedVCImplication) obj; - return origin.equals(other.origin); - } -} diff --git a/liquidjava-verifier/src/main/java/liquidjava/processor/VCImplication.java b/liquidjava-verifier/src/main/java/liquidjava/processor/VCImplication.java index 2130ee18..37ea117b 100644 --- a/liquidjava-verifier/src/main/java/liquidjava/processor/VCImplication.java +++ b/liquidjava-verifier/src/main/java/liquidjava/processor/VCImplication.java @@ -4,6 +4,7 @@ import liquidjava.rj_language.Predicate; import liquidjava.rj_language.opt.VCSimplification; +import liquidjava.rj_language.opt.VCSimplificationResult; import liquidjava.utils.Utils; import spoon.reflect.reference.CtTypeReference; @@ -32,21 +33,6 @@ public VCImplication(VCImplication implication, Predicate ref) { this.refinement = ref; } - public VCImplication getOrigin() { - return null; - } - - public Predicate getOriginRefinement() { - VCImplication origin = getOrigin(); - if (origin == null) - return refinement.clone(); - return origin.getRefinement().clone(); - } - - public VCImplication copyWithRefinement(Predicate refinement) { - return new VCImplication(this, refinement); - } - public void setNext(VCImplication c) { next = c; } @@ -89,7 +75,7 @@ public String toString() { return String.format("%-20s %s", "", refinement.toString()); } - public VCImplication simplify() { + public VCSimplificationResult simplify() { return VCSimplification.simplifyToFixedPoint(this); } diff --git a/liquidjava-verifier/src/main/java/liquidjava/rj_language/Predicate.java b/liquidjava-verifier/src/main/java/liquidjava/rj_language/Predicate.java index 303551cf..0516b098 100644 --- a/liquidjava-verifier/src/main/java/liquidjava/rj_language/Predicate.java +++ b/liquidjava-verifier/src/main/java/liquidjava/rj_language/Predicate.java @@ -10,6 +10,7 @@ import liquidjava.diagnostics.errors.LJError; import liquidjava.diagnostics.errors.NotFoundError; import liquidjava.processor.VCImplication; +import liquidjava.rj_language.opt.VCSimplificationResult; import liquidjava.processor.context.AliasWrapper; import liquidjava.processor.context.Context; import liquidjava.processor.context.GhostFunction; @@ -259,12 +260,6 @@ public Predicate getOrigin() { return this; } - public VCImplication simplify() { - VCImplication result = new VCImplication(clone()).simplify(); - DebugLog.simplification(this.getExpression(), result.getRefinement().getExpression()); - return result; - } - private static boolean isBooleanLiteral(Expression expr, boolean value) { return expr instanceof LiteralBoolean && expr.isBooleanTrue() == value; } 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 d5dbf55a..3b5f2866 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 @@ -1,10 +1,10 @@ package liquidjava.rj_language.opt; import static liquidjava.rj_language.opt.VCSimplificationUtils.containsVar; +import static liquidjava.rj_language.opt.VCSimplificationUtils.copyWithRefinement; import static liquidjava.rj_language.opt.VCSimplificationUtils.isFalse; import static liquidjava.rj_language.opt.VCSimplificationUtils.isTrue; -import liquidjava.processor.SimplifiedVCImplication; import liquidjava.processor.VCImplication; import liquidjava.rj_language.Predicate; import liquidjava.rj_language.ast.LiteralBoolean; @@ -41,7 +41,7 @@ private VCImplication simplify(VCImplication implication) { if (next == null) return null; - VCImplication result = implication.copyWithRefinement(implication.getRefinement().clone()); + VCImplication result = copyWithRefinement(implication, implication.getRefinement().clone()); result.setNext(next); return result; } @@ -53,17 +53,12 @@ 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; - } + if (next != null) + return next.clone(); // ∀x. true -> true Predicate truePredicate = new Predicate(new LiteralBoolean(true)); - return new SimplifiedVCImplication(new VCImplication(truePredicate), truePredicate, implication); + return new VCImplication(truePredicate); } /** @@ -72,7 +67,7 @@ private VCImplication removeTrueBinder(VCImplication implication) { private VCImplication collapseFalseBinder(VCImplication implication) { // ∀x. false => P -> true Predicate truePredicate = new Predicate(new LiteralBoolean(true)); - return new SimplifiedVCImplication(new VCImplication(truePredicate), truePredicate, implication); + return new VCImplication(truePredicate); } /** diff --git a/liquidjava-verifier/src/main/java/liquidjava/rj_language/opt/VCExpressionSimplificationPass.java b/liquidjava-verifier/src/main/java/liquidjava/rj_language/opt/VCExpressionSimplificationPass.java index c4baf16a..5f40533c 100644 --- a/liquidjava-verifier/src/main/java/liquidjava/rj_language/opt/VCExpressionSimplificationPass.java +++ b/liquidjava-verifier/src/main/java/liquidjava/rj_language/opt/VCExpressionSimplificationPass.java @@ -1,6 +1,7 @@ package liquidjava.rj_language.opt; -import liquidjava.processor.SimplifiedVCImplication; +import static liquidjava.rj_language.opt.VCSimplificationUtils.copyWithRefinement; + import liquidjava.processor.VCImplication; import liquidjava.rj_language.Predicate; import liquidjava.rj_language.ast.Expression; @@ -32,7 +33,7 @@ private VCImplication apply(VCImplication implication, C context) { Expression expression = implication.getRefinement().getExpression(); Expression simplified = simplify(expression, context); if (!expression.equals(simplified)) { - VCImplication result = new SimplifiedVCImplication(implication, new Predicate(simplified), implication); + VCImplication result = copyWithRefinement(implication, new Predicate(simplified)); result.setNext(implication.getNext() == null ? null : implication.getNext().clone()); return result; } @@ -41,7 +42,7 @@ private VCImplication apply(VCImplication implication, C context) { if (implication.getNext() == null || implication.getNext().equals(next)) return implication; - VCImplication result = implication.copyWithRefinement(implication.getRefinement().clone()); + VCImplication result = copyWithRefinement(implication, implication.getRefinement().clone()); result.setNext(next); return result; } 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 b26af0e6..4de3ff94 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 @@ -15,16 +15,15 @@ public class VCSimplification { /** * Applies all available simplification steps to a VC chain until a fixed point is reached */ - public static VCImplication simplifyToFixedPoint(VCImplication implication) { + public static VCSimplificationResult simplifyToFixedPoint(VCImplication implication) { if (implication == null) return null; - // keep applying simplification steps until a fixed point is reached - VCImplication current = implication.clone(); + VCSimplificationResult current = new VCSimplificationResult(implication); while (true) { - VCImplication simplified = simplifyOnce(current); - if (current.equals(simplified)) - return simplified; // fixed point reached + VCSimplificationResult simplified = simplifyOnce(current.getImplication(), current); + if (simplified.getOrigin() == null) + return current; // fixed point reached current = simplified; } } @@ -32,15 +31,22 @@ public static VCImplication simplifyToFixedPoint(VCImplication implication) { /** * Applies one simplification step to a VC chain */ - public static VCImplication simplifyOnce(VCImplication implication) { + public static VCSimplificationResult simplifyOnce(VCImplication implication) { if (implication == null) return null; + return simplifyOnce(implication, new VCSimplificationResult(implication)); + } + + /** + * Applies one simplification step to a VC chain, keeping track of the origin of the simplification + */ + private static VCSimplificationResult simplifyOnce(VCImplication implication, VCSimplificationResult origin) { for (VCSimplificationPass pass : PASSES) { VCImplication simplified = pass.apply(implication); if (!implication.equals(simplified)) - return simplified; + return new VCSimplificationResult(simplified, origin); } - return implication; + return new VCSimplificationResult(implication); } } 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 new file mode 100644 index 00000000..30ef879d --- /dev/null +++ b/liquidjava-verifier/src/main/java/liquidjava/rj_language/opt/VCSimplificationResult.java @@ -0,0 +1,44 @@ +package liquidjava.rj_language.opt; + +import java.util.Objects; + +import liquidjava.processor.VCImplication; + +/** + * Result of simplifying VC implication chain + */ +public final class VCSimplificationResult { + + private final VCImplication implication; + private final VCSimplificationResult origin; + + public VCSimplificationResult(VCImplication implication) { + this(implication, null); + } + + public VCSimplificationResult(VCImplication implication, VCSimplificationResult origin) { + this.implication = Objects.requireNonNull(implication).clone(); + this.origin = origin; + } + + /** + * Returns the simplified VC chain represented by this result + */ + public VCImplication getImplication() { + return implication; + } + + /** + * Returns the origin of this simplification result or null if this result is the original VC chain + */ + public VCSimplificationResult getOrigin() { + return origin; + } + + @Override + public String toString() { + if (origin == null) + return "\n" + implication; + return "\n" + implication + "\n" + origin.toString().indent(2).stripTrailing(); + } +} 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 43b7aed5..042aa413 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 @@ -4,11 +4,16 @@ import java.util.List; import liquidjava.processor.VCImplication; +import liquidjava.rj_language.Predicate; import liquidjava.rj_language.ast.Expression; import liquidjava.rj_language.ast.LiteralBoolean; public final class VCSimplificationUtils { + public static VCImplication copyWithRefinement(VCImplication implication, Predicate refinement) { + return new VCImplication(implication, refinement); + } + public static boolean containsVar(Expression expression, String name) { List names = new ArrayList<>(); expression.getVariableNames(names); diff --git a/liquidjava-verifier/src/main/java/liquidjava/rj_language/opt/VCSubstitution.java b/liquidjava-verifier/src/main/java/liquidjava/rj_language/opt/VCSubstitution.java index 556ab9e1..e08a058c 100644 --- a/liquidjava-verifier/src/main/java/liquidjava/rj_language/opt/VCSubstitution.java +++ b/liquidjava-verifier/src/main/java/liquidjava/rj_language/opt/VCSubstitution.java @@ -1,10 +1,10 @@ package liquidjava.rj_language.opt; import static liquidjava.rj_language.opt.VCSimplificationUtils.containsVar; +import static liquidjava.rj_language.opt.VCSimplificationUtils.copyWithRefinement; import java.util.Optional; -import liquidjava.processor.SimplifiedVCImplication; import liquidjava.processor.VCImplication; import liquidjava.rj_language.Predicate; import liquidjava.rj_language.ast.BinaryExpression; @@ -56,16 +56,15 @@ private VCImplication substitute(VCImplication implication, VCImplication node, } /** - * Substitutes a source binder inside one VC node while preserving simplification metadata + * Substitutes a source binder inside one VC node */ private VCImplication substituteNode(VCImplication implication, VCImplication node, Expression replacement) { Expression exp = implication.getRefinement().getExpression().clone(); if (!containsVar(exp, node.getName())) - return implication.copyWithRefinement(new Predicate(exp)); + return copyWithRefinement(implication, new Predicate(exp)); Expression substituted = exp.substitute(new Var(node.getName()), replacement.clone()); - VCImplication origin = new VCImplication(node.getName(), node.getType(), implication.getOriginRefinement()); - return new SimplifiedVCImplication(implication, new Predicate(substituted), origin); + return copyWithRefinement(implication, new Predicate(substituted)); } /** diff --git a/liquidjava-verifier/src/test/java/liquidjava/rj_language/opt/VCArithmeticSimplificationTest.java b/liquidjava-verifier/src/test/java/liquidjava/rj_language/opt/VCArithmeticSimplificationTest.java index 349d8a31..bac89371 100644 --- a/liquidjava-verifier/src/test/java/liquidjava/rj_language/opt/VCArithmeticSimplificationTest.java +++ b/liquidjava-verifier/src/test/java/liquidjava/rj_language/opt/VCArithmeticSimplificationTest.java @@ -1,10 +1,6 @@ package liquidjava.rj_language.opt; import static liquidjava.utils.VCTestUtils.*; -import static org.junit.jupiter.api.Assertions.assertEquals; -import static org.junit.jupiter.api.Assertions.assertInstanceOf; - -import liquidjava.processor.SimplifiedVCImplication; import liquidjava.processor.VCImplication; import org.junit.jupiter.api.Test; @@ -67,10 +63,7 @@ void simplifiesOnlyFirstArithmeticIdentity() { void recordsOriginWhenSimplifyingLaterImplication() { VCImplication implication = vc("x > 0", "y + 0 > x"); - VCImplication result = assertSimplificationSteps(simplification::apply, implication, + assertSimplificationSteps(simplification::apply, implication, chain(expect("x > 0"), expect("y > x", "y + 0 > x"))); - - SimplifiedVCImplication simplifiedNext = assertInstanceOf(SimplifiedVCImplication.class, result.getNext()); - assertEquals("y + 0 > x", simplifiedNext.getOrigin().getRefinement().getExpression().toDisplayString()); } } diff --git a/liquidjava-verifier/src/test/java/liquidjava/rj_language/opt/VCFoldingTest.java b/liquidjava-verifier/src/test/java/liquidjava/rj_language/opt/VCFoldingTest.java index 64df5d85..140946c3 100644 --- a/liquidjava-verifier/src/test/java/liquidjava/rj_language/opt/VCFoldingTest.java +++ b/liquidjava-verifier/src/test/java/liquidjava/rj_language/opt/VCFoldingTest.java @@ -2,14 +2,10 @@ import static liquidjava.utils.VCTestUtils.*; import static org.junit.jupiter.api.Assertions.assertEquals; -import static org.junit.jupiter.api.Assertions.assertInstanceOf; - -import liquidjava.processor.SimplifiedVCImplication; import liquidjava.processor.VCImplication; import liquidjava.rj_language.Predicate; import liquidjava.rj_language.ast.BinaryExpression; import liquidjava.rj_language.ast.Enum; -import liquidjava.rj_language.ast.GroupExpression; import liquidjava.rj_language.ast.LiteralInt; import org.junit.jupiter.api.Test; @@ -161,9 +157,7 @@ void recordsOriginWhenOnlyGroupIsUnwrapped() { VCImplication implication = vc("(x > 0)"); VCImplication result = assertSimplificationSteps(folding::apply, implication, chain(expect("x > 0", "x > 0"))); - SimplifiedVCImplication simplified = assertInstanceOf(SimplifiedVCImplication.class, result); - assertEquals("x > 0", simplified.getRefinement().toString()); - assertInstanceOf(GroupExpression.class, simplified.getOrigin().getRefinement().getExpression()); + assertEquals("x > 0", result.getRefinement().toString()); } @Test @@ -173,13 +167,8 @@ void recordsOriginWhenFoldingLaterImplication() { VCImplication result = assertSimplificationSteps(folding::apply, implication, chain(expect("x > 0"), expect("3 > 0", "1 + 2 > 0"))); - SimplifiedVCImplication simplifiedNext = assertInstanceOf(SimplifiedVCImplication.class, result.getNext()); - assertEquals("1 + 2 > 0", simplifiedNext.getOrigin().getRefinement().getExpression().toDisplayString()); - result = assertSimplificationSteps(folding::apply, result, chain(expect("x > 0"), expect("true", "3 > 0"))); - - simplifiedNext = assertInstanceOf(SimplifiedVCImplication.class, result.getNext()); - assertEquals("3 > 0", simplifiedNext.getOrigin().getRefinement().getExpression().toDisplayString()); + assertEquals("true", result.getNext().getRefinement().getExpression().toDisplayString()); } } diff --git a/liquidjava-verifier/src/test/java/liquidjava/rj_language/opt/VCLogicalSimplificationTest.java b/liquidjava-verifier/src/test/java/liquidjava/rj_language/opt/VCLogicalSimplificationTest.java index 673025f0..5d3e3ccd 100644 --- a/liquidjava-verifier/src/test/java/liquidjava/rj_language/opt/VCLogicalSimplificationTest.java +++ b/liquidjava-verifier/src/test/java/liquidjava/rj_language/opt/VCLogicalSimplificationTest.java @@ -1,10 +1,6 @@ package liquidjava.rj_language.opt; import static liquidjava.utils.VCTestUtils.*; -import static org.junit.jupiter.api.Assertions.assertEquals; -import static org.junit.jupiter.api.Assertions.assertInstanceOf; - -import liquidjava.processor.SimplifiedVCImplication; import liquidjava.processor.VCImplication; import org.junit.jupiter.api.Test; @@ -75,10 +71,7 @@ void simplifiesIteChildren() { void recordsOriginWhenSimplifyingLaterImplication() { VCImplication implication = vc("x > 0", "y || false"); - VCImplication result = assertSimplificationSteps(simplification::apply, implication, + assertSimplificationSteps(simplification::apply, implication, chain(expect("x > 0"), expect("y", "y || false"))); - - SimplifiedVCImplication simplifiedNext = assertInstanceOf(SimplifiedVCImplication.class, result.getNext()); - assertEquals("y || false", simplifiedNext.getOrigin().getRefinement().getExpression().toDisplayString()); } } 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 8a638ddc..4ed71a94 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 @@ -32,9 +32,11 @@ public void eachSimplificationStepPreservesVcSemantics(@From(VCImplicationGenera VCImplication current = vc; for (int step = 0; step < MAX_STEPS; step++) { - VCImplication simplified = VCSimplification.simplifyOnce(current); + VCSimplificationResult result = VCSimplification.simplifyOnce(current); + VCImplication simplified = result.getImplication(); if (current.equals(simplified)) return; + assertTrue(current.equals(result.getOrigin().getImplication())); assertEquivalent(current, simplified, step); current = simplified; } 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 62514f4e..79cbde0f 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 @@ -1,6 +1,8 @@ package liquidjava.rj_language.opt; import static liquidjava.utils.VCTestUtils.*; +import static org.junit.jupiter.api.Assertions.assertEquals; +import static org.junit.jupiter.api.Assertions.assertNotNull; import static org.junit.jupiter.api.Assertions.assertNull; import liquidjava.processor.VCImplication; @@ -22,7 +24,7 @@ void simplifyOnceReturnsNullForNullImplication() { void simplifyOnceAppliesSubstitutionBeforeFolding() { VCImplication implication = vc("∀x:int. x == 1 + 2", "x > 2"); - assertSimplificationSteps(VCSimplification::simplifyOnce, implication, + assertSimplificationResults(VCSimplification::simplifyOnce, implication, chain(expect("1 + 2 > 2", "∀x:int. x > 2")), chain(expect("3 > 2", "1 + 2 > 2")), chain(expect("true", "3 > 2"))); } @@ -31,7 +33,7 @@ void simplifyOnceAppliesSubstitutionBeforeFolding() { void simplifyOnceDoesNotFoldAfterSubstitutionInSameStep() { VCImplication implication = vc("∀x:int. x == 1 + 2", "x == 3"); - assertSimplificationSteps(VCSimplification::simplifyOnce, implication, + assertSimplificationResults(VCSimplification::simplifyOnce, implication, chain(expect("1 + 2 == 3", "∀x:int. x == 3")), chain(expect("3 == 3", "1 + 2 == 3")), chain(expect("true", "3 == 3"))); } @@ -40,7 +42,7 @@ void simplifyOnceDoesNotFoldAfterSubstitutionInSameStep() { void simplifyOnceAppliesSubstitutionBeforeBinderSimplification() { VCImplication implication = vc("∀x:int. x == 3", "∀y:int. true", "x > 0"); - assertSimplificationSteps(VCSimplification::simplifyOnce, implication, + assertSimplificationResults(VCSimplification::simplifyOnce, implication, chain(expect("true"), expect("3 > 0", "∀x:int. x > 0")), chain(expect("3 > 0", "∀y:int. x > 0")), chain(expect("true", "3 > 0"))); } @@ -49,7 +51,7 @@ void simplifyOnceAppliesSubstitutionBeforeBinderSimplification() { void simplifyOnceAppliesBinderSimplificationBeforeFolding() { VCImplication implication = vc("∀x:int. true", "1 + 2 > 0"); - assertSimplificationSteps(VCSimplification::simplifyOnce, implication, + assertSimplificationResults(VCSimplification::simplifyOnce, implication, chain(expect("1 + 2 > 0", "∀x:int. 1 + 2 > 0")), chain(expect("3 > 0", "1 + 2 > 0"))); } @@ -57,7 +59,7 @@ void simplifyOnceAppliesBinderSimplificationBeforeFolding() { void simplifyOnceAppliesBinderSimplificationBeforeLogicalSimplification() { VCImplication implication = vc("∀x:int. true", "y && true"); - assertSimplificationSteps(VCSimplification::simplifyOnce, implication, + assertSimplificationResults(VCSimplification::simplifyOnce, implication, chain(expect("y && true", "∀x:int. y && true")), chain(expect("y", "y && true"))); } @@ -65,7 +67,7 @@ void simplifyOnceAppliesBinderSimplificationBeforeLogicalSimplification() { void simplifyOnceAppliesFoldingWhenNoSubstitutionIsAvailable() { VCImplication implication = vc("1 + 2 > 2"); - assertSimplificationSteps(VCSimplification::simplifyOnce, implication, chain(expect("3 > 2", "1 + 2 > 2")), + assertSimplificationResults(VCSimplification::simplifyOnce, implication, chain(expect("3 > 2", "1 + 2 > 2")), chain(expect("true", "3 > 2"))); } @@ -73,7 +75,7 @@ void simplifyOnceAppliesFoldingWhenNoSubstitutionIsAvailable() { void simplifyOnceAppliesFoldingBeforeArithmeticSimplification() { VCImplication implication = vc("1 + 2 + x + 0 > 0"); - assertSimplificationSteps(VCSimplification::simplifyOnce, implication, + assertSimplificationResults(VCSimplification::simplifyOnce, implication, chain(expect("3 + x + 0 > 0", "1 + 2 + x + 0 > 0"))); } @@ -81,14 +83,14 @@ void simplifyOnceAppliesFoldingBeforeArithmeticSimplification() { void simplifyOnceAppliesArithmeticWhenNoSubstitutionOrFoldingIsAvailable() { VCImplication implication = vc("x + 0 > 0"); - assertSimplificationSteps(VCSimplification::simplifyOnce, implication, chain(expect("x > 0", "x + 0 > 0"))); + assertSimplificationResults(VCSimplification::simplifyOnce, implication, chain(expect("x > 0", "x + 0 > 0"))); } @Test void simplifyOnceAppliesArithmeticBeforeLogicalSimplification() { VCImplication implication = vc("x + 0 == x"); - assertSimplificationSteps(VCSimplification::simplifyOnce, implication, chain(expect("x == x", "x + 0 == x")), + assertSimplificationResults(VCSimplification::simplifyOnce, implication, chain(expect("x == x", "x + 0 == x")), chain(expect("true", "x == x"))); } @@ -96,14 +98,14 @@ void simplifyOnceAppliesArithmeticBeforeLogicalSimplification() { void simplifyOnceAppliesLogicalWhenNoEarlierSimplificationIsAvailable() { VCImplication implication = vc("x && true"); - assertSimplificationSteps(VCSimplification::simplifyOnce, implication, chain(expect("x", "x && true"))); + assertSimplificationResults(VCSimplification::simplifyOnce, implication, chain(expect("x", "x && true"))); } @Test void simplifyAppliesLogicalStepsUntilFixedPoint() { VCImplication implication = vc("x && true && true"); - assertSimplificationSteps(VCSimplification::simplifyOnce, implication, + assertSimplificationResults(VCSimplification::simplifyOnce, implication, chain(expect("x && true", "x && true && true")), chain(expect("x", "x && true"))); } @@ -111,7 +113,7 @@ void simplifyAppliesLogicalStepsUntilFixedPoint() { void simplifyKeepsApplyingStepsUntilFixedPoint() { VCImplication implication = vc("∀x:int. x == 1 + 2", "x + 1 > 3"); - assertSimplificationSteps(VCSimplification::simplifyOnce, implication, + assertSimplificationResults(VCSimplification::simplifyOnce, implication, chain(expect("1 + 2 + 1 > 3", "∀x:int. x + 1 > 3")), chain(expect("3 + 1 > 3", "1 + 2 + 1 > 3")), chain(expect("4 > 3", "3 + 1 > 3")), chain(expect("true", "4 > 3"))); } @@ -120,16 +122,20 @@ void simplifyKeepsApplyingStepsUntilFixedPoint() { void simplifyToFixedPointRemovesTrueBindersOverMultipleSteps() { VCImplication implication = vc("∀x:int. true", "∀y:int. true", "z > 0"); - assertSimplifiedVC(VCSimplification.simplifyToFixedPoint(implication), expect("z > 0", "∀y:int. z > 0")); + VCSimplificationResult result = VCSimplification.simplifyToFixedPoint(implication); + + assertSimplifiedVC(result.getImplication(), expect("z > 0", "∀y:int. z > 0")); + assertNotNull(result.getOrigin()); + assertNotNull(result.getOrigin().getOrigin()); } @Test void simplifyAppliesMultipleSubstitutionsBeforeReachingFixedPoint() { VCImplication implication = vc("∀x:int. x == 3", "∀y:int. y == x + 1", "y > x"); - assertSimplificationSteps(VCSimplification::simplifyOnce, implication, + assertSimplificationResults(VCSimplification::simplifyOnce, implication, chain(expect("y == 3 + 1", "∀x:int. y == x + 1"), expect("y > 3", "∀x:int. y > x")), - chain(expect("3 + 1 > 3", "∀y:int. y > x")), chain(expect("4 > 3", "3 + 1 > 3")), + chain(expect("3 + 1 > 3", "∀y:int. y > 3")), chain(expect("4 > 3", "3 + 1 > 3")), chain(expect("true", "4 > 3"))); } @@ -137,7 +143,7 @@ void simplifyAppliesMultipleSubstitutionsBeforeReachingFixedPoint() { void simplifyAppliesLongSubstitutionChainBeforeReachingFixedPoint() { VCImplication implication = vc("∀x:int. x == 1", "∀y:int. y == x + 1", "∀z:int. z == y + 1", "z == 3"); - assertSimplificationSteps(VCSimplification::simplifyOnce, implication, + assertSimplificationResults(VCSimplification::simplifyOnce, implication, chain(expect("y == 1 + 1", "∀x:int. y == x + 1"), expect("z == y + 1"), expect("z == 3")), chain(expect("z == 1 + 1 + 1", "∀y:int. z == y + 1"), expect("z == 3")), chain(expect("1 + 1 + 1 == 3", "∀z:int. z == 3")), chain(expect("2 + 1 == 3", "1 + 1 + 1 == 3")), @@ -148,7 +154,7 @@ void simplifyAppliesLongSubstitutionChainBeforeReachingFixedPoint() { void simplifyCombinesSubstitutionAndNestedFoldingAcrossFixedPoint() { VCImplication implication = vc("∀x:int. x == 1", "∀y:int. y == x + 2", "y - 1 == 2"); - assertSimplificationSteps(VCSimplification::simplifyOnce, implication, + assertSimplificationResults(VCSimplification::simplifyOnce, implication, chain(expect("y == 1 + 2", "∀x:int. y == x + 2"), expect("y - 1 == 2")), chain(expect("1 + 2 - 1 == 2", "∀y:int. y - 1 == 2")), chain(expect("3 - 1 == 2", "1 + 2 - 1 == 2")), chain(expect("2 == 2", "3 - 1 == 2")), chain(expect("true", "2 == 2"))); @@ -158,7 +164,7 @@ void simplifyCombinesSubstitutionAndNestedFoldingAcrossFixedPoint() { void simplifyStopsAfterSubstitutionWhenOnlyNegativeLiteralShapeChanges() { VCImplication implication = vc("∀x:int. x == a + 0", "x >= -3"); - assertSimplificationSteps(VCSimplification::simplifyOnce, implication, + assertSimplificationResults(VCSimplification::simplifyOnce, implication, chain(expect("a + 0 >= -3", "∀x:int. x >= -3"))); } @@ -166,6 +172,33 @@ void simplifyStopsAfterSubstitutionWhenOnlyNegativeLiteralShapeChanges() { void simplifyLeavesUnchangedVcAsPlainPredicates() { VCImplication implication = vc("x > 0", "y > x"); - assertSimplificationSteps(VCSimplification::simplifyOnce, implication, chain(expect("x > 0"), expect("y > x"))); + VCSimplificationResult result = VCSimplification.simplifyOnce(implication); + + assertSimplifiedVC(result.getImplication(), expect("x > 0"), expect("y > x")); + assertNull(result.getOrigin()); + } + + @Test + void simplifyOnceStoresACompleteClonedOriginChain() { + VCImplication implication = vc("x > 0", "y + 0 > x"); + + VCSimplificationResult result = VCSimplification.simplifyOnce(implication); + implication.getNext().setRefinement(vc("changed").getRefinement()); + + assertSimplifiedVC(result.getImplication(), expect("x > 0"), expect("y > x")); + assertSimplifiedVC(result.getOrigin().getImplication(), expect("x > 0"), expect("y + 0 > x")); + } + + @Test + void fixedPointHistoryLinksEverySuccessfulStep() { + VCImplication implication = vc("∀x:int. x == 1 + 2", "x + 0 > 2"); + + VCSimplificationResult result = VCSimplification.simplifyToFixedPoint(implication); + int historyLength = 0; + for (VCSimplificationResult current = result.getOrigin(); current != null; current = current.getOrigin()) + historyLength++; + + assertEquals(4, historyLength); + assertSimplifiedVC(result.getImplication(), expect("true")); } } diff --git a/liquidjava-verifier/src/test/java/liquidjava/rj_language/opt/VCSubstitutionTest.java b/liquidjava-verifier/src/test/java/liquidjava/rj_language/opt/VCSubstitutionTest.java index 95d6c347..a9b13054 100644 --- a/liquidjava-verifier/src/test/java/liquidjava/rj_language/opt/VCSubstitutionTest.java +++ b/liquidjava-verifier/src/test/java/liquidjava/rj_language/opt/VCSubstitutionTest.java @@ -1,7 +1,6 @@ package liquidjava.rj_language.opt; import static liquidjava.utils.VCTestUtils.*; - import liquidjava.processor.VCImplication; import org.junit.jupiter.api.Test; @@ -88,7 +87,7 @@ void substitutesOuterKnownValueIntoNestedBinderRefinements() { assertSimplificationSteps(substitution::apply, implication, chain(expect("y == 3 + 1", "∀x:int. y == x + 1"), expect("y > 3", "∀x:int. y > x")), - chain(expect("3 + 1 > 3", "∀y:int. y > x"))); + chain(expect("3 + 1 > 3", "∀y:int. y > 3"))); } @Test diff --git a/liquidjava-verifier/src/test/java/liquidjava/utils/VCTestUtils.java b/liquidjava-verifier/src/test/java/liquidjava/utils/VCTestUtils.java index df051aaf..3556cf5e 100644 --- a/liquidjava-verifier/src/test/java/liquidjava/utils/VCTestUtils.java +++ b/liquidjava-verifier/src/test/java/liquidjava/utils/VCTestUtils.java @@ -1,13 +1,14 @@ package liquidjava.utils; import static org.junit.jupiter.api.Assertions.assertEquals; -import static org.junit.jupiter.api.Assertions.assertNotNull; import static org.junit.jupiter.api.Assertions.assertNull; +import java.util.function.Function; import java.util.function.UnaryOperator; import liquidjava.processor.VCImplication; import liquidjava.rj_language.Predicate; +import liquidjava.rj_language.opt.VCSimplificationResult; import liquidjava.rj_language.parsing.RefinementsParser; import spoon.Launcher; import spoon.reflect.reference.CtTypeReference; @@ -55,15 +56,7 @@ public static void assertSimplifiedVC(VCImplication implication, ExpectedSimplif assertEquals(Predicate.class, current.getRefinement().getClass(), "Expected simplified refinement at implication " + i + " to be a plain Predicate"); assertEquals(expectedPredicate.simplified(), formatRefinement(current), - "Unexpected simplified expression at implication " + i); - if (expectedPredicate.origin() == null) - assertNull(current.getOrigin(), "Unexpected origin VC at implication " + i); - else { - VCImplication origin = current.getOrigin(); - assertNotNull(origin, "Expected origin VC at implication " + i); - assertEquals(expectedPredicate.origin(), formatOrigin(origin), - "Unexpected origin VC at implication " + i); - } + "Unexpected simplified expression at implication " + i + sourceContext(expectedPredicate)); current = current.getNext(); } assertNull(current, "Expected VC chain to end after " + expected.length + " implications"); @@ -79,29 +72,41 @@ public static VCImplication assertSimplificationSteps(UnaryOperator simplifier, VCImplication implication, + ExpectedSimplificationStep... expectedSteps) { + VCSimplificationResult current = new VCSimplificationResult(implication); + for (ExpectedSimplificationStep expectedStep : expectedSteps) { + VCSimplificationResult result = simplifier.apply(current.getImplication()); + assertEquals(current.getImplication(), result.getOrigin().getImplication(), + "Unexpected whole-chain simplification origin"); + assertSimplifiedVC(result.getImplication(), expectedStep.implications()); + current = result; + } + return current; + } + public static ExpectedSimplificationStep chain(ExpectedSimplifiedVCImplication... implications) { return new ExpectedSimplificationStep(implications); } - public static ExpectedSimplifiedVCImplication expect(String simplified, String origin) { - return new ExpectedSimplifiedVCImplication(simplified, origin); + public static ExpectedSimplifiedVCImplication expect(String simplified, String source) { + return new ExpectedSimplifiedVCImplication(simplified, source); } public static ExpectedSimplifiedVCImplication expect(String simplified) { return new ExpectedSimplifiedVCImplication(simplified, null); } - private static String formatOrigin(VCImplication origin) { - if (!origin.hasBinder()) - return formatRefinement(origin); - return "∀" + origin.getName() + ":" + origin.getType().getQualifiedName() + ". " + formatRefinement(origin); - } - private static String formatRefinement(VCImplication implication) { return implication.getRefinement().getExpression().toDisplayString(); } - public record ExpectedSimplifiedVCImplication(String simplified, String origin) { + private static String sourceContext(ExpectedSimplifiedVCImplication expected) { + return expected.source() == null ? "" : " (rewrite source: " + expected.source() + ")"; + } + + public record ExpectedSimplifiedVCImplication(String simplified, String source) { } public record ExpectedSimplificationStep(ExpectedSimplifiedVCImplication... implications) { From 08ec7307e97a516b2f945d8ed3c7385b3fafdf3f Mon Sep 17 00:00:00 2001 From: Ricardo Costa Date: Thu, 18 Jun 2026 15:49:00 +0100 Subject: [PATCH 2/5] Refactoring --- .../rj_language/opt/VCSimplification.java | 35 ++++---- .../opt/VCArithmeticSimplificationTest.java | 53 +++++------ .../opt/VCBinderSimplificationTest.java | 16 ++-- .../rj_language/opt/VCFoldingTest.java | 90 ++++++++----------- .../opt/VCLogicalSimplificationTest.java | 46 +++++----- .../VCSimplificationPropertyBasedTest.java | 13 +-- .../rj_language/opt/VCSimplificationTest.java | 75 ++++++---------- .../rj_language/opt/VCSubstitutionTest.java | 35 ++++---- .../java/liquidjava/utils/VCTestUtils.java | 64 ++++++------- 9 files changed, 187 insertions(+), 240 deletions(-) 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 4de3ff94..b9678874 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 @@ -21,32 +21,35 @@ public static VCSimplificationResult simplifyToFixedPoint(VCImplication implicat VCSimplificationResult current = new VCSimplificationResult(implication); while (true) { - VCSimplificationResult simplified = simplifyOnce(current.getImplication(), current); - if (simplified.getOrigin() == null) + VCSimplificationResult simplified = simplifyOnce(current); + if (simplified == current) return current; // fixed point reached current = simplified; } } /** - * Applies one simplification step to a VC chain + * Applies one simplification step to a VC chain from all available simplification passes */ - public static VCSimplificationResult simplifyOnce(VCImplication implication) { - if (implication == null) - return null; - - return simplifyOnce(implication, new VCSimplificationResult(implication)); + public static VCSimplificationResult simplifyOnce(VCSimplificationResult implication) { + for (VCSimplificationPass pass : PASSES) { + VCSimplificationResult simplified = simplifyOnce(implication, pass); + if (simplified != implication) + return simplified; + } + return implication; } /** - * Applies one simplification step to a VC chain, keeping track of the origin of the simplification + * Applies one selected simplification pass to a VC chain */ - private static VCSimplificationResult simplifyOnce(VCImplication implication, VCSimplificationResult origin) { - for (VCSimplificationPass pass : PASSES) { - VCImplication simplified = pass.apply(implication); - if (!implication.equals(simplified)) - return new VCSimplificationResult(simplified, origin); - } - return new VCSimplificationResult(implication); + public static VCSimplificationResult simplifyOnce(VCSimplificationResult implication, VCSimplificationPass pass) { + if (implication == null) + return null; + + VCImplication simplified = pass.apply(implication.getImplication()); + if (implication.getImplication().equals(simplified)) + return implication; + return new VCSimplificationResult(simplified, implication); } } diff --git a/liquidjava-verifier/src/test/java/liquidjava/rj_language/opt/VCArithmeticSimplificationTest.java b/liquidjava-verifier/src/test/java/liquidjava/rj_language/opt/VCArithmeticSimplificationTest.java index bac89371..e0496dc3 100644 --- a/liquidjava-verifier/src/test/java/liquidjava/rj_language/opt/VCArithmeticSimplificationTest.java +++ b/liquidjava-verifier/src/test/java/liquidjava/rj_language/opt/VCArithmeticSimplificationTest.java @@ -10,60 +10,55 @@ class VCArithmeticSimplificationTest { @Test void simplifiesAdditiveIdentities() { - assertSimplificationSteps(simplification::apply, vc("x + 0 > 0"), chain(expect("x > 0", "x + 0 > 0"))); - assertSimplificationSteps(simplification::apply, vc("0 + x > 0"), chain(expect("x > 0", "0 + x > 0"))); - assertSimplificationSteps(simplification::apply, vc("x - 0 > 0"), chain(expect("x > 0", "x - 0 > 0"))); - assertSimplificationSteps(simplification::apply, vc("0 - x > 0"), chain(expect("-x > 0", "0 - x > 0"))); + assertSimplificationSteps(simplification, vc("x + 0 > 0"), step("x > 0")); + assertSimplificationSteps(simplification, vc("0 + x > 0"), step("x > 0")); + assertSimplificationSteps(simplification, vc("x - 0 > 0"), step("x > 0")); + assertSimplificationSteps(simplification, vc("0 - x > 0"), step("-x > 0")); } @Test void simplifiesNegatedAdditionAndSubtraction() { - assertSimplificationSteps(simplification::apply, vc("x + -x == 0"), chain(expect("0 == 0", "x + -x == 0"))); - assertSimplificationSteps(simplification::apply, vc("-x + x == 0"), chain(expect("0 == 0", "-x + x == 0"))); - assertSimplificationSteps(simplification::apply, vc("x - x == 0"), chain(expect("0 == 0", "x - x == 0"))); - assertSimplificationSteps(simplification::apply, vc("--x == x"), chain(expect("x == x", "-(-x) == x"))); - assertSimplificationSteps(simplification::apply, vc("x + -y == 0"), chain(expect("x - y == 0", "x + -y == 0"))); - assertSimplificationSteps(simplification::apply, vc("x - -y == 0"), chain(expect("x + y == 0", "x - -y == 0"))); + assertSimplificationSteps(simplification, vc("x + -x == 0"), step("0 == 0")); + assertSimplificationSteps(simplification, vc("-x + x == 0"), step("0 == 0")); + assertSimplificationSteps(simplification, vc("x - x == 0"), step("0 == 0")); + assertSimplificationSteps(simplification, vc("--x == x"), step("x == x")); + assertSimplificationSteps(simplification, vc("x + -y == 0"), step("x - y == 0")); + assertSimplificationSteps(simplification, vc("x - -y == 0"), step("x + y == 0")); } @Test void simplifiesMultiplicativeIdentities() { - assertSimplificationSteps(simplification::apply, vc("x * 1 > 0"), chain(expect("x > 0", "x * 1 > 0"))); - assertSimplificationSteps(simplification::apply, vc("1 * x > 0"), chain(expect("x > 0", "1 * x > 0"))); - assertSimplificationSteps(simplification::apply, vc("x * 0 == 0"), chain(expect("0 == 0", "x * 0 == 0"))); - assertSimplificationSteps(simplification::apply, vc("0 * x == 0"), chain(expect("0 == 0", "0 * x == 0"))); - assertSimplificationSteps(simplification::apply, vc("x / 1 > 0"), chain(expect("x > 0", "x / 1 > 0"))); - assertSimplificationSteps(simplification::apply, vc("x % 1 == 0"), chain(expect("0 == 0", "x % 1 == 0"))); + assertSimplificationSteps(simplification, vc("x * 1 > 0"), step("x > 0")); + assertSimplificationSteps(simplification, vc("1 * x > 0"), step("x > 0")); + assertSimplificationSteps(simplification, vc("x * 0 == 0"), step("0 == 0")); + assertSimplificationSteps(simplification, vc("0 * x == 0"), step("0 == 0")); + assertSimplificationSteps(simplification, vc("x / 1 > 0"), step("x > 0")); + assertSimplificationSteps(simplification, vc("x % 1 == 0"), step("0 == 0")); } @Test void simplifiesGuardedDivisionAndModuloIdentities() { - assertSimplificationSteps(simplification::apply, vc("x != 0", "0 / x == 0"), - chain(expect("x != 0"), expect("0 == 0", "0 / x == 0"))); - assertSimplificationSteps(simplification::apply, vc("x != 0", "x / x == 1"), - chain(expect("x != 0"), expect("1 == 1", "x / x == 1"))); - assertSimplificationSteps(simplification::apply, vc("0 != x", "x % x == 0"), - chain(expect("0 != x"), expect("0 == 0", "x % x == 0"))); + assertSimplificationSteps(simplification, vc("x != 0", "0 / x == 0"), step("x != 0", "0 == 0")); + assertSimplificationSteps(simplification, vc("x != 0", "x / x == 1"), step("x != 0", "1 == 1")); + assertSimplificationSteps(simplification, vc("0 != x", "x % x == 0"), step("0 != x", "0 == 0")); } @Test void leavesUnguardedDivisionAndModuloIdentitiesUnchanged() { - assertSimplificationSteps(simplification::apply, vc("0 / x == 0"), chain(expect("0 / x == 0"))); - assertSimplificationSteps(simplification::apply, vc("x / x == 1"), chain(expect("x / x == 1"))); - assertSimplificationSteps(simplification::apply, vc("x % x == 0"), chain(expect("x % x == 0"))); + assertSimplificationSteps(simplification, vc("0 / x == 0"), step("0 / x == 0")); + assertSimplificationSteps(simplification, vc("x / x == 1"), step("x / x == 1")); + assertSimplificationSteps(simplification, vc("x % x == 0"), step("x % x == 0")); } @Test void simplifiesOnlyFirstArithmeticIdentity() { - assertSimplificationSteps(simplification::apply, vc("x + 0 + 1 > 0"), - chain(expect("x + 1 > 0", "x + 0 + 1 > 0"))); + assertSimplificationSteps(simplification, vc("x + 0 + 1 > 0"), step("x + 1 > 0")); } @Test void recordsOriginWhenSimplifyingLaterImplication() { VCImplication implication = vc("x > 0", "y + 0 > x"); - assertSimplificationSteps(simplification::apply, implication, - chain(expect("x > 0"), expect("y > x", "y + 0 > x"))); + assertSimplificationSteps(simplification, implication, step("x > 0", "y > x")); } } 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 6dfa5a29..1028b7b3 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 @@ -14,14 +14,14 @@ class VCBinderSimplificationTest { void removesTrueBinderWhenVariableIsUnusedDownstream() { VCImplication implication = vc("∀x:int. true", "y > 0"); - assertSimplificationSteps(binderSimplification::apply, implication, chain(expect("y > 0", "∀x:int. y > 0"))); + assertSimplificationSteps(binderSimplification, implication, step("y > 0")); } @Test void keepsTrueBinderWhenVariableIsUsedDownstream() { VCImplication implication = vc("∀x:int. true", "x > 0"); - assertSimplificationSteps(binderSimplification::apply, implication, chain(expect("true"), expect("x > 0"))); + assertSimplificationSteps(binderSimplification, implication, step("true", "x > 0")); } @Test @@ -30,30 +30,28 @@ void collapsesFalseBinderSuffixToPlainTrue() { VCImplication result = binderSimplification.apply(implication); assertFalse(result.hasBinder()); - assertSimplifiedVC(result, expect("true", "∀x:int. false")); + assertSimplifiedVC(result, "true"); } @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"))); + assertSimplificationSteps(binderSimplification, implication, step("true", "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"), expect("x > 0"), expect("z > 0", "∀y:int. z > 0"))); + assertSimplificationSteps(binderSimplification, implication, step("true", "x > 0", "z > 0")); } @Test void ignoresNonBinderBooleanLiterals() { VCImplication implication = vc("true", "false"); - assertSimplificationSteps(binderSimplification::apply, implication, chain(expect("true"), expect("false"))); + assertSimplificationSteps(binderSimplification, implication, step("true", "false")); } @Test @@ -62,6 +60,6 @@ void trueBinderWithoutSuffixBecomesPlainTrue() { VCImplication result = binderSimplification.apply(implication); assertFalse(result.hasBinder()); - assertSimplifiedVC(result, expect("true", "∀x:int. true")); + assertSimplifiedVC(result, "true"); } } diff --git a/liquidjava-verifier/src/test/java/liquidjava/rj_language/opt/VCFoldingTest.java b/liquidjava-verifier/src/test/java/liquidjava/rj_language/opt/VCFoldingTest.java index 140946c3..c6255752 100644 --- a/liquidjava-verifier/src/test/java/liquidjava/rj_language/opt/VCFoldingTest.java +++ b/liquidjava-verifier/src/test/java/liquidjava/rj_language/opt/VCFoldingTest.java @@ -17,9 +17,8 @@ class VCFoldingTest { void foldsIntegerArithmeticAndComparisons() { VCImplication implication = vc("1 + 2 == 3"); - assertSimplificationSteps(folding::apply, implication, chain(expect("3 == 3", "1 + 2 == 3")), - chain(expect("true", "3 == 3"))); - assertSimplificationSteps(folding::apply, vc("4 > 7"), chain(expect("false", "4 > 7"))); + assertSimplificationSteps(folding, implication, step("3 == 3"), step("true")); + assertSimplificationSteps(folding, vc("4 > 7"), step("false")); } @Test @@ -27,31 +26,28 @@ void foldsRealAndMixedNumericExpressions() { VCImplication realArithmetic = vc("1.5 + 2.0 == 3.5"); VCImplication mixedArithmetic = vc("2 + 0.5 > 2"); - assertSimplificationSteps(folding::apply, realArithmetic, chain(expect("3.5 == 3.5", "1.5 + 2.0 == 3.5")), - chain(expect("true", "3.5 == 3.5"))); - assertSimplificationSteps(folding::apply, mixedArithmetic, chain(expect("2.5 > 2", "2 + 0.5 > 2")), - chain(expect("true", "2.5 > 2"))); + assertSimplificationSteps(folding, realArithmetic, step("3.5 == 3.5"), step("true")); + assertSimplificationSteps(folding, mixedArithmetic, step("2.5 > 2"), step("true")); } @Test void leavesDivisionAndModuloByZeroUnchanged() { - assertSimplificationSteps(folding::apply, vc("4 / 0 == 0"), chain(expect("4 / 0 == 0"))); - assertSimplificationSteps(folding::apply, vc("4 % 0 == 0"), chain(expect("4 % 0 == 0"))); + assertSimplificationSteps(folding, vc("4 / 0 == 0"), step("4 / 0 == 0")); + assertSimplificationSteps(folding, vc("4 % 0 == 0"), step("4 % 0 == 0")); } @Test void leavesRealDivisionAndModuloByZeroUnchanged() { - assertSimplificationSteps(folding::apply, vc("4.0 / 0.0 == 0.0"), chain(expect("4.0 / 0.0 == 0.0"))); - assertSimplificationSteps(folding::apply, vc("4.0 % 0.0 == 0.0"), chain(expect("4.0 % 0.0 == 0.0"))); + assertSimplificationSteps(folding, vc("4.0 / 0.0 == 0.0"), step("4.0 / 0.0 == 0.0")); + assertSimplificationSteps(folding, vc("4.0 % 0.0 == 0.0"), step("4.0 % 0.0 == 0.0")); } @Test void foldsIntegerDivisionTowardZeroForNegativeResults() { VCImplication implication = vc("(2 - 7) / 2 == -2"); - assertSimplificationSteps(folding::apply, implication, chain(expect("(2 - 7) / 2 == -2", "(2 - 7) / 2 == -2")), - chain(expect("-5 / 2 == -2", "(2 - 7) / 2 == -2")), chain(expect("-2 == -2", "-5 / 2 == -2")), - chain(expect("-2 == -2", "-2 == -2")), chain(expect("true", "-2 == -2"))); + assertSimplificationSteps(folding, implication, step("(2 - 7) / 2 == -2"), step("-5 / 2 == -2"), + step("-2 == -2"), step("-2 == -2"), step("true")); } @Test @@ -59,74 +55,67 @@ void foldsIntegerModuloWithJavaSignedRemainder() { VCImplication negativeDividend = vc("-5 % 2 < 0"); VCImplication negativeDivisor = vc("5 % -2 > 0"); - assertSimplificationSteps(folding::apply, negativeDividend, chain(expect("-5 % 2 < 0", "-5 % 2 < 0")), - chain(expect("-1 < 0", "-5 % 2 < 0")), chain(expect("true", "-1 < 0"))); - assertSimplificationSteps(folding::apply, negativeDivisor, chain(expect("5 % -2 > 0", "5 % -2 > 0")), - chain(expect("1 > 0", "5 % -2 > 0")), chain(expect("true", "1 > 0"))); + assertSimplificationSteps(folding, negativeDividend, step("-5 % 2 < 0"), step("-1 < 0"), step("true")); + assertSimplificationSteps(folding, negativeDivisor, step("5 % -2 > 0"), step("1 > 0"), step("true")); } @Test void foldsBooleanBinaryExpressions() { - assertSimplificationSteps(folding::apply, vc("true && false"), chain(expect("false", "true && false"))); - assertSimplificationSteps(folding::apply, vc("false --> true"), chain(expect("true", "false --> true"))); - assertSimplificationSteps(folding::apply, vc("true != false"), chain(expect("true", "true != false"))); + assertSimplificationSteps(folding, vc("true && false"), step("false")); + assertSimplificationSteps(folding, vc("false --> true"), step("true")); + assertSimplificationSteps(folding, vc("true != false"), step("true")); } @Test void foldsBooleanSubexpressionsInsideLargerExpression() { - assertSimplificationSteps(folding::apply, vc("true && false || ok"), - chain(expect("false || ok", "true && false || ok"))); + assertSimplificationSteps(folding, vc("true && false || ok"), step("false || ok")); } @Test void foldsNestedConstantsInsideLargerExpression() { - assertSimplificationSteps(folding::apply, vc("x > 1 + 2"), chain(expect("x > 3", "x > 1 + 2"))); - assertSimplificationSteps(folding::apply, vc("x + 1 + 2 > 4"), chain(expect("x + 3 > 4", "x + 1 + 2 > 4"))); + assertSimplificationSteps(folding, vc("x > 1 + 2"), step("x > 3")); + assertSimplificationSteps(folding, vc("x + 1 + 2 > 4"), step("x + 3 > 4")); } @Test void foldsPartialComparisonsWithoutDroppingSymbolicTerms() { - assertSimplificationSteps(folding::apply, vc("1 + 2 < x + 4"), chain(expect("3 < x + 4", "1 + 2 < x + 4"))); + assertSimplificationSteps(folding, vc("1 + 2 < x + 4"), step("3 < x + 4")); } @Test void foldsUnaryExpressions() { - assertSimplificationSteps(folding::apply, vc("!true"), chain(expect("false", "!true"))); + assertSimplificationSteps(folding, vc("!true"), step("false")); VCImplication implication = vc("-3 < 0"); - assertSimplificationSteps(folding::apply, implication, chain(expect("-3 < 0", "-3 < 0")), - chain(expect("true", "-3 < 0"))); + assertSimplificationSteps(folding, implication, step("-3 < 0"), step("true")); } @Test void foldsIteExpressions() { - assertSimplificationSteps(folding::apply, vc("true ? a : b"), chain(expect("a", "true ? a : b"))); - assertSimplificationSteps(folding::apply, vc("false ? a : b"), chain(expect("b", "false ? a : b"))); - assertSimplificationSteps(folding::apply, vc("cond ? b : b"), chain(expect("b", "cond ? b : b"))); + assertSimplificationSteps(folding, vc("true ? a : b"), step("a")); + assertSimplificationSteps(folding, vc("false ? a : b"), step("b")); + assertSimplificationSteps(folding, vc("cond ? b : b"), step("b")); } @Test void foldsIteBranchesBeforeComparingThem() { VCImplication implication = vc("cond ? 1 + 2 : 3"); - assertSimplificationSteps(folding::apply, implication, chain(expect("cond ? 3 : 3", "cond ? 1 + 2 : 3")), - chain(expect("3", "cond ? 3 : 3"))); + assertSimplificationSteps(folding, implication, step("cond ? 3 : 3"), step("3")); } @Test void foldsAdjacentIntegerConstants() { - assertSimplificationSteps(folding::apply, vc("x + 1 - 2"), chain(expect("x - 1", "x + 1 - 2"))); - assertSimplificationSteps(folding::apply, vc("x - 1 + 2"), chain(expect("x + 1", "x - 1 + 2"))); - assertSimplificationSteps(folding::apply, vc("x + 1 + 2"), chain(expect("x + 3", "x + 1 + 2"))); - assertSimplificationSteps(folding::apply, vc("x + 1 - 1"), chain(expect("x", "x + 1 - 1"))); + assertSimplificationSteps(folding, vc("x + 1 - 2"), step("x - 1")); + assertSimplificationSteps(folding, vc("x - 1 + 2"), step("x + 1")); + assertSimplificationSteps(folding, vc("x + 1 + 2"), step("x + 3")); + assertSimplificationSteps(folding, vc("x + 1 - 1"), step("x")); } @Test void foldsEnumEqualityAndInequality() { - assertSimplificationSteps(folding::apply, vc("Mode.Photo == Mode.Photo"), - chain(expect("true", "Mode.Photo == Mode.Photo"))); - assertSimplificationSteps(folding::apply, vc("Mode.Photo != Mode.Video"), - chain(expect("true", "Mode.Photo != Mode.Video"))); + assertSimplificationSteps(folding, vc("Mode.Photo == Mode.Photo"), step("true")); + assertSimplificationSteps(folding, vc("Mode.Photo != Mode.Video"), step("true")); } @Test @@ -136,8 +125,7 @@ void foldsResolvedEnumLiterals() { VCImplication implication = new VCImplication( new Predicate(new BinaryExpression(limit, "==", new LiteralInt(3)))); - assertSimplificationSteps(folding::apply, implication, chain(expect("3 == 3", "Config.LIMIT == 3")), - chain(expect("true", "3 == 3"))); + assertSimplificationSteps(folding, implication, step("3 == 3"), step("true")); } @Test @@ -148,27 +136,25 @@ void foldsResolvedEnumLiteralsInsideLargerExpression() { VCImplication implication = new VCImplication( new Predicate(new BinaryExpression(arithmetic, "==", new LiteralInt(5)))); - assertSimplificationSteps(folding::apply, implication, chain(expect("3 + 2 == 5", "Config.LIMIT + 2 == 5")), - chain(expect("5 == 5", "3 + 2 == 5")), chain(expect("true", "5 == 5"))); + assertSimplificationSteps(folding, implication, step("3 + 2 == 5"), step("5 == 5"), step("true")); } @Test void recordsOriginWhenOnlyGroupIsUnwrapped() { VCImplication implication = vc("(x > 0)"); - VCImplication result = assertSimplificationSteps(folding::apply, implication, chain(expect("x > 0", "x > 0"))); + VCSimplificationResult result = assertSimplificationSteps(folding, implication, step("x > 0")); - assertEquals("x > 0", result.getRefinement().toString()); + assertEquals("x > 0", result.getImplication().getRefinement().toString()); } @Test void recordsOriginWhenFoldingLaterImplication() { VCImplication implication = vc("x > 0", "1 + 2 > 0"); - VCImplication result = assertSimplificationSteps(folding::apply, implication, - chain(expect("x > 0"), expect("3 > 0", "1 + 2 > 0"))); + VCSimplificationResult result = assertSimplificationSteps(folding, implication, step("x > 0", "3 > 0")); - result = assertSimplificationSteps(folding::apply, result, chain(expect("x > 0"), expect("true", "3 > 0"))); - assertEquals("true", result.getNext().getRefinement().getExpression().toDisplayString()); + result = assertSimplificationSteps(folding, result.getImplication(), step("x > 0", "true")); + assertEquals("true", result.getImplication().getNext().getRefinement().getExpression().toDisplayString()); } } diff --git a/liquidjava-verifier/src/test/java/liquidjava/rj_language/opt/VCLogicalSimplificationTest.java b/liquidjava-verifier/src/test/java/liquidjava/rj_language/opt/VCLogicalSimplificationTest.java index 5d3e3ccd..99ad7cc1 100644 --- a/liquidjava-verifier/src/test/java/liquidjava/rj_language/opt/VCLogicalSimplificationTest.java +++ b/liquidjava-verifier/src/test/java/liquidjava/rj_language/opt/VCLogicalSimplificationTest.java @@ -10,68 +10,64 @@ class VCLogicalSimplificationTest { @Test void simplifiesConjunctionWithBooleanLiterals() { - assertSimplificationSteps(simplification::apply, vc("x && true"), chain(expect("x", "x && true"))); - assertSimplificationSteps(simplification::apply, vc("true && x"), chain(expect("x", "true && x"))); - assertSimplificationSteps(simplification::apply, vc("x && false"), chain(expect("false", "x && false"))); - assertSimplificationSteps(simplification::apply, vc("false && x"), chain(expect("false", "false && x"))); + assertSimplificationSteps(simplification, vc("x && true"), step("x")); + assertSimplificationSteps(simplification, vc("true && x"), step("x")); + assertSimplificationSteps(simplification, vc("x && false"), step("false")); + assertSimplificationSteps(simplification, vc("false && x"), step("false")); } @Test void simplifiesDisjunctionWithBooleanLiterals() { - assertSimplificationSteps(simplification::apply, vc("x || true"), chain(expect("true", "x || true"))); - assertSimplificationSteps(simplification::apply, vc("true || x"), chain(expect("true", "true || x"))); - assertSimplificationSteps(simplification::apply, vc("x || false"), chain(expect("x", "x || false"))); - assertSimplificationSteps(simplification::apply, vc("false || x"), chain(expect("x", "false || x"))); + assertSimplificationSteps(simplification, vc("x || true"), step("true")); + assertSimplificationSteps(simplification, vc("true || x"), step("true")); + assertSimplificationSteps(simplification, vc("x || false"), step("x")); + assertSimplificationSteps(simplification, vc("false || x"), step("x")); } @Test void simplifiesDoubleNegation() { - assertSimplificationSteps(simplification::apply, vc("!!x"), chain(expect("x", "!!x"))); + assertSimplificationSteps(simplification, vc("!!x"), step("x")); } @Test void simplifiesDuplicateLogicalOperands() { - assertSimplificationSteps(simplification::apply, vc("p && p"), chain(expect("p", "p && p"))); - assertSimplificationSteps(simplification::apply, vc("p || p"), chain(expect("p", "p || p"))); + assertSimplificationSteps(simplification, vc("p && p"), step("p")); + assertSimplificationSteps(simplification, vc("p || p"), step("p")); } @Test void simplifiesSelfEqualityAndInequality() { - assertSimplificationSteps(simplification::apply, vc("x == x"), chain(expect("true", "x == x"))); - assertSimplificationSteps(simplification::apply, vc("x != x"), chain(expect("false", "x != x"))); + assertSimplificationSteps(simplification, vc("x == x"), step("true")); + assertSimplificationSteps(simplification, vc("x != x"), step("false")); } @Test void simplifiesImplicationIdentities() { - assertSimplificationSteps(simplification::apply, vc("x --> true"), chain(expect("true", "x --> true"))); - assertSimplificationSteps(simplification::apply, vc("false --> x"), chain(expect("true", "false --> x"))); - assertSimplificationSteps(simplification::apply, vc("true --> x"), chain(expect("x", "true --> x"))); - assertSimplificationSteps(simplification::apply, vc("x --> x"), chain(expect("true", "x --> x"))); + assertSimplificationSteps(simplification, vc("x --> true"), step("true")); + assertSimplificationSteps(simplification, vc("false --> x"), step("true")); + assertSimplificationSteps(simplification, vc("true --> x"), step("x")); + assertSimplificationSteps(simplification, vc("x --> x"), step("true")); } @Test void simplifiesOnlyFirstLogicalIdentity() { - assertSimplificationSteps(simplification::apply, vc("x && true && false"), - chain(expect("x && false", "x && true && false"))); + assertSimplificationSteps(simplification, vc("x && true && false"), step("x && false")); } @Test void simplifiesNestedExpressionsBeforeParent() { - assertSimplificationSteps(simplification::apply, vc("(x && true) || false"), - chain(expect("x || false", "x && true || false"))); + assertSimplificationSteps(simplification, vc("(x && true) || false"), step("x || false")); } @Test void simplifiesIteChildren() { - assertSimplificationSteps(simplification::apply, vc("cond ? x && true : y || false"), - chain(expect("cond ? x : y || false", "cond ? x && true : y || false"))); + assertSimplificationSteps(simplification, vc("cond ? x && true : y || false"), step("cond ? x : y || false")); } @Test void recordsOriginWhenSimplifyingLaterImplication() { VCImplication implication = vc("x > 0", "y || false"); - assertSimplificationSteps(simplification::apply, implication, - chain(expect("x > 0"), expect("y", "y || false"))); + assertSimplificationSteps(simplification, implication, step("x > 0", "y")); } } 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 4ed71a94..49186622 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 @@ -29,18 +29,19 @@ public class VCSimplificationPropertyBasedTest { @Property(trials = TRIALS) public void eachSimplificationStepPreservesVcSemantics(@From(VCImplicationGenerator.class) VCImplication vc) { setUpContext(); - VCImplication current = vc; + VCSimplificationResult current = new VCSimplificationResult(vc); for (int step = 0; step < MAX_STEPS; step++) { VCSimplificationResult result = VCSimplification.simplifyOnce(current); VCImplication simplified = result.getImplication(); - if (current.equals(simplified)) + if (result == current) return; - assertTrue(current.equals(result.getOrigin().getImplication())); - assertEquivalent(current, simplified, step); - current = simplified; + assertTrue(current.getImplication().equals(result.getOrigin().getImplication())); + assertEquivalent(current.getImplication(), simplified, step); + current = result; } - fail("VC simplification did not reach a fixed point within " + MAX_STEPS + " steps: " + current); + fail("VC simplification did not reach a fixed point within " + MAX_STEPS + " steps: " + + current.getImplication()); } private static void setUpContext() { 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 79cbde0f..8e3115bd 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 @@ -24,98 +24,84 @@ void simplifyOnceReturnsNullForNullImplication() { void simplifyOnceAppliesSubstitutionBeforeFolding() { VCImplication implication = vc("∀x:int. x == 1 + 2", "x > 2"); - assertSimplificationResults(VCSimplification::simplifyOnce, implication, - chain(expect("1 + 2 > 2", "∀x:int. x > 2")), chain(expect("3 > 2", "1 + 2 > 2")), - chain(expect("true", "3 > 2"))); + assertSimplificationSteps(implication, step("1 + 2 > 2"), step("3 > 2"), step("true")); } @Test void simplifyOnceDoesNotFoldAfterSubstitutionInSameStep() { VCImplication implication = vc("∀x:int. x == 1 + 2", "x == 3"); - assertSimplificationResults(VCSimplification::simplifyOnce, implication, - chain(expect("1 + 2 == 3", "∀x:int. x == 3")), chain(expect("3 == 3", "1 + 2 == 3")), - chain(expect("true", "3 == 3"))); + assertSimplificationSteps(implication, step("1 + 2 == 3"), step("3 == 3"), step("true")); } @Test void simplifyOnceAppliesSubstitutionBeforeBinderSimplification() { VCImplication implication = vc("∀x:int. x == 3", "∀y:int. true", "x > 0"); - assertSimplificationResults(VCSimplification::simplifyOnce, implication, - chain(expect("true"), expect("3 > 0", "∀x:int. x > 0")), chain(expect("3 > 0", "∀y:int. x > 0")), - chain(expect("true", "3 > 0"))); + assertSimplificationSteps(implication, step("true", "3 > 0"), step("3 > 0"), step("true")); } @Test void simplifyOnceAppliesBinderSimplificationBeforeFolding() { VCImplication implication = vc("∀x:int. true", "1 + 2 > 0"); - assertSimplificationResults(VCSimplification::simplifyOnce, implication, - chain(expect("1 + 2 > 0", "∀x:int. 1 + 2 > 0")), chain(expect("3 > 0", "1 + 2 > 0"))); + assertSimplificationSteps(implication, step("1 + 2 > 0"), step("3 > 0")); } @Test void simplifyOnceAppliesBinderSimplificationBeforeLogicalSimplification() { VCImplication implication = vc("∀x:int. true", "y && true"); - assertSimplificationResults(VCSimplification::simplifyOnce, implication, - chain(expect("y && true", "∀x:int. y && true")), chain(expect("y", "y && true"))); + assertSimplificationSteps(implication, step("y && true"), step("y")); } @Test void simplifyOnceAppliesFoldingWhenNoSubstitutionIsAvailable() { VCImplication implication = vc("1 + 2 > 2"); - assertSimplificationResults(VCSimplification::simplifyOnce, implication, chain(expect("3 > 2", "1 + 2 > 2")), - chain(expect("true", "3 > 2"))); + assertSimplificationSteps(implication, step("3 > 2"), step("true")); } @Test void simplifyOnceAppliesFoldingBeforeArithmeticSimplification() { VCImplication implication = vc("1 + 2 + x + 0 > 0"); - assertSimplificationResults(VCSimplification::simplifyOnce, implication, - chain(expect("3 + x + 0 > 0", "1 + 2 + x + 0 > 0"))); + assertSimplificationSteps(implication, step("3 + x + 0 > 0")); } @Test void simplifyOnceAppliesArithmeticWhenNoSubstitutionOrFoldingIsAvailable() { VCImplication implication = vc("x + 0 > 0"); - assertSimplificationResults(VCSimplification::simplifyOnce, implication, chain(expect("x > 0", "x + 0 > 0"))); + assertSimplificationSteps(implication, step("x > 0")); } @Test void simplifyOnceAppliesArithmeticBeforeLogicalSimplification() { VCImplication implication = vc("x + 0 == x"); - assertSimplificationResults(VCSimplification::simplifyOnce, implication, chain(expect("x == x", "x + 0 == x")), - chain(expect("true", "x == x"))); + assertSimplificationSteps(implication, step("x == x"), step("true")); } @Test void simplifyOnceAppliesLogicalWhenNoEarlierSimplificationIsAvailable() { VCImplication implication = vc("x && true"); - assertSimplificationResults(VCSimplification::simplifyOnce, implication, chain(expect("x", "x && true"))); + assertSimplificationSteps(implication, step("x")); } @Test void simplifyAppliesLogicalStepsUntilFixedPoint() { VCImplication implication = vc("x && true && true"); - assertSimplificationResults(VCSimplification::simplifyOnce, implication, - chain(expect("x && true", "x && true && true")), chain(expect("x", "x && true"))); + assertSimplificationSteps(implication, step("x && true"), step("x")); } @Test void simplifyKeepsApplyingStepsUntilFixedPoint() { VCImplication implication = vc("∀x:int. x == 1 + 2", "x + 1 > 3"); - assertSimplificationResults(VCSimplification::simplifyOnce, implication, - chain(expect("1 + 2 + 1 > 3", "∀x:int. x + 1 > 3")), chain(expect("3 + 1 > 3", "1 + 2 + 1 > 3")), - chain(expect("4 > 3", "3 + 1 > 3")), chain(expect("true", "4 > 3"))); + assertSimplificationSteps(implication, step("1 + 2 + 1 > 3"), step("3 + 1 > 3"), step("4 > 3"), step("true")); } @Test @@ -124,7 +110,7 @@ void simplifyToFixedPointRemovesTrueBindersOverMultipleSteps() { VCSimplificationResult result = VCSimplification.simplifyToFixedPoint(implication); - assertSimplifiedVC(result.getImplication(), expect("z > 0", "∀y:int. z > 0")); + assertSimplifiedVC(result.getImplication(), "z > 0"); assertNotNull(result.getOrigin()); assertNotNull(result.getOrigin().getOrigin()); } @@ -133,48 +119,41 @@ void simplifyToFixedPointRemovesTrueBindersOverMultipleSteps() { void simplifyAppliesMultipleSubstitutionsBeforeReachingFixedPoint() { VCImplication implication = vc("∀x:int. x == 3", "∀y:int. y == x + 1", "y > x"); - assertSimplificationResults(VCSimplification::simplifyOnce, implication, - chain(expect("y == 3 + 1", "∀x:int. y == x + 1"), expect("y > 3", "∀x:int. y > x")), - chain(expect("3 + 1 > 3", "∀y:int. y > 3")), chain(expect("4 > 3", "3 + 1 > 3")), - chain(expect("true", "4 > 3"))); + assertSimplificationSteps(implication, step("y == 3 + 1", "y > 3"), step("3 + 1 > 3"), step("4 > 3"), + step("true")); } @Test void simplifyAppliesLongSubstitutionChainBeforeReachingFixedPoint() { VCImplication implication = vc("∀x:int. x == 1", "∀y:int. y == x + 1", "∀z:int. z == y + 1", "z == 3"); - assertSimplificationResults(VCSimplification::simplifyOnce, implication, - chain(expect("y == 1 + 1", "∀x:int. y == x + 1"), expect("z == y + 1"), expect("z == 3")), - chain(expect("z == 1 + 1 + 1", "∀y:int. z == y + 1"), expect("z == 3")), - chain(expect("1 + 1 + 1 == 3", "∀z:int. z == 3")), chain(expect("2 + 1 == 3", "1 + 1 + 1 == 3")), - chain(expect("3 == 3", "2 + 1 == 3")), chain(expect("true", "3 == 3"))); + assertSimplificationSteps(implication, step("y == 1 + 1", "z == y + 1", "z == 3"), + step("z == 1 + 1 + 1", "z == 3"), step("1 + 1 + 1 == 3"), step("2 + 1 == 3"), step("3 == 3"), + step("true")); } @Test void simplifyCombinesSubstitutionAndNestedFoldingAcrossFixedPoint() { VCImplication implication = vc("∀x:int. x == 1", "∀y:int. y == x + 2", "y - 1 == 2"); - assertSimplificationResults(VCSimplification::simplifyOnce, implication, - chain(expect("y == 1 + 2", "∀x:int. y == x + 2"), expect("y - 1 == 2")), - chain(expect("1 + 2 - 1 == 2", "∀y:int. y - 1 == 2")), chain(expect("3 - 1 == 2", "1 + 2 - 1 == 2")), - chain(expect("2 == 2", "3 - 1 == 2")), chain(expect("true", "2 == 2"))); + assertSimplificationSteps(implication, step("y == 1 + 2", "y - 1 == 2"), step("1 + 2 - 1 == 2"), + step("3 - 1 == 2"), step("2 == 2"), step("true")); } @Test void simplifyStopsAfterSubstitutionWhenOnlyNegativeLiteralShapeChanges() { VCImplication implication = vc("∀x:int. x == a + 0", "x >= -3"); - assertSimplificationResults(VCSimplification::simplifyOnce, implication, - chain(expect("a + 0 >= -3", "∀x:int. x >= -3"))); + assertSimplificationSteps(implication, step("a + 0 >= -3")); } @Test void simplifyLeavesUnchangedVcAsPlainPredicates() { VCImplication implication = vc("x > 0", "y > x"); - VCSimplificationResult result = VCSimplification.simplifyOnce(implication); + VCSimplificationResult result = VCSimplification.simplifyOnce(new VCSimplificationResult(implication)); - assertSimplifiedVC(result.getImplication(), expect("x > 0"), expect("y > x")); + assertSimplifiedVC(result.getImplication(), "x > 0", "y > x"); assertNull(result.getOrigin()); } @@ -182,11 +161,11 @@ void simplifyLeavesUnchangedVcAsPlainPredicates() { void simplifyOnceStoresACompleteClonedOriginChain() { VCImplication implication = vc("x > 0", "y + 0 > x"); - VCSimplificationResult result = VCSimplification.simplifyOnce(implication); + VCSimplificationResult result = VCSimplification.simplifyOnce(new VCSimplificationResult(implication)); implication.getNext().setRefinement(vc("changed").getRefinement()); - assertSimplifiedVC(result.getImplication(), expect("x > 0"), expect("y > x")); - assertSimplifiedVC(result.getOrigin().getImplication(), expect("x > 0"), expect("y + 0 > x")); + assertSimplifiedVC(result.getImplication(), "x > 0", "y > x"); + assertSimplifiedVC(result.getOrigin().getImplication(), "x > 0", "y + 0 > x"); } @Test @@ -199,6 +178,6 @@ void fixedPointHistoryLinksEverySuccessfulStep() { historyLength++; assertEquals(4, historyLength); - assertSimplifiedVC(result.getImplication(), expect("true")); + assertSimplifiedVC(result.getImplication(), "true"); } } diff --git a/liquidjava-verifier/src/test/java/liquidjava/rj_language/opt/VCSubstitutionTest.java b/liquidjava-verifier/src/test/java/liquidjava/rj_language/opt/VCSubstitutionTest.java index a9b13054..2af1733a 100644 --- a/liquidjava-verifier/src/test/java/liquidjava/rj_language/opt/VCSubstitutionTest.java +++ b/liquidjava-verifier/src/test/java/liquidjava/rj_language/opt/VCSubstitutionTest.java @@ -12,109 +12,104 @@ class VCSubstitutionTest { void substitutesBinderEqualityIntoWholeChain() { VCImplication implication = vc("∀x:int. x == 3", "x > 0"); - assertSimplificationSteps(substitution::apply, implication, chain(expect("3 > 0", "∀x:int. x > 0"))); + assertSimplificationSteps(substitution, implication, step("3 > 0")); } @Test void substitutesReverseBinderEquality() { VCImplication implication = vc("∀x:int. 3 == x", "x > 0"); - assertSimplificationSteps(substitution::apply, implication, chain(expect("3 > 0", "∀x:int. x > 0"))); + assertSimplificationSteps(substitution, implication, step("3 > 0")); } @Test void substitutesCompoundKnownValue() { VCImplication implication = vc("∀x:int. x == y + 1", "x > y"); - assertSimplificationSteps(substitution::apply, implication, chain(expect("y + 1 > y", "∀x:int. x > y"))); + assertSimplificationSteps(substitution, implication, step("y + 1 > y")); } @Test void substitutesOnlyWholeVariableReferences() { VCImplication implication = vc("∀x:int. x == 3", "xx > x"); - assertSimplificationSteps(substitution::apply, implication, chain(expect("xx > 3", "∀x:int. xx > x"))); + assertSimplificationSteps(substitution, implication, step("xx > 3")); } @Test void substitutesEveryOccurrenceInPredicate() { VCImplication implication = vc("∀x:int. x == 2", "x + x > 0"); - assertSimplificationSteps(substitution::apply, implication, chain(expect("2 + 2 > 0", "∀x:int. x + x > 0"))); + assertSimplificationSteps(substitution, implication, step("2 + 2 > 0")); } @Test void preservesRemainingBinderAfterSubstitution() { VCImplication implication = vc("∀x:int. x == 3", "∀y:int. y > x", "y > 0"); - assertSimplificationSteps(substitution::apply, implication, - chain(expect("y > 3", "∀x:int. y > x"), expect("y > 0"))); + assertSimplificationSteps(substitution, implication, step("y > 3", "y > 0")); } @Test void keepsSourceNodeWhenItIsLastInChain() { VCImplication implication = vc("x > 0", "∀y:int. y == 1"); - assertSimplificationSteps(substitution::apply, implication, chain(expect("x > 0"), expect("y == 1"))); + assertSimplificationSteps(substitution, implication, step("x > 0", "y == 1")); } @Test void keepsReturnBinderWhenConclusionIsSeparate() { VCImplication implication = vc("∀x:int. true", "∀#ret_8:int. #ret_8 == x + 1"); - assertSimplificationSteps(substitution::apply, implication, chain(expect("true"), expect("#ret⁸ == x + 1"))); + assertSimplificationSteps(substitution, implication, step("true", "#ret⁸ == x + 1")); } @Test void usesFirstSubstitutionFoundInChain() { VCImplication implication = vc("∀x:int. x > 0", "∀y:int. y == 4", "x + y > 0"); - assertSimplificationSteps(substitution::apply, implication, - chain(expect("x > 0"), expect("x + 4 > 0", "∀y:int. x + y > 0"))); + assertSimplificationSteps(substitution, implication, step("x > 0", "x + 4 > 0")); } @Test void substitutesInnerKnownValueAcrossNestedImplications() { VCImplication implication = vc("∀x:int. true", "∀y:int. y == 1", "∀z:int. z > y", "y + z > 0"); - assertSimplificationSteps(substitution::apply, implication, - chain(expect("true"), expect("z > 1", "∀y:int. z > y"), expect("1 + z > 0", "∀y:int. y + z > 0"))); + assertSimplificationSteps(substitution, implication, step("true", "z > 1", "1 + z > 0")); } @Test void substitutesOuterKnownValueIntoNestedBinderRefinements() { VCImplication implication = vc("∀x:int. x == 3", "∀y:int. y == x + 1", "y > x"); - assertSimplificationSteps(substitution::apply, implication, - chain(expect("y == 3 + 1", "∀x:int. y == x + 1"), expect("y > 3", "∀x:int. y > x")), - chain(expect("3 + 1 > 3", "∀y:int. y > 3"))); + assertSimplificationSteps(substitution, implication, step("y == 3 + 1", "y > 3"), step("3 + 1 > 3")); } @Test void ignoresRecursiveBinderEquality() { VCImplication implication = vc("∀x:int. x == x + 1", "x > 0"); - assertSimplificationSteps(substitution::apply, implication, chain(expect("x == x + 1"), expect("x > 0"))); + assertSimplificationSteps(substitution, implication, step("x == x + 1", "x > 0")); } @Test void ignoresNonEqualityBinderRefinement() { VCImplication implication = vc("∀x:int. x > 3", "x > 0"); - assertSimplificationSteps(substitution::apply, implication, chain(expect("x > 3"), expect("x > 0"))); + assertSimplificationSteps(substitution, implication, step("x > 3", "x > 0")); } @Test void ignoresDerivedBinderEquality() { VCImplication implication = vc("∀x:int. x + 1 == 3", "x > 0"); - assertSimplificationSteps(substitution::apply, implication, chain(expect("x + 1 == 3"), expect("x > 0"))); + assertSimplificationSteps(substitution, implication, step("x + 1 == 3", "x > 0")); } @Test void ignoresEqualityWithoutBinder() { VCImplication implication = vc("x == 3", "x > 0"); - assertSimplificationSteps(substitution::apply, implication, chain(expect("x == 3"), expect("x > 0"))); + assertSimplificationSteps(substitution, implication, step("x == 3", "x > 0")); } } diff --git a/liquidjava-verifier/src/test/java/liquidjava/utils/VCTestUtils.java b/liquidjava-verifier/src/test/java/liquidjava/utils/VCTestUtils.java index 3556cf5e..96b23754 100644 --- a/liquidjava-verifier/src/test/java/liquidjava/utils/VCTestUtils.java +++ b/liquidjava-verifier/src/test/java/liquidjava/utils/VCTestUtils.java @@ -1,13 +1,13 @@ package liquidjava.utils; import static org.junit.jupiter.api.Assertions.assertEquals; +import static org.junit.jupiter.api.Assertions.assertNotNull; import static org.junit.jupiter.api.Assertions.assertNull; -import java.util.function.Function; -import java.util.function.UnaryOperator; - import liquidjava.processor.VCImplication; import liquidjava.rj_language.Predicate; +import liquidjava.rj_language.opt.VCSimplification; +import liquidjava.rj_language.opt.VCSimplificationPass; import liquidjava.rj_language.opt.VCSimplificationResult; import liquidjava.rj_language.parsing.RefinementsParser; import spoon.Launcher; @@ -49,66 +49,60 @@ private static CtTypeReference type(String name) { throw new IllegalArgumentException("Unsupported test type: " + name); } - public static void assertSimplifiedVC(VCImplication implication, ExpectedSimplifiedVCImplication... expected) { + public static void assertSimplifiedVC(VCImplication implication, String... expected) { VCImplication current = implication; for (int i = 0; i < expected.length; i++) { - ExpectedSimplifiedVCImplication expectedPredicate = expected[i]; assertEquals(Predicate.class, current.getRefinement().getClass(), "Expected simplified refinement at implication " + i + " to be a plain Predicate"); - assertEquals(expectedPredicate.simplified(), formatRefinement(current), - "Unexpected simplified expression at implication " + i + sourceContext(expectedPredicate)); + assertEquals(expected[i], formatRefinement(current), + "Unexpected simplified expression at implication " + i); current = current.getNext(); } assertNull(current, "Expected VC chain to end after " + expected.length + " implications"); } - public static VCImplication assertSimplificationSteps(UnaryOperator simplifier, - VCImplication implication, ExpectedSimplificationStep... expectedSteps) { - VCImplication current = implication; + public static VCSimplificationResult assertSimplificationSteps(VCImplication implication, + ExpectedSimplificationStep... expectedSteps) { + VCSimplificationResult current = new VCSimplificationResult(implication); for (ExpectedSimplificationStep expectedStep : expectedSteps) { - current = simplifier.apply(current); - assertSimplifiedVC(current, expectedStep.implications()); + VCSimplificationResult result = VCSimplification.simplifyOnce(current); + assertSimplificationResult(current, result, expectedStep); + current = result; } return current; } - public static VCSimplificationResult assertSimplificationResults( - Function simplifier, VCImplication implication, - ExpectedSimplificationStep... expectedSteps) { + public static VCSimplificationResult assertSimplificationSteps(VCSimplificationPass simplifier, + VCImplication implication, ExpectedSimplificationStep... expectedSteps) { VCSimplificationResult current = new VCSimplificationResult(implication); for (ExpectedSimplificationStep expectedStep : expectedSteps) { - VCSimplificationResult result = simplifier.apply(current.getImplication()); - assertEquals(current.getImplication(), result.getOrigin().getImplication(), - "Unexpected whole-chain simplification origin"); - assertSimplifiedVC(result.getImplication(), expectedStep.implications()); + VCSimplificationResult result = VCSimplification.simplifyOnce(current, simplifier); + assertSimplificationResult(current, result, expectedStep); current = result; } return current; } - public static ExpectedSimplificationStep chain(ExpectedSimplifiedVCImplication... implications) { - return new ExpectedSimplificationStep(implications); - } - - public static ExpectedSimplifiedVCImplication expect(String simplified, String source) { - return new ExpectedSimplifiedVCImplication(simplified, source); + private static void assertSimplificationResult(VCSimplificationResult previous, VCSimplificationResult result, + ExpectedSimplificationStep expectedStep) { + if (previous.getImplication().equals(result.getImplication())) { + assertNull(result.getOrigin(), "Unchanged simplification result should not have an origin"); + } else { + assertNotNull(result.getOrigin(), "Changed simplification result should have an origin"); + assertEquals(previous.getImplication(), result.getOrigin().getImplication(), + "Simplification origin should be the complete previous VC"); + } + assertSimplifiedVC(result.getImplication(), expectedStep.implications()); } - public static ExpectedSimplifiedVCImplication expect(String simplified) { - return new ExpectedSimplifiedVCImplication(simplified, null); + public static ExpectedSimplificationStep step(String... implications) { + return new ExpectedSimplificationStep(implications); } private static String formatRefinement(VCImplication implication) { return implication.getRefinement().getExpression().toDisplayString(); } - private static String sourceContext(ExpectedSimplifiedVCImplication expected) { - return expected.source() == null ? "" : " (rewrite source: " + expected.source() + ")"; - } - - public record ExpectedSimplifiedVCImplication(String simplified, String source) { - } - - public record ExpectedSimplificationStep(ExpectedSimplifiedVCImplication... implications) { + public record ExpectedSimplificationStep(String... implications) { } } From 96f984263b5242dad350b37db8aa663e0cebde00 Mon Sep 17 00:00:00 2001 From: Ricardo Costa Date: Thu, 18 Jun 2026 16:11:27 +0100 Subject: [PATCH 3/5] Refactor Tests --- .../opt/VCArithmeticSimplificationTest.java | 5 +- .../opt/VCBinderSimplificationTest.java | 37 ++---- .../rj_language/opt/VCFoldingTest.java | 60 +++------ .../opt/VCLogicalSimplificationTest.java | 5 +- .../rj_language/opt/VCSimplificationTest.java | 119 ++++-------------- .../rj_language/opt/VCSubstitutionTest.java | 65 +++------- .../java/liquidjava/utils/VCTestUtils.java | 64 +++++----- 7 files changed, 106 insertions(+), 249 deletions(-) diff --git a/liquidjava-verifier/src/test/java/liquidjava/rj_language/opt/VCArithmeticSimplificationTest.java b/liquidjava-verifier/src/test/java/liquidjava/rj_language/opt/VCArithmeticSimplificationTest.java index e0496dc3..6551459b 100644 --- a/liquidjava-verifier/src/test/java/liquidjava/rj_language/opt/VCArithmeticSimplificationTest.java +++ b/liquidjava-verifier/src/test/java/liquidjava/rj_language/opt/VCArithmeticSimplificationTest.java @@ -1,7 +1,6 @@ package liquidjava.rj_language.opt; import static liquidjava.utils.VCTestUtils.*; -import liquidjava.processor.VCImplication; import org.junit.jupiter.api.Test; class VCArithmeticSimplificationTest { @@ -57,8 +56,6 @@ void simplifiesOnlyFirstArithmeticIdentity() { @Test void recordsOriginWhenSimplifyingLaterImplication() { - VCImplication implication = vc("x > 0", "y + 0 > x"); - - assertSimplificationSteps(simplification, implication, step("x > 0", "y > x")); + assertSimplificationSteps(simplification, vc("x > 0", "y + 0 > x"), step("x > 0", "y > x")); } } 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 1028b7b3..581688dd 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 @@ -1,9 +1,6 @@ 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 { @@ -12,54 +9,38 @@ class VCBinderSimplificationTest { @Test void removesTrueBinderWhenVariableIsUnusedDownstream() { - VCImplication implication = vc("∀x:int. true", "y > 0"); - - assertSimplificationSteps(binderSimplification, implication, step("y > 0")); + assertSimplificationSteps(binderSimplification, vc("∀x:int. true", "y > 0"), step("y > 0")); } @Test void keepsTrueBinderWhenVariableIsUsedDownstream() { - VCImplication implication = vc("∀x:int. true", "x > 0"); - - assertSimplificationSteps(binderSimplification, implication, step("true", "x > 0")); + assertSimplificationSteps(binderSimplification, vc("∀x:int. true", "x > 0"), step("true", "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, "true"); + assertSimplificationSteps(binderSimplification, vc("∀x:int. false", "y > 0"), step("true")); } @Test void simplifiesOnlyFirstApplicableBinder() { - VCImplication implication = vc("∀x:int. true", "∀y:int. true", "z > 0"); - - assertSimplificationSteps(binderSimplification, implication, step("true", "z > 0")); + assertSimplificationSteps(binderSimplification, vc("∀x:int. true", "∀y:int. true", "z > 0"), + step("true", "z > 0")); } @Test void skipsInapplicableTrueBinderAndSimplifiesLaterBinder() { - VCImplication implication = vc("∀x:int. true", "x > 0", "∀y:int. true", "z > 0"); - - assertSimplificationSteps(binderSimplification, implication, step("true", "x > 0", "z > 0")); + assertSimplificationSteps(binderSimplification, vc("∀x:int. true", "x > 0", "∀y:int. true", "z > 0"), + step("true", "x > 0", "z > 0")); } @Test void ignoresNonBinderBooleanLiterals() { - VCImplication implication = vc("true", "false"); - - assertSimplificationSteps(binderSimplification, implication, step("true", "false")); + assertSimplificationSteps(binderSimplification, vc("true", "false"), step("true", "false")); } @Test void trueBinderWithoutSuffixBecomesPlainTrue() { - VCImplication implication = vc("∀x:int. true"); - VCImplication result = binderSimplification.apply(implication); - - assertFalse(result.hasBinder()); - assertSimplifiedVC(result, "true"); + assertSimplificationSteps(binderSimplification, vc("∀x:int. true"), step("true")); } } diff --git a/liquidjava-verifier/src/test/java/liquidjava/rj_language/opt/VCFoldingTest.java b/liquidjava-verifier/src/test/java/liquidjava/rj_language/opt/VCFoldingTest.java index c6255752..15cc99bc 100644 --- a/liquidjava-verifier/src/test/java/liquidjava/rj_language/opt/VCFoldingTest.java +++ b/liquidjava-verifier/src/test/java/liquidjava/rj_language/opt/VCFoldingTest.java @@ -1,7 +1,6 @@ package liquidjava.rj_language.opt; import static liquidjava.utils.VCTestUtils.*; -import static org.junit.jupiter.api.Assertions.assertEquals; import liquidjava.processor.VCImplication; import liquidjava.rj_language.Predicate; import liquidjava.rj_language.ast.BinaryExpression; @@ -15,19 +14,14 @@ class VCFoldingTest { @Test void foldsIntegerArithmeticAndComparisons() { - VCImplication implication = vc("1 + 2 == 3"); - - assertSimplificationSteps(folding, implication, step("3 == 3"), step("true")); + assertSimplificationSteps(folding, vc("1 + 2 == 3"), step("3 == 3"), step("true")); assertSimplificationSteps(folding, vc("4 > 7"), step("false")); } @Test void foldsRealAndMixedNumericExpressions() { - VCImplication realArithmetic = vc("1.5 + 2.0 == 3.5"); - VCImplication mixedArithmetic = vc("2 + 0.5 > 2"); - - assertSimplificationSteps(folding, realArithmetic, step("3.5 == 3.5"), step("true")); - assertSimplificationSteps(folding, mixedArithmetic, step("2.5 > 2"), step("true")); + assertSimplificationSteps(folding, vc("1.5 + 2.0 == 3.5"), step("3.5 == 3.5"), step("true")); + assertSimplificationSteps(folding, vc("2 + 0.5 > 2"), step("2.5 > 2"), step("true")); } @Test @@ -44,19 +38,14 @@ void leavesRealDivisionAndModuloByZeroUnchanged() { @Test void foldsIntegerDivisionTowardZeroForNegativeResults() { - VCImplication implication = vc("(2 - 7) / 2 == -2"); - - assertSimplificationSteps(folding, implication, step("(2 - 7) / 2 == -2"), step("-5 / 2 == -2"), + assertSimplificationSteps(folding, vc("(2 - 7) / 2 == -2"), step("(2 - 7) / 2 == -2"), step("-5 / 2 == -2"), step("-2 == -2"), step("-2 == -2"), step("true")); } @Test void foldsIntegerModuloWithJavaSignedRemainder() { - VCImplication negativeDividend = vc("-5 % 2 < 0"); - VCImplication negativeDivisor = vc("5 % -2 > 0"); - - assertSimplificationSteps(folding, negativeDividend, step("-5 % 2 < 0"), step("-1 < 0"), step("true")); - assertSimplificationSteps(folding, negativeDivisor, step("5 % -2 > 0"), step("1 > 0"), step("true")); + assertSimplificationSteps(folding, vc("-5 % 2 < 0"), step("-5 % 2 < 0"), step("-1 < 0"), step("true")); + assertSimplificationSteps(folding, vc("5 % -2 > 0"), step("5 % -2 > 0"), step("1 > 0"), step("true")); } @Test @@ -85,9 +74,7 @@ void foldsPartialComparisonsWithoutDroppingSymbolicTerms() { @Test void foldsUnaryExpressions() { assertSimplificationSteps(folding, vc("!true"), step("false")); - VCImplication implication = vc("-3 < 0"); - - assertSimplificationSteps(folding, implication, step("-3 < 0"), step("true")); + assertSimplificationSteps(folding, vc("-3 < 0"), step("-3 < 0"), step("true")); } @Test @@ -99,9 +86,7 @@ void foldsIteExpressions() { @Test void foldsIteBranchesBeforeComparingThem() { - VCImplication implication = vc("cond ? 1 + 2 : 3"); - - assertSimplificationSteps(folding, implication, step("cond ? 3 : 3"), step("3")); + assertSimplificationSteps(folding, vc("cond ? 1 + 2 : 3"), step("cond ? 3 : 3"), step("3")); } @Test @@ -118,6 +103,16 @@ void foldsEnumEqualityAndInequality() { assertSimplificationSteps(folding, vc("Mode.Photo != Mode.Video"), step("true")); } + @Test + void recordsOriginWhenOnlyGroupIsUnwrapped() { + assertSimplificationSteps(folding, vc("(x > 0)"), step("x > 0")); + } + + @Test + void recordsOriginWhenFoldingLaterImplication() { + assertSimplificationSteps(folding, vc("x > 0", "1 + 2 > 0"), step("x > 0", "3 > 0"), step("x > 0", "true")); + } + @Test void foldsResolvedEnumLiterals() { Enum limit = new Enum("Config", "LIMIT"); @@ -138,23 +133,4 @@ void foldsResolvedEnumLiteralsInsideLargerExpression() { assertSimplificationSteps(folding, implication, step("3 + 2 == 5"), step("5 == 5"), step("true")); } - - @Test - void recordsOriginWhenOnlyGroupIsUnwrapped() { - VCImplication implication = vc("(x > 0)"); - VCSimplificationResult result = assertSimplificationSteps(folding, implication, step("x > 0")); - - assertEquals("x > 0", result.getImplication().getRefinement().toString()); - } - - @Test - void recordsOriginWhenFoldingLaterImplication() { - VCImplication implication = vc("x > 0", "1 + 2 > 0"); - - VCSimplificationResult result = assertSimplificationSteps(folding, implication, step("x > 0", "3 > 0")); - - result = assertSimplificationSteps(folding, result.getImplication(), step("x > 0", "true")); - assertEquals("true", result.getImplication().getNext().getRefinement().getExpression().toDisplayString()); - } - } diff --git a/liquidjava-verifier/src/test/java/liquidjava/rj_language/opt/VCLogicalSimplificationTest.java b/liquidjava-verifier/src/test/java/liquidjava/rj_language/opt/VCLogicalSimplificationTest.java index 99ad7cc1..141744d9 100644 --- a/liquidjava-verifier/src/test/java/liquidjava/rj_language/opt/VCLogicalSimplificationTest.java +++ b/liquidjava-verifier/src/test/java/liquidjava/rj_language/opt/VCLogicalSimplificationTest.java @@ -1,7 +1,6 @@ package liquidjava.rj_language.opt; import static liquidjava.utils.VCTestUtils.*; -import liquidjava.processor.VCImplication; import org.junit.jupiter.api.Test; class VCLogicalSimplificationTest { @@ -66,8 +65,6 @@ void simplifiesIteChildren() { @Test void recordsOriginWhenSimplifyingLaterImplication() { - VCImplication implication = vc("x > 0", "y || false"); - - assertSimplificationSteps(simplification, implication, step("x > 0", "y")); + assertSimplificationSteps(simplification, vc("x > 0", "y || false"), step("x > 0", "y")); } } 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 8e3115bd..b2c18116 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 @@ -1,11 +1,8 @@ package liquidjava.rj_language.opt; import static liquidjava.utils.VCTestUtils.*; -import static org.junit.jupiter.api.Assertions.assertEquals; -import static org.junit.jupiter.api.Assertions.assertNotNull; import static org.junit.jupiter.api.Assertions.assertNull; -import liquidjava.processor.VCImplication; import org.junit.jupiter.api.Test; class VCSimplificationTest { @@ -22,162 +19,98 @@ void simplifyOnceReturnsNullForNullImplication() { @Test void simplifyOnceAppliesSubstitutionBeforeFolding() { - VCImplication implication = vc("∀x:int. x == 1 + 2", "x > 2"); - - assertSimplificationSteps(implication, step("1 + 2 > 2"), step("3 > 2"), step("true")); + assertSimplificationSteps(vc("∀x:int. x == 1 + 2", "x > 2"), step("1 + 2 > 2"), step("3 > 2"), step("true")); } @Test void simplifyOnceDoesNotFoldAfterSubstitutionInSameStep() { - VCImplication implication = vc("∀x:int. x == 1 + 2", "x == 3"); - - assertSimplificationSteps(implication, step("1 + 2 == 3"), step("3 == 3"), step("true")); + assertSimplificationSteps(vc("∀x:int. x == 1 + 2", "x == 3"), step("1 + 2 == 3"), step("3 == 3"), step("true")); } @Test void simplifyOnceAppliesSubstitutionBeforeBinderSimplification() { - VCImplication implication = vc("∀x:int. x == 3", "∀y:int. true", "x > 0"); - - assertSimplificationSteps(implication, step("true", "3 > 0"), step("3 > 0"), step("true")); + assertSimplificationSteps(vc("∀x:int. x == 3", "∀y:int. true", "x > 0"), step("true", "3 > 0"), step("3 > 0"), + step("true")); } @Test void simplifyOnceAppliesBinderSimplificationBeforeFolding() { - VCImplication implication = vc("∀x:int. true", "1 + 2 > 0"); - - assertSimplificationSteps(implication, step("1 + 2 > 0"), step("3 > 0")); + assertSimplificationSteps(vc("∀x:int. true", "1 + 2 > 0"), step("1 + 2 > 0"), step("3 > 0")); } @Test void simplifyOnceAppliesBinderSimplificationBeforeLogicalSimplification() { - VCImplication implication = vc("∀x:int. true", "y && true"); - - assertSimplificationSteps(implication, step("y && true"), step("y")); + assertSimplificationSteps(vc("∀x:int. true", "y && true"), step("y && true"), step("y")); } @Test void simplifyOnceAppliesFoldingWhenNoSubstitutionIsAvailable() { - VCImplication implication = vc("1 + 2 > 2"); - - assertSimplificationSteps(implication, step("3 > 2"), step("true")); + assertSimplificationSteps(vc("1 + 2 > 2"), step("3 > 2"), step("true")); } @Test void simplifyOnceAppliesFoldingBeforeArithmeticSimplification() { - VCImplication implication = vc("1 + 2 + x + 0 > 0"); - - assertSimplificationSteps(implication, step("3 + x + 0 > 0")); + assertSimplificationSteps(vc("1 + 2 + x + 0 > 0"), step("3 + x + 0 > 0")); } @Test void simplifyOnceAppliesArithmeticWhenNoSubstitutionOrFoldingIsAvailable() { - VCImplication implication = vc("x + 0 > 0"); - - assertSimplificationSteps(implication, step("x > 0")); + assertSimplificationSteps(vc("x + 0 > 0"), step("x > 0")); } @Test void simplifyOnceAppliesArithmeticBeforeLogicalSimplification() { - VCImplication implication = vc("x + 0 == x"); - - assertSimplificationSteps(implication, step("x == x"), step("true")); + assertSimplificationSteps(vc("x + 0 == x"), step("x == x"), step("true")); } @Test void simplifyOnceAppliesLogicalWhenNoEarlierSimplificationIsAvailable() { - VCImplication implication = vc("x && true"); - - assertSimplificationSteps(implication, step("x")); + assertSimplificationSteps(vc("x && true"), step("x")); } @Test void simplifyAppliesLogicalStepsUntilFixedPoint() { - VCImplication implication = vc("x && true && true"); - - assertSimplificationSteps(implication, step("x && true"), step("x")); + assertSimplificationSteps(vc("x && true && true"), step("x && true"), step("x")); } @Test void simplifyKeepsApplyingStepsUntilFixedPoint() { - VCImplication implication = vc("∀x:int. x == 1 + 2", "x + 1 > 3"); - - assertSimplificationSteps(implication, step("1 + 2 + 1 > 3"), step("3 + 1 > 3"), step("4 > 3"), step("true")); + assertSimplificationSteps(vc("∀x:int. x == 1 + 2", "x + 1 > 3"), step("1 + 2 + 1 > 3"), step("3 + 1 > 3"), + step("4 > 3"), step("true")); } @Test - void simplifyToFixedPointRemovesTrueBindersOverMultipleSteps() { - VCImplication implication = vc("∀x:int. true", "∀y:int. true", "z > 0"); - - VCSimplificationResult result = VCSimplification.simplifyToFixedPoint(implication); - - assertSimplifiedVC(result.getImplication(), "z > 0"); - assertNotNull(result.getOrigin()); - assertNotNull(result.getOrigin().getOrigin()); + void simplifyRemovesTrueBindersOverMultipleSteps() { + assertSimplificationSteps(vc("∀x:int. true", "∀y:int. true", "z > 0"), step("true", "z > 0"), step("z > 0")); } @Test void simplifyAppliesMultipleSubstitutionsBeforeReachingFixedPoint() { - VCImplication implication = vc("∀x:int. x == 3", "∀y:int. y == x + 1", "y > x"); - - assertSimplificationSteps(implication, step("y == 3 + 1", "y > 3"), step("3 + 1 > 3"), step("4 > 3"), - step("true")); + assertSimplificationSteps(vc("∀x:int. x == 3", "∀y:int. y == x + 1", "y > x"), step("y == 3 + 1", "y > 3"), + step("3 + 1 > 3"), step("4 > 3"), step("true")); } @Test void simplifyAppliesLongSubstitutionChainBeforeReachingFixedPoint() { - VCImplication implication = vc("∀x:int. x == 1", "∀y:int. y == x + 1", "∀z:int. z == y + 1", "z == 3"); - - assertSimplificationSteps(implication, step("y == 1 + 1", "z == y + 1", "z == 3"), - step("z == 1 + 1 + 1", "z == 3"), step("1 + 1 + 1 == 3"), step("2 + 1 == 3"), step("3 == 3"), - step("true")); + assertSimplificationSteps(vc("∀x:int. x == 1", "∀y:int. y == x + 1", "∀z:int. z == y + 1", "z == 3"), + step("y == 1 + 1", "z == y + 1", "z == 3"), step("z == 1 + 1 + 1", "z == 3"), step("1 + 1 + 1 == 3"), + step("2 + 1 == 3"), step("3 == 3"), step("true")); } @Test void simplifyCombinesSubstitutionAndNestedFoldingAcrossFixedPoint() { - VCImplication implication = vc("∀x:int. x == 1", "∀y:int. y == x + 2", "y - 1 == 2"); - - assertSimplificationSteps(implication, step("y == 1 + 2", "y - 1 == 2"), step("1 + 2 - 1 == 2"), - step("3 - 1 == 2"), step("2 == 2"), step("true")); + assertSimplificationSteps(vc("∀x:int. x == 1", "∀y:int. y == x + 2", "y - 1 == 2"), + step("y == 1 + 2", "y - 1 == 2"), step("1 + 2 - 1 == 2"), step("3 - 1 == 2"), step("2 == 2"), + step("true")); } @Test void simplifyStopsAfterSubstitutionWhenOnlyNegativeLiteralShapeChanges() { - VCImplication implication = vc("∀x:int. x == a + 0", "x >= -3"); - - assertSimplificationSteps(implication, step("a + 0 >= -3")); + assertSimplificationSteps(vc("∀x:int. x == a + 0", "x >= -3"), step("a + 0 >= -3")); } @Test void simplifyLeavesUnchangedVcAsPlainPredicates() { - VCImplication implication = vc("x > 0", "y > x"); - - VCSimplificationResult result = VCSimplification.simplifyOnce(new VCSimplificationResult(implication)); - - assertSimplifiedVC(result.getImplication(), "x > 0", "y > x"); - assertNull(result.getOrigin()); - } - - @Test - void simplifyOnceStoresACompleteClonedOriginChain() { - VCImplication implication = vc("x > 0", "y + 0 > x"); - - VCSimplificationResult result = VCSimplification.simplifyOnce(new VCSimplificationResult(implication)); - implication.getNext().setRefinement(vc("changed").getRefinement()); - - assertSimplifiedVC(result.getImplication(), "x > 0", "y > x"); - assertSimplifiedVC(result.getOrigin().getImplication(), "x > 0", "y + 0 > x"); - } - - @Test - void fixedPointHistoryLinksEverySuccessfulStep() { - VCImplication implication = vc("∀x:int. x == 1 + 2", "x + 0 > 2"); - - VCSimplificationResult result = VCSimplification.simplifyToFixedPoint(implication); - int historyLength = 0; - for (VCSimplificationResult current = result.getOrigin(); current != null; current = current.getOrigin()) - historyLength++; - - assertEquals(4, historyLength); - assertSimplifiedVC(result.getImplication(), "true"); + assertSimplificationSteps(vc("x > 0", "y > x"), step("x > 0", "y > x")); } } diff --git a/liquidjava-verifier/src/test/java/liquidjava/rj_language/opt/VCSubstitutionTest.java b/liquidjava-verifier/src/test/java/liquidjava/rj_language/opt/VCSubstitutionTest.java index 2af1733a..299e7b02 100644 --- a/liquidjava-verifier/src/test/java/liquidjava/rj_language/opt/VCSubstitutionTest.java +++ b/liquidjava-verifier/src/test/java/liquidjava/rj_language/opt/VCSubstitutionTest.java @@ -1,7 +1,6 @@ package liquidjava.rj_language.opt; import static liquidjava.utils.VCTestUtils.*; -import liquidjava.processor.VCImplication; import org.junit.jupiter.api.Test; class VCSubstitutionTest { @@ -10,106 +9,80 @@ class VCSubstitutionTest { @Test void substitutesBinderEqualityIntoWholeChain() { - VCImplication implication = vc("∀x:int. x == 3", "x > 0"); - - assertSimplificationSteps(substitution, implication, step("3 > 0")); + assertSimplificationSteps(substitution, vc("∀x:int. x == 3", "x > 0"), step("3 > 0")); } @Test void substitutesReverseBinderEquality() { - VCImplication implication = vc("∀x:int. 3 == x", "x > 0"); - - assertSimplificationSteps(substitution, implication, step("3 > 0")); + assertSimplificationSteps(substitution, vc("∀x:int. 3 == x", "x > 0"), step("3 > 0")); } @Test void substitutesCompoundKnownValue() { - VCImplication implication = vc("∀x:int. x == y + 1", "x > y"); - - assertSimplificationSteps(substitution, implication, step("y + 1 > y")); + assertSimplificationSteps(substitution, vc("∀x:int. x == y + 1", "x > y"), step("y + 1 > y")); } @Test void substitutesOnlyWholeVariableReferences() { - VCImplication implication = vc("∀x:int. x == 3", "xx > x"); - - assertSimplificationSteps(substitution, implication, step("xx > 3")); + assertSimplificationSteps(substitution, vc("∀x:int. x == 3", "xx > x"), step("xx > 3")); } @Test void substitutesEveryOccurrenceInPredicate() { - VCImplication implication = vc("∀x:int. x == 2", "x + x > 0"); - - assertSimplificationSteps(substitution, implication, step("2 + 2 > 0")); + assertSimplificationSteps(substitution, vc("∀x:int. x == 2", "x + x > 0"), step("2 + 2 > 0")); } @Test void preservesRemainingBinderAfterSubstitution() { - VCImplication implication = vc("∀x:int. x == 3", "∀y:int. y > x", "y > 0"); - - assertSimplificationSteps(substitution, implication, step("y > 3", "y > 0")); + assertSimplificationSteps(substitution, vc("∀x:int. x == 3", "∀y:int. y > x", "y > 0"), step("y > 3", "y > 0")); } @Test void keepsSourceNodeWhenItIsLastInChain() { - VCImplication implication = vc("x > 0", "∀y:int. y == 1"); - - assertSimplificationSteps(substitution, implication, step("x > 0", "y == 1")); + assertSimplificationSteps(substitution, vc("x > 0", "∀y:int. y == 1"), step("x > 0", "y == 1")); } @Test void keepsReturnBinderWhenConclusionIsSeparate() { - VCImplication implication = vc("∀x:int. true", "∀#ret_8:int. #ret_8 == x + 1"); - - assertSimplificationSteps(substitution, implication, step("true", "#ret⁸ == x + 1")); + assertSimplificationSteps(substitution, vc("∀x:int. true", "∀#ret_8:int. #ret_8 == x + 1"), + step("true", "#ret⁸ == x + 1")); } @Test void usesFirstSubstitutionFoundInChain() { - VCImplication implication = vc("∀x:int. x > 0", "∀y:int. y == 4", "x + y > 0"); - - assertSimplificationSteps(substitution, implication, step("x > 0", "x + 4 > 0")); + assertSimplificationSteps(substitution, vc("∀x:int. x > 0", "∀y:int. y == 4", "x + y > 0"), + step("x > 0", "x + 4 > 0")); } @Test void substitutesInnerKnownValueAcrossNestedImplications() { - VCImplication implication = vc("∀x:int. true", "∀y:int. y == 1", "∀z:int. z > y", "y + z > 0"); - - assertSimplificationSteps(substitution, implication, step("true", "z > 1", "1 + z > 0")); + assertSimplificationSteps(substitution, vc("∀x:int. true", "∀y:int. y == 1", "∀z:int. z > y", "y + z > 0"), + step("true", "z > 1", "1 + z > 0")); } @Test void substitutesOuterKnownValueIntoNestedBinderRefinements() { - VCImplication implication = vc("∀x:int. x == 3", "∀y:int. y == x + 1", "y > x"); - - assertSimplificationSteps(substitution, implication, step("y == 3 + 1", "y > 3"), step("3 + 1 > 3")); + assertSimplificationSteps(substitution, vc("∀x:int. x == 3", "∀y:int. y == x + 1", "y > x"), + step("y == 3 + 1", "y > 3"), step("3 + 1 > 3")); } @Test void ignoresRecursiveBinderEquality() { - VCImplication implication = vc("∀x:int. x == x + 1", "x > 0"); - - assertSimplificationSteps(substitution, implication, step("x == x + 1", "x > 0")); + assertSimplificationSteps(substitution, vc("∀x:int. x == x + 1", "x > 0"), step("x == x + 1", "x > 0")); } @Test void ignoresNonEqualityBinderRefinement() { - VCImplication implication = vc("∀x:int. x > 3", "x > 0"); - - assertSimplificationSteps(substitution, implication, step("x > 3", "x > 0")); + assertSimplificationSteps(substitution, vc("∀x:int. x > 3", "x > 0"), step("x > 3", "x > 0")); } @Test void ignoresDerivedBinderEquality() { - VCImplication implication = vc("∀x:int. x + 1 == 3", "x > 0"); - - assertSimplificationSteps(substitution, implication, step("x + 1 == 3", "x > 0")); + assertSimplificationSteps(substitution, vc("∀x:int. x + 1 == 3", "x > 0"), step("x + 1 == 3", "x > 0")); } @Test void ignoresEqualityWithoutBinder() { - VCImplication implication = vc("x == 3", "x > 0"); - - assertSimplificationSteps(substitution, implication, step("x == 3", "x > 0")); + assertSimplificationSteps(substitution, vc("x == 3", "x > 0"), step("x == 3", "x > 0")); } } diff --git a/liquidjava-verifier/src/test/java/liquidjava/utils/VCTestUtils.java b/liquidjava-verifier/src/test/java/liquidjava/utils/VCTestUtils.java index 96b23754..89203ea4 100644 --- a/liquidjava-verifier/src/test/java/liquidjava/utils/VCTestUtils.java +++ b/liquidjava-verifier/src/test/java/liquidjava/utils/VCTestUtils.java @@ -31,36 +31,6 @@ public static VCImplication vc(String... implications) { return first; } - private static VCImplication parseImplication(String implication) { - if (!implication.startsWith("∀")) - return new VCImplication(new Predicate(RefinementsParser.createAST(implication, ""))); - - int refinementStart = implication.indexOf('.'); - String binder = implication.substring(1, refinementStart).trim(); - String refinement = implication.substring(refinementStart + 1).trim(); - String[] parts = binder.split(":"); - return new VCImplication(parts[0].trim(), type(parts[1].trim()), - new Predicate(RefinementsParser.createAST(refinement, ""))); - } - - private static CtTypeReference type(String name) { - if ("int".equals(name)) - return INT; - throw new IllegalArgumentException("Unsupported test type: " + name); - } - - public static void assertSimplifiedVC(VCImplication implication, String... expected) { - VCImplication current = implication; - for (int i = 0; i < expected.length; i++) { - assertEquals(Predicate.class, current.getRefinement().getClass(), - "Expected simplified refinement at implication " + i + " to be a plain Predicate"); - assertEquals(expected[i], formatRefinement(current), - "Unexpected simplified expression at implication " + i); - current = current.getNext(); - } - assertNull(current, "Expected VC chain to end after " + expected.length + " implications"); - } - public static VCSimplificationResult assertSimplificationSteps(VCImplication implication, ExpectedSimplificationStep... expectedSteps) { VCSimplificationResult current = new VCSimplificationResult(implication); @@ -95,14 +65,44 @@ private static void assertSimplificationResult(VCSimplificationResult previous, assertSimplifiedVC(result.getImplication(), expectedStep.implications()); } - public static ExpectedSimplificationStep step(String... implications) { - return new ExpectedSimplificationStep(implications); + private static void assertSimplifiedVC(VCImplication implication, String... expected) { + VCImplication current = implication; + for (int i = 0; i < expected.length; i++) { + assertEquals(Predicate.class, current.getRefinement().getClass(), + "Expected simplified refinement at implication " + i + " to be a plain Predicate"); + assertEquals(expected[i], formatRefinement(current), + "Unexpected simplified expression at implication " + i); + current = current.getNext(); + } + assertNull(current, "Expected VC chain to end after " + expected.length + " implications"); + } + + private static VCImplication parseImplication(String implication) { + if (!implication.startsWith("∀")) + return new VCImplication(new Predicate(RefinementsParser.createAST(implication, ""))); + + int refinementStart = implication.indexOf('.'); + String binder = implication.substring(1, refinementStart).trim(); + String refinement = implication.substring(refinementStart + 1).trim(); + String[] parts = binder.split(":"); + return new VCImplication(parts[0].trim(), type(parts[1].trim()), + new Predicate(RefinementsParser.createAST(refinement, ""))); + } + + private static CtTypeReference type(String name) { + if ("int".equals(name)) + return INT; + throw new IllegalArgumentException("Unsupported test type: " + name); } private static String formatRefinement(VCImplication implication) { return implication.getRefinement().getExpression().toDisplayString(); } + public static ExpectedSimplificationStep step(String... implications) { + return new ExpectedSimplificationStep(implications); + } + public record ExpectedSimplificationStep(String... implications) { } } From 9e76dcf67c0fb2696caab95a1d3fbf148e567df7 Mon Sep 17 00:00:00 2001 From: Ricardo Costa Date: Thu, 18 Jun 2026 16:14:38 +0100 Subject: [PATCH 4/5] Add More Tests --- .../rj_language/opt/VCSimplificationTest.java | 53 ++++++++++++++++++- .../java/liquidjava/utils/VCTestUtils.java | 1 + 2 files changed, 53 insertions(+), 1 deletion(-) 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 b2c18116..908ea716 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 @@ -33,6 +33,12 @@ void simplifyOnceAppliesSubstitutionBeforeBinderSimplification() { step("true")); } + @Test + void simplifyCombinesSubstitutionWithArithmeticAndLogicalSimplification() { + assertSimplificationSteps(vc("∀x:int. x == y + 0", "x > 0 && true"), step("y + 0 > 0 && true"), + step("y > 0 && true"), step("y > 0")); + } + @Test void simplifyOnceAppliesBinderSimplificationBeforeFolding() { assertSimplificationSteps(vc("∀x:int. true", "1 + 2 > 0"), step("1 + 2 > 0"), step("3 > 0")); @@ -43,6 +49,11 @@ void simplifyOnceAppliesBinderSimplificationBeforeLogicalSimplification() { assertSimplificationSteps(vc("∀x:int. true", "y && true"), step("y && true"), step("y")); } + @Test + void simplifyOnceAppliesBinderSimplificationBeforeArithmeticSimplification() { + assertSimplificationSteps(vc("∀x:int. true", "y + 0 > 0"), step("y + 0 > 0"), step("y > 0")); + } + @Test void simplifyOnceAppliesFoldingWhenNoSubstitutionIsAvailable() { assertSimplificationSteps(vc("1 + 2 > 2"), step("3 > 2"), step("true")); @@ -50,7 +61,13 @@ void simplifyOnceAppliesFoldingWhenNoSubstitutionIsAvailable() { @Test void simplifyOnceAppliesFoldingBeforeArithmeticSimplification() { - assertSimplificationSteps(vc("1 + 2 + x + 0 > 0"), step("3 + x + 0 > 0")); + assertSimplificationSteps(vc("1 + 2 + x + 0 > 0"), step("3 + x + 0 > 0"), step("3 + x > 0")); + } + + @Test + void simplifyCombinesFoldingArithmeticAndLogicalSimplification() { + assertSimplificationSteps(vc("1 + 2 + x + 0 == 3 + x"), step("3 + x + 0 == 3 + x"), step("3 + x == 3 + x"), + step("true")); } @Test @@ -63,11 +80,45 @@ void simplifyOnceAppliesArithmeticBeforeLogicalSimplification() { assertSimplificationSteps(vc("x + 0 == x"), step("x == x"), step("true")); } + @Test + void simplifyOnceAppliesArithmeticBeforeFoldingOnNextStep() { + assertSimplificationSteps(vc("x - x == 0"), step("0 == 0"), step("true")); + } + @Test void simplifyOnceAppliesLogicalWhenNoEarlierSimplificationIsAvailable() { assertSimplificationSteps(vc("x && true"), step("x")); } + @Test + void simplifyUsesFoldingToEnableSubstitutionOnNextStep() { + assertSimplificationSteps(vc("∀x:int. (x) == 3", "x > 0"), step("x == 3", "x > 0"), step("3 > 0"), + step("true")); + } + + @Test + void simplifyUsesArithmeticToEnableSubstitutionOnNextStep() { + assertSimplificationSteps(vc("∀x:int. x + 0 == 3", "x > 0"), step("x == 3", "x > 0"), step("3 > 0"), + step("true")); + } + + @Test + void simplifyUsesLogicalSimplificationToEnableSubstitutionOnNextStep() { + assertSimplificationSteps(vc("∀x:int. true && x == 3", "x > 0"), step("x == 3", "x > 0"), step("3 > 0"), + step("true")); + } + + @Test + void simplifyUsesFoldingToEnableBinderSimplificationOnNextStep() { + assertSimplificationSteps(vc("∀x:int. 1 > 2", "y > 0"), step("false", "y > 0"), step("true")); + } + + @Test + void simplifyUsesArithmeticAndLogicalSimplificationToEnableBinderRemoval() { + assertSimplificationSteps(vc("∀x:int. x + 0 == x", "y > 0"), step("x == x", "y > 0"), step("true", "y > 0"), + step("y > 0")); + } + @Test void simplifyAppliesLogicalStepsUntilFixedPoint() { assertSimplificationSteps(vc("x && true && true"), step("x && true"), step("x")); diff --git a/liquidjava-verifier/src/test/java/liquidjava/utils/VCTestUtils.java b/liquidjava-verifier/src/test/java/liquidjava/utils/VCTestUtils.java index 89203ea4..ab99e559 100644 --- a/liquidjava-verifier/src/test/java/liquidjava/utils/VCTestUtils.java +++ b/liquidjava-verifier/src/test/java/liquidjava/utils/VCTestUtils.java @@ -68,6 +68,7 @@ private static void assertSimplificationResult(VCSimplificationResult previous, private static void assertSimplifiedVC(VCImplication implication, String... expected) { VCImplication current = implication; for (int i = 0; i < expected.length; i++) { + assertNotNull(current, "Expected implication " + i + " with refinement " + expected[i]); assertEquals(Predicate.class, current.getRefinement().getClass(), "Expected simplified refinement at implication " + i + " to be a plain Predicate"); assertEquals(expected[i], formatRefinement(current), From f5cccb137f417facb9a653750c1114bb3d0cb80f Mon Sep 17 00:00:00 2001 From: Ricardo Costa Date: Thu, 18 Jun 2026 16:15:46 +0100 Subject: [PATCH 5/5] Assert Origin Not Equal to Simplified --- .../src/test/java/liquidjava/utils/VCTestUtils.java | 5 +++++ 1 file changed, 5 insertions(+) diff --git a/liquidjava-verifier/src/test/java/liquidjava/utils/VCTestUtils.java b/liquidjava-verifier/src/test/java/liquidjava/utils/VCTestUtils.java index ab99e559..a3e1aa3c 100644 --- a/liquidjava-verifier/src/test/java/liquidjava/utils/VCTestUtils.java +++ b/liquidjava-verifier/src/test/java/liquidjava/utils/VCTestUtils.java @@ -2,6 +2,8 @@ import static org.junit.jupiter.api.Assertions.assertEquals; import static org.junit.jupiter.api.Assertions.assertNotNull; +import static org.junit.jupiter.api.Assertions.assertNotEquals; +import static org.junit.jupiter.api.Assertions.assertNotSame; import static org.junit.jupiter.api.Assertions.assertNull; import liquidjava.processor.VCImplication; @@ -59,6 +61,9 @@ private static void assertSimplificationResult(VCSimplificationResult previous, assertNull(result.getOrigin(), "Unchanged simplification result should not have an origin"); } else { assertNotNull(result.getOrigin(), "Changed simplification result should have an origin"); + assertNotSame(result, result.getOrigin(), "Simplification result should not be its own origin"); + assertNotEquals(result.getImplication(), result.getOrigin().getImplication(), + "Simplification origin should differ from the simplified VC"); assertEquals(previous.getImplication(), result.getOrigin().getImplication(), "Simplification origin should be the complete previous VC"); }