feat(compiler): demand promotion — GC-ness fully inferred (7b Phase 2b core)
Structural inference (2a) covers cyclic classes; this adds the DEMAND half for the acyclic-but-aliased case, so @gc is now redundant everywhere. - owner.ml: a `promote` sink on ctx. In collect mode, a class value that would raise WO-E304 (escape) records its class instead of erroring — because a class that MUST escape cannot be owned (second-class borrows can't be stored or returned), so it must be traced. `class_of_ty` extracts the class from the escaping local's type. analyze/analyze_fn take ?promote. - main.ml typecheck_all: after structural injection, a fixpoint runs ownership in collect mode over every file, unioning promotions into syms.traced (and every module table), before owner/emit see it. Terminates (promotions only grow, bounded by class count). - gcinfer.render_final: --dump-gc now reads the authoritative is_gc_class (structural + demand + the remaining @gc bridge), with the reason. Effect: a class that escapes is inferred `gc` with no annotation — e.g. `Cache` (rc.wo sans @gc) shows `gc (alias escape (demand))`; `Box` returned out of `leak` is promoted and the program is valid. No false positives: employee's Department/Employee stay owned; the 566 goldens + 14 test_diag unchanged. Corpus: compile-fail/borrow-escape-return reclassified to run/ (prints 1) — returning a borrowed class is now legal under demand promotion; the fixture encoded pre-7b behavior. Verified: woc-test 566/0 + test_diag 14/0; oop-e2e 79/0; employee 8/0; log-watcher 7/0. NOT in this slice: removing the `@gc` KEYWORD (parser rejection + rewriting the RC/@gc golden + test_diag assertions + moving the inference injection into the library so unit tests see it) — coupled to Phase 3, which deletes the RC machinery those tests cover. The ring still needs Phase 3 to RUN (nullable `?Node` gcref path). Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
This commit is contained in:
parent
f130999018
commit
26771e6aa4
8 changed files with 126 additions and 35 deletions
|
|
@ -379,6 +379,38 @@ let typecheck_all (collector : Woc_lib.Diag.Collector.t) ~(root : string)
|
|||
(fun (f, prog) (_, file_syms) ->
|
||||
Woc_lib.Types.typecheck_program ~file:f ~module_of ~module_syms ~file_syms prog syms collector)
|
||||
parsed per_file_syms;
|
||||
(* iteration 7b Phase 2b — demand promotion. Run ownership in collect mode
|
||||
over every file (structural traced already in place); any owned class value
|
||||
that would fail the escape rule (a shape that only a traced class can hold)
|
||||
records its class. Fixpoint: promotions only grow (bounded by class count),
|
||||
so this terminates — one or two passes in practice. The throwaway collector
|
||||
is discarded; this pass reports nothing. *)
|
||||
let traced_full = ref syms.Woc_lib.Types.traced in
|
||||
let throwaway = Woc_lib.Diag.Collector.create () in
|
||||
let changed = ref true in
|
||||
while !changed do
|
||||
let promoted = Hashtbl.create 16 in
|
||||
let syms_c = { syms with Woc_lib.Types.traced = !traced_full } in
|
||||
List.iter
|
||||
(fun (f, prog) ->
|
||||
ignore
|
||||
(Woc_lib.Owner.analyze ~file:f
|
||||
~promote:(Some (fun c -> Hashtbl.replace promoted c ()))
|
||||
prog syms_c throwaway))
|
||||
parsed;
|
||||
let next =
|
||||
Hashtbl.fold
|
||||
(fun c () acc -> Woc_lib.Types.StringSet.add c acc)
|
||||
promoted !traced_full
|
||||
in
|
||||
changed := not (Woc_lib.Types.StringSet.equal next !traced_full);
|
||||
traced_full := next
|
||||
done;
|
||||
let syms = { syms with Woc_lib.Types.traced = !traced_full } in
|
||||
Hashtbl.fold
|
||||
(fun k v acc -> (k, { v with Woc_lib.Types.traced = !traced_full }) :: acc)
|
||||
module_syms []
|
||||
|> List.iter (fun (k, v) -> Hashtbl.replace module_syms k v);
|
||||
(syms, module_syms)
|
||||
|
||||
let dump_tokens path =
|
||||
|
|
@ -427,7 +459,7 @@ let dump_gc path =
|
|||
let collector = Woc_lib.Diag.Collector.create () in
|
||||
let parsed = parse_all collector sources in
|
||||
let syms, _module_syms = typecheck_all collector ~root:path parsed in
|
||||
print_string (Woc_lib.Gcinfer.render (Woc_lib.Gcinfer.classify syms));
|
||||
print_string (Woc_lib.Gcinfer.render_final syms);
|
||||
finish collector (build_lookup sources)
|
||||
|
||||
(* The bare `woc <path>` form (Task 8): runs the full pipeline with no
|
||||
|
|
|
|||
|
|
@ -109,7 +109,31 @@ let classify (syms : Types.symbols) : result =
|
|||
{ traced; order = nodes }
|
||||
|
||||
(* The `--dump-gc` artifact (spec §1): one line per class in sorted order,
|
||||
`gc`/`owned`, with the reason in parens for traced classes. *)
|
||||
reading the AUTHORITATIVE traced set on `syms` (structural SCC + demand
|
||||
promotions injected by the pipeline). Reason = the structural cycle path
|
||||
when there is one, else a demand-promotion note. *)
|
||||
let render_final (syms : Types.symbols) : string =
|
||||
let struct_reasons = (classify syms).traced in
|
||||
let names =
|
||||
SMap.fold (fun k _ acc -> k :: acc) syms.Types.classes [] |> List.sort compare
|
||||
in
|
||||
let buf = Buffer.create 256 in
|
||||
List.iter
|
||||
(fun name ->
|
||||
if Types.is_gc_class syms name then
|
||||
let reason =
|
||||
match SMap.find_opt name struct_reasons with
|
||||
| Some r -> r
|
||||
| None ->
|
||||
if Types.StringSet.mem name syms.Types.traced then "alias escape (demand)"
|
||||
else "@gc annotation (redundant — inference covers it)"
|
||||
in
|
||||
Buffer.add_string buf (Printf.sprintf "%-10s gc (%s)\n" name reason)
|
||||
else Buffer.add_string buf (Printf.sprintf "%-10s owned\n" name))
|
||||
names;
|
||||
Buffer.contents buf
|
||||
|
||||
(* Structural-only render (pre-injection); kept for unit tests of the SCC half. *)
|
||||
let render (r : result) : string =
|
||||
let buf = Buffer.create 256 in
|
||||
List.iter
|
||||
|
|
|
|||
|
|
@ -401,6 +401,11 @@ type ctx = {
|
|||
this function — an rc pair whose source root is clobbered cannot be
|
||||
elided, because the original reference may die inside the scope *)
|
||||
clobbered : (string, unit) Hashtbl.t;
|
||||
(* iteration 7b demand-promotion (Gcinfer): when Some, the pass runs in
|
||||
collect mode — a class value that would fail the escape rule records its
|
||||
class here instead of raising WO-E304, so inference can promote it to
|
||||
traced. None = normal report mode. *)
|
||||
promote : (string -> unit) option;
|
||||
}
|
||||
|
||||
(* ============================================================
|
||||
|
|
@ -1060,8 +1065,27 @@ let use_place (ctx : ctx) (p : place) : unit =
|
|||
else Printf.sprintf "`%s` moved here" l_name)
|
||||
| _ -> ()
|
||||
|
||||
(* The user class an escaping value's type resolves to, if any (unwrapping `?`).
|
||||
A class value that escapes is the demand-promotion signal: second-class
|
||||
borrows cannot be stored or returned, so a class that must escape has to be
|
||||
traced. Scalars, builtins, and non-class names are genuine escape errors. *)
|
||||
let class_of_ty (syms : Types.symbols) (t : Ast.field_ty) : string option =
|
||||
let rec base = function Ast.Nullable ft -> base ft | ft -> ft in
|
||||
match base t with
|
||||
| Ast.Scalar n when Types.StringMap.mem n syms.Types.classes -> Some n
|
||||
| _ -> None
|
||||
|
||||
let escape (ctx : ctx) (l : local) ~(pos : Ast.pos) ~message : unit =
|
||||
report ctx ~code:borrow_escape_code ~pos ~message ~rel:l.l_pos ~label:(borrow_label l)
|
||||
match ctx.promote with
|
||||
| Some record -> (
|
||||
match class_of_ty ctx.syms l.l_ty with
|
||||
| Some c -> record c (* demand promotion instead of WO-E304 *)
|
||||
| None ->
|
||||
report ctx ~code:borrow_escape_code ~pos ~message ~rel:l.l_pos
|
||||
~label:(borrow_label l))
|
||||
| None ->
|
||||
report ctx ~code:borrow_escape_code ~pos ~message ~rel:l.l_pos
|
||||
~label:(borrow_label l)
|
||||
|
||||
(* A @gc value reaching a location that outlives this scope: one
|
||||
increment at the escape site, never elidable. If the escaping value is
|
||||
|
|
@ -2008,12 +2032,13 @@ let resolve_rc (ctx : ctx) : unit =
|
|||
ctx.fn_rcs;
|
||||
ctx.sink.s_rcs <- ctx.fn_rcs @ ctx.sink.s_rcs
|
||||
|
||||
let analyze_fn ~(file : string) (syms : Types.symbols) (coll : Diag.Collector.t) (sink : sink)
|
||||
let analyze_fn ~(file : string) ?(promote : (string -> unit) option = None)
|
||||
(syms : Types.symbols) (coll : Diag.Collector.t) (sink : sink)
|
||||
~(self_class : string option) (m : Ast.method_decl) : unit =
|
||||
let ctx =
|
||||
{ file; syms; coll; sink; fn_name = m.name; scopes = []; loop_stack = []; recording = true;
|
||||
diverged = false; fn_rcs = []; rc_groups = Hashtbl.create 8; rc_escaped = Hashtbl.create 8;
|
||||
clobbered = Hashtbl.create 8 }
|
||||
clobbered = Hashtbl.create 8; promote }
|
||||
in
|
||||
push_scope ctx ~node:m.id ~pos:m.pos ~label:"BODY";
|
||||
(* `self` is always a borrow (spec rule 6) *)
|
||||
|
|
@ -2037,15 +2062,17 @@ let analyze_fn ~(file : string) (syms : Types.symbols) (coll : Diag.Collector.t)
|
|||
|
||||
let pos_key (p : Ast.pos) = (p.line, p.col)
|
||||
|
||||
let analyze ~(file : string) (prog : Ast.program) (syms : Types.symbols)
|
||||
(coll : Diag.Collector.t) : tables =
|
||||
let analyze ~(file : string) ?(promote : (string -> unit) option = None)
|
||||
(prog : Ast.program) (syms : Types.symbols) (coll : Diag.Collector.t) : tables =
|
||||
let sink = { s_moves = []; s_drops = []; s_rcs = []; s_res = [] } in
|
||||
List.iter
|
||||
(function
|
||||
| Ast.Class c ->
|
||||
List.iter (fun m -> analyze_fn ~file syms coll sink ~self_class:(Some c.name) m) c.methods
|
||||
List.iter
|
||||
(fun m -> analyze_fn ~file ~promote syms coll sink ~self_class:(Some c.name) m)
|
||||
c.methods
|
||||
| Ast.Interface _ -> ()
|
||||
| Ast.Fn f -> analyze_fn ~file syms coll sink ~self_class:None f
|
||||
| Ast.Fn f -> analyze_fn ~file ~promote syms coll sink ~self_class:None f
|
||||
| Ast.Use _ -> ()
|
||||
| Ast.Const _ -> ()
|
||||
| Ast.Union _ -> () (* haxe-parity Task 4: no bodies to analyze *))
|
||||
|
|
|
|||
|
|
@ -205,9 +205,17 @@ unimplemented — even a one-hop `a.next = b; print(a.next.label)` traps
|
|||
`null receiver` (the existing gc corpus only exercises `multi` gcref fields,
|
||||
which do work). Running the ring, and reclaiming it, is **Phase 3**: the
|
||||
incremental mark-sweep collector + full gcref field paths, the `.wob`
|
||||
opcode-27/28 retirement, and the sweep list. Remaining front-end work
|
||||
(**Phase 2b**): demand-promotion for the acyclic-but-aliased case, then
|
||||
`@gc`-in-source becomes an error and the annotation bridge is removed.
|
||||
opcode-27/28 retirement, and the sweep list.
|
||||
|
||||
**Phase 2b (landed).** Demand promotion: the ownership pass, run in collect
|
||||
mode, promotes any class whose value *must escape* (returned, stored where it
|
||||
outlives its scope) — the acyclic-but-aliased case (`PriceCache`) inference by
|
||||
structure cannot see. So GC-ness is now fully inferred (cycles by structure +
|
||||
aliasing by demand), and `@gc` is redundant everywhere. What remains is
|
||||
*removing the `@gc` keyword itself* — the parser rejecting it, and the RC/`@gc`
|
||||
golden + `test_diag` assertions being rewritten — which is coupled to Phase 3
|
||||
(the RC machinery those tests cover is deleted there), so the keyword removal
|
||||
lands with Phase 3.
|
||||
|
||||
When 7b lands, the acceptance is:
|
||||
- `woc --dump-gc docs/examples/gc-cycle` classifies `Node gc (cycle …)` /
|
||||
|
|
|
|||
|
|
@ -1 +0,0 @@
|
|||
WO-E304
|
||||
|
|
@ -1,22 +0,0 @@
|
|||
-- Ownership suite (plan 2), as an end-user program: `h` is a plain
|
||||
-- (borrowed) parameter, so returning `h.box` out of `leak` would let the
|
||||
-- borrow outlive the scope it was borrowed from. Mirrors the `leak` case
|
||||
-- of compiler/test/golden/owner-err/borrow-escape.wo, given a `main` that
|
||||
-- actually calls it.
|
||||
class Box {
|
||||
n: Int
|
||||
}
|
||||
|
||||
class Holder {
|
||||
box: Box
|
||||
}
|
||||
|
||||
fn leak(h: Holder) -> Box {
|
||||
return h.box
|
||||
}
|
||||
|
||||
fn main() {
|
||||
let h = Holder { box: Box { n: 1 } }
|
||||
let b = leak(h)
|
||||
print_int(b.n)
|
||||
}
|
||||
1
tests/corpus/run/borrow-escape-return/fixture.out
Normal file
1
tests/corpus/run/borrow-escape-return/fixture.out
Normal file
|
|
@ -0,0 +1 @@
|
|||
1
|
||||
22
tests/corpus/run/borrow-escape-return/fixture.wo
Normal file
22
tests/corpus/run/borrow-escape-return/fixture.wo
Normal file
|
|
@ -0,0 +1,22 @@
|
|||
-- Iteration 7b demand promotion: `leak` returns `h.box`, a `Box` borrowed from
|
||||
-- the parameter. Under strict ownership that is a borrow escape (WO-E304), but a
|
||||
-- class that MUST escape is demand-promoted to traced (gc) by the inference
|
||||
-- pass — traced classes alias freely — so this program is valid and prints
|
||||
-- `b.n` = 1. (Was compile-fail/borrow-escape-return before 7b.)
|
||||
class Box {
|
||||
n: Int
|
||||
}
|
||||
|
||||
class Holder {
|
||||
box: Box
|
||||
}
|
||||
|
||||
fn leak(h: Holder) -> Box {
|
||||
return h.box
|
||||
}
|
||||
|
||||
fn main() {
|
||||
let h = Holder { box: Box { n: 1 } }
|
||||
let b = leak(h)
|
||||
print_int(b.n)
|
||||
}
|
||||
Loading…
Reference in a new issue