Skip to content

Commit daa6a97

Browse files
rcosta358rcosta358
committed
Add Property Based Test using JUnit Quickcheck
1 parent 14374c2 commit daa6a97

3 files changed

Lines changed: 238 additions & 10 deletions

File tree

‎liquidjava-verifier/pom.xml‎

Lines changed: 22 additions & 10 deletions
Original file line numberDiff line numberDiff line change
@@ -301,16 +301,28 @@
301301
<artifactId>junit-vintage-engine</artifactId>
302302
<scope>test</scope>
303303
</dependency>
304-
<dependency>
305-
<groupId>org.junit.jupiter</groupId>
306-
<artifactId>junit-jupiter-params</artifactId>
307-
<scope>test</scope>
308-
</dependency>
309-
<dependency>
310-
<groupId>ch.qos.logback</groupId>
311-
<artifactId>logback-classic</artifactId>
312-
<version>1.4.12</version>
313-
</dependency>
304+
<dependency>
305+
<groupId>org.junit.jupiter</groupId>
306+
<artifactId>junit-jupiter-params</artifactId>
307+
<scope>test</scope>
308+
</dependency>
309+
<dependency>
310+
<groupId>com.pholser</groupId>
311+
<artifactId>junit-quickcheck-core</artifactId>
312+
<version>1.0</version>
313+
<scope>test</scope>
314+
</dependency>
315+
<dependency>
316+
<groupId>com.pholser</groupId>
317+
<artifactId>junit-quickcheck-generators</artifactId>
318+
<version>1.0</version>
319+
<scope>test</scope>
320+
</dependency>
321+
<dependency>
322+
<groupId>ch.qos.logback</groupId>
323+
<artifactId>logback-classic</artifactId>
324+
<version>1.4.12</version>
325+
</dependency>
314326
<dependency>
315327
<groupId>org.mdkt.compiler</groupId>
316328
<artifactId>InMemoryJavaCompiler</artifactId>

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

