Repository navigation
Model the implicit close() of try-with-resources - #358
Open
CatarinaGamboa wants to merge 1 commit into
Open
CatarinaGamboa wants to merge 1 commit into
CatarinaGamboa wants to merge 1 commit into
Conversation
Check `r.close()` for each resource when the try body ends, in reverse declaration order and before catch/finally, so typestate errors from the implicit close (double close, use after the block) are reported. Java 9 resource references (`try (r)`) are modelled by Spoon 10.4.2 as an implicit copy of r's declaration (initializer included), repeated once per earlier local with the same name; these are not scanned and closed once. Fixes #334 Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>
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
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 #334. Stacked on #352 (compliance level 17, needed to parse
try (r)); retarget tomainonce #352 merges.Problem
The
close()Java inserts at the end of a try-with-resources block was never checked, so a double close or a use after the block passed verification.Change
RefinementTypeChecker#visitCtTryWithResourcescans resources → body → a synthesizedr.close()per resource (reverse declaration order, as Java does) → catchers → finally. The close goes through the normal invocation check, so it works for both@StateRefinementclasses and external refinements.Errors are reported at the resource declaration (
Res r = new Res()). For a Java 9 resource reference they're reported at thetry (r)header.Spoon workaround: Spoon 10.4.2 models
try (r)as an implicit copy ofr's declaration, initializer included. It is also repeated once per earlier local namedrin the file, sotry (r)can yield[r, r, r]. Scanning those would re-runnew Res()and reset the state, so implicit resources are not scanned and are closed once per name.Tests
classes/try_with_resources_error: double close (both reproducers from Soundness: the implicitclose()of try-with-resources is not modelled #334), use after the block, use incatch, andtry (r)on an already-closedr.classes/try_with_resources_correct: use inside, multiple resources,try (r), catch + finally.mvn test: 369/369 pass.🤖 Generated with Claude Code