Skip to content

Commit b814114

Browse files
rcosta358rcosta358
committed
Improve Tests
1 parent 401725e commit b814114

File tree

2 files changed

+133
-123
lines changed

2 files changed

+133
-123
lines changed

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

Lines changed: 72 additions & 123 deletions
Original file line numberDiff line numberDiff line change
@@ -1,9 +1,8 @@
11
package liquidjava.rj_language.opt;
22

33
import static org.junit.jupiter.api.Assertions.*;
4+
import static liquidjava.utils.TestUtils.*;
45

5-
import liquidjava.processor.context.Context;
6-
import liquidjava.rj_language.Predicate;
76
import java.util.List;
87
import java.util.Map;
98

@@ -17,23 +16,17 @@
1716
import liquidjava.rj_language.ast.UnaryExpression;
1817
import liquidjava.rj_language.ast.Var;
1918
import liquidjava.rj_language.opt.derivation_node.BinaryDerivationNode;
20-
import liquidjava.rj_language.opt.derivation_node.DerivationNode;
2119
import liquidjava.rj_language.opt.derivation_node.IteDerivationNode;
2220
import liquidjava.rj_language.opt.derivation_node.UnaryDerivationNode;
2321
import liquidjava.rj_language.opt.derivation_node.ValDerivationNode;
2422
import liquidjava.rj_language.opt.derivation_node.VarDerivationNode;
2523
import org.junit.jupiter.api.Test;
26-
import spoon.Launcher;
27-
import spoon.reflect.factory.Factory;
2824

