Skip to content

Commit 6f55e1c

Browse files
rcosta358rcosta358
committed
Fix VC Function Substitution
1 parent 6aa3a40 commit 6f55e1c

5 files changed

Lines changed: 91 additions & 42 deletions

File tree

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

Lines changed: 37 additions & 33 deletions
Original file line numberDiff line numberDiff line change
@@ -1,7 +1,10 @@
11
package liquidjava.rj_language.opt;
22

33
import static liquidjava.rj_language.opt.VCSimplificationUtils.copyWithRefinement;
4+
import static liquidjava.rj_language.opt.VCSimplificationUtils.containsExpression;
45

6+
import java.util.ArrayList;
7+
import java.util.List;
58
import java.util.Optional;
69

710
import liquidjava.processor.VCImplication;
@@ -18,7 +21,8 @@ public class VCFunctionSubstitution implements VCSimplificationPass {
1821
/**
1922
* A substitution discovered from a function invocation equality
2023
*/
21-
private record Substitution(VCImplication node, FunctionInvocation invocation, Expression replacement) {
24+
private record Substitution(VCImplication node, FunctionInvocation invocation, Expression replacement,
25+
Expression sourceEquality) {
2226
}
2327

2428
/**
@@ -31,32 +35,52 @@ public VCImplication apply(VCImplication implication) {
3135

3236
if (substitutionOpt.isPresent()) {
3337
Substitution substitution = substitutionOpt.get();
34-
result = substitute(result, substitution.node(), substitution.invocation(), substitution.replacement());
38+
result = substitute(result, substitution.node(), substitution.invocation(), substitution.replacement(),
39+
substitution.sourceEquality());
3540
}
3641
return result;
3742
}
3843

3944
/**
40-
* Preserves nodes before the source equality and starts rewriting at the source suffix
45+
* Rewrites one VC chain with a single substitution and removes its source equality
4146
*/
4247
private VCImplication substitute(VCImplication implication, VCImplication node, FunctionInvocation invocation,
43-
Expression replacement) {
48+
Expression replacement, Expression sourceEquality) {
4449
if (implication == null)
4550
return null;
4651

47-
// skip the source node to remove it from the chain and start substitution from the next node
52+
// consume the source equality and start substitution from the next node
4853
if (implication == node) {
49-
VCImplication result = copyWithRefinement(implication, implication.getRefinement().clone());
50-
result.setNext(substituteSuffix(implication.getNext(), invocation, replacement));
51-
return result;
54+
VCImplication suffix = substituteSuffix(implication.getNext(), invocation, replacement);
55+
VCImplication source = removeSourceEquality(implication, sourceEquality);
56+
if (source == null)
57+
return suffix;
58+
source.setNext(suffix);
59+
return source;
5260
}
5361

5462
// preserve the current node and continue rewriting the suffix
5563
VCImplication result = copyWithRefinement(implication, implication.getRefinement().clone());
56-
result.setNext(substitute(implication.getNext(), node, invocation, replacement));
64+
result.setNext(substitute(implication.getNext(), node, invocation, replacement, sourceEquality));
5765
return result;
5866
}
5967

68+
/**
69+
* Removes the equality conjunct that supplied the substitution, preserving any sibling conjuncts
70+
*/
71+
private VCImplication removeSourceEquality(VCImplication implication, Expression sourceEquality) {
72+
List<Expression> remaining = new ArrayList<>(implication.getRefinement().getExpression().getConjuncts());
73+
if (!remaining.remove(sourceEquality))
74+
return copyWithRefinement(implication, implication.getRefinement().clone());
75+
if (remaining.isEmpty())
76+
return null;
77+
78+
Predicate refinement = new Predicate();
79+
for (Expression conjunct : remaining)
80+
refinement = Predicate.createConjunction(refinement, new Predicate(conjunct.clone()));
81+
return copyWithRefinement(implication, refinement);
82+
}
83+
6084
/**
6185
* Rewrites every node after the source equality with one function substitution
6286
*/
@@ -121,33 +145,13 @@ private Optional<Substitution> getSubstitution(VCImplication implication, Expres
121145
Expression left = binary.getFirstOperand();
122146
Expression right = binary.getSecondOperand();
123147
if (left instanceof FunctionInvocation invocation && !containsExpression(right, left))
124-
return Optional.of(new Substitution(implication, (FunctionInvocation) invocation.clone(), right.clone()));
148+
return Optional.of(new Substitution(implication, (FunctionInvocation) invocation.clone(), right.clone(),
149+
binary.clone()));
125150
if (right instanceof FunctionInvocation invocation && !containsExpression(left, right))
126-
return Optional.of(new Substitution(implication, (FunctionInvocation) invocation.clone(), left.clone()));
151+
return Optional.of(new Substitution(implication, (FunctionInvocation) invocation.clone(), left.clone(),
152+
binary.clone()));
127153

128154
return Optional.empty();
129155
}
130156

131-
/**
132-
* Checks whether an expression contains another expression
133-
*/
134-
private boolean containsExpression(Expression expression, Expression target) {
135-
if (expression.equals(target))
136-
return true;
137-
138-
for (Expression child : expression.getChildren())
139-
if (containsExpression(child, target))
140-
return true;
141-
return false;
142-
}
143-
144-
/**
145-
* Checks whether a VC suffix contains an expression
146-
*/
147-
private boolean containsExpression(VCImplication implication, Expression target) {
148-
for (VCImplication current = implication; current != null; current = current.getNext())
149-
if (containsExpression(current.getRefinement().getExpression(), target))
150-
return true;
151-
return false;
152-
}
153157
}

‎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/main/java/liquidjava/rj_language/opt/VCSimplificationUtils.java‎

Lines changed: 17 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -28,6 +28,23 @@ public static boolean containsVar(VCImplication implication, String name) {
2828
return false;
2929
}
3030

31+
public static boolean containsExpression(Expression expression, Expression target) {
32+
if (expression.equals(target))
33+
return true;
34+
35+
for (Expression child : expression.getChildren())
36+
if (containsExpression(child, target))
37+
return true;
38+
return false;
39+
}
40+
41+
public static boolean containsExpression(VCImplication implication, Expression target) {
42+
for (VCImplication current = implication; current != null; current = current.getNext())
43+
if (containsExpression(current.getRefinement().getExpression(), target))
44+
return true;
45+
return false;
46+
}
47+
3148
public static boolean isTrue(Expression expression) {
3249
return expression instanceof LiteralBoolean literal && literal.isBooleanTrue();
3350
}

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

Lines changed: 14 additions & 7 deletions
Original file line numberDiff line numberDiff line change
@@ -13,21 +13,21 @@ class VCFunctionSubstitutionTest {
1313
void substitutesExactFunctionInvocationIntoSuffix() {
1414
VCImplication implication = vc("f(x) == 0", "f(y) == f(x) + 1");
1515

16-
assertSimplificationSteps(substitution::apply, implication, step("f(x) == 0", "f(y) == 0 + 1"));
16+
assertSimplificationSteps(substitution::apply, implication, step("f(y) == 0 + 1"));
1717
}
1818

1919
@Test
2020
void substitutesReverseFunctionEquality() {
2121
VCImplication implication = vc("0 == f(x)", "f(y) == f(x) + 1");
2222

23-
assertSimplificationSteps(substitution::apply, implication, step("0 == f(x)", "f(y) == 0 + 1"));
23+
assertSimplificationSteps(substitution::apply, implication, step("f(y) == 0 + 1"));
2424
}
2525

2626
@Test
27-
void preservesSourceNode() {
27+
void consumesSourceNodeWhenSubstitutedInvocationIsGoneFromSuffix() {
2828
VCImplication implication = vc("f(x) == 0", "f(x) > -1");
2929

30-
assertSimplificationSteps(substitution::apply, implication, step("f(x) == 0", "0 > -1"));
30+
assertSimplificationSteps(substitution::apply, implication, step("0 > -1"));
3131
}
3232

3333
@Test
@@ -41,8 +41,8 @@ void doesNotRewriteEarlierNodesFromLaterEquality() {
4141
void skipsUsedUpEqualityAndUsesNextAvailableEquality() {
4242
VCImplication implication = vc("f(x) == 0", "f(y) == f(x) + 1", "f(y) == 1");
4343

44-
assertSimplificationSteps(substitution::apply, implication, step("f(x) == 0", "f(y) == 0 + 1", "f(y) == 1"),
45-
step("f(x) == 0", "f(y) == 0 + 1", "0 + 1 == 1"));
44+
assertSimplificationSteps(substitution::apply, implication, step("f(y) == 0 + 1", "f(y) == 1"),
45+
step("0 + 1 == 1"));
4646
}
4747

4848
@Test
@@ -63,6 +63,13 @@ void ignoresRecursiveFunctionEquality() {
6363
void extractsEqualityFromTopLevelConjunction() {
6464
VCImplication implication = vc("ok && f(x) == 0", "f(y) == f(x) + 1");
6565

66-
assertSimplificationSteps(substitution::apply, implication, step("ok && f(x) == 0", "f(y) == 0 + 1"));
66+
assertSimplificationSteps(substitution::apply, implication, step("ok", "f(y) == 0 + 1"));
67+
}
68+
69+
@Test
70+
void removesOnlySourceEqualityConjunct() {
71+
VCImplication implication = vc("ok && f(x) == 0 && ready", "f(y) == f(x) + 1");
72+
73+
assertSimplificationSteps(substitution::apply, implication, step("ok && ready", "f(y) == 0 + 1"));
6774
}
6875
}

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

Lines changed: 20 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -2,6 +2,7 @@
22

33
import static org.junit.jupiter.api.Assertions.assertTrue;
44
import static org.junit.jupiter.api.Assertions.fail;
5+
import static liquidjava.rj_language.opt.VCSimplificationUtils.containsExpression;
56

67
import java.util.ArrayList;
78
import java.util.List;
@@ -15,6 +16,7 @@
1516
import liquidjava.rj_language.Predicate;
1617
import liquidjava.rj_language.ast.BinaryExpression;
1718
import liquidjava.rj_language.ast.Expression;
19+
import liquidjava.rj_language.ast.FunctionInvocation;
1820
import liquidjava.rj_language.ast.Var;
1921
import liquidjava.smt.SMTEvaluator;
2022
import liquidjava.smt.SMTResult;
@@ -81,10 +83,28 @@ private static Predicate substitutionPremises(VCImplication implication) {
8183
for (VCImplication current = implication; current != null; current = current.getNext()) {
8284
if (isSubstitution(current))
8385
premises = Predicate.createConjunction(premises, current.getRefinement());
86+
for (Expression conjunct : current.getRefinement().getExpression().getConjuncts()) {
87+
if (!isFunctionSubstitution(conjunct, current.getNext()))
88+
continue;
89+
premises = Predicate.createConjunction(premises, new Predicate(conjunct.clone()));
90+
}
8491
}
8592
return premises;
8693
}
8794

95+
private static boolean isFunctionSubstitution(Expression expression, VCImplication suffix) {
96+
if (!(expression instanceof BinaryExpression binary) || !"==".equals(binary.getOperator()))
97+
return false;
98+
99+
Expression left = binary.getFirstOperand();
100+
Expression right = binary.getSecondOperand();
101+
if (left instanceof FunctionInvocation && !containsExpression(right, left))
102+
return containsExpression(suffix, left);
103+
if (right instanceof FunctionInvocation && !containsExpression(left, right))
104+
return containsExpression(suffix, right);
105+
return false;
106+
}
107+
88108
private static boolean isSubstitution(VCImplication implication) {
89109
if (!implication.hasBinder())
90110
return false;

0 commit comments

Comments
 (0)