Lines changed: 89 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,89 @@
1+
package liquidjava.rj_language.opt;
2+
3+
import static liquidjava.utils.VCTestUtils.vc;
4+
5+
import com.pholser.junit.quickcheck.generator.GenerationStatus;
6+
import com.pholser.junit.quickcheck.generator.Generator;
7+
import com.pholser.junit.quickcheck.random.SourceOfRandomness;
8+
import liquidjava.processor.VCImplication;
9+
10+
public class VCImplicationGenerator extends Generator<VCImplication> {
11+
12+
static final String[] BINDERS = { "x", "y", "z" };
13+
static final String[] FREE_VARS = { "a", "b", "c" };
14+
private static final String[] COMPARISON_OPS = { "==", "!=", ">=", ">", "<=", "<" };
15+
16+
public VCImplicationGenerator() {
17+
super(VCImplication.class);
18+
}
19+
20+
@Override
21+
public VCImplication generate(SourceOfRandomness random, GenerationStatus status) {
22+
return switch (random.nextInt(0, 5)) {
23+
case 0 -> vc(substitution(random, "x"), comparison(random, "x"));
24+
case 1 -> vc(reverseSubstitution(random, "x"), comparison(random, "x"));
25+
case 2 -> vc(nonSubstitution(random, "x"), substitution(random, "y"), comparison(random, "y"));
26+
case 3 -> vc(substitution(random, "x"), dependentSubstitution(random), comparison(random, "y"));
27+
case 4 -> vc("∀y:int. true", "∀x:int. x == y + 1", comparison(random, "x"));
28+
default -> vc(substitution(random, "x"), substitution(random, "y"), comparison(random, "z"));
29+
};
30+
}
31+
32+
private static String substitution(SourceOfRandomness random, String binder) {
33+
String value = value(random);
34+
if (random.nextBoolean())
35+
return "∀" + binder + ":int. " + binder + " == " + value;
36+
return "∀" + binder + ":int. " + value + " == " + binder;
37+
}
38+
39+
private static String reverseSubstitution(SourceOfRandomness random, String binder) {
40+
return "∀" + binder + ":int. " + value(random) + " == " + binder;
41+
}
42+
43+
private static String dependentSubstitution(SourceOfRandomness random) {
44+
int offset = random.nextInt(-3, 3);
45+
return "∀y:int. y == x " + signed(offset);
46+
}
47+
48+
private static String nonSubstitution(SourceOfRandomness random, String binder) {
49+
if (random.nextBoolean())
50+
return "∀" + binder + ":int. " + binder + " > " + intLiteral(random);
51+
return "∀" + binder + ":int. " + binder + " == " + binder + " " + signed(random.nextInt(1, 5));
52+
}
53+
54+
private static String comparison(SourceOfRandomness random, String preferredVar) {
55+
String left = random.nextBoolean() ? preferredVar : arithmetic(random, preferredVar);
56+
String right = random.nextBoolean() ? intLiteral(random)
57+
: arithmetic(random, FREE_VARS[random.nextInt(0, FREE_VARS.length - 1)]);
58+
return left + " " + COMPARISON_OPS[random.nextInt(0, COMPARISON_OPS.length - 1)] + " " + right;
59+
}
60+
61+
private static String value(SourceOfRandomness random) {
62+
String var = FREE_VARS[random.nextInt(0, FREE_VARS.length - 1)];
63+
return switch (random.nextInt(0, 3)) {
64+
case 0 -> intLiteral(random);
65+
case 1 -> var;
66+
case 2 -> var + " " + signed(random.nextInt(-4, 4));
67+
default -> arithmetic(random, var);
68+
};
69+
}
70+
71+
private static String arithmetic(SourceOfRandomness random, String var) {
72+
int constant = random.nextInt(-3, 3);
73+
return switch (random.nextInt(0, 2)) {
74+
case 0 -> var + " " + signed(constant);
75+
case 1 -> var + " * " + random.nextInt(1, 5);
76+
default -> "(" + var + " " + signed(constant) + ")";
77+
};
78+
}
79+
80+
private static String signed(int value) {
81+
if (value < 0)
82+
return "- " + Math.abs(value);
83+
return "+ " + value;
84+
}
85+
86+
private static String intLiteral(SourceOfRandomness random) {
87+
return Integer.toString(random.nextInt(-7, 7));
88+
}
89+
}

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

