Propagate Function Invocations

liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/RefinementTypeChecker.java

@@ -379,7 +379,7 @@ public void visitCtIf(CtIf ifElement) {
                 thenRefs = Predicate.createConjunction(expRefs, freshIsTrue);
                 elseRefs = Predicate.createConjunction(expRefs, freshIsFalse);
             }
-            
+
             freshRV = context.addInstanceToContext(pathVarName, factory.Type().BOOLEAN_PRIMITIVE, thenRefs, exp);
         }
         vcChecker.addPathVariable(freshRV);

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

@@ -146,6 +146,10 @@ else if (left instanceof LiteralBoolean && right instanceof LiteralBoolean) {
                 return new ValDerivationNode(res, new BinaryDerivationNode(leftNode, rightNode, op));
         }
 
+        ValDerivationNode adjacentConstants = foldAdjacentIntegerConstants(leftNode, rightNode, op);
+        if (adjacentConstants != null)
+            return adjacentConstants;
+
         // no folding
         DerivationNode origin = (leftNode.getOrigin() != null || rightNode.getOrigin() != null)
                 ? new BinaryDerivationNode(leftNode, rightNode, op) : null;
@@ -243,4 +247,32 @@ private static ValDerivationNode foldIte(ValDerivationNode node) {
     private static boolean hasIteChildOrigin(ValDerivationNode cond, ValDerivationNode then, ValDerivationNode els) {
         return cond.getOrigin() != null || then.getOrigin() != null || els.getOrigin() != null;
     }
-}
+
+    private static ValDerivationNode foldAdjacentIntegerConstants(ValDerivationNode leftNode,
+            ValDerivationNode rightNode, String op) {
+        if (!"+".equals(op) && !"-".equals(op))
+            return null;
+        if (!(rightNode.getValue()instanceof LiteralInt rightLiteral))
+            return null;
+        if (!(leftNode.getValue()instanceof BinaryExpression leftBinary))
+            return null;
+        if (!"+".equals(leftBinary.getOperator()) && !"-".equals(leftBinary.getOperator()))
+            return null;
+        if (!(leftBinary.getSecondOperand()instanceof LiteralInt leftLiteral))
+            return null;
+
+        int signedLeft = "+".equals(leftBinary.getOperator()) ? leftLiteral.getValue() : -leftLiteral.getValue();
+        int signedRight = "+".equals(op) ? rightLiteral.getValue() : -rightLiteral.getValue();
+        Expression folded = expressionWithConstant(leftBinary.getFirstOperand(), signedLeft + signedRight);
+
+        return new ValDerivationNode(folded, new BinaryDerivationNode(leftNode, rightNode, op));
+    }
+
+    private static Expression expressionWithConstant(Expression base, int constant) {
+        if (constant == 0)
+            return base.clone();
+        if (constant > 0)
+            return new BinaryExpression(base.clone(), "+", new LiteralInt(constant));
+        return new BinaryExpression(base.clone(), "-", new LiteralInt(-constant));
+    }
+}

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

@@ -2,6 +2,7 @@
 
 import liquidjava.rj_language.ast.BinaryExpression;
 import liquidjava.rj_language.ast.Expression;
+import liquidjava.rj_language.ast.FunctionInvocation;
 import liquidjava.rj_language.ast.UnaryExpression;
 import liquidjava.rj_language.ast.Var;
 import liquidjava.rj_language.opt.derivation_node.BinaryDerivationNode;
