From 694e7ecfa574e9bd29e70aba0a786df61248db26 Mon Sep 17 00:00:00 2001 From: Ricardo Costa Date: Wed, 1 Apr 2026 14:54:40 +0100 Subject: [PATCH 1/4] Special Variable Substitution --- .../rj_language/opt/VariableResolver.java | 18 ++++++++++--- .../rj_language/opt/VariableResolverTest.java | 26 +++++++++++++++++++ 2 files changed, 41 insertions(+), 3 deletions(-) diff --git a/liquidjava-verifier/src/main/java/liquidjava/rj_language/opt/VariableResolver.java b/liquidjava-verifier/src/main/java/liquidjava/rj_language/opt/VariableResolver.java index bd6364a7..024f7037 100644 --- a/liquidjava-verifier/src/main/java/liquidjava/rj_language/opt/VariableResolver.java +++ b/liquidjava-verifier/src/main/java/liquidjava/rj_language/opt/VariableResolver.java @@ -11,6 +11,9 @@ public class VariableResolver { + private static final String RET_PREFIX = "#ret_"; + private static final String FRESH_PREFIX = "#fresh_"; + /** * Extracts variables with constant values from an expression * @@ -54,21 +57,30 @@ private static void resolveRecursive(Expression exp, Map 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 (leftVar.isInternal() && !rightVar.isInternal() && !isReturnVar(leftVar)) { map.put(leftVar.getName(), right.clone()); - } else if (rightVar.isInternal() && !leftVar.isInternal()) { + } else if (rightVar.isInternal() && !leftVar.isInternal() && !isReturnVar(rightVar)) { map.put(rightVar.getName(), left.clone()); } else if (leftVar.isInternal() && rightVar.isInternal()) { // to substitute the lower-counter variable with the higher-counter one boolean isLeftCounterLower = leftVar.getCounter() <= rightVar.getCounter(); 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()); } } } } + private static boolean isReturnVar(Var var) { + return var.getName().startsWith(RET_PREFIX); + } + + private static boolean isFreshVar(Var var) { + return var.getName().startsWith(FRESH_PREFIX); + } + /** * Handles transitive variable equalities in the map (e.g. map: x -> y, y -> 1 => map: x -> 1, y -> 1) * diff --git a/liquidjava-verifier/src/test/java/liquidjava/rj_language/opt/VariableResolverTest.java b/liquidjava-verifier/src/test/java/liquidjava/rj_language/opt/VariableResolverTest.java index 6f799aa2..561d6a3e 100644 --- a/liquidjava-verifier/src/test/java/liquidjava/rj_language/opt/VariableResolverTest.java +++ b/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 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 result = VariableResolver.resolve(fullExpr); + assertTrue(result.isEmpty(), "Fresh variables should not replace another variable"); + } } From 1ef22fce904216a508cd6b4774deb4da9730647a Mon Sep 17 00:00:00 2001 From: Ricardo Costa Date: Wed, 1 Apr 2026 17:14:44 +0100 Subject: [PATCH 2/4] Code Refactoring --- .../java/liquidjava/rj_language/ast/Var.java | 11 ------ .../rj_language/opt/VariableResolver.java | 35 ++++++++++++------- 2 files changed, 23 insertions(+), 23 deletions(-) diff --git a/liquidjava-verifier/src/main/java/liquidjava/rj_language/ast/Var.java b/liquidjava-verifier/src/main/java/liquidjava/rj_language/ast/Var.java index d69d0d74..495a873b 100644 --- a/liquidjava-verifier/src/main/java/liquidjava/rj_language/ast/Var.java +++ b/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)); - } } diff --git a/liquidjava-verifier/src/main/java/liquidjava/rj_language/opt/VariableResolver.java b/liquidjava-verifier/src/main/java/liquidjava/rj_language/opt/VariableResolver.java index 024f7037..514b90c7 100644 --- a/liquidjava-verifier/src/main/java/liquidjava/rj_language/opt/VariableResolver.java +++ b/liquidjava-verifier/src/main/java/liquidjava/rj_language/opt/VariableResolver.java @@ -57,13 +57,13 @@ private static void resolveRecursive(Expression exp, Map 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() && !isReturnVar(leftVar)) { + if (isInternal(leftVar) && !isInternal(rightVar) && !isReturnVar(leftVar)) { map.put(leftVar.getName(), right.clone()); - } else if (rightVar.isInternal() && !leftVar.isInternal() && !isReturnVar(rightVar)) { + } 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; if (!isReturnVar(lowerVar) && !isFreshVar(higherVar)) @@ -73,14 +73,6 @@ private static void resolveRecursive(Expression exp, Map map } } - private static boolean isReturnVar(Var var) { - return var.getName().startsWith(RET_PREFIX); - } - - private static boolean isFreshVar(Var var) { - return var.getName().startsWith(FRESH_PREFIX); - } - /** * Handles transitive variable equalities in the map (e.g. map: x -> y, y -> 1 => map: x -> 1, y -> 1) * @@ -156,4 +148,23 @@ private static boolean hasUsage(Expression exp, String name) { // usage not found return false; } + + private static boolean isInternal(Var var) { + return var.getName().startsWith("#"); + } + + 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 isReturnVar(Var var) { + return var.getName().startsWith(RET_PREFIX); + } + + private static boolean isFreshVar(Var var) { + return var.getName().startsWith(FRESH_PREFIX); + } } \ No newline at end of file From 0f47626825f39aa0a1522ae66f1a6fe445739cf8 Mon Sep 17 00:00:00 2001 From: Ricardo Costa Date: Wed, 1 Apr 2026 17:15:29 +0100 Subject: [PATCH 3/4] Minor Change --- .../java/liquidjava/rj_language/opt/VariableResolver.java | 7 ++----- 1 file changed, 2 insertions(+), 5 deletions(-) diff --git a/liquidjava-verifier/src/main/java/liquidjava/rj_language/opt/VariableResolver.java b/liquidjava-verifier/src/main/java/liquidjava/rj_language/opt/VariableResolver.java index 514b90c7..153753a8 100644 --- a/liquidjava-verifier/src/main/java/liquidjava/rj_language/opt/VariableResolver.java +++ b/liquidjava-verifier/src/main/java/liquidjava/rj_language/opt/VariableResolver.java @@ -11,9 +11,6 @@ public class VariableResolver { - private static final String RET_PREFIX = "#ret_"; - private static final String FRESH_PREFIX = "#fresh_"; - /** * Extracts variables with constant values from an expression * @@ -161,10 +158,10 @@ private static int getCounter(Var var) { } private static boolean isReturnVar(Var var) { - return var.getName().startsWith(RET_PREFIX); + return var.getName().startsWith("#ret_"); } private static boolean isFreshVar(Var var) { - return var.getName().startsWith(FRESH_PREFIX); + return var.getName().startsWith("#fresh_"); } } \ No newline at end of file From 0c83251acf8627e97ff9bf703a5d155c1b5d0a74 Mon Sep 17 00:00:00 2001 From: Ricardo Costa Date: Wed, 1 Apr 2026 17:17:10 +0100 Subject: [PATCH 4/4] Minor Change --- .../java/liquidjava/rj_language/opt/VariableResolver.java | 8 ++++---- 1 file changed, 4 insertions(+), 4 deletions(-) diff --git a/liquidjava-verifier/src/main/java/liquidjava/rj_language/opt/VariableResolver.java b/liquidjava-verifier/src/main/java/liquidjava/rj_language/opt/VariableResolver.java index 153753a8..fd807849 100644 --- a/liquidjava-verifier/src/main/java/liquidjava/rj_language/opt/VariableResolver.java +++ b/liquidjava-verifier/src/main/java/liquidjava/rj_language/opt/VariableResolver.java @@ -146,10 +146,6 @@ private static boolean hasUsage(Expression exp, String name) { return false; } - private static boolean isInternal(Var var) { - return var.getName().startsWith("#"); - } - private static int getCounter(Var var) { if (!isInternal(var)) throw new IllegalStateException("Cannot get counter of non-internal variable"); @@ -157,6 +153,10 @@ private static int getCounter(Var var) { 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_"); }