2925
/**
3026
* Test suite for expression simplification using constant propagation and folding
3127
*/
3228
class ExpressionSimplifierTest {
3329

34-
private final Factory factory = new Launcher().getFactory();
35-
private final Context context = Context.getInstance();
36-
3730
@Test
3831
void testNegation() {
3932
// Given: -a && a == 7
@@ -891,81 +884,6 @@ void testInternalToInternalNoFurtherResolution() {
891884
"#a_3 (lower counter) replaced by #b_7 (higher counter); equality collapses to trivial");
892885
}
893886

894-
@Test
895-
void testEntailedConjunctIsRemovedButOriginIsPreserved() {
896-
// Given: b >= 100 && b > 0
897-
// Expected: b >= 100 (b >= 100 implies b > 0)
898-
899-
addIntVariableToContext("b");
900-
Expression b = new Var("b");
901-
Expression bGe100 = new BinaryExpression(b, ">=", new LiteralInt(100));
902-
Expression bGt0 = new BinaryExpression(b, ">", new LiteralInt(0));
903-
Expression fullExpression = new BinaryExpression(bGe100, "&&", bGt0);
904-
905-
ValDerivationNode result = ExpressionSimplifier.simplify(fullExpression);
906-
907-
assertNotNull(result);
908-
assertEquals("b >= 100", result.getValue().toString(),
909-
"The weaker conjunct should be removed when implied by the stronger one");
910-
911-
ValDerivationNode expectedLeft = new ValDerivationNode(bGe100, null);
912-
ValDerivationNode expectedRight = new ValDerivationNode(bGt0, null);
913-
ValDerivationNode expected = new ValDerivationNode(bGe100,
914-
new BinaryDerivationNode(expectedLeft, expectedRight, "&&"));
915-
916-
assertDerivationEquals(expected, result, "Entailment simplification should preserve conjunction origin");
917-
}
918-
919-
@Test
920-
void testStrictComparisonImpliesNonStrictComparison() {
921-
// Given: x > y && x >= y
922-
// Expected: x > y (x > y implies x >= y)
923-
924-
addIntVariableToContext("x");
925-
addIntVariableToContext("y");
926-
Expression x = new Var("x");
927-
Expression y = new Var("y");
928-
Expression xGtY = new BinaryExpression(x, ">", y);
929-
Expression xGeY = new BinaryExpression(x, ">=", y);
930-
Expression fullExpression = new BinaryExpression(xGtY, "&&", xGeY);
931-
932-
ValDerivationNode result = ExpressionSimplifier.simplify(fullExpression);
933-
934-
assertNotNull(result);
935-
assertEquals("x > y", result.getValue().toString(),
936-
"The stricter comparison should be kept when it implies the weaker one");
937-
938-
ValDerivationNode expectedLeft = new ValDerivationNode(xGtY, null);
939-
ValDerivationNode expectedRight = new ValDerivationNode(xGeY, null);
940-
ValDerivationNode expected = new ValDerivationNode(xGtY,
941-
new BinaryDerivationNode(expectedLeft, expectedRight, "&&"));
942-
943-
assertDerivationEquals(expected, result, "Strict comparison simplification should preserve conjunction origin");
944-
}
945-
946-
@Test
947-
void testEquivalentBoundsKeepOneSide() {
948-
// Given: i >= 0 && 0 <= i
949-
// Expected: 0 <= i (both conjuncts express the same condition)
950-
addIntVariableToContext("i");
951-
Expression i = new Var("i");
952-
Expression zeroLeI = new BinaryExpression(new LiteralInt(0), "<=", i);
953-
Expression iGeZero = new BinaryExpression(i, ">=", new LiteralInt(0));
954-
Expression fullExpression = new BinaryExpression(zeroLeI, "&&", iGeZero);
955-
956-
ValDerivationNode result = ExpressionSimplifier.simplify(fullExpression);
957-
958-
assertNotNull(result);
959-
assertEquals("0 <= i", result.getValue().toString(), "Equivalent bounds should collapse to a single conjunct");
960-
961-
ValDerivationNode expectedLeft = new ValDerivationNode(zeroLeI, null);
962-
ValDerivationNode expectedRight = new ValDerivationNode(iGeZero, null);
963-
ValDerivationNode expected = new ValDerivationNode(zeroLeI,
964-
new BinaryDerivationNode(expectedLeft, expectedRight, "&&"));
965-
966-
assertDerivationEquals(expected, result, "Equivalent bounds simplification should preserve conjunction origin");
967-
}
968-
969887
@Test
970888
void testIteTrueConditionSimplifiesToThenBranch() {
971889
// Given: true ? a : b
@@ -1102,47 +1020,78 @@ void testTwoArgAliasWithNormalExpression() {
11021020
assertNull(rightNode.getOrigin());
11031021
}
11041022

1105-
/**
1106-
* Helper method to compare two derivation nodes recursively
1107-
*/
1108-
private void assertDerivationEquals(DerivationNode expected, DerivationNode actual, String message) {
1109-
if (expected == null && actual == null)
1110-
return;
1111-
1112-
assertNotNull(expected);
1113-
assertEquals(expected.getClass(), actual.getClass(), message + ": node types should match");
1114-
if (expected instanceof ValDerivationNode expectedVal) {
1115-
ValDerivationNode actualVal = (ValDerivationNode) actual;
1116-
assertEquals(expectedVal.getValue().toString(), actualVal.getValue().toString(),
1117-
message + ": values should match");
1118-
assertDerivationEquals(expectedVal.getOrigin(), actualVal.getOrigin(), message + " > origin");
1119-
} else if (expected instanceof BinaryDerivationNode expectedBin) {
1120-
BinaryDerivationNode actualBin = (BinaryDerivationNode) actual;
1121-
assertEquals(expectedBin.getOp(), actualBin.getOp(), message + ": operators should match");
1122-
assertDerivationEquals(expectedBin.getLeft(), actualBin.getLeft(), message + " > left");
1123-
assertDerivationEquals(expectedBin.getRight(), actualBin.getRight(), message + " > right");
1124-
} else if (expected instanceof VarDerivationNode expectedVar) {
1125-
VarDerivationNode actualVar = (VarDerivationNode) actual;
1126-
assertEquals(expectedVar.getVar(), actualVar.getVar(), message + ": variables should match");
1127-
} else if (expected instanceof UnaryDerivationNode expectedUnary) {
1128-
UnaryDerivationNode actualUnary = (UnaryDerivationNode) actual;
1129-
assertEquals(expectedUnary.getOp(), actualUnary.getOp(), message + ": operators should match");
1130-
assertDerivationEquals(expectedUnary.getOperand(), actualUnary.getOperand(), message + " > operand");
1131-
} else if (expected instanceof IteDerivationNode expectedIte) {
1132-
IteDerivationNode actualIte = (IteDerivationNode) actual;
1133-
assertDerivationEquals(expectedIte.getCondition(), actualIte.getCondition(), message + " > condition");
1134-
assertDerivationEquals(expectedIte.getThenBranch(), actualIte.getThenBranch(), message + " > then");
1135-
assertDerivationEquals(expectedIte.getElseBranch(), actualIte.getElseBranch(), message + " > else");
1136-
}
1023+
@Test
1024+
void testEntailedConjunctIsRemovedButOriginIsPreserved() {
1025+
// Given: b >= 100 && b > 0
1026+
// Expected: b >= 100 (b >= 100 implies b > 0)
1027+
1028+
addIntVariableToContext("b");
1029+
Expression b = new Var("b");
1030+
Expression bGe100 = new BinaryExpression(b, ">=", new LiteralInt(100));
1031+
Expression bGt0 = new BinaryExpression(b, ">", new LiteralInt(0));
1032+
Expression fullExpression = new BinaryExpression(bGe100, "&&", bGt0);
1033+
1034+
ValDerivationNode result = ExpressionSimplifier.simplify(fullExpression);
1035+
1036+
assertNotNull(result);
1037+
assertEquals("b >= 100", result.getValue().toString(),
1038+
"The weaker conjunct should be removed when implied by the stronger one");
1039+
1040+
ValDerivationNode expectedLeft = new ValDerivationNode(bGe100, null);
1041+
ValDerivationNode expectedRight = new ValDerivationNode(bGt0, null);
1042+
ValDerivationNode expected = new ValDerivationNode(bGe100,
1043+
new BinaryDerivationNode(expectedLeft, expectedRight, "&&"));
1044+
1045+
assertDerivationEquals(expected, result, "Entailment simplification should preserve conjunction origin");
11371046
}
11381047

1139-
/**
1140-
* Helper method to add an integer variable to the context Needed for tests that rely on the SMT-based implication
1141-
* checks The simplifier asks Z3 whether one conjunct implies another, so every variable in those expressions must
1142-
* be in the context
1143-
*/
1144-
private void addIntVariableToContext(String name) {
1145-
context.addVarToContext(name, factory.Type().INTEGER_PRIMITIVE, new Predicate(),
1146-
factory.Code().createCodeSnippetStatement(""));
1048+
@Test
1049+
void testStrictComparisonImpliesNonStrictComparison() {
1050+
// Given: x > y && x >= y
1051+
// Expected: x > y (x > y implies x >= y)
1052+
1053+
addIntVariableToContext("x");
1054+
addIntVariableToContext("y");
1055+
Expression x = new Var("x");
1056+
Expression y = new Var("y");
1057+
Expression xGtY = new BinaryExpression(x, ">", y);
1058+
Expression xGeY = new BinaryExpression(x, ">=", y);
1059+
Expression fullExpression = new BinaryExpression(xGtY, "&&", xGeY);
1060+
1061+
ValDerivationNode result = ExpressionSimplifier.simplify(fullExpression);
1062+
1063+
assertNotNull(result);
1064+
assertEquals("x > y", result.getValue().toString(),
1065+
"The stricter comparison should be kept when it implies the weaker one");
1066+
1067+
ValDerivationNode expectedLeft = new ValDerivationNode(xGtY, null);
1068+
ValDerivationNode expectedRight = new ValDerivationNode(xGeY, null);
1069+
ValDerivationNode expected = new ValDerivationNode(xGtY,
1070+
new BinaryDerivationNode(expectedLeft, expectedRight, "&&"));
1071+
1072+
assertDerivationEquals(expected, result, "Strict comparison simplification should preserve conjunction origin");
1073+
}
1074+
1075+
@Test
1076+
void testEquivalentBoundsKeepOneSide() {
1077+
// Given: i >= 0 && 0 <= i
1078+
// Expected: 0 <= i (both conjuncts express the same condition)
1079+
addIntVariableToContext("i");
1080+
Expression i = new Var("i");
1081+
Expression zeroLeI = new BinaryExpression(new LiteralInt(0), "<=", i);
1082+
Expression iGeZero = new BinaryExpression(i, ">=", new LiteralInt(0));
1083+
Expression fullExpression = new BinaryExpression(zeroLeI, "&&", iGeZero);
1084+
1085+
ValDerivationNode result = ExpressionSimplifier.simplify(fullExpression);
1086+
1087+
assertNotNull(result);
1088+
assertEquals("0 <= i", result.getValue().toString(), "Equivalent bounds should collapse to a single conjunct");
1089+
1090+
ValDerivationNode expectedLeft = new ValDerivationNode(zeroLeI, null);
1091+
ValDerivationNode expectedRight = new ValDerivationNode(iGeZero, null);
1092+
ValDerivationNode expected = new ValDerivationNode(zeroLeI,
1093+
new BinaryDerivationNode(expectedLeft, expectedRight, "&&"));
1094+
1095+
assertDerivationEquals(expected, result, "Equivalent bounds simplification should preserve conjunction origin");
11471096
}
11481097
}

‎liquidjava-verifier/src/test/java/liquidjava/utils/TestUtils.java‎

Lines changed: 61 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -1,13 +1,30 @@
11
package liquidjava.utils;
22

3+
import static org.junit.jupiter.api.Assertions.assertEquals;
4+
import static org.junit.jupiter.api.Assertions.assertNotNull;
5+
36
import java.io.IOException;
47
import java.nio.file.Files;
58
import java.nio.file.Path;
69
import java.util.Optional;
710
import java.util.stream.Stream;
811

12+
import liquidjava.processor.context.Context;
13+
import liquidjava.rj_language.Predicate;
14+
import liquidjava.rj_language.opt.derivation_node.BinaryDerivationNode;
15+
import liquidjava.rj_language.opt.derivation_node.DerivationNode;
16+
import liquidjava.rj_language.opt.derivation_node.IteDerivationNode;
17+
import liquidjava.rj_language.opt.derivation_node.UnaryDerivationNode;
18+
import liquidjava.rj_language.opt.derivation_node.ValDerivationNode;
19+
import liquidjava.rj_language.opt.derivation_node.VarDerivationNode;
20+
import spoon.Launcher;
21+
import spoon.reflect.factory.Factory;
22+
923
public class TestUtils {
1024

25+
private final static Factory factory = new Launcher().getFactory();
26+
private final static Context context = Context.getInstance();
27+
1128
/**
1229
* Determines if the given path indicates that the test should pass
1330
*
@@ -64,4 +81,48 @@ public static Optional<String> getExpectedErrorFromDirectory(Path dirPath) {
6481
}
6582
return Optional.empty();
6683
}
84+
85+
/**
86+
* Helper method to compare two derivation nodes recursively
87+
*/
88+
public static void assertDerivationEquals(DerivationNode expected, DerivationNode actual, String message) {
89+
if (expected == null && actual == null)
90+
return;
91+
92+
assertNotNull(expected);
93+
assertEquals(expected.getClass(), actual.getClass(), message + ": node types should match");
94+
if (expected instanceof ValDerivationNode expectedVal) {
95+
ValDerivationNode actualVal = (ValDerivationNode) actual;
96+
assertEquals(expectedVal.getValue().toString(), actualVal.getValue().toString(),
97+
message + ": values should match");
98+
assertDerivationEquals(expectedVal.getOrigin(), actualVal.getOrigin(), message + " > origin");
99+
} else if (expected instanceof BinaryDerivationNode expectedBin) {
100+
BinaryDerivationNode actualBin = (BinaryDerivationNode) actual;
101+
assertEquals(expectedBin.getOp(), actualBin.getOp(), message + ": operators should match");
102+
assertDerivationEquals(expectedBin.getLeft(), actualBin.getLeft(), message + " > left");
103+
assertDerivationEquals(expectedBin.getRight(), actualBin.getRight(), message + " > right");
104+
} else if (expected instanceof VarDerivationNode expectedVar) {
105+
VarDerivationNode actualVar = (VarDerivationNode) actual;
106+
assertEquals(expectedVar.getVar(), actualVar.getVar(), message + ": variables should match");
107+
} else if (expected instanceof UnaryDerivationNode expectedUnary) {
108+
UnaryDerivationNode actualUnary = (UnaryDerivationNode) actual;
109+
assertEquals(expectedUnary.getOp(), actualUnary.getOp(), message + ": operators should match");
110+
assertDerivationEquals(expectedUnary.getOperand(), actualUnary.getOperand(), message + " > operand");
111+
} else if (expected instanceof IteDerivationNode expectedIte) {
112+
IteDerivationNode actualIte = (IteDerivationNode) actual;
113+
assertDerivationEquals(expectedIte.getCondition(), actualIte.getCondition(), message + " > condition");
114+
assertDerivationEquals(expectedIte.getThenBranch(), actualIte.getThenBranch(), message + " > then");
115+
assertDerivationEquals(expectedIte.getElseBranch(), actualIte.getElseBranch(), message + " > else");
116+
}
117+
}
118+
119+
/**
120+
* Helper method to add an integer variable to the context Needed for tests that rely on the SMT-based implication
121+
* checks The simplifier asks Z3 whether one conjunct implies another, so every variable in those expressions must
122+
* be in the context
123+
*/
124+
public static void addIntVariableToContext(String name) {
125+
context.addVarToContext(name, factory.Type().INTEGER_PRIMITIVE, new Predicate(),
126+
factory.Code().createCodeSnippetStatement(""));
127+
}
67128
}

0 commit comments

Comments
 (0)