Skip to content
Merged
Show file tree
Hide file tree
Changes from all commits
Commits
File filter

Filter by extension

Filter by extension


Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
18 changes: 11 additions & 7 deletions .github/workflows/ci.yml
Original file line number Diff line number Diff line change
Expand Up @@ -796,11 +796,15 @@ jobs:
# leak / double-dispose ride the flow (POOL001/003 — `memorypool-double-dispose` -> OWN003), and
# its `owner.Memory` / `owner.Memory.Span` view is a borrow lowered to a use of the OWNER
# (`ViewOwner`), so reading it after Dispose trips OWN002 (POOL002 — `memorypool-view-after-
# dispose`). A FIELD-mediated cross-method use-after-dispose is caught too: an IDisposable field
# disposed in `Dispose()` and DIRECTLY read (`_field.Member`) in a live subscription-target handler
# (RHS of a `+=` / arg of a `.Subscribe(...)`, not torn down, no `if (_disposed) return;` guard) is
# lowered to a synthetic acquire/release/use flow -> OWN002 (`field-use-after-dispose`). Remaining
# backlog: a view stored in a FIELD, an INDIRECT (helper-mediated) field use after dispose, and an
# injected-source region-escape. A drop below the floor is a regression.
run: python scripts/benchmark.py --min-recall 20
# dispose`). Returning the BARE owner under `using` (`using owner = …; return owner;`) is the twin
# of the returned-view dangle: the using-owner stays tracked through the bare return (a non-using
# transfer does not) and its use is threaded after the scope-exit release -> OWN002 (`memorypool-
# using-owner-escape`). A FIELD-mediated cross-method use-after-dispose is caught too: an IDisposable
# field disposed in `Dispose()` and read in a live subscription-target handler (RHS of a `+=` / arg
# of a `.Subscribe(...)`, not torn down, no `if (_disposed) return;` guard) — DIRECTLY
# (`field-use-after-dispose`) or ONE hop down through a private helper (`handler-use-after-dispose`)
# — lowered to a synthetic acquire/release/use flow -> OWN002. Remaining backlog: a view stored in a
# FIELD, a TWO-plus-hop indirect field use, and an injected-source region-escape. A drop below the
# floor is a regression.
run: python scripts/benchmark.py --min-recall 22

15 changes: 15 additions & 0 deletions corpus/real-world/memorypool-using-owner-escape/after.cs
Original file line number Diff line number Diff line change
@@ -0,0 +1,15 @@
// AFTER (fixed). Ownership is TRANSFERRED to the caller: no `using`, so the owner is NOT disposed at
// scope exit — the method hands back a live `IMemoryOwner<T>` and the caller owns its lifetime
// (disposes it when done). A bare owner returned WITHOUT `using` is a genuine ownership transfer, so
// the flow pass does not track it and the checker stays silent.
using System;
using System.Buffers;

static class MemoryPoolUsingOwnerEscape
{
static IMemoryOwner<byte> Borrow(int n)
{
IMemoryOwner<byte> owner = MemoryPool<byte>.Shared.Rent(n); // no `using` -> transfer
return owner; // caller owns and disposes it
}
}
21 changes: 21 additions & 0 deletions corpus/real-world/memorypool-using-owner-escape/before.cs
Original file line number Diff line number Diff line change
@@ -0,0 +1,21 @@
// BEFORE (buggy). The bare-owner `using` dangle — the twin of `memorypool-using-view-escape`. An
// `IMemoryOwner<T>` from `MemoryPool<T>` is held with a `using` declaration — so it is `Dispose()`d
// at scope exit — but the method RETURNS THE OWNER ITSELF. The implicit dispose runs as the method
// returns, so the caller receives an `IMemoryOwner<T>` already disposed (its pooled buffer handed
// back to the pool): a dangling owner / use-after-free. `using owner = …; return owner;` is exactly
// `try { return owner; } finally { owner.Dispose(); }`. The fix TRANSFERS ownership: drop the
// `using` and let the caller own and dispose it (see after.cs).
//
// Wrapped in a class so the extractor's per-class flow pass visits it.
using System;
using System.Buffers;

