Skip to content

Commit 3f184df

Browse files
rcosta358rcosta358
committed
Merge branch 'misleading-expansions' into substitute-internal-vars
2 parents c0123ec + ac1ef3e commit 3f184df

2 files changed

Lines changed: 197 additions & 25 deletions

File tree

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

Lines changed: 61 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -3,8 +3,10 @@
33
import liquidjava.rj_language.ast.BinaryExpression;
44
import liquidjava.rj_language.ast.Expression;
55
import liquidjava.rj_language.ast.LiteralBoolean;
6+
import liquidjava.rj_language.ast.UnaryExpression;
67
import liquidjava.rj_language.opt.derivation_node.BinaryDerivationNode;
78
import liquidjava.rj_language.opt.derivation_node.DerivationNode;
9+
import liquidjava.rj_language.opt.derivation_node.UnaryDerivationNode;
810
import liquidjava.rj_language.opt.derivation_node.ValDerivationNode;
911

1012
public class ExpressionSimplifier {
@@ -15,7 +17,8 @@ public class ExpressionSimplifier {
1517
*/
1618
public static ValDerivationNode simplify(Expression exp) {
1719
ValDerivationNode fixedPoint = simplifyToFixedPoint(null, exp);
18-
return simplifyValDerivationNode(fixedPoint);
20+
ValDerivationNode simplified = simplifyValDerivationNode(fixedPoint);
21+
return unwrapDerivedBooleans(simplified);
1922
}
2023

2124
/**
@@ -123,4 +126,61 @@ private static boolean isRedundant(Expression exp) {
123126
}
124127
return false;
125128
}
129+
130+
/**
131+
* Recursively traverses the derivation tree and replaces boolean literals with the expressions that produced them,
132+
* but only when at least one operand in the derivation is non-boolean. e.g. "x == true" where true came from "1 >
133+
* 0" becomes "x == 1 > 0"
134+
*/
135+
static ValDerivationNode unwrapDerivedBooleans(ValDerivationNode node) {
136+
Expression value = node.getValue();
137+
DerivationNode origin = node.getOrigin();
138+
139+
if (origin == null)
140+
return node;
141+
142+
// unwrap binary expressions
143+
if (value instanceof BinaryExpression binExp && origin instanceof BinaryDerivationNode binOrigin) {
144+
ValDerivationNode left = unwrapDerivedBooleans(binOrigin.getLeft());
145+
ValDerivationNode right = unwrapDerivedBooleans(binOrigin.getRight());
146+
if (left != binOrigin.getLeft() || right != binOrigin.getRight()) {
147+
Expression newValue = new BinaryExpression(left.getValue(), binExp.getOperator(), right.getValue());
148+
return new ValDerivationNode(newValue, new BinaryDerivationNode(left, right, binOrigin.getOp()));
149+
}
150+
return node;
151+
}
152+
153+
// unwrap unary expressions
154+
if (value instanceof UnaryExpression unaryExp && origin instanceof UnaryDerivationNode unaryOrigin) {
155+
ValDerivationNode operand = unwrapDerivedBooleans(unaryOrigin.getOperand());
156+
if (operand != unaryOrigin.getOperand()) {
157+
Expression newValue = new UnaryExpression(unaryExp.getOp(), operand.getValue());
158+
return new ValDerivationNode(newValue, new UnaryDerivationNode(operand, unaryOrigin.getOp()));
159+
}
160+
return node;
161+
}
162+
163+
// boolean literal with binary origin: unwrap if at least one child is non-boolean
164+
if (value instanceof LiteralBoolean && origin instanceof BinaryDerivationNode binOrigin) {
165+
ValDerivationNode left = unwrapDerivedBooleans(binOrigin.getLeft());
166+
ValDerivationNode right = unwrapDerivedBooleans(binOrigin.getRight());
167+
if (!(left.getValue() instanceof LiteralBoolean) || !(right.getValue() instanceof LiteralBoolean)) {
168+
Expression newValue = new BinaryExpression(left.getValue(), binOrigin.getOp(), right.getValue());
169+
return new ValDerivationNode(newValue, new BinaryDerivationNode(left, right, binOrigin.getOp()));
170+
}
171+
return node;
172+
}
173+
174+
// boolean literal with unary origin: unwrap if operand is non-boolean
175+
if (value instanceof LiteralBoolean && origin instanceof UnaryDerivationNode unaryOrigin) {
176+
ValDerivationNode operand = unwrapDerivedBooleans(unaryOrigin.getOperand());
177+
if (!(operand.getValue() instanceof LiteralBoolean)) {
178+
Expression newValue = new UnaryExpression(unaryOrigin.getOp(), operand.getValue());
179+
return new ValDerivationNode(newValue, new UnaryDerivationNode(operand, unaryOrigin.getOp()));
180+
}
181+
return node;
182+
}
183+
184+
return node;
185+
}
126186
}

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

Lines changed: 136 additions & 24 deletions
Original file line numberDiff line numberDiff line change
@@ -239,13 +239,13 @@ void testComplexArithmeticWithMultipleOperations() {
239239
// When
240240
ValDerivationNode result = ExpressionSimplifier.simplify(fullExpression);
241241

242-
// Then
242+
// Then: boolean literals are unwrapped to show the verified conditions
243243
assertNotNull(result, "Result should not be null");
244244
assertNotNull(result.getValue(), "Result value should not be null");
245-
assertInstanceOf(LiteralBoolean.class, result.getValue(), "Result should be a boolean literal");
246-
assertTrue(result.getValue().isBooleanTrue(), "Expected result to be true");
245+
assertEquals("14 == 14 && 5 == 5 && 7 == 7 && 14 == 14", result.getValue().toString(),
246+
"All verified conditions should be visible instead of collapsed to true");
247247

248-
// 5 * 2 + 7 - 3
248+
// 5 * 2 + 7 - 3 = 14
249249
ValDerivationNode val5 = new ValDerivationNode(new LiteralInt(5), new VarDerivationNode("a"));
250250
ValDerivationNode val2 = new ValDerivationNode(new LiteralInt(2), null);
251251
BinaryDerivationNode mult5Times2 = new BinaryDerivationNode(val5, val2, "*");
@@ -262,39 +262,45 @@ void testComplexArithmeticWithMultipleOperations() {
262262
// 14 from variable c
263263
ValDerivationNode val14Right = new ValDerivationNode(new LiteralInt(14), new VarDerivationNode("c"));
264264

265-
// 14 == 14
265+
// 14 == 14 (unwrapped from true)
266266
BinaryDerivationNode compare14 = new BinaryDerivationNode(val14Left, val14Right, "==");
267-
ValDerivationNode trueFromComparison = new ValDerivationNode(new LiteralBoolean(true), compare14);
267+
Expression expr14Eq14 = new BinaryExpression(new LiteralInt(14), "==", new LiteralInt(14));
268+
ValDerivationNode compare14Node = new ValDerivationNode(expr14Eq14, compare14);
268269

269-
// a == 5 => true
270+
// a == 5 => 5 == 5 (unwrapped from true)
270271
ValDerivationNode val5ForCompA = new ValDerivationNode(new LiteralInt(5), new VarDerivationNode("a"));
271272
ValDerivationNode val5Literal = new ValDerivationNode(new LiteralInt(5), null);
272273
BinaryDerivationNode compareA5 = new BinaryDerivationNode(val5ForCompA, val5Literal, "==");
273-
ValDerivationNode trueFromA = new ValDerivationNode(new LiteralBoolean(true), compareA5);
274+
Expression expr5Eq5 = new BinaryExpression(new LiteralInt(5), "==", new LiteralInt(5));
275+
ValDerivationNode compare5Node = new ValDerivationNode(expr5Eq5, compareA5);
274276

275-
// b == 7 => true
277+
// b == 7 => 7 == 7 (unwrapped from true)
276278
ValDerivationNode val7ForCompB = new ValDerivationNode(new LiteralInt(7), new VarDerivationNode("b"));
277279
ValDerivationNode val7Literal = new ValDerivationNode(new LiteralInt(7), null);
278280
BinaryDerivationNode compareB7 = new BinaryDerivationNode(val7ForCompB, val7Literal, "==");
279-
ValDerivationNode trueFromB = new ValDerivationNode(new LiteralBoolean(true), compareB7);
281+
Expression expr7Eq7 = new BinaryExpression(new LiteralInt(7), "==", new LiteralInt(7));
282+
ValDerivationNode compare7Node = new ValDerivationNode(expr7Eq7, compareB7);
280283

281-
// (a == 5) && (b == 7) => true
282-
BinaryDerivationNode andAB = new BinaryDerivationNode(trueFromA, trueFromB, "&&");
283-
ValDerivationNode trueFromAB = new ValDerivationNode(new LiteralBoolean(true), andAB);
284+
// (5 == 5) && (7 == 7) (unwrapped from true)
285+
BinaryDerivationNode andAB = new BinaryDerivationNode(compare5Node, compare7Node, "&&");
286+
Expression expr5And7 = new BinaryExpression(expr5Eq5, "&&", expr7Eq7);
287+
ValDerivationNode and5And7Node = new ValDerivationNode(expr5And7, andAB);
284288

285-
// c == 14 => true
289+
// c == 14 => 14 == 14 (unwrapped from true)
286290
ValDerivationNode val14ForCompC = new ValDerivationNode(new LiteralInt(14), new VarDerivationNode("c"));
287291
ValDerivationNode val14Literal = new ValDerivationNode(new LiteralInt(14), null);
288292
BinaryDerivationNode compareC14 = new BinaryDerivationNode(val14ForCompC, val14Literal, "==");
289-
ValDerivationNode trueFromC = new ValDerivationNode(new LiteralBoolean(true), compareC14);
293+
Expression expr14Eq14b = new BinaryExpression(new LiteralInt(14), "==", new LiteralInt(14));
294+
ValDerivationNode compare14bNode = new ValDerivationNode(expr14Eq14b, compareC14);
290295

291-
// ((a == 5) && (b == 7)) && (c == 14) => true
292-
BinaryDerivationNode andABC = new BinaryDerivationNode(trueFromAB, trueFromC, "&&");
293-
ValDerivationNode trueFromAllConditions = new ValDerivationNode(new LiteralBoolean(true), andABC);
296+
// ((5 == 5) && (7 == 7)) && (14 == 14) (unwrapped from true)
297+
BinaryDerivationNode andABC = new BinaryDerivationNode(and5And7Node, compare14bNode, "&&");
298+
Expression exprConditions = new BinaryExpression(expr5And7, "&&", expr14Eq14b);
299+
ValDerivationNode conditionsNode = new ValDerivationNode(exprConditions, andABC);
294300

295-
// 14 == 14 => true
296-
BinaryDerivationNode finalAnd = new BinaryDerivationNode(trueFromComparison, trueFromAllConditions, "&&");
297-
ValDerivationNode expected = new ValDerivationNode(new LiteralBoolean(true), finalAnd);
301+
// (14 == 14) && ((5 == 5 && 7 == 7) && 14 == 14)
302+
BinaryDerivationNode finalAnd = new BinaryDerivationNode(compare14Node, conditionsNode, "&&");
303+
ValDerivationNode expected = new ValDerivationNode(result.getValue(), finalAnd);
298304

299305
// Compare the derivation trees
300306
assertDerivationEquals(expected, result, "");
@@ -754,7 +760,8 @@ void testInternalToInternalChainWithUserFacingVariableInternalFirst() {
754760
@Test
755761
void testInternalToInternalBothResolvingToLiteral() {
756762
// Given: #a_3 == #b_7 && #b_7 == 5
757-
// Expected: 5 == 5 && 5 == 5 -> true (#a_3 has lower counter so #a_3 -> #b_7; #b_7 -> 5)
763+
// Expected: 5 == 5 && 5 == 5 (#a_3 has lower counter so #a_3 -> #b_7; #b_7 -> 5;
764+
// both equalities collapse to 5 == 5, unwrapped from true to show verified conditions)
758765

759766
Expression a3 = new Var("#a_3");
760767
Expression b7 = new Var("#b_7");
@@ -766,8 +773,8 @@ void testInternalToInternalBothResolvingToLiteral() {
766773
ValDerivationNode result = ExpressionSimplifier.simplify(fullExpression);
767774

768775
assertNotNull(result);
769-
assertEquals("true", result.getValue().toString(),
770-
"#a_3 -> #b_7 -> 5 and #b_7 -> 5; both equalities collapse to 5 == 5 -> true");
776+
assertEquals("5 == 5 && 5 == 5", result.getValue().toString(),
777+
"#a_3 -> #b_7 -> 5 and #b_7 -> 5; both equalities unwrapped to show 5 == 5");
771778
}
772779

773780
@Test
@@ -789,6 +796,111 @@ void testInternalToInternalNoFurtherResolution() {
789796
"#a_3 (lower counter) replaced by #b_7 (higher counter); equality collapses to trivial");
790797
}
791798

799+
@Test
800+
void testShouldUnwrapBooleanInEquality() {
801+
// Given: x == (1 > 0)
802+
// Without unwrapping: x == true (unhelpful - hides what "true" came from)
803+
// Expected: x == 1 > 0 (unwrapped to show the original comparison)
804+
805+
Expression varX = new Var("x");
806+
Expression one = new LiteralInt(1);
807+
Expression zero = new LiteralInt(0);
808+
Expression oneGreaterZero = new BinaryExpression(one, ">", zero);
809+
Expression fullExpression = new BinaryExpression(varX, "==", oneGreaterZero);
810+
811+
// When
812+
ValDerivationNode result = ExpressionSimplifier.simplify(fullExpression);
813+
814+
// Then
815+
assertNotNull(result, "Result should not be null");
816+
assertEquals("x == 1 > 0", result.getValue().toString(),
817+
"Boolean in equality should be unwrapped to show the original comparison");
818+
}
819+
820+
@Test
821+
void testShouldUnwrapBooleanInEqualityWithPropagation() {
822+
// Given: x == (a > b) && a == 3 && b == 1
823+
// Without unwrapping: x == true (unhelpful)
824+
// Expected: x == 3 > 1 (unwrapped and propagated)
825+
826+
Expression varX = new Var("x");
827+
Expression varA = new Var("a");
828+
Expression varB = new Var("b");
829+
Expression aGreaterB = new BinaryExpression(varA, ">", varB);
830+
Expression xEqualsComp = new BinaryExpression(varX, "==", aGreaterB);
831+
832+
Expression three = new LiteralInt(3);
833+
Expression aEquals3 = new BinaryExpression(varA, "==", three);
834+
Expression one = new LiteralInt(1);
835+
Expression bEquals1 = new BinaryExpression(varB, "==", one);
836+
837+
Expression conditions = new BinaryExpression(aEquals3, "&&", bEquals1);
838+
Expression fullExpression = new BinaryExpression(xEqualsComp, "&&", conditions);
839+
840+
// When
841+
ValDerivationNode result = ExpressionSimplifier.simplify(fullExpression);
842+
843+
// Then
844+
assertNotNull(result, "Result should not be null");
845+
assertEquals("x == 3 > 1", result.getValue().toString(),
846+
"Boolean in equality should be unwrapped after propagation");
847+
}
848+
849+
@Test
850+
void testShouldNotUnwrapBooleanWithBooleanChildren() {
851+
// Given: (y || true) && !true && y == false
852+
// Expected: false (both children of the fold are boolean, so no unwrapping needed)
853+
854+
Expression varY = new Var("y");
855+
Expression trueExp = new LiteralBoolean(true);
856+
Expression yOrTrue = new BinaryExpression(varY, "||", trueExp);
857+
Expression notTrue = new UnaryExpression("!", trueExp);
858+
Expression falseExp = new LiteralBoolean(false);
859+
Expression yEqualsFalse = new BinaryExpression(varY, "==", falseExp);
860+
861+
Expression firstAnd = new BinaryExpression(yOrTrue, "&&", notTrue);
862+
Expression fullExpression = new BinaryExpression(firstAnd, "&&", yEqualsFalse);
863+
864+
// When
865+
ValDerivationNode result = ExpressionSimplifier.simplify(fullExpression);
866+
867+
// Then: false stays as false since both sides in the derivation are booleans
868+
assertNotNull(result, "Result should not be null");
869+
assertInstanceOf(LiteralBoolean.class, result.getValue(), "Result should remain a boolean");
870+
assertFalse(result.getValue().isBooleanTrue(), "Expected result to be false");
871+
}
872+
873+
@Test
874+
void testShouldUnwrapNestedBooleanInEquality() {
875+
// Given: x == (a + b > 10) && a == 3 && b == 5
876+
// Without unwrapping: x == true (unhelpful)
877+
// Expected: x == 8 > 10 (shows the actual comparison that produced the boolean)
878+
879+
Expression varX = new Var("x");
880+
Expression varA = new Var("a");
881+
Expression varB = new Var("b");
882+
Expression aPlusB = new BinaryExpression(varA, "+", varB);
883+
Expression ten = new LiteralInt(10);
884+
Expression comparison = new BinaryExpression(aPlusB, ">", ten);
885+
Expression xEqualsComp = new BinaryExpression(varX, "==", comparison);
886+
887+
Expression three = new LiteralInt(3);
888+
Expression aEquals3 = new BinaryExpression(varA, "==", three);
889+
Expression five = new LiteralInt(5);
890+
Expression bEquals5 = new BinaryExpression(varB, "==", five);
891+
892+
Expression conditions = new BinaryExpression(aEquals3, "&&", bEquals5);
893+
Expression fullExpression = new BinaryExpression(xEqualsComp, "&&", conditions);
894+
895+
// When
896+
ValDerivationNode result = ExpressionSimplifier.simplify(fullExpression);
897+
898+
// Then
899+
assertNotNull(result, "Result should not be null");
900+
assertEquals("x == 8 > 10", result.getValue().toString(),
901+
"Boolean in equality should be unwrapped to show the computed comparison");
902+
}
903+
792904
/**
793905
* Helper method to compare two derivation nodes recursively
794906
*/

0 commit comments

Comments
 (0)