From c6a3259a6220571f8a89212c72c8581996501512 Mon Sep 17 00:00:00 2001
From: Joseph Ferano <joseph@ferano.io>
Date: Fri, 25 Sep 2026 20:33:11 +0700
Subject: [PATCH 1/3] A function that returns or stores into a global an
 address or slice of its own frame is refused, a dev free-all poisons any
 arena's released bytes and ASan sees them released, and @sanitize checks
 stack use after return

---
 TODO.org                                 |  16 +-
 lib/check.ml                             | 185 +++++++++++++++++++++++
 runtime/flan_rt.c                        |  48 +++++-
 test/dune                                |   3 +-
 test/programs/arena-free-all-poison.flan |   8 +
 test/test_acceptance.ml                  |   8 +
 test/test_flan.ml                        |  56 ++++++-
 test/test_sanitize.ml                    |   8 +-
 8 files changed, 314 insertions(+), 18 deletions(-)
 create mode 100644 test/programs/arena-free-all-poison.flan

diff --git a/TODO.org b/TODO.org
index 72d9a41b..7a1bfdb8 100644
--- a/TODO.org
+++ b/TODO.org
@@ -868,13 +868,12 @@ correct code, so any per-push flag is a false positive by the language's own
 semantics; the refined version needs liveness across control flow, which is the
 flow tracking that was repealed.
 
-** NEXT Catching a use-after-release statically
-Decided 2026-09-25 (91): build (A) Odin's unsafe-return refusal — returning (addr local), (slice local-array …) or (addr (at local-array i)); (B) the same test on a set into a global; (C) dev fills a fixed arena's freed bytes with poison on free-all; (D) detect_stack_use_after_return=1 for @sanitize. Rules out a with-allocator escape check: the runtime epoch check catches it and a static rule flags building into the caller's arena. Probes: p1-p16 of the study.
-Decided 2026-09-25: a study, not a build — how arena memory escapes in real Flan code, and whether a sound lexical check would catch most of it. The result goes in docs/BUILT.md; nothing is built on it without the author.
-Open, and for the first time with evidence available: the epoch trap is built, and
-there is a =Vec= to write real arena programs with, so whether the escapes that
-actually occur are lexical can now be answered. The next thing to look at, not the
-next thing to build.
+** DONE Catching a use-after-release statically
+CLOSED: [2026-09-25]
+Studied (p1-p16); the compile-time checks that fit are returning, or storing into a global, an address or slice of the function's own frame. Rules out lexical tracking of arena and heap releases: the rest of the escapes the study found are the runtime epoch check's and the dev poison's.
+
+** CANCELLED A with-allocator escape check
+The runtime epoch check already catches it, and a static rule flags the normal idiom of building into the caller's arena.
 
 ** DONE (vec-new [u8]) is refused
 CLOSED: [2026-09-25]
@@ -1177,6 +1176,9 @@ dev build wipes it at a top-level agent poll; an expression run at a stop gets a
 
 * Runtime
 