Lines changed: 127 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,127 @@
1+
package liquidjava.rj_language.opt;
2+
3+
import static liquidjava.utils.VCTestUtils.vc;
4+
import static org.junit.jupiter.api.Assertions.assertTrue;
5+
6+
import com.pholser.junit.quickcheck.From;
7+
import com.pholser.junit.quickcheck.Property;
8+
import com.pholser.junit.quickcheck.runner.JUnitQuickcheck;
9+
import java.util.ArrayList;
10+
import java.util.List;
11+
import liquidjava.processor.VCImplication;
12+
import liquidjava.processor.context.Context;
13+
import liquidjava.rj_language.Predicate;
14+
import liquidjava.rj_language.SimplifiedPredicate;
15+
import liquidjava.rj_language.ast.BinaryExpression;
16+
import liquidjava.rj_language.ast.Expression;
17+
import liquidjava.rj_language.ast.Var;
18+
import liquidjava.smt.SMTEvaluator;
19+
import liquidjava.smt.SMTResult;
20+
import liquidjava.utils.TestUtils;
21+
import org.junit.runner.RunWith;
22+
23+
@RunWith(JUnitQuickcheck.class)
24+
public class VCSimplificationPropertyBasedTest {
25+
26+
private static final int TRIALS = 800;
27+
28+
@Property(trials = TRIALS)
29+
public void eachSimplificationStepPreservesVcSemantics(@From(VCImplicationGenerator.class) VCImplication vc) {
30+
setUpContext();
31+
VCImplication current = vc;
32+
33+
for (int step = 0; step < VCImplicationGenerator.BINDERS.length; step++) {
34+
VCImplication simplified = VCSimplifier.simplifyOnce(current);
35+
if (sameVc(current, simplified))
36+
break;
37+
38+
assertEquivalent(current, simplified, step);
39+
current = simplified;
40+
}
41+
System.out.println("---------------------------------------------------------");
42+
}
43+
44+
private static void setUpContext() {
45+
Context.getInstance().reinitializeAllContext();
46+
for (String variable : VCImplicationGenerator.BINDERS)
47+
TestUtils.addIntVariableToContext(variable);
48+
for (String variable : VCImplicationGenerator.FREE_VARS)
49+
TestUtils.addIntVariableToContext(variable);
50+
}
51+
52+
private static boolean sameVc(VCImplication left, VCImplication right) {
53+
return left.toString().equals(right.toString());
54+
}
55+
56+
private static void assertEquivalent(VCImplication unsimplified, VCImplication simplified, int step) {
57+
Predicate premises = substitutionPremises(unsimplified);
58+
Predicate unsimplifiedFormula = Predicate.createConjunction(premises, new Predicate(vcFormula(unsimplified)));
59+
Predicate simplifiedFormula = Predicate.createConjunction(premises, new Predicate(vcFormula(simplified)));
60+
System.out.println(unsimplifiedFormula);
61+
System.out.println("=>");
62+
System.out.println(simplifiedFormula);
63+
assertImplies(unsimplifiedFormula, simplifiedFormula, unsimplified, simplified, step,
64+
"unsimplified => simplified");
65+
assertImplies(simplifiedFormula, unsimplifiedFormula, unsimplified, simplified, step,
66+
"simplified => unsimplified");
67+
}
68+
69+
private static Expression vcFormula(VCImplication implication) {
70+
Expression refinement = activeExpression(implication.getRefinement()).clone();
71+
if (!implication.hasNext())
72+
return refinement;
73+
return new BinaryExpression(refinement, "-->", vcFormula(implication.getNext()));
74+
}
75+
76+
private static Predicate substitutionPremises(VCImplication implication) {
77+
Predicate premises = new Predicate();
78+
for (VCImplication current = implication; current != null; current = current.getNext()) {
79+
if (isSubstitution(current))
80+
premises = Predicate.createConjunction(premises, current.getRefinement());
81+
}
82+
return premises;
83+
}
84+
85+
private static boolean isSubstitution(VCImplication implication) {
86+
if (!implication.hasBinder())
87+
return false;
88+
89+
Expression refinement = activeExpression(implication.getRefinement());
90+
if (!(refinement instanceof BinaryExpression binary) || !"==".equals(binary.getOperator()))
91+
return false;
92+
93+
String name = implication.getName();
94+
Expression left = binary.getFirstOperand();
95+
Expression right = binary.getSecondOperand();
96+
return isVar(left, name) && !containsVariable(right, name)
97+
|| isVar(right, name) && !containsVariable(left, name);
98+
}
99+
100+
private static void assertImplies(Predicate antecedent, Predicate consequent, VCImplication unsimplified,
101+
VCImplication simplified, int step, String direction) {
102+
try {
103+
SMTResult result = new SMTEvaluator().verifySubtype(antecedent, consequent, Context.getInstance(), true);
104+
assertTrue(result.isOk(), () -> direction + " failed at step " + step + "\nunsimplified: " + unsimplified
105+
+ "\nsimplified: " + simplified);
106+
} catch (Exception e) {
107+
throw new AssertionError(direction + " could not be checked at step " + step + "\nunsimplified: "
108+
+ unsimplified + "\nsimplified: " + simplified, e);
109+
}
110+
}
111+
112+
private static boolean isVar(Expression expression, String name) {
113+
return expression instanceof Var var && name.equals(var.getName());
114+
}
115+
116+
private static boolean containsVariable(Expression expression, String name) {
117+
List<String> names = new ArrayList<>();
118+
expression.getVariableNames(names);
119+
return names.contains(name);
120+
}
121+
122+
private static Expression activeExpression(Predicate predicate) {
123+
if (predicate instanceof SimplifiedPredicate simplified)
124+
return simplified.getSimplifiedPredicate().getExpression();
125+
return predicate.getExpression();
126+
}
127+
}

0 commit comments

Comments
 (0)