Special Variable Substitution

liquidjava-verifier/src/main/java/liquidjava/rj_language/ast/Var.java

@@ -70,15 +70,4 @@ public boolean equals(Object obj) {
             return name.equals(other.name);
         }
     }
-
-    public boolean isInternal() {
-        return name.startsWith("#");
-    }
-
-    public int getCounter() {
-        if (!isInternal())
-            throw new IllegalStateException("Cannot get counter of non-internal variable");
-        int lastUnderscore = name.lastIndexOf('_');
-        return Integer.parseInt(name.substring(lastUnderscore + 1));
-    }
 }

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

@@ -54,16 +54,17 @@ private static void resolveRecursive(Expression exp, Map<String, Expression> map
                 map.put(var.getName(), left.clone());
             } else if (left instanceof Var leftVar && right instanceof Var rightVar) {
                 // to substitute internal variable with user-facing variable
-                if (leftVar.isInternal() && !rightVar.isInternal()) {
+                if (isInternal(leftVar) && !isInternal(rightVar) && !isReturnVar(leftVar)) {
                     map.put(leftVar.getName(), right.clone());
-                } else if (rightVar.isInternal() && !leftVar.isInternal()) {
+                } else if (isInternal(rightVar) && !isInternal(leftVar) && !isReturnVar(rightVar)) {
                     map.put(rightVar.getName(), left.clone());
-                } else if (leftVar.isInternal() && rightVar.isInternal()) {
+                } else if (isInternal(leftVar) && isInternal(rightVar)) {
                     // to substitute the lower-counter variable with the higher-counter one
-                    boolean isLeftCounterLower = leftVar.getCounter() <= rightVar.getCounter();
+                    boolean isLeftCounterLower = getCounter(leftVar) <= getCounter(rightVar);
                     Var lowerVar = isLeftCounterLower ? leftVar : rightVar;
                     Var higherVar = isLeftCounterLower ? rightVar : leftVar;
-                    map.putIfAbsent(lowerVar.getName(), higherVar.clone());
+                    if (!isReturnVar(lowerVar) && !isFreshVar(higherVar))
+                        map.putIfAbsent(lowerVar.getName(), higherVar.clone());
                 }
             }
         }
@@ -144,4 +145,23 @@ private static boolean hasUsage(Expression exp, String name) {
         // usage not found
         return false;
     }
+
+    private static int getCounter(Var var) {
+        if (!isInternal(var))
+            throw new IllegalStateException("Cannot get counter of non-internal variable");
+        int lastUnderscore = var.getName().lastIndexOf('_');
+        return Integer.parseInt(var.getName().substring(lastUnderscore + 1));
+    }
+
+    private static boolean isInternal(Var var) {
+        return var.getName().startsWith("#");
+    }
+
+    private static boolean isReturnVar(Var var) {
+        return var.getName().startsWith("#ret_");
+    }
+
+    private static boolean isFreshVar(Var var) {
+        return var.getName().startsWith("#fresh_");
+    }
 }

liquidjava-verifier/src/test/java/liquidjava/rj_language/opt/VariableResolverTest.java

@@ -142,4 +142,30 @@ void testUnusedEqualitiesShouldBeIgnored() {
         assertEquals(1, result.size(), "Should only extract used variable z");
         assertEquals("3", result.get("z").toString());
     }
+
+    @Test
+    void testReturnVariableIsNotSubstituted() {
+        // #ret_1 == x && x > 0 should not substitute #ret_1 with x
+        Expression ret = new Var("#ret_1");
+        Expression x = new Var("x");
+        Expression xGreaterZero = new BinaryExpression(x, ">", new LiteralInt(0));
+        Expression retEqualsX = new BinaryExpression(ret, "==", x);
+        Expression fullExpr = new BinaryExpression(xGreaterZero, "&&", retEqualsX);
+
+        Map<String, Expression> result = VariableResolver.resolve(fullExpr);
+        assertTrue(result.isEmpty(), "Return variables should not be substituted with another variable");
+    }
+
+    @Test
+    void testFreshVariableIsNotUsedAsSubstitutionTarget() {
+        // #tmp_1 > 0 && #tmp_1 == #fresh_2 should not substitute #tmp_1 with #fresh_2
+        Expression internal = new Var("#tmp_1");
+        Expression fresh = new Var("#fresh_2");
+        Expression internalGreaterZero = new BinaryExpression(internal, ">", new LiteralInt(0));
+        Expression internalEqualsFresh = new BinaryExpression(internal, "==", fresh);
+        Expression fullExpr = new BinaryExpression(internalGreaterZero, "&&", internalEqualsFresh);
+
+        Map<String, Expression> result = VariableResolver.resolve(fullExpr);
+        assertTrue(result.isEmpty(), "Fresh variables should not replace another variable");
+    }
 }