Skip to content

Commit 46bb174

Browse files
hyperpolymathhyperpolymath
authored
feat(codegen): #234 S4 — retire the hardcoded async_primitives set (ADR-016 complete) (#278)
Final ADR-016 slice. The async boundary is now decided *purely* from the effect side-table; the structural name list is gone. - codegen.ml: deleted `async_primitives = ["http_request_thenable"]`. `is_async_prim_call e = Effect_sites.is_async_call e` (no name disjunct). `mentions_async_prim` (PR3a single-boundary guard) is now `Effect_sites.exists_call Effect_sites.is_async_call e` — effect- driven over the SAME shared traversal the numbering uses, so it cannot miss a call shape the detector counts. The ADR's "table-miss fallback" is the oracle being empty / count-mismatched (⇒ no transform = exact pre-#234 behaviour), NOT a name list. - effect_sites.ml: factored the call traversal into shared `visit_expr`/`visit_block`/`visit_program`; `fold_calls` (program) and the new `exists_call` (expr) both use it — single source, no drift between numbering and sub-expression scans. (Dead legacy body removed.) - typecheck.ml: **root-cause fix for the cross-module gap S4 exposed.** `populate_call_effects` only scanned the local unit's `prog_decls`; imported async primitives (`http_request_thenable` — declared `/{Net,Async}` in stdlib Http, resolved as a wasm import, NOT in `prog_decls`) got EPure ⇒ once the structural mask was removed the CPS transform stopped firing for them. Now falls back to the callee's resolved scheme in `ctx.name_types` (populated by resolve, incl. imports), unioning the arrow-spine effect components (declared row ⊆ that; superset is sound for "row ⊇ Async"). Verification: full `tools/run_codegen_wasm_tests.sh` green — http_cps_base/capture/chain + http_response_reader (imported `http_request_thenable`, now via scheme-eff) AND effect_async_boundary (user `/{Async}` fn) all pass with NO structural list. `dune test --force` 290/290. Zero regression. #234 fully delivered: S1 ADR-016 (#270), S2a numbering (#275), S2b table (#276), S3 codegen switch (#277), S4 (this). Closes #234.
1 parent 52b799c commit 46bb174

3 files changed

Lines changed: 140 additions & 90 deletions

File tree

‎lib/codegen.ml‎

Lines changed: 15 additions & 19 deletions
Original file line numberDiff line numberDiff line change
@@ -1917,29 +1917,25 @@ let simple_pat_name (p : pattern) : string option =
19171917
affinescript#234 for the effect-threaded generalisation). The async
19181918
boundary is a `let` whose RHS is a call to one of these names. Extend
19191919
this list as wasm-path async stdlib primitives are added. *)
1920-
let async_primitives = [ "http_request_thenable" ]
1921-
1922-
(* ADR-016 / #234 S3: the async boundary is now ANY call whose effect
1923-
row ⊇ Async (the typecheck side-table, keyed by the shared
1924-
Effect_sites ordinal, consulted via [Effect_sites.is_async_call]),
1925-
generalising the structural-conservative hardcoded set. The
1926-
structural disjunct is retained as the sound table-miss fallback
1927-
(empty oracle / count-mismatch ⇒ exactly the pre-#234 behaviour;
1928-
zero regression). S4 retires [async_primitives]. *)
1920+
(* ADR-016 / #234 S4: the hardcoded `async_primitives` name set is
1921+
RETIRED. The async boundary is exactly "a call whose effect row ⊇
1922+
Async", decided from the typecheck side-table keyed by the shared
1923+
[Effect_sites] ordinal ([Effect_sites.is_async_call]). The ADR's
1924+
"table-miss fallback" is the oracle being empty / count-mismatched
1925+
(⇒ [is_async_call] is always false ⇒ no transform = exact pre-#234
1926+
behaviour), NOT a name list — so no structural name disjunct
1927+
remains. `http_request_thenable` is still detected because
1928+
stdlib/Http.affine declares it `/ { Net, Async }`. *)
19291929
let is_async_prim_call (e : expr) : bool =
19301930
Effect_sites.is_async_call e
1931-
||
1932-
match e with
1933-
| ExprApp (ExprVar id, _) -> List.mem id.name async_primitives
1934-
| _ -> false
19351931

