Repository navigation
Resolve field reads by declaring type and target object - #392
Open
CatarinaGamboa wants to merge 1 commit into
Open
CatarinaGamboa wants to merge 1 commit into
CatarinaGamboa wants to merge 1 commit into
Conversation
A field read first looked up the field's simple name in the context. Since #327 fields live there only under their qualified name, so that lookup could only find an unrelated local with the same name: Format.JPG was read as the local JPG (#321). That branch is removed. The context variable this#C.f tracks the value of the field of the current object, but reads of the same field on another object (other.val) used it too, so facts about this.val leaked into other.val (#322). Utils gains accessesTrackedField, true for static fields and for this/super/Outer.this targets; field reads on any other target use the field's declared refinement instead, in visitCtFieldRead and in the operand and compound assignment paths of OperationsChecker. Limits.max vs this.max (the first #322 reproducer) was already fixed by the qualified names of #327 and gets a regression test. Fixes #321 Fixes #322 Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>
Collaborator
Author
|
lgtm |
rcosta358
approved these changes
Oct 13, 2026
|
|
||
| } else if (context.hasVariable(Utils.qualifyFieldName(fieldRead.getVariable()))) { | ||
| // fields live in the context under their qualified name only: a variable with the field's simple name is an | ||
| // unrelated local (#321), and the tracked value is that of this object, not of another one (#322) |
Collaborator
There was a problem hiding this comment.
Suggested change
| // unrelated local (#321), and the tracked value is that of this object, not of another one (#322) | |
| // unrelated local, the tracked value is that of this object, not of another one |
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
2 participants
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
Fixes #321, fixes #322.
Field reads could pick up the refinement of the wrong variable, so real violations passed:
visitCtFieldReadfirst looked a field up by its simple name. Since Fix collisions between same-named fields #327 fields are stored only under their qualified name (this#<DeclaringType>.<name>), that lookup could only find a local with the same name, soFormat.JPGread a localJPG. That branch is removed.Limits.maxalready resolves correctly on main thanks to Fix collisions between same-named fields #327's qualified names; this PR adds a regression fixture.other.valstill used the trackedthis#C.val, which holds the current object's value. The newUtils.accessesTrackedFieldis true only for static fields andthis,superandOuter.thistargets; 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 (includingifconditions, which previously also overwrote what was known aboutthis.val) and compound assignments such asj += other.val.Fixtures:
ErrorFieldOfOtherClass,ErrorFieldOfOtherObject(plain read, sum,+=,ifcondition),ErrorLocalShadowsConstant(enum constant andstatic final int), and the controlCorrectFieldReadResolution. 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 = 9is checked against the declared refinement but also updatesthis#C.val, soval = 7; other.val = 9;then@Refinement("_ == 9") int k = val;verifies. The same write path handlesother.val++, compound assignments, and the typestate ghost-field update inAuxStateHandler.updateGhostField, which assumesthis.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 testpasses all 414 tests (253 TestExamples cases).🤖 Generated with Claude Code