Skip to content

Commit e0a6c81

Browse files
CatarinaGamboaclaude
CatarinaGamboa
and
claude
authored
Resolve field reads by declaring type and target object (#392)
Fixes #321, fixes #322. Field reads could pick up the refinement of the wrong variable, so real violations passed: - **#321:** `visitCtFieldRead` first looked a field up by its simple name. Since #327 fields are stored only under their qualified name (`this#<DeclaringType>.<name>`), that lookup could only find a local with the same name, so `Format.JPG` read a local `JPG`. That branch is removed. - **#322:** `Limits.max` already resolves correctly on main thanks to #327's qualified names; this PR adds a regression fixture. `other.val` still used the tracked `this#C.val`, which holds the current object's value. The new `Utils.accessesTrackedField` is true only for static fields and `this`, `super` and `Outer.this` targets; reads on any other object now use the field's declared refinement, which is checked at every write and so holds for every instance. This applies to field reads, binary-operation operands (including `if` conditions, which previously also overwrote what was known about `this.val`) and compound assignments such as `j += other.val`. Fixtures: `ErrorFieldOfOtherClass`, `ErrorFieldOfOtherObject` (plain read, sum, `+=`, `if` condition), `ErrorLocalShadowsConstant` (enum constant and `static final int`), and the control `CorrectFieldReadResolution`. Without the fix the two latter Error fixtures pass verification and the control gives a false error. Not fixed here (writes, needs its own issue): `other.val = 9` is checked against the declared refinement but also updates `this#C.val`, so `val = 7; other.val = 9;` then `@Refinement("_ == 9") int k = val;` verifies. The same write path handles `other.val++`, compound assignments, and the typestate ghost-field update in `AuxStateHandler.updateGhostField`, which assumes `this`. Also observed: test files that each declare an enum with the same simple name can clash within one JVM run ("Sorts ...A$Format and ...B$Format are incompatible"), so some state persists across test files. The fixtures use distinct enum names to avoid it. Validation: `mvn test` passes all 414 tests (253 TestExamples cases). 🤖 Generated with [Claude Code](https://claude.com/claude-code) --------- Co-authored-by: Claude Opus 5.5 <noreply@anthropic.com>
1 parent 8f9e862 commit e0a6c81

7 files changed

Lines changed: 173 additions & 15 deletions

File tree

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

Lines changed: 65 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,65 @@
1+
package testSuite;
2+
3+
import liquidjava.specification.Refinement;
4+
5+
// #321, #322: field reads resolve to the field of the class and object they name
6+
public class CorrectFieldReadResolution {
7+
enum Codec {
8+
JPG, PNG
9+
}
10+
11+
static final int LIMIT = 10;
12+
13+
@Refinement("val > 0")
14+
int val;
15+
16+
int max = 5;
17+
18+
public CorrectFieldReadResolution(@Refinement("_ > 0") int v) {
19+
val = v;
20+
}
21+
22+
static void onlyPng(@Refinement("_ == Codec.PNG") Codec f) {}
23+
24+
void otherClass() {
25+
@Refinement("_ == 10")
26+
int k = Limits.max;
27+
@Refinement("_ == 5")
28+
int m = max;
29+
@Refinement("_ == 5")
30+
int t = this.max;
31+
}
32+
33+
void otherObject(CorrectFieldReadResolution other) {
34+
val = 7;
35+
@Refinement("_ > 0")
36+
int k = other.val;
37+
@Refinement("_ > 7")
38+
int s = val + other.val;
39+
if (other.val == 3) {
40+
@Refinement("_ == 7")
41+
int t = val;
42+
}
43+
@Refinement("_ == 7")
44+
int u = this.val;
45+
}
46+
47+
static void sameNamedLocals() {
48+
Codec JPG = Codec.JPG;
49+
Codec PNG = Codec.PNG;
50+
onlyPng(PNG);
51+
onlyPng(Codec.PNG);
52+
Codec g = Codec.PNG;
53+
onlyPng(g);
54+
55+
int LIMIT = 3;
56+
@Refinement("_ == 10")
57+
int k = CorrectFieldReadResolution.LIMIT;
58+
@Refinement("_ == 3")
59+
int l = LIMIT;
60+
}
61+
62+
static class Limits {
63+
static final int max = 10;
64+
}
65+
}

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

Lines changed: 17 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,17 @@
1+
package testSuite;
2+
3+
import liquidjava.specification.Refinement;
4+
5+
// #322: Limits.max must not be read as this class's own field max
6+
public class ErrorFieldOfOtherClass {
7+
int max = 5;
8+
9+
void check() {
10+
@Refinement("_ == 5")
11+
int k = Limits.max; // Expect: Refinement Error
12+
}
13+
14+
static class Limits {
15+
static final int max = 10;
16+
}
17+
}

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

Lines changed: 41 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,41 @@
1+
package testSuite;
2+
3+
import liquidjava.specification.Refinement;
4+
5+
// #322: other.val is a different object's field, not this.val
6+
public class ErrorFieldOfOtherObject {
7+
@Refinement("val > 0")
8+
int val;
9+
10+
public ErrorFieldOfOtherObject(@Refinement("_ > 0") int v) {
11+
val = v;
12+
}
13+
14+
void read(ErrorFieldOfOtherObject other) {
15+
val = 7;
16+
@Refinement("_ == 7")
17+
int k = other.val; // Expect: Refinement Error
18+
}
19+
20+
void sum(ErrorFieldOfOtherObject other) {
21+
val = 7;
22+
@Refinement("_ == 14")
23+
int k = val + other.val; // Expect: Refinement Error
24+
}
25+
26+
void compound(ErrorFieldOfOtherObject other) {
27+
val = 7;
28+
int j = 0;
29+
j += other.val;
30+
@Refinement("_ == 7")
31+
int k = j; // Expect: Refinement Error
32+
}
33+
34+
void condition(ErrorFieldOfOtherObject other) {
35+
val = 7;
36+
if (other.val == 3) {
37+
@Refinement("_ == 3")
38+
int k = val; // Expect: Refinement Error
39+
}
40+
}
41+
}

‎liquidjava-example/src/main/java/testSuite/ErrorLocalShadowsConstant.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.Refinement;
4+
5+
// #321: a local named like a constant must not stand for the constant
6+
public class ErrorLocalShadowsConstant {
7+
enum Encoding {
8+
JPG, PNG
9+
}
10+
11+
static final int LIMIT = 10;
12+
13+
static void onlyPng(@Refinement("_ == Encoding.PNG") Encoding f) {}
14+
15+
public static void main(String[] args) {
16+
Encoding JPG = Encoding.PNG;
17+
Encoding g = Encoding.JPG;
18+
onlyPng(g); // Expect: Refinement Error
19+
}
20+
21+
static void staticConstant() {
22+
int LIMIT = 3;
23+
@Refinement("_ == 3")
24+
int k = ErrorLocalShadowsConstant.LIMIT; // Expect: Refinement Error
25+
}
26+
}

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

Lines changed: 4 additions & 11 deletions
Original file line numberDiff line numberDiff line change
@@ -316,17 +316,10 @@ public <T> void visitCtField(CtField<T> f) {
316316
@Override
317317
public <T> void visitCtFieldRead(CtFieldRead<T> fieldRead) {
318318
String fieldName = fieldRead.getVariable().getSimpleName();
319-
if (context.hasVariable(fieldName)) {
320-
RefinedVariable rv = context.getVariableByName(fieldName);
321-
if (rv instanceof Variable && ((Variable) rv).getLocation().isPresent()
322-
&& ((Variable) rv).getLocation().get().equals(fieldRead.getTarget().toString())) {
323-
fieldRead.putMetadata(Keys.REFINEMENT, context.getVariableRefinements(fieldName));
324-
} else {
325-
fieldRead.putMetadata(Keys.REFINEMENT,
326-
Predicate.createEquals(Predicate.createVar(Keys.WILDCARD), Predicate.createVar(fieldName)));
327-
}
328-
329-
} else if (context.hasVariable(Utils.qualifyFieldName(fieldRead.getVariable()))) {
319+
// fields live in the context under their qualified name only: a variable with the field's simple name is an
320+
// unrelated local, the tracked value is that of this object, not of another one
321+
if (Utils.accessesTrackedField(fieldRead)
322+
&& context.hasVariable(Utils.qualifyFieldName(fieldRead.getVariable()))) {
330323
String thisName = Utils.qualifyFieldName(fieldRead.getVariable());
331324
fieldRead.putMetadata(Keys.REFINEMENT,
332325
Predicate.createEquals(Predicate.createVar(Keys.WILDCARD), Predicate.createVar(thisName)));

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

Lines changed: 7 additions & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -267,9 +267,10 @@ private Predicate getOperationRefinements(CtBinaryOperator<?> operator, CtVariab
267267
elemName = Utils.qualifyFieldName(fieldRead.getVariable());
268268
Predicate elemRef = rtc.getContext().getVariableRefinements(elemName);
269269

270-
// Not a field of this class (e.g. an enum constant or a static constant): use the value given by the
271-
// field read refinement (e.g. Format.JPG), or an unconstrained fresh value when there is none
272-
if (elemRef == null && elemVar instanceof CtFieldRead)
270+
// Not a field of this class or of this object (e.g. an enum constant, a static constant or other.f): use
271+
// the value given by the field read refinement (e.g. Format.JPG), or an unconstrained fresh value
272+
if (elemVar instanceof CtFieldRead<?> fieldRead
273+
&& (elemRef == null || !Utils.accessesTrackedField(fieldRead)))
273274
return valueFromRefinement(elemVar, rtc.getRefinement(elemVar));
274275

275276
String returnName = elemName;
@@ -406,7 +407,9 @@ private Predicate getCurrentVariableValue(String name) {
406407
* Converts a operator assignment into an arithmetic predicate operand
407408
*/
408409
private Predicate getOperatorAssignmentRefinement(CtExpression<?> element) throws LJError {
409-
if (element instanceof CtVariableRead<?> variableRead) {
410+
if (element instanceof CtFieldRead<?> fieldRead && !Utils.accessesTrackedField(fieldRead)) {
411+
return valueFromRefinement(element, rtc.getRefinement(element)); // a field of another object
412+
} else if (element instanceof CtVariableRead<?> variableRead) {
410413
String name = variableRead.getVariable().getSimpleName();
411414
if (variableRead instanceof CtFieldRead<?> fieldRead)
412415
name = Utils.qualifyFieldName(fieldRead.getVariable());

‎liquidjava-verifier/src/main/java/liquidjava/utils/Utils.java‎

Lines changed: 13 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -9,9 +9,12 @@
99

1010
import liquidjava.utils.constants.Types;
1111
import spoon.reflect.code.CtBlock;
12+
import spoon.reflect.code.CtFieldAccess;
1213
import spoon.reflect.code.CtFor;
1314
import spoon.reflect.code.CtForEach;
1415
import spoon.reflect.code.CtIf;
16+
import spoon.reflect.code.CtSuperAccess;
17+
import spoon.reflect.code.CtThisAccess;
1518
import spoon.reflect.code.CtTry;
1619
import spoon.reflect.code.CtWhile;
1720
import spoon.reflect.cu.SourcePosition;
@@ -146,4 +149,14 @@ public static String getExpressionFromPosition(SourcePosition position) {
146149
}
147150
return null;
148151
}
152+
153+
/**
154+
* Whether the context variable {@link #qualifyFieldName} names the field accessed here: a static field, or a field
155+
* of the current object ({@code f}, {@code this.f}, {@code super.f}, {@code Outer.this.f}). A field of another
156+
* object ({@code other.f}) has its own value, which is not tracked in the context.
157+
*/
158+
public static boolean accessesTrackedField(CtFieldAccess<?> access) {
159+
return access.getVariable().isStatic() || access.getTarget() == null
160+
|| access.getTarget() instanceof CtThisAccess<?> || access.getTarget() instanceof CtSuperAccess<?>;
161+
}
149162
}

0 commit comments

Comments
 (0)