static class MemoryPoolUsingOwnerEscape
{
static IMemoryOwner<byte> Borrow(int n)
{
using IMemoryOwner<byte> owner = MemoryPool<byte>.Shared.Rent(n);
return owner; // <-- BUG: the `using` disposes owner as we return, so the caller gets an
// IMemoryOwner already returned to the pool
}
}
16 changes: 16 additions & 0 deletions corpus/real-world/memorypool-using-owner-escape/case.own
Original file line number Diff line number Diff line change
@@ -0,0 +1,16 @@
// OwnLang model of the MemoryPool bare-owner `using` escape. `acquire` == MemoryPool.Rent,
// `release` == the implicit `using` scope-exit Dispose. The method returns the OWNER itself, but
// the `using` disposes it FIRST (the extractor desugars `using owner = …; return owner;` to
// `acquire; release; use` — the returned owner is read by the caller AFTER Dispose), so the caller
// holds an `IMemoryOwner` already returned to the pool: a use-after-release lowered to OWN002. The
// bare-owner twin of `memorypool-using-view-escape` (which returns `owner.Memory`, a view of it).
module Corpus
resource MemoryOwner {
acquire Rent
release Dispose
}
fn lease(n: int) {
let owner = acquire MemoryOwner(n); // using MemoryPool.Rent
release owner; // implicit `using` Dispose at scope exit
use owner; // return owner — read by the caller AFTER Dispose -> OWN002
}
Original file line number Diff line number Diff line change
@@ -0,0 +1 @@
OWN002
30 changes: 30 additions & 0 deletions corpus/real-world/memorypool-using-owner-escape/notes.md
Original file line number Diff line number Diff line change
@@ -0,0 +1,30 @@
# MemoryPool bare-owner `using` escape (`using owner = …; return owner;`)

**Pattern:** an `IMemoryOwner<T>` from `MemoryPool<T>` is held with a `using` declaration (so it is
`Dispose()`d at scope exit), but the method **returns the owner itself**. The implicit dispose runs
as the method returns, so the caller receives an `IMemoryOwner<T>` whose pooled buffer has already
been handed back to the pool — a dangling owner / use-after-free. It is exactly
`try { return owner; } finally { owner.Dispose(); }` — the **bare-owner** twin of the returned-view
dangle (`memorypool-using-view-escape`, which returns `owner.Memory`). The fix is to **transfer
ownership**: drop the `using` and return the live owner so the caller owns its lifetime.

