From 01e60fa5b780db04d81b8cfdb647bee902e0d1b6 Mon Sep 17 00:00:00 2001 From: Joseph Ferano Date: Sat, 19 Sep 2026 14:30:46 +0700 Subject: [PATCH] A struct cannot hold a dyn field the collector would never find MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit The condition payload was already refused on exactly this ground; the plain struct got the same shape past the checker. The audit's probe showed the emitted program rooting the temporary, popping it at ret, and leaving the field's vec reachable only through arena memory the marker never walks — a use-after-free on a timer. Lifted with milestone 2's per-type descriptors, alongside the condition's. --- lib/check.ml | 17 +++++++++++++++++ test/test_flan.ml | 8 ++++++++ 2 files changed, 25 insertions(+) diff --git a/lib/check.ml b/lib/check.ml index 61ce1f5..3ec1de0 100644 --- a/lib/check.ml +++ b/lib/check.ml @@ -6106,6 +6106,23 @@ let collect env (decls : Ast.decl list) = means reading [Value]'s own cases back out of the table. A [fail] aborts the whole compilation, so an entry left behind by a declaration that is about to be refused is never read. *) + (* A dyn field is refused for the reason a condition's already is + (see the [signal] arm): the collector's roots are the frames, and + a struct outlives the frame that built it — its dyn field would be + a live value reachable only through memory the marker never walks, + which is a use-after-free on a timer. The audit that found the + hole is docs/SPIKE-DUPLICITY.md, question 1; the per-type + descriptor that lifts this is milestone 2's, alongside the + condition payload's. *) + List.iter + (fun (f : Tast.field) -> + if f.Tast.fty = Types.Dyn then + no_dyn_yet loc ~into:false Types.Dyn + (Printf.sprintf + " — the field %s of %s is one, and a struct outlives the \ + frame that roots its values, which is milestone 2" + f.Tast.fname n)) + fields; Hashtbl.replace env.structs n { Tast.sname = n; fields }; (* A struct field may own storage. Since the repeal a struct holding a [(Vec i32)] is an ordinary value: assignment copies the diff --git a/test/test_flan.ml b/test/test_flan.ml index cd0041d..74fa8b3 100644 --- a/test/test_flan.ml +++ b/test/test_flan.ml @@ -890,6 +890,14 @@ let () = "(defstruct Boom [what dyn])\n\ (defn main [] () (signal (Boom {.what 1})))" ~needle:"milestone 2"; + (* A plain struct too, not only a condition's: the struct outlives the + frame that roots its values, so a dyn field is reachable only through + memory the marker never walks. Found as SPIKE-DUPLICITY.md's question 1 + — the emitted program rooted the temporary, popped it at ret, and left + the field's vec live and untraced. *) + rejects_check "a dyn field in a struct" + "(defstruct S [x dyn])\n(defn main [] i32 0)" + ~needle:"a struct outlives the frame"; (* And the C boundary, which is the one that would otherwise pass silently: a dyn is one word and would cross as an integer, and nothing on the other side can ask what the word means. *)