Skip to content

Model the implicit close() of try-with-resources - #358

Merged
CatarinaGamboa merged 1 commit into
mainfrom
fix/334-twr-close
Oct 7, 2026
Merged

CatarinaGamboa merged 1 commit into
mainfrom
fix/334-twr-close

Conversation

@CatarinaGamboa

Copy link
Copy Markdown
Collaborator

Fixes #334. Stacked on #352 (compliance level 17, needed to parse try (r)); retarget to main once #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#visitCtTryWithResource scans resources → body → a synthesized r.close() per resource (reverse declaration order, as Java does) → catchers → finally. The close goes through the normal invocation check, so it works for both @StateRefinement classes and external refinements.

Errors are reported at the resource declaration (Res r = new Res()). For a Java 9 resource reference they're reported at the try (r) header.

Spoon workaround: Spoon 10.4.2 models try (r) as an implicit copy of r's declaration, initializer included. It is also repeated once per earlier local named r in the file, so try (r) can yield [r, r, r]. Scanning those would re-run new Res() and reset the state, so implicit resources are not scanned and are closed once per name.

Tests

mvn test: 369/369 pass.

🤖 Generated with Claude Code

@CatarinaGamboa

Copy link
Copy Markdown
Collaborator Author

This looks good! Once we update the versions of spoon/java we might need to consider more cases but probably through the same strategy

@CatarinaGamboa CatarinaGamboa added the enhancement New feature or request label Oct 7, 2026

@rcosta358 rcosta358 left a comment

Copy link
Copy Markdown
Collaborator

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

lgtm

@CatarinaGamboa
CatarinaGamboa added this pull request to stack #365 October 7, 2026 11:33
Base automatically changed from fix/compliance-level to main October 7, 2026 11:35
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>
@CatarinaGamboa
CatarinaGamboa merged commit a4fbebe into main Oct 7, 2026
1 check passed
CatarinaGamboa added a commit that referenced this pull request Oct 8, 2026
Redoes #363, which was merged into `fix/compliance-level` after that
branch had already been merged into `main` (#352), so `main` is still on
Spoon 10.4.2.

## Change
- `version.spoon`: 10.4.2 → **11.5.0** (JDT 3.46). Its class files
target Java 17, so it runs on our Java 20 build.
- `ComplianceLevel`: the cap goes from 19 to **26** (highest level JDT
3.46 accepts; `27` throws), and a separate `DEFAULT` of **21** is used
when no pom declares a Java version (it used to be the cap).
- `RefinementTypeChecker#visitCtTryWithResource` (from #358): in Spoon
11, `CtResource` is no longer a `CtVariable`. A resource is now either a
`CtLocalVariable` (`try (R r = ...)`) or a `CtVariableRead` (Java 9 `try
(r)`). Spoon 10 modelled `try (r)` as an implicit copy of `r`'s
declaration, repeated per earlier same-named local. That workaround
(skip implicit copies, dedupe by name, header position) is gone: every
resource is scanned and closed once, and the implicit `close()` is built
from the declaration's reference or a clone of the read, positioned at
the resource.

## Downstream
`vscode-liquidjava/server/pom.xml` declares `spoon-core` 10.4.2
directly, which overrides the verifier's version. Bump it to 11.5.0
together with the verifier release that includes this.

## Testing
`mvn test`: 379/379 pass, including `try_with_resources_correct` /
`try_with_resources_error` (both resource forms) and
`CorrectModernJavaSyntax`.

🤖 Generated with [Claude Code](https://claude.com/claude-code)

Co-authored-by: Claude Opus 5.5 <noreply@anthropic.com>
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

enhancement New feature or request

Projects

None yet

Development

Successfully merging this pull request may close these issues.

Soundness: the implicit close() of try-with-resources is not modelled

2 participants