From 1afe4b64a7075b05ace31dabe261f98624011872 Mon Sep 17 00:00:00 2001 From: Ricardo Costa Date: Tue, 17 Mar 2026 11:52:15 +0000 Subject: [PATCH 1/7] Substitute Internal with User-Facing Variables --- .../java/liquidjava/rj_language/opt/VariableResolver.java | 7 +++++++ 1 file changed, 7 insertions(+) diff --git a/liquidjava-verifier/src/main/java/liquidjava/rj_language/opt/VariableResolver.java b/liquidjava-verifier/src/main/java/liquidjava/rj_language/opt/VariableResolver.java index 9d5850e6..06a22d98 100644 --- a/liquidjava-verifier/src/main/java/liquidjava/rj_language/opt/VariableResolver.java +++ b/liquidjava-verifier/src/main/java/liquidjava/rj_language/opt/VariableResolver.java @@ -52,6 +52,13 @@ private static void resolveRecursive(Expression exp, Map map map.put(var.getName(), right.clone()); } else if (right instanceof Var var && left.isLiteral()) { map.put(var.getName(), left.clone()); + } else if (left instanceof Var leftVar && right instanceof Var rightVar) { + // to later substitute internal variable with user-facing variable + if (leftVar.isInternal() && !rightVar.isInternal()) { + map.put(leftVar.getName(), right.clone()); + } else if (rightVar.isInternal() && !leftVar.isInternal()) { + map.put(rightVar.getName(), left.clone()); + } } } } From ad21eb03f1604374824d18e3d40fce7f6a487094 Mon Sep 17 00:00:00 2001 From: Ricardo Costa Date: Tue, 17 Mar 2026 23:50:45 +0000 Subject: [PATCH 2/7] Substitute Internal Variables by Counter --- .../src/main/java/liquidjava/rj_language/ast/Var.java | 11 +++++++++++ .../liquidjava/rj_language/opt/VariableResolver.java | 6 ++++++ 2 files changed, 17 insertions(+) diff --git a/liquidjava-verifier/src/main/java/liquidjava/rj_language/ast/Var.java b/liquidjava-verifier/src/main/java/liquidjava/rj_language/ast/Var.java index 495a873b..d69d0d74 100644 --- a/liquidjava-verifier/src/main/java/liquidjava/rj_language/ast/Var.java +++ b/liquidjava-verifier/src/main/java/liquidjava/rj_language/ast/Var.java @@ -70,4 +70,15 @@ public boolean equals(Object obj) { return name.equals(other.name); } } + + public boolean isInternal() { + return name.startsWith("#"); + } + + public int getCounter() { + if (!isInternal()) + throw new IllegalStateException("Cannot get counter of non-internal variable"); + int lastUnderscore = name.lastIndexOf('_'); + return Integer.parseInt(name.substring(lastUnderscore + 1)); + } } diff --git a/liquidjava-verifier/src/main/java/liquidjava/rj_language/opt/VariableResolver.java b/liquidjava-verifier/src/main/java/liquidjava/rj_language/opt/VariableResolver.java index 06a22d98..c11c730e 100644 --- a/liquidjava-verifier/src/main/java/liquidjava/rj_language/opt/VariableResolver.java +++ b/liquidjava-verifier/src/main/java/liquidjava/rj_language/opt/VariableResolver.java @@ -58,6 +58,12 @@ private static void resolveRecursive(Expression exp, Map map map.put(leftVar.getName(), right.clone()); } else if (rightVar.isInternal() && !leftVar.isInternal()) { map.put(rightVar.getName(), left.clone()); + } else if (leftVar.isInternal() && rightVar.isInternal()) { + // substitute the lower-counter variable with the higher-counter one + boolean isLeftCounterLower = leftVar.getCounter() <= rightVar.getCounter(); + Var lowerVar = isLeftCounterLower ? leftVar : rightVar; + Var higherVar = isLeftCounterLower ? rightVar : leftVar; + map.putIfAbsent(lowerVar.getName(), higherVar.clone()); } } } From cc86f95d1ce8651595e2a192f48e8f5ec31d4969 Mon Sep 17 00:00:00 2001 From: Ricardo Costa Date: Tue, 17 Mar 2026 23:55:13 +0000 Subject: [PATCH 3/7] Update Comments --- .../java/liquidjava/rj_language/opt/VariableResolver.java | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/liquidjava-verifier/src/main/java/liquidjava/rj_language/opt/VariableResolver.java b/liquidjava-verifier/src/main/java/liquidjava/rj_language/opt/VariableResolver.java index c11c730e..bd6364a7 100644 --- a/liquidjava-verifier/src/main/java/liquidjava/rj_language/opt/VariableResolver.java +++ b/liquidjava-verifier/src/main/java/liquidjava/rj_language/opt/VariableResolver.java @@ -53,13 +53,13 @@ private static void resolveRecursive(Expression exp, Map map } else if (right instanceof Var var && left.isLiteral()) { map.put(var.getName(), left.clone()); } else if (left instanceof Var leftVar && right instanceof Var rightVar) { - // to later substitute internal variable with user-facing variable + // to substitute internal variable with user-facing variable if (leftVar.isInternal() && !rightVar.isInternal()) { map.put(leftVar.getName(), right.clone()); } else if (rightVar.isInternal() && !leftVar.isInternal()) { map.put(rightVar.getName(), left.clone()); } else if (leftVar.isInternal() && rightVar.isInternal()) { - // substitute the lower-counter variable with the higher-counter one + // to substitute the lower-counter variable with the higher-counter one boolean isLeftCounterLower = leftVar.getCounter() <= rightVar.getCounter(); Var lowerVar = isLeftCounterLower ? leftVar : rightVar; Var higherVar = isLeftCounterLower ? rightVar : leftVar; From b9a3513af55735a5ce15533215fc32bd65977e15 Mon Sep 17 00:00:00 2001 From: Ricardo Costa Date: Wed, 18 Mar 2026 16:25:38 +0000 Subject: [PATCH 4/7] Trigger Workflow From a80817997306bd5ebe19df6230741f79b26526da Mon Sep 17 00:00:00 2001 From: Ricardo Costa Date: Wed, 18 Mar 2026 17:16:38 +0000 Subject: [PATCH 5/7] Add Tests --- .../opt/ExpressionSimplifierTest.java | 190 ++++++++++++++++++ 1 file changed, 190 insertions(+) diff --git a/liquidjava-verifier/src/test/java/liquidjava/rj_language/opt/ExpressionSimplifierTest.java b/liquidjava-verifier/src/test/java/liquidjava/rj_language/opt/ExpressionSimplifierTest.java index b49ce805..142e19f5 100644 --- a/liquidjava-verifier/src/test/java/liquidjava/rj_language/opt/ExpressionSimplifierTest.java +++ b/liquidjava-verifier/src/test/java/liquidjava/rj_language/opt/ExpressionSimplifierTest.java @@ -550,6 +550,196 @@ void testTransitive() { assertEquals("a == 1", result.getValue().toString(), "Expected result to be a == 1"); } + @Test + void testVarToVarPropagationWithInternalVariable() { + // Given: #x_0 == a && #x_0 > 5 + // Expected: a > 5 (internal #x_0 substituted with user-facing a) + + Expression varX0 = new Var("#x_0"); + Expression varA = new Var("a"); + Expression x0EqualsA = new BinaryExpression(varX0, "==", varA); + Expression x0Greater5 = new BinaryExpression(varX0, ">", new LiteralInt(5)); + Expression fullExpression = new BinaryExpression(x0EqualsA, "&&", x0Greater5); + + // When + ValDerivationNode result = ExpressionSimplifier.simplify(fullExpression); + + // Then + assertNotNull(result, "Result should not be null"); + assertEquals("a > 5", result.getValue().toString(), + "Internal variable #x_0 should be substituted with user-facing variable a"); + } + + @Test + void testVarToVarInternalToInternal() { + // Given: #a_1 == #b_2 && #b_2 == 5 && x == #a_1 + 1 + // Expected: x == 5 + 1 = x == 6 + + Expression varA = new Var("#a_1"); + Expression varB = new Var("#b_2"); + Expression varX = new Var("x"); + Expression five = new LiteralInt(5); + Expression aEqualsB = new BinaryExpression(varA, "==", varB); + Expression bEquals5 = new BinaryExpression(varB, "==", five); + Expression aPlus1 = new BinaryExpression(varA, "+", new LiteralInt(1)); + Expression xEqualsAPlus1 = new BinaryExpression(varX, "==", aPlus1); + Expression firstAnd = new BinaryExpression(aEqualsB, "&&", bEquals5); + Expression fullExpression = new BinaryExpression(firstAnd, "&&", xEqualsAPlus1); + + // When + ValDerivationNode result = ExpressionSimplifier.simplify(fullExpression); + + // Then + assertNotNull(result, "Result should not be null"); + assertEquals("x == 6", result.getValue().toString(), + "#a should resolve through #b to 5 across passes, then x == 5 + 1 = x == 6"); + } + + @Test + void testVarToVarDoesNotAffectUserFacingVariables() { + // Given: x == y && x > 5 + // Expected: x == y && x > 5 (user-facing var-to-var should not be propagated) + + Expression varX = new Var("x"); + Expression varY = new Var("y"); + Expression xEqualsY = new BinaryExpression(varX, "==", varY); + Expression xGreater5 = new BinaryExpression(varX, ">", new LiteralInt(5)); + Expression fullExpression = new BinaryExpression(xEqualsY, "&&", xGreater5); + + // When + ValDerivationNode result = ExpressionSimplifier.simplify(fullExpression); + + // Then + assertNotNull(result, "Result should not be null"); + assertEquals("x == y && x > 5", result.getValue().toString(), + "User-facing variable equalities should not trigger var-to-var propagation"); + } + + @Test + void testVarToVarRemovesRedundantEquality() { + // Given: #ret_1 == #b_0 - 100 && #b_0 == b && b >= -128 && b <= 127 + // Expected: #ret_1 == b - 100 && b >= -128 && b <= 127 (#b_0 replaced with b, #b_0 == b removed) + + Expression ret1 = new Var("#ret_1"); + Expression b0 = new Var("#b_0"); + Expression b = new Var("b"); + Expression ret1EqB0Minus100 = new BinaryExpression(ret1, "==", + new BinaryExpression(b0, "-", new LiteralInt(100))); + Expression b0EqB = new BinaryExpression(b0, "==", b); + Expression bGeMinus128 = new BinaryExpression(b, ">=", new UnaryExpression("-", new LiteralInt(128))); + Expression bLe127 = new BinaryExpression(b, "<=", new LiteralInt(127)); + Expression and1 = new BinaryExpression(ret1EqB0Minus100, "&&", b0EqB); + Expression and2 = new BinaryExpression(bGeMinus128, "&&", bLe127); + Expression fullExpression = new BinaryExpression(and1, "&&", and2); + + // When + ValDerivationNode result = ExpressionSimplifier.simplify(fullExpression); + + // Then + assertNotNull(result, "Result should not be null"); + assertEquals("#ret_1 == b - 100 && b >= -128 && b <= 127", result.getValue().toString(), + "Internal variable #b_0 should be replaced with b and redundant equality removed"); + assertNotNull(result.getOrigin(), "Origin should be present showing the var-to-var derivation"); + } + + @Test + void testInternalToInternalReducesRedundantVariable() { + // Given: #a_3 == #b_7 && #a_3 > 5 + // Expected: #b_7 > 5 (#a_3 has lower counter, so #a_3 -> #b_7) + + Expression a3 = new Var("#a_3"); + Expression b7 = new Var("#b_7"); + Expression a3EqualsB7 = new BinaryExpression(a3, "==", b7); + Expression a3Greater5 = new BinaryExpression(a3, ">", new LiteralInt(5)); + Expression fullExpression = new BinaryExpression(a3EqualsB7, "&&", a3Greater5); + + ValDerivationNode result = ExpressionSimplifier.simplify(fullExpression); + + assertNotNull(result); + assertEquals("#b_7 > 5", result.getValue().toString(), + "#a_3 (lower counter) should be substituted with #b_7 (higher counter)"); + } + + @Test + void testInternalToInternalChainWithUserFacingVariableUserFacingFirst() { + // Given: #b_7 == x && #a_3 == #b_7 && x > 0 + // Expected: x > 0 (#b_7 -> x (user-facing); #a_3 has lower counter so #a_3 -> #b_7) + + Expression a3 = new Var("#a_3"); + Expression b7 = new Var("#b_7"); + Expression x = new Var("x"); + Expression b7EqualsX = new BinaryExpression(b7, "==", x); + Expression a3EqualsB7 = new BinaryExpression(a3, "==", b7); + Expression xGreater0 = new BinaryExpression(x, ">", new LiteralInt(0)); + Expression and1 = new BinaryExpression(b7EqualsX, "&&", a3EqualsB7); + Expression fullExpression = new BinaryExpression(and1, "&&", xGreater0); + + ValDerivationNode result = ExpressionSimplifier.simplify(fullExpression); + + assertNotNull(result); + assertEquals("x > 0", result.getValue().toString(), + "Both internal variables should be eliminated via chain resolution"); + } + + @Test + void testInternalToInternalChainWithUserFacingVariableInternalFirst() { + // Given: #a_3 == #b_7 && #b_7 == x && x > 0 + // Expected: x > 0 (#a_3 has lower counter so #a_3 -> #b_7; #b_7 -> x (user-facing) overwrites) + + Expression a3 = new Var("#a_3"); + Expression b7 = new Var("#b_7"); + Expression x = new Var("x"); + Expression a3EqualsB7 = new BinaryExpression(a3, "==", b7); + Expression b7EqualsX = new BinaryExpression(b7, "==", x); + Expression xGreater0 = new BinaryExpression(x, ">", new LiteralInt(0)); + Expression and1 = new BinaryExpression(a3EqualsB7, "&&", b7EqualsX); + Expression fullExpression = new BinaryExpression(and1, "&&", xGreater0); + + ValDerivationNode result = ExpressionSimplifier.simplify(fullExpression); + + assertNotNull(result); + assertEquals("x > 0", result.getValue().toString(), + "Both internal variables should be eliminated via fixed-point iteration"); + } + + @Test + void testInternalToInternalBothResolvingToLiteral() { + // Given: #a_3 == #b_7 && #b_7 == 5 + // Expected: 5 == 5 && 5 == 5 -> true (#a_3 has lower counter so #a_3 -> #b_7; #b_7 -> 5) + + Expression a3 = new Var("#a_3"); + Expression b7 = new Var("#b_7"); + Expression five = new LiteralInt(5); + Expression a3EqualsB7 = new BinaryExpression(a3, "==", b7); + Expression b7Equals5 = new BinaryExpression(b7, "==", five); + Expression fullExpression = new BinaryExpression(a3EqualsB7, "&&", b7Equals5); + + ValDerivationNode result = ExpressionSimplifier.simplify(fullExpression); + + assertNotNull(result); + assertEquals("true", result.getValue().toString(), + "#a_3 -> #b_7 -> 5 and #b_7 -> 5; both equalities collapse to 5 == 5 -> true"); + } + + @Test + void testInternalToInternalNoFurtherResolution() { + // Given: #a_3 == #b_7 && #b_7 + 1 > 0 + // Expected: #b_7 + 1 > 0 (#a_3 has lower counter, so #a_3 -> #b_7) + + Expression a3 = new Var("#a_3"); + Expression b7 = new Var("#b_7"); + Expression a3EqualsB7 = new BinaryExpression(a3, "==", b7); + Expression b7Plus1 = new BinaryExpression(b7, "+", new LiteralInt(1)); + Expression b7Plus1Greater0 = new BinaryExpression(b7Plus1, ">", new LiteralInt(0)); + Expression fullExpression = new BinaryExpression(a3EqualsB7, "&&", b7Plus1Greater0); + + ValDerivationNode result = ExpressionSimplifier.simplify(fullExpression); + + assertNotNull(result); + assertEquals("#b_7 + 1 > 0", result.getValue().toString(), + "#a_3 (lower counter) replaced by #b_7 (higher counter); equality collapses to trivial"); + } + /** * Helper method to compare two derivation nodes recursively */ From 9b8041865bcc5d3976f25b3d39267b316bff4291 Mon Sep 17 00:00:00 2001 From: Ricardo Costa Date: Fri, 20 Mar 2026 19:56:53 +0000 Subject: [PATCH 6/7] Remove Weaker Conjuncts --- .../rj_language/opt/ExpressionSimplifier.java | 27 ++++++ .../opt/ExpressionSimplifierTest.java | 92 +++++++++++++++++++ 2 files changed, 119 insertions(+) diff --git a/liquidjava-verifier/src/main/java/liquidjava/rj_language/opt/ExpressionSimplifier.java b/liquidjava-verifier/src/main/java/liquidjava/rj_language/opt/ExpressionSimplifier.java index 2e43e326..daff33f4 100644 --- a/liquidjava-verifier/src/main/java/liquidjava/rj_language/opt/ExpressionSimplifier.java +++ b/liquidjava-verifier/src/main/java/liquidjava/rj_language/opt/ExpressionSimplifier.java @@ -1,11 +1,15 @@ package liquidjava.rj_language.opt; +import liquidjava.processor.context.Context; +import liquidjava.rj_language.Predicate; import liquidjava.rj_language.ast.BinaryExpression; import liquidjava.rj_language.ast.Expression; import liquidjava.rj_language.ast.LiteralBoolean; import liquidjava.rj_language.opt.derivation_node.BinaryDerivationNode; import liquidjava.rj_language.opt.derivation_node.DerivationNode; import liquidjava.rj_language.opt.derivation_node.ValDerivationNode; +import liquidjava.smt.SMTEvaluator; +import liquidjava.smt.SMTResult; public class ExpressionSimplifier { @@ -74,6 +78,16 @@ private static ValDerivationNode simplifyValDerivationNode(ValDerivationNode nod return leftSimplified; } + // remove weaker conjuncts (e.g. x > 0 && x > -1 => x > 0) + if (implies(leftSimplified.getValue(), rightSimplified.getValue())) { + return new ValDerivationNode(leftSimplified.getValue(), + new BinaryDerivationNode(leftSimplified, rightSimplified, "&&")); + } + if (implies(rightSimplified.getValue(), leftSimplified.getValue())) { + return new ValDerivationNode(rightSimplified.getValue(), + new BinaryDerivationNode(leftSimplified, rightSimplified, "&&")); + } + // return the conjunction with simplified children Expression newValue = new BinaryExpression(leftSimplified.getValue(), "&&", rightSimplified.getValue()); DerivationNode newOrigin = new BinaryDerivationNode(leftSimplified, rightSimplified, "&&"); @@ -114,4 +128,17 @@ private static boolean isRedundant(Expression exp) { } return false; } + + /** + * Checks whether one expression implies another by asking Z3, used to remove weaker conjuncts in the simplification + */ + private static boolean implies(Expression stronger, Expression weaker) { + try { + SMTResult result = new SMTEvaluator().verifySubtype(new Predicate(stronger), new Predicate(weaker), + Context.getInstance()); + return result.isOk(); + } catch (Exception e) { + return false; + } + } } diff --git a/liquidjava-verifier/src/test/java/liquidjava/rj_language/opt/ExpressionSimplifierTest.java b/liquidjava-verifier/src/test/java/liquidjava/rj_language/opt/ExpressionSimplifierTest.java index 142e19f5..ea408b0d 100644 --- a/liquidjava-verifier/src/test/java/liquidjava/rj_language/opt/ExpressionSimplifierTest.java +++ b/liquidjava-verifier/src/test/java/liquidjava/rj_language/opt/ExpressionSimplifierTest.java @@ -2,6 +2,8 @@ import static org.junit.jupiter.api.Assertions.*; +import liquidjava.processor.context.Context; +import liquidjava.rj_language.Predicate; import liquidjava.rj_language.ast.BinaryExpression; import liquidjava.rj_language.ast.Expression; import liquidjava.rj_language.ast.LiteralBoolean; @@ -14,12 +16,17 @@ import liquidjava.rj_language.opt.derivation_node.ValDerivationNode; import liquidjava.rj_language.opt.derivation_node.VarDerivationNode; import org.junit.jupiter.api.Test; +import spoon.Launcher; +import spoon.reflect.factory.Factory; /** * Test suite for expression simplification using constant propagation and folding */ class ExpressionSimplifierTest { + private final Factory factory = new Launcher().getFactory(); + private final Context context = Context.getInstance(); + @Test void testNegation() { // Given: -a && a == 7 @@ -740,6 +747,81 @@ void testInternalToInternalNoFurtherResolution() { "#a_3 (lower counter) replaced by #b_7 (higher counter); equality collapses to trivial"); } + @Test + void testEntailedConjunctIsRemovedButOriginIsPreserved() { + // Given: b >= 100 && b > 0 + // Expected: b >= 100 (b >= 100 implies b > 0) + + addIntVariableToContext("b"); + Expression b = new Var("b"); + Expression bGe100 = new BinaryExpression(b, ">=", new LiteralInt(100)); + Expression bGt0 = new BinaryExpression(b, ">", new LiteralInt(0)); + Expression fullExpression = new BinaryExpression(bGe100, "&&", bGt0); + + ValDerivationNode result = ExpressionSimplifier.simplify(fullExpression); + + assertNotNull(result); + assertEquals("b >= 100", result.getValue().toString(), + "The weaker conjunct should be removed when implied by the stronger one"); + + ValDerivationNode expectedLeft = new ValDerivationNode(bGe100, null); + ValDerivationNode expectedRight = new ValDerivationNode(bGt0, null); + ValDerivationNode expected = new ValDerivationNode(bGe100, + new BinaryDerivationNode(expectedLeft, expectedRight, "&&")); + + assertDerivationEquals(expected, result, "Entailment simplification should preserve conjunction origin"); + } + + @Test + void testStrictComparisonImpliesNonStrictComparison() { + // Given: x > y && x >= y + // Expected: x > y (x > y implies x >= y) + + addIntVariableToContext("x"); + addIntVariableToContext("y"); + Expression x = new Var("x"); + Expression y = new Var("y"); + Expression xGtY = new BinaryExpression(x, ">", y); + Expression xGeY = new BinaryExpression(x, ">=", y); + Expression fullExpression = new BinaryExpression(xGtY, "&&", xGeY); + + ValDerivationNode result = ExpressionSimplifier.simplify(fullExpression); + + assertNotNull(result); + assertEquals("x > y", result.getValue().toString(), + "The stricter comparison should be kept when it implies the weaker one"); + + ValDerivationNode expectedLeft = new ValDerivationNode(xGtY, null); + ValDerivationNode expectedRight = new ValDerivationNode(xGeY, null); + ValDerivationNode expected = new ValDerivationNode(xGtY, + new BinaryDerivationNode(expectedLeft, expectedRight, "&&")); + + assertDerivationEquals(expected, result, "Strict comparison simplification should preserve conjunction origin"); + } + + @Test + void testEquivalentBoundsKeepOneSide() { + // Given: i >= 0 && 0 <= i + // Expected: 0 <= i (both conjuncts express the same condition) + addIntVariableToContext("i"); + Expression i = new Var("i"); + Expression zeroLeI = new BinaryExpression(new LiteralInt(0), "<=", i); + Expression iGeZero = new BinaryExpression(i, ">=", new LiteralInt(0)); + Expression fullExpression = new BinaryExpression(zeroLeI, "&&", iGeZero); + + ValDerivationNode result = ExpressionSimplifier.simplify(fullExpression); + + assertNotNull(result); + assertEquals("0 <= i", result.getValue().toString(), "Equivalent bounds should collapse to a single conjunct"); + + ValDerivationNode expectedLeft = new ValDerivationNode(zeroLeI, null); + ValDerivationNode expectedRight = new ValDerivationNode(iGeZero, null); + ValDerivationNode expected = new ValDerivationNode(zeroLeI, + new BinaryDerivationNode(expectedLeft, expectedRight, "&&")); + + assertDerivationEquals(expected, result, "Equivalent bounds simplification should preserve conjunction origin"); + } + /** * Helper method to compare two derivation nodes recursively */ @@ -768,4 +850,14 @@ private void assertDerivationEquals(DerivationNode expected, DerivationNode actu assertDerivationEquals(expectedUnary.getOperand(), actualUnary.getOperand(), message + " > operand"); } } + + /** + * Helper method to add an integer variable to the context Needed for tests that rely on the SMT-based implication + * checks The simplifier asks Z3 whether one conjunct implies another, so every variable in those expressions must + * be in the context + */ + private void addIntVariableToContext(String name) { + context.addVarToContext(name, factory.Type().INTEGER_PRIMITIVE, new Predicate(), + factory.Code().createCodeSnippetStatement("")); + } } From b8141146d83d212b9c89e4240fc4c2de1acf4610 Mon Sep 17 00:00:00 2001 From: Ricardo Costa Date: Sat, 28 Mar 2026 15:21:10 +0000 Subject: [PATCH 7/7] Improve Tests --- .../opt/ExpressionSimplifierTest.java | 195 +++++++----------- .../test/java/liquidjava/utils/TestUtils.java | 61 ++++++ 2 files changed, 133 insertions(+), 123 deletions(-) diff --git a/liquidjava-verifier/src/test/java/liquidjava/rj_language/opt/ExpressionSimplifierTest.java b/liquidjava-verifier/src/test/java/liquidjava/rj_language/opt/ExpressionSimplifierTest.java index ea0921cb..6ac20359 100644 --- a/liquidjava-verifier/src/test/java/liquidjava/rj_language/opt/ExpressionSimplifierTest.java +++ b/liquidjava-verifier/src/test/java/liquidjava/rj_language/opt/ExpressionSimplifierTest.java @@ -1,9 +1,8 @@ package liquidjava.rj_language.opt; import static org.junit.jupiter.api.Assertions.*; +import static liquidjava.utils.TestUtils.*; -import liquidjava.processor.context.Context; -import liquidjava.rj_language.Predicate; import java.util.List; import java.util.Map; @@ -17,23 +16,17 @@ import liquidjava.rj_language.ast.UnaryExpression; import liquidjava.rj_language.ast.Var; import liquidjava.rj_language.opt.derivation_node.BinaryDerivationNode; -import liquidjava.rj_language.opt.derivation_node.DerivationNode; import liquidjava.rj_language.opt.derivation_node.IteDerivationNode; import liquidjava.rj_language.opt.derivation_node.UnaryDerivationNode; import liquidjava.rj_language.opt.derivation_node.ValDerivationNode; import liquidjava.rj_language.opt.derivation_node.VarDerivationNode; import org.junit.jupiter.api.Test; -import spoon.Launcher; -import spoon.reflect.factory.Factory; /** * Test suite for expression simplification using constant propagation and folding */ class ExpressionSimplifierTest { - private final Factory factory = new Launcher().getFactory(); - private final Context context = Context.getInstance(); - @Test void testNegation() { // Given: -a && a == 7 @@ -891,81 +884,6 @@ void testInternalToInternalNoFurtherResolution() { "#a_3 (lower counter) replaced by #b_7 (higher counter); equality collapses to trivial"); } - @Test - void testEntailedConjunctIsRemovedButOriginIsPreserved() { - // Given: b >= 100 && b > 0 - // Expected: b >= 100 (b >= 100 implies b > 0) - - addIntVariableToContext("b"); - Expression b = new Var("b"); - Expression bGe100 = new BinaryExpression(b, ">=", new LiteralInt(100)); - Expression bGt0 = new BinaryExpression(b, ">", new LiteralInt(0)); - Expression fullExpression = new BinaryExpression(bGe100, "&&", bGt0); - - ValDerivationNode result = ExpressionSimplifier.simplify(fullExpression); - - assertNotNull(result); - assertEquals("b >= 100", result.getValue().toString(), - "The weaker conjunct should be removed when implied by the stronger one"); - - ValDerivationNode expectedLeft = new ValDerivationNode(bGe100, null); - ValDerivationNode expectedRight = new ValDerivationNode(bGt0, null); - ValDerivationNode expected = new ValDerivationNode(bGe100, - new BinaryDerivationNode(expectedLeft, expectedRight, "&&")); - - assertDerivationEquals(expected, result, "Entailment simplification should preserve conjunction origin"); - } - - @Test - void testStrictComparisonImpliesNonStrictComparison() { - // Given: x > y && x >= y - // Expected: x > y (x > y implies x >= y) - - addIntVariableToContext("x"); - addIntVariableToContext("y"); - Expression x = new Var("x"); - Expression y = new Var("y"); - Expression xGtY = new BinaryExpression(x, ">", y); - Expression xGeY = new BinaryExpression(x, ">=", y); - Expression fullExpression = new BinaryExpression(xGtY, "&&", xGeY); - - ValDerivationNode result = ExpressionSimplifier.simplify(fullExpression); - - assertNotNull(result); - assertEquals("x > y", result.getValue().toString(), - "The stricter comparison should be kept when it implies the weaker one"); - - ValDerivationNode expectedLeft = new ValDerivationNode(xGtY, null); - ValDerivationNode expectedRight = new ValDerivationNode(xGeY, null); - ValDerivationNode expected = new ValDerivationNode(xGtY, - new BinaryDerivationNode(expectedLeft, expectedRight, "&&")); - - assertDerivationEquals(expected, result, "Strict comparison simplification should preserve conjunction origin"); - } - - @Test - void testEquivalentBoundsKeepOneSide() { - // Given: i >= 0 && 0 <= i - // Expected: 0 <= i (both conjuncts express the same condition) - addIntVariableToContext("i"); - Expression i = new Var("i"); - Expression zeroLeI = new BinaryExpression(new LiteralInt(0), "<=", i); - Expression iGeZero = new BinaryExpression(i, ">=", new LiteralInt(0)); - Expression fullExpression = new BinaryExpression(zeroLeI, "&&", iGeZero); - - ValDerivationNode result = ExpressionSimplifier.simplify(fullExpression); - - assertNotNull(result); - assertEquals("0 <= i", result.getValue().toString(), "Equivalent bounds should collapse to a single conjunct"); - - ValDerivationNode expectedLeft = new ValDerivationNode(zeroLeI, null); - ValDerivationNode expectedRight = new ValDerivationNode(iGeZero, null); - ValDerivationNode expected = new ValDerivationNode(zeroLeI, - new BinaryDerivationNode(expectedLeft, expectedRight, "&&")); - - assertDerivationEquals(expected, result, "Equivalent bounds simplification should preserve conjunction origin"); - } - @Test void testIteTrueConditionSimplifiesToThenBranch() { // Given: true ? a : b @@ -1102,47 +1020,78 @@ void testTwoArgAliasWithNormalExpression() { assertNull(rightNode.getOrigin()); } - /** - * Helper method to compare two derivation nodes recursively - */ - private void assertDerivationEquals(DerivationNode expected, DerivationNode actual, String message) { - if (expected == null && actual == null) - return; - - assertNotNull(expected); - assertEquals(expected.getClass(), actual.getClass(), message + ": node types should match"); - if (expected instanceof ValDerivationNode expectedVal) { - ValDerivationNode actualVal = (ValDerivationNode) actual; - assertEquals(expectedVal.getValue().toString(), actualVal.getValue().toString(), - message + ": values should match"); - assertDerivationEquals(expectedVal.getOrigin(), actualVal.getOrigin(), message + " > origin"); - } else if (expected instanceof BinaryDerivationNode expectedBin) { - BinaryDerivationNode actualBin = (BinaryDerivationNode) actual; - assertEquals(expectedBin.getOp(), actualBin.getOp(), message + ": operators should match"); - assertDerivationEquals(expectedBin.getLeft(), actualBin.getLeft(), message + " > left"); - assertDerivationEquals(expectedBin.getRight(), actualBin.getRight(), message + " > right"); - } else if (expected instanceof VarDerivationNode expectedVar) { - VarDerivationNode actualVar = (VarDerivationNode) actual; - assertEquals(expectedVar.getVar(), actualVar.getVar(), message + ": variables should match"); - } else if (expected instanceof UnaryDerivationNode expectedUnary) { - UnaryDerivationNode actualUnary = (UnaryDerivationNode) actual; - assertEquals(expectedUnary.getOp(), actualUnary.getOp(), message + ": operators should match"); - assertDerivationEquals(expectedUnary.getOperand(), actualUnary.getOperand(), message + " > operand"); - } else if (expected instanceof IteDerivationNode expectedIte) { - IteDerivationNode actualIte = (IteDerivationNode) actual; - assertDerivationEquals(expectedIte.getCondition(), actualIte.getCondition(), message + " > condition"); - assertDerivationEquals(expectedIte.getThenBranch(), actualIte.getThenBranch(), message + " > then"); - assertDerivationEquals(expectedIte.getElseBranch(), actualIte.getElseBranch(), message + " > else"); - } + @Test + void testEntailedConjunctIsRemovedButOriginIsPreserved() { + // Given: b >= 100 && b > 0 + // Expected: b >= 100 (b >= 100 implies b > 0) + + addIntVariableToContext("b"); + Expression b = new Var("b"); + Expression bGe100 = new BinaryExpression(b, ">=", new LiteralInt(100)); + Expression bGt0 = new BinaryExpression(b, ">", new LiteralInt(0)); + Expression fullExpression = new BinaryExpression(bGe100, "&&", bGt0); + + ValDerivationNode result = ExpressionSimplifier.simplify(fullExpression); + + assertNotNull(result); + assertEquals("b >= 100", result.getValue().toString(), + "The weaker conjunct should be removed when implied by the stronger one"); + + ValDerivationNode expectedLeft = new ValDerivationNode(bGe100, null); + ValDerivationNode expectedRight = new ValDerivationNode(bGt0, null); + ValDerivationNode expected = new ValDerivationNode(bGe100, + new BinaryDerivationNode(expectedLeft, expectedRight, "&&")); + + assertDerivationEquals(expected, result, "Entailment simplification should preserve conjunction origin"); } - /** - * Helper method to add an integer variable to the context Needed for tests that rely on the SMT-based implication - * checks The simplifier asks Z3 whether one conjunct implies another, so every variable in those expressions must - * be in the context - */ - private void addIntVariableToContext(String name) { - context.addVarToContext(name, factory.Type().INTEGER_PRIMITIVE, new Predicate(), - factory.Code().createCodeSnippetStatement("")); + @Test + void testStrictComparisonImpliesNonStrictComparison() { + // Given: x > y && x >= y + // Expected: x > y (x > y implies x >= y) + + addIntVariableToContext("x"); + addIntVariableToContext("y"); + Expression x = new Var("x"); + Expression y = new Var("y"); + Expression xGtY = new BinaryExpression(x, ">", y); + Expression xGeY = new BinaryExpression(x, ">=", y); + Expression fullExpression = new BinaryExpression(xGtY, "&&", xGeY); + + ValDerivationNode result = ExpressionSimplifier.simplify(fullExpression); + + assertNotNull(result); + assertEquals("x > y", result.getValue().toString(), + "The stricter comparison should be kept when it implies the weaker one"); + + ValDerivationNode expectedLeft = new ValDerivationNode(xGtY, null); + ValDerivationNode expectedRight = new ValDerivationNode(xGeY, null); + ValDerivationNode expected = new ValDerivationNode(xGtY, + new BinaryDerivationNode(expectedLeft, expectedRight, "&&")); + + assertDerivationEquals(expected, result, "Strict comparison simplification should preserve conjunction origin"); + } + + @Test + void testEquivalentBoundsKeepOneSide() { + // Given: i >= 0 && 0 <= i + // Expected: 0 <= i (both conjuncts express the same condition) + addIntVariableToContext("i"); + Expression i = new Var("i"); + Expression zeroLeI = new BinaryExpression(new LiteralInt(0), "<=", i); + Expression iGeZero = new BinaryExpression(i, ">=", new LiteralInt(0)); + Expression fullExpression = new BinaryExpression(zeroLeI, "&&", iGeZero); + + ValDerivationNode result = ExpressionSimplifier.simplify(fullExpression); + + assertNotNull(result); + assertEquals("0 <= i", result.getValue().toString(), "Equivalent bounds should collapse to a single conjunct"); + + ValDerivationNode expectedLeft = new ValDerivationNode(zeroLeI, null); + ValDerivationNode expectedRight = new ValDerivationNode(iGeZero, null); + ValDerivationNode expected = new ValDerivationNode(zeroLeI, + new BinaryDerivationNode(expectedLeft, expectedRight, "&&")); + + assertDerivationEquals(expected, result, "Equivalent bounds simplification should preserve conjunction origin"); } } diff --git a/liquidjava-verifier/src/test/java/liquidjava/utils/TestUtils.java b/liquidjava-verifier/src/test/java/liquidjava/utils/TestUtils.java index cd15f869..628ecc40 100644 --- a/liquidjava-verifier/src/test/java/liquidjava/utils/TestUtils.java +++ b/liquidjava-verifier/src/test/java/liquidjava/utils/TestUtils.java @@ -1,13 +1,30 @@ package liquidjava.utils; +import static org.junit.jupiter.api.Assertions.assertEquals; +import static org.junit.jupiter.api.Assertions.assertNotNull; + import java.io.IOException; import java.nio.file.Files; import java.nio.file.Path; import java.util.Optional; import java.util.stream.Stream; +import liquidjava.processor.context.Context; +import liquidjava.rj_language.Predicate; +import liquidjava.rj_language.opt.derivation_node.BinaryDerivationNode; +import liquidjava.rj_language.opt.derivation_node.DerivationNode; +import liquidjava.rj_language.opt.derivation_node.IteDerivationNode; +import liquidjava.rj_language.opt.derivation_node.UnaryDerivationNode; +import liquidjava.rj_language.opt.derivation_node.ValDerivationNode; +import liquidjava.rj_language.opt.derivation_node.VarDerivationNode; +import spoon.Launcher; +import spoon.reflect.factory.Factory; + public class TestUtils { + private final static Factory factory = new Launcher().getFactory(); + private final static Context context = Context.getInstance(); + /** * Determines if the given path indicates that the test should pass * @@ -64,4 +81,48 @@ public static Optional getExpectedErrorFromDirectory(Path dirPath) { } return Optional.empty(); } + + /** + * Helper method to compare two derivation nodes recursively + */ + public static void assertDerivationEquals(DerivationNode expected, DerivationNode actual, String message) { + if (expected == null && actual == null) + return; + + assertNotNull(expected); + assertEquals(expected.getClass(), actual.getClass(), message + ": node types should match"); + if (expected instanceof ValDerivationNode expectedVal) { + ValDerivationNode actualVal = (ValDerivationNode) actual; + assertEquals(expectedVal.getValue().toString(), actualVal.getValue().toString(), + message + ": values should match"); + assertDerivationEquals(expectedVal.getOrigin(), actualVal.getOrigin(), message + " > origin"); + } else if (expected instanceof BinaryDerivationNode expectedBin) { + BinaryDerivationNode actualBin = (BinaryDerivationNode) actual; + assertEquals(expectedBin.getOp(), actualBin.getOp(), message + ": operators should match"); + assertDerivationEquals(expectedBin.getLeft(), actualBin.getLeft(), message + " > left"); + assertDerivationEquals(expectedBin.getRight(), actualBin.getRight(), message + " > right"); + } else if (expected instanceof VarDerivationNode expectedVar) { + VarDerivationNode actualVar = (VarDerivationNode) actual; + assertEquals(expectedVar.getVar(), actualVar.getVar(), message + ": variables should match"); + } else if (expected instanceof UnaryDerivationNode expectedUnary) { + UnaryDerivationNode actualUnary = (UnaryDerivationNode) actual; + assertEquals(expectedUnary.getOp(), actualUnary.getOp(), message + ": operators should match"); + assertDerivationEquals(expectedUnary.getOperand(), actualUnary.getOperand(), message + " > operand"); + } else if (expected instanceof IteDerivationNode expectedIte) { + IteDerivationNode actualIte = (IteDerivationNode) actual; + assertDerivationEquals(expectedIte.getCondition(), actualIte.getCondition(), message + " > condition"); + assertDerivationEquals(expectedIte.getThenBranch(), actualIte.getThenBranch(), message + " > then"); + assertDerivationEquals(expectedIte.getElseBranch(), actualIte.getElseBranch(), message + " > else"); + } + } + + /** + * Helper method to add an integer variable to the context Needed for tests that rely on the SMT-based implication + * checks The simplifier asks Z3 whether one conjunct implies another, so every variable in those expressions must + * be in the context + */ + public static void addIntVariableToContext(String name) { + context.addVarToContext(name, factory.Type().INTEGER_PRIMITIVE, new Predicate(), + factory.Code().createCodeSnippetStatement("")); + } }