Skip to content

Commit ddf15ea

Browse files
rcosta358rcosta358
committed
Add VC Substitution
1 parent dfb80ab commit ddf15ea

6 files changed

Lines changed: 435 additions & 0 deletions

File tree

‎liquidjava-verifier/src/main/java/liquidjava/processor/VCImplication.java‎

Lines changed: 8 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -47,6 +47,14 @@ public VCImplication getNext() {
4747
return next;
4848
}
4949

50+
public boolean hasNext() {
51+
return next != null;
52+
}
53+
54+
public boolean hasBinder() {
55+
return name != null && type != null;
56+
}
57+
5058
public String toString() {
5159
if (name != null && type != null) {
5260
String qualType = type.getQualifiedName();

‎liquidjava-verifier/src/main/java/liquidjava/rj_language/SimplifiedPredicate.java‎

Lines changed: 5 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -88,6 +88,11 @@ public String getType() {
8888
return type;
8989
}
9090

91+
@Override
92+
public String toString() {
93+
return name + ":" + type;
94+
}
95+
9196
@Override
9297
public int hashCode() {
9398
return Objects.hash(name, type);

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

Lines changed: 10 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,10 @@
1+
package liquidjava.rj_language.opt;
2+
3+
import liquidjava.processor.VCImplication;
4+
5+
public class VCSimplifier {
6+
7+
public static VCImplication simplifyOnce(VCImplication implication) {
8+
return VCSubstitution.apply(implication);
9+
}
10+
}

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

Lines changed: 183 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,183 @@
1+
package liquidjava.rj_language.opt;
2+
3+
import java.util.ArrayList;
4+
import java.util.List;
5+
import java.util.Optional;
6+
7+
import liquidjava.processor.VCImplication;
8+
import liquidjava.rj_language.Predicate;
9+
import liquidjava.rj_language.ast.BinaryExpression;
10+
import liquidjava.rj_language.ast.Expression;
11+
import liquidjava.rj_language.ast.SimplifiedExpression;
12+
import liquidjava.rj_language.ast.Var;
13+
14+
/**
15+
* Simplifies VCImplication chains by replacing binder equalities with their known values
16+
*/
17+
public class VCSubstitution {
18+
19+
/**
20+
* A substitution discovered from an implication node
21+
*/
22+
private record Substitution(VCImplication source, Expression value) {
23+
}
24+
25+
/**
26+
* Applies all available binder equality substitutions in a VC chain
27+
*/
28+
public static VCImplication apply(VCImplication implication) {
29+
if (implication == null)
30+
return null;
31+
32+
VCImplication result = implication.clone();
33+
Optional<VCSubstitution.Substitution> substitutionOpt = VCSubstitution.findSubstitution(result);
34+
35+
// keep applying substitutions until there are no more substitutions available
36+
while (substitutionOpt.isPresent()) {
37+
VCSubstitution.Substitution substitution = substitutionOpt.get();
38+
result = VCSubstitution.substitute(result, substitution.source(), substitution.value());
39+
substitutionOpt = VCSubstitution.findSubstitution(result);
40+
}
41+
return result;
42+
}
43+
44+
/**
45+
* Applies one substitution in a VC chain
46+
*/
47+
public static VCImplication applyOnce(VCImplication implication) {
48+
if (implication == null)
49+
return null;
50+
51+
VCImplication result = implication.clone();
52+
Optional<VCSubstitution.Substitution> substitutionOpt = VCSubstitution.findSubstitution(result);
53+
54+
// apply only the first available substitution
55+
if (substitutionOpt.isPresent()) {
56+
VCSubstitution.Substitution substitution = substitutionOpt.get();
57+
result = VCSubstitution.substitute(result, substitution.source(), substitution.value());
58+
}
59+
return result;
60+
}
61+
62+
/**
63+
* Rewrites one VC chain with a single substitution and removes its source node
64+
*/
65+
private static VCImplication substitute(VCImplication implication, VCImplication source, Expression value) {
66+
if (implication == null)
67+
return null;
68+
69+
// skip the source node to remove it from the chain and start substitution from the next node
70+
if (implication == source)
71+
return substitute(implication.getNext(), source, value);
72+
73+
Predicate refinement = substituteRefinement(implication.getRefinement(), source, value);
74+
VCImplication result = copyWithRefinement(implication, refinement);
75+
result.setNext(substitute(implication.getNext(), source, value));
76+
return result;
77+
}
78+
79+
/**
80+
* Substitutes a source binder inside one predicate while preserving simplification metadata
81+
*/
82+
private static Predicate substituteRefinement(Predicate refinement, VCImplication source, Expression value) {
83+
Expression expression = refinement.getExpression();
84+
Expression active = activeExpression(expression);
85+
SimplifiedExpression.Binder binder = new SimplifiedExpression.Binder(source.getName(), source.getType());
86+
Expression substituted = active.substitute(new Var(binder.getName()), value.clone());
87+
88+
return new Predicate(new SimplifiedExpression(substituted, originExpression(expression),
89+
bindersAfterSubstitution(expression, active, binder)));
90+
}
91+
92+
/**
93+
* Copies an implication node with a replacement refinement
94+
*/
95+
private static VCImplication copyWithRefinement(VCImplication implication, Predicate refinement) {
96+
if (implication.hasBinder())
97+
return new VCImplication(implication.getName(), implication.getType(), refinement);
98+
return new VCImplication(refinement);
99+
}
100+
101+
/**
102+
* Returns the expression that should be shown as the original formula
103+
*/
104+
private static Expression originExpression(Expression expression) {
105+
if (expression instanceof SimplifiedExpression simplified)
106+
return simplified.getOrigin().clone();
107+
return expression.clone();
108+
}
109+
110+
/**
111+
* Builds the binder metadata after one substitution
112+
*/
113+
private static List<SimplifiedExpression.Binder> bindersAfterSubstitution(Expression expression, Expression active,
114+
SimplifiedExpression.Binder binder) {
115+
List<SimplifiedExpression.Binder> binders = expression instanceof SimplifiedExpression previous
116+
? new ArrayList<>(previous.getBinders()) : new ArrayList<>();
117+
if (containsVariable(active, binder.getName()) && !binders.contains(binder))
118+
binders.add(binder);
119+
return binders;
120+
}
121+
122+
/**
123+
* Finds the first substitution candidate in the VC chain
124+
*/
125+
private static Optional<Substitution> findSubstitution(VCImplication implication) {
126+
if (implication == null)
127+
return Optional.empty();
128+
129+
Optional<Substitution> current = getSubstitution(implication);
130+
if (current.isPresent())
131+
return current;
132+
133+
return findSubstitution(implication.getNext());
134+
}
135+
136+
/**
137+
* Extracts a substitution from one binder equality
138+
*/
139+
private static Optional<Substitution> getSubstitution(VCImplication implication) {
140+
if (!implication.hasBinder())
141+
return Optional.empty();
142+
143+
Expression refinement = activeExpression(implication.getRefinement().getExpression());
144+
if (!(refinement instanceof BinaryExpression binary) || !"==".equals(binary.getOperator()))
145+
return Optional.empty();
146+
147+
String name = implication.getName();
148+
Expression left = binary.getFirstOperand();
149+
Expression right = binary.getSecondOperand();
150+
151+
if (isVar(left, name) && !containsVariable(right, name))
152+
return Optional.of(new Substitution(implication, right.clone()));
153+
if (isVar(right, name) && !containsVariable(left, name))
154+
return Optional.of(new Substitution(implication, left.clone()));
155+
156+
return Optional.empty();
157+
}
158+
159+
/**
160+
* Checks whether an expression is a variable with a given name
161+
*/
162+
private static boolean isVar(Expression expression, String name) {
163+
return expression instanceof Var var && name.equals(var.getName());
164+
}
165+
166+
/**
167+
* Checks whether an expression contains a variable name
168+
*/
169+
private static boolean containsVariable(Expression expression, String name) {
170+
List<String> names = new ArrayList<>();
171+
expression.getVariableNames(names);
172+
return names.contains(name);
173+
}
174+
175+
/**
176+
* Returns the expression used for matching and substitution
177+
*/
178+
private static Expression activeExpression(Expression expression) {
179+
if (expression instanceof SimplifiedExpression simplified)
180+
return simplified.getSimplifiedExpression().clone();
181+
return expression.clone();
182+
}
183+
}

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

Lines changed: 100 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,100 @@
1+
package liquidjava.rj_language.opt;
2+
3+
import static liquidjava.utils.VCTestUtils.*;
4+
import static org.junit.jupiter.api.Assertions.assertNotSame;
5+
import static org.junit.jupiter.api.Assertions.assertNull;
6+
7+
import liquidjava.processor.VCImplication;
8+
import org.junit.jupiter.api.Test;
9+
10+
class VCSubstitutionTest {
11+
12+
@Test
13+
void applyReturnsNullForNullImplication() {
14+
assertNull(VCSubstitution.apply(null));
15+
}
16+
17+
@Test
18+
void substitutesBinderEqualityIntoWholeChain() {
19+
VCImplication implication = vc("∀x:int. x == 3", "x > 0");
20+
21+
VCImplication result = VCSubstitution.apply(implication);
22+
23+
assertSimplifiedVC(result, simplified("3 > 0", "x > 0", "x:int"));
24+
}
25+
26+
@Test
27+
void substitutesReverseBinderEquality() {
28+
VCImplication implication = vc("∀x:int. 3 == x", "x > 0");
29+
30+
VCImplication result = VCSubstitution.apply(implication);
31+
32+
assertSimplifiedVC(result, simplified("3 > 0", "x > 0", "x:int"));
33+
}
34+
35+
@Test
36+
void substitutesCompoundKnownValue() {
37+
VCImplication implication = vc("∀x:int. x == y + 1", "x > y");
38+
39+
VCImplication result = VCSubstitution.apply(implication);
40+
41+
assertSimplifiedVC(result, simplified("y + 1 > y", "x > y", "x:int"));
42+
}
43+
44+
@Test
45+
void usesFirstSubstitutionFoundInChain() {
46+
VCImplication implication = vc("∀x:int. x > 0", "∀y:int. y == 4", "x + y > 0");
47+
48+
VCImplication result = VCSubstitution.apply(implication);
49+
50+
assertSimplifiedVC(result, simplified("x > 0", "x > 0", ""), simplified("x + 4 > 0", "x + y > 0", "y:int"));
51+
}
52+
53+
@Test
54+
void substitutesInnerKnownValueAcrossNestedImplications() {
55+
VCImplication implication = vc("∀x:int. true", "∀y:int. y == 1", "∀z:int. z > y", "y + z > 0");
56+
57+
VCImplication result = VCSubstitution.apply(implication);
58+
59+
assertSimplifiedVC(result, simplified("true", "true", ""), simplified("z > 1", "z > y", "y:int"),
60+
simplified("1 + z > 0", "y + z > 0", "y:int"));
61+
}
62+
63+
@Test
64+
void substitutesOuterKnownValueIntoNestedBinderRefinements() {
65+
VCImplication implication = vc("∀x:int. x == 3", "∀y:int. y == x + 1", "y > x");
66+
67+
VCImplication result = VCSubstitution.apply(implication);
68+
69+
assertSimplifiedVC(result, simplified("3 + 1 > 3", "y > x", "x:int, y:int"));
70+
}
71+
72+
@Test
73+
void ignoresRecursiveBinderEquality() {
74+
VCImplication implication = vc("∀x:int. x == x + 1", "x > 0");
75+
76+
VCImplication result = VCSubstitution.apply(implication);
77+
78+
assertNotSame(implication, result);
79+
assertVC(result, "x == x + 1", "x > 0");
80+
}
81+
82+
@Test
83+
void ignoresNonEqualityBinderRefinement() {
84+
VCImplication implication = vc("∀x:int. x > 3", "x > 0");
85+
86+
VCImplication result = VCSubstitution.apply(implication);
87+
88+
assertNotSame(implication, result);
89+
assertVC(result, "x > 3", "x > 0");
90+
}
91+
92+
@Test
93+
void ignoresEqualityWithoutBinder() {
94+
VCImplication implication = vc("x == 3", "x > 0");
95+
96+
VCImplication result = VCSubstitution.apply(implication);
97+
98+
assertVC(result, "x == 3", "x > 0");
99+
}
100+
}

0 commit comments

Comments
 (0)