Skip to content

Commit 7f422cc

Browse files
rcosta358rcosta358
committed
Merge branch 'main' into vc-simplification-refactor
2 parents 935a168 + 3402d89 commit 7f422cc

12 files changed

Lines changed: 385 additions & 26 deletions

File tree

‎liquidjava-example/src/main/java/testSuite/CorrectInterfaceStateSet.java‎

Lines changed: 7 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,7 @@
1+
package testSuite;
2+
3+
import liquidjava.specification.StateSet;
4+
5+
@StateSet({"idle", "running"})
6+
public interface CorrectInterfaceStateSet {
7+
}

‎liquidjava-example/src/main/java/testSuite/classes/resultset_forward_correct/ResultSetTests.java‎

Lines changed: 16 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -62,4 +62,20 @@ float readAverage(Connection conn) throws SQLException {
6262
return 0.0f;
6363
}
6464
}
65+
66+
float readAverageStoredCondition(Connection conn) throws SQLException {
67+
Statement parentstmt = conn.createStatement();
68+
ResultSet parentMessage =
69+
parentstmt.executeQuery("SELECT SUM(IMPORTANCE) AS IMPAVG FROM MAIL");
70+
// Regression for issue #241: next()'s result is stored in a boolean before the `if`.
71+
// The transition (_ ? onRow : endRows) must still flow through `b`, so the guarded
72+
// getFloat() is on a row (onRow) and verifies — exactly as the inline readAverage above.
73+
boolean b = parentMessage.next();
74+
if( b ) {
75+
float avgsum = parentMessage.getFloat("IMPAVG");
76+
return avgsum;
77+
} else {
78+
return 0.0f;
79+
}
80+
}
6581
}

‎liquidjava-example/src/main/java/testSuite/classes/resultset_forward_error/ResultSetTests.java‎

Lines changed: 25 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -67,4 +67,29 @@ float readAverage(Connection conn) throws SQLException {
6767
float avgsum = parentMessage.getFloat("IMPAVG"); // State Refinement Error
6868
return avgsum;
6969
}
70+
71+
// Issue #241 soundness: storing next()'s result in a boolean must NOT make getFloat()
72+
// unconditionally legal. With no guard the state is `next ? onRow : endRows`, so onRow is
73+
// not guaranteed and getFloat() must still be rejected.
74+
float readAverageStoredNoGuard(Connection conn) throws SQLException {
75+
Statement parentstmt = conn.createStatement();
76+
ResultSet parentMessage = parentstmt.executeQuery("SELECT SUM(IMPORTANCE) AS IMPAVG FROM MAIL");
77+
boolean b = parentMessage.next();
78+
float avgsum = parentMessage.getFloat("IMPAVG"); // State Refinement Error
79+
return avgsum;
80+
}
81+
82+
// Issue #241 branch-sensitivity: legal in the then-branch (onRow), illegal in the else-branch (endRows).
83+
float readAverageVarElse(Connection conn) throws SQLException {
84+
Statement parentstmt = conn.createStatement();
85+
ResultSet parentMessage = parentstmt.executeQuery("SELECT SUM(IMPORTANCE) AS IMPAVG FROM MAIL");
86+
float avgsum = 0.0f;
87+
boolean b = parentMessage.next();
88+
if (b) {
89+
avgsum = parentMessage.getFloat("IMPAVG");
90+
} else {
91+
avgsum = parentMessage.getFloat("IMPAVG"); // State Refinement Error
92+
}
93+
return avgsum;
94+
}
7095
}

‎liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/RefinementTypeChecker.java‎