+** TODO Heap quarantine in dev
+A dev build could hold freed heap blocks back from reuse for a while (Zig's debug allocator), so a read after a free sees poison rather than a new owner's data.
+
 ** DONE An index out of range is a condition
 CLOSED: [2026-09-13]
 A failed bounds check signals =BoundsError=; a handler can answer it, a
diff --git a/lib/check.ml b/lib/check.ml
index aede389e..3103436c 100644
--- a/lib/check.ml
+++ b/lib/check.ml
@@ -13415,6 +13415,187 @@ let escaping_names ~returns (body : Ast.expr list) : string list =
   if returns then (match List.rev body with x :: _ -> tails x | [] -> ());
   !names
 
+(* A value handed out of [f] that points into [f]'s own frame: returned (the
+   last form's tails, or a [return]), or stored into a global or a field or
+   array element of one. Both read a dead frame the moment [f] returns, so
+   both are refused.
+
+   Deliberately narrow — the exact spellings that can only be wrong, so
+   nothing that could be valid is ever refused:
+   - [(addr p)] where [p] is a local, a field of one, or an element of a
+     local *array* (an array's elements are the frame's bytes; a Vec's or a
+     slice's are not);
+   - [(slice a …)] where [a] is such a place of array type;
+   - a local bound by [let] to one of those and never assigned or addressed
+     afterwards, which is also how a [return] under a [defer] arrives here.
+   A parameter is a local: its value is copied into the frame (an array
+   parameter too), so its address dies with the frame as well. Anything
+   reached through a [Ptr] is not the frame's, and a struct literal holding
+   such an address is not looked into.
+
+   The store is let through in two cases where it can be right. In [main],
+   whose frame outlives everything the program runs. And where the function
+   sets that same global again elsewhere — the stash-then-restore shape, the
+   global pointed at the frame only while the frame was live. *)
+let refuse_frame_escapes (f : Tast.fn) =
+  (* Keyed by slot alone: [fresh_slot] never reuses one, so a slot has at
+     most one binding [Let] in the function. *)
+  let binds = Hashtbl.create 16 in
+  let unstable = Hashtbl.create 16 in
+  let global_sets = Hashtbl.create 8 in
+  let rec place_global = function
+    | Tast.Pglobal g -> Some g
+    | Tast.Pfield (t, _) -> expr_global t
+    | Tast.Pindex (t, idx) when all_array t.Tast.ty idx -> expr_global t
+    | _ -> None
+  and expr_global (e : Tast.expr) =
+    match e.Tast.e with
+    | Tast.Global g -> Some g
+    | Tast.Field (t, _) -> expr_global t
+    | Tast.Prim (Tast.At, t :: idx) when all_array t.Tast.ty idx -> expr_global t
+    | _ -> None
+  (* [(at a i j)] is one node carrying every index; each level stepped must
+     be an array for the element to be inside [a]'s own bytes. *)
+  and all_array ty = function
+    | [] -> true
+    | _ :: rest ->
+      (match ty with Types.Array (_, el) -> all_array el rest | _ -> false)
+  in
+  List.iter
+    (Tast.walk (fun (e : Tast.expr) ->
+         match e.Tast.e with
+         | Tast.Let (bs, _) -> List.iter (fun (s, v) -> Hashtbl.replace binds s v) bs
+         | Tast.Set (Tast.Plocal s, _) | Tast.Addr (Tast.Plocal s) ->
+           Hashtbl.replace unstable s ()
+         | Tast.Set (p, _) ->
+           Option.iter
+             (fun g ->
+                Hashtbl.replace global_sets g
+                  (1 + Option.value ~default:0 (Hashtbl.find_opt global_sets g)))
+             (place_global p)
+         | _ -> ()))
+    f.Tast.body;
+  (* The local at the root of a place inside this frame, if it is one. *)
+  let rec root_expr (e : Tast.expr) =
+    match e.Tast.e with
+    | Tast.Local s -> Some s
+    | Tast.Field (t, _) -> root_expr t
+    | Tast.Prim (Tast.At, t :: idx) when all_array t.Tast.ty idx -> root_expr t
+    | _ -> None
+  in
+  let root_place = function
+    | Tast.Plocal s -> Some s
+    | Tast.Pfield (t, _) -> root_expr t
+    | Tast.Pindex (t, idx) when all_array t.Tast.ty idx -> root_expr t
+    | _ -> None
+  in
+  (* What escapes: the root local, whether it is a slice (else an address),
+     and whether the place is the bare local rather than a path into it —
+     only then can the fix be spelled with its name alone. *)
+  let rec escapes depth (e : Tast.expr) =
+    match e.Tast.e with
+    | Tast.Addr p ->
+      Option.map
+        (fun s ->
+           (e, (s, `Addr, (match p with Tast.Plocal _ -> true | _ -> false))))
+        (root_place p)
+    | Tast.Prim (Tast.Slice, [ t; _; _ ]) ->
+      (match t.Tast.ty with
+       | Types.Array _ ->
+         Option.map
+           (fun s ->
+              ( e,
+                (s, `Slice,
+                 (match t.Tast.e with Tast.Local _ -> true | _ -> false)) ))
+           (root_expr t)
+       | _ -> None)
+    | Tast.Local s when depth < 32 && not (Hashtbl.mem unstable s) ->
+      Option.bind (Hashtbl.find_opt binds s) (escapes (depth + 1))
+    | _ -> None
+  in
+  (* A slot with no name is a value the function made for itself, such as
+     the array a literal like [(slice [7 8 9])] is stored in. *)
+  let what (s, kind, exact) =
+    match f.Tast.snames.(s), kind, exact with
+    | Some n, `Slice, true -> "a slice of " ^ n
+    | Some n, `Slice, false -> "a slice of an array inside " ^ n
+    | Some n, `Addr, true -> "the address of " ^ n
+    | Some n, `Addr, false -> "an address inside " ^ n
+    | None, `Slice, _ -> "a slice of a temporary array"
+    | None, `Addr, _ -> "the address of a temporary"
+  in
+  (* Reported at the addr or slice itself: a [return] under a [defer], or a
+     local bound to one, reaches here as a read of a slot, and the caret
+     belongs on the form that took the address. *)
+  let fail ~verb ~target ~fix_slice ~fix_addr
+      ((e : Tast.expr), ((s, kind, exact) as hit)) =
+    let fix =
+      match f.Tast.snames.(s), kind, exact with
+      | Some n, `Slice, true ->
+        fix_slice ("wrap the slice in clone, as in (clone (slice " ^ n ^ "))")
+      | _, `Slice, _ -> fix_slice "wrap the slice in (clone ...)"
+      | _, `Addr, _ ->
+        let pointee =
+          match e.Tast.ty with
+          | Types.Ptr (_, t) -> Types.to_string t
+          | t -> Types.to_string t
+        in
+        fix_addr pointee
+    in
+    let whose =
+      match f.Tast.snames.(s) with
+      | Some n -> Printf.sprintf "%s is a local of %s" n f.Tast.name
+      | None -> "That value lives in " ^ f.Tast.name ^ "'s frame"
+    in
+    Loc.failk "check/frame-escape" e.Tast.loc
+      "%s %s %s%s. %s, and its storage is gone once %s returns, so every \
+       later read through it reads whatever the next call leaves there. %s"
+      f.Tast.name verb (what hit) target whose f.Tast.name fix
+  in
+  let rec tails (e : Tast.expr) =
+    match e.Tast.e with
+    | Tast.Do es | Tast.Let (_, es) | Tast.WithAlloc (_, es) ->
+      (match List.rev es with x :: _ -> tails x | [] -> ())
+    | Tast.If (_, a, b) -> tails a; tails b
+    | Tast.Match (_, arms) ->
+      List.iter
+        (fun (a : Tast.arm) ->
+           match List.rev a.Tast.abody with x :: _ -> tails x | [] -> ())
+        arms
+    | _ ->
+      Option.iter
+        (fail ~verb:"returns" ~target:""
+           ~fix_slice:(fun c ->
+               "Return a copy the caller owns: " ^ c
+               ^ ", which puts the elements in the context allocator")
+           ~fix_addr:(fun t ->
+               "Return the value instead: declare " ^ f.Tast.name
+               ^ " to return " ^ t ^ " and drop the addr"))
+        (escapes 0 e)
+  in
+  let returns = not (Types.equal f.Tast.ret Types.Unit) in
+  List.iter
+    (Tast.walk (fun (e : Tast.expr) ->
+         match e.Tast.e with
+         | Tast.Return (Some v) when returns -> tails v
+         | Tast.Set (p, v) when not (String.equal f.Tast.name "main") ->
+           (match place_global p with
+            | Some g when Hashtbl.find_opt global_sets g = Some 1 ->
+              Option.iter
+                (fail ~verb:"stores" ~target:(" into the global " ^ g)
+                   ~fix_slice:(fun c ->
+                       "Store a copy that outlives the frame: " ^ c
+                       ^ ", which puts the elements in the context allocator")
+                   ~fix_addr:(fun t ->
+                       "Store the value instead: declare " ^ g ^ " as " ^ t
+                       ^ " and drop the addr"))
+                (escapes 0 v)
+            | _ -> ())
+         | _ -> ()))
+    f.Tast.body;
+  if returns then
+    match List.rev f.Tast.body with x :: _ -> tails x | [] -> ()
+
 let rec check_fn env (fn : Ast.fn) : Tast.fn =
   let params, ret = Hashtbl.find env.fns fn.Ast.name in
   let ctx = { (invented_ctx env ret) with owner = fn.Ast.name } in
@@ -13545,6 +13726,7 @@ let rec check_fn env (fn : Ast.fn) : Tast.fn =
     | None -> body
     | Some s -> defer_counter_zero s fn.Ast.nloc :: body
   in
+  let checked =
   { Tast.name = fn.Ast.name; params;
     slots = Array.of_list (List.rev ctx.slot_tys);
     snames = Array.of_list (List.rev ctx.slot_names);
@@ -13558,6 +13740,9 @@ let rec check_fn env (fn : Ast.fn) : Tast.fn =
        | None -> ctx.defers
        | Some s -> guarded_defers s ctx.defers);
     fenv = None; fparent = None; floc = fn.Ast.nloc }
+  in
+  refuse_frame_escapes checked;
+  checked
 
 (* The generic body, checked once with its variables abstract. Nothing is kept
    — the [Tast.fn] it produces is thrown away, and so is anything it lifted —
diff --git a/runtime/flan_rt.c b/runtime/flan_rt.c
index 8801cff7..28564e0e 100644
--- a/runtime/flan_rt.c
+++ b/runtime/flan_rt.c
@@ -1858,6 +1858,30 @@ static flan_allocator flan_heap = {
 #define FLAN_VG_MAKE_MEM_UNDEFINED(p, n) ((void)(p), (void)(n))
 #endif
 
+/* The same fact told to AddressSanitizer: an arena's released bytes are
+ * poisoned at free-all, so a read through a slice kept past it reports under
+ * --sanitize instead of printing what is there. Every path that hands arena
+ * bytes back out — the bump, a resize in place, the temp arena's text fast
+ * path — unpoisons exactly what it hands out, and every path that writes
+ * over released bytes itself (the dev fill, a chunk dropped or freed)
+ * unpoisons first. */
+#if defined(__SANITIZE_ADDRESS__)
+#define FLAN_ASAN 1
+#elif defined(__has_feature)
+#if __has_feature(address_sanitizer)
+#define FLAN_ASAN 1
+#endif
+#endif
+#ifdef FLAN_ASAN
+void __asan_poison_memory_region(void const volatile *addr, size_t size);
+void __asan_unpoison_memory_region(void const volatile *addr, size_t size);
+#define FLAN_ASAN_POISON(p, n) __asan_poison_memory_region((p), (size_t)(n))
+#define FLAN_ASAN_UNPOISON(p, n) __asan_unpoison_memory_region((p), (size_t)(n))
+#else
+#define FLAN_ASAN_POISON(p, n) ((void)(p), (void)(n))
+#define FLAN_ASAN_UNPOISON(p, n) ((void)(p), (void)(n))
+#endif
+
 /* -- The arena: one fixed backing buffer and a bump offset. ----------
  *
  * `free-all` is retain-capacity: offset = 0, the pages stay. That is an
@@ -1923,6 +1947,7 @@ static void flan_arena_drop_old(flan_arena *ar) {
     flan_chunk *c = ar->old;
     ar->old = c->next;
     flan_dev_reg_dead_range(c->base, c->cap);
+    FLAN_ASAN_UNPOISON(c->base, c->cap);
     flan_dev_poison(c->base, c->cap);
     free(c->base);
     free(c);
@@ -1955,6 +1980,7 @@ static void *flan_arena_proc(flan_allocator *a, int32_t mode, void *p,
     if (end > ar->peak) ar->peak = end;
     a->live_blocks++;
     a->live_bytes += size;
+    FLAN_ASAN_UNPOISON(ar->base + start, size);
     return ar->base + start;
   }
   case FLAN_ALLOC_RESIZE: {
@@ -1974,6 +2000,7 @@ static void *flan_arena_proc(flan_allocator *a, int32_t mode, void *p,
       ar->offset = end;
       if (end > ar->peak) ar->peak = end;
       a->live_bytes += size - old_size;
+      FLAN_ASAN_UNPOISON(p, size);
       return p;
     }
     q = flan_arena_proc(a, FLAN_ALLOC_ALLOC, NULL, 0, size, align);
@@ -2005,11 +2032,14 @@ static void *flan_arena_proc(flan_allocator *a, int32_t mode, void *p,
        cheaper if the second could be skipped. */
     flan_arena_drop_old(ar);
     flan_dev_reg_dead_range(ar->base, ar->cap);
-    /* The temp arena's wipe, in a dev build, fills what was handed out with
-       the pattern a moved Vec's old buffer gets, so text kept past its frame
-       without a clone reads as garbage rather than as last frame's value. */
-    if (ar->grow) flan_dev_poison(ar->base, ar->offset);
+    /* A dev build fills what was handed out with the pattern a moved Vec's
+       old buffer gets, so a slice or text kept past the free-all reads as
+       garbage rather than as the last round's values — the temp arena and a
+       program's own arena alike. A release build leaves the bytes. */
+    FLAN_ASAN_UNPOISON(ar->base, ar->offset);
+    flan_dev_poison(ar->base, ar->offset);
     FLAN_VG_MAKE_MEM_UNDEFINED(ar->base, ar->cap);
+    FLAN_ASAN_POISON(ar->base, ar->cap);
     ar->offset = 0;
     a->live_blocks = 0;
     a->live_bytes = 0;
@@ -2259,6 +2289,7 @@ void flan_arena_destroy(flan_allocator *a) {
   a->epoch++;
   flan_arena_drop_old(ar);
   flan_dev_reg_dead_range(ar->base, ar->cap);
+  FLAN_ASAN_UNPOISON(ar->base, ar->cap);
   free(ar->base);
   free(ar);
   flan_header_retire(a);
@@ -2519,7 +2550,10 @@ static int8_t flan_temp_text(flan_render render, const void *x,
   ar = (flan_arena *)a->data;
   if (a->budget <= 0 && ar->cap - ar->offset >= FLAN_NUM_BYTES) {
     q = ar->base + ar->offset;
+    FLAN_ASAN_UNPOISON(q, FLAN_NUM_BYTES);
     len = fit(render(x, (char *)q, FLAN_NUM_BYTES));
+    /* The tail the text did not use goes back to released. */
+    FLAN_ASAN_POISON(q + len, FLAN_NUM_BYTES - len);
     ar->offset += len;
     if (ar->offset > ar->peak) ar->peak = ar->offset;
     a->live_blocks++;
@@ -2752,9 +2786,9 @@ void flan_vec_as_slice(flan_vec *v, void *out, int32_t lo, int32_t hi,
 }
 
 /* spec-memory.md's first release point. The Vec is left zeroed rather than
- * dangling — the checker has already made using it afterwards a compile error,
- * and zeroing costs nothing and makes a bug that slips past the checker a null
- * deref rather than a use-after-free. An allocator without can-free keeps the
+ * dangling: a later use of it is then a null deref rather than a
+ * use-after-free, and a slice taken of it before the free is the dev
+ * registry's to catch. An allocator without can-free keeps the
  * block: releasing it is free-all's job, and pretending otherwise here is the
  * silent-no-op this file refuses elsewhere. */
 void flan_vec_free(flan_vec *v, int64_t size, int64_t align,
diff --git a/test/dune b/test/dune
index 87b732d4..8d773345 100644
--- a/test/dune
+++ b/test/dune
@@ -134,7 +134,8 @@
  (deps
   (alias corpus)
   test_sanitize.exe
-  ; ASAN_OPTIONS=detect_leaks=1 asks the leak question; see test_sanitize.ml.
+  ; ASAN_OPTIONS=detect_leaks=1:detect_stack_use_after_return=1 asks the leak
+  ; question and keeps the frame check; see test_sanitize.ml.
   (env_var ASAN_OPTIONS)
   ; The dyn runtime's C main, which is the one thing in this sweep that is not
   ; a Flan program: flan_dyn.c has no Flan spelling yet. It is also the one
diff --git a/test/programs/arena-free-all-poison.flan b/test/programs/arena-free-all-poison.flan
new file mode 100644
index 00000000..378b53ac
--- /dev/null
+++ b/test/programs/arena-free-all-poison.flan
@@ -0,0 +1,8 @@
+;;;; A slice kept past its arena's free-all. A dev build fills the released
+;;;; bytes with 0xDEADBEEF, so the element reads -559038737; a release build
+;;;; leaves the old value, 7.
+(defn main [] i32
+  (let [a (arena-new 4096) v (vec-new i32 a)]
+    (push v 7)
+    (let [s (slice v)] (free-all a) (println (at s 0))))
+  0)
diff --git a/test/test_acceptance.ml b/test/test_acceptance.ml
index 71bc029f..1234ccf3 100644
--- a/test/test_acceptance.ml
+++ b/test/test_acceptance.ml
@@ -1087,6 +1087,14 @@ let () =
     outputs ~dev:true "a dev free-temp poisons the wiped text" tg (tg_out "239");
     outputs ~dev:true ~x86:true "a dev free-temp poisons the wiped text, --x86"
       tg (tg_out "239");
+    let fp = "programs/arena-free-all-poison.flan" in
+    outputs "a release free-all leaves the arena's bytes" fp "7\n";
+    outputs ~dev:true "a dev free-all poisons a program's own arena" fp
+      "-559038737\n";
+    outputs ~dev:true ~opt:"-O0" "a dev free-all poisons a program's own arena, -O0"
+      fp "-559038737\n";
+    outputs ~dev:true ~x86:true
+      "a dev free-all poisons a program's own arena, --x86" fp "-559038737\n";
     (* A dev build's agent poll is a frame boundary and wipes the temp
        allocator itself: a loop that polls and never calls free-temp does not
        fill the registry. *)
diff --git a/test/test_flan.ml b/test/test_flan.ml
index 38f09568..cf4aa30b 100644
--- a/test/test_flan.ml
+++ b/test/test_flan.ml
@@ -2203,7 +2203,10 @@ let () =
     "(defn mk [] [3 i32] [7 8 9]) (defn f [] [i32] (slice (mk) 0 3))"
     ~needle:"a temporary the slice would outlive";
   accepts "slice of an array literal"
-    "(defn f [] [i32] (slice [7 8 9]))";
+    "(defn f [] i32 (at (slice [7 8 9]) 0))";
+  rejects_check "returning a slice of an array literal"
+    "(defn f [] [i32] (slice [7 8 9]))"
+    ~needle:"f returns a slice of a temporary array";
   (* One builtin, one answer about a bound. A slice bound is a subscript and
      goes through [index_expr] like every other one, so a u32 is admitted on
      an array exactly as it always was on a Vec, and an i64 is refused by name
@@ -3356,6 +3359,57 @@ let () =
   rejects_check "a dead-beef pattern out of u32 range"
     "(defn f [] () (let [a (array 4 u8)] (set a (dead-beef 0x1DEADBEEF))))"
     ~needle:"does not fit in u32";
+  (* A pointer or slice into the frame, handed out of it. *)
+  rejects_check "returning the address of a local"
+    "(defn mk [] (Ptr i32) (let [x (i32 42)] (addr x)))"
+    ~needle:"mk returns the address of x";
+  rejects_check "returning the address of a local with return"
+    "(defn mk [] (Ptr i32) (let [x (i32 42)] (return (addr x))))"
+    ~needle:"mk returns the address of x";
+  rejects_check "returning the address of a local under a defer"
+    "(defn mk [] (Ptr i32) (let [x (i32 42)] (defer (println 1)) \
+     (return (addr x))))"
+    ~needle:"mk returns the address of x";
+  rejects_check "returning a slice of a local array"
+    "(defn mk [] [i32] (let [a [1 2 3 4]] (slice a)))"
+    ~needle:"mk returns a slice of a";
+  rejects_check "returning a local bound to a slice of a local array"
+    "(defn mk [] [i32] (let [a [1 2 3 4] s (slice a 1 3)] s))"
+    ~needle:"(clone (slice a))";
+  rejects_check "returning a slice of an array parameter"
+    "(defn mk [a [4 i32]] [i32] (slice a))"
+    ~needle:"mk returns a slice of a";
+  rejects_check "returning the address of a local array's element"
+    "(defn mk [] (Ptr i32) (let [a [1 2 3 4]] (addr (at a 2))))"
+    ~needle:"mk returns an address inside a";
+  rejects_check "returning the address of a local from one if arm"
+    "(defn mk [c bool] (Ptr i32) (let [x (i32 1)] (if c (addr x) (addr x))))"
+    ~needle:"declare mk to return i32";
+  rejects_check "storing a slice of a local array into a global"
+    "(defonce g [i32]) (defn stash [] () (let [a [5 6 7]] (set g (slice a))))"
+    ~needle:"stash stores a slice of a into the global g";
+  rejects_check "storing a local field's address into a global"
+    "(defstruct P [x i32 y i32]) (defonce g (Ptr i32)) \
+     (defn stash [] () (let [p (P 1 2)] (set g (addr (.y p)))))"
+    ~needle:"declare g as i32";
+  (* And what is left alone: storage that outlives the frame, a slice of a
+     Vec, a pointer passed in, a stash the function restores, and main. *)
+  accepts "a slice of a Vec is returned"
+    "(defn mk [] [i32] (let [v (vec-new i32)] (push v 1) (slice v)))";
+  accepts "an element of a slice parameter is returned"
+    "(defn mk [s [i32]] (Ptr i32) (addr (at s 0)))";
+  accepts "a slice of a global array is returned"
+    "(defonce k [3 i32]) (defn mk [] [i32] (slice k))";
+  accepts "a local reassigned before it is returned"
+    "(defonce k [3 i32]) \
+     (defn mk [] [i32] (let [a [1 2 3] s (slice a)] (set s (slice k)) s))";
+  accepts "a global stashed and restored"
+    "(defonce g [i32]) (defonce k [3 i32]) \
+     (defn f [] () (let [a [1 2 3]] (set g (slice a)) (set g (slice k))))";
+  accepts "main stores its own local into a global"
+    "(defonce g (Ptr i32)) (defn main [] i32 (let [x (i32 5)] (set g (addr x))) 0)";
+  accepts "a unit function's last form is not returned"
+    "(defn f [] () (let [x (i32 4)] (addr x)))";
   (* A fill is never a value the linker can write into the image, so a
      defconst of one is refused by the constant rule rather than by anything
      of this feature's own. A defonce is fine: its initialiser runs at
diff --git a/test/test_sanitize.ml b/test/test_sanitize.ml
index 422dc8aa..529864d9 100644
--- a/test/test_sanitize.ml
+++ b/test/test_sanitize.ml
@@ -43,10 +43,13 @@ let scratch = Test_support.scratch
    by design — [rt_args] says so in its own comment — so LeakSanitizer here
    produces a suppression list and no information. Set in the environment
    rather than baked in, so a session asking the leak question can ask it.
+   [detect_stack_use_after_return] moves frames to a fake stack that is
+   poisoned when the function returns, so a pointer or slice into a frame that
+   has returned reports rather than reading whatever the next call left.
    [print_stacktrace] is what turns a UBSan report from a source line into
    something with a caller in it, and it is off by default. *)
 let env =
-  "ASAN_OPTIONS=${ASAN_OPTIONS:-detect_leaks=0} \
+  "ASAN_OPTIONS=${ASAN_OPTIONS:-detect_leaks=0:detect_stack_use_after_return=1} \
    UBSAN_OPTIONS=${UBSAN_OPTIONS:-print_stacktrace=1} "
 
 let run exe args =
@@ -486,7 +489,8 @@ let dev_session () =
   let fd = Unix.openfile log [ Unix.O_WRONLY; Unix.O_CREAT; Unix.O_TRUNC ] 0o600 in
   let env =
     Array.append (Unix.environment ())
-      [| "ASAN_OPTIONS=detect_leaks=0"; "UBSAN_OPTIONS=print_stacktrace=1" |]
+      [| "ASAN_OPTIONS=detect_leaks=0:detect_stack_use_after_return=1";
+         "UBSAN_OPTIONS=print_stacktrace=1" |]
   in
   let pid =
     Unix.create_process_env flan

From a6ccce0e6741a42c0da4695a8fc192355a52b164 Mon Sep 17 00:00:00 2001
From: Joseph Ferano <joseph@ferano.io>
Date: Fri, 25 Sep 2026 20:50:17 +0700
Subject: [PATCH 2/3] Every store of a frame address into a global outside main
 is refused, fn and handler bodies and restart clauses are checked as frames
 of their own, and the suggested clone keeps the slice's bounds

---
 lib/check.ml      | 427 ++++++++++++++++++++++++++--------------------
 test/test_flan.ml |  32 +++-
 2 files changed, 270 insertions(+), 189 deletions(-)

diff --git a/lib/check.ml b/lib/check.ml
index 3103436c..10d65729 100644
--- a/lib/check.ml
+++ b/lib/check.ml
@@ -3084,6 +3084,240 @@ let view_not_permanent loc (container : Types.t) =
      the other"
     (Types.to_string container) (Types.to_string container)
 
+(* A value handed out of [f] that points into [f]'s own frame: returned (the
+   last form's tails, or a [return]), or stored into a global or a field or
+   array element of one. Both read a dead frame the moment [f] returns, so
+   both are refused.
+
+   Deliberately narrow — the exact spellings that can only be wrong, so
+   nothing that could be valid is ever refused:
+   - [(addr p)] where [p] is a local, a field of one, or an element of a
+     local *array* (an array's elements are the frame's bytes; a Vec's or a
+     slice's are not);
+   - [(slice a …)] where [a] is such a place of array type;
+   - a local bound by [let] to one of those and never assigned or addressed
+     afterwards, which is also how a [return] under a [defer] arrives here.
+   A parameter is a local: its value is copied into the frame (an array
+   parameter too), so its address dies with the frame as well. Anything
+   reached through a [Ptr] is not the frame's, and a struct literal holding
+   such an address is not looked into.
+
+   The store is let through in [main], whose frame outlives everything the
+   program runs.
+
+   A lifted [fn] literal or handler clause is checked as a function of its
+   own: its parameters, its locals and its copies of what it captured are its
+   frame. What this does not see is the enclosing function's frame escaping
+   *through* one — a closure over a pointer to a local, handed out — because
+   that is a value holding an address, not one of the spellings above. *)
+let refuse_frame_escapes (f : Tast.fn) =
+  (* Keyed by slot alone: [fresh_slot] never reuses one, so a slot has at
+     most one binding [Let] in the function. *)
+  let binds = Hashtbl.create 16 in
+  let unstable = Hashtbl.create 16 in
+  let rec place_global = function
+    | Tast.Pglobal g -> Some g
+    | Tast.Pfield (t, _) -> expr_global t
+    | Tast.Pindex (t, idx) when all_array t.Tast.ty idx -> expr_global t
+    | _ -> None
+  and expr_global (e : Tast.expr) =
+    match e.Tast.e with
+    | Tast.Global g -> Some g
+    | Tast.Field (t, _) -> expr_global t
+    | Tast.Prim (Tast.At, t :: idx) when all_array t.Tast.ty idx -> expr_global t
+    | _ -> None
+  (* [(at a i j)] is one node carrying every index; each level stepped must
+     be an array for the element to be inside [a]'s own bytes. *)
+  and all_array ty = function
+    | [] -> true
+    | _ :: rest ->
+      (match ty with Types.Array (_, el) -> all_array el rest | _ -> false)
+  in
+  List.iter
+    (Tast.walk (fun (e : Tast.expr) ->
+         match e.Tast.e with
+         | Tast.Let (bs, _) -> List.iter (fun (s, v) -> Hashtbl.replace binds s v) bs
+         | Tast.Set (Tast.Plocal s, _) | Tast.Addr (Tast.Plocal s) ->
+           Hashtbl.replace unstable s ()
+         | _ -> ()))
+    f.Tast.body;
+  (* The local at the root of a place inside this frame, if it is one. *)
+  let rec root_expr (e : Tast.expr) =
+    match e.Tast.e with
+    | Tast.Local s -> Some s
+    | Tast.Field (t, _) -> root_expr t
+    | Tast.Prim (Tast.At, t :: idx) when all_array t.Tast.ty idx -> root_expr t
+    | _ -> None
+  in
+  let root_place = function
+    | Tast.Plocal s -> Some s
+    | Tast.Pfield (t, _) -> root_expr t
+    | Tast.Pindex (t, idx) when all_array t.Tast.ty idx -> root_expr t
+    | _ -> None
+  in
+  (* What escapes: the root local, whether it is a slice (else an address),
+     and whether the place is the bare local rather than a path into it —
+     only then can the fix be spelled with its name alone. *)
+  let rec escapes depth (e : Tast.expr) =
+    match e.Tast.e with
+    | Tast.Addr p ->
+      Option.map
+        (fun s ->
+           (e, (s, `Addr, (match p with Tast.Plocal _ -> true | _ -> false))))
+        (root_place p)
+    | Tast.Prim (Tast.Slice, [ t; _; _ ]) ->
+      (match t.Tast.ty with
+       | Types.Array _ ->
+         Option.map
+           (fun s ->
+              ( e,
+                (s, `Slice,
+                 (match t.Tast.e with Tast.Local _ -> true | _ -> false)) ))
+           (root_expr t)
+       | _ -> None)
+    | Tast.Local s when depth < 32 && not (Hashtbl.mem unstable s) ->
+      Option.bind (Hashtbl.find_opt binds s) (escapes (depth + 1))
+    | _ -> None
+  in
+  (* A slot with no name is a value the function made for itself, such as
+     the array a literal like [(slice [7 8 9])] is stored in. *)
+  (* What a lifted body is called in a message: its symbol is the compiler's. *)
+  let who =
+    let starts p =
+      String.length f.Tast.name >= String.length p
+      && String.sub f.Tast.name 0 (String.length p) = p
+    in
+    if starts "fn/" then "this fn"
+    else if starts "handler/" then "this handler"
+    else f.Tast.name
+  in
+  let what (s, kind, exact) =
+    match f.Tast.snames.(s), kind, exact with
+    | Some n, `Slice, true -> "a slice of " ^ n
+    | Some n, `Slice, false -> "a slice of an array inside " ^ n
+    | Some n, `Addr, true -> "the address of " ^ n
+    | Some n, `Addr, false -> "an address inside " ^ n
+    | None, `Slice, _ -> "a slice of a temporary array"
+    | None, `Addr, _ -> "the address of a temporary"
+  in
+  (* Reported at the addr or slice itself: a [return] under a [defer], or a
+     local bound to one, reaches here as a read of a slot, and the caret
+     belongs on the form that took the address. *)
+  let fail ~verb ~target ~fix_slice ~fix_addr
+      ((e : Tast.expr), ((s, kind, exact) as hit)) =
+    let fix =
+      (* The slice as written, bounds and all, when the source can be read
+         back; its root's name otherwise. *)
+      let rec bound (b : Tast.expr) =
+        match b.Tast.e with
+        | Tast.Int (v, _) -> Some (Int64.to_string v)
+        | Tast.Local i -> f.Tast.snames.(i)
+        | Tast.Prim (Tast.Cast _, [ x ]) -> bound x
+        | _ -> None
+      in
+      let rebuilt =
+        match e.Tast.e, f.Tast.snames.(s), exact with
+        | Tast.Prim (Tast.Slice, [ t; lo; hi ]), Some n, true ->
+          (match t.Tast.ty, bound lo, bound hi with
+           | Types.Array (len, _), Some "0", Some h
+             when h = Int64.to_string len ->
+             Some ("(slice " ^ n ^ ")")
+           | _, Some l, Some h -> Some ("(slice " ^ n ^ " " ^ l ^ " " ^ h ^ ")")
+           | _ -> None)
+        | _ -> None
+      in
+      let written =
+        match rebuilt, Loc.snippet ~lim:120 e.Tast.loc with
+        | Some t, _ -> Some t
+        | None, Some t
+          when String.length t > 7 && String.sub t 0 7 = "(slice "
+               && not (String.contains t '\n')
+               && not (String.ends_with ~suffix:"\xe2\x80\xa6" t) -> Some t
+        | _ -> None
+      in
+      match written, f.Tast.snames.(s), kind, exact with
+      | Some t, _, `Slice, _ ->
+        fix_slice ("wrap the slice in clone, as in (clone " ^ t ^ ")")
+      | None, Some n, `Slice, true ->
+        fix_slice ("wrap the slice in clone, as in (clone (slice " ^ n ^ "))")
+      | _, _, `Slice, _ -> fix_slice "wrap the slice in (clone ...)"
+      | _, _, `Addr, _ ->
+        let pointee =
+          match e.Tast.ty with
+          | Types.Ptr (_, t) -> Types.to_string t
+          | t -> Types.to_string t
+        in
+        fix_addr pointee
+    in
+    let whose =
+      match f.Tast.snames.(s) with
+      | Some n -> Printf.sprintf "%s is a local of %s" n who
+      | None -> "That value lives in the frame of " ^ who
+    in
+    Loc.failk "check/frame-escape" e.Tast.loc
+      "%s %s %s%s. %s, and its storage is gone once %s returns, so every \
+       later read through it reads whatever the next call leaves there. %s"
+      (if String.equal who f.Tast.name then who
+       else String.capitalize_ascii who)
+      verb (what hit) target whose who fix
+  in
+  let rec tails (e : Tast.expr) =
+    match e.Tast.e with
+    | Tast.Do es | Tast.Let (_, es) | Tast.WithAlloc (_, es)
+    | Tast.Handled (_, es) ->
+      (match List.rev es with x :: _ -> tails x | [] -> ())
+    (* A restart clause is a branch of this function whose value is the
+       form's value when that restart is taken. *)
+    | Tast.RestartCase (cs, body) ->
+      List.iter
+        (fun (c : Tast.rclause) ->
+           match List.rev c.Tast.rbody with x :: _ -> tails x | [] -> ())
+        cs;
+      tails body
+    | Tast.If (_, a, b) -> tails a; tails b
+    | Tast.Match (_, arms) ->
+      List.iter
+        (fun (a : Tast.arm) ->
+           match List.rev a.Tast.abody with x :: _ -> tails x | [] -> ())
+        arms
+    | _ ->
+      Option.iter
+        (fail ~verb:"returns" ~target:""
+           ~fix_slice:(fun c ->
+               "Return a copy the caller owns: " ^ c
+               ^ ", which puts the elements in the context allocator")
+           ~fix_addr:(fun t ->
+               if String.equal who f.Tast.name then
+                 "Return the value instead: declare " ^ who
+                 ^ " to return " ^ t ^ " and drop the addr"
+               else
+                 "Return the value, of type " ^ t
+                 ^ ", instead of its address: drop the addr"))
+        (escapes 0 e)
+  in
+  let returns = not (Types.equal f.Tast.ret Types.Unit) in
+  List.iter
+    (Tast.walk (fun (e : Tast.expr) ->
+         match e.Tast.e with
+         | Tast.Return (Some v) when returns -> tails v
+         | Tast.Set (p, v) when not (String.equal f.Tast.name "main") ->
+           (match place_global p with
+            | Some g ->
+              Option.iter
+                (fail ~verb:"stores" ~target:(" into the global " ^ g)
+                   ~fix_slice:(fun c ->
+                       "Store a copy that outlives the frame: " ^ c
+                       ^ ", which puts the elements in the context allocator")
+                   ~fix_addr:(fun t ->
+                       "Store the value instead: declare " ^ g ^ " as " ^ t
+                       ^ " and drop the addr"))
+                (escapes 0 v)
+            | _ -> ())
+         | _ -> ()))
+    f.Tast.body;
+  if returns then
+    match List.rev f.Tast.body with x :: _ -> tails x | [] -> ()
+
 let box loc (e : Tast.expr) : Tast.expr =
   let dyn sym args = rt loc Types.Dyn sym args in
   match e.Tast.ty with
@@ -5450,13 +5684,15 @@ and check_fn ctx ~want ?gen loc (params : string list) body =
      one must not — it is reached by calls that pass none, and a parameter
      nobody supplies is read off whatever the register held. *)
   let fenv = if bare then fenv else declare_env fctx fenv in
-  ctx.env.lifted <-
+  let lifted =
     { Tast.name = fname; params = pts;
       slots = Array.of_list (List.rev fctx.slot_tys);
       snames = Array.of_list (List.rev fctx.slot_names);
       ret; body = prefix fbody; fdefers = [];
       fenv; fparent = Some ctx.owner; floc = loc }
-    :: ctx.env.lifted;
+  in
+  refuse_frame_escapes lifted;
+  ctx.env.lifted <- lifted :: ctx.env.lifted;
   let fty = if bare then Types.CFn (pts, ret) else Types.Fn (pts, ret) in
   (* [Flanfn] and not [Fnval], which is the handler clause's choice and is the
      same choice for the same reason. [Fnval] exists so that a *name* taken as
@@ -5571,13 +5807,15 @@ and check_handler_bind ctx ?want ?(what = "handler-bind") loc clauses body =
             [flan_signal] reads it off the frame and passes it to whichever
             clause matched, and it cannot know which of them captured. *)
          let fenv = declare_env hctx fenv in
-         ctx.env.lifted <-
+         let lifted =
            { Tast.name = fname; params = [ Types.Ptr (Types.Mut, ty) ];
              slots = Array.of_list (List.rev hctx.slot_tys);
              snames = Array.of_list (List.rev hctx.slot_names);
              ret = Types.Unit; body = prefix hbody; fdefers = [];
              fenv; fparent = Some ctx.owner; floc = c.Ast.hloc }
-           :: ctx.env.lifted;
+         in
+         refuse_frame_escapes lifted;
+         ctx.env.lifted <- lifted :: ctx.env.lifted;
          { Tast.htype = type_id name; hfn = fname; henv = addr }, bind)
       clauses
   in
@@ -13415,187 +13653,6 @@ let escaping_names ~returns (body : Ast.expr list) : string list =
   if returns then (match List.rev body with x :: _ -> tails x | [] -> ());
   !names
 
-(* A value handed out of [f] that points into [f]'s own frame: returned (the
-   last form's tails, or a [return]), or stored into a global or a field or
-   array element of one. Both read a dead frame the moment [f] returns, so
-   both are refused.
-
-   Deliberately narrow — the exact spellings that can only be wrong, so
-   nothing that could be valid is ever refused:
-   - [(addr p)] where [p] is a local, a field of one, or an element of a
-     local *array* (an array's elements are the frame's bytes; a Vec's or a
-     slice's are not);
-   - [(slice a …)] where [a] is such a place of array type;
-   - a local bound by [let] to one of those and never assigned or addressed
-     afterwards, which is also how a [return] under a [defer] arrives here.
-   A parameter is a local: its value is copied into the frame (an array
-   parameter too), so its address dies with the frame as well. Anything
-   reached through a [Ptr] is not the frame's, and a struct literal holding
-   such an address is not looked into.
-
-   The store is let through in two cases where it can be right. In [main],
-   whose frame outlives everything the program runs. And where the function
-   sets that same global again elsewhere — the stash-then-restore shape, the
-   global pointed at the frame only while the frame was live. *)
-let refuse_frame_escapes (f : Tast.fn) =
-  (* Keyed by slot alone: [fresh_slot] never reuses one, so a slot has at
-     most one binding [Let] in the function. *)
-  let binds = Hashtbl.create 16 in
-  let unstable = Hashtbl.create 16 in
-  let global_sets = Hashtbl.create 8 in
-  let rec place_global = function
-    | Tast.Pglobal g -> Some g
-    | Tast.Pfield (t, _) -> expr_global t
-    | Tast.Pindex (t, idx) when all_array t.Tast.ty idx -> expr_global t
-    | _ -> None
-  and expr_global (e : Tast.expr) =
-    match e.Tast.e with
-    | Tast.Global g -> Some g
-    | Tast.Field (t, _) -> expr_global t
-    | Tast.Prim (Tast.At, t :: idx) when all_array t.Tast.ty idx -> expr_global t
-    | _ -> None
-  (* [(at a i j)] is one node carrying every index; each level stepped must
-     be an array for the element to be inside [a]'s own bytes. *)
-  and all_array ty = function
-    | [] -> true
-    | _ :: rest ->
-      (match ty with Types.Array (_, el) -> all_array el rest | _ -> false)
-  in
-  List.iter
-    (Tast.walk (fun (e : Tast.expr) ->
-         match e.Tast.e with
-         | Tast.Let (bs, _) -> List.iter (fun (s, v) -> Hashtbl.replace binds s v) bs
-         | Tast.Set (Tast.Plocal s, _) | Tast.Addr (Tast.Plocal s) ->
-           Hashtbl.replace unstable s ()
-         | Tast.Set (p, _) ->
-           Option.iter
-             (fun g ->
-                Hashtbl.replace global_sets g
-                  (1 + Option.value ~default:0 (Hashtbl.find_opt global_sets g)))
-             (place_global p)
-         | _ -> ()))
-    f.Tast.body;
-  (* The local at the root of a place inside this frame, if it is one. *)
-  let rec root_expr (e : Tast.expr) =
-    match e.Tast.e with
-    | Tast.Local s -> Some s
-    | Tast.Field (t, _) -> root_expr t
-    | Tast.Prim (Tast.At, t :: idx) when all_array t.Tast.ty idx -> root_expr t
-    | _ -> None
-  in
-  let root_place = function
-    | Tast.Plocal s -> Some s
-    | Tast.Pfield (t, _) -> root_expr t
-    | Tast.Pindex (t, idx) when all_array t.Tast.ty idx -> root_expr t
-    | _ -> None
-  in
-  (* What escapes: the root local, whether it is a slice (else an address),
-     and whether the place is the bare local rather than a path into it —
-     only then can the fix be spelled with its name alone. *)
-  let rec escapes depth (e : Tast.expr) =
-    match e.Tast.e with
-    | Tast.Addr p ->
-      Option.map
-        (fun s ->
-           (e, (s, `Addr, (match p with Tast.Plocal _ -> true | _ -> false))))
-        (root_place p)
-    | Tast.Prim (Tast.Slice, [ t; _; _ ]) ->
-      (match t.Tast.ty with
-       | Types.Array _ ->
-         Option.map
-           (fun s ->
-              ( e,
-                (s, `Slice,
-                 (match t.Tast.e with Tast.Local _ -> true | _ -> false)) ))
-           (root_expr t)
-       | _ -> None)
-    | Tast.Local s when depth < 32 && not (Hashtbl.mem unstable s) ->
-      Option.bind (Hashtbl.find_opt binds s) (escapes (depth + 1))
-    | _ -> None
-  in
-  (* A slot with no name is a value the function made for itself, such as
-     the array a literal like [(slice [7 8 9])] is stored in. *)
-  let what (s, kind, exact) =
-    match f.Tast.snames.(s), kind, exact with
-    | Some n, `Slice, true -> "a slice of " ^ n
-    | Some n, `Slice, false -> "a slice of an array inside " ^ n
-    | Some n, `Addr, true -> "the address of " ^ n
-    | Some n, `Addr, false -> "an address inside " ^ n
-    | None, `Slice, _ -> "a slice of a temporary array"
-    | None, `Addr, _ -> "the address of a temporary"
-  in
-  (* Reported at the addr or slice itself: a [return] under a [defer], or a
-     local bound to one, reaches here as a read of a slot, and the caret
-     belongs on the form that took the address. *)
-  let fail ~verb ~target ~fix_slice ~fix_addr
-      ((e : Tast.expr), ((s, kind, exact) as hit)) =
-    let fix =
-      match f.Tast.snames.(s), kind, exact with
-      | Some n, `Slice, true ->
-        fix_slice ("wrap the slice in clone, as in (clone (slice " ^ n ^ "))")
-      | _, `Slice, _ -> fix_slice "wrap the slice in (clone ...)"
-      | _, `Addr, _ ->
-        let pointee =
-          match e.Tast.ty with
-          | Types.Ptr (_, t) -> Types.to_string t
-          | t -> Types.to_string t
-        in
-        fix_addr pointee
-    in
-    let whose =
-      match f.Tast.snames.(s) with
-      | Some n -> Printf.sprintf "%s is a local of %s" n f.Tast.name
-      | None -> "That value lives in " ^ f.Tast.name ^ "'s frame"
-    in
-    Loc.failk "check/frame-escape" e.Tast.loc
-      "%s %s %s%s. %s, and its storage is gone once %s returns, so every \
-       later read through it reads whatever the next call leaves there. %s"
-      f.Tast.name verb (what hit) target whose f.Tast.name fix
-  in
-  let rec tails (e : Tast.expr) =
-    match e.Tast.e with
-    | Tast.Do es | Tast.Let (_, es) | Tast.WithAlloc (_, es) ->
-      (match List.rev es with x :: _ -> tails x | [] -> ())
-    | Tast.If (_, a, b) -> tails a; tails b
-    | Tast.Match (_, arms) ->
-      List.iter
-        (fun (a : Tast.arm) ->
-           match List.rev a.Tast.abody with x :: _ -> tails x | [] -> ())
-        arms
-    | _ ->
-      Option.iter
-        (fail ~verb:"returns" ~target:""
-           ~fix_slice:(fun c ->
-               "Return a copy the caller owns: " ^ c
-               ^ ", which puts the elements in the context allocator")
-           ~fix_addr:(fun t ->
-               "Return the value instead: declare " ^ f.Tast.name
-               ^ " to return " ^ t ^ " and drop the addr"))
-        (escapes 0 e)
-  in
-  let returns = not (Types.equal f.Tast.ret Types.Unit) in
-  List.iter
-    (Tast.walk (fun (e : Tast.expr) ->
-         match e.Tast.e with
-         | Tast.Return (Some v) when returns -> tails v
-         | Tast.Set (p, v) when not (String.equal f.Tast.name "main") ->
-           (match place_global p with
-            | Some g when Hashtbl.find_opt global_sets g = Some 1 ->
-              Option.iter
-                (fail ~verb:"stores" ~target:(" into the global " ^ g)
-                   ~fix_slice:(fun c ->
-                       "Store a copy that outlives the frame: " ^ c
-                       ^ ", which puts the elements in the context allocator")
-                   ~fix_addr:(fun t ->
-                       "Store the value instead: declare " ^ g ^ " as " ^ t
-                       ^ " and drop the addr"))
-                (escapes 0 v)
-            | _ -> ())
-         | _ -> ()))
-    f.Tast.body;
-  if returns then
-    match List.rev f.Tast.body with x :: _ -> tails x | [] -> ()
-
 let rec check_fn env (fn : Ast.fn) : Tast.fn =
   let params, ret = Hashtbl.find env.fns fn.Ast.name in
   let ctx = { (invented_ctx env ret) with owner = fn.Ast.name } in
diff --git a/test/test_flan.ml b/test/test_flan.ml
index cf4aa30b..c1cae02e 100644
--- a/test/test_flan.ml
+++ b/test/test_flan.ml
@@ -3375,7 +3375,7 @@ let () =
     ~needle:"mk returns a slice of a";
   rejects_check "returning a local bound to a slice of a local array"
     "(defn mk [] [i32] (let [a [1 2 3 4] s (slice a 1 3)] s))"
-    ~needle:"(clone (slice a))";
+    ~needle:"(clone (slice a 1 3))";
   rejects_check "returning a slice of an array parameter"
     "(defn mk [a [4 i32]] [i32] (slice a))"
     ~needle:"mk returns a slice of a";
@@ -3403,9 +3403,33 @@ let () =
   accepts "a local reassigned before it is returned"
     "(defonce k [3 i32]) \
      (defn mk [] [i32] (let [a [1 2 3] s (slice a)] (set s (slice k)) s))";
-  accepts "a global stashed and restored"
-    "(defonce g [i32]) (defonce k [3 i32]) \
-     (defn f [] () (let [a [1 2 3]] (set g (slice a)) (set g (slice k))))";
+  rejects_check "two slices of locals stored into one global"
+    "(defonce g [i32]) \
+     (defn f [] () (let [a [1 2 3] b [4 5]] (set g (slice a)) (set g (slice b))))"
+    ~needle:"f stores a slice of a into the global g";
+  rejects_check "the fix keeps the slice's bounds"
+    "(defn mk [a [4 i32]] [i32] (slice a 1 3))"
+    ~needle:"(clone (slice a 1 3))";
+  rejects_check "an fn returning the address of its own local"
+    "(defn call [f (Fn [] (Ptr i32))] (Ptr i32) (f)) \
+     (defn g [] (Ptr i32) (call (fn [] (let [x (i32 4)] (addr x)))))"
+    ~needle:"This fn returns the address of x";
+  rejects_check "an fn returning a slice of its copy of a captured array"
+    "(defn call [f (Fn [] [i32])] [i32] (f)) \
+     (defn g [] i32 (let [a [1 2 3]] (at (call (fn [] (slice a))) 0)))"
+    ~needle:"This fn returns a slice of a";
+  rejects_check "a handler storing a slice of its local into a global"
+    "(defstruct Oops [code i32]) (defonce g [i32]) \
+     (defn main [] i32 \
+       (handler-bind [(Oops [c] (let [a [1 2 3]] (set g (slice a))))] \
+         (signal (Oops {.code 1}))) 0)"
+    ~needle:"This handler stores a slice of a into the global g";
+  rejects_check "a restart clause answering the address of a local"
+    "(defstruct Oops [code i32]) \
+     (defn mk [p (Ptr i32)] (Ptr i32) (let [x (i32 4)] \
+       (restart-case (do (signal (Oops {.code 1})) p) \
+         (use-it [] (addr x)))))"
+    ~needle:"mk returns the address of x";
   accepts "main stores its own local into a global"
     "(defonce g (Ptr i32)) (defn main [] i32 (let [x (i32 5)] (set g (addr x))) 0)";
   accepts "a unit function's last form is not returned"

From ab5fe36a485f82c826a025142a709e625d758345 Mon Sep 17 00:00:00 2001
From: Joseph Ferano <joseph@ferano.io>
Date: Fri, 25 Sep 2026 21:18:48 +0700
Subject: [PATCH 3/3] A frame address stored into a global's field, array or
 Vec element, or pushed or put into a global container is refused with a fix
 that names no wrong type, and the sanitizer sweep builds at -O0 so a read of
 a returned frame reports

---
 lib/check.ml          | 66 ++++++++++++++++++++++++++++++++++---------
 test/test_flan.ml     | 23 +++++++++++++++
 test/test_sanitize.ml | 25 ++++++++++------
 3 files changed, 92 insertions(+), 22 deletions(-)

diff --git a/lib/check.ml b/lib/check.ml
index c51d5690..01f3e36c 100644
--- a/lib/check.ml
+++ b/lib/check.ml
@@ -3585,17 +3585,33 @@ let refuse_frame_escapes (f : Tast.fn) =
      most one binding [Let] in the function. *)
   let binds = Hashtbl.create 16 in
   let unstable = Hashtbl.create 16 in
+  (* A place a global owns, and so one that outlives every frame: the global,
+     a field or array element of it, or an element of a Vec it holds — the
+     Vec's block is the global's for as long as the global keeps it. A slice
+     is not stepped through: its storage may be anyone's. *)
   let rec place_global = function
     | Tast.Pglobal g -> Some g
     | Tast.Pfield (t, _) -> expr_global t
-    | Tast.Pindex (t, idx) when all_array t.Tast.ty idx -> expr_global t
+    | Tast.Pindex (t, idx) when owned_levels t.Tast.ty idx -> expr_global t
+    (* [(set (at v i) x)] on a Vec is a store through the checked element
+       address [vec_at] builds. Any other pointer's target is not known to
+       be the global's. *)
+    | Tast.Pderef { Tast.e = Tast.Prim (Tast.Rt "flan_vec_at", t :: _); _ } ->
+      expr_global t
     | _ -> None
   and expr_global (e : Tast.expr) =
     match e.Tast.e with
     | Tast.Global g -> Some g
     | Tast.Field (t, _) -> expr_global t
-    | Tast.Prim (Tast.At, t :: idx) when all_array t.Tast.ty idx -> expr_global t
+    | Tast.Prim (Tast.At, t :: idx) when owned_levels t.Tast.ty idx ->
+      expr_global t
     | _ -> None
+  and owned_levels ty = function
+    | [] -> true
+    | _ :: rest ->
+      (match ty with
+       | Types.Array (_, el) | Types.Vec el -> owned_levels el rest
+       | _ -> false)
   (* [(at a i j)] is one node carrying every index; each level stepped must
      be an array for the element to be inside [a]'s own bytes. *)
   and all_array ty = function
@@ -3765,24 +3781,46 @@ let refuse_frame_escapes (f : Tast.fn) =
                  ^ ", instead of its address: drop the addr"))
         (escapes 0 e)
   in
+  (* Only a store into the global itself can be fixed by changing the
+     global's type; for a field, an element or a push, the value's type
+     belongs to something else. *)
+  let stored ~bare g v =
+    Option.iter
+      (fail ~verb:"stores" ~target:(" into the global " ^ g)
+         ~fix_slice:(fun c ->
+             "Store a copy that outlives the frame: " ^ c
+             ^ ", which puts the elements in the context allocator")
+         ~fix_addr:(fun t ->
+             if bare then
+               "Store the value instead: declare " ^ g ^ " as " ^ t
+               ^ " and drop the addr"
+             else "Store the value instead of its address"))
+      (escapes 0 v)
+  in
   let returns = not (Types.equal f.Tast.ret Types.Unit) in
   List.iter
     (Tast.walk (fun (e : Tast.expr) ->
          match e.Tast.e with
          | Tast.Return (Some v) when returns -> tails v
          | Tast.Set (p, v) when not (String.equal f.Tast.name "main") ->
-           (match place_global p with
-            | Some g ->
-              Option.iter
-                (fail ~verb:"stores" ~target:(" into the global " ^ g)
-                   ~fix_slice:(fun c ->
-                       "Store a copy that outlives the frame: " ^ c
-                       ^ ", which puts the elements in the context allocator")
-                   ~fix_addr:(fun t ->
-                       "Store the value instead: declare " ^ g ^ " as " ^ t
-                       ^ " and drop the addr"))
-                (escapes 0 v)
-            | _ -> ())
+           Option.iter
+             (fun g ->
+                stored ~bare:(match p with Tast.Pglobal _ -> true | _ -> false)
+                  g v)
+             (place_global p)
+         (* A push or put into a container a global owns: the element was
+            bound to a slot first, and its address is what the call takes. *)
+         | Tast.Prim (Tast.Rt ("flan_vec_push" | "flan_map_put"), target :: rest)
+           when not (String.equal f.Tast.name "main") ->
+           Option.iter
+             (fun g ->
+                List.iter
+                  (fun (a : Tast.expr) ->
+                     match a.Tast.e with
+                     | Tast.Prim (Tast.AddrOf, [ v ]) -> stored ~bare:false g v
+                     | _ -> ())
+                  rest)
+             (expr_global target)
          | _ -> ()))
     f.Tast.body;
   if returns then
diff --git a/test/test_flan.ml b/test/test_flan.ml
index 4135988e..5b63acd7 100644
--- a/test/test_flan.ml
+++ b/test/test_flan.ml
@@ -3405,6 +3405,29 @@ let () =
     "(defonce g [i32]) \
      (defn f [] () (let [a [1 2 3] b [4 5]] (set g (slice a)) (set g (slice b))))"
     ~needle:"f stores a slice of a into the global g";
+  rejects_check "a local's address into a global array's element"
+    "(defonce gs [2 (Ptr i32)]) \
+     (defn f [] () (let [x (i32 1)] (set (at gs 0) (addr x))))"
+    ~needle:"Store the value instead of its address";
+  rejects_check "a local's address into a global struct's field"
+    "(defstruct Q [p (Ptr i32)]) (defonce gq Q) \
+     (defn f [] () (let [x (i32 1)] (set (.p gq) (addr x))))"
+    ~needle:"f stores the address of x into the global gq";
+  rejects_check "a local's address into a global Vec's element"
+    "(defonce gv (Vec (Ptr i32))) \
+     (defn f [] () (let [x (i32 1)] (set (at gv 0) (addr x))))"
+    ~needle:"f stores the address of x into the global gv";
+  rejects_check "a local's address pushed onto a global Vec"
+    "(defonce gv (Vec (Ptr i32))) \
+     (defn f [] () (let [x (i32 1)] (push gv (addr x))))"
+    ~needle:"f stores the address of x into the global gv";
+  rejects_check "a local's address put into a global Map"
+    "(defonce gm (Map i32 (Ptr i32))) \
+     (defn f [] () (let [x (i32 1)] (put gm 1 (addr x))))"
+    ~needle:"f stores the address of x into the global gm";
+  accepts "a pointer parameter pushed onto a global Vec"
+    "(defonce gv (Vec (Ptr i32))) \
+     (defn f [p (Ptr i32)] () (push gv p))";
   rejects_check "the fix keeps the slice's bounds"
     "(defn mk [a [4 i32]] [i32] (slice a 1 3))"
     ~needle:"(clone (slice a 1 3))";
diff --git a/test/test_sanitize.ml b/test/test_sanitize.ml
index 529864d9..5e5b61bf 100644
--- a/test/test_sanitize.ml
+++ b/test/test_sanitize.ml
@@ -64,7 +64,7 @@ let run exe args =
   (try Sys.remove out with Sys_error _ -> ());
   (code, text)
 
-let compile ?(dev = false) ~sanitize ~checks path =
+let compile ?(dev = false) ?(opt = "-O0") ~sanitize ~checks path =
   let exe =
     Filename.concat scratch
       (Printf.sprintf "flan-san-%s%s-%s"
@@ -73,10 +73,15 @@ let compile ?(dev = false) ~sanitize ~checks path =
          (Filename.remove_extension (Filename.basename path)))
   in
   let p, csrcs, lflags = Test_support.linked ~dev path in
+  (* -O0 by default, both builds: detect_stack_use_after_return (see [env]) can only
+     report a read of a frame's variable that still has a stack slot. At -O2
+     the local is promoted to a register and the read folded to the value it
+     held, so a pointer into a returned frame reads nothing the fake stack
+     can poison. *)
   ignore
     (Build.executable
-       ~opts:{ Build.default with checks; sanitize; dev } ~csrcs ~lflags p
-       ~out:exe);
+       ~opts:{ Build.default with checks; sanitize; dev; opt }
+       ~csrcs ~lflags p ~out:exe);
   exe
 
 let contains = Test_support.contains
@@ -107,6 +112,9 @@ let reported text = List.exists (contains text) markers
    calc-me is here and is not in test/programs: it is the one string parser in
    the corpus, which makes it the likeliest to push [scratch] or [escaped]
    anywhere near their bounds. *)
+(* temp-grow and condition-temp read text after a (free-temp) on purpose, to
+   show the dev poison, and a sanitized build reports exactly that read: they
+   stay out of this list. *)
 let corpus =
   [ (* bounds.flan selects its case from argv, and every case but 0 is one
        that traps. Argument 0 is the in-bounds path — the last index of a
@@ -327,7 +335,7 @@ let dyn_sweep () =
   let p, csrcs, lflags = Test_support.linked path in
   match
     Build.executable
-      ~opts:{ Build.default with Build.sanitize = true }
+      ~opts:{ Build.default with Build.sanitize = true; opt = "-O0" }
       ~csrcs:(csrcs @ [ "dyn_ops.c" ]) ~lflags p ~out:exe
   with
   | exception Failure m -> fail "dyn: sanitized build: %s" m
@@ -439,8 +447,8 @@ let dev_sweep () =
    sanitized run must produce ASan's report and must NOT produce the
    handler's line, and that is the assertion.
 
-   And it has to be built at -O0. At the sweep's -O2 a store through a null
-   pointer is undefined and need not fault — so a case that is about what happens
+   And it has to be built at -O0, as the sweep now is. At -O2 a store through
+   a null pointer is undefined and need not fault — so a case that is about what happens
    on a fault has to be compiled where the fault happens. Same family as the
    -O0/-O2 split [unchecked_controls] records for bounds.flan.
 
@@ -592,7 +600,8 @@ let control ~expect_report ?(args = []) ~why name src =
    wrong answer instead of touching a redzone. At -O0, with the load still in
    the program, ASan reports it. That divergence is why [--sanitize] does not
    force -O0 the way [--debug] does — the optimiser is half of what is being
-   measured. *)
+   measured — and why this one control is built at -O2 while the sweep is
+   not. *)
 let unchecked_controls () =
   let reports = [ "3"; "7"; "4" ] in
   let silent =
@@ -616,7 +625,7 @@ let unchecked_controls () =
              here and now for a better reason. The trap itself is asserted in \
              test_acceptance.ml" ]
   in
-  match compile ~sanitize:true ~checks:false "programs/bounds.flan" with
+  match compile ~opt:"-O2" ~sanitize:true ~checks:false "programs/bounds.flan" with
   | exception Failure m -> fail "unchecked bounds.flan: build: %s" m
   | exe ->
     List.iter