Skip to content

Commit 0de6d8f

Browse files
rcosta358rcosta358
authored
Propagate Expressions (#215)
1 parent dd47e55 commit 0de6d8f

5 files changed

Lines changed: 114 additions & 5 deletions

File tree

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

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -379,7 +379,7 @@ public void visitCtIf(CtIf ifElement) {
379379
thenRefs = Predicate.createConjunction(expRefs, freshIsTrue);
380380
elseRefs = Predicate.createConjunction(expRefs, freshIsFalse);
381381
}
382-
382+
383383
freshRV = context.addInstanceToContext(pathVarName, factory.Type().BOOLEAN_PRIMITIVE, thenRefs, exp);
384384
}
385385
vcChecker.addPathVariable(freshRV);

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

Lines changed: 33 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -146,6 +146,10 @@ else if (left instanceof LiteralBoolean && right instanceof LiteralBoolean) {
146146
return new ValDerivationNode(res, new BinaryDerivationNode(leftNode, rightNode, op));
147147
}
148148

149+
ValDerivationNode adjacentConstants = foldAdjacentIntegerConstants(leftNode, rightNode, op);
150+
if (adjacentConstants != null)
151+
return adjacentConstants;
152+
149153
// no folding
150154
DerivationNode origin = (leftNode.getOrigin() != null || rightNode.getOrigin() != null)
151155
? new BinaryDerivationNode(leftNode, rightNode, op) : null;
@@ -243,4 +247,32 @@ private static ValDerivationNode foldIte(ValDerivationNode node) {
243247
private static boolean hasIteChildOrigin(ValDerivationNode cond, ValDerivationNode then, ValDerivationNode els) {
244248
return cond.getOrigin() != null || then.getOrigin() != null || els.getOrigin() != null;
245249
}
246-
}
250+
251+
private static ValDerivationNode foldAdjacentIntegerConstants(ValDerivationNode leftNode,
252+
ValDerivationNode rightNode, String op) {
253+
if (!"+".equals(op) && !"-".equals(op))
254+
return null;
255+
if (!(rightNode.getValue()instanceof LiteralInt rightLiteral))
256+
return null;
257+
if (!(leftNode.getValue()instanceof BinaryExpression leftBinary))
258+
return null;
259+
if (!"+".equals(leftBinary.getOperator()) && !"-".equals(leftBinary.getOperator()))
260+
return null;
261+
if (!(leftBinary.getSecondOperand()instanceof LiteralInt leftLiteral))
262+
return null;
263+
264+
int signedLeft = "+".equals(leftBinary.getOperator()) ? leftLiteral.getValue() : -leftLiteral.getValue();
265+
int signedRight = "+".equals(op) ? rightLiteral.getValue() : -rightLiteral.getValue();
266+
Expression folded = expressionWithConstant(leftBinary.getFirstOperand(), signedLeft + signedRight);
267+
268+
return new ValDerivationNode(folded, new BinaryDerivationNode(leftNode, rightNode, op));
269+
}
270+
271+
private static Expression expressionWithConstant(Expression base, int constant) {
272+
if (constant == 0)
273+
return base.clone();
274+
if (constant > 0)
275+
return new BinaryExpression(base.clone(), "+", new LiteralInt(constant));
276+
return new BinaryExpression(base.clone(), "-", new LiteralInt(-constant));
277+
}
278+
}

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

