GV

GeezerVison

The World Wide Web, restored to 800 pixels of glory.

Home|About|Gaming cabinet|Archives|How it works|Starter sites

On this site

  • Sign in
  • ActionsCI/CD and automation
  • CodespacesCloud development environments
  • All Features
  • Documentation
  • Training
  • Certifications
  • Build with Copilot
  • Customize Copilot
  • Integrations
  • Trending repos
  • GitHub Sponsors
  • Developer articles
  • Enterprises

This view

  • Original page
  • New address

GeezerVison is showing github.com — Model the implicit close() of try-with-resources by CatarinaGamboa · Pull Request #358 · liquid-java/liquidjava

Conversation

@CatarinaGamboa

@CatarinaGamboa CatarinaGamboa commented Oct 6, 2026

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

  • classes/try_with_resources_error: double close (both reproducers from Soundness: the implicit close() of try-with-resources is not modelled #334), use after the block, use in catch, and try (r) on an already-closed r.
  • classes/try_with_resources_correct: use inside, multiple resources, try (r), catch + finally.

mvn test: 369/369 pass.

🤖 Generated with Claude Code

Sorry, something went wrong.

Uh oh!

There was an error while loading. Please reload this page.
All reactions
@CatarinaGamboa

CatarinaGamboa commented Oct 7, 2026

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
All reactions

Sorry, something went wrong.

Uh oh!

There was an error while loading. Please reload this page.
@CatarinaGamboa CatarinaGamboa added the enhancement New feature or request label Oct 7, 2026
rcosta358
rcosta358 approved these changes Oct 7, 2026
View reviewed changes

@rcosta358 rcosta358 left a comment

Copy link
Copy Markdown
Collaborator

There was a problem hiding this comment.

Choose a reason for hiding this comment

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

lgtm

Sorry, something went wrong.

Uh oh!

There was an error while loading. Please reload this page.
All reactions
@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
@CatarinaGamboa @claude
Model the implicit close() of try-with-resources
3c29de4 
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 <[email protected]>
@CatarinaGamboa
CatarinaGamboa force-pushed the fix/334-twr-close branch from 869ac9a to 3c29de4 Compare October 7, 2026 11:35
@CatarinaGamboa
CatarinaGamboa merged commit a4fbebe into main Oct 7, 2026
1 check passed

Uh oh!

There was an error while loading. Please reload this page.
@CatarinaGamboa CatarinaGamboa mentioned this pull request Oct 8, 2026
Upgrade Spoon to 11.5.0 and default the compliance level to 21 #368
Merged
CatarinaGamboa added a commit that referenced this pull request Oct 8, 2026
@CatarinaGamboa @claude
Upgrade Spoon to 11.5.0 and default the compliance level to 21 (#368)
43023fc 
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 <[email protected]>
@rcosta358
rcosta358 deleted the fix/334-twr-close branch October 13, 2026 16:56
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Reviewers

@rcosta358 rcosta358 rcosta358 approved these changes

Uh oh!

There was an error while loading. Please reload this page.

Assignees

No one assigned

Labels

enhancement New feature or request

Projects

None yet

Milestone

No milestone

Development

Successfully merging this pull request may close these issues.

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

Uh oh!

There was an error while loading. Please reload this page.

2 participants

@CatarinaGamboa @rcosta358
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.
You are visitor 01402503 — GeezerVison does not store the pages you look up.
Best viewed with Netscape Navigator 4.7 or Internet Explorer 6 at 800×600. No cookies required.