Repository navigation
See state changes through aliases and forget mutable field initializers across methods - #393
Open
CatarinaGamboa wants to merge 2 commits into
Open
CatarinaGamboa wants to merge 2 commits into
CatarinaGamboa wants to merge 2 commits into
Conversation
A typestate transition creates a new instance of the variable it was made through (`b#2` with `closed(b#2)`), but other variables bound to the same object (`Res b = a;` gives `b#1 == a#1`) kept their old instance, so `a` was still considered open after `b.close()`. After a transition, every other reference variable of a related type whose current instance is provably equal to the target's previous instance gets a new instance equal to the transitioned one, so the new state is seen through all must-aliases (including aliases of aliases and aliases created by a later assignment). Reassigning the alias (`b = new Res()`) breaks the proved equality, so later changes through it no longer affect the original. Variables that may, but need not, alias the target keep their state. Fixes #337 Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>
A field initializer's instance stayed the field's last instance for the whole class, so every method read a non-final field as if it still held its initializer, although any other method (e.g. a setter) may have reassigned it. Passing such a field to a refined parameter was accepted. On entry to a method (constructors are unchanged), each non-final field with a recorded value gets a fresh instance carrying only its declared refinement. Final fields keep their initializer. Assignments made inside the method are still tracked as before. The field cases of the deferred-callback fixtures relied on the initializer state of a non-final field in a method; they now check that state in the constructor, where it does hold, so they keep testing that creating a callback does not run it. Fixes #340 Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>
Collaborator
Author
|
lgtm |
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
1 participant
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 #337, fixes #340.
Two false negatives found in the real-code examples, one commit each.
#337: state changes through an alias.
Res b = a;recordsb == a, butb.close()gaveba new closed version that was no longer equal toa, soa.read()passed. After a state change, every other variable of a related type that the solver proves refers to the same object now points to the new version (AuxStateHandler.updateAliases,relatedTypes). Reassigningb = new Res()breaks the alias, so closingbafterwards leavesaalone.Fixtures:
ErrorStateChangeThroughAlias(plain alias, alias of an alias, alias created by a later assignment, close inside anif) andCorrectStateChangeThroughAlias(separate objects, reassignment, state-preserving calls, closing through either name in different branches).#340: a mutable field read as its initializer. A field initializer's value stayed visible in every method. When a method (not a constructor) starts, each non-final field now keeps only its declared refinement (
RefinementTypeChecker.forgetMutableFieldValues). Final fields keep their initializer, and assignments within the method are still tracked.Fixtures:
ErrorMutableFieldInitializer(the reproducer viaqandthis.q, a static non-final field, a non-final field holding an object with a state) andCorrectMutableFieldInitializer(final field, field refinement that guarantees the bound, assign-then-read, read in the constructor).Existing fixtures changed: three field cases in
CorrectDeferredCallbackState/ErrorDeferredCallbackStaterelied on a non-final field's initializer state inside a method. Their calls moved into the constructors, where that state really holds, so they still test that creating a callback does not run it.Not covered:
updateGhostField(state-trackedintfield writes) does not update aliases.classes/state_field_initializer_correct(Fix Field Initialization #281), so it needs a design decision.this.setQ(x)) does not invalidate the value assigned earlier in the method (pre-existing).Validation:
mvn testpasses all 414 tests (253 TestExamples cases).🤖 Generated with Claude Code