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. *)