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 80e654c5ba9f3e7f6cf287b7820852cf4abc1089 Mon Sep 17 00:00:00 2001 From: Ricardo Costa Date: Sat, 28 Mar 2026 14:25:57 +0000 Subject: [PATCH 6/7] Rename Classes --- .../{ConstantFolding.java => ExpressionFolding.java} | 10 +++++----- .../rj_language/opt/ExpressionSimplifier.java | 4 ++-- ...nstantPropagation.java => VariablePropagation.java} | 10 +++++----- .../test/java/liquidjava/api/tests/TestExamples.java | 2 +- 4 files changed, 13 insertions(+), 13 deletions(-) rename liquidjava-verifier/src/main/java/liquidjava/rj_language/opt/{ConstantFolding.java => ExpressionFolding.java} (95%) rename liquidjava-verifier/src/main/java/liquidjava/rj_language/opt/{ConstantPropagation.java => VariablePropagation.java} (93%) diff --git a/liquidjava-verifier/src/main/java/liquidjava/rj_language/opt/ConstantFolding.java b/liquidjava-verifier/src/main/java/liquidjava/rj_language/opt/ExpressionFolding.java similarity index 95% rename from liquidjava-verifier/src/main/java/liquidjava/rj_language/opt/ConstantFolding.java rename to liquidjava-verifier/src/main/java/liquidjava/rj_language/opt/ExpressionFolding.java index 3a6200c4..f3ab6c1c 100644 --- a/liquidjava-verifier/src/main/java/liquidjava/rj_language/opt/ConstantFolding.java +++ b/liquidjava-verifier/src/main/java/liquidjava/rj_language/opt/ExpressionFolding.java @@ -12,11 +12,11 @@ import liquidjava.rj_language.opt.derivation_node.UnaryDerivationNode; import liquidjava.rj_language.opt.derivation_node.ValDerivationNode; -public class ConstantFolding { +public class ExpressionFolding { /** - * Performs constant folding on a derivation node by evaluating nodes with constant values. Returns a new derivation - * node representing the folding steps taken + * Performs expression folding on a derivation node by evaluating nodes when possible. Returns a new derivation node + * representing the folding steps taken */ public static ValDerivationNode fold(ValDerivationNode node) { Expression exp = node.getValue(); @@ -35,7 +35,7 @@ public static ValDerivationNode fold(ValDerivationNode node) { } /** - * Folds a binary expression node if both children are constant values (e.g. 1 + 2 => 3) + * Folds a binary expression node (e.g. 1 + 2 => 3) */ private static ValDerivationNode foldBinary(ValDerivationNode node) { BinaryExpression binExp = (BinaryExpression) node.getValue(); @@ -148,7 +148,7 @@ else if (left instanceof LiteralBoolean && right instanceof LiteralBoolean) { } /** - * Folds a unary expression node if the child (operand) is a constant value (e.g. !true => false) + * Folds a unary expression node (e.g. !true => false) */ private static ValDerivationNode foldUnary(ValDerivationNode node) { UnaryExpression unaryExp = (UnaryExpression) node.getValue(); 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 fd70ec60..fd29d8c8 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 @@ -27,8 +27,8 @@ public static ValDerivationNode simplify(Expression exp) { */ private static ValDerivationNode simplifyToFixedPoint(ValDerivationNode current, Expression prevExp) { // apply propagation and folding - ValDerivationNode prop = ConstantPropagation.propagate(prevExp, current); - ValDerivationNode fold = ConstantFolding.fold(prop); + ValDerivationNode prop = VariablePropagation.propagate(prevExp, current); + ValDerivationNode fold = ExpressionFolding.fold(prop); ValDerivationNode simplified = simplifyValDerivationNode(fold); Expression currExp = simplified.getValue(); diff --git a/liquidjava-verifier/src/main/java/liquidjava/rj_language/opt/ConstantPropagation.java b/liquidjava-verifier/src/main/java/liquidjava/rj_language/opt/VariablePropagation.java similarity index 93% rename from liquidjava-verifier/src/main/java/liquidjava/rj_language/opt/ConstantPropagation.java rename to liquidjava-verifier/src/main/java/liquidjava/rj_language/opt/VariablePropagation.java index 5cc0562e..af7e7d07 100644 --- a/liquidjava-verifier/src/main/java/liquidjava/rj_language/opt/ConstantPropagation.java +++ b/liquidjava-verifier/src/main/java/liquidjava/rj_language/opt/VariablePropagation.java @@ -13,12 +13,12 @@ import java.util.HashMap; import java.util.Map; -public class ConstantPropagation { +public class VariablePropagation { /** - * Performs constant propagation on an expression, by substituting variables with their constant values. Uses the - * VariableResolver to extract variable equalities from the expression first. Returns a derivation node representing - * the propagation steps taken. + * Performs constant and variable propagation on an expression, by substituting variables. Uses the VariableResolver + * to extract variable equalities from the expression first. Returns a derivation node representing the propagation + * steps taken. */ public static ValDerivationNode propagate(Expression exp, ValDerivationNode previousOrigin) { Map substitutions = VariableResolver.resolve(exp); @@ -32,7 +32,7 @@ public static ValDerivationNode propagate(Expression exp, ValDerivationNode prev } /** - * Recursively performs constant propagation on an expression (e.g. x + y && x == 1 && y == 2 => 1 + 2) + * Recursively performs propagation on an expression (e.g. x + y && x == 1 && y == 2 => 1 + 2) */ private static ValDerivationNode propagateRecursive(Expression exp, Map subs, Map varOrigins) { diff --git a/liquidjava-verifier/src/test/java/liquidjava/api/tests/TestExamples.java b/liquidjava-verifier/src/test/java/liquidjava/api/tests/TestExamples.java index 0f3552e8..e90588e3 100644 --- a/liquidjava-verifier/src/test/java/liquidjava/api/tests/TestExamples.java +++ b/liquidjava-verifier/src/test/java/liquidjava/api/tests/TestExamples.java @@ -11,8 +11,8 @@ import java.util.stream.Stream; import liquidjava.api.CommandLineLauncher; import liquidjava.diagnostics.Diagnostics; +import liquidjava.diagnostics.errors.*; -import liquidjava.diagnostics.errors.LJError; import org.junit.Test; import org.junit.jupiter.params.ParameterizedTest; import org.junit.jupiter.params.provider.MethodSource; From 8925be8c1630430c0afc1cb20dc925c6218e9a14 Mon Sep 17 00:00:00 2001 From: Ricardo Costa Date: Sat, 28 Mar 2026 14:30:49 +0000 Subject: [PATCH 7/7] Fix Merge --- .../liquidjava/rj_language/opt/ExpressionSimplifierTest.java | 1 + 1 file changed, 1 insertion(+) 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 e33bbbfb..546479c6 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 @@ -552,6 +552,7 @@ void testTransitive() { assertEquals("a == 1", result.getValue().toString(), "Expected result to be a == 1"); } + @Test void testShouldNotOversimplifyToTrue() { // Given: x > 5 && x == y && y == 10 // Iteration 1: resolves y == 10, substitutes y -> 10: x > 5 && x == 10