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
484a3259b5
commit
6d589824e7
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) ->
|
(fun (f, prog) (_, file_syms) ->
|
||||||
Woc_lib.Types.typecheck_program ~file:f ~module_of ~module_syms ~file_syms prog syms collector)
|
Woc_lib.Types.typecheck_program ~file:f ~module_of ~module_syms ~file_syms prog syms collector)
|
||||||
parsed per_file_syms;
|
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)
|
(syms, module_syms)
|
||||||
|
|
||||||
let dump_tokens path =
|
let dump_tokens path =
|
||||||
|
|
@ -427,7 +459,7 @@ let dump_gc path =
|
||||||
let collector = Woc_lib.Diag.Collector.create () in
|
let collector = Woc_lib.Diag.Collector.create () in
|
||||||
let parsed = parse_all collector sources in
|
let parsed = parse_all collector sources in
|
||||||
let syms, _module_syms = typecheck_all collector ~root:path parsed 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)
|
finish collector (build_lookup sources)
|
||||||
|
|
||||||
(* The bare `woc <path>` form (Task 8): runs the full pipeline with no
|
(* 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 }
|
{ traced; order = nodes }
|
||||||
|
|
||||||
(* The `--dump-gc` artifact (spec §1): one line per class in sorted order,
|
(* 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 render (r : result) : string =
|
||||||
let buf = Buffer.create 256 in
|
let buf = Buffer.create 256 in
|
||||||
List.iter
|
List.iter
|
||||||
|
|
|
||||||
|
|
@ -401,6 +401,11 @@ type ctx = {
|
||||||
this function — an rc pair whose source root is clobbered cannot be
|
this function — an rc pair whose source root is clobbered cannot be
|
||||||
elided, because the original reference may die inside the scope *)
|
elided, because the original reference may die inside the scope *)
|
||||||
clobbered : (string, unit) Hashtbl.t;
|
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)
|
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 =
|
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
|
(* A @gc value reaching a location that outlives this scope: one
|
||||||
increment at the escape site, never elidable. If the escaping value is
|
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.fn_rcs;
|
||||||
ctx.sink.s_rcs <- ctx.fn_rcs @ ctx.sink.s_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 =
|
~(self_class : string option) (m : Ast.method_decl) : unit =
|
||||||
let ctx =
|
let ctx =
|
||||||
{ file; syms; coll; sink; fn_name = m.name; scopes = []; loop_stack = []; recording = true;
|
{ 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;
|
diverged = false; fn_rcs = []; rc_groups = Hashtbl.create 8; rc_escaped = Hashtbl.create 8;
|
||||||
clobbered = Hashtbl.create 8 }
|
clobbered = Hashtbl.create 8; promote }
|
||||||
in
|
in
|
||||||
push_scope ctx ~node:m.id ~pos:m.pos ~label:"BODY";
|
push_scope ctx ~node:m.id ~pos:m.pos ~label:"BODY";
|
||||||
(* `self` is always a borrow (spec rule 6) *)
|
(* `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 pos_key (p : Ast.pos) = (p.line, p.col)
|
||||||
|
|
||||||
let analyze ~(file : string) (prog : Ast.program) (syms : Types.symbols)
|
let analyze ~(file : string) ?(promote : (string -> unit) option = None)
|
||||||
(coll : Diag.Collector.t) : tables =
|
(prog : Ast.program) (syms : Types.symbols) (coll : Diag.Collector.t) : tables =
|
||||||
let sink = { s_moves = []; s_drops = []; s_rcs = []; s_res = [] } in
|
let sink = { s_moves = []; s_drops = []; s_rcs = []; s_res = [] } in
|
||||||
List.iter
|
List.iter
|
||||||
(function
|
(function
|
||||||
| Ast.Class c ->
|
| 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.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.Use _ -> ()
|
||||||
| Ast.Const _ -> ()
|
| Ast.Const _ -> ()
|
||||||
| Ast.Union _ -> () (* haxe-parity Task 4: no bodies to analyze *))
|
| 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,
|
`null receiver` (the existing gc corpus only exercises `multi` gcref fields,
|
||||||
which do work). Running the ring, and reclaiming it, is **Phase 3**: the
|
which do work). Running the ring, and reclaiming it, is **Phase 3**: the
|
||||||
incremental mark-sweep collector + full gcref field paths, the `.wob`
|
incremental mark-sweep collector + full gcref field paths, the `.wob`
|
||||||
opcode-27/28 retirement, and the sweep list. Remaining front-end work
|
opcode-27/28 retirement, and the sweep list.
|
||||||
(**Phase 2b**): demand-promotion for the acyclic-but-aliased case, then
|
|
||||||
`@gc`-in-source becomes an error and the annotation bridge is removed.
|
**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:
|
When 7b lands, the acceptance is:
|
||||||
- `woc --dump-gc docs/examples/gc-cycle` classifies `Node gc (cycle …)` /
|
- `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