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
42 changes: 35 additions & 7 deletions docs/notes/d5-ownership-transfer.md
Original file line number Diff line number Diff line change
Expand Up @@ -359,13 +359,41 @@ escape-without-transfer and all `unknown`/`may` lower to **silence** in the defa
C#-extractor table (the bool literal is a per-call-site fact the extractor sees), so it is
CI/C#-only, not a pure-Python slice.
- **D5.4 — T4 wrap/adopt** (the obligation-identity model, §11). Lands in a **three-commit
cadence** so the core change is de-risked: **(step 0)** a *no-op identity refactor* —
move resource state from per-binding to per-RID with a 1:1 binding↔RID mapping, behaviour
unchanged, validated against the green D5.0–D5.3 corpus; **(step 1)** add the `alias_join`
lowering; **(step 2)** turn on the extractor branches that emit `aliasOf:i` for *verified*
wrapper / factory / ctor-adopt sites. Result: **Dapper / Polly** modelled explicitly and
added as oracle regression anchors that now resolve *with a recorded reason* (cross-link
`field-notes-patterns.md`).
cadence** so the core change is de-risked.
- **Step 0 — the no-op RID identity refactor (shipped).** Resource state in the core flow
analysis (`analysis.py`) moved from per-binding to per-**RID**: `State.var` is keyed by an
obligation id, and a handle (local/param `Symbol`) denotes a RID through `State.handle_rid`.
The mapping is **1:1** (each `acquire`/owned-param `mint`s its own RID, `RID == id(sym)`),
so the analysis is byte-for-byte the pre-RID behaviour — the whole green corpus is the
proof. `join` merges `handle_rid` and raises (always-on, `-O`-safe) on a conflicting
mapping, locking the single-mapping invariant. Tested directly in `test_rid.py` (rid_of
1:1 default, mint, the join union/raise, and end-to-end leak/release/double/return-escape
unchanged).
- **Step 1 — the `alias_join` lowering (shipped).** A new core primitive `AliasJoin(handle,
src)` (AST + CFG + `analysis.step`) makes `handle` a **new owning alias of `src`'s RID**:
the two handles denote one obligation, `src` stays owning (unlike `move`). Because state
lives on the RID, the existing per-RID checks now do T4 for free — releasing or escaping
through **either** alias discharges the one resource (clean), a leak of the shared RID is
reported **once**, releasing **both** is OWN003, and using either after release is OWN002.
The OwnIR bridge lowers an `alias_join` flow op (`var` = the new owning handle, `src` = the
adopted local) to it; an `alias_join` over an untracked `src` makes no claim (optimistic-
silent, the v1 must-only rule, §11). **T4a ≡ T4b**: one primitive, two extractor recognisers
(step 2). The **Dapper precision win** is proven — a factory that acquires `inner` locally,
`alias_join`s a wrapper `w`, and **returns `w`** drops `inner` as a local but its obligation
escaped through `w`, so per-RID evaluation reports **no leak** (the own-only-0-with-a-reason
case the model exists for). Tests in `test_ownir.py` (release-wrapper / release-inner clean,
drop-both leaks once, double-release OWN003, use-after-release OWN002, untracked-src silent,
return-wrapper precision). *Limitation (deferred):* `alias_join` is straight-line only — an
alias minted inside one branch of an `if` that merges with a non-aliasing path is out of v1
scope (the bridge emits it straight-line at the wrapper site); the conflicting-merge raise
in `_join_handle_rid` keeps that loud rather than silently wrong.
- **Step 2 — extractor emission (next).** Turn on the Roslyn recogniser branches that emit
the `alias_join` flow op for *verified* wrapper / factory / ctor-adopt sites: **(a)** the arg
is forwarded to an `aliasOf` position and the method returns that call's result, or **(b)**
the arg is stored into a single owning field whose `Dispose()` releases it (§11). Result:
**Dapper / Polly** (`BulkheadSemaphoreFactory` → owning fields) modelled explicitly and added
as oracle regression anchors that resolve *with a recorded reason* (cross-link
`field-notes-patterns.md`).
- **D5.5 — Tier C annotations** (`[OwnTransfers]` / `[MustCallAlias]` + external file).
- **D5.x — advisory** `OWN051` for `may`/`unknown`, and the strict/pessimistic mode.

