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 2e43e326..c506741c 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 @@ -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; diff --git a/liquidjava-verifier/src/test/java/liquidjava/rj_language/opt/ExpressionSimplifierTest.java b/liquidjava-verifier/src/test/java/liquidjava/rj_language/opt/ExpressionSimplifierTest.java index b49ce805..6d353ff5 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, "+");