Fix Expression Mutation in ConstantPropagation

Author: rcosta358

liquidjava-verifier/pom.xml

@@ -11,7 +11,7 @@
 
 	<groupId>io.github.liquid-java</groupId>
 	<artifactId>liquidjava-verifier</artifactId>
-	<version>0.0.4</version>
+	<version>0.0.8</version>
 	<name>liquidjava-verifier</name>
 	<description>LiquidJava Verifier</description>
 	<url>https://github.com/liquid-java/liquidjava</url>

liquidjava-verifier/src/main/java/liquidjava/rj_language/opt/ConstantPropagation.java

@@ -44,23 +44,25 @@ private static ValDerivationNode propagateRecursive(Expression exp, Map<String,
         // lift unary origin
         if (exp instanceof UnaryExpression unary) {
             ValDerivationNode operand = propagateRecursive(unary.getChildren().get(0), subs);
-            unary.setChild(0, operand.getValue());
+            UnaryExpression cloned = (UnaryExpression) unary.clone();
+            cloned.setChild(0, operand.getValue());
 
-            DerivationNode origin = operand.getOrigin() != null ? new UnaryDerivationNode(operand, unary.getOp())
+            DerivationNode origin = operand.getOrigin() != null ? new UnaryDerivationNode(operand, cloned.getOp())
                     : null;
-            return new ValDerivationNode(unary, origin);
+            return new ValDerivationNode(cloned, origin);
         }
 
         // lift binary origin
         if (exp instanceof BinaryExpression binary) {
             ValDerivationNode left = propagateRecursive(binary.getFirstOperand(), subs);
             ValDerivationNode right = propagateRecursive(binary.getSecondOperand(), subs);
-            binary.setChild(0, left.getValue());
-            binary.setChild(1, right.getValue());
+            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, binary.getOperator()) : null;
-            return new ValDerivationNode(binary, origin);
+                    ? new BinaryDerivationNode(left, right, cloned.getOperator()) : null;
+            return new ValDerivationNode(cloned, origin);
         }
 
         // recursively propagate children

liquidjava-verifier/src/main/java/liquidjava/rj_language/opt/VariableResolver.java

@@ -13,7 +13,9 @@ public class VariableResolver {
 
     /**
      * Extracts variables with constant values from an expression
+     * 
      * @param exp
+     * 
      * @returns map from variable names to their values
      */
     public static Map<String, Expression> resolve(Expression exp) {
@@ -28,8 +30,10 @@ public static Map<String, Expression> 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<String, Expression> 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<String, Expression> resolveTransitive(Map<String, Expression> map) {
@@ -85,9 +92,11 @@ private static Map<String, Expression> resolveTransitive(Map<String, Expression>
     /**
      * 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<String, Expression> map, Set<String> seen) {

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

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<String, Expression> 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<String, Expression> result = VariableResolver.resolve(conjunction);
+        assertTrue(result.isEmpty(), "Circular dependency should not extract variable mappings");
+    }
 }