Distinguish Definitions from Usages in Variable Resolver (#219)

Author: rcosta358

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

@@ -26,7 +26,7 @@ public static Map<String, Expression> resolve(Expression exp) {
         resolveRecursive(exp, map);
 
         // remove variables that were not used in the expression
-        map.entrySet().removeIf(entry -> !hasUsage(exp, entry.getKey()));
+        map.entrySet().removeIf(entry -> !hasUsage(exp, entry.getKey(), entry.getValue()));
 
         // transitively resolve variables
         return resolveTransitive(map);
@@ -138,20 +138,21 @@ private static Expression lookup(Expression exp, Map<String, Expression> map, Se
      *
      * @return true if used, false otherwise
      */
-    private static boolean hasUsage(Expression exp, String name) {
+    private static boolean hasUsage(Expression exp, String name, Expression value) {
         // exclude own definitions
         if (exp instanceof BinaryExpression binary && "==".equals(binary.getOperator())) {
             Expression left = binary.getFirstOperand();
             Expression right = binary.getSecondOperand();
-            if (left instanceof Var v && v.getName().equals(name)
+            if (left instanceof Var v && v.getName().equals(name) && right.equals(value)
                     && (right.isLiteral() || (!(right instanceof Var) && canSubstitute(v, right))))
                 return false;
-            if (left instanceof FunctionInvocation && left.toString().equals(name)
+            if (left instanceof FunctionInvocation && left.toString().equals(name) && right.equals(value)
                     && (right.isLiteral() || (!(right instanceof Var) && !containsExpression(right, left))))
                 return false;
-            if (right instanceof Var v && v.getName().equals(name) && left.isLiteral())
+            if (right instanceof Var v && v.getName().equals(name) && left.equals(value) && left.isLiteral())
                 return false;
-            if (right instanceof FunctionInvocation && right.toString().equals(name) && left.isLiteral())
+            if (right instanceof FunctionInvocation && right.toString().equals(name) && left.equals(value)
+                    && left.isLiteral())
                 return false;
         }
 
@@ -166,7 +167,7 @@ private static boolean hasUsage(Expression exp, String name) {
         // recurse children
         if (exp.hasChildren()) {
             for (Expression child : exp.getChildren())
-                if (hasUsage(child, name))
+                if (hasUsage(child, name, value))
                     return true;
         }
 

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

@@ -457,6 +457,16 @@ void testIteEqualBranchesSimplifiesToBranch() {
         assertDerivationEquals(expected, result, "");
     }
 
+    @Test
+    void testIteConditionUsesEqualityFromConjunction() {
+        Expression expr = parse("mode == 1 && (mode == 2 ? explicit(param) : start(param))");
+        ValDerivationNode result = ExpressionSimplifier.simplify(expr);
+
+        assertNotNull(result, "Result should not be null");
+        assertEquals("start(param)", result.getValue().toString(),
+                "mode == 1 should make the mode == 2 ternary condition false");
+    }
+
     @Test
     void testByteAliasExpansion() {
         String sut = "Byte(b)";

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

@@ -90,6 +90,15 @@ void testUnusedEqualitiesShouldBeIgnored() {
         assertEquals("3", result.get("z").toString());
     }
 
+    @Test
+    void testDifferentEqualityInIteConditionCountsAsUsage() {
+        Expression expression = parse("mode == 1 && (mode == 2 ? explicit(param) : start(param))");
+        Map<String, Expression> result = VariableResolver.resolve(expression);
+
+        assertEquals(1, result.size(), "Ternary condition should count as a use of mode");
+        assertEquals("1", result.get("mode").toString());
+    }
+
     @Test
     void testReturnVariableIsNotSubstituted() {
         Expression expression = parse("x > 0 && #ret_1 == x");