Skip to content

Commit 551da2b

Browse files
committed
merge: integrate main (#556 async fence) into #555 resume-soundness branch
Resolves the test_e2e.ml conflict — both the #556 async_fence_tests and the #555 resume_soundness_tests groups coexist (disjoint test functions, both registered). Full suite 457/457 green.
2 parents 6336115 + 187f21a commit 551da2b

5 files changed

Lines changed: 138 additions & 0 deletions

File tree

lib/codegen.ml

Lines changed: 41 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -2772,6 +2772,23 @@ let is_async_prim_call (e : expr) : bool =
27722772
let mentions_async_prim (e : expr) : bool =
27732773
Effect_sites.exists_call Effect_sites.is_async_call e
27742774

2775+
(** ADR-013 / #556. An `Async` fn that the CPS transform did NOT recognise
2776+
is SOUND to lower synchronously in exactly one shape: its async boundary
2777+
is a bare tail call whose `Thenable` result flows straight out as the
2778+
return value (the #205 convergence protocol — the host, not the guest,
2779+
awaits the handle; e.g. `tests/codegen/http_thenable_skeleton.affine`).
2780+
Any other un-transformed `Async` body runs a continuation against an
2781+
unsettled handle, the silent miscompile #556 closes. Recognise the safe
2782+
pass-through: after peeling trivial block / `return` wrappers the tail is
2783+
itself an async-primitive call. *)
2784+
let is_async_passthrough (body : expr) : bool =
2785+
let rec tail = function
2786+
| ExprBlock { blk_stmts = []; blk_expr = Some e } -> tail e
2787+
| ExprReturn (Some e) -> tail e
2788+
| e -> e
2789+
in
2790+
is_async_prim_call (tail body)
2791+
27752792
(** Async-fn body recogniser (ADR-013 #225). Returns
27762793
[Some (pre, binder, async_call, cont)] iff the body is, after
27772794
trivial-block unwrapping, a sequence of zero or more simple
@@ -3013,6 +3030,30 @@ let gen_function (ctx : context) (fd : fn_decl) : (context * func) result =
30133030
match async_base with
30143031
| Some (pre, binder, call, cont, tt_idx) ->
30153032
gen_async_base_case ctx_with_params pre binder call cont tt_idx
3033+
| None when fn_is_async fd
3034+
&& mentions_async_prim body_expr
3035+
&& not (is_async_passthrough body_expr) ->
3036+
(* #556: this `Async` fn performs an async call whose result is
3037+
consumed by a continuation, but the CPS transform did not fire
3038+
(`thenableThen` not importable on this backend, the body is not the
3039+
recognised `let r = <async-call>; <cont>` base case, or the effect
3040+
side-table missed the call site). Lowering it synchronously would
3041+
run the continuation against an UNSETTLED handle — a silent wrong
3042+
result. Fail loudly instead; the bare tail-return-`Thenable`
3043+
pass-through (#205) is still lowered by the `Some`/`gen_expr` arms.
3044+
This back-ports the #555/#566 "fail loud, never silent" fence to the
3045+
async path. *)
3046+
Error (UnsupportedFeature
3047+
(Printf.sprintf
3048+
"async function `%s` performs an async call whose result is used \
3049+
by a continuation, but it could not be lowered to the WASM CPS \
3050+
form (ADR-013): the `thenableThen` host import is not in scope, \
3051+
the body is not the recognised `let r = <async-call>; <cont>` \
3052+
base case, or the effect side-table missed this call site \
3053+
(Refs #556); lowering it synchronously would run the \
3054+
continuation before the async result settles. Use `--interp` / \
3055+
`-i`, or a backend where `thenableThen` is importable."
3056+
fd.fd_name.name))
30163057
| None -> gen_expr ctx_with_params body_expr
30173058
in
30183059

Lines changed: 15 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,15 @@
1+
// SPDX-License-Identifier: MPL-2.0
2+
// SPDX-FileCopyrightText: 2026 hyperpolymath
3+
//
4+
// Issue #556 regression fixture (POSITIVE / no-over-rejection). `noop` is
5+
// declared `Async` but performs no async call at all, so there is no
6+
// continuation to mis-order — synchronous lowering is correct and must not
7+
// trip the #556 fence (the guard keys on an actual async-prim call, not the
8+
// effect row alone).
9+
fn noop(u: Int) -> Int / { Async } {
10+
return u + 1;
11+
}
12+
13+
fn main() -> Int {
14+
return noop(7);
15+
}
Lines changed: 17 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,17 @@
1+
// SPDX-License-Identifier: MPL-2.0
2+
// SPDX-FileCopyrightText: 2026 hyperpolymath
3+
//
4+
// Issue #556 regression fixture (POSITIVE / no-over-rejection). `launch` is
5+
// `Async` but its async call is in TAIL position — the `Thenable` handle
6+
// flows straight out as the return value (the #205 convergence protocol; the
7+
// host, not the guest, awaits it). This is sound to lower synchronously and
8+
// must keep compiling: the #556 fence must NOT reject the pass-through shape.
9+
extern fn fetchHandle(u: Int) -> Int / { Async };
10+
11+
fn launch(u: Int) -> Int / { Async } {
12+
fetchHandle(u)
13+
}
14+
15+
fn main() -> Int {
16+
return 0;
17+
}
Lines changed: 20 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,20 @@
1+
// SPDX-License-Identifier: MPL-2.0
2+
// SPDX-FileCopyrightText: 2026 hyperpolymath
3+
//
4+
// Issue #556 regression fixture (NEGATIVE). `get` is declared `Async` and
5+
// performs an async call (`getThenable`) whose result is consumed by a
6+
// continuation (`h + 0`), but the core-WASM CPS transform cannot fire here
7+
// (`thenableThen` is not importable). Lowering it synchronously would run
8+
// the continuation against an UNSETTLED handle — the silent miscompile #556
9+
// closes. The backend must now fail loudly with an UnsupportedFeature error.
10+
extern fn getThenable(u: Int) -> Int / { Async };
11+
12+
fn get(u: Int) -> Int / { Async } {
13+
let bumped = u + 1;
14+
let h = getThenable(bumped);
15+
return h + 0;
16+
}
17+
18+
fn main() -> Int {
19+
return get(7);
20+
}

test/test_e2e.ml

Lines changed: 45 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -2268,6 +2268,50 @@ let handler_fence_tests = [
22682268
Alcotest.test_case "deno-esm: handle → loud failure" `Quick test_handle_deno_loud_fail;
22692269
]
22702270

2271+
(* ============================================================================
2272+
Issue #556: async CPS table-miss loud-fail fence
2273+
============================================================================
2274+
2275+
gen_function previously fell through to synchronous `gen_expr` whenever the
2276+
ADR-013 CPS transform did not fire — even for an `Async` fn that performs an
2277+
async call whose result is consumed by a continuation. That silently ran the
2278+
continuation against an unsettled `Thenable` handle (a wrong value, no
2279+
diagnostic). The fence makes that case fail loudly, while still lowering the
2280+
sound shapes: the `let r = <async-call>; <cont>` base case (transformed), the
2281+
bare tail-return-`Thenable` pass-through (#205 convergence protocol), and an
2282+
`Async` fn that performs no async call at all. *)
2283+
2284+
let test_async_wasm_loud_fail () =
2285+
match run_wasm_pipeline (fixture "async_sync_fallback.affine") with
2286+
| Ok _ ->
2287+
Alcotest.fail
2288+
"expected UnsupportedFeature for an un-lowerable async-consuming fn \
2289+
on core-WASM (Refs #556); got Ok — silent synchronous fallback has \
2290+
regressed"
2291+
| Error msg ->
2292+
Alcotest.(check bool) "error names the async fence" true
2293+
(contains_str "async function" msg)
2294+
2295+
let test_async_passthrough_still_compiles () =
2296+
(* Tail-return-Thenable pass-through (#205): sound to lower synchronously;
2297+
the fence must not over-reject it. *)
2298+
match run_wasm_pipeline (fixture "async_passthrough_thenable.affine") with
2299+
| Error msg -> Alcotest.failf "async pass-through should compile, got: %s" msg
2300+
| Ok _ -> ()
2301+
2302+
let test_async_no_boundary_still_compiles () =
2303+
(* `Async` row but no async call ⇒ no continuation to mis-order; must
2304+
compile (the guard keys on an actual async-prim call, not the row). *)
2305+
match run_wasm_pipeline (fixture "async_no_boundary.affine") with
2306+
| Error msg -> Alcotest.failf "async-rowed fn with no async call should compile, got: %s" msg
2307+
| Ok _ -> ()
2308+
2309+
let async_fence_tests = [
2310+
Alcotest.test_case "wasm: async-consuming fn → loud UnsupportedFeature" `Quick test_async_wasm_loud_fail;
2311+
Alcotest.test_case "wasm: tail-return-Thenable pass-through compiles" `Quick test_async_passthrough_still_compiles;
2312+
Alcotest.test_case "wasm: async row without async call compiles" `Quick test_async_no_boundary_still_compiles;
2313+
]
2314+
22712315
(* ============================================================================
22722316
Issue #555: interpreter resume soundness (multi-shot loud-fail)
22732317
============================================================================
@@ -5479,6 +5523,7 @@ let tests =
54795523
("E2E LSP Phase D", lsp_phase_d_tests);
54805524
("E2E Try/Catch/Finally", try_catch_tests);
54815525
("E2E Handler Fence (#555)", handler_fence_tests);
5526+
("E2E Async Fence (#556)", async_fence_tests);
54825527
("E2E Resume Soundness (#555)", resume_soundness_tests);
54835528
("E2E Ownership Verify", tw_verify_tests);
54845529
("E2E Cmd Linearity", cmd_linear_tests);

0 commit comments

Comments
 (0)