@@ -23,13 +24,25 @@ public class VariablePropagation {
      */
     public static ValDerivationNode propagate(Expression exp, ValDerivationNode previousOrigin) {
         Map<String, Expression> substitutions = VariableResolver.resolve(exp);
+        Map<String, Expression> constantSubstitutions = new HashMap<>();
+        Map<String, Expression> expressionSubstitutions = new HashMap<>();
+        for (Map.Entry<String, Expression> entry : substitutions.entrySet()) {
+            Expression value = entry.getValue();
+            if (value.isLiteral() || value instanceof Var) {
+                constantSubstitutions.put(entry.getKey(), value);
+            } else {
+                expressionSubstitutions.put(entry.getKey(), value);
+            }
+        }
 
         // map of variable origins from the previous derivation tree
         Map<String, DerivationNode> varOrigins = new HashMap<>();
         if (previousOrigin != null) {
             extractVarOrigins(previousOrigin, varOrigins);
         }
-        return propagateRecursive(exp, substitutions, varOrigins);
+        Map<String, Expression> activeSubstitutions = constantSubstitutions.isEmpty() ? expressionSubstitutions
+                : constantSubstitutions;
+        return propagateRecursive(exp, activeSubstitutions, varOrigins);
     }
 
     /**
@@ -57,6 +70,12 @@ private static ValDerivationNode propagateRecursive(Expression exp, Map<String,
             return new ValDerivationNode(var, null);
         }
 
+        if (exp instanceof FunctionInvocation) {
+            Expression value = subs.get(exp.toString());
+            if (value != null)
+                return new ValDerivationNode(value.clone(), new VarDerivationNode(exp.toString()));
+        }
+
         // lift unary origin
         if (exp instanceof UnaryExpression unary) {
             ValDerivationNode operand = propagateRecursive(unary.getChildren().get(0), subs, varOrigins);

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

@@ -7,6 +7,7 @@
 
 import liquidjava.rj_language.ast.BinaryExpression;
 import liquidjava.rj_language.ast.Expression;
+import liquidjava.rj_language.ast.FunctionInvocation;
 import liquidjava.rj_language.ast.Var;
 
 public class VariableResolver {
@@ -45,31 +46,50 @@ private static void resolveRecursive(Expression exp, Map<String, Expression> map
         if ("&&".equals(op)) {
             resolveRecursive(be.getFirstOperand(), map);
             resolveRecursive(be.getSecondOperand(), map);
-        } else if ("==".equals(op)) {
-            Expression left = be.getFirstOperand();
-            Expression right = be.getSecondOperand();
-            if (left instanceof Var var && right.isLiteral()) {
-                map.put(var.getName(), right.clone());
-            } else if (right instanceof Var var && left.isLiteral()) {
-                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 (isInternal(leftVar) && !isInternal(rightVar) && !isReturnVar(leftVar)) {
-                    map.put(leftVar.getName(), right.clone());
-                } else if (isInternal(rightVar) && !isInternal(leftVar) && !isReturnVar(rightVar)) {
-                    map.put(rightVar.getName(), left.clone());
-                } else if (isInternal(leftVar) && isInternal(rightVar)) {
-                    // to substitute the lower-counter variable with the higher-counter one
-                    boolean isLeftCounterLower = getCounter(leftVar) <= getCounter(rightVar);
-                    Var lowerVar = isLeftCounterLower ? leftVar : rightVar;
-                    Var higherVar = isLeftCounterLower ? rightVar : leftVar;
-                    if (!isReturnVar(lowerVar) && !isFreshVar(higherVar))
-                        map.putIfAbsent(lowerVar.getName(), higherVar.clone());
-                }
+            return;
+        }
+        if (!"==".equals(op))
+            return;
+
+        Expression left = be.getFirstOperand();
+        Expression right = be.getSecondOperand();
+        String leftKey = substitutionKey(left);
+        String rightKey = substitutionKey(right);
+
+        if (leftKey != null && right.isLiteral()) {
+            map.put(leftKey, right.clone());
+        } else if (rightKey != null && left.isLiteral()) {
+            map.put(rightKey, left.clone());
+        } else if (left instanceof Var leftVar && right instanceof Var rightVar) {
+            // to substitute internal variable with user-facing variable
+            if (isInternal(leftVar) && !isInternal(rightVar) && !isReturnVar(leftVar)) {
+                map.put(leftVar.getName(), right.clone());
+            } else if (isInternal(rightVar) && !isInternal(leftVar) && !isReturnVar(rightVar)) {
+                map.put(rightVar.getName(), left.clone());
+            } else if (isInternal(leftVar) && isInternal(rightVar)) {
+                // to substitute the lower-counter variable with the higher-counter one
+                boolean isLeftCounterLower = getCounter(leftVar) <= getCounter(rightVar);
+                Var lowerVar = isLeftCounterLower ? leftVar : rightVar;
+                Var higherVar = isLeftCounterLower ? rightVar : leftVar;
+                if (!isReturnVar(lowerVar) && !isFreshVar(higherVar))
+                    map.putIfAbsent(lowerVar.getName(), higherVar.clone());
             }
+        } else if (left instanceof Var var && !(right instanceof Var) && canSubstitute(var, right)) {
+            map.put(var.getName(), right.clone());
+        } else if (left instanceof FunctionInvocation && !(right instanceof Var)
+                && !right.toString().contains(leftKey)) {
+            map.put(leftKey, right.clone());
         }
     }
 
+    private static String substitutionKey(Expression exp) {
+        if (exp instanceof Var var)
+            return var.getName();
+        if (exp instanceof FunctionInvocation)
+            return exp.toString();
+        return null;
+    }
+
     /**
      * Handles transitive variable equalities in the map (e.g. map: x -> y, y -> 1 => map: x -> 1, y -> 1)
      * 
@@ -124,16 +144,25 @@ private static boolean hasUsage(Expression exp, String name) {
         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) && right.isLiteral())
+            if (left instanceof Var v && v.getName().equals(name)
+                    && (right.isLiteral() || (!(right instanceof Var) && canSubstitute(v, right))))
+                return false;
+            if (left instanceof FunctionInvocation && left.toString().equals(name)
+                    && (right.isLiteral() || (!(right instanceof Var) && !right.toString().contains(name))))
                 return false;
             if (right instanceof Var v && v.getName().equals(name) && left.isLiteral())
                 return false;
+            if (right instanceof FunctionInvocation && right.toString().equals(name) && left.isLiteral())
+                return false;
         }
 
         // usage found
         if (exp instanceof Var var && var.getName().equals(name)) {
             return true;
         }
+        if (exp instanceof FunctionInvocation && exp.toString().equals(name)) {
+            return true;
+        }
 
         // recurse children
         if (exp.hasChildren()) {
@@ -164,4 +193,22 @@ private static boolean isReturnVar(Var var) {
     private static boolean isFreshVar(Var var) {
         return var.getName().startsWith("#fresh_");
     }
-}
+
+    private static boolean canSubstitute(Var var, Expression value) {
+        return !isReturnVar(var) && !isFreshVar(var) && !containsVariable(value, var.getName());
+    }
+
+    private static boolean containsVariable(Expression exp, String name) {
+        if (exp instanceof Var var)
+            return var.getName().equals(name);
+
+        if (!exp.hasChildren())
+            return false;
+
+        for (Expression child : exp.getChildren()) {
+            if (containsVariable(child, name))
+                return true;
+        }
+        return false;
+    }
+}

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

@@ -10,6 +10,7 @@
 import liquidjava.rj_language.ast.AliasInvocation;
 import liquidjava.rj_language.ast.BinaryExpression;
 import liquidjava.rj_language.ast.Expression;
+import liquidjava.rj_language.ast.FunctionInvocation;
 import liquidjava.rj_language.ast.Ite;
 import liquidjava.rj_language.ast.LiteralBoolean;
 import liquidjava.rj_language.ast.LiteralInt;
@@ -1089,4 +1090,72 @@ void testEquivalentBoundsKeepOneSide() {
 
         assertDerivationEquals(expected, result, "Equivalent bounds simplification should preserve conjunction origin");
     }
+
+    @Test
+    void testSubstitutesVariableDefinedByArithmeticExpression() {
+        // Given: z == y - 2 && y == x + 1
+        // Expected: z == x - 1
+
+        Expression z = new Var("z");
+        Expression y = new Var("y");
+        Expression x = new Var("x");
+
+        Expression returnExpression = new BinaryExpression(z, "==", new BinaryExpression(y, "-", new LiteralInt(2)));
+        Expression yDefinition = new BinaryExpression(y, "==", new BinaryExpression(x, "+", new LiteralInt(1)));
+        Expression fullExpression = new BinaryExpression(returnExpression, "&&", yDefinition);
+
+        // When
+        ValDerivationNode result = ExpressionSimplifier.simplify(fullExpression);
+
+        // Then
+        assertNotNull(result, "Result should not be null");
+        assertEquals("z == x - 1", result.getValue().toString(), "Expected variable definition to be substituted");
+    }
+
+    @Test
+    void testFoldsAdjacentIntegerConstantsInLeftAssociatedArithmetic() {
+        // Given: x + 1 - 2, x - 1 + 2, x + 1 + 2, and x + 1 - 1
+        // Expected: x - 1, x + 1, x + 3, and x
+
+        Expression x = new Var("x");
+
+        Expression xPlus1Minus2 = new BinaryExpression(new BinaryExpression(x, "+", new LiteralInt(1)), "-",
+                new LiteralInt(2));
+        Expression xMinus1Plus2 = new BinaryExpression(new BinaryExpression(x, "-", new LiteralInt(1)), "+",
+                new LiteralInt(2));
+        Expression xPlus1Plus2 = new BinaryExpression(new BinaryExpression(x, "+", new LiteralInt(1)), "+",
+                new LiteralInt(2));
+        Expression xPlus1Minus1 = new BinaryExpression(new BinaryExpression(x, "+", new LiteralInt(1)), "-",
+                new LiteralInt(1));
+
+        // When / Then
+        assertEquals("x - 1", ExpressionSimplifier.simplify(xPlus1Minus2).getValue().toString());
+        assertEquals("x + 1", ExpressionSimplifier.simplify(xMinus1Plus2).getValue().toString());
+        assertEquals("x + 3", ExpressionSimplifier.simplify(xPlus1Plus2).getValue().toString());
+        assertEquals("x", ExpressionSimplifier.simplify(xPlus1Minus1).getValue().toString());
+    }
+
+    @Test
+    void testFunctionInvocationEqualitiesPropagateTransitively() {
+        // Given: size(x3) == size(x2) - 1 && size(x2) == size(x1) + 1 && size(x1) == 0
+        // Expected: size(x3) == 0
+        Expression x1 = new Var("x1");
+        Expression x2 = new Var("x2");
+        Expression x3 = new Var("x3");
+        Expression sizeX1 = new FunctionInvocation("size", List.of(x1));
+        Expression sizeX2 = new FunctionInvocation("size", List.of(x2));
+        Expression sizeX3 = new FunctionInvocation("size", List.of(x3));
+
+        Expression sizeX3EqualsSizeX2Minus1 = new BinaryExpression(sizeX3, "==",
+                new BinaryExpression(sizeX2, "-", new LiteralInt(1)));
+        Expression sizeX2EqualsSizeX1Plus1 = new BinaryExpression(sizeX2, "==",
+                new BinaryExpression(sizeX1, "+", new LiteralInt(1)));
+        Expression sizeX1Equals0 = new BinaryExpression(sizeX1, "==", new LiteralInt(0));
+        Expression fullExpression = new BinaryExpression(sizeX3EqualsSizeX2Minus1, "&&",
+                new BinaryExpression(sizeX2EqualsSizeX1Plus1, "&&", sizeX1Equals0));
+
+        ValDerivationNode result = ExpressionSimplifier.simplify(fullExpression);
+
+        assertEquals("size(x3) == 0", result.getValue().toString());
+    }
 }