From 151628518483e2e5492ea2efdb75a40e9c74746c Mon Sep 17 00:00:00 2001 From: Ricardo Costa Date: Sat, 9 May 2026 22:28:07 +0100 Subject: [PATCH 1/2] Add Function Invocation Simplification --- .../rj_language/opt/VariablePropagation.java | 7 ++ .../rj_language/opt/VariableResolver.java | 72 +++++++++++++------ .../opt/ExpressionSimplifierTest.java | 25 +++++++ 3 files changed, 81 insertions(+), 23 deletions(-) diff --git a/liquidjava-verifier/src/main/java/liquidjava/rj_language/opt/VariablePropagation.java b/liquidjava-verifier/src/main/java/liquidjava/rj_language/opt/VariablePropagation.java index 9ec29203..490b241e 100644 --- a/liquidjava-verifier/src/main/java/liquidjava/rj_language/opt/VariablePropagation.java +++ b/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; @@ -69,6 +70,12 @@ private static ValDerivationNode propagateRecursive(Expression exp, Map 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()); - } - } else if (left instanceof Var var && !(right instanceof Var) && canSubstitute(var, right)) { - map.put(var.getName(), right.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) * @@ -129,14 +147,22 @@ private static boolean hasUsage(Expression exp, String name) { 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()) { diff --git a/liquidjava-verifier/src/test/java/liquidjava/rj_language/opt/ExpressionSimplifierTest.java b/liquidjava-verifier/src/test/java/liquidjava/rj_language/opt/ExpressionSimplifierTest.java index df7f2593..5c16b9f6 100644 --- a/liquidjava-verifier/src/test/java/liquidjava/rj_language/opt/ExpressionSimplifierTest.java +++ b/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; @@ -1133,4 +1134,28 @@ void testFoldsAdjacentIntegerConstantsInLeftAssociatedArithmetic() { 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()); + } } From 9970654d395b343eb16cd191e7b5766247072154 Mon Sep 17 00:00:00 2001 From: Ricardo Costa Date: Sat, 9 May 2026 22:53:45 +0100 Subject: [PATCH 2/2] Trigger Workflow