Expand Down
31 changes: 27 additions & 4 deletions ownlang/analysis.py
Original file line number Diff line number Diff line change
Expand Up @@ -51,6 +51,7 @@
CFG,
Acquire,
AcquireBuffer,
AliasJoin,
Block,
BorrowEnd,
BorrowStart,
Expand Down Expand Up @@ -82,7 +83,8 @@ class LoanKind(Enum):
@dataclass(frozen=True)
class Loan:
loan_id: int # we use id(binding_symbol): unique per borrow scope
owner: int # id(owner_symbol)
owner: int # the owner's RID (rid_of(owner)) — so the loan is seen
# through every owning alias of the borrowed resource
binding: int # id(binding_symbol)
kind: LoanKind

Expand Down Expand Up @@ -194,10 +196,16 @@ def err(self, code: str, msg: str, line: int,
# -- loan / permission helpers -----------------------------------------

def loans_on(self, st: State, owner: Symbol) -> tuple[int, bool]:
# A loan's owner is recorded by RID (see BorrowStart), so a borrow of one
# owning alias is seen through ALL aliases of the same resource: releasing
# or using a different owning handle of a borrowed resource is still caught
# (OWN008 / OWN013). In the 1:1 case `rid_of` is identity, so this is the
# pre-alias behaviour exactly. (Codex P2 — alias loans follow the RID.)
owner_rid = st.rid_of(owner)
shared = 0
mut = False
for ln in st.loans.values():
if ln.owner == id(owner):
if ln.owner == owner_rid:
if ln.kind == LoanKind.SHARED:
shared += 1
else:
Expand Down Expand Up @@ -351,7 +359,7 @@ def _sym_by_id(self, symid: int) -> Symbol | None:
idx[id(p)] = p
for b in self.cfg.blocks:
for ins in b.instrs:
for attr in ("sym", "dst", "src", "owner", "binding"):
for attr in ("sym", "dst", "src", "owner", "binding", "handle"):
s = getattr(ins, attr, None)
if isinstance(s, Symbol):
idx[id(s)] = s
Expand Down Expand Up @@ -385,6 +393,18 @@ def step(self, ins: Instr, st: State) -> None:
st.var[st.mint(ins.dst)] = {VarState.OWNED}
return

if isinstance(ins, AliasJoin):
# `handle` joins `src`'s resource obligation: it becomes an owning
# alias of the SAME RID (no new resource is minted). State lives on the
# RID, so the per-RID checks already do the right thing — releasing or
# escaping through either handle discharges the one obligation, a second
# release is OWN003, and a leak of the shared RID is reported once. We do
# NOT touch `src`'s state (it stays owning, unlike a move). If `src` was
# already released/escaped, point at its RID anyway so a later use/release
# of `handle` resolves to that (released) RID and reports correctly.
st.handle_rid[id(ins.handle)] = st.rid_of(ins.src)

Copy link
Copy Markdown

Choose a reason for hiding this comment

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

P2 Badge Make alias loans follow the shared RID

After this maps the new handle onto src's RID, active loans are still recorded and queried by the original handle id (Loan.owner / loans_on), not by RID. That means alias_join w inner; borrow inner as b { release w; } is accepted even though releasing another owning alias of the borrowed resource should be OWN008, and the same gap applies to mutable-borrow/use checks through the other alias. The loan owner needs to resolve through the shared RID once aliases exist.

Useful? React with 👍 / 👎.

return

if isinstance(ins, Release):
subj = ins.sym.origin
rkind = ins.sym.resource_kind
Expand Down Expand Up @@ -446,8 +466,11 @@ def step(self, ins: Instr, st: State) -> None:
else:
self._check_shared_borrowable(st, ins.owner, ins.line)
kind = LoanKind.SHARED
# Record the owner by RID so the loan is visible through every owning
# alias of the resource (Codex P2). `loan_id`/`binding` stay keyed by the
# binding handle (the borrow binding is its own handle, never aliased).
st.loans[id(ins.binding)] = Loan(
loan_id=id(ins.binding), owner=id(ins.owner),
loan_id=id(ins.binding), owner=st.rid_of(ins.owner),
binding=id(ins.binding), kind=kind)
return

Expand Down
19 changes: 17 additions & 2 deletions ownlang/ast_nodes.py
Original file line number Diff line number Diff line change
Expand Up @@ -132,6 +132,21 @@ class Call:
line: int


@dataclass(frozen=True)
class AliasJoin:
"""`name` is a *new owning handle* on the SAME resource obligation as `src`
(a resource-alias / RLC's `@MustCallAlias`). Releasing or escaping either
handle discharges the one underlying resource; releasing both is a double-
release; using either after the resource is released is a use-after-release.
The T4 wrap/adopt primitive (P-005 D5.4): a factory returning a wrapper of
`src`, or a constructor adopting `src` into an owning field, both reduce to
the same fact — a new owning handle joined `src`'s alias set (T4a ≡ T4b).
Unlike `move`, `src` stays owning (it is not invalidated)."""
name: str # the new owning handle that joins the alias set
src: str # an existing handle whose resource obligation `name` shares
line: int


@dataclass(frozen=True)
class BorrowBlock:
owner: str
Expand Down Expand Up @@ -176,8 +191,8 @@ class Subscribe:
line: int


Stmt = (Let | Release | Use | Overspan | Call | BorrowBlock | If | While
| Return | Subscribe)
Stmt = (Let | Release | Use | Overspan | Call | AliasJoin | BorrowBlock | If
| While | Return | Subscribe)


# ---- top level ------------------------------------------------------------
Expand Down
37 changes: 36 additions & 1 deletion ownlang/cfg.py
Original file line number Diff line number Diff line change
Expand Up @@ -151,14 +151,25 @@ class BorrowEnd:
line: int


@dataclass
class AliasJoin:
"""`handle` becomes a new owning alias of `src`'s resource obligation (its
RID): the two handles denote one underlying resource. Releasing/escaping
either discharges it; releasing both is a double-release. The T4 wrap/adopt
primitive (P-005 D5.4). `src` is NOT invalidated (unlike `MoveInto`)."""
handle: Symbol
src: Symbol
line: int


@dataclass
class Return:
sym: Symbol | None
line: int


Instr = (Acquire | AcquireBuffer | MoveInto | Release | Use | Overspan | Invoke
| BorrowStart | BorrowEnd | Return)
| BorrowStart | BorrowEnd | AliasJoin | Return)