Lines changed: 9 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -321,6 +321,10 @@ private <T> boolean tryStaticFinalConstantRefinement(CtFieldRead<T> fieldRead) {
321321
public <T> void visitCtVariableRead(CtVariableRead<T> variableRead) {
322322
super.visitCtVariableRead(variableRead);
323323
CtVariable<T> varDecl = variableRead.getVariable().getDeclaration();
324+
// Some CtVariableRead forms have no resolvable declaration (e.g. accesses to symbols outside the
325+
// model); with no name there is no context entry to attach, so leave the metadata as-is.
326+
if (varDecl == null)
327+
return;
324328
getPutVariableMetadata(variableRead, varDecl.getSimpleName());
325329
}
326330

@@ -538,8 +542,11 @@ private Predicate getAssignmentRefinement(String name, CtExpression<?> assignmen
538542
}
539543

540544
private Predicate getExpressionRefinements(CtExpression<?> element) throws LJError {
541-
if (element instanceof CtVariableRead<?>) {
542-
// CtVariableRead<?> elemVar = (CtVariableRead<?>) element;
545+
if (element instanceof CtFieldRead<?> fieldRead) {
546+
visitCtFieldRead(fieldRead);
547+
return getRefinement(element);
548+
} else if (element instanceof CtVariableRead<?> varRead) {
549+
visitCtVariableRead(varRead);
543550
return getRefinement(element);
544551
} else if (element instanceof CtBinaryOperator<?>) {
545552
CtBinaryOperator<?> binop = (CtBinaryOperator<?>) element;

‎liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/TypeChecker.java‎

Lines changed: 13 additions & 21 deletions
Original file line numberDiff line numberDiff line change
@@ -263,40 +263,32 @@ private void createStateGhost(String string, CtElement element, SourcePosition p
263263
}
264264

265265
protected String getQualifiedClassName(CtElement element) {
266-
if (element.getParent() instanceof CtClass<?>) {
267-
return ((CtClass<?>) element.getParent()).getQualifiedName();
268-
} else if (element instanceof CtClass<?>) {
269-
return ((CtClass<?>) element).getQualifiedName();
270-
}
271-
return null;
266+
return getEnclosingType(element).map(CtType::getQualifiedName).orElse(null);
272267
}
273268

274269
protected String getSimpleClassName(CtElement element) {
275-
if (element.getParent() instanceof CtClass<?>) {
276-
return ((CtClass<?>) element.getParent()).getSimpleName();
277-
} else if (element instanceof CtClass<?>) {
278-
return ((CtClass<?>) element).getSimpleName();
279-
}
280-
return null;
270+
return getEnclosingType(element).map(CtType::getSimpleName).orElse(null);
281271
}
282272

283273
protected Optional<GhostFunction> createStateGhost(int order, CtElement element) {
284-
CtClass<?> klass = null;
285-
if (element.getParent() instanceof CtClass<?>) {
286-
klass = (CtClass<?>) element.getParent();
287-
} else if (element instanceof CtClass<?>) {
288-
klass = (CtClass<?>) element;
289-
}
290-
if (klass != null) {
274+
Optional<CtType<?>> enclosingType = getEnclosingType(element);
275+
if (enclosingType.isPresent()) {
276+
CtType<?> type = enclosingType.get();
291277
CtTypeReference<?> ret = factory.Type().INTEGER_PRIMITIVE;
292-
List<String> params = Collections.singletonList(klass.getSimpleName());
278+
List<String> params = Collections.singletonList(type.getSimpleName());
293279
String name = String.format("state%d", order);
294-
GhostFunction gh = new GhostFunction(name, params, ret, factory, klass.getQualifiedName());
280+
GhostFunction gh = new GhostFunction(name, params, ret, factory, type.getQualifiedName());
295281
return Optional.of(gh);
296282
}
297283
return Optional.empty();
298284
}
299285

286+
private Optional<CtType<?>> getEnclosingType(CtElement element) {
287+
if (element instanceof CtType<?> type)
288+
return Optional.of(type);
289+
return Optional.ofNullable(element.getParent(CtType.class));
290+
}
291+
300292
protected void getGhostFunction(String value, CtElement element, SourcePosition position) throws LJError {
301293
GhostDTO f = getGhostDeclaration(value, position);
302294
CtType<?> type = element instanceof CtType<?> t ? t : element.getParent()instanceof CtType<?> t ? t : null;

‎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/main/java/liquidjava/smt/TranslatorToZ3.java‎

Lines changed: 2 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -338,12 +338,14 @@ public Expr<?> makeDiv(Expr<?> eval, Expr<?> eval2) {
338338
return z3.mkFPDiv(z3.mkFPRoundNearestTiesToEven(), toFP(eval), toFP(eval2));
339339
if (eval instanceof RealExpr || eval2 instanceof RealExpr)
340340
return z3.mkDiv(toReal(eval), toReal(eval2));
341+
// Z3 integer division does not model Java's truncation toward zero for negative operands
341342
return z3.mkDiv((ArithExpr) eval, (ArithExpr) eval2);
342343
}
343344

344345
public Expr<?> makeMod(Expr<?> eval, Expr<?> eval2) {
345346
if (eval instanceof FPExpr || eval2 instanceof FPExpr)
346347
return z3.mkFPRem(toFP(eval), toFP(eval2));
348+
// Z3 integer modulo does not model Java's dividend-signed remainder for negative operands
347349
if (eval instanceof RealExpr || eval2 instanceof RealExpr)
348350
return z3.mkMod(toInt(eval), toInt(eval2));
349351
return z3.mkMod((IntExpr) eval, (IntExpr) eval2);

‎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+
}

0 commit comments

Comments
 (0)