1936-
(** Any recognised async-primitive name occurring free in [e]. Reuses
1937-
[find_free_vars] (which traverses call heads), so this catches an
1938-
async primitive anywhere in a sub-expression — used to enforce the
1939-
single-boundary rule for PR3a (Async→Async chaining is PR3c). *)
1932+
(** Does [e] contain (at any depth) a call whose effect row ⊇ Async?
1933+
Enforces the PR3a single-boundary rule (a pre-value must not hide
1934+
an async call; Async→Async chaining is PR3c). Now effect-driven via
1935+
the shared [Effect_sites] traversal — same call-site set the
1936+
numbering uses, so it can never miss a shape the detector counts. *)
19401937
let mentions_async_prim (e : expr) : bool =
1941-
let fv = find_free_vars [] e in
1942-
List.exists (fun p -> List.mem p fv) async_primitives
1938+
Effect_sites.exists_call Effect_sites.is_async_call e
19431939

19441940
(** Async-fn body recogniser (ADR-013 #225). Returns
19451941
[Some (pre, binder, async_call, cont)] iff the body is, after

‎lib/effect_sites.ml‎

Lines changed: 97 additions & 69 deletions
Original file line numberDiff line numberDiff line change
@@ -19,99 +19,107 @@
1919
source order. [TopFn]/[TopConst]/[TopImpl]/[TopTrait] default
2020
bodies are walked in [prog_decls] order.
2121
22-
This module is pure and depends only on [Ast]; it has no notion of
23-
effects itself (S2a). S2b/S3 build the table on top of it. *)
22+
The traversal core ([visit_*]/[fold_calls]/[exists_call]) is pure
23+
and depends only on [Ast]. The S3 ordinal-keyed async oracle
24+
(bottom of this file) is the producer/consumer bridge built on that
25+
numbering (ADR-016 S2b/S3/S4). *)
2426

2527
open Ast
2628

2729
(* The visitor threads an accumulator and a mutable next-ordinal
2830
counter (held in a ref captured by the closures, so the ordinal is a
2931
pure function of traversal position). *)
3032

