-
Notifications
You must be signed in to change notification settings - Fork 0
feat(extractor): transitive consume contract — use-after-handoff through a forwarding consumer #68
New issue
Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.
By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.
Already on GitHub? Sign in to your account
Merged
Merged
Changes from all commits
Commits
Show all changes
3 commits
Select commit
Hold shift + click to select a range
File filter
Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
There are no files selected for viewing
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
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
28 changes: 28 additions & 0 deletions
28
corpus/real-world/ownership-handoff-use-transitive/after.cs
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
| Original file line number | Diff line number | Diff line change |
|---|---|---|
| @@ -0,0 +1,28 @@ | ||
| using System; | ||
| using System.IO; | ||
|
|
||
| // FIX: read the stream BEFORE handing ownership to the consumer chain, so nothing touches it | ||
| // after the handoff. Same transitive handoff (Consume -> Inner -> Dispose), correct order. The | ||
| // handoff still discharges ownership (Inner closes it), so there is no leak and no | ||
| // use-after-handoff -- the case must stay SILENT (this is the no-false-positive arm). | ||
| static class HandoffUseTransitive | ||
| { | ||
| static void Inner(Stream s) | ||
| { | ||
| s.CopyTo(Stream.Null); | ||
| s.Dispose(); | ||
| } | ||
|
|
||
| static void Consume(Stream sink) | ||
| { | ||
| Inner(sink); | ||
| } | ||
|
|
||
| static long Run(string path) | ||
| { | ||
| var s = File.OpenRead(path); | ||
| var len = s.Length; // read BEFORE the handoff | ||
| Consume(s); // ownership moves to Consume -> Inner (disposed) | ||
| return len; // no use after the handoff -> silent | ||
| } | ||
| } |
35 changes: 35 additions & 0 deletions
35
corpus/real-world/ownership-handoff-use-transitive/before.cs
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
| Original file line number | Diff line number | Diff line change |
|---|---|---|
| @@ -0,0 +1,35 @@ | ||
| using System; | ||
| using System.IO; | ||
|
|
||
| // A TRANSITIVE inter-procedural use-after-handoff: the stream is handed to `Consume`, which | ||
| // does NOT dispose it directly -- it FORWARDS it to `Inner`, which owns and closes it. So | ||
| // `Consume` consumes its parameter *transitively* (one hop further down the chain), and the | ||
| // caller's later read is a use-after-handoff. The consume signal travels through the | ||
| // forwarding chain: the extractor follows `Consume -> Inner -> Dispose` and models `Consume(s)` | ||
| // as a release of the argument at the call site, so a use after it trips OWN002. Unlike | ||
| // `ownership-handoff-use` (the callee disposes the param itself), here the callee only forwards. | ||
| static class HandoffUseTransitive | ||
| { | ||
| // Direct consumer: owns and closes the stream. | ||
| static void Inner(Stream s) | ||
| { | ||
| s.CopyTo(Stream.Null); | ||
| s.Dispose(); // Inner owns and closes it | ||
| } | ||
|
|
||
| // Transitive consumer: it does NOT close `sink` itself -- it forwards ownership to Inner. | ||
| // `sink` is still consumed (its obligation is discharged via Inner), so a caller must not | ||
| // touch the argument after the handoff. | ||
| static void Consume(Stream sink) | ||
| { | ||
| Inner(sink); // ownership forwarded to the real consumer | ||
| } | ||
|
|
||
| // BUG: ownership moved into Consume (-> Inner, which disposed it), then the stream is read. | ||
| static long Run(string path) | ||
| { | ||
| var s = File.OpenRead(path); | ||
| Consume(s); // ownership moves to Consume -> Inner (disposed) | ||
| return s.Length; // use-after-handoff (s is disposed) -> OWN002 | ||
| } | ||
| } |
28 changes: 28 additions & 0 deletions
28
corpus/real-world/ownership-handoff-use-transitive/case.own
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
| Original file line number | Diff line number | Diff line change |
|---|---|---|
| @@ -0,0 +1,28 @@ | ||
| // OwnLang model of a TRANSITIVE inter-procedural use-after-handoff. `take` does not close the | ||
| // stream itself -- it FORWARDS it to `inner`, which owns and closes it. So `take` consumes its | ||
| // parameter TRANSITIVELY (the obligation travels one hop further), and `run` touching the | ||
| // stream after `take(s)` is a use-after-handoff -> OWN002. The signature is still the cut: the | ||
| // caller is checked against `take`'s (transitively inferred) contract, not its body -- no | ||
| // whole-program analysis. (`consume` is an OwnLang keyword, so the reduction names the | ||
| // consumers `take`/`inner`; the C# consumers are `Consume`/`Inner`.) | ||
| module Corpus | ||
| resource Stream { | ||
| acquire open | ||
| release close | ||
| } | ||
| // direct consumer: it OWNS the stream and closes it. | ||
| fn inner(s: Stream) { | ||
| use s; | ||
| release s; | ||
| } | ||
| // transitive consumer: it forwards ownership to `inner` (does NOT close it itself), so it | ||
| // consumes `s` one hop down the chain. | ||
| fn take(s: Stream) { | ||
| inner(s); | ||
| } | ||
| // BUG: the stream is used after ownership moved into `take` (-> inner, which closed it). | ||
| fn run() { | ||
| let s = acquire Stream(); | ||
| take(s); // ownership consumed transitively (take -> inner) | ||
| use s; // <-- touched after handoff -> OWN002 | ||
| } |
1 change: 1 addition & 0 deletions
1
corpus/real-world/ownership-handoff-use-transitive/expected-diagnostics.txt
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
| Original file line number | Diff line number | Diff line change |
|---|---|---|
| @@ -0,0 +1 @@ | ||
| OWN002 |
33 changes: 33 additions & 0 deletions
33
corpus/real-world/ownership-handoff-use-transitive/notes.md
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
| Original file line number | Diff line number | Diff line change |
|---|---|---|
| @@ -0,0 +1,33 @@ | ||
| # Inter-procedural use-after-handoff — the TRANSITIVE (forwarded) consumer | ||
|
|
||
| **Pattern:** the same use-after-handoff as `ownership-handoff-use`, but the consumer does **not** | ||
| dispose the stream itself — it **forwards** it to another method that owns and closes it | ||
| (`Consume(sink) -> Inner(sink) -> sink.Dispose()`). The caller hands ownership to `Consume`, then | ||
| touches the stream again. The bug is the use **after** ownership moved; the handoff itself is | ||
| correct (the stream is closed, just one hop further down). | ||
|
|
||
| **What the checker says:** using a resource after it was consumed (here, *transitively*) by a | ||
| callee is the generic **OWN002** (use after release) — the same code as use-after-dispose. | ||
|
|
||
| **Why this case exists (the transitive consume-contract).** The consume contract was already | ||
| modelled for a callee that disposes a by-value `IDisposable` parameter *directly* | ||
| (`ownership-handoff-use`). But the inference deliberately **stopped at one hop**: a parameter | ||
| merely *handed to another call* was "genuinely ambiguous without that callee's contract, so we do | ||
| not infer it" (`ownlang/ownir.py`, the `passed` branch) — and the extractor's | ||
| `ConsumeReleaseArgs` only recognised a *direct* disposer. So `Consume` (which forwards rather than | ||
| disposes) was **not** seen as a consumer, the handoff was not a release, and the later `s.Length` | ||
| was invisible — a **miss**. | ||
|
|
||
| Now the extractor's consumer detection (`ConsumesParam`) is **transitive**: a parameter is | ||
| consumed if the body either disposes it directly **or** forwards it to another first-party | ||
| consumer that consumes it — following `Consume -> Inner -> Dispose` through the chain, guarded | ||
| against cycles. Inspecting each callee's own body keeps it inter-procedural without a cross-call | ||
| signature table (and without a dangling-callee crash). Conservative: a parameter handed to an | ||
| unknown or merely-borrowing callee is **not** treated as consumed (no false release, no false | ||
| OWN002). This fixture is a **miss** before and a **catch** after — the ratchet row that lifts the | ||
| use-after-handoff capability across a forwarding hop. The `.own` reduction already checks the | ||
| transitive shape (the front-end's signature inference recurses); this brings it to real C#. | ||
|
|
||
| **Honesty / scope.** `case.own` is a faithful hand reduction of the C# pattern, not C# the `.own` | ||
| checker ingested. `before.cs` / `after.cs` are representative of the bug and its fix, not a | ||
| verbatim copy of one PR. |
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
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
Oops, something went wrong.
Oops, something went wrong.
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.
Uh oh!
There was an error while loading. Please reload this page.