Fix Misleading Expansions

Author: rcosta358

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("#");
+    }
 }

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);
             }
         }
 

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;

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
      */