31-
let fold_calls (type a) (f : a -> int -> expr -> a) (init : a)
32-
(prog : program) : a =
33-
let acc = ref init in
34-
let next = ref 0 in
35-
let rec go_expr (e : expr) : unit =
36-
(match e with
37-
| ExprApp (fn, args) ->
38-
(* Number THIS call site before descending (pre-order). *)
39-
let ord = !next in
40-
incr next;
41-
acc := f !acc ord e;
42-
go_expr fn;
43-
List.iter go_expr args
44-
| ExprLit _ | ExprVar _ | ExprVariant _ -> ()
45-
| ExprLet l ->
46-
go_expr l.el_value;
47-
(match l.el_body with Some b -> go_expr b | None -> ())
48-
| ExprIf i ->
49-
go_expr i.ei_cond;
50-
go_expr i.ei_then;
51-
(match i.ei_else with Some e -> go_expr e | None -> ())
52-
| ExprMatch m ->
53-
go_expr m.em_scrutinee;
54-
List.iter go_arm m.em_arms
55-
| ExprLambda l -> go_expr l.elam_body
56-
| ExprField (e, _) | ExprTupleIndex (e, _) | ExprRowRestrict (e, _)
57-
| ExprSpan (e, _) | ExprUnary (_, e) ->
58-
go_expr e
59-
| ExprIndex (a, b) | ExprBinary (a, _, b) ->
60-
go_expr a;
61-
go_expr b
62-
| ExprTuple es | ExprArray es -> List.iter go_expr es
63-
| ExprRecord r ->
64-
List.iter
65-
(fun (_, eo) -> match eo with Some e -> go_expr e | None -> ())
66-
r.er_fields;
67-
(match r.er_spread with Some e -> go_expr e | None -> ())
68-
| ExprBlock b -> go_block b
69-
| ExprReturn eo | ExprResume eo ->
70-
(match eo with Some e -> go_expr e | None -> ())
71-
| ExprTry t ->
72-
go_block t.et_body;
73-
(match t.et_catch with Some arms -> List.iter go_arm arms | None -> ());
74-
(match t.et_finally with Some b -> go_block b | None -> ())
75-
| ExprHandle h ->
76-
go_expr h.eh_body;
77-
List.iter go_handler h.eh_handlers
78-
| ExprUnsafe ops -> List.iter go_unsafe ops)
79-
and go_arm (a : match_arm) : unit =
33+
(* Single source of the traversal: [visit] is called on every
34+
[ExprApp] node in strict left-to-right pre-order (the call node
35+
*before* its callee/args are descended). [fold_calls] (program) and
36+
[exists_call] (expr) both use it, so the numbering and any
37+
sub-expression call scan can never diverge. *)
38+
let rec visit_expr (visit : expr -> unit) (e : expr) : unit =
39+
let go_expr = visit_expr visit in
40+
let go_arm (a : match_arm) : unit =
8041
(match a.ma_guard with Some g -> go_expr g | None -> ());
8142
go_expr a.ma_body
82-
and go_handler = function
43+
in
44+
let go_handler = function
8345
| HandlerReturn (_, e) -> go_expr e
8446
| HandlerOp (_, _, e) -> go_expr e
85-
and go_unsafe = function
47+
in
48+
let go_unsafe = function
8649
| UnsafeRead e | UnsafeForget e -> go_expr e
8750
| UnsafeWrite (a, b) | UnsafeOffset (a, b) ->
8851
go_expr a;
8952
go_expr b
9053
| UnsafeTransmute (_, _, e) -> go_expr e
91-
and go_block (b : block) : unit =
92-
List.iter go_stmt b.blk_stmts;
93-
(match b.blk_expr with Some e -> go_expr e | None -> ())
94-
and go_stmt = function
95-
| StmtLet l -> go_expr l.sl_value
96-
| StmtExpr e -> go_expr e
54+
in
55+
match e with
56+
| ExprApp (fn, args) ->
57+
(* Visit THIS call site before descending (pre-order). *)
58+
visit e;
59+
go_expr fn;
60+
List.iter go_expr args
61+
| ExprLit _ | ExprVar _ | ExprVariant _ -> ()
62+
| ExprLet l ->
63+
go_expr l.el_value;
64+
(match l.el_body with Some b -> go_expr b | None -> ())
65+
| ExprIf i ->
66+
go_expr i.ei_cond;
67+
go_expr i.ei_then;
68+
(match i.ei_else with Some e -> go_expr e | None -> ())
69+
| ExprMatch m ->
70+
go_expr m.em_scrutinee;
71+
List.iter go_arm m.em_arms
72+
| ExprLambda l -> go_expr l.elam_body
73+
| ExprField (e, _) | ExprTupleIndex (e, _) | ExprRowRestrict (e, _)
74+
| ExprSpan (e, _) | ExprUnary (_, e) ->
75+
go_expr e
76+
| ExprIndex (a, b) | ExprBinary (a, _, b) ->
77+
go_expr a;
78+
go_expr b
79+
| ExprTuple es | ExprArray es -> List.iter go_expr es
80+
| ExprRecord r ->
81+
List.iter
82+
(fun (_, eo) -> match eo with Some e -> go_expr e | None -> ())
83+
r.er_fields;
84+
(match r.er_spread with Some e -> go_expr e | None -> ())
85+
| ExprBlock b -> visit_block visit b
86+
| ExprReturn eo | ExprResume eo ->
87+
(match eo with Some e -> go_expr e | None -> ())
88+
| ExprTry t ->
89+
visit_block visit t.et_body;
90+
(match t.et_catch with Some arms -> List.iter go_arm arms | None -> ());
91+
(match t.et_finally with Some b -> visit_block visit b | None -> ())
92+
| ExprHandle h ->
93+
go_expr h.eh_body;
94+
List.iter go_handler h.eh_handlers
95+
| ExprUnsafe ops -> List.iter go_unsafe ops
96+
97+
and visit_block (visit : expr -> unit) (b : block) : unit =
98+
let go_stmt = function
99+
| StmtLet l -> visit_expr visit l.sl_value
100+
| StmtExpr e -> visit_expr visit e
97101
| StmtAssign (a, _, b) ->
98-
go_expr a;
99-
go_expr b
102+
visit_expr visit a;
103+
visit_expr visit b
100104
| StmtWhile (c, b) ->
101-
go_expr c;
102-
go_block b
105+
visit_expr visit c;
106+
visit_block visit b
103107
| StmtFor (_, e, b) ->
104-
go_expr e;
105-
go_block b
108+
visit_expr visit e;
109+
visit_block visit b
106110
in
111+
List.iter go_stmt b.blk_stmts;
112+
(match b.blk_expr with Some e -> visit_expr visit e | None -> ())
113+
114+
let visit_program (visit : expr -> unit) (prog : program) : unit =
107115
let go_fn_body = function
108-
| FnBlock b -> go_block b
109-
| FnExpr e -> go_expr e
116+
| FnBlock b -> visit_block visit b
117+
| FnExpr e -> visit_expr visit e
110118
| FnExtern -> ()
111119
in
112120
let go_top = function
113121
| TopFn fd -> go_fn_body fd.fd_body
114-
| TopConst c -> go_expr c.tc_value
122+
| TopConst c -> visit_expr visit c.tc_value
115123
| TopImpl ib ->
116124
List.iter
117125
(function ImplFn fd -> go_fn_body fd.fd_body | ImplType _ -> ())
@@ -124,9 +132,29 @@ let fold_calls (type a) (f : a -> int -> expr -> a) (init : a)
124132
trd.trd_items
125133
| TopType _ | TopEffect _ | TopExternType _ | TopExternFn _ -> ()
126134
in
127-
List.iter go_top prog.prog_decls;
135+
List.iter go_top prog.prog_decls
136+
137+
let fold_calls (type a) (f : a -> int -> expr -> a) (init : a)
138+
(prog : program) : a =
139+
let acc = ref init in
140+
let next = ref 0 in
141+
visit_program
142+
(fun call ->
143+
let ord = !next in
144+
incr next;
145+
acc := f !acc ord call)
146+
prog;
128147
!acc
129148