# ---------------------------------------------------------------------------
Expand Down Expand Up @@ -354,6 +365,8 @@ def lower_stmt(self, st: A.Stmt, cur: Block) -> Block | None:
return cur
if isinstance(st, A.Call):
return self.lower_call(st, cur)
if isinstance(st, A.AliasJoin):
return self.lower_alias_join(st, cur)
if isinstance(st, A.BorrowBlock):
return self.lower_borrow(st, cur)
if isinstance(st, A.If):
Expand Down Expand Up @@ -424,6 +437,28 @@ def lower_let(self, st: A.Let, cur: Block) -> Block:
return cur
assert_never(rhs)

def lower_alias_join(self, st: A.AliasJoin, cur: Block) -> Block:
"""`name` joins `src`'s resource obligation as a new owning alias. `src`
must be an owned resource; `name` is a fresh owning handle that shares
`src`'s RID (and inherits its origin/type/kind so a per-RID finding
attributes to the one underlying resource). Unlike `move`, `src` stays
owning."""
src = self.lookup(st.src, st.line)
if src is not None and src.kind != Kind.OWNED:
self.diags.append(Diagnostic(
"OWN034",
f"cannot alias '{st.src}': it is not an owned resource "
f"({src.kind.name.lower()})", st.line))
src = None
handle = self.declare(st.name, Kind.OWNED, st.line)
if src is not None:
handle.origin = src.origin
handle.type_name = src.type_name
handle.resource_kind = src.resource_kind
handle.buffer = src.buffer
cur.instrs.append(AliasJoin(handle, src, st.line))
return cur

