Skip to content

Commit f3466c8

Browse files
rcosta358rcosta358
authored
Fix VC Function Substitution (#267)
1 parent f4d1e50 commit f3466c8

6 files changed

Lines changed: 102 additions & 53 deletions

File tree

‎liquidjava-verifier/src/main/java/liquidjava/rj_language/ast/FunctionInvocation.java‎

Lines changed: 5 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -93,7 +93,7 @@ public int hashCode() {
9393
final int prime = 31;
9494
int result = 1;
9595
result = prime * result + ((getArgs() == null) ? 0 : getArgs().hashCode());
96-
result = prime * result + ((name == null) ? 0 : name.hashCode());
96+
result = prime * result + ((name == null) ? 0 : Utils.getSimpleName(name).hashCode()); // same here
9797
return result;
9898
}
9999

@@ -114,7 +114,10 @@ public boolean equals(Object obj) {
114114
if (name == null) {
115115
return other.name == null;
116116
} else {
117-
return name.equals(other.name);
117+
// prefixes are inconsistent for refined class ghost calls: some use the
118+
// original class prefix, others use the caller class prefix
119+
// for now we compare simple names, but prefix handling should be fixed instead of having this workaround
120+
return other.name != null && Utils.getSimpleName(name).equals(Utils.getSimpleName(other.name));
118121
}
119122
}
120123
}

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

Lines changed: 43 additions & 42 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;
@@ -16,47 +19,67 @@
1619
public class VCFunctionSubstitution implements VCSimplificationPass {
1720

1821
/**
19-
* A substitution discovered from a function invocation equality
22+
* A substitution discovered from a function invocation equality. At {@code sourceNode}, remove
23+
* {@code sourceEquality} and in the following nodes replace {@code invocation} with {@code replacement}
2024
*/
21-
private record Substitution(VCImplication node, FunctionInvocation invocation, Expression replacement) {
25+
private record Substitution(VCImplication sourceNode, FunctionInvocation invocation, Expression replacement,
26+
Expression sourceEquality) {
2227
}
2328

2429
/**
2530
* Applies one function invocation substitution in a VC chain
2631
*/
2732
@Override
2833
public VCImplication apply(VCImplication implication) {
29-
VCImplication result = implication.clone();
30-
Optional<Substitution> substitutionOpt = findSubstitution(result);
34+
Optional<Substitution> substitutionOpt = findSubstitution(implication);
3135

3236
if (substitutionOpt.isPresent()) {
3337
Substitution substitution = substitutionOpt.get();
34-
result = substitute(result, substitution.node(), substitution.invocation(), substitution.replacement());
38+
return substitute(implication, substitution.sourceNode(), substitution.invocation(),
39+
substitution.replacement(), substitution.sourceEquality());
3540
}
36-
return result;
41+
return implication;
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
55-
VCImplication result = copyWithRefinement(implication, implication.getRefinement().clone());
56-
result.setNext(substitute(implication.getNext(), node, invocation, replacement));
63+
VCImplication result = copyWithRefinement(implication, implication.getRefinement());
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+
remaining.remove(sourceEquality);
74+
if (remaining.isEmpty())
75+
return null;
76+
77+
Predicate refinement = new Predicate();
78+
for (Expression conjunct : remaining)
79+
refinement = Predicate.createConjunction(refinement, new Predicate(conjunct));
80+
return copyWithRefinement(implication, refinement);
81+
}
82+
6083
/**
6184
* Rewrites every node after the source equality with one function substitution
6285
*/
@@ -75,11 +98,11 @@ private VCImplication substituteSuffix(VCImplication implication, FunctionInvoca
7598
*/
7699
private VCImplication substituteNode(VCImplication implication, FunctionInvocation invocation,
77100
Expression replacement) {
78-
Expression expression = implication.getRefinement().getExpression().clone();
101+
Expression expression = implication.getRefinement().getExpression();
79102
if (!containsExpression(expression, invocation))
80-
return copyWithRefinement(implication, new Predicate(expression));
103+
return copyWithRefinement(implication, implication.getRefinement());
81104

82-
Expression substituted = expression.substitute(invocation, replacement.clone());
105+
Expression substituted = expression.substitute(invocation, replacement);
83106
return copyWithRefinement(implication, new Predicate(substituted));
84107
}
85108

@@ -101,7 +124,7 @@ private Optional<Substitution> findSubstitution(VCImplication implication) {
101124
* Extracts a substitution from one VC node refinement
102125
*/
103126
private Optional<Substitution> getSubstitution(VCImplication implication) {
104-
return getSubstitution(implication, implication.getRefinement().getExpression().clone());
127+
return getSubstitution(implication, implication.getRefinement().getExpression());
105128
}
106129

107130
/**
@@ -121,33 +144,11 @@ private Optional<Substitution> getSubstitution(VCImplication implication, Expres
121144
Expression left = binary.getFirstOperand();
122145
Expression right = binary.getSecondOperand();
123146
if (left instanceof FunctionInvocation invocation && !containsExpression(right, left))
124-
return Optional.of(new Substitution(implication, (FunctionInvocation) invocation.clone(), right.clone()));
147+
return Optional.of(new Substitution(implication, invocation, right, binary));
125148
if (right instanceof FunctionInvocation invocation && !containsExpression(left, right))
126-
return Optional.of(new Substitution(implication, (FunctionInvocation) invocation.clone(), left.clone()));
149+
return Optional.of(new Substitution(implication, invocation, left, binary));
127150

128151
return Optional.empty();
129152
}
130153

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-
}
153154
}

‎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
@@ -10,8 +10,9 @@
1010
*/
1111
public class VCSimplification {
1212

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

1617
/**
1718
* 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)