149+
(** [exists_call pred e] — is there a call site within [e] (any depth)
150+
for which [pred] holds? Uses the SAME pre-order traversal as
151+
[fold_calls], so a sub-expression scan can never miss a call shape
152+
the numbering counts. *)
153+
let exists_call (pred : expr -> bool) (e : expr) : bool =
154+
let found = ref false in
155+
visit_expr (fun call -> if pred call then found := true) e;
156+
!found
157+
130158
(** Total number of call sites ([ExprApp] nodes) in [prog]. *)
131159
let count (prog : program) : int =
132160
fold_calls (fun n _ _ -> n + 1) 0 prog

‎lib/typecheck.ml‎

Lines changed: 28 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -1794,6 +1794,32 @@ let populate_call_effects (ctx : context) (prog : Ast.program) : unit =
17941794
| Ast.ExprSpan (e, _) -> callee_name e
17951795
| _ -> None
17961796
in
1797+
(* The local `fd_eff` map only covers callees declared in *this*
1798+
unit's `prog_decls`. On WasmGC, imported async primitives
1799+
(`http_request_thenable`, …) and any cross-module callee are NOT
1800+
in `prog_decls` (the backend does not flatten imports) — their
1801+
resolved effect row lives in the callee's scheme in
1802+
`ctx.name_types` (populated by resolve, incl. imports). Fall back
1803+
to that: union the effect components along the arrow spine (the
1804+
declared row is among them; a superset is sound for the
1805+
boundary predicate "row ⊇ Async"). Without this the side-table
1806+
was silently empty for imported async primitives — masked by S3's
1807+
structural disjunct and exposed when S4 retires it. *)
1808+
let rec eff_of_ty (t : ty) : eff =
1809+
match t with
1810+
| TArrow (_, _, b, e) ->
1811+
(match e with
1812+
| EPure -> eff_of_ty b
1813+
| _ -> (match eff_of_ty b with
1814+
| EPure -> e
1815+
| e2 -> EUnion [ e; e2 ]))
1816+
| _ -> EPure
1817+
in
1818+
let scheme_eff (n : string) : eff =
1819+
match Hashtbl.find_opt ctx.name_types n with
1820+
| Some sc -> (try eff_of_ty (instantiate ctx.level sc) with _ -> EPure)
1821+
| None -> EPure
1822+
in
17971823
Effect_sites.iter
17981824
(fun ord call ->
17991825
let row =
@@ -1802,8 +1828,8 @@ let populate_call_effects (ctx : context) (prog : Ast.program) : unit =
18021828
(match callee_name head with
18031829
| Some n ->
18041830
(match Hashtbl.find_opt fn_eff n with
1805-
| Some e -> e
1806-
| None -> EPure)
1831+
| Some e when e <> EPure -> e
1832+
| _ -> scheme_eff n)
18071833
| None -> EPure)
18081834
| _ -> EPure
18091835
in

0 commit comments

Comments
 (0)