diff --git a/ownlang/ownership.py b/ownlang/ownership.py index b03af6bf..1908ae04 100644 --- a/ownlang/ownership.py +++ b/ownlang/ownership.py @@ -5,37 +5,43 @@ This module is pure **data + algorithm**: it computes a Method Ownership Summary (MOS) for each first-party method from per-method *local evidence* (a "skeleton" of what a body directly does with each disposable parameter and what it returns), -resolving the parts that depend on other methods' summaries via a **depth-capped -bottom-up resolution** over the call graph. - -D5.0 deliberately does **nothing** to findings — no extractor wiring, no -behaviour change. It defines the summary vocabulary and the solver so the lattice -can be unit-tested in pure Python (the synthetic-flow discipline, lifted to the -effect level). Lowering a summary into the core's `consume`/`borrow`/`acquire` -vocabulary is D5.1+; the wrapper/alias (`aliasOf`) obligation-identity model is -D5.4 (see the note's §11). - -The skeleton is the extractor-facing input; here it is hand-authored in tests. +resolving the parts that depend on other methods' summaries by a **summary +fixpoint over the strongly-connected-component condensation** of the call graph. + +The summary is *context-insensitive*: each method has exactly one MOS, independent +of who calls it or how deep the call sits. That is what makes the computation both +linear (each method resolved once and reused — no per-call re-descent) and exact +on recursion: cycles are solved to their least fixpoint on the four-point lattice +rather than truncated. There is **no depth cap** — the SCC condensation bounds the +work without one (an earlier slice capped the recursive descent at depth 3 purely +to dodge the exponential a memo-less re-descent would otherwise hit on diamond call +graphs; the condensation removes both the blowup and the cap-induced false +`unknown`s on deep chains). + +Lowering a summary into the core's `consume`/`borrow`/`acquire` vocabulary lives in +the bridge (`ownir.py`, D5.1+: `must`→consume, `no`→borrow, `may`/`unknown`→plain); +the wrapper/alias (`aliasOf`) obligation-identity model is D5.4. The skeleton is the +extractor-facing input; here it is hand-authored in tests. Precision note: a parameter is reported `must`-transfer only when ownership leaves -the caller on **every** normal-return path the skeleton lists. A recursive forward -edge contributes *no* transfer evidence (the cycle is broken at `no`), and a chain -deeper than the cap, or a forward to an unsummarized (extern) callee, degrades to -`unknown` — never to a guessed `must`. That keeps the project's precision-first -stance: we only ever *claim* transfer when we can prove it. +the caller on **every** normal-return path. The fixpoint seeds each recursive edge +at the lattice bottom (⊥, "no evidence yet") rather than at a spurious `no`, so a +method that disposes on its base case and recurses otherwise resolves to `must` +(every *terminating* path disposes), and mutual recursion that never disposes +settles at `no`. A residual `unknown` is never a guessed `must`: it comes either +from an extern (unsummarized) callee — which `solve_with_log` surfaces in its log — +or from a deliberate precision-safe degradation intrinsic to the input (a +return-forward cycle, an `aliasOf` that cannot be re-mapped without the call's arg +mapping, an unrecognised or sparse shape), which is not logged. That keeps the +project's precision-first stance: we only ever *claim* transfer when we can prove it. """ from __future__ import annotations -from collections.abc import Iterable +from collections.abc import Iterable, Iterator from dataclasses import dataclass, field from enum import StrEnum -# Default interprocedural forward-chain depth, matching CA2000's -# `max_interprocedural_method_call_chain` default. Beyond it, a forward degrades -# to `unknown` (and is logged) rather than spending unbounded work. -DEFAULT_CAP = 3 - class Transfer(StrEnum): """Did ownership of a disposable parameter leave the caller? @@ -147,90 +153,105 @@ def to_dict(self) -> dict[str, object]: } -def _resolve_param(key: str, i: int, depth: int, stack: frozenset[str], - cap: int, sk: dict[str, MethodSkeleton], - capped: list[str]) -> Transfer: - skel = sk.get(key) - if skel is None: - return Transfer.UNKNOWN - # `i` is the callee's *logical* parameter index (`ParamSkeleton.index`), which - # need not equal the tuple offset — a skeleton may list only the disposable / - # interesting params, so a wrapper `Create(cmd, reader)` can carry just index 1. - # Resolve by `.index`, never by position. - p = next((q for q in skel.params if q.index == i), None) - if p is None: - return Transfer.UNKNOWN - if not p.disposable: - return Transfer.NO - if not p.paths: - return Transfer.NO # nothing happens to it -> kept (borrowed) - verdict: Transfer | None = None - for a in p.paths: - verdict = _path_verdict(a, depth, stack, cap, sk, capped) if verdict is None \ - else join(verdict, _path_verdict(a, depth, stack, cap, sk, capped)) - return verdict if verdict is not None else Transfer.NO - - -def _path_verdict(a: PathAction, depth: int, stack: frozenset[str], cap: int, - sk: dict[str, MethodSkeleton], capped: list[str]) -> Transfer: - if a.kind in ("dispose", "adopt", "return"): - return Transfer.MUST # ownership left the caller on this path - if a.kind == "borrow": - return Transfer.NO - if a.kind == "forward": - if a.callee not in sk: - return Transfer.UNKNOWN # extern / unsummarized callee - if depth + 1 >= cap: - capped.append(f"{a.callee}#{a.arg} (depth {depth + 1} >= cap {cap})") - return Transfer.UNKNOWN - if a.callee in stack: - return Transfer.NO # recursion: this edge carries no transfer evidence - return _resolve_param(a.callee, a.arg, depth + 1, stack | {a.callee}, - cap, sk, capped) - return Transfer.UNKNOWN - - -def _resolve_return(key: str, depth: int, stack: frozenset[str], cap: int, - sk: dict[str, MethodSkeleton], capped: list[str]) -> str: - skel = sk.get(key) - if skel is None: - return "unknown" - r = skel.ret - if r.kind == "fresh": - return "fresh" - if r.kind == "aliasOf": - return f"aliasOf:{r.arg}" - if r.kind == "aliased": - return "aliased" - if r.kind == "forward": - if r.callee not in sk: - return "unknown" - if depth + 1 >= cap: - capped.append(f"return {r.callee} (depth {depth + 1} >= cap {cap})") - return "unknown" - if r.callee in stack: - return "unknown" - inner = _resolve_return(r.callee, depth + 1, stack | {r.callee}, cap, sk, capped) - if inner.startswith("aliasOf:"): - # `inner` aliases one of the *callee's* params; remapping it to one of - # OUR args needs the call's argument mapping, which the skeleton does not - # carry yet (it arrives with the obligation-identity model in D5.4). Until - # then, never propagate a wrong index — degrade to unknown (precision-safe: - # nothing is acquired/aliased at lowering). - return "unknown" - return inner # fresh / aliased / none / unknown propagate as-is - if r.kind == "none": - return "none" # explicit no-owned-return - return "unknown" # an unrecognised kind fails closed, never silently "none" - - -def solve_with_log(skeletons: Iterable[MethodSkeleton], *, - cap: int = DEFAULT_CAP) -> tuple[dict[str, MethodSummary], list[str]]: - """Resolve every method's MOS from its skeleton plus its callees' skeletons. - - Returns (summaries-by-key, capped-log). The log names every forward that hit - the depth cap, so a run can surface what it gave up on (no silent - truncation).""" +# A parameter is resolved by `.index` (its logical `ParamSkeleton.index`), never by +# tuple offset: a skeleton may list only the disposable/interesting params, so a +# wrapper `Create(cmd, reader)` can carry just index 1. +ParamKey = tuple[str, int] # (method key, logical parameter index) + +# `None` is the lattice bottom ⊥ ("no evidence yet") used only as the fixpoint seed +# on a recursive edge. It never escapes a solved summary — it is mapped to `no` at +# finalization (a parameter nothing demonstrably consumes is kept = borrowed). +def _join_opt(a: Transfer | None, b: Transfer | None) -> Transfer | None: + """`join` lifted to the bottom-extended lattice: ⊥ (None) is the identity.""" + if a is None: + return b + if b is None: + return a + return join(a, b) + + +def _sccs(adj: dict[str, set[str]]) -> list[list[str]]: + """Tarjan's SCCs, returned bottom-up (every component precedes its callers). + + Iterative (no Python recursion limit on deep call graphs). Tarjan emits each + component only after all components it depends on, so the natural output order + is exactly the reverse-topological order the summary fixpoint wants: a callee's + summary is final before any caller reads it; only same-SCC callees are still + mid-iteration. Adjacency is sorted so the result (and the cap-free log) is + deterministic regardless of input ordering.""" + index: dict[str, int] = {} + low: dict[str, int] = {} + on_stack: set[str] = set() + stack: list[str] = [] + out: list[list[str]] = [] + counter = 0 + for root in adj: + if root in index: + continue + index[root] = low[root] = counter + counter += 1 + stack.append(root) + on_stack.add(root) + work: list[tuple[str, Iterator[str]]] = [(root, iter(sorted(adj[root])))] + while work: + node, it = work[-1] + descended = False + for w in it: # the iterator is stored in `work`, so it resumes here + if w not in index: + index[w] = low[w] = counter + counter += 1 + stack.append(w) + on_stack.add(w) + work.append((w, iter(sorted(adj[w])))) + descended = True + break + if w in on_stack: + low[node] = min(low[node], index[w]) + if descended: + continue + if low[node] == index[node]: # component root + comp: list[str] = [] + while True: + x = stack.pop() + on_stack.discard(x) + comp.append(x) + if x == node: + break + out.append(comp) + work.pop() + if work: # propagate this node's low-link up to its DFS parent + parent = work[-1][0] + low[parent] = min(low[parent], low[node]) + return out + + +def _call_graph(sk: dict[str, MethodSkeleton]) -> dict[str, set[str]]: + """Dependency edges M -> callees whose summaries M's summary reads: every + first-party callee a param forwards to, plus a forwarded return target.""" + adj: dict[str, set[str]] = {k: set() for k in sk} + for k, skel in sk.items(): + deps = adj[k] + for p in skel.params: + for a in p.paths: + if a.kind == "forward" and a.callee in sk: + deps.add(a.callee) + if skel.ret.kind == "forward" and skel.ret.callee in sk: + deps.add(skel.ret.callee) + return adj + + +def solve_with_log(skeletons: Iterable[MethodSkeleton]) -> tuple[ + dict[str, MethodSummary], list[str]]: + """Resolve every method's MOS by a summary fixpoint over the call graph's SCC + condensation. + + Returns (summaries-by-key, unresolved-log). The log names every forward — param + or return — that crosses an extern (unsummarized) boundary: the `unknown`s that + come from *outside* the analyzed set. It is NOT a log of all `unknown`s — the + intrinsic, precision-safe degradations (a return-forward cycle, an un-remappable + `aliasOf`, a missing param index or unrecognised shape) are deterministic from + the input and not logged. There is no depth cap, so no work is truncated: the + condensation makes the work linear, and recursion is solved, not cut off.""" sk: dict[str, MethodSkeleton] = {} for s in skeletons: if s.key in sk: @@ -239,24 +260,138 @@ def solve_with_log(skeletons: Iterable[MethodSkeleton], *, # depend on input order — fail fast instead. raise ValueError(f"duplicate MethodSkeleton key: {s.key}") sk[s.key] = s - capped: list[str] = [] + + unresolved: set[str] = set() + param_val: dict[ParamKey, Transfer] = {} # finalized disposable-param transfers + + def lookup(callee: str, arg: int, cur: dict[ParamKey, Transfer | None]) -> Transfer | None: + """The current transfer of callee param `arg` (resolve by `.index`): a final + value for a callee in a lower SCC, the live iterate for one in the current + SCC (possibly ⊥), `no` for a non-disposable, `unknown` past an extern edge.""" + skel = sk.get(callee) + if skel is None: + unresolved.add(f"{callee}#{arg} (extern, no summary)") + return Transfer.UNKNOWN + p = next((q for q in skel.params if q.index == arg), None) + if p is None: + return Transfer.UNKNOWN # callee has no such logical param + if not p.disposable: + return Transfer.NO + keyp = (callee, arg) + if keyp in param_val: + return param_val[keyp] + if keyp in cur: + return cur[keyp] # same-SCC member, mid-fixpoint (may be ⊥) + return Transfer.UNKNOWN # unreachable under a correct topo order; fail closed + + def contrib(a: PathAction, cur: dict[ParamKey, Transfer | None]) -> Transfer | None: + if a.kind in ("dispose", "adopt", "return"): + return Transfer.MUST # ownership left the caller on this path + if a.kind == "borrow": + return Transfer.NO + if a.kind == "forward": + return lookup(a.callee, a.arg, cur) + return Transfer.UNKNOWN + + def transfer_of(key: str, index: int, + cur: dict[ParamKey, Transfer | None]) -> Transfer | None: + p = next(q for q in sk[key].params if q.index == index) + if not p.paths: + return Transfer.NO # nothing happens to it -> kept (borrowed) + acc: Transfer | None = None + for a in p.paths: + acc = _join_opt(acc, contrib(a, cur)) + return acc + + # --- param transfers: bottom-up, per-SCC least fixpoint on the lattice ------- + for comp in _sccs(_call_graph(sk)): + members: list[ParamKey] = [ + (k, p.index) for k in comp for p in sk[k].params if p.disposable + ] + if not members: + continue + cur: dict[ParamKey, Transfer | None] = dict.fromkeys(members) # seed ⊥ (None) + changed = True + while changed: # monotone ascent on a height-3 lattice: converges fast + changed = False + for m in members: + new = transfer_of(m[0], m[1], cur) + if new != cur[m]: + cur[m] = new + changed = True + for m in members: # ⊥ (no evidence) finalizes as `no` (kept/borrowed) + v = cur[m] + param_val[m] = v if v is not None else Transfer.NO + + # --- returns: an iterative, memoized, cycle-safe chase along forward edges ---- + # A return has at most ONE forward target, so resolution is a linked-list walk, + # not a tree. Done iteratively (not recursively) so a deep but acyclic wrapper + # chain cannot blow Python's recursion limit — which, since the bridge catches a + # solve() exception by dropping to an EMPTY MOS, would otherwise disable every + # method's summary over one long chain rather than just that chain (Codex P2). + ret_val: dict[str, str] = {} + + def _terminal(r: ReturnSkeleton) -> str: + if r.kind == "fresh": + return "fresh" + if r.kind == "aliasOf": + return f"aliasOf:{r.arg}" + if r.kind == "aliased": + return "aliased" + if r.kind == "none": + return "none" # explicit no-owned-return + return "unknown" # an unrecognised kind fails closed, never silently "none" + + def resolve_return(start: str) -> str: + if start in ret_val: + return ret_val[start] # context-insensitive: one forward target per return + path: list[str] = [] # forward nodes above the stop node (shallow -> deep) + on_path: set[str] = set() + key = start + while True: + if key in ret_val: + val = ret_val[key] + break + r = sk[key].ret + if r.kind != "forward": + val = ret_val[key] = _terminal(r) + break + if r.callee not in sk: + unresolved.add(f"return {r.callee} (extern, no summary)") + val = ret_val[key] = "unknown" + break + if r.callee == key or r.callee in on_path: + # forward-return cycle: this node (and all that feed it) have no ground + val = ret_val[key] = "unknown" + break + path.append(key) + on_path.add(key) + key = r.callee + # Propagate the stop node's value up the forward chain. At each hop an + # aliasOf: aliases one of the *callee's* params; remapping it to OUR args + # needs the call's argument mapping the skeleton does not carry yet (the + # obligation-identity model, D5.4) — so degrade to unknown rather than + # propagate a wrong index. fresh / aliased / none / unknown propagate as-is. + for k in reversed(path): + val = "unknown" if val.startswith("aliasOf:") else val + ret_val[k] = val + return ret_val[start] + out: dict[str, MethodSummary] = {} for key, skel in sk.items(): params = tuple( ParamSummary( p.index, p.name, p.disposable, - _resolve_param(key, p.index, 0, frozenset({key}), cap, sk, capped) - if p.disposable else Transfer.NO, + param_val.get((key, p.index), Transfer.NO) if p.disposable else Transfer.NO, p.escapes, ) for p in skel.params ) - returns = _resolve_return(key, 0, frozenset({key}), cap, sk, capped) + returns = resolve_return(key) out[key] = MethodSummary(key, params, returns, skel.file, skel.line) - return out, capped + return out, sorted(unresolved) -def solve(skeletons: Iterable[MethodSkeleton], *, - cap: int = DEFAULT_CAP) -> dict[str, MethodSummary]: - """Convenience wrapper around :func:`solve_with_log` dropping the cap log.""" - return solve_with_log(skeletons, cap=cap)[0] +def solve(skeletons: Iterable[MethodSkeleton]) -> dict[str, MethodSummary]: + """Convenience wrapper around :func:`solve_with_log` dropping the unresolved log.""" + return solve_with_log(skeletons)[0] diff --git a/tests/test_ownership.py b/tests/test_ownership.py index 65c39c8c..42006ea8 100644 --- a/tests/test_ownership.py +++ b/tests/test_ownership.py @@ -3,8 +3,9 @@ Pure-Python, no extractor, no dotnet: hand-author method skeletons and assert the solved Method Ownership Summaries. Exercises the transfer lattice (must/may/no/ -unknown), the depth-capped bottom-up resolution, recursion/SCC convergence, the -extern boundary, return-kind resolution (fresh/aliasOf/aliased), and the +unknown), the summary fixpoint over the call graph's SCC condensation (deep chains +resolve without a depth cap; recursion is solved, not truncated), the extern +boundary and its log, return-kind resolution (fresh/aliasOf/aliased), and the `summaries[]` serialization. Run: python tests/test_ownership.py @@ -120,30 +121,71 @@ def expect(cond, msg): s = solve([_m("Caller", _p(0, PathAction("forward", "Extern", 0)))]) # Extern unsummarized expect(_t(s, "Caller", 0) == Transfer.UNKNOWN, "forward to extern -> unknown") - # --- depth cap ---------------------------------------------------------- - chain = [ + # --- deep chains: no depth cap (the SCC condensation bounds the work) ----- + # A 4-hop forward chain a former depth-3 cap would have degraded to `unknown` + # now resolves end-to-end: the consumer at the bottom propagates up exactly. + deep = [ _m("A", _p(0, PathAction("forward", "B", 0))), _m("B", _p(0, PathAction("forward", "C", 0))), - _m("C", _p(0, PathAction("dispose"))), + _m("C", _p(0, PathAction("forward", "D", 0))), + _m("D", _p(0, PathAction("dispose"))), ] - s2, log = solve_with_log(chain, cap=2) - expect(s2["A"].params[0].transfer == Transfer.UNKNOWN, "chain past cap=2 -> unknown") - expect(any("C#0" in e for e in log), "depth cap is logged, not silent") + s2, log = solve_with_log(deep) + expect(s2["A"].params[0].transfer == Transfer.MUST, "deep chain resolves (no cap)") + expect(log == [], "a fully-summarized graph leaves nothing unresolved") + + # The log is not silent about the one residual unknown: an extern (unsummarized) + # forward boundary is named, so a run can see exactly what it could not resolve. + _, log2 = solve_with_log([_m("Caller", _p(0, PathAction("forward", "Extern", 0)))]) + expect(any("Extern#0" in e for e in log2), "extern forward is logged, not silent") + + # The return chase logs its extern boundary too (a separate code path from the + # param forward above) — a forward-return to an unsummarized callee. + s3, log3 = solve_with_log([_m("Caller", ret=ReturnSkeleton("forward", callee="Extern"))]) + expect(s3["Caller"].returns == "unknown", "forward-return to extern -> unknown") + expect(any("return Extern" in e for e in log3), "extern forward-return is logged") + + # A deep but acyclic chain must not blow Python's recursion limit (the solver is + # iterative end to end; a RecursionError here would, via the bridge's catch-all, + # drop the WHOLE input's MOS to empty over one long chain). 3000 > default limit. + N = 3000 + param_chain = [ + _m(f"L{i}", _p(0, PathAction("forward", f"L{i + 1}", 0))) for i in range(N) + ] + [_m(f"L{N}", _p(0, PathAction("dispose")))] + expect(_t(solve(param_chain), "L0", 0) == Transfer.MUST, + "deep param forward chain resolves without RecursionError") + ret_chain = [ + _m(f"R{i}", ret=ReturnSkeleton("forward", callee=f"R{i + 1}")) for i in range(N) + ] + [_m(f"R{N}", ret=ReturnSkeleton("fresh"))] + expect(solve(ret_chain)["R0"].returns == "fresh", + "deep forward-return chain resolves without RecursionError") # --- recursion / SCC convergence ---------------------------------------- - # Mutual recursion that never disposes -> no (and, crucially, terminates). + # Mutual recursion that never disposes -> no (the cycle seeds at bottom and the + # fixpoint settles at `no`; crucially, it terminates). s = solve([ _m("F", _p(0, PathAction("forward", "G", 0))), _m("G", _p(0, PathAction("forward", "F", 0))), ]) expect(_t(s, "F", 0) == Transfer.NO, "mutual recursion w/o dispose -> no (terminates)") - # Self-recursion with a base-case dispose: provable on some but not all paths - # through the recursion -> may (precision-safe; never a hard must). + # Self-recursion with a base-case dispose: every *terminating* path disposes (the + # recursive edge defers, it does not keep), so the fixpoint resolves it to `must`. + # The old depth-broken resolver injected a spurious `no` at the cycle and got the + # weaker `may`; the least-fixpoint over the lattice is exact here. s = solve([ _m("Rec", _p(0, PathAction("dispose"), PathAction("forward", "Rec", 0))), ]) - expect(_t(s, "Rec", 0) == Transfer.MAY, "self-recursion + base dispose -> may") + expect(_t(s, "Rec", 0) == Transfer.MUST, "self-recursion + base dispose -> must") + + # Mutual recursion where the only ground is a dispose deep in the cycle: the + # fixpoint carries it across the SCC, where breaking the cycle at `no` would not. + s = solve([ + _m("P", _p(0, PathAction("forward", "Q", 0))), + _m("Q", _p(0, PathAction("dispose"), PathAction("forward", "P", 0))), + ]) + expect(_t(s, "P", 0) == Transfer.MUST, "mutual recursion grounded by dispose -> must") + expect(_t(s, "Q", 0) == Transfer.MUST, "the grounding method is must too") # --- return-kind resolution --------------------------------------------- s = solve([_m("Factory", ret=ReturnSkeleton("fresh"))])