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

@@ -76,8 +76,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, "+");