def lower_buffer(self, st: A.Let, rhs: A.BufferIntent, cur: Block) -> Block:
if rhs.ns != "Buffer":
self.diags.append(Diagnostic(
Expand Down
16 changes: 16 additions & 0 deletions ownlang/codegen.py
Original file line number Diff line number Diff line change
Expand Up @@ -450,6 +450,22 @@ def _stmt_inline(self, st: A.Stmt, ind: str) -> list[str]:
f"// full-length view over the pooled tail (over-read)"]
if isinstance(st, A.Call):
return [f"{ind}{st.callee}({', '.join(self._arg(a) for a in st.args)});"]
if isinstance(st, A.AliasJoin):
# a (re)declaration of this name shadows any stale buffer bookkeeping from
# an earlier same-named buffer, exactly as the Let branch does — else a later
# `release {st.name}` could emit that stale cleanup (CodeRabbit).
self.buffer_cleanup.pop(st.name, None)
self.buffer_vars.pop(st.name, None)
# `name` is an owning alias of `src` (they share one obligation). Carry
# the resource/buffer bookkeeping across so a later release of either
# emits the right cleanup; `src` stays valid (no move-out comment).
if st.src in self.buffer_cleanup:
self.buffer_cleanup[st.name] = self.buffer_cleanup[st.src]
if st.src in self.buffer_vars:
self.buffer_vars[st.name] = self.buffer_vars[st.src]
self.owned_resource[st.name] = self.owned_resource.get(st.src, "")
return [f"{ind}var {st.name} = {st.src}; "
f"// owning alias of {st.src} (shared obligation)"]
Comment thread
coderabbitai[bot] marked this conversation as resolved.
if isinstance(st, A.BorrowBlock):
kind = "mutable" if st.kind == A.BorrowKind.MUT else "shared"
rt = self.owned_resource.get(st.owner, "")
Expand Down
28 changes: 28 additions & 0 deletions ownlang/ownir.py
Original file line number Diff line number Diff line change
Expand Up @@ -105,6 +105,7 @@

from .ast_nodes import (
Acquire,
AliasJoin,
Call,
Effect,
EffectParam,
Expand Down Expand Up @@ -1539,6 +1540,33 @@ def _lower_flow(nodes: list[Any], ffile: str, fname: str,
# partial-path leak reads as a "pooled buffer", not "disposable".
"pool": n.get("kind") == "pool"}
body.append(Let(handle, Acquire("Disposable", [], line), line))
elif op == "alias_join":
# P-005 D5.4 (T4 wrap/adopt): `var` is a new owning handle on the SAME
# resource obligation as `src` — a factory returning a wrapper of `src`,
# or a ctor adopting `src` into an owning field (T4a ≡ T4b). The result
# joins `src`'s alias set: dropping the wrapper while `src` is released is
# NOT a leak, releasing both is OWN003, using either after release is
# OWN002 — all evaluated per-RID by the core. Emitted only when `src` is a
# tracked local; an unknown `src` makes no claim (precision-first).
name = str(n.get("var", "?"))
src_h = localmap.get(str(n.get("src", "")))
# Overwriting a tracked local KILLS its previous ownership binding — the
# same rule as a call-result overwrite (D5.2). Drop the stale mapping FIRST,
# even when the new alias's `src` is untracked: we make no claim on the new
# handle, but the OLD obligation must not be silently discharged by a later
# `release name` resolving to the dead handle (Codex P2). It leaks instead.
# A hoisted local keeps its single outer-scope handle (declared once).
if name not in hoisted:
localmap.pop(name, None)
if src_h is not None and name not in hoisted:

Copy link
Copy Markdown

Choose a reason for hiding this comment

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

P2 Badge Clear overwritten aliases with unknown sources

When an alias_join assigns to a local whose src is untracked, this guard skips the whole operation without removing any existing localmap entry for var. In a flow such as acquire w; alias_join w <- ghost; release w, the release is incorrectly applied to the old w obligation, so the overwritten resource is reported clean instead of leaking. Please kill the stale binding even when the new alias cannot be tracked.

Useful? React with 👍 / 👎.

handle = f"loc_{loc[0]}"
loc[0] += 1
localmap[name] = handle
handles[handle] = {"file": ffile, "line": line, "event": name,
"component": fname, "resource": "flow-local",
"ever_released": name in released_vars,
"pool": False}
body.append(AliasJoin(handle, src_h, line))
elif op == "use":
h = localmap.get(str(n.get("var")))
if h is not None:
Expand Down
Loading
Loading