From 9761cedb1a58fcc167033af02869cd8de850dd2f Mon Sep 17 00:00:00 2001 From: Ricardo Costa Date: Fri, 21 Nov 2025 15:14:09 +0000 Subject: [PATCH 01/14] Use DerivationNodes in Expected of Refinement Error --- .../liquidjava/diagnostics/errors/RefinementError.java | 10 +++++----- .../processor/refinement_checker/VCChecker.java | 6 +++--- 2 files changed, 8 insertions(+), 8 deletions(-) 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 a2c13c91..4c2d2ff6 100644 --- a/liquidjava-verifier/src/main/java/liquidjava/diagnostics/errors/RefinementError.java +++ b/liquidjava-verifier/src/main/java/liquidjava/diagnostics/errors/RefinementError.java @@ -12,19 +12,19 @@ */ public class RefinementError extends LJError { - private final String expected; + private final ValDerivationNode expected; private final ValDerivationNode found; - public RefinementError(SourcePosition position, Expression expected, ValDerivationNode found, + public RefinementError(SourcePosition position, ValDerivationNode expected, ValDerivationNode found, TranslationTable translationTable) { super("Refinement Error", - String.format("%s is not a subtype of %s", found.getValue(), expected.toSimplifiedString()), position, + String.format("%s is not a subtype of %s", found.getValue(), expected.getValue()), position, translationTable); - this.expected = expected.toSimplifiedString(); + this.expected = expected; this.found = found; } - public String getExpected() { + public ValDerivationNode getExpected() { return expected; } diff --git a/liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/VCChecker.java b/liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/VCChecker.java index 4cad3a80..b3dd6cd7 100644 --- a/liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/VCChecker.java +++ b/liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/VCChecker.java @@ -51,7 +51,7 @@ public void processSubtyping(Predicate expectedType, List list, CtEl premises = premisesBeforeChange.changeStatesToRefinements(filtered, s).changeAliasToRefinement(context, f); et = expectedType.changeStatesToRefinements(filtered, s).changeAliasToRefinement(context, f); } catch (Exception e) { - throw new RefinementError(element.getPosition(), expectedType.getExpression(), premises.simplify(), map); + throw new RefinementError(element.getPosition(), expectedType.simplify(), premises.simplify(), map); } try { @@ -267,7 +267,7 @@ private TranslationTable createMap(Predicate expectedType) { protected void raiseError(Exception e, SourcePosition position, Predicate found, Predicate expected, TranslationTable map) throws LJError { if (e instanceof TypeCheckError) { - throw new RefinementError(position, expected.getExpression(), found.simplify(), map); + throw new RefinementError(position, expected.simplify(), found.simplify(), map); } else if (e instanceof liquidjava.smt.errors.NotFoundError nfe) { throw new NotFoundError(position, e.getMessage(), nfe.getName(), nfe.getKind(), map); } else { @@ -288,7 +288,7 @@ protected void raiseSubtypingError(SourcePosition position, Predicate expected, gatherVariables(found, lrv, mainVars); TranslationTable map = new TranslationTable(); Predicate premises = joinPredicates(expected, mainVars, lrv, map).toConjunctions(); - throw new RefinementError(position, expected.getExpression(), premises.simplify(), map); + throw new RefinementError(position, expected.simplify(), premises.simplify(), map); } protected void raiseSameStateError(SourcePosition position, Predicate expected, String klass) throws LJError { From 921136a54df707cfb1f0f9b1e29ead2e543b9f3b Mon Sep 17 00:00:00 2001 From: Ricardo Costa Date: Fri, 21 Nov 2025 15:28:25 +0000 Subject: [PATCH 02/14] Simplify Until Fixed Point --- .../diagnostics/errors/RefinementError.java | 5 ++- .../rj_language/opt/ExpressionSimplifier.java | 28 +++++++++++++++-- .../opt/ExpressionSimplifierTest.java | 31 ++++++++++++++++++- 3 files changed, 58 insertions(+), 6 deletions(-) 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 4c2d2ff6..93a8a447 100644 --- a/liquidjava-verifier/src/main/java/liquidjava/diagnostics/errors/RefinementError.java +++ b/liquidjava-verifier/src/main/java/liquidjava/diagnostics/errors/RefinementError.java @@ -17,9 +17,8 @@ public class RefinementError extends LJError { public RefinementError(SourcePosition position, ValDerivationNode expected, ValDerivationNode found, TranslationTable translationTable) { - super("Refinement Error", - String.format("%s is not a subtype of %s", found.getValue(), expected.getValue()), position, - translationTable); + super("Refinement Error", String.format("%s is not a subtype of %s", found.getValue(), expected.getValue()), + position, translationTable); this.expected = expected; this.found = found; } 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 4bb4050a..05edc9fd 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 @@ -14,9 +14,33 @@ public class ExpressionSimplifier { * Returns a derivation node representing the tree of simplifications applied */ public static ValDerivationNode simplify(Expression exp) { - ValDerivationNode prop = ConstantPropagation.propagate(exp); + ValDerivationNode fixedPoint = simplifyToFixedPoint(null, null, exp); + return simplifyDerivationTree(fixedPoint); + } + + /** + * Recursively applies propagation and folding until the expression stops changing (fixed point) Stops early if the + * expression simplifies to 'true', which means we've simplified too much + */ + private static ValDerivationNode simplifyToFixedPoint(ValDerivationNode current, ValDerivationNode previous, + Expression prevExp) { + // apply propagation and folding + ValDerivationNode prop = ConstantPropagation.propagate(prevExp); ValDerivationNode fold = ConstantFolding.fold(prop); - return simplifyDerivationTree(fold); + Expression currExp = fold.getValue(); + + // fixed point reached + if (current != null && currExp.equals(current.getValue())) { + return current; + } + + // stop if simplified to 'true' + if (current != null && currExp instanceof LiteralBoolean && currExp.isBooleanTrue()) { + return current; + } + + // continue simplifying + return simplifyToFixedPoint(fold, current, fold.getValue()); } /** 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 ff034f93..15bdbb1a 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 @@ -305,7 +305,7 @@ void testComplexArithmeticWithMultipleOperations() { } @Test - void testSingleEqualityNotSimplifiedToTrue() { + void testSingleEqualityShouldNotSimplify() { // Given: x == 1 // Expected: x == 1 (should not be simplified to "true") @@ -329,6 +329,35 @@ void testSingleEqualityNotSimplifiedToTrue() { assertEquals("1", resultExpr.getSecondOperand().toString(), "Right operand should be 1"); } + @Test + void testFixedPointSimplification() { + // Given: x == -y && y == a / b && a == 6 && b == 3 + // Expected: x == -2 + Expression varX = new Var("x"); + Expression varY = new Var("y"); + Expression varA = new Var("a"); + Expression varB = new Var("b"); + + Expression aDivB = new BinaryExpression(varA, "/", varB); + Expression yEqualsADivB = new BinaryExpression(varY, "==", aDivB); + Expression negY = new UnaryExpression("-", varY); + Expression xEqualsNegY = new BinaryExpression(varX, "==", negY); + Expression six = new LiteralInt(6); + Expression aEquals6 = new BinaryExpression(varA, "==", six); + Expression three = new LiteralInt(3); + Expression bEquals3 = new BinaryExpression(varB, "==", three); + Expression firstAnd = new BinaryExpression(xEqualsNegY, "&&", yEqualsADivB); + Expression secondAnd = new BinaryExpression(aEquals6, "&&", bEquals3); + Expression fullExpression = new BinaryExpression(firstAnd, "&&", secondAnd); + + // When + ValDerivationNode result = ExpressionSimplifier.simplify(fullExpression); + + // Then + assertNotNull(result, "Result should not be null"); + assertEquals("x == -2", result.getValue().toString(), "Expected result to be x == -2"); + } + /** * Helper method to compare two derivation nodes recursively */ From cbb80d5afcd50b33ae9b4c406fe7802e4950532e Mon Sep 17 00:00:00 2001 From: Ricardo Costa Date: Fri, 21 Nov 2025 16:05:48 +0000 Subject: [PATCH 03/14] Fix `VariableResolver` Filter out variables that only appear in their own definition. --- .../rj_language/opt/VariableResolver.java | 52 ++++++++--- .../opt/ExpressionSimplifierTest.java | 92 +++++++++++++++---- .../rj_language/opt/VariableResolverTest.java | 14 +++ 3 files changed, 127 insertions(+), 31 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 b93c78db..2bff9f64 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 @@ -12,25 +12,43 @@ public class VariableResolver { /** - * Extracts variables with constant values from an expression Returns a map from variable names to their values + * Extracts variables with constant values from an expression + * @param exp + * @returns map from variable names to their values */ public static Map resolve(Expression exp) { - // if the expression is just a single equality (not a conjunction) don't extract it - // this avoids creating tautologies like "1 == 1" after substitution, which are then simplified to "true" - if (exp instanceof BinaryExpression be) { - if ("==".equals(be.getOperator())) { - return new HashMap<>(); - } - } - Map map = new HashMap<>(); resolveRecursive(exp, map); + + // filter out variables that only appear in their own definition + map.entrySet().removeIf(entry -> countOccurrences(exp, entry.getKey()) < 2); + return resolveTransitive(map); } + /** + * Counts occurrences of a variable in an expression + * @param exp + * @param varName + * @return number of occurrences + */ + private static int countOccurrences(Expression exp, String varName) { + if (exp instanceof Var var && var.getName().equals(varName)) { + return 1; + } + if (exp instanceof BinaryExpression be) { + return countOccurrences(be.getFirstOperand(), varName) + countOccurrences(be.getSecondOperand(), varName); + } + if (exp.getChildren() != null) { + return exp.getChildren().stream().mapToInt(child -> countOccurrences(child, varName)).sum(); + } + return 0; + } + /** * Recursively extracts variable equalities from an expression (e.g. ... && x == 1 && y == 2 => map: x -> 1, y -> 2) - * Modifies the given map in place + * @param exp + * @param map */ private static void resolveRecursive(Expression exp, Map map) { if (!(exp instanceof BinaryExpression be)) @@ -43,16 +61,18 @@ private static void resolveRecursive(Expression exp, Map map } else if ("==".equals(op)) { Expression left = be.getFirstOperand(); Expression right = be.getSecondOperand(); - if (left instanceof Var && (right.isLiteral() || right instanceof Var)) { - map.put(((Var) left).getName(), right.clone()); - } else if (right instanceof Var && left.isLiteral()) { - map.put(((Var) right).getName(), left.clone()); + if (left instanceof Var var && right.isLiteral()) { + map.put(var.getName(), right.clone()); + } else if (right instanceof Var var && left.isLiteral()) { + map.put(var.getName(), left.clone()); } } } /** * Handles transitive variable equalities in the map (e.g. map: x -> y, y -> 1 => map: x -> 1, y -> 1) + * @param map + * @return new map with resolved values */ private static Map resolveTransitive(Map map) { Map result = new HashMap<>(); @@ -65,6 +85,10 @@ private static Map resolveTransitive(Map /** * Returns the value of a variable by looking up in the map recursively Uses the seen set to avoid circular * references (e.g. x -> y, y -> x) which would cause infinite recursion + * @param exp + * @param map + * @param seen + * @return resolved expression */ private static Expression lookup(Expression exp, Map map, Set seen) { if (!(exp instanceof Var)) 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 15bdbb1a..13253d3e 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 @@ -304,6 +304,35 @@ void testComplexArithmeticWithMultipleOperations() { assertDerivationEquals(expected, result, ""); } + @Test + void testFixedPointSimplification() { + // Given: x == -y && y == a / b && a == 6 && b == 3 + // Expected: x == -2 + Expression varX = new Var("x"); + Expression varY = new Var("y"); + Expression varA = new Var("a"); + Expression varB = new Var("b"); + + Expression aDivB = new BinaryExpression(varA, "/", varB); + Expression yEqualsADivB = new BinaryExpression(varY, "==", aDivB); + Expression negY = new UnaryExpression("-", varY); + Expression xEqualsNegY = new BinaryExpression(varX, "==", negY); + Expression six = new LiteralInt(6); + Expression aEquals6 = new BinaryExpression(varA, "==", six); + Expression three = new LiteralInt(3); + Expression bEquals3 = new BinaryExpression(varB, "==", three); + Expression firstAnd = new BinaryExpression(xEqualsNegY, "&&", yEqualsADivB); + Expression secondAnd = new BinaryExpression(aEquals6, "&&", bEquals3); + Expression fullExpression = new BinaryExpression(firstAnd, "&&", secondAnd); + + // When + ValDerivationNode result = ExpressionSimplifier.simplify(fullExpression); + + // Then + assertNotNull(result, "Result should not be null"); + assertEquals("x == -2", result.getValue().toString(), "Expected result to be x == -2"); + } + @Test void testSingleEqualityShouldNotSimplify() { // Given: x == 1 @@ -330,32 +359,61 @@ void testSingleEqualityShouldNotSimplify() { } @Test - void testFixedPointSimplification() { - // Given: x == -y && y == a / b && a == 6 && b == 3 - // Expected: x == -2 + void testTwoEqualitiesShouldNotSimplify() { + // Given: x == 1 && y == 2 + // Expected: x == 1 && y == 2 (should not be simplified to "true") + Expression varX = new Var("x"); + Expression one = new LiteralInt(1); + Expression xEquals1 = new BinaryExpression(varX, "==", one); + Expression varY = new Var("y"); - Expression varA = new Var("a"); - Expression varB = new Var("b"); + Expression two = new LiteralInt(2); + Expression yEquals2 = new BinaryExpression(varY, "==", two); - Expression aDivB = new BinaryExpression(varA, "/", varB); - Expression yEqualsADivB = new BinaryExpression(varY, "==", aDivB); - Expression negY = new UnaryExpression("-", varY); - Expression xEqualsNegY = new BinaryExpression(varX, "==", negY); - Expression six = new LiteralInt(6); - Expression aEquals6 = new BinaryExpression(varA, "==", six); - Expression three = new LiteralInt(3); - Expression bEquals3 = new BinaryExpression(varB, "==", three); - Expression firstAnd = new BinaryExpression(xEqualsNegY, "&&", yEqualsADivB); - Expression secondAnd = new BinaryExpression(aEquals6, "&&", bEquals3); - Expression fullExpression = new BinaryExpression(firstAnd, "&&", secondAnd); + Expression fullExpression = new BinaryExpression(xEquals1, "&&", yEquals2); // When ValDerivationNode result = ExpressionSimplifier.simplify(fullExpression); // Then assertNotNull(result, "Result should not be null"); - assertEquals("x == -2", result.getValue().toString(), "Expected result to be x == -2"); + assertEquals("x == 1 && y == 2", result.getValue().toString(), + "Two equalities should not be simplified to a boolean literal"); + + // The result should be the original expression unchanged + assertTrue(result.getValue() instanceof BinaryExpression, "Result should still be a binary expression"); + BinaryExpression resultExpr = (BinaryExpression) result.getValue(); + assertEquals("&&", resultExpr.getOperator(), "Operator should still be &&"); + assertEquals("x == 1", resultExpr.getFirstOperand().toString(), "Left operand should be x == 1"); + assertEquals("y == 2", resultExpr.getSecondOperand().toString(), "Right operand should be y == 2"); + } + + @Test + void testCircularDependencyShouldNotSimplify() { + // Given: x == y && y == x + // Expected: x == y && y == x (should not be simplified to "true") + + Expression varX = new Var("x"); + Expression varY = new Var("y"); + Expression xEqualsY = new BinaryExpression(varX, "==", varY); + Expression yEqualsX = new BinaryExpression(varY, "==", varX); + Expression fullExpression = new BinaryExpression(xEqualsY, "&&", yEqualsX); + + // When + ValDerivationNode result = ExpressionSimplifier.simplify(fullExpression); + + // Then + assertNotNull(result, "Result should not be null"); + assertEquals("x == y && y == x", result.getValue().toString(), + "Circular dependency should not be simplified to a boolean literal"); + + // The result should be the original expression unchanged + assertTrue(result.getValue() instanceof BinaryExpression, "Result should still be a binary expression"); + BinaryExpression resultExpr = (BinaryExpression) result.getValue(); + assertEquals("&&", resultExpr.getOperator(), "Operator should still be &&"); + assertEquals("x == y", resultExpr.getFirstOperand().toString(), "Left operand should be x == y"); + assertEquals("y == x", resultExpr.getSecondOperand().toString(), "Right operand should be y == x"); } /** diff --git a/liquidjava-verifier/src/test/java/liquidjava/rj_language/opt/VariableResolverTest.java b/liquidjava-verifier/src/test/java/liquidjava/rj_language/opt/VariableResolverTest.java index 0d08e9a2..a5136e36 100644 --- a/liquidjava-verifier/src/test/java/liquidjava/rj_language/opt/VariableResolverTest.java +++ b/liquidjava-verifier/src/test/java/liquidjava/rj_language/opt/VariableResolverTest.java @@ -107,4 +107,18 @@ void testGroupedEquality() { Map result = VariableResolver.resolve(grouped); assertTrue(result.isEmpty(), "Grouped single equality should not extract variable mapping"); } + + @Test + void testCircularDependency() { + // x == y && y == x should not extract anything due to circular dependency + Expression varX = new Var("x"); + Expression varY = new Var("y"); + + Expression xEqualsY = new BinaryExpression(varX, "==", varY); + Expression yEqualsX = new BinaryExpression(varY, "==", varX); + Expression conjunction = new BinaryExpression(xEqualsY, "&&", yEqualsX); + + Map result = VariableResolver.resolve(conjunction); + assertTrue(result.isEmpty(), "Circular dependency should not extract variable mappings"); + } } From 990ddeb7323f6c634c15e6a93057d0ce9727a1d5 Mon Sep 17 00:00:00 2001 From: Ricardo Costa Date: Fri, 21 Nov 2025 17:31:40 +0000 Subject: [PATCH 04/14] Fix Expression Mutation in `ConstantPropagation` --- liquidjava-verifier/pom.xml | 2 +- .../rj_language/opt/ConstantPropagation.java | 16 +++--- .../rj_language/opt/VariableResolver.java | 9 ++++ .../opt/ExpressionSimplifierTest.java | 51 +++++++++++++++++++ .../rj_language/opt/VariableResolverTest.java | 26 +++++----- 5 files changed, 83 insertions(+), 21 deletions(-) diff --git a/liquidjava-verifier/pom.xml b/liquidjava-verifier/pom.xml index 2461306e..af57236d 100644 --- a/liquidjava-verifier/pom.xml +++ b/liquidjava-verifier/pom.xml @@ -11,7 +11,7 @@ io.github.liquid-java liquidjava-verifier - 0.0.4 + 0.0.8 liquidjava-verifier LiquidJava Verifier https://github.com/liquid-java/liquidjava diff --git a/liquidjava-verifier/src/main/java/liquidjava/rj_language/opt/ConstantPropagation.java b/liquidjava-verifier/src/main/java/liquidjava/rj_language/opt/ConstantPropagation.java index 5c74897f..9853b5c6 100644 --- a/liquidjava-verifier/src/main/java/liquidjava/rj_language/opt/ConstantPropagation.java +++ b/liquidjava-verifier/src/main/java/liquidjava/rj_language/opt/ConstantPropagation.java @@ -44,23 +44,25 @@ private static ValDerivationNode propagateRecursive(Expression exp, Map resolve(Expression exp) { @@ -28,8 +30,10 @@ public static Map resolve(Expression exp) { /** * Counts occurrences of a variable in an expression + * * @param exp * @param varName + * * @return number of occurrences */ private static int countOccurrences(Expression exp, String varName) { @@ -47,6 +51,7 @@ private static int countOccurrences(Expression exp, String varName) { /** * Recursively extracts variable equalities from an expression (e.g. ... && x == 1 && y == 2 => map: x -> 1, y -> 2) + * * @param exp * @param map */ @@ -71,7 +76,9 @@ private static void resolveRecursive(Expression exp, Map map /** * Handles transitive variable equalities in the map (e.g. map: x -> y, y -> 1 => map: x -> 1, y -> 1) + * * @param map + * * @return new map with resolved values */ private static Map resolveTransitive(Map map) { @@ -85,9 +92,11 @@ private static Map resolveTransitive(Map /** * Returns the value of a variable by looking up in the map recursively Uses the seen set to avoid circular * references (e.g. x -> y, y -> x) which would cause infinite recursion + * * @param exp * @param map * @param seen + * * @return resolved expression */ private static Expression lookup(Expression exp, Map map, Set seen) { 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 13253d3e..85951456 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 @@ -416,6 +416,57 @@ void testCircularDependencyShouldNotSimplify() { assertEquals("y == x", resultExpr.getSecondOperand().toString(), "Right operand should be y == x"); } + @Test + void testRealExpression() { + // Given: #a_5 == (-#fresh_4) && #fresh_4 == #x_2 / #y_3 && #x_2 == #x_0 && #x_0 == 6 && #y_3 == #y_1 && #y_1 == + // 3 + // Expected: #a_5 == -2 + Expression varA5 = new Var("#a_5"); + Expression varFresh4 = new Var("#fresh_4"); + Expression varX2 = new Var("#x_2"); + Expression varY3 = new Var("#y_3"); + Expression varX0 = new Var("#x_0"); + Expression varY1 = new Var("#y_1"); + Expression six = new LiteralInt(6); + Expression three = new LiteralInt(3); + Expression fresh4EqualsX2DivY3 = new BinaryExpression(varFresh4, "==", new BinaryExpression(varX2, "/", varY3)); + Expression x2EqualsX0 = new BinaryExpression(varX2, "==", varX0); + Expression x0Equals6 = new BinaryExpression(varX0, "==", six); + Expression y3EqualsY1 = new BinaryExpression(varY3, "==", varY1); + Expression y1Equals3 = new BinaryExpression(varY1, "==", three); + Expression negFresh4 = new UnaryExpression("-", varFresh4); + Expression a5EqualsNegFresh4 = new BinaryExpression(varA5, "==", negFresh4); + Expression firstAnd = new BinaryExpression(a5EqualsNegFresh4, "&&", fresh4EqualsX2DivY3); + Expression secondAnd = new BinaryExpression(x2EqualsX0, "&&", x0Equals6); + Expression thirdAnd = new BinaryExpression(y3EqualsY1, "&&", y1Equals3); + Expression firstBigAnd = new BinaryExpression(firstAnd, "&&", secondAnd); + Expression fullExpression = new BinaryExpression(firstBigAnd, "&&", thirdAnd); + // When + ValDerivationNode result = ExpressionSimplifier.simplify(fullExpression); + // Then + assertNotNull(result, "Result should not be null"); + assertEquals("#a_5 == -2", result.getValue().toString(), "Expected result to be #a_5 == -2"); + + } + + @Test + void testTransitive() { + // Given: a == b && b == 1 + // Expected: a == 1 + Expression varA = new Var("a"); + Expression varB = new Var("b"); + Expression one = new LiteralInt(1); + Expression aEqualsB = new BinaryExpression(varA, "==", varB); + Expression bEquals1 = new BinaryExpression(varB, "==", one); + Expression fullExpression = new BinaryExpression(aEqualsB, "&&", bEquals1); + // When + ValDerivationNode result = ExpressionSimplifier.simplify(fullExpression); + // Then + assertNotNull(result, "Result should not be null"); + assertEquals("a == 1", result.getValue().toString(), "Expected result to be a == 1"); + + } + /** * Helper method to compare two derivation nodes recursively */ diff --git a/liquidjava-verifier/src/test/java/liquidjava/rj_language/opt/VariableResolverTest.java b/liquidjava-verifier/src/test/java/liquidjava/rj_language/opt/VariableResolverTest.java index a5136e36..bd0dee0d 100644 --- a/liquidjava-verifier/src/test/java/liquidjava/rj_language/opt/VariableResolverTest.java +++ b/liquidjava-verifier/src/test/java/liquidjava/rj_language/opt/VariableResolverTest.java @@ -108,17 +108,17 @@ void testGroupedEquality() { assertTrue(result.isEmpty(), "Grouped single equality should not extract variable mapping"); } - @Test - void testCircularDependency() { - // x == y && y == x should not extract anything due to circular dependency - Expression varX = new Var("x"); - Expression varY = new Var("y"); - - Expression xEqualsY = new BinaryExpression(varX, "==", varY); - Expression yEqualsX = new BinaryExpression(varY, "==", varX); - Expression conjunction = new BinaryExpression(xEqualsY, "&&", yEqualsX); - - Map result = VariableResolver.resolve(conjunction); - assertTrue(result.isEmpty(), "Circular dependency should not extract variable mappings"); - } + @Test + void testCircularDependency() { + // x == y && y == x should not extract anything due to circular dependency + Expression varX = new Var("x"); + Expression varY = new Var("y"); + + Expression xEqualsY = new BinaryExpression(varX, "==", varY); + Expression yEqualsX = new BinaryExpression(varY, "==", varX); + Expression conjunction = new BinaryExpression(xEqualsY, "&&", yEqualsX); + + Map result = VariableResolver.resolve(conjunction); + assertTrue(result.isEmpty(), "Circular dependency should not extract variable mappings"); + } } From 0ab2f69ace5b2468b5d7791fa0d56c0f381c5b2c Mon Sep 17 00:00:00 2001 From: Ricardo Costa Date: Fri, 21 Nov 2025 20:52:44 +0000 Subject: [PATCH 05/14] Remove Oversimplification Check --- .../liquidjava/rj_language/opt/ExpressionSimplifier.java | 5 ----- 1 file changed, 5 deletions(-) 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 05edc9fd..7e1b8c05 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 @@ -34,11 +34,6 @@ private static ValDerivationNode simplifyToFixedPoint(ValDerivationNode current, return current; } - // stop if simplified to 'true' - if (current != null && currExp instanceof LiteralBoolean && currExp.isBooleanTrue()) { - return current; - } - // continue simplifying return simplifyToFixedPoint(fold, current, fold.getValue()); } From edc622090178197071591c7df5ffac8e1932d660 Mon Sep 17 00:00:00 2001 From: Ricardo Costa Date: Sun, 23 Nov 2025 14:00:08 +0000 Subject: [PATCH 06/14] Fix Variable Resolution & Expression Simplification - Ignore unused variable equalities in VariableResolver, only extracts the variables actually used in the expression (excluding its own definitions) - Improves ExpressionSimplifier by collapsing duplicate conjuctions (e.g. x && x => x) --- .../rj_language/opt/ExpressionSimplifier.java | 39 +++++++----- .../rj_language/opt/VariableResolver.java | 63 ++++++++++++------- .../opt/ExpressionSimplifierTest.java | 57 +++++++++++++++++ .../rj_language/opt/VariableResolverTest.java | 22 +++++++ 4 files changed, 144 insertions(+), 37 deletions(-) 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 7e1b8c05..5ff23e0d 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 @@ -46,23 +46,34 @@ private static ValDerivationNode simplifyDerivationTree(ValDerivationNode node) DerivationNode origin = node.getOrigin(); // binary expression with && - if (value instanceof BinaryExpression binExp) { - if ("&&".equals(binExp.getOperator()) && origin instanceof BinaryDerivationNode binOrigin) { - // recursively simplify children - ValDerivationNode leftSimplified = simplifyDerivationTree(binOrigin.getLeft()); - ValDerivationNode rightSimplified = simplifyDerivationTree(binOrigin.getRight()); + if (value instanceof BinaryExpression binExp && "&&".equals(binExp.getOperator())) { + ValDerivationNode leftSimplified; + ValDerivationNode rightSimplified; - // check if either side is redundant - if (isRedundant(leftSimplified.getValue())) - return rightSimplified; - if (isRedundant(rightSimplified.getValue())) - return leftSimplified; + // simplify children + if (origin instanceof BinaryDerivationNode binOrigin) { + leftSimplified = simplifyDerivationTree(binOrigin.getLeft()); + rightSimplified = simplifyDerivationTree(binOrigin.getRight()); + } else { + leftSimplified = simplifyDerivationTree(new ValDerivationNode(binExp.getFirstOperand(), null)); + rightSimplified = simplifyDerivationTree(new ValDerivationNode(binExp.getSecondOperand(), null)); + } + + // check if either side is redundant + if (isRedundant(leftSimplified.getValue())) + return rightSimplified; + if (isRedundant(rightSimplified.getValue())) + return leftSimplified; - // return the conjunction with simplified children - Expression newValue = new BinaryExpression(leftSimplified.getValue(), "&&", rightSimplified.getValue()); - DerivationNode newOrigin = new BinaryDerivationNode(leftSimplified, rightSimplified, "&&"); - return new ValDerivationNode(newValue, newOrigin); + // check if children are equal (x && x => x) + if (leftSimplified.getValue().toString().equals(rightSimplified.getValue().toString())) { + return leftSimplified; } + + // return the conjunction with simplified children + Expression newValue = new BinaryExpression(leftSimplified.getValue(), "&&", rightSimplified.getValue()); + DerivationNode newOrigin = new BinaryDerivationNode(leftSimplified, rightSimplified, "&&"); + return new ValDerivationNode(newValue, newOrigin); } // no simplification return node; 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 fa4b63b0..9d5850e6 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 @@ -20,35 +20,17 @@ public class VariableResolver { */ public static Map resolve(Expression exp) { Map map = new HashMap<>(); + + // extract variable equalities recursively resolveRecursive(exp, map); - // filter out variables that only appear in their own definition - map.entrySet().removeIf(entry -> countOccurrences(exp, entry.getKey()) < 2); + // remove variables that were not used in the expression + map.entrySet().removeIf(entry -> !hasUsage(exp, entry.getKey())); + // transitively resolve variables return resolveTransitive(map); } - /** - * Counts occurrences of a variable in an expression - * - * @param exp - * @param varName - * - * @return number of occurrences - */ - private static int countOccurrences(Expression exp, String varName) { - if (exp instanceof Var var && var.getName().equals(varName)) { - return 1; - } - if (exp instanceof BinaryExpression be) { - return countOccurrences(be.getFirstOperand(), varName) + countOccurrences(be.getSecondOperand(), varName); - } - if (exp.getChildren() != null) { - return exp.getChildren().stream().mapToInt(child -> countOccurrences(child, varName)).sum(); - } - return 0; - } - /** * Recursively extracts variable equalities from an expression (e.g. ... && x == 1 && y == 2 => map: x -> 1, y -> 2) * @@ -114,4 +96,39 @@ private static Expression lookup(Expression exp, Map map, Se seen.add(name); return lookup(value, map, seen); } + + /** + * Checks if a variable is used in the expression (excluding its own definitions) + * + * @param exp + * @param name + * + * @return true if used, false otherwise + */ + private static boolean hasUsage(Expression exp, String name) { + // exclude own definitions + if (exp instanceof BinaryExpression binary && "==".equals(binary.getOperator())) { + Expression left = binary.getFirstOperand(); + Expression right = binary.getSecondOperand(); + if (left instanceof Var v && v.getName().equals(name) && right.isLiteral()) + return false; + if (right instanceof Var v && v.getName().equals(name) && left.isLiteral()) + return false; + } + + // usage found + if (exp instanceof Var var && var.getName().equals(name)) { + return true; + } + + // recurse children + if (exp.hasChildren()) { + for (Expression child : exp.getChildren()) + if (hasUsage(child, name)) + return true; + } + + // usage not found + return false; + } } \ No newline at end of file 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 85951456..4e515108 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,8 +2,11 @@ import static org.junit.jupiter.api.Assertions.*; +import java.util.ArrayList; + import liquidjava.rj_language.ast.BinaryExpression; import liquidjava.rj_language.ast.Expression; +import liquidjava.rj_language.ast.FunctionInvocation; import liquidjava.rj_language.ast.LiteralBoolean; import liquidjava.rj_language.ast.LiteralInt; import liquidjava.rj_language.ast.UnaryExpression; @@ -389,6 +392,60 @@ void testTwoEqualitiesShouldNotSimplify() { assertEquals("y == 2", resultExpr.getSecondOperand().toString(), "Right operand should be y == 2"); } + @Test + void testSameVarTwiceShouldSimplifyToSingle() { + // Given: x && x + // Expected: x + Expression varX = new Var("x"); + Expression fullExpression = new BinaryExpression(varX, "&&", varX); + // When + ValDerivationNode result = ExpressionSimplifier.simplify(fullExpression); + // Then + assertNotNull(result, "Result should not be null"); + assertEquals("x", result.getValue().toString(), + "Same variable twice should be simplified to a single variable"); + } + + @Test + void testSameEqualityTwiceShouldSimplifyToSingle() { + // Given: x == 1 && x == 1 + // Expected: x == 1 + Expression varX = new Var("x"); + Expression one = new LiteralInt(1); + Expression xEquals1First = new BinaryExpression(varX, "==", one); + Expression xEquals1Second = new BinaryExpression(varX, "==", one); + Expression fullExpression = new BinaryExpression(xEquals1First, "&&", xEquals1Second); + + // When + ValDerivationNode result = ExpressionSimplifier.simplify(fullExpression); + + // Then + assertNotNull(result, "Result should not be null"); + assertEquals("x == 1", result.getValue().toString(), + "Same equality twice should be simplified to a single equality"); + } + + @Test + void testSameExpressionTwiceShouldSimplifyToSingle() { + // Given: a + b == 1 && a + b == 1 + // Expected: a + b == 1 + Expression varA = new Var("a"); + Expression varB = new Var("b"); + Expression sum = new BinaryExpression(varA, "+", varB); + Expression one = new LiteralInt(1); + Expression sumEquals3First = new BinaryExpression(sum, "==", one); + Expression sumEquals3Second = new BinaryExpression(sum, "==", one); + Expression fullExpression = new BinaryExpression(sumEquals3First, "&&", sumEquals3Second); + + // When + ValDerivationNode result = ExpressionSimplifier.simplify(fullExpression); + + // Then + assertNotNull(result, "Result should not be null"); + assertEquals("a + b == 1", result.getValue().toString(), + "Same expression twice should be simplified to a single equality"); + } + @Test void testCircularDependencyShouldNotSimplify() { // Given: x == y && y == x diff --git a/liquidjava-verifier/src/test/java/liquidjava/rj_language/opt/VariableResolverTest.java b/liquidjava-verifier/src/test/java/liquidjava/rj_language/opt/VariableResolverTest.java index bd0dee0d..97c1beb3 100644 --- a/liquidjava-verifier/src/test/java/liquidjava/rj_language/opt/VariableResolverTest.java +++ b/liquidjava-verifier/src/test/java/liquidjava/rj_language/opt/VariableResolverTest.java @@ -12,6 +12,7 @@ import liquidjava.rj_language.ast.LiteralInt; import liquidjava.rj_language.ast.UnaryExpression; import liquidjava.rj_language.ast.Var; +import org.junit.jupiter.api.TestTemplate; class VariableResolverTest { @@ -121,4 +122,25 @@ void testCircularDependency() { Map result = VariableResolver.resolve(conjunction); assertTrue(result.isEmpty(), "Circular dependency should not extract variable mappings"); } + + @Test + void testUnusedEqualitiesShouldBeIgnored() { + // z > 0 && x == 1 && y == 2 && z == 3 + Expression varX = new Var("x"); + Expression varY = new Var("y"); + Expression varZ = new Var("z"); + Expression one = new LiteralInt(1); + Expression two = new LiteralInt(2); + Expression three = new LiteralInt(3); + Expression zero = new LiteralInt(0); + Expression zGreaterZero = new BinaryExpression(varZ, ">", zero); + Expression xEquals1 = new BinaryExpression(varX, "==", one); + Expression yEquals2 = new BinaryExpression(varY, "==", two); + Expression zEquals3 = new BinaryExpression(varZ, "==", three); + Expression conditions = new BinaryExpression(xEquals1, "&&", new BinaryExpression(yEquals2, "&&", zEquals3)); + Expression fullExpr = new BinaryExpression(zGreaterZero, "&&", conditions); + Map result = VariableResolver.resolve(fullExpr); + assertEquals(1, result.size(), "Should only extract used variable z"); + assertEquals("3", result.get("z").toString()); + } } From cba9719fafa75de895788b71fdd862996b8429e0 Mon Sep 17 00:00:00 2001 From: Ricardo Costa Date: Sun, 23 Nov 2025 14:11:27 +0000 Subject: [PATCH 07/14] Cleanup Tests --- .../opt/ExpressionSimplifierTest.java | 45 ++++++++++--------- .../rj_language/opt/VariableResolverTest.java | 1 - 2 files changed, 24 insertions(+), 22 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 4e515108..bf9b5315 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,11 +2,8 @@ import static org.junit.jupiter.api.Assertions.*; -import java.util.ArrayList; - import liquidjava.rj_language.ast.BinaryExpression; import liquidjava.rj_language.ast.Expression; -import liquidjava.rj_language.ast.FunctionInvocation; import liquidjava.rj_language.ast.LiteralBoolean; import liquidjava.rj_language.ast.LiteralInt; import liquidjava.rj_language.ast.UnaryExpression; @@ -113,7 +110,7 @@ void testSimpleComparison() { // Then assertNotNull(result, "Result should not be null"); - assertTrue(result.getValue() instanceof LiteralBoolean, "Result should be a boolean"); + assertInstanceOf(LiteralBoolean.class, result.getValue(), "Result should be a boolean"); assertFalse(((LiteralBoolean) result.getValue()).isBooleanTrue(), "Expected result to befalse"); // (y || true) && y == false => false || true = true @@ -249,8 +246,8 @@ void testComplexArithmeticWithMultipleOperations() { // Then assertNotNull(result, "Result should not be null"); assertNotNull(result.getValue(), "Result value should not be null"); - assertTrue(result.getValue() instanceof LiteralBoolean, "Result should be a boolean literal"); - assertTrue(((LiteralBoolean) result.getValue()).isBooleanTrue(), "Expected result to be true"); + assertInstanceOf(LiteralBoolean.class, result.getValue(), "Result should be a boolean literal"); + assertTrue(result.getValue().isBooleanTrue(), "Expected result to be true"); // 5 * 2 + 7 - 3 ValDerivationNode val5 = new ValDerivationNode(new LiteralInt(5), new VarDerivationNode("a")); @@ -311,6 +308,7 @@ void testComplexArithmeticWithMultipleOperations() { void testFixedPointSimplification() { // Given: x == -y && y == a / b && a == 6 && b == 3 // Expected: x == -2 + Expression varX = new Var("x"); Expression varY = new Var("y"); Expression varA = new Var("a"); @@ -354,7 +352,7 @@ void testSingleEqualityShouldNotSimplify() { "Single equality should not be simplified to a boolean literal"); // The result should be the original expression unchanged - assertTrue(result.getValue() instanceof BinaryExpression, "Result should still be a binary expression"); + assertInstanceOf(BinaryExpression.class, result.getValue(), "Result should still be a binary expression"); BinaryExpression resultExpr = (BinaryExpression) result.getValue(); assertEquals("==", resultExpr.getOperator(), "Operator should still be =="); assertEquals("x", resultExpr.getFirstOperand().toString(), "Left operand should be x"); @@ -373,7 +371,6 @@ void testTwoEqualitiesShouldNotSimplify() { Expression varY = new Var("y"); Expression two = new LiteralInt(2); Expression yEquals2 = new BinaryExpression(varY, "==", two); - Expression fullExpression = new BinaryExpression(xEquals1, "&&", yEquals2); // When @@ -385,7 +382,7 @@ void testTwoEqualitiesShouldNotSimplify() { "Two equalities should not be simplified to a boolean literal"); // The result should be the original expression unchanged - assertTrue(result.getValue() instanceof BinaryExpression, "Result should still be a binary expression"); + assertInstanceOf(BinaryExpression.class, result.getValue(), "Result should still be a binary expression"); BinaryExpression resultExpr = (BinaryExpression) result.getValue(); assertEquals("&&", resultExpr.getOperator(), "Operator should still be &&"); assertEquals("x == 1", resultExpr.getFirstOperand().toString(), "Left operand should be x == 1"); @@ -396,11 +393,14 @@ void testTwoEqualitiesShouldNotSimplify() { void testSameVarTwiceShouldSimplifyToSingle() { // Given: x && x // Expected: x + Expression varX = new Var("x"); Expression fullExpression = new BinaryExpression(varX, "&&", varX); // When + ValDerivationNode result = ExpressionSimplifier.simplify(fullExpression); // Then + assertNotNull(result, "Result should not be null"); assertEquals("x", result.getValue().toString(), "Same variable twice should be simplified to a single variable"); @@ -410,6 +410,7 @@ void testSameVarTwiceShouldSimplifyToSingle() { void testSameEqualityTwiceShouldSimplifyToSingle() { // Given: x == 1 && x == 1 // Expected: x == 1 + Expression varX = new Var("x"); Expression one = new LiteralInt(1); Expression xEquals1First = new BinaryExpression(varX, "==", one); @@ -429,6 +430,7 @@ void testSameEqualityTwiceShouldSimplifyToSingle() { void testSameExpressionTwiceShouldSimplifyToSingle() { // Given: a + b == 1 && a + b == 1 // Expected: a + b == 1 + Expression varA = new Var("a"); Expression varB = new Var("b"); Expression sum = new BinaryExpression(varA, "+", varB); @@ -466,7 +468,7 @@ void testCircularDependencyShouldNotSimplify() { "Circular dependency should not be simplified to a boolean literal"); // The result should be the original expression unchanged - assertTrue(result.getValue() instanceof BinaryExpression, "Result should still be a binary expression"); + assertInstanceOf(BinaryExpression.class, result.getValue(), "Result should still be a binary expression"); BinaryExpression resultExpr = (BinaryExpression) result.getValue(); assertEquals("&&", resultExpr.getOperator(), "Operator should still be &&"); assertEquals("x == y", resultExpr.getFirstOperand().toString(), "Left operand should be x == y"); @@ -475,9 +477,9 @@ void testCircularDependencyShouldNotSimplify() { @Test void testRealExpression() { - // Given: #a_5 == (-#fresh_4) && #fresh_4 == #x_2 / #y_3 && #x_2 == #x_0 && #x_0 == 6 && #y_3 == #y_1 && #y_1 == - // 3 + // Given: #a_5 == -#fresh_4 && #fresh_4 == #x_2 / #y_3 && #x_2 == #x_0 && #x_0 == 6 && #y_3 == #y_1 && #y_1 == 3 // Expected: #a_5 == -2 + Expression varA5 = new Var("#a_5"); Expression varFresh4 = new Var("#fresh_4"); Expression varX2 = new Var("#x_2"); @@ -498,8 +500,10 @@ void testRealExpression() { Expression thirdAnd = new BinaryExpression(y3EqualsY1, "&&", y1Equals3); Expression firstBigAnd = new BinaryExpression(firstAnd, "&&", secondAnd); Expression fullExpression = new BinaryExpression(firstBigAnd, "&&", thirdAnd); + // When ValDerivationNode result = ExpressionSimplifier.simplify(fullExpression); + // Then assertNotNull(result, "Result should not be null"); assertEquals("#a_5 == -2", result.getValue().toString(), "Expected result to be #a_5 == -2"); @@ -510,18 +514,20 @@ void testRealExpression() { void testTransitive() { // Given: a == b && b == 1 // Expected: a == 1 + Expression varA = new Var("a"); Expression varB = new Var("b"); Expression one = new LiteralInt(1); Expression aEqualsB = new BinaryExpression(varA, "==", varB); Expression bEquals1 = new BinaryExpression(varB, "==", one); Expression fullExpression = new BinaryExpression(aEqualsB, "&&", bEquals1); + // When ValDerivationNode result = ExpressionSimplifier.simplify(fullExpression); + // Then assertNotNull(result, "Result should not be null"); assertEquals("a == 1", result.getValue().toString(), "Expected result to be a == 1"); - } /** @@ -531,25 +537,22 @@ private void assertDerivationEquals(DerivationNode expected, DerivationNode actu if (expected == null && actual == null) return; + assertNotNull(expected); assertEquals(expected.getClass(), actual.getClass(), message + ": node types should match"); - if (expected instanceof ValDerivationNode) { - ValDerivationNode expectedVal = (ValDerivationNode) expected; + 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) { - BinaryDerivationNode expectedBin = (BinaryDerivationNode) expected; + } 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) { - VarDerivationNode expectedVar = (VarDerivationNode) expected; + } else if (expected instanceof VarDerivationNode expectedVar) { VarDerivationNode actualVar = (VarDerivationNode) actual; assertEquals(expectedVar.getVar(), actualVar.getVar(), message + ": variables should match"); - } else if (expected instanceof UnaryDerivationNode) { - UnaryDerivationNode expectedUnary = (UnaryDerivationNode) expected; + } 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"); diff --git a/liquidjava-verifier/src/test/java/liquidjava/rj_language/opt/VariableResolverTest.java b/liquidjava-verifier/src/test/java/liquidjava/rj_language/opt/VariableResolverTest.java index 97c1beb3..6f799aa2 100644 --- a/liquidjava-verifier/src/test/java/liquidjava/rj_language/opt/VariableResolverTest.java +++ b/liquidjava-verifier/src/test/java/liquidjava/rj_language/opt/VariableResolverTest.java @@ -12,7 +12,6 @@ import liquidjava.rj_language.ast.LiteralInt; import liquidjava.rj_language.ast.UnaryExpression; import liquidjava.rj_language.ast.Var; -import org.junit.jupiter.api.TestTemplate; class VariableResolverTest { From b592ef5a75d559b956a380ad5cbb147104c8f7f7 Mon Sep 17 00:00:00 2001 From: Ricardo Costa Date: Sun, 23 Nov 2025 15:07:05 +0000 Subject: [PATCH 08/14] Fix Losing Previous Simplification Nodes on Multiple Passes Fixed by tracking previous origins in constant propagation --- .../rj_language/opt/ConstantPropagation.java | 25 +++++----- .../rj_language/opt/ExpressionSimplifier.java | 49 +++++++++++++++---- .../opt/ExpressionSimplifierTest.java | 41 +++++++++++++++- 3 files changed, 92 insertions(+), 23 deletions(-) diff --git a/liquidjava-verifier/src/main/java/liquidjava/rj_language/opt/ConstantPropagation.java b/liquidjava-verifier/src/main/java/liquidjava/rj_language/opt/ConstantPropagation.java index 9853b5c6..05887b12 100644 --- a/liquidjava-verifier/src/main/java/liquidjava/rj_language/opt/ConstantPropagation.java +++ b/liquidjava-verifier/src/main/java/liquidjava/rj_language/opt/ConstantPropagation.java @@ -19,15 +19,16 @@ public class ConstantPropagation { * VariableResolver to extract variable equalities from the expression first. Returns a derivation node representing * the propagation steps taken. */ - public static ValDerivationNode propagate(Expression exp) { + public static ValDerivationNode propagate(Expression exp, DerivationNode defaultOrigin) { Map substitutions = VariableResolver.resolve(exp); - return propagateRecursive(exp, substitutions); + return propagateRecursive(exp, substitutions, defaultOrigin); } /** * Recursively performs constant propagation on an expression (e.g. x + y && x == 1 && y == 2 => 1 + 2) */ - private static ValDerivationNode propagateRecursive(Expression exp, Map subs) { + private static ValDerivationNode propagateRecursive(Expression exp, Map subs, + DerivationNode defaultOrigin) { // substitute variable if (exp instanceof Var var) { @@ -38,30 +39,30 @@ private static ValDerivationNode propagateRecursive(Expression exp, Map x) + // collapse identical sides (x && x => x) if (leftSimplified.getValue().toString().equals(rightSimplified.getValue().toString())) { return leftSimplified; } @@ -75,10 +75,41 @@ private static ValDerivationNode simplifyDerivationTree(ValDerivationNode node) DerivationNode newOrigin = new BinaryDerivationNode(leftSimplified, rightSimplified, "&&"); return new ValDerivationNode(newValue, newOrigin); } + + // simplify origin + DerivationNode simplifiedOrigin = simplifyDerivationNode(origin); + if (simplifiedOrigin != origin) { + return new ValDerivationNode(value, simplifiedOrigin); + } + // no simplification return node; } + private static DerivationNode simplifyDerivationNode(DerivationNode node) { + if (node == null) + return null; + if (node instanceof ValDerivationNode val) { + return simplifyValDerivationNode(val); + } + if (node instanceof BinaryDerivationNode binary) { + ValDerivationNode left = simplifyValDerivationNode(binary.getLeft()); + ValDerivationNode right = simplifyValDerivationNode(binary.getRight()); + if (left != binary.getLeft() || right != binary.getRight()) { + return new BinaryDerivationNode(left, right, binary.getOp()); + } + return binary; + } + if (node instanceof UnaryDerivationNode unary) { + ValDerivationNode operand = simplifyValDerivationNode(unary.getOperand()); + if (operand != unary.getOperand()) { + return new UnaryDerivationNode(operand, unary.getOp()); + } + return unary; + } + return node; + } + /** * Checks if an expression is redundant (e.g. true or x == x) */ 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 bf9b5315..d886695d 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 @@ -308,7 +308,6 @@ void testComplexArithmeticWithMultipleOperations() { void testFixedPointSimplification() { // Given: x == -y && y == a / b && a == 6 && b == 3 // Expected: x == -2 - Expression varX = new Var("x"); Expression varY = new Var("y"); Expression varA = new Var("a"); @@ -332,6 +331,44 @@ void testFixedPointSimplification() { // Then assertNotNull(result, "Result should not be null"); assertEquals("x == -2", result.getValue().toString(), "Expected result to be x == -2"); + + // Compare derivation tree structure + + // Origin of y (value 2) - right operand of result + ValDerivationNode originY = new ValDerivationNode(new LiteralInt(2), new VarDerivationNode("y")); + UnaryDerivationNode originNeg2 = new UnaryDerivationNode(originY, "-"); + ValDerivationNode rightNode = new ValDerivationNode(new LiteralInt(-2), originNeg2); + + // Origin of x - left operand of result + // 6 (from a) / 3 (from b) -> 2 + ValDerivationNode val6 = new ValDerivationNode(new LiteralInt(6), new VarDerivationNode("a")); + ValDerivationNode val3 = new ValDerivationNode(new LiteralInt(3), new VarDerivationNode("b")); + BinaryDerivationNode divOp = new BinaryDerivationNode(val6, val3, "/"); + ValDerivationNode val2FromDiv = new ValDerivationNode(new LiteralInt(2), divOp); + + // y == 2 (from y == 6 / 3) + ValDerivationNode valYNode = new ValDerivationNode(new Var("y"), null); + BinaryDerivationNode eqYOp = new BinaryDerivationNode(valYNode, val2FromDiv, "=="); + ValDerivationNode yEq2 = new ValDerivationNode(new BinaryExpression(new Var("y"), "==", new LiteralInt(2)), + eqYOp); + + // x == -y + ValDerivationNode xEqNegY = new ValDerivationNode( + new BinaryExpression(new Var("x"), "==", new UnaryExpression("-", new Var("y"))), null); + + // x == -y && y == 2 + BinaryDerivationNode andOp1 = new BinaryDerivationNode(xEqNegY, yEq2, "&&"); + ValDerivationNode xEqNegYAndYEq2 = new ValDerivationNode( + new BinaryExpression(xEqNegY.getValue(), "&&", yEq2.getValue()), andOp1); + + // Left node x has origin pointing to the previous simplification's tree + ValDerivationNode leftNode = new ValDerivationNode(new Var("x"), xEqNegYAndYEq2); + + // Root equality + BinaryDerivationNode rootOrigin = new BinaryDerivationNode(leftNode, rightNode, "=="); + ValDerivationNode expected = new ValDerivationNode(result.getValue(), rootOrigin); + + assertDerivationEquals(expected, result, "Derivation tree structure"); } @Test @@ -447,7 +484,7 @@ void testSameExpressionTwiceShouldSimplifyToSingle() { assertEquals("a + b == 1", result.getValue().toString(), "Same expression twice should be simplified to a single equality"); } - + @Test void testCircularDependencyShouldNotSimplify() { // Given: x == y && y == x From 3f38abc8e623e24a20cd1b79dd6ab2b5a5ef4542 Mon Sep 17 00:00:00 2001 From: Ricardo Costa Date: Sun, 23 Nov 2025 15:18:53 +0000 Subject: [PATCH 09/14] Code Refactoring --- .../rj_language/opt/ExpressionSimplifier.java | 36 ++----------------- .../opt/ExpressionSimplifierTest.java | 1 + 2 files changed, 4 insertions(+), 33 deletions(-) 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 295d25f8..ab47f1d9 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 @@ -28,7 +28,8 @@ private static ValDerivationNode simplifyToFixedPoint(ValDerivationNode current, // apply propagation and folding ValDerivationNode prop = ConstantPropagation.propagate(prevExp, current); ValDerivationNode fold = ConstantFolding.fold(prop); - Expression currExp = fold.getValue(); + ValDerivationNode simplified = simplifyValDerivationNode(fold); + Expression currExp = simplified.getValue(); // fixed point reached if (current != null && currExp.equals(current.getValue())) { @@ -36,7 +37,7 @@ private static ValDerivationNode simplifyToFixedPoint(ValDerivationNode current, } // continue simplifying - return simplifyToFixedPoint(fold, current, fold.getValue()); + return simplifyToFixedPoint(simplified, current, simplified.getValue()); } /** @@ -75,41 +76,10 @@ private static ValDerivationNode simplifyValDerivationNode(ValDerivationNode nod DerivationNode newOrigin = new BinaryDerivationNode(leftSimplified, rightSimplified, "&&"); return new ValDerivationNode(newValue, newOrigin); } - - // simplify origin - DerivationNode simplifiedOrigin = simplifyDerivationNode(origin); - if (simplifiedOrigin != origin) { - return new ValDerivationNode(value, simplifiedOrigin); - } - // no simplification return node; } - private static DerivationNode simplifyDerivationNode(DerivationNode node) { - if (node == null) - return null; - if (node instanceof ValDerivationNode val) { - return simplifyValDerivationNode(val); - } - if (node instanceof BinaryDerivationNode binary) { - ValDerivationNode left = simplifyValDerivationNode(binary.getLeft()); - ValDerivationNode right = simplifyValDerivationNode(binary.getRight()); - if (left != binary.getLeft() || right != binary.getRight()) { - return new BinaryDerivationNode(left, right, binary.getOp()); - } - return binary; - } - if (node instanceof UnaryDerivationNode unary) { - ValDerivationNode operand = simplifyValDerivationNode(unary.getOperand()); - if (operand != unary.getOperand()) { - return new UnaryDerivationNode(operand, unary.getOp()); - } - return unary; - } - return node; - } - /** * Checks if an expression is redundant (e.g. true or x == x) */ 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 d886695d..2c0d6ff3 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 @@ -308,6 +308,7 @@ void testComplexArithmeticWithMultipleOperations() { void testFixedPointSimplification() { // Given: x == -y && y == a / b && a == 6 && b == 3 // Expected: x == -2 + Expression varX = new Var("x"); Expression varY = new Var("y"); Expression varA = new Var("a"); From 79ca87d1cc6c397b92546850138e2ebd15bd7a38 Mon Sep 17 00:00:00 2001 From: Ricardo Costa Date: Sun, 23 Nov 2025 15:20:54 +0000 Subject: [PATCH 10/14] Cleanup --- .../liquidjava/rj_language/opt/ExpressionSimplifier.java | 8 +++----- .../rj_language/opt/ExpressionSimplifierTest.java | 2 +- 2 files changed, 4 insertions(+), 6 deletions(-) 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 ab47f1d9..4b5aa99c 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 @@ -5,7 +5,6 @@ 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.UnaryDerivationNode; import liquidjava.rj_language.opt.derivation_node.ValDerivationNode; public class ExpressionSimplifier { @@ -15,7 +14,7 @@ public class ExpressionSimplifier { * Returns a derivation node representing the tree of simplifications applied */ public static ValDerivationNode simplify(Expression exp) { - ValDerivationNode fixedPoint = simplifyToFixedPoint(null, null, exp); + ValDerivationNode fixedPoint = simplifyToFixedPoint(null, exp); return simplifyValDerivationNode(fixedPoint); } @@ -23,8 +22,7 @@ public static ValDerivationNode simplify(Expression exp) { * Recursively applies propagation and folding until the expression stops changing (fixed point) Stops early if the * expression simplifies to 'true', which means we've simplified too much */ - private static ValDerivationNode simplifyToFixedPoint(ValDerivationNode current, ValDerivationNode previous, - Expression prevExp) { + private static ValDerivationNode simplifyToFixedPoint(ValDerivationNode current, Expression prevExp) { // apply propagation and folding ValDerivationNode prop = ConstantPropagation.propagate(prevExp, current); ValDerivationNode fold = ConstantFolding.fold(prop); @@ -37,7 +35,7 @@ private static ValDerivationNode simplifyToFixedPoint(ValDerivationNode current, } // continue simplifying - return simplifyToFixedPoint(simplified, current, simplified.getValue()); + return simplifyToFixedPoint(simplified, simplified.getValue()); } /** 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 2c0d6ff3..bae1b60e 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 @@ -308,7 +308,7 @@ void testComplexArithmeticWithMultipleOperations() { void testFixedPointSimplification() { // Given: x == -y && y == a / b && a == 6 && b == 3 // Expected: x == -2 - + Expression varX = new Var("x"); Expression varY = new Var("y"); Expression varA = new Var("a"); From 8db7a47cca6873433b7934f8cc16bacf5ef9bb34 Mon Sep 17 00:00:00 2001 From: Ricardo Costa Date: Sun, 23 Nov 2025 16:00:52 +0000 Subject: [PATCH 11/14] Simplify Symmetric Equalities --- .../rj_language/opt/ExpressionSimplifier.java | 20 ++++++++++++++++++- .../opt/ExpressionSimplifierTest.java | 15 ++++---------- 2 files changed, 23 insertions(+), 12 deletions(-) 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 4b5aa99c..2e43e326 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 @@ -65,7 +65,12 @@ private static ValDerivationNode simplifyValDerivationNode(ValDerivationNode nod return leftSimplified; // collapse identical sides (x && x => x) - if (leftSimplified.getValue().toString().equals(rightSimplified.getValue().toString())) { + if (leftSimplified.getValue().equals(rightSimplified.getValue())) { + return leftSimplified; + } + + // collapse symmetric equalities (e.g. x == y && y == x => x == y) + if (isSymmetricEquality(leftSimplified.getValue(), rightSimplified.getValue())) { return leftSimplified; } @@ -78,6 +83,19 @@ private static ValDerivationNode simplifyValDerivationNode(ValDerivationNode nod return node; } + private static boolean isSymmetricEquality(Expression left, Expression right) { + if (left instanceof BinaryExpression b1 && "==".equals(b1.getOperator()) && right instanceof BinaryExpression b2 + && "==".equals(b2.getOperator())) { + + Expression l1 = b1.getFirstOperand(); + Expression r1 = b1.getSecondOperand(); + Expression l2 = b2.getFirstOperand(); + Expression r2 = b2.getSecondOperand(); + return l1.equals(r2) && r1.equals(l2); + } + return false; + } + /** * Checks if an expression is redundant (e.g. true or x == x) */ 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 bae1b60e..6f5bd722 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 @@ -487,9 +487,9 @@ void testSameExpressionTwiceShouldSimplifyToSingle() { } @Test - void testCircularDependencyShouldNotSimplify() { + void testSymmetricEqualityShouldSimplify() { // Given: x == y && y == x - // Expected: x == y && y == x (should not be simplified to "true") + // Expected: x == y Expression varX = new Var("x"); Expression varY = new Var("y"); @@ -502,15 +502,8 @@ void testCircularDependencyShouldNotSimplify() { // Then assertNotNull(result, "Result should not be null"); - assertEquals("x == y && y == x", result.getValue().toString(), - "Circular dependency should not be simplified to a boolean literal"); - - // The result should be the original expression unchanged - assertInstanceOf(BinaryExpression.class, result.getValue(), "Result should still be a binary expression"); - BinaryExpression resultExpr = (BinaryExpression) result.getValue(); - assertEquals("&&", resultExpr.getOperator(), "Operator should still be &&"); - assertEquals("x == y", resultExpr.getFirstOperand().toString(), "Left operand should be x == y"); - assertEquals("y == x", resultExpr.getSecondOperand().toString(), "Right operand should be y == x"); + assertEquals("x == y", result.getValue().toString(), + "Symmetric equality should be simplified to a single equality"); } @Test From 176f866924756781428f748a38e6330aa72ad357 Mon Sep 17 00:00:00 2001 From: Ricardo Costa Date: Sat, 29 Nov 2025 17:04:46 +0000 Subject: [PATCH 12/14] Fix Derivation Across Multiple Passes Variable nodes should have origin nodes so when expressions are simplified in multiple passes, previous simplifications are preserved --- .../rj_language/opt/ConstantPropagation.java | 95 +++++++++++++++---- .../derivation_node/VarDerivationNode.java | 11 +++ .../opt/ExpressionSimplifierTest.java | 45 ++++----- 3 files changed, 105 insertions(+), 46 deletions(-) diff --git a/liquidjava-verifier/src/main/java/liquidjava/rj_language/opt/ConstantPropagation.java b/liquidjava-verifier/src/main/java/liquidjava/rj_language/opt/ConstantPropagation.java index 05887b12..fee2b2c4 100644 --- a/liquidjava-verifier/src/main/java/liquidjava/rj_language/opt/ConstantPropagation.java +++ b/liquidjava-verifier/src/main/java/liquidjava/rj_language/opt/ConstantPropagation.java @@ -10,6 +10,7 @@ import liquidjava.rj_language.opt.derivation_node.ValDerivationNode; import liquidjava.rj_language.opt.derivation_node.VarDerivationNode; +import java.util.HashMap; import java.util.Map; public class ConstantPropagation { @@ -19,64 +20,122 @@ public class ConstantPropagation { * VariableResolver to extract variable equalities from the expression first. Returns a derivation node representing * the propagation steps taken. */ - public static ValDerivationNode propagate(Expression exp, DerivationNode defaultOrigin) { + public static ValDerivationNode propagate(Expression exp, ValDerivationNode previousOrigin) { Map substitutions = VariableResolver.resolve(exp); - return propagateRecursive(exp, substitutions, defaultOrigin); + + // map of variable origins from the previous derivation tree + Map varOrigins = new HashMap<>(); + if (previousOrigin != null) { + extractVarOrigins(previousOrigin, varOrigins); + } + return propagateRecursive(exp, substitutions, varOrigins); } /** * Recursively performs constant propagation on an expression (e.g. x + y && x == 1 && y == 2 => 1 + 2) */ private static ValDerivationNode propagateRecursive(Expression exp, Map subs, - DerivationNode defaultOrigin) { + Map varOrigins) { // substitute variable if (exp instanceof Var var) { String name = var.getName(); Expression value = subs.get(name); // substitution - if (value != null) - return new ValDerivationNode(value.clone(), new VarDerivationNode(name)); + if (value != null) { + // check if this variable has an origin from a previous pass + DerivationNode previousOrigin = varOrigins.get(name); + + // preserve origin if value came from previous derivation + DerivationNode origin = previousOrigin != null ? new VarDerivationNode(name, previousOrigin) : new VarDerivationNode(name); + return new ValDerivationNode(value.clone(), origin); + } // no substitution - return new ValDerivationNode(var, defaultOrigin); + return new ValDerivationNode(var, null); } // lift unary origin if (exp instanceof UnaryExpression unary) { - ValDerivationNode operand = propagateRecursive(unary.getChildren().get(0), subs, defaultOrigin); + ValDerivationNode operand = propagateRecursive(unary.getChildren().get(0), subs, varOrigins); UnaryExpression cloned = (UnaryExpression) unary.clone(); cloned.setChild(0, operand.getValue()); - DerivationNode origin = operand.getOrigin() != null ? new UnaryDerivationNode(operand, cloned.getOp()) - : defaultOrigin; - return new ValDerivationNode(cloned, origin); + return operand.getOrigin() != null + ? new ValDerivationNode(cloned, new UnaryDerivationNode(operand, cloned.getOp())) + : new ValDerivationNode(cloned, null); } // lift binary origin if (exp instanceof BinaryExpression binary) { - ValDerivationNode left = propagateRecursive(binary.getFirstOperand(), subs, defaultOrigin); - ValDerivationNode right = propagateRecursive(binary.getSecondOperand(), subs, defaultOrigin); + ValDerivationNode left = propagateRecursive(binary.getFirstOperand(), subs, varOrigins); + ValDerivationNode right = propagateRecursive(binary.getSecondOperand(), subs, varOrigins); BinaryExpression cloned = (BinaryExpression) binary.clone(); cloned.setChild(0, left.getValue()); cloned.setChild(1, right.getValue()); - DerivationNode origin = (left.getOrigin() != null || right.getOrigin() != null) - ? new BinaryDerivationNode(left, right, cloned.getOperator()) : defaultOrigin; - return new ValDerivationNode(cloned, origin); + return (left.getOrigin() != null || right.getOrigin() != null) + ? new ValDerivationNode(cloned, new BinaryDerivationNode(left, right, cloned.getOperator())) + : new ValDerivationNode(cloned, null); } // recursively propagate children if (exp.hasChildren()) { Expression propagated = exp.clone(); for (int i = 0; i < exp.getChildren().size(); i++) { - ValDerivationNode child = propagateRecursive(exp.getChildren().get(i), subs, defaultOrigin); + ValDerivationNode child = propagateRecursive(exp.getChildren().get(i), subs, varOrigins); propagated.setChild(i, child.getValue()); } - return new ValDerivationNode(propagated, defaultOrigin); + return new ValDerivationNode(propagated, null); } // no propagation - return new ValDerivationNode(exp, defaultOrigin); + return new ValDerivationNode(exp, null); + } + + + /** + * Extracts the derivation nodes for variable values from the derivation tree + * This is so done so when we find "var == value" in the tree, we store the derivation of the value + * So it can be preserved when var is substituted in subsequent passes + */ + private static void extractVarOrigins(ValDerivationNode node, Map varOrigins) { + if (node == null) + return; + + Expression value = node.getValue(); + DerivationNode origin = node.getOrigin(); + + // check for equality expressions + if (value instanceof BinaryExpression binExp && "==".equals(binExp.getOperator()) + && origin instanceof BinaryDerivationNode binOrigin) { + Expression left = binExp.getFirstOperand(); + Expression right = binExp.getSecondOperand(); + + // extract variable name and value derivation from either side + String varName = null; + ValDerivationNode valueDerivation = null; + + if (left instanceof Var var && right.isLiteral()) { + varName = var.getName(); + valueDerivation = binOrigin.getRight(); + } else if (right instanceof Var var && left.isLiteral()) { + varName = var.getName(); + valueDerivation = binOrigin.getLeft(); + } + if (varName != null && valueDerivation != null && valueDerivation.getOrigin() != null) { + varOrigins.put(varName, valueDerivation.getOrigin()); + } + } + + // recursively process the origin tree + if (origin instanceof BinaryDerivationNode binOrigin) { + extractVarOrigins(binOrigin.getLeft(), varOrigins); + extractVarOrigins(binOrigin.getRight(), varOrigins); + } else if (origin instanceof UnaryDerivationNode unaryOrigin) { + extractVarOrigins(unaryOrigin.getOperand(), varOrigins); + } else if (origin instanceof ValDerivationNode valOrigin) { + extractVarOrigins(valOrigin, varOrigins); + } } } \ No newline at end of file diff --git a/liquidjava-verifier/src/main/java/liquidjava/rj_language/opt/derivation_node/VarDerivationNode.java b/liquidjava-verifier/src/main/java/liquidjava/rj_language/opt/derivation_node/VarDerivationNode.java index 1c044f52..c134a44e 100644 --- a/liquidjava-verifier/src/main/java/liquidjava/rj_language/opt/derivation_node/VarDerivationNode.java +++ b/liquidjava-verifier/src/main/java/liquidjava/rj_language/opt/derivation_node/VarDerivationNode.java @@ -3,12 +3,23 @@ public class VarDerivationNode extends DerivationNode { private final String var; + private final DerivationNode origin; public VarDerivationNode(String var) { this.var = var; + this.origin = null; + } + + public VarDerivationNode(String var, DerivationNode origin) { + this.var = var; + this.origin = origin; } public String getVar() { return var; } + + public DerivationNode getOrigin() { + return origin; + } } 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 6f5bd722..b49ce805 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 @@ -335,35 +335,24 @@ void testFixedPointSimplification() { // Compare derivation tree structure - // Origin of y (value 2) - right operand of result - ValDerivationNode originY = new ValDerivationNode(new LiteralInt(2), new VarDerivationNode("y")); - UnaryDerivationNode originNeg2 = new UnaryDerivationNode(originY, "-"); - ValDerivationNode rightNode = new ValDerivationNode(new LiteralInt(-2), originNeg2); + // Build the derivation chain for the right side: + // 6 came from a, 3 came from b + ValDerivationNode val6FromA = new ValDerivationNode(new LiteralInt(6), new VarDerivationNode("a")); + ValDerivationNode val3FromB = new ValDerivationNode(new LiteralInt(3), new VarDerivationNode("b")); - // Origin of x - left operand of result - // 6 (from a) / 3 (from b) -> 2 - ValDerivationNode val6 = new ValDerivationNode(new LiteralInt(6), new VarDerivationNode("a")); - ValDerivationNode val3 = new ValDerivationNode(new LiteralInt(3), new VarDerivationNode("b")); - BinaryDerivationNode divOp = new BinaryDerivationNode(val6, val3, "/"); - ValDerivationNode val2FromDiv = new ValDerivationNode(new LiteralInt(2), divOp); - - // y == 2 (from y == 6 / 3) - ValDerivationNode valYNode = new ValDerivationNode(new Var("y"), null); - BinaryDerivationNode eqYOp = new BinaryDerivationNode(valYNode, val2FromDiv, "=="); - ValDerivationNode yEq2 = new ValDerivationNode(new BinaryExpression(new Var("y"), "==", new LiteralInt(2)), - eqYOp); - - // x == -y - ValDerivationNode xEqNegY = new ValDerivationNode( - new BinaryExpression(new Var("x"), "==", new UnaryExpression("-", new Var("y"))), null); - - // x == -y && y == 2 - BinaryDerivationNode andOp1 = new BinaryDerivationNode(xEqNegY, yEq2, "&&"); - ValDerivationNode xEqNegYAndYEq2 = new ValDerivationNode( - new BinaryExpression(xEqNegY.getValue(), "&&", yEq2.getValue()), andOp1); - - // Left node x has origin pointing to the previous simplification's tree - ValDerivationNode leftNode = new ValDerivationNode(new Var("x"), xEqNegYAndYEq2); + // 6 / 3 -> 2 + BinaryDerivationNode divOrigin = new BinaryDerivationNode(val6FromA, val3FromB, "/"); + + // 2 came from y, and y's value came from 6 / 2 + VarDerivationNode yChainedOrigin = new VarDerivationNode("y", divOrigin); + ValDerivationNode val2FromY = new ValDerivationNode(new LiteralInt(2), yChainedOrigin); + + // -2 + UnaryDerivationNode negOrigin = new UnaryDerivationNode(val2FromY, "-"); + ValDerivationNode rightNode = new ValDerivationNode(new LiteralInt(-2), negOrigin); + + // Left node x has no origin + ValDerivationNode leftNode = new ValDerivationNode(new Var("x"), null); // Root equality BinaryDerivationNode rootOrigin = new BinaryDerivationNode(leftNode, rightNode, "=="); From 53a05342921ba1ee1fd43134a7b3997b11f2a2c6 Mon Sep 17 00:00:00 2001 From: Ricardo Costa Date: Sat, 29 Nov 2025 17:05:14 +0000 Subject: [PATCH 13/14] Formatting --- .../rj_language/opt/ConstantPropagation.java | 12 ++++++------ 1 file changed, 6 insertions(+), 6 deletions(-) diff --git a/liquidjava-verifier/src/main/java/liquidjava/rj_language/opt/ConstantPropagation.java b/liquidjava-verifier/src/main/java/liquidjava/rj_language/opt/ConstantPropagation.java index fee2b2c4..5cc0562e 100644 --- a/liquidjava-verifier/src/main/java/liquidjava/rj_language/opt/ConstantPropagation.java +++ b/liquidjava-verifier/src/main/java/liquidjava/rj_language/opt/ConstantPropagation.java @@ -45,9 +45,10 @@ private static ValDerivationNode propagateRecursive(Expression exp, Map varOrigins) { if (node == null) From 50cf074d3eb6655d24a32c935f6c648e060a2569 Mon Sep 17 00:00:00 2001 From: Ricardo Costa Date: Thu, 4 Dec 2025 20:47:47 +0000 Subject: [PATCH 14/14] Fix Merge --- .../liquidjava/processor/refinement_checker/VCChecker.java | 6 +++--- .../main/java/liquidjava/rj_language/ast/Expression.java | 2 +- 2 files changed, 4 insertions(+), 4 deletions(-) diff --git a/liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/VCChecker.java b/liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/VCChecker.java index 3df794ac..0c2fba5e 100644 --- a/liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/VCChecker.java +++ b/liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/VCChecker.java @@ -52,8 +52,8 @@ public void processSubtyping(Predicate expectedType, List list, CtEl } boolean isSubtype = smtChecks(expected, premises, element.getPosition()); if (!isSubtype) - throw new RefinementError(element.getPosition(), expectedType.getExpression(), - premisesBeforeChange.simplify(), map); + throw new RefinementError(element.getPosition(), expectedType.simplify(), premisesBeforeChange.simplify(), + map); } /** @@ -263,7 +263,7 @@ protected void throwRefinementError(SourcePosition position, Predicate expected, gatherVariables(found, lrv, mainVars); TranslationTable map = new TranslationTable(); Predicate premises = joinPredicates(expected, mainVars, lrv, map).toConjunctions(); - throw new RefinementError(position, expected.getExpression(), premises.simplify(), map); + throw new RefinementError(position, expected.simplify(), premises.simplify(), map); } protected void throwStateRefinementError(SourcePosition position, Predicate found, Predicate expected) diff --git a/liquidjava-verifier/src/main/java/liquidjava/rj_language/ast/Expression.java b/liquidjava-verifier/src/main/java/liquidjava/rj_language/ast/Expression.java index fac053e6..5449949b 100644 --- a/liquidjava-verifier/src/main/java/liquidjava/rj_language/ast/Expression.java +++ b/liquidjava-verifier/src/main/java/liquidjava/rj_language/ast/Expression.java @@ -271,7 +271,7 @@ public void validateGhostInvocations(Context ctx, Factory f) throws LJError { if (this instanceof FunctionInvocation fi) { // get all ghosts with the matching name List candidates = ctx.getGhosts().stream().filter(g -> g.matches(fi.name)).toList(); - if (candidates.isEmpty()) + if (candidates.isEmpty()) return; // not found error is thrown elsewhere // find matching overload