From 0d5b026dad448278dc016c62e2e31c43ac74f655 Mon Sep 17 00:00:00 2001 From: Ricardo Costa Date: Tue, 17 Mar 2026 11:34:57 +0000 Subject: [PATCH] Fix Misleading Expansions --- .../java/liquidjava/rj_language/ast/Var.java | 4 +++ .../rj_language/opt/ConstantFolding.java | 12 +++++-- .../rj_language/opt/ExpressionSimplifier.java | 8 +++-- .../opt/ExpressionSimplifierTest.java | 33 +++++++++++++++---- 4 files changed, 45 insertions(+), 12 deletions(-) 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..fab196bc 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,8 @@ public boolean equals(Object obj) { return name.equals(other.name); } } + + public boolean isInternal() { + return name.startsWith("#"); + } } diff --git a/liquidjava-verifier/src/main/java/liquidjava/rj_language/opt/ConstantFolding.java b/liquidjava-verifier/src/main/java/liquidjava/rj_language/opt/ConstantFolding.java index b52f8eb7..3a6200c4 100644 --- a/liquidjava-verifier/src/main/java/liquidjava/rj_language/opt/ConstantFolding.java +++ b/liquidjava-verifier/src/main/java/liquidjava/rj_language/opt/ConstantFolding.java @@ -172,18 +172,24 @@ private static ValDerivationNode foldUnary(ValDerivationNode node) { // !true => false, !false => true boolean value = operand.isBooleanTrue(); Expression res = new LiteralBoolean(!value); - return new ValDerivationNode(res, new UnaryDerivationNode(operandNode, operator)); + DerivationNode origin = operandNode.getOrigin() != null ? new UnaryDerivationNode(operandNode, operator) + : null; + return new ValDerivationNode(res, origin); } // unary minus if ("-".equals(operator)) { // -(x) => -x if (operand instanceof LiteralInt) { Expression res = new LiteralInt(-((LiteralInt) operand).getValue()); - return new ValDerivationNode(res, new UnaryDerivationNode(operandNode, operator)); + DerivationNode origin = operandNode.getOrigin() != null ? new UnaryDerivationNode(operandNode, operator) + : null; + return new ValDerivationNode(res, origin); } if (operand instanceof LiteralReal) { Expression res = new LiteralReal(-((LiteralReal) operand).getValue()); - return new ValDerivationNode(res, new UnaryDerivationNode(operandNode, operator)); + DerivationNode origin = operandNode.getOrigin() != null ? new UnaryDerivationNode(operandNode, operator) + : null; + return new ValDerivationNode(res, origin); } } 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 da99efac..26ce9f0b 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 @@ -81,8 +81,12 @@ private static ValDerivationNode simplifyValDerivationNode(ValDerivationNode nod // 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); + // only create origin if at least one child has a meaningful origin + if (leftSimplified.getOrigin() != null || rightSimplified.getOrigin() != null) { + DerivationNode newOrigin = new BinaryDerivationNode(leftSimplified, rightSimplified, "&&"); + return new ValDerivationNode(newValue, newOrigin); + } + return new ValDerivationNode(newValue, null); } // no simplification return node; 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 a51b824e..981e877e 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 @@ -120,9 +120,7 @@ void testSimpleComparison() { ValDerivationNode trueFromOr = new ValDerivationNode(new LiteralBoolean(true), orFalseTrue); // !true = false - ValDerivationNode valTrue2 = new ValDerivationNode(new LiteralBoolean(true), null); - UnaryDerivationNode notOp = new UnaryDerivationNode(valTrue2, "!"); - ValDerivationNode falseFromNot = new ValDerivationNode(new LiteralBoolean(false), notOp); + ValDerivationNode falseFromNot = new ValDerivationNode(new LiteralBoolean(false), null); // true && false = false BinaryDerivationNode andTrueFalse = new BinaryDerivationNode(trueFromOr, falseFromNot, "&&"); @@ -187,10 +185,8 @@ void testArithmeticWithConstants() { BinaryDerivationNode div6By2 = new BinaryDerivationNode(val6, val2, "/"); ValDerivationNode val3 = new ValDerivationNode(new LiteralInt(3), div6By2); - // -5 from unary negation of 5 - ValDerivationNode val5 = new ValDerivationNode(new LiteralInt(5), null); - UnaryDerivationNode unaryNeg5 = new UnaryDerivationNode(val5, "-"); - ValDerivationNode valNeg5 = new ValDerivationNode(new LiteralInt(-5), unaryNeg5); + // -5 is a literal with no origin + ValDerivationNode valNeg5 = new ValDerivationNode(new LiteralInt(-5), null); // 3 + (-5) = -2 BinaryDerivationNode add3AndNeg5 = new BinaryDerivationNode(val3, valNeg5, "+"); @@ -580,6 +576,29 @@ void testShouldNotOversimplifyToTrue() { "Should stop simplification before collapsing to true"); } + @Test + void testNoSimplificationHasNoOrigin() { + // Given: x > 0 && y >= -128 && y <= 127 + // Expected: same expression with no origin (nothing to simplify) + + Expression varX = new Var("x"); + Expression varY = new Var("y"); + Expression xGreater0 = new BinaryExpression(varX, ">", new LiteralInt(0)); + Expression yGeMinus128 = new BinaryExpression(varY, ">=", new UnaryExpression("-", new LiteralInt(128))); + Expression yLe127 = new BinaryExpression(varY, "<=", new LiteralInt(127)); + Expression firstAnd = new BinaryExpression(xGreater0, "&&", yGeMinus128); + Expression fullExpression = new BinaryExpression(firstAnd, "&&", yLe127); + + // When + ValDerivationNode result = ExpressionSimplifier.simplify(fullExpression); + + // Then + assertNotNull(result, "Result should not be null"); + assertEquals("x > 0 && y >= -128 && y <= 127", result.getValue().toString(), + "Expression should remain unchanged"); + assertNull(result.getOrigin(), "No origin should be present when nothing was simplified"); + } + /** * Helper method to compare two derivation nodes recursively */