**Why it was missed before (Codex follow-up on #74):** a local that is `return`ed is treated as an
ownership transfer (the caller's to release) and dropped from the tracked set — so the bare-owner
return escaped and was never analysed, even though the `using` makes it a dangle rather than a
transfer. This slice keeps a **`using`-declared MemoryPool owner that is returned bare** tracked
(only this shape is exempted from the return-escape — a non-`using` returned owner stays a genuine
transfer, untracked, silent), and threads a use of the returned owner after the `using`-desugar's
scope-exit release — reusing the exact return-chain insertion that already catches the returned
**view** (`memorypool-using-view-escape`). So the caller's use of the owner lands after the release
and trips OWN002.

**What the checker says:** the OwnLang model and the real `before.cs` both trip **OWN002**. The
ownership-transfer fix in `after.cs` returns the owner with no `using`, so the escaped owner is
untracked and the checker is silent.

**Honesty / scope.** `case.own` is a faithful hand reduction (not C# ingested by the checker);
`before.cs` / `after.cs` are representative of the bug and its fix. One escape vector each: this
catches the bare OWNER return; `memorypool-using-view-escape` catches the returned VIEW.

Reference: [P-007](../../../docs/proposals/P-007-arraypool-span.md); the view twin is
`memorypool-using-view-escape` (#73/#74).
26 changes: 22 additions & 4 deletions corpus/wpf/handler-use-after-dispose/after.cs
Original file line number Diff line number Diff line change
@@ -1,13 +1,19 @@
// FIXED. The callback guards on the disposed flag (and/or the subscription is
// disposed only after the dispatcher queue is drained), so nothing touches the
// subscription-backed state after Dispose().
// FIXED. The callback guards on the disposed flag BEFORE it calls the helper, so a late, already-
// dispatched callback bails before anything reaches the connection. (Equivalently, drain the
// dispatcher queue before disposing.) The extractor's field-UAF pass sees the opening
// `if (_disposed) return;` guard precede the helper call and stays silent.
using System;
using System.Data.SqlClient;

public sealed class CustomerViewModel : IDisposable
{
private readonly IDisposable _sub;
private readonly SqlConnection _conn;
private bool _disposed;

public CustomerViewModel(IEventBus bus)
{
_conn = new SqlConnection("Server=.;Database=Customers");
_sub = bus.Subscribe<CustomerChanged>(OnCustomerChanged);
}

Expand All @@ -17,11 +23,23 @@ private void OnCustomerChanged(CustomerChanged e)
Refresh();
}

private void Refresh() { /* ... */ }
private void Refresh()
{
_conn.ChangeDatabase("customers");
}

public void Dispose()
{
_disposed = true;
_sub.Dispose();
_conn.Dispose();
}
}

// Minimal in-file stand-ins so the reduction is self-contained.
public interface IEventBus
{
IDisposable Subscribe<T>(Action<T> handler);
}

public sealed class CustomerChanged { }
36 changes: 28 additions & 8 deletions corpus/wpf/handler-use-after-dispose/before.cs
Original file line number Diff line number Diff line change
@@ -1,29 +1,49 @@
// BUGGY (representative WPF pattern, hand-reduced into case.own).
// BUGGY (representative WPF pattern; the C# extractor now catches this end-to-end via its one-hop
// indirect field-UAF pass).
//
// The VM disposes its subscription on close, but a callback that was already
// queued on the dispatcher still runs and touches the (now disposed) state. In
// real code this surfaces as an ObjectDisposedException or a read of torn state.
// The VM disposes its subscription (and its owned connection) on close, but a callback already
// queued on the dispatcher still runs after Dispose() and reaches the disposed connection
// INDIRECTLY: the handler calls a private `Refresh()` helper that reads `_conn` (disposed in
// Dispose()). In real code this surfaces as an ObjectDisposedException or a read of torn state.
// Unlike `field-use-after-dispose` (a DIRECT `_conn.X` read in the handler), here the disposed field
// is one hop down, behind the helper — the extractor chases that single hop. The fix (after.cs)
// guards the handler on a disposed flag before it calls the helper.
using System;
using System.Data.SqlClient;

public sealed class CustomerViewModel : IDisposable
{
private readonly IDisposable _sub;
private bool _disposed;
private readonly SqlConnection _conn;

public CustomerViewModel(IEventBus bus)
{
_conn = new SqlConnection("Server=.;Database=Customers");
_sub = bus.Subscribe<CustomerChanged>(OnCustomerChanged);
}

private void OnCustomerChanged(CustomerChanged e)
{
// a late, already-dispatched callback: runs after Dispose()
Refresh(); // touches subscription-backed state after it was disposed
Refresh(); // reaches the disposed _conn INDIRECTLY (one hop, through the helper)
}

private void Refresh() { /* reads disposed state */ }
private void Refresh()
{
_conn.ChangeDatabase("customers"); // <-- reads the disposed connection
}

public void Dispose()
{
_disposed = true;
_sub.Dispose();
_conn.Dispose();
}
}

// Minimal in-file stand-ins so the reduction is self-contained.
public interface IEventBus
{
IDisposable Subscribe<T>(Action<T> handler);
}

public sealed class CustomerChanged { }
24 changes: 13 additions & 11 deletions corpus/wpf/handler-use-after-dispose/case.own
Original file line number Diff line number Diff line change
@@ -1,17 +1,19 @@
// OwnLang model of the field-mediated use-after-dispose reached INDIRECTLY (through a helper).
// `acquire` == the owned connection's construction, `release` == its Dispose() in the ViewModel's
// Dispose(), `use` == a late dispatcher callback (the subscribed handler) reaching the connection
// one hop down — via a private Refresh() helper — AFTER Dispose(). Using a disposable after its
// release is the generic OWN002, tagged with the resource kind. The indirect twin of
// `field-use-after-dispose` (a DIRECT field read); the extractor now chases the single helper hop.
module WpfHandlerAfterDispose

// Same subscription-token protocol, tagged with its kind.
resource Subscription {
acquire Subscribe
resource Connection {
acquire Open
release Dispose
kind "subscription token"
kind "disposable"
}

// On window close the VM disposes (unsubscribes) its subscription, but a late
// queued callback still touches it. Using a subscription after Dispose is the
// generic use-after-release (OWN002), tagged with the resource kind.
fn CloseHandler(bus: int) {
let sub = acquire Subscription(bus);
release sub; // unsubscribed / disposed on close
use sub; // a late callback still touches it -> OWN002
fn OnCustomerChanged(bus: int) {
let conn = acquire Connection(bus);
release conn; // ViewModel.Dispose() disposes the owned connection
use conn; // a late callback reaches it via Refresh() after Dispose -> OWN002
}
47 changes: 27 additions & 20 deletions corpus/wpf/handler-use-after-dispose/notes.md
Original file line number Diff line number Diff line change
@@ -1,25 +1,32 @@
# WPF subscription used after Dispose
# WPF field-use-after-dispose reached INDIRECTLY (through a helper)

**Pattern:** a ViewModel unsubscribes / disposes its subscription on close, but a
callback that was already queued on the dispatcher still runs and touches the
disposed, subscription-backed state. In real code this is an
`ObjectDisposedException` or a read of torn state — the use-after-dispose cousin
**Pattern:** a ViewModel owns an `IDisposable` (here a `SqlConnection`) and subscribes a handler to
an event source. On teardown `Dispose()` disposes the connection (and the subscription token), but a
callback already queued on the dispatcher still runs after `Dispose()` and reaches the disposed
connection **indirectly** — the handler calls a private `Refresh()` helper that reads `_conn`. In
real code this is an `ObjectDisposedException` or a read of torn state — the use-after-dispose cousin
of the zombie-ViewModel leak.

**What the checker says:** using a resource after its `release` (Dispose) is the
generic **OWN002** (use after release), carrying the resource-kind tag:
**What's new — the extractor catches the one hop.** The Roslyn extractor's field-mediated
use-after-dispose pass (under `--flow-locals`) already caught a **direct** `_field.Member` read in a
live handler (`field-use-after-dispose`). This slice chases a **single hop**: a subscribed handler
that calls a **private same-class helper** (`Refresh()` / `this.Refresh()`) which itself
*unguardedly* reads a disposed field — with no `if (_disposed) return;` guard before the call — is
lowered to a synthetic `acquire`/`release`/`use` flow → **OWN002**, via the existing OwnIR bridge
(no new diagnostic). On the real C# the `corpus-benchmark` job scores `before.cs` as caught and
`after.cs` (the guarded fix) as silent.

```text
$ python -m ownlang check corpus/wpf/handler-use-after-dispose/case.own
case.own:16:9: error: [OWN002] use 'sub' after it was released
[resource: subscription token]
16 | use sub;
^
```
**Precision (why it stays low-FP).** One hop only — a deeper chain stays an honest miss. The helper
must be a **private instance** method (not a public/virtual member with a broader contract); both the
handler (before the call) and the helper must lack a disposed-guard; and the field read is a
**direct** `this`-owned `_field.Member`. The guard exclusion is the canonical fix, so the guarded
`after.cs` is silent.

**Honesty / scope.** `case.own` is a *hand reduction* of the C# pattern, not
direct C# extractor output (the C# extractor in P-001 is narrow — event
subscriptions only). It shows the ownership
*logic* maps onto the real bug; it does not model the dispatcher queue or
exception flow. `before.cs` / `after.cs` are representative, not a verbatim copy
of one PR.
**Honesty / scope.** This catches the **direct** read (`field-use-after-dispose`) and now the
**one-hop indirect** read (this case). A two-plus-hop chain, or a read through a field/property
indirection, remains an honest extractor miss — the `case.own` reduction still fires OWN002, showing
the ownership logic maps onto the real bug. `before.cs` / `after.cs` are representative of the bug
and its fix.

Reference: [P-007](../../../docs/proposals/P-007-arraypool-span.md); the direct twin is
`field-use-after-dispose`; the late-callback framing matches `zombie-viewmodel`.
Loading
Loading