Skip to content

Commit fbfb4e2

Browse files
CatarinaGamboaclaude
CatarinaGamboa
and
claude
authored
Treat results of methods without refinements as unconstrained in operations (#312)
When an invocation of a method with no refinements (e.g. `s.length()`, `s.equals(..)`, `list.size()`) was an operand of a comparison or boolean operator, `OperationsChecker` looked up the `RefinedFunction`, got `null`, and crashed with an NPE, even in programs with no refinements at all. Now, in both `getOperationRefinements` (invocation branch) and `getOperationRefinementFromExternalLib`, a missing function yields a fresh variable of the invocation's type with refinement `true`, so the result is treated as unconstrained instead of breaking verification. Fixes #300 ## Testing - New `CorrectUnknownMethodInComparison`: `if (s.length() < 3)`, `s.equals("a") || s.equals("b")`, and a `for` loop bounded by `list.size()` (crashes without the fix). - New `ErrorUnknownMethodInOperation`: `@Refinement("_ > 0") int x = s.length() + 1;` is still reported as a Refinement Error (no information is assumed about the result). - `mvn test`: 340 tests run, 0 failures, 0 errors. - The repro from the issue now prints `Correct! Passed Verification.` via `./liquidjava`. 🤖 Generated with [Claude Code](https://claude.com/claude-code) --------- Co-authored-by: Claude Opus 5.5 <noreply@anthropic.com>
1 parent 03a15b1 commit fbfb4e2

6 files changed

Lines changed: 247 additions & 3 deletions

File tree

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

Lines changed: 80 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,80 @@
1+
package testSuite;
2+
3+
import java.util.List;
4+
import java.util.Map;
5+
6+
import liquidjava.specification.Refinement;
7+
8+
// Results of methods without refinements can be used in operations (issue #300)
9+
@SuppressWarnings("unused")
10+
public class CorrectUnknownMethodInComparison {
11+
interface Shape {
12+
int area();
13+
}
14+
15+
int helper() {
16+
return 1;
17+
}
18+
19+
public void lengthInComparison(String s) {
20+
if (s.length() < 3) {
21+
@Refinement("_ > 0")
22+
int y = 1;
23+
} else {
24+
@Refinement("_ > 0")
25+
int z = 1;
26+
}
27+
}
28+
29+
public void equalsInDisjunction(String s) {
30+
boolean known = s.equals("a") || s.equals("b");
31+
}
32+
33+
public void sizeInLoopBound(List<String> list) {
34+
for (int i = 0; i < list.size(); i++) {
35+
System.out.println(list.get(i));
36+
}
37+
}
38+
39+
public void boxedResult(List<Integer> list) {
40+
if (list.get(0) > 3) {
41+
@Refinement("_ > 0")
42+
int y = 1;
43+
}
44+
}
45+
46+
public void booleanResultInConjunction(Map<String, Integer> map, String k, int n) {
47+
if (map.containsKey(k) && n > 0) {
48+
@Refinement("_ > 0")
49+
int y = n;
50+
}
51+
}
52+
53+
public void staticCall(int a, int b) {
54+
if (Math.max(a, b) > 0) {
55+
@Refinement("_ > 0")
56+
int y = 1;
57+
}
58+
}
59+
60+
public void chainedCall(String s) {
61+
if (s.trim().length() > 0) {
62+
@Refinement("_ > 0")
63+
int y = 1;
64+
}
65+
}
66+
67+
public void implicitThisCall() {
68+
if (helper() > 0) {
69+
@Refinement("_ > 0")
70+
int y = 1;
71+
}
72+
}
73+
74+
public void interfaceMethod(Shape shape) {
75+
if (shape.area() > 0) {
76+
@Refinement("_ > 0")
77+
int y = 1;
78+
}
79+
}
80+
}

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

Lines changed: 26 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,26 @@
1+
package testSuite;
2+
3+
import liquidjava.specification.StateRefinement;
4+
import liquidjava.specification.StateSet;
5+
6+
// Calling a method without refinements in a condition keeps the object's state (issue #300)
7+
@StateSet({"open", "closed"})
8+
public class CorrectUnknownMethodInComparisonState {
9+
@StateRefinement(to = "open(this)")
10+
public CorrectUnknownMethodInComparisonState() {}
11+
12+
@StateRefinement(from = "open(this)", to = "closed(this)")
13+
public void close() {}
14+
15+
public int count() {
16+
return 0;
17+
}
18+
19+
public static void main(String[] args) {
20+
CorrectUnknownMethodInComparisonState r = new CorrectUnknownMethodInComparisonState();
21+
if (r.count() > 0) {
22+
System.out.println("non-empty");
23+
}
24+
r.close();
25+
}
26+
}

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

Lines changed: 85 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,85 @@
1+
package testSuite;
2+
3+
import java.util.List;
4+
import java.util.Map;
5+
6+
import liquidjava.specification.Refinement;
7+
8+
// Results of methods without refinements are unconstrained, so no branch is dead (issue #300)
9+
@SuppressWarnings("unused")
10+
public class ErrorUnknownMethodInComparison {
11+
interface Shape {
12+
int area();
13+
}
14+
15+
int helper() {
16+
return 1;
17+
}
18+
19+
public void thenBranch(String s) {
20+
if (s.length() < 3) {
21+
@Refinement("_ > 0")
22+
int y = -1; // Expect: Refinement Error
23+
}
24+
}
25+
26+
public void elseBranch(String s) {
27+
if (s.length() < 3) {
28+
} else {
29+
@Refinement("_ > 0")
30+
int z = -1; // Expect: Refinement Error
31+
}
32+
}
33+
34+
public void equalsInDisjunction(String s) {
35+
if (s.equals("a") || s.equals("b")) {
36+
@Refinement("_ > 0")
37+
int y = -1; // Expect: Refinement Error
38+
}
39+
}
40+
41+
public void boxedResult(List<Integer> list) {
42+
if (list.get(0) > 3) {
43+
} else {
44+
@Refinement("_ > 0")
45+
int y = -1; // Expect: Refinement Error
46+
}
47+
}
48+
49+
public void booleanResultInConjunction(Map<String, Integer> map, String k, int n) {
50+
if (map.containsKey(k) && n > 0) {
51+
@Refinement("_ > 0")
52+
int y = n - 1; // Expect: Refinement Error
53+
}
54+
}
55+
56+
public void staticCall(int a, int b) {
57+
if (Math.max(a, b) > 0) {
58+
} else {
59+
@Refinement("_ > 0")
60+
int y = -1; // Expect: Refinement Error
61+
}
62+
}
63+
64+
public void chainedCall(String s) {
65+
if (s.trim().length() > 0) {
66+
@Refinement("_ > 0")
67+
int y = -1; // Expect: Refinement Error
68+
}
69+
}
70+
71+
public void implicitThisCall() {
72+
if (helper() > 0) {
73+
} else {
74+
@Refinement("_ > 0")
75+
int y = -1; // Expect: Refinement Error
76+
}
77+
}
78+
79+
public void interfaceMethod(Shape shape) {
80+
if (shape.area() > 0) {
81+
@Refinement("_ > 0")
82+
int y = -1; // Expect: Refinement Error
83+
}
84+
}
85+
}

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

Lines changed: 27 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,27 @@
1+
package testSuite;
2+
3+
import liquidjava.specification.StateRefinement;
4+
import liquidjava.specification.StateSet;
5+
6+
// Calling a method without refinements in a condition keeps the object's state (issue #300)
7+
@StateSet({"open", "closed"})
8+
public class ErrorUnknownMethodInComparisonState {
9+
@StateRefinement(to = "open(this)")
10+
public ErrorUnknownMethodInComparisonState() {}
11+
12+
@StateRefinement(from = "open(this)", to = "closed(this)")
13+
public void close() {}
14+
15+
public int count() {
16+
return 0;
17+
}
18+
19+
public static void main(String[] args) {
20+
ErrorUnknownMethodInComparisonState r = new ErrorUnknownMethodInComparisonState();
21+
r.close();
22+
if (r.count() > 0) {
23+
System.out.println("non-empty");
24+
}
25+
r.close(); // Expect: State Refinement Error
26+
}
27+
}

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

Lines changed: 12 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,12 @@
1+
package testSuite;
2+
3+
import liquidjava.specification.Refinement;
4+
5+
// Results of methods without refinements carry no information (issue #300)
6+
@SuppressWarnings("unused")
7+
public class ErrorUnknownMethodInOperation {
8+
public void lengthPlusOne(String s) {
9+
@Refinement("_ > 0")
10+
int x = s.length() + 1; // Expect: Refinement Error
11+
}
12+
}

‎liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/general_checkers/OperationsChecker.java‎

Lines changed: 17 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -36,9 +36,9 @@
3636
import spoon.reflect.code.CtVariableWrite;
3737
import spoon.reflect.code.UnaryOperatorKind;
3838
import spoon.reflect.declaration.CtAnnotation;
39-
import spoon.reflect.declaration.CtClass;
4039
import spoon.reflect.declaration.CtElement;
4140
import spoon.reflect.declaration.CtExecutable;
41+
import spoon.reflect.declaration.CtType;
4242
import spoon.reflect.declaration.ParentNotInitializedException;
4343
import spoon.reflect.reference.CtVariableReference;
4444
import spoon.support.reflect.code.CtIfImpl;
@@ -252,8 +252,10 @@ private Predicate getOperationRefinements(CtBinaryOperator<?> operator, CtVariab
252252
return getOperationRefinementFromExternalLib(inv);
253253

254254
// Get function refinements with non_used variables
255-
String met = ((CtClass<?>) method.getParent()).getQualifiedName(); // TODO check
255+
String met = method.getParent(CtType.class).getQualifiedName(); // TODO check
256256
RefinedFunction fi = rtc.getContext().getFunction(method.getSimpleName(), met, inv.getArguments().size());
257+
if (fi == null)
258+
return getUnconstrainedInvocationVariable(inv);
257259
Predicate innerRefs = fi.getRenamedRefinements(rtc.getContext(), inv); // TODO REVIEW!!
258260

259261
// Substitute _ by the variable that we send
@@ -266,6 +268,16 @@ private Predicate getOperationRefinements(CtBinaryOperator<?> operator, CtVariab
266268
// TODO Maybe add cases
267269
}
268270

271+
/**
272+
* Creates a fresh variable with no information (refinement true) to represent the result of an invocation of a
273+
* method without refinements
274+
*/
275+
private Predicate getUnconstrainedInvocationVariable(CtInvocation<?> inv) {
276+
String newName = String.format(Formats.FRESH, rtc.getContext().getCounter());
277+
rtc.getContext().addVarToContext(newName, inv.getType(), new Predicate(), inv);
278+
return new Predicate(newName, inv);
279+
}
280+
269281
private Predicate getOperationRefinementFromExternalLib(CtInvocation<?> inv) throws LJError {
270282

271283
CtExpression<?> t = inv.getTarget();
@@ -280,6 +292,8 @@ private Predicate getOperationRefinementFromExternalLib(CtInvocation<?> inv) thr
280292
String methodInClassName = typeNotParametrized + "." + simpleName;
281293
RefinedFunction fi = rtc.getContext().getFunction(methodInClassName, typeNotParametrized,
282294
inv.getArguments().size());
295+
if (fi == null)
296+
return getUnconstrainedInvocationVariable(inv);
283297
Predicate innerRefs = fi.getRenamedRefinements(rtc.getContext(), inv); // TODO REVIEW!!
284298

285299
// Substitute _ by the variable that we send
@@ -297,7 +311,7 @@ private Predicate getOperationRefinementFromExternalLib(CtInvocation<?> inv) thr
297311
rtc.getContext().addVarToContext(newName, fi.getType(), innerRefs, inv);
298312
return new Predicate(newName, inv); // Return variable that represents the invocation
299313
}
300-
return new Predicate();
314+
return getUnconstrainedInvocationVariable(inv);
301315
}
302316

303317
private static boolean hasNullOperand(CtBinaryOperator<?> binop) {

0 commit comments

Comments
 (0)