Skip to content

Commit 3402d89

Browse files
rcosta358rcosta358
authored
Add VC Function Substitution (#258)
1 parent fa8114a commit 3402d89

6 files changed

Lines changed: 313 additions & 3 deletions

File tree

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

Lines changed: 156 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,156 @@
1+
package liquidjava.rj_language.opt;
2+
3+
import java.util.Optional;
4+
5+
import liquidjava.processor.SimplifiedVCImplication;
6+
import liquidjava.processor.VCImplication;
7+
import liquidjava.rj_language.Predicate;
8+
import liquidjava.rj_language.ast.BinaryExpression;
9+
import liquidjava.rj_language.ast.Expression;
10+
import liquidjava.rj_language.ast.FunctionInvocation;
11+
import liquidjava.rj_language.ast.GroupExpression;
12+
13+
/**
14+
* Simplifies VCImplication chains by propagating exact function invocation equalities
15+
*/
16+
public class VCFunctionSubstitution implements VCSimplificationPass {
17+
18+
/**
19+
* A substitution discovered from a function invocation equality
20+
*/
21+
private record Substitution(VCImplication node, FunctionInvocation invocation, Expression replacement) {
22+
}
23+
24+
/**
25+
* Applies one function invocation substitution in a VC chain
26+
*/
27+
@Override
28+
public VCImplication apply(VCImplication implication) {
29+
VCImplication result = implication.clone();
30+
Optional<Substitution> substitutionOpt = findSubstitution(result);
31+
32+
if (substitutionOpt.isPresent()) {
33+
Substitution substitution = substitutionOpt.get();
34+
result = substitute(result, substitution.node(), substitution.invocation(), substitution.replacement());
35+
}
36+
return result;
37+
}
38+
39+
/**
40+
* Preserves nodes before the source equality and starts rewriting at the source suffix
41+
*/
42+
private VCImplication substitute(VCImplication implication, VCImplication node, FunctionInvocation invocation,
43+
Expression replacement) {
44+
if (implication == null)
45+
return null;
46+
47+
// skip the source node to remove it from the chain and start substitution from the next node
48+
if (implication == node) {
49+
VCImplication result = implication.copyWithRefinement(implication.getRefinement().clone());
50+
result.setNext(substituteSuffix(implication.getNext(), node, invocation, replacement));
51+
return result;
52+
}
53+
54+
// preserve the current node and continue rewriting the suffix
55+
VCImplication result = implication.copyWithRefinement(implication.getRefinement().clone());
56+
result.setNext(substitute(implication.getNext(), node, invocation, replacement));
57+
return result;
58+
}
59+
60+
/**
61+
* Rewrites every node after the source equality with one function substitution
62+
*/
63+
private VCImplication substituteSuffix(VCImplication implication, VCImplication source,
64+
FunctionInvocation invocation, Expression replacement) {
65+
if (implication == null)
66+
return null;
67+
68+
VCImplication result = substituteNode(implication, source, invocation, replacement);
69+
result.setNext(substituteSuffix(implication.getNext(), source, invocation, replacement));
70+
return result;
71+
}
72+
73+
/**
74+
* Substitutes one exact function invocation inside one VC node while preserving simplification metadata
75+
*/
76+
private VCImplication substituteNode(VCImplication implication, VCImplication source, FunctionInvocation invocation,
77+
Expression replacement) {
78+
Expression expression = implication.getRefinement().getExpression().clone();
79+
if (!containsExpression(expression, invocation))
80+
return implication.copyWithRefinement(new Predicate(expression));
81+
82+
Expression substituted = expression.substitute(invocation, replacement.clone());
83+
return new SimplifiedVCImplication(implication, new Predicate(substituted), source);
84+
}
85+
86+
/**
87+
* Finds the first function substitution candidate that is used in the remaining suffix
88+
*/
89+
private Optional<Substitution> findSubstitution(VCImplication implication) {
90+
if (implication == null)
91+
return Optional.empty();
92+
93+
Optional<Substitution> current = getSubstitution(implication);
94+
if (current.isPresent() && containsExpression(implication.getNext(), current.get().invocation()))
95+
return current;
96+
97+
return findSubstitution(implication.getNext());
98+
}
99+
100+
/**
101+
* Extracts a substitution from one VC node refinement
102+
*/
103+
private Optional<Substitution> getSubstitution(VCImplication implication) {
104+
return getSubstitution(implication, implication.getRefinement().getExpression().clone());
105+
}
106+
107+
/**
108+
* Extracts a substitution from a top-level equality or conjunction
109+
*/
110+
private Optional<Substitution> getSubstitution(VCImplication implication, Expression expression) {
111+
if (expression instanceof GroupExpression group)
112+
return getSubstitution(implication, group.getExpression());
113+
114+
if (expression instanceof BinaryExpression binary && "&&".equals(binary.getOperator())) {
115+
Optional<Substitution> left = getSubstitution(implication, binary.getFirstOperand());
116+
if (left.isPresent())
117+
return left;
118+
return getSubstitution(implication, binary.getSecondOperand());
119+
}
120+
121+
if (!(expression instanceof BinaryExpression binary) || !"==".equals(binary.getOperator()))
122+
return Optional.empty();
123+
124+
Expression left = binary.getFirstOperand();
125+
Expression right = binary.getSecondOperand();
126+
if (left instanceof FunctionInvocation invocation && !containsExpression(right, left))
127+
return Optional.of(new Substitution(implication, (FunctionInvocation) invocation.clone(), right.clone()));
128+
if (right instanceof FunctionInvocation invocation && !containsExpression(left, right))
129+
return Optional.of(new Substitution(implication, (FunctionInvocation) invocation.clone(), left.clone()));
130+
131+
return Optional.empty();
132+
}
133+
134+
/**
135+
* Checks whether an expression contains another expression
136+
*/
137+
private boolean containsExpression(Expression expression, Expression target) {
138+
if (expression.equals(target))
139+
return true;
140+
141+
for (Expression child : expression.getChildren())
142+
if (containsExpression(child, target))
143+
return true;
144+
return false;
145+
}
146+
147+
/**
148+
* Checks whether a VC suffix contains an expression
149+
*/
150+
private boolean containsExpression(VCImplication implication, Expression target) {
151+
for (VCImplication current = implication; current != null; current = current.getNext())
152+
if (containsExpression(current.getRefinement().getExpression(), target))
153+
return true;
154+
return false;
155+
}
156+
}

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

Lines changed: 3 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -9,8 +9,9 @@
99
*/
1010
public class VCSimplification {
1111

12-
private static final List<VCSimplificationPass> PASSES = List.of(new VCSubstitution(), new VCBinderSimplification(),
13-
new VCFolding(), new VCArithmeticSimplification(), new VCLogicalSimplification());
12+
private static final List<VCSimplificationPass> PASSES = List.of(new VCSubstitution(), new VCFunctionSubstitution(),
13+
new VCBinderSimplification(), new VCFolding(), new VCArithmeticSimplification(),
14+
new VCLogicalSimplification());
1415

1516
/**
1617
* Applies all available simplification steps to a VC chain until a fixed point is reached

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

Lines changed: 75 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,75 @@
1+
package liquidjava.rj_language.opt;
2+
3+
import static liquidjava.utils.VCTestUtils.*;
4+
5+
import liquidjava.processor.VCImplication;
6+
import org.junit.jupiter.api.Test;
7+
8+
class VCFunctionSubstitutionTest {
9+
10+
private final VCFunctionSubstitution substitution = new VCFunctionSubstitution();
11+
12+
@Test
13+
void substitutesExactFunctionInvocationIntoSuffix() {
14+
VCImplication implication = vc("f(x) == 0", "f(y) == f(x) + 1");
15+
16+
assertSimplificationSteps(substitution::apply, implication,
17+
chain(expect("f(x) == 0"), expect("f(y) == 0 + 1", "f(x) == 0")));
18+
}
19+
20+
@Test
21+
void substitutesReverseFunctionEquality() {
22+
VCImplication implication = vc("0 == f(x)", "f(y) == f(x) + 1");
23+
24+
assertSimplificationSteps(substitution::apply, implication,
25+
chain(expect("0 == f(x)"), expect("f(y) == 0 + 1", "0 == f(x)")));
26+
}
27+
28+
@Test
29+
void preservesSourceNode() {
30+
VCImplication implication = vc("f(x) == 0", "f(x) > -1");
31+
32+
assertSimplificationSteps(substitution::apply, implication,
33+
chain(expect("f(x) == 0"), expect("0 > -1", "f(x) == 0")));
34+
}
35+
36+
@Test
37+
void doesNotRewriteEarlierNodesFromLaterEquality() {
38+
VCImplication implication = vc("f(x) > 0", "f(x) == 1");
39+
40+
assertSimplificationSteps(substitution::apply, implication, chain(expect("f(x) > 0"), expect("f(x) == 1")));
41+
}
42+
43+
@Test
44+
void skipsUsedUpEqualityAndUsesNextAvailableEquality() {
45+
VCImplication implication = vc("f(x) == 0", "f(y) == f(x) + 1", "f(y) == 1");
46+
47+
assertSimplificationSteps(substitution::apply, implication,
48+
chain(expect("f(x) == 0"), expect("f(y) == 0 + 1", "f(x) == 0"), expect("f(y) == 1")),
49+
chain(expect("f(x) == 0"), expect("f(y) == 0 + 1", "f(x) == 0"),
50+
expect("0 + 1 == 1", "f(y) == 0 + 1")));
51+
}
52+
53+
@Test
54+
void doesNotGeneralizeAcrossDifferentArguments() {
55+
VCImplication implication = vc("f(x) == 0", "f(y) == 0");
56+
57+
assertSimplificationSteps(substitution::apply, implication, chain(expect("f(x) == 0"), expect("f(y) == 0")));
58+
}
59+
60+
@Test
61+
void ignoresRecursiveFunctionEquality() {
62+
VCImplication implication = vc("f(x) == f(x) + 1", "f(x) > 0");
63+
64+
assertSimplificationSteps(substitution::apply, implication,
65+
chain(expect("f(x) == f(x) + 1"), expect("f(x) > 0")));
66+
}
67+
68+
@Test
69+
void extractsEqualityFromTopLevelConjunction() {
70+
VCImplication implication = vc("ok && f(x) == 0", "f(y) == f(x) + 1");
71+
72+
assertSimplificationSteps(substitution::apply, implication,
73+
chain(expect("ok && f(x) == 0"), expect("f(y) == 0 + 1", "ok && f(x) == 0")));
74+
}
75+
}

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

Lines changed: 60 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -11,6 +11,7 @@ public class VCImplicationGenerator extends Generator<VCImplication> {
1111

1212
public static final String[] BINDERS = { "x", "y", "z", "w" };
1313
public static final String[] FREE_VARS = { "a", "b", "c", "d" };
14+
public static final String[] FUNCTIONS = { "f", "g" };
1415
private static final String[] COMPARISON_OPS = { "==", "!=", ">=", ">", "<=", "<" };
1516
private static final String[] BOOLEAN_OPS = { "&&", "||", "-->", "==", "!=" };
1617
private static final String[] ARITHMETIC_OPS = { "+", "-", "*" };
@@ -21,7 +22,7 @@ public VCImplicationGenerator() {
2122

2223
@Override
2324
public VCImplication generate(SourceOfRandomness random, GenerationStatus status) {
24-
return switch (random.nextInt(0, 14)) {
25+
return switch (random.nextInt(0, 18)) {
2526
case 0 -> vc(substitution(random, "x"), comparison(random, "x"));
2627
case 1 -> vc(reverseSubstitution(random, "x"), comparison(random, "x"));
2728
case 2 -> vc(nonSubstitution(random, "x"), substitution(random, "y"), comparison(random, "y"));
@@ -36,6 +37,11 @@ public VCImplication generate(SourceOfRandomness random, GenerationStatus status
3637
case 11 -> vc(logicalIdentity(random));
3738
case 12 -> vc(unusedTrueBinder(random));
3839
case 13 -> vc(falseBinder(random));
40+
case 14 -> exactFunctionSubstitution(random);
41+
case 15 -> reverseFunctionSubstitution(random);
42+
case 16 -> chainedFunctionSubstitution(random);
43+
case 17 -> differentArgumentFunctionSubstitution(random);
44+
case 18 -> recursiveFunctionSubstitution(random);
3945
default -> vc(substitution(random, "x"), substitution(random, "y"), foldableComparison(random));
4046
};
4147
}
@@ -62,6 +68,59 @@ private static String nonSubstitution(SourceOfRandomness random, String binder)
6268
return "∀" + binder + ":int. " + binder + " == " + binder + " " + signed(random.nextInt(1, 5));
6369
}
6470

71+
private static VCImplication exactFunctionSubstitution(SourceOfRandomness random) {
72+
String function = functionName(random);
73+
return vc(functionSubstitution(random, function, "a"), functionUse(random, function, "a"));
74+
}
75+
76+
private static VCImplication reverseFunctionSubstitution(SourceOfRandomness random) {
77+
String function = functionName(random);
78+
return vc(reverseFunctionSubstitution(random, function, "a"), functionUse(random, function, "a"));
79+
}
80+
81+
private static VCImplication chainedFunctionSubstitution(SourceOfRandomness random) {
82+
String function = functionName(random);
83+
return vc(functionSubstitution(random, function, "a"), dependentFunctionSubstitution(random, function),
84+
functionUse(random, function, "b"));
85+
}
86+
87+
private static VCImplication differentArgumentFunctionSubstitution(SourceOfRandomness random) {
88+
String function = functionName(random);
89+
return vc(functionSubstitution(random, function, "a"), functionUse(random, function, "b"));
90+
}
91+
92+
private static VCImplication recursiveFunctionSubstitution(SourceOfRandomness random) {
93+
String function = functionName(random);
94+
String invocation = functionInvocation(function, "a");
95+
return vc(invocation + " == " + invocation + " " + signed(random.nextInt(1, 5)),
96+
functionUse(random, function, "a"));
97+
}
98+
99+
private static String functionSubstitution(SourceOfRandomness random, String function, String argument) {
100+
return functionInvocation(function, argument) + " == " + value(random);
101+
}
102+
103+
private static String reverseFunctionSubstitution(SourceOfRandomness random, String function, String argument) {
104+
return value(random) + " == " + functionInvocation(function, argument);
105+
}
106+
107+
private static String dependentFunctionSubstitution(SourceOfRandomness random, String function) {
108+
return functionInvocation(function, "b") + " == " + functionInvocation(function, "a") + " "
109+
+ signed(random.nextInt(-3, 3));
110+
}
111+
112+
private static String functionUse(SourceOfRandomness random, String function, String argument) {
113+
return functionInvocation(function, argument) + " " + comparisonOperator(random) + " " + intLiteral(random);
114+
}
115+
116+
private static String functionInvocation(String function, String argument) {
117+
return function + "(" + argument + ")";
118+
}
119+
120+
private static String functionName(SourceOfRandomness random) {
121+
return FUNCTIONS[random.nextInt(0, FUNCTIONS.length - 1)];
122+
}
123+
65124
private static String[] unusedTrueBinder(SourceOfRandomness random) {
66125
return new String[] { "∀x:int. true", comparison(random, "a") };
67126
}

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

Lines changed: 7 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -11,6 +11,7 @@
1111
import com.pholser.junit.quickcheck.runner.JUnitQuickcheck;
1212
import liquidjava.processor.VCImplication;
1313
import liquidjava.processor.context.Context;
14+
import liquidjava.processor.context.GhostFunction;
1415
import liquidjava.rj_language.Predicate;
1516
import liquidjava.rj_language.ast.BinaryExpression;
1617
import liquidjava.rj_language.ast.Expression;
@@ -19,12 +20,15 @@
1920
import liquidjava.smt.SMTResult;
2021
import liquidjava.utils.TestUtils;
2122
import org.junit.runner.RunWith;
23+
import spoon.Launcher;
24+
import spoon.reflect.factory.Factory;
2225

2326
@RunWith(JUnitQuickcheck.class)
2427
public class VCSimplificationPropertyBasedTest {
2528

2629
private static final int TRIALS = 50; // number of random VCs to test
2730
private static final int MAX_STEPS = 20; // to prevent infinite loops in case of non-termination
31+
private static final Factory FACTORY = new Launcher().getFactory();
2832

2933
@Property(trials = TRIALS)
3034
public void eachSimplificationStepPreservesVcSemantics(@From(VCImplicationGenerator.class) VCImplication vc) {
@@ -47,6 +51,9 @@ private static void setUpContext() {
4751
TestUtils.addIntVariableToContext(variable);
4852
for (String variable : VCImplicationGenerator.FREE_VARS)
4953
TestUtils.addIntVariableToContext(variable);
54+
for (String function : VCImplicationGenerator.FUNCTIONS)
55+
Context.getInstance().addGhostFunction(
56+
new GhostFunction(function, List.of("int"), FACTORY.Type().INTEGER_PRIMITIVE, FACTORY, ""));
5057
}
5158

5259
private static void assertEquivalent(VCImplication unsimplified, VCImplication simplified, int step) {

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

Lines changed: 12 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -144,6 +144,18 @@ void simplifyAppliesLongSubstitutionChainBeforeReachingFixedPoint() {
144144
chain(expect("3 == 3", "2 + 1 == 3")), chain(expect("true", "3 == 3")));
145145
}
146146

147+
@Test
148+
void simplifyPropagatesFunctionInvocationEqualitiesBeforeReachingFixedPoint() {
149+
VCImplication implication = vc("f(x) == 0", "f(y) == f(x) + 1", "f(y) == 1");
150+
151+
assertSimplificationSteps(VCSimplification::simplifyOnce, implication,
152+
chain(expect("f(x) == 0"), expect("f(y) == 0 + 1", "f(x) == 0"), expect("f(y) == 1")),
153+
chain(expect("f(x) == 0"), expect("f(y) == 0 + 1", "f(x) == 0"), expect("0 + 1 == 1", "f(y) == 0 + 1")),
154+
chain(expect("f(x) == 0"), expect("f(y) == 1", "f(y) == 0 + 1"), expect("0 + 1 == 1", "f(y) == 0 + 1")),
155+
chain(expect("f(x) == 0"), expect("f(y) == 1", "f(y) == 0 + 1"), expect("1 == 1", "0 + 1 == 1")),
156+
chain(expect("f(x) == 0"), expect("f(y) == 1", "f(y) == 0 + 1"), expect("true", "1 == 1")));
157+
}
158+
147159
@Test
148160
void simplifyCombinesSubstitutionAndNestedFoldingAcrossFixedPoint() {
149161
VCImplication implication = vc("∀x:int. x == 1", "∀y:int. y == x + 2", "y - 1 == 2");

0 commit comments

Comments
 (0)