Lines changed: 13 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -23,13 +23,25 @@ public class VariablePropagation {
2323
*/
2424
public static ValDerivationNode propagate(Expression exp, ValDerivationNode previousOrigin) {
2525
Map<String, Expression> substitutions = VariableResolver.resolve(exp);
26+
Map<String, Expression> directSubstitutions = new HashMap<>(); // var == literal or var == var
27+
Map<String, Expression> expressionSubstitutions = new HashMap<>(); // var == expression
28+
for (Map.Entry<String, Expression> entry : substitutions.entrySet()) {
29+
Expression value = entry.getValue();
30+
if (value.isLiteral() || value instanceof Var) {
31+
directSubstitutions.put(entry.getKey(), value);
32+
} else {
33+
expressionSubstitutions.put(entry.getKey(), value);
34+
}
35+
}
2636

2737
// map of variable origins from the previous derivation tree
2838
Map<String, DerivationNode> varOrigins = new HashMap<>();
2939
if (previousOrigin != null) {
3040
extractVarOrigins(previousOrigin, varOrigins);
3141
}
32-
return propagateRecursive(exp, substitutions, varOrigins);
42+
Map<String, Expression> activeSubstitutions = directSubstitutions.isEmpty() ? expressionSubstitutions
43+
: directSubstitutions;
44+
return propagateRecursive(exp, activeSubstitutions, varOrigins);
3345
}
3446

3547
/**

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

Lines changed: 23 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -66,6 +66,8 @@ private static void resolveRecursive(Expression exp, Map<String, Expression> map
6666
if (!isReturnVar(lowerVar) && !isFreshVar(higherVar))
6767
map.putIfAbsent(lowerVar.getName(), higherVar.clone());
6868
}
69+
} else if (left instanceof Var var && !(right instanceof Var) && canSubstitute(var, right)) {
70+
map.put(var.getName(), right.clone());
6971
}
7072
}
7173
}
@@ -124,7 +126,8 @@ private static boolean hasUsage(Expression exp, String name) {
124126
if (exp instanceof BinaryExpression binary && "==".equals(binary.getOperator())) {
125127
Expression left = binary.getFirstOperand();
126128
Expression right = binary.getSecondOperand();
127-
if (left instanceof Var v && v.getName().equals(name) && right.isLiteral())
129+
if (left instanceof Var v && v.getName().equals(name)
130+
&& (right.isLiteral() || (!(right instanceof Var) && canSubstitute(v, right))))
128131
return false;
129132
if (right instanceof Var v && v.getName().equals(name) && left.isLiteral())
130133
return false;
@@ -164,4 +167,22 @@ private static boolean isReturnVar(Var var) {
164167
private static boolean isFreshVar(Var var) {
165168
return var.getName().startsWith("#fresh_");
166169
}
167-
}
170+
171+
private static boolean canSubstitute(Var var, Expression value) {
172+
return !isReturnVar(var) && !isFreshVar(var) && !containsVariable(value, var.getName());
173+
}
174+
175+
private static boolean containsVariable(Expression exp, String name) {
176+
if (exp instanceof Var var)
177+
return var.getName().equals(name);
178+
179+
if (!exp.hasChildren())
180+
return false;
181+
182+
for (Expression child : exp.getChildren()) {
183+
if (containsVariable(child, name))
184+
return true;
185+
}
186+
return false;
187+
}
188+
}

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

Lines changed: 44 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -1089,4 +1089,48 @@ void testEquivalentBoundsKeepOneSide() {
10891089

10901090
assertDerivationEquals(expected, result, "Equivalent bounds simplification should preserve conjunction origin");
10911091
}
1092+
1093+
@Test
1094+
void testSubstitutesVariableDefinedByArithmeticExpression() {
1095+
// Given: z == y - 2 && y == x + 1
1096+
// Expected: z == x - 1
1097+
1098+
Expression z = new Var("z");
1099+
Expression y = new Var("y");
1100+
Expression x = new Var("x");
1101+
1102+
Expression returnExpression = new BinaryExpression(z, "==", new BinaryExpression(y, "-", new LiteralInt(2)));
1103+
Expression yDefinition = new BinaryExpression(y, "==", new BinaryExpression(x, "+", new LiteralInt(1)));
1104+
Expression fullExpression = new BinaryExpression(returnExpression, "&&", yDefinition);
1105+
1106+
// When
1107+
ValDerivationNode result = ExpressionSimplifier.simplify(fullExpression);
1108+
1109+
// Then
1110+
assertNotNull(result, "Result should not be null");
1111+
assertEquals("z == x - 1", result.getValue().toString(), "Expected variable definition to be substituted");
1112+
}
1113+
1114+
@Test
1115+
void testFoldsAdjacentIntegerConstantsInLeftAssociatedArithmetic() {
1116+
// Given: x + 1 - 2, x - 1 + 2, x + 1 + 2, and x + 1 - 1
1117+
// Expected: x - 1, x + 1, x + 3, and x
1118+
1119+
Expression x = new Var("x");
1120+
1121+
Expression xPlus1Minus2 = new BinaryExpression(new BinaryExpression(x, "+", new LiteralInt(1)), "-",
1122+
new LiteralInt(2));
1123+
Expression xMinus1Plus2 = new BinaryExpression(new BinaryExpression(x, "-", new LiteralInt(1)), "+",
1124+
new LiteralInt(2));
1125+
Expression xPlus1Plus2 = new BinaryExpression(new BinaryExpression(x, "+", new LiteralInt(1)), "+",
1126+
new LiteralInt(2));
1127+
Expression xPlus1Minus1 = new BinaryExpression(new BinaryExpression(x, "+", new LiteralInt(1)), "-",
1128+
new LiteralInt(1));
1129+
1130+
// When / Then
1131+
assertEquals("x - 1", ExpressionSimplifier.simplify(xPlus1Minus2).getValue().toString());
1132+
assertEquals("x + 1", ExpressionSimplifier.simplify(xMinus1Plus2).getValue().toString());
1133+
assertEquals("x + 3", ExpressionSimplifier.simplify(xPlus1Plus2).getValue().toString());
1134+
assertEquals("x", ExpressionSimplifier.simplify(xPlus1Minus1).getValue().toString());
1135+
}
10921136
}

0 commit comments

Comments
 (0)