From b3c83ce3a98dd52e75c11e76a4cf44fe214513cb Mon Sep 17 00:00:00 2001 From: Ricardo Costa Date: Sat, 9 May 2026 20:52:29 +0100 Subject: [PATCH 1/4] Propagate Expressions --- .../RefinementTypeChecker.java | 2 +- .../rj_language/opt/VariablePropagation.java | 14 ++++++++++- .../rj_language/opt/VariableResolver.java | 25 +++++++++++++++++-- .../opt/ExpressionSimplifierTest.java | 21 ++++++++++++++++ 4 files changed, 58 insertions(+), 4 deletions(-) diff --git a/liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/RefinementTypeChecker.java b/liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/RefinementTypeChecker.java index 09095f35..e5655d5a 100644 --- a/liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/RefinementTypeChecker.java +++ b/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); 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 bc76343d..9ec29203 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 @@ -23,13 +23,25 @@ public class VariablePropagation { */ public static ValDerivationNode propagate(Expression exp, ValDerivationNode previousOrigin) { Map substitutions = VariableResolver.resolve(exp); + Map constantSubstitutions = new HashMap<>(); + Map expressionSubstitutions = new HashMap<>(); + for (Map.Entry 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 varOrigins = new HashMap<>(); if (previousOrigin != null) { extractVarOrigins(previousOrigin, varOrigins); } - return propagateRecursive(exp, substitutions, varOrigins); + Map activeSubstitutions = constantSubstitutions.isEmpty() ? expressionSubstitutions + : constantSubstitutions; + return propagateRecursive(exp, activeSubstitutions, varOrigins); } /** 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 fd807849..eb5f25d7 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 @@ -66,6 +66,8 @@ private static void resolveRecursive(Expression exp, Map map 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()); } } } @@ -124,7 +126,8 @@ 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 (right instanceof Var v && v.getName().equals(name) && left.isLiteral()) return false; @@ -164,4 +167,22 @@ private static boolean isReturnVar(Var var) { private static boolean isFreshVar(Var var) { return var.getName().startsWith("#fresh_"); } -} \ No newline at end of file + + 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; + } +} 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 de2c553a..e65eb5c7 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 @@ -1089,4 +1089,25 @@ 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 - 2 + + 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 - 2", result.getValue().toString(), "Expected variable definition to be substituted"); + } } From c7afdde3beaf345ad664a2ae7df0997bc27ec3ab Mon Sep 17 00:00:00 2001 From: Ricardo Costa Date: Sat, 9 May 2026 21:04:42 +0100 Subject: [PATCH 2/4] Fold Adjacent Constants --- .../rj_language/opt/ExpressionFolding.java | 34 ++++++++++++++++++- .../opt/ExpressionSimplifierTest.java | 27 +++++++++++++-- 2 files changed, 58 insertions(+), 3 deletions(-) diff --git a/liquidjava-verifier/src/main/java/liquidjava/rj_language/opt/ExpressionFolding.java b/liquidjava-verifier/src/main/java/liquidjava/rj_language/opt/ExpressionFolding.java index 27aa7cf2..2bdd96c5 100644 --- a/liquidjava-verifier/src/main/java/liquidjava/rj_language/opt/ExpressionFolding.java +++ b/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; } -} \ No newline at end of file + + 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)); + } +} 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 e65eb5c7..df7f2593 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 @@ -1093,7 +1093,7 @@ void testEquivalentBoundsKeepOneSide() { @Test void testSubstitutesVariableDefinedByArithmeticExpression() { // Given: z == y - 2 && y == x + 1 - // Expected: z == x + 1 - 2 + // Expected: z == x - 1 Expression z = new Var("z"); Expression y = new Var("y"); @@ -1108,6 +1108,29 @@ void testSubstitutesVariableDefinedByArithmeticExpression() { // Then assertNotNull(result, "Result should not be null"); - assertEquals("z == x + 1 - 2", result.getValue().toString(), "Expected variable definition to be substituted"); + 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()); } } From 3d595d3038418b0226202fbfff4e611dc863e72d Mon Sep 17 00:00:00 2001 From: Ricardo Costa Date: Sun, 10 May 2026 22:49:08 +0100 Subject: [PATCH 3/4] Minor Change --- .../rj_language/opt/VariablePropagation.java | 10 +++++----- 1 file changed, 5 insertions(+), 5 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..d7835cd2 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 @@ -23,12 +23,12 @@ public class VariablePropagation { */ public static ValDerivationNode propagate(Expression exp, ValDerivationNode previousOrigin) { Map substitutions = VariableResolver.resolve(exp); - Map constantSubstitutions = new HashMap<>(); - Map expressionSubstitutions = new HashMap<>(); + Map directSubstitutions = new HashMap<>(); // var == value or var == var + Map expressionSubstitutions = new HashMap<>(); // var == expression for (Map.Entry entry : substitutions.entrySet()) { Expression value = entry.getValue(); if (value.isLiteral() || value instanceof Var) { - constantSubstitutions.put(entry.getKey(), value); + directSubstitutions.put(entry.getKey(), value); } else { expressionSubstitutions.put(entry.getKey(), value); } @@ -39,8 +39,8 @@ public static ValDerivationNode propagate(Expression exp, ValDerivationNode prev if (previousOrigin != null) { extractVarOrigins(previousOrigin, varOrigins); } - Map activeSubstitutions = constantSubstitutions.isEmpty() ? expressionSubstitutions - : constantSubstitutions; + Map activeSubstitutions = directSubstitutions.isEmpty() ? expressionSubstitutions + : directSubstitutions; return propagateRecursive(exp, activeSubstitutions, varOrigins); } From c81d76c839ac6ba879b7d0f60ac82c869c80c609 Mon Sep 17 00:00:00 2001 From: Ricardo Costa Date: Sun, 10 May 2026 22:51:11 +0100 Subject: [PATCH 4/4] Update Comment --- .../java/liquidjava/rj_language/opt/VariablePropagation.java | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) 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 d7835cd2..5d2c6470 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 @@ -23,7 +23,7 @@ public class VariablePropagation { */ public static ValDerivationNode propagate(Expression exp, ValDerivationNode previousOrigin) { Map substitutions = VariableResolver.resolve(exp); - Map directSubstitutions = new HashMap<>(); // var == value or var == var + Map directSubstitutions = new HashMap<>(); // var == literal or var == var Map expressionSubstitutions = new HashMap<>(); // var == expression for (Map.Entry entry : substitutions.entrySet()) { Expression value = entry.getValue();