diff --git a/FIX.org b/FIX.org index d6b3978..dd09153 100644 --- a/FIX.org +++ b/FIX.org @@ -443,10 +443,13 @@ rename. typed-flan branch freezes the static language pre-dyn. refused every container outright. Three routes, all newly constructible, all stack-use-after-return: returning a view, stashing one in a dyn global, leaving one behind across a condition transfer. AUTHOR'S RULE: - on the dynamic side Flan follows Clojure and Common Lisp, where holding a - value never hands you garbage, so a container may cross into dyn as a - view only when its own storage is permanent — a global's. [permanent_root] - in check.ml decides it: a global, a field or an array element of one, or + on the dynamic side Flan aims where Clojure and Common Lisp are — holding + a value should not hand you garbage — so a container may cross into dyn as + a view only when its own storage is permanent — a global's. + [permanent_root] in check.ml decides it: a global, a field of one, an + element of a permanent ARRAY (an element of a slice is NOT — a slice holds + only ptr+len, and what they point at can be a frame already gone; the [At] + arm checks the target's type for exactly this), or a slice cut directly from one at the call (the trace is lost the moment it is bound to a name first). Everything else — a local, a parameter, a temporary, anything behind a (Ptr T) — is refused by name, pointing at @@ -454,10 +457,33 @@ rename. typed-flan branch freezes the static language pre-dyn. soundly at this milestone for a structural reason rather than a missing feature: a (Ptr (Vec i64)) taken off a heap block and one taken off a local are the same type, so admitting a Ptr as permanent would readmit - the exact hole this closes. An arena-held header is not a separate case - at all — an arena changes where a Vec's elements live, never where its - own header (the binding) lives, so it is already covered by the cases - above. + the exact hole this closes. + + The rule is a narrowing, not a proof, and flan_dyn.h states the property + that actually holds: a view is exactly as stale-safe as the thing it is a + view of, no more and no less. A global [i64] whose data was cut from a + frame that has since returned still passes [permanent_root] and still + reads a dead frame. What the guard closes is the routes the checker can + see, not every route. + + An arena-held header is not a separate case for [permanent_root] — an + arena changes where a Vec's elements live, never where its own header + (the binding) lives, so the cases above already decide it — but that is + coverage of the HEADER's lifetime only, and releasing the arena under a + live view is a separate hazard handled at RUN time, not here. + [view_vec_check] in flan_dyn.c is what handles it: a Vec records its + allocator's epoch and every view operation re-checks it, so (free-all ar) + with a live view over an arena-grown global Vec traps cleanly and by name + at the next read — verified. (arena-destroy ar) is the gap: it frees the + allocator block itself, so the epoch [view_vec_check] goes to read is + freed memory. Run plainly it happens to trap anyway — the freed block + still held the bumped epoch — but that is the allocator not having reused + it yet, not a check that held; under ASan the same program is a + heap-use-after-free in [view_vec_check] before it decides anything. Left + standing rather than fixed with this lane: the typed side has it + identically in [flan_vec_check], flan_rt.c, which reads the same freed + allocator's epoch, so it is a repo-level question about arena-destroy's + ordering and not about views. Three more, all in the runtime rather than the boundary: [view_vec_check] recursed into itself rendering the very view it had just declared unsafe diff --git a/lib/check.ml b/lib/check.ml index fb4e056..0786a21 100644 --- a/lib/check.ml +++ b/lib/check.ml @@ -1468,12 +1468,13 @@ let view_not_yet loc (container : Types.t) (elem : Types.t) = no_dyn_yet loc ~into:true container (Printf.sprintf ". A container view at this milestone holds i64, f64 or bool \ - elements only — %s is neither a width this milestone's view carries \ - nor the case the restriction exists for, which is a string element: \ - a dyn string's form is a pointer into the collector's heap, and a \ - typed container's storage is memory the collector never scans, so \ - a write through a view over strings could plant a pointer where \ - nothing will ever trace it" + elements only, and %s is not one of the three. The restriction \ + exists for the string case: a dyn string's form is a pointer into \ + the collector's heap, and a typed container's storage is memory the \ + collector never scans, so a write through a view over strings could \ + plant a pointer where nothing will ever trace it. Every other \ + element type is refused with it rather than admitted one width at a \ + time" (Types.to_string elem)) (* M2 item 3's second guard, added on review: a view's descriptor holds an @@ -1487,19 +1488,32 @@ let view_not_yet loc (container : Types.t) (elem : Types.t) = — reachable now for the first time, not a pre-existing hole this lane merely inherited. - On the dynamic side Flan follows Clojure and Common Lisp: holding a value - can never hand you garbage. Treating a view as a bare pointer and calling - the lifetime the programmer's problem is the Odin answer, and neither - Odin nor C stops it — but a dyn value that can dangle is the wrong trade - on this side of the language, so this is refused rather than merely - documented. + On the dynamic side Flan aims where Clojure and Common Lisp are: holding + a value should not hand you garbage. Treating a view as a bare pointer and + calling the lifetime the programmer's problem is the Odin answer, and + neither Odin nor C stops it — this guard is the trade going the other way, + refused rather than merely documented. + + What it is NOT is a proof. runtime/flan_dyn.h states the actual property: + the view is exactly as stale-safe as the thing it is a view of, no more + and no less. This guard narrows what a view can be taken of; it does not + make the underlying storage outlive anything. A global [[T]] slice whose + data was cut from a frame that has since returned still passes here, and + reading through the view then reads a dead frame. So this is a guard that + closes the routes the checker can see, not a guarantee that a dyn value + never dangles. [permanent_root] asks whether an expression's own address — the one a view's pointer will chase — is guaranteed to outlive every frame, which is true of exactly one thing at this milestone: a global. A field of a - permanent value is permanent at the same fixed offset from it, and an - array element of one likewise; both are still inside the global's own - storage. A slice built directly from [(slice T lo hi)] inherits the + permanent value is permanent at the same fixed offset from it, and so is + an element of a permanent *array* — both are still inside the permanent + value's own storage. An element of a permanent *slice* is not, and the + [At] arm below checks the target's type for exactly that reason: a slice + is ptr+len, so a global [[T]] holds only the two words, and the storage + they point at can be a frame that has already gone. That distinction is + the whole of the arm's guard. A slice built directly from + [(slice T lo hi)] inherits the permanence of the [T] it was cut from — unwrapped here because that is the one shape still carrying the trace back to it; once a slice has been bound to a name the trace is gone and it is refused; the spelling that @@ -1523,20 +1537,25 @@ let rec permanent_root (e : Tast.expr) : bool = match e.Tast.e with | Tast.Global _ -> true | Tast.Field (target, _) -> permanent_root target - | Tast.Prim (Tast.At, target :: _) -> permanent_root target + | Tast.Prim (Tast.At, target :: _) -> + (match target.Tast.ty with + | Types.Array _ -> permanent_root target + | _ -> false) | Tast.Prim (Tast.Slice, [ target; _; _ ]) -> permanent_root target | _ -> false let view_not_permanent loc (container : Types.t) = Loc.failk "check/dyn-view-lifetime" loc "%s does not cross into dyn as a view here — its storage is not known \ - to outlive the view, and a dyn value that can dangle is not one this \ - language will hand back. A global's does: (defvar g %s ...) viewed \ - from anywhere is sound, because a global's address is fixed for the \ - process. A local, a parameter, a temporary, or anything reached \ - through a (Ptr T) is refused for the same reason — the checker cannot \ - tell a heap-durable pointer from a frame's own, and admitting one \ - admits the other" + to outlive the view, and a view is exactly as stale-safe as the thing \ + it is a view of, no more and no less. A global's storage does outlive \ + it: (defvar g %s ...) viewed from anywhere reads storage fixed for the \ + process, and so does a field or an array element of one. A local, a \ + parameter, a temporary, an element of a slice — even a global slice, \ + which holds only ptr+len and can point at a frame that is gone — or \ + anything reached through a (Ptr T) is refused: the checker cannot tell \ + a heap-durable pointer from a frame's own, and admitting one admits \ + the other" (Types.to_string container) (Types.to_string container) let box loc (e : Tast.expr) : Tast.expr = @@ -1573,26 +1592,32 @@ let box loc (e : Tast.expr) : Tast.expr = no snapshot for the growth to invalidate. A slice and a fixed array cannot grow, so a snapshot taken once at the crossing is sound for both, and they share [flan_dyn_view_flat]. *) + (* The element check runs before the lifetime one in all three arms, and + the order is load-bearing rather than incidental: the lifetime message + points at [(defvar g ...)] as the spelling that works, and for an + element type no view can carry — a string, an i32 — the global spelling + is refused too, so the wrong order hands the programmer advice that + fails when they take it. Whichever refusal is unconditional wins. *) | Types.Vec elem -> - if not (permanent_root e) then view_not_permanent loc e.Tast.ty - else - (match view_elem elem with - | Some k -> dyn "flan_dyn_view_vec" [ e; view_elem_lit loc k ] - | None -> view_not_yet loc e.Tast.ty elem) + (match view_elem elem with + | None -> view_not_yet loc e.Tast.ty elem + | Some k -> + if not (permanent_root e) then view_not_permanent loc e.Tast.ty + else dyn "flan_dyn_view_vec" [ e; view_elem_lit loc k ]) | Types.Slice elem -> - if not (permanent_root e) then view_not_permanent loc e.Tast.ty - else - (match view_elem elem with - | Some k -> dyn "flan_dyn_view_flat" [ e; view_elem_lit loc k ] - | None -> view_not_yet loc e.Tast.ty elem) + (match view_elem elem with + | None -> view_not_yet loc e.Tast.ty elem + | Some k -> + if not (permanent_root e) then view_not_permanent loc e.Tast.ty + else dyn "flan_dyn_view_flat" [ e; view_elem_lit loc k ]) | Types.Array (n, elem) -> - if not (permanent_root e) then view_not_permanent loc e.Tast.ty - else - (match view_elem elem with - | Some k -> + (match view_elem elem with + | None -> view_not_yet loc e.Tast.ty elem + | Some k -> + if not (permanent_root e) then view_not_permanent loc e.Tast.ty + else dyn "flan_dyn_view_flat" - [ e; mk loc dyn_i64 (Tast.Int (n, Types.I64)); view_elem_lit loc k ] - | None -> view_not_yet loc e.Tast.ty elem) + [ e; mk loc dyn_i64 (Tast.Int (n, Types.I64)); view_elem_lit loc k ]) | Types.Map _ -> no_dyn_yet loc ~into:true e.Tast.ty ". The dyn container at this milestone is the runtime's own, from \ diff --git a/runtime/flan_dyn.h b/runtime/flan_dyn.h index 2cd0a5e..c563b34 100644 --- a/runtime/flan_dyn.h +++ b/runtime/flan_dyn.h @@ -173,8 +173,12 @@ flan_dyn flan_dyn_need_not_nil(flan_dyn v); * [flan_dyn_view_vec] takes the address of the Vec's own header — the * struct [flan_vec] in flan_rt.c, restated in flan_dyn.c under the same * "if either table changes, change both" rule this whole boundary already - * lives under. That address is the Vec's home: a local's slot, a global, a - * field, fixed for as long as the Vec exists. Every operation re-reads that + * lives under. That address is the Vec's home, fixed for as long as the Vec + * exists — but "as long as the Vec exists" is the whole of the guarantee, + * which is why [permanent_root] in lib/check.ml admits only storage that + * outlives every frame: a global, a field or an array element of one, or a + * slice cut from one at the crossing. A local's slot is a home too, and it + * is precisely the one that is refused. Every operation re-reads that * header's [ptr] and [len] fresh, so a push that grows and moves the Vec is * never seen as stale — [flan_vec_grow] overwrites the SAME header's [ptr] * field in place, and there is no snapshot anywhere to go stale. That is diff --git a/runtime/flan_rt.c b/runtime/flan_rt.c index db240b1..0883940 100644 --- a/runtime/flan_rt.c +++ b/runtime/flan_rt.c @@ -1493,8 +1493,9 @@ typedef struct flan_vec { /* This struct's layout is restated twice more in the tree — flan_dyn.c's * [flan_dyn_vec_hdr], for a typed container's view (M2 item 3), and - * test/dyn_ops.c's [hand_vec], which builds one by hand with no [flan_rt.c] - * linked in to call [flan_vec_init] for it. None of the three can [#include] + * test/dyn_ops.c's [hand_vec], which builds one by hand because it has no + * [flan_vec] type to initialise, this file being linked into it but not + * included by it. None of the three can [#include] * this file (see [Build.compile_c]), so nothing at compile time ties them * together — a reordered field here links and runs, and corrupts whichever * of the other two disagrees. [flan_vec_layout] is the tie: it reports this diff --git a/test/dyn_ops.c b/test/dyn_ops.c index 6030516..c7f81f1 100644 --- a/test/dyn_ops.c +++ b/test/dyn_ops.c @@ -353,9 +353,12 @@ static void ops(void) { /* A typed container's own header, restated a third time — flan_rt.c's * [flan_vec], flan_dyn.c's [flan_dyn_vec_hdr], and this. The three must * agree on layout, and none of them can [#include] another's to say so at - * compile time (see [Build.compile_c]): there is no [flan_vec_init] to call - * from here, so the header below is built by hand, the same five words - * [flan_vec_grow] would leave behind after a few pushes. + * compile time (see [Build.compile_c]) — so the header below is built by + * hand, the same five words [flan_vec_grow] would leave behind after a few + * pushes. flan_rt.c IS linked into this binary (the [flan_vec_free] and + * [flan_vec_layout] calls below are its), but without its header there is + * no [flan_vec] type to declare an initialiser over; the restatement is + * what the [#include] restriction costs, not a missing link. * * What actually ties the three together is [layout], further down: it reads * flan_rt.c's [flan_vec_layout] and flan_dyn.c's [flan_dyn_vec_hdr_layout] diff --git a/test/programs/dyn-view.flan b/test/programs/dyn-view.flan index a76cc5b..e70af64 100644 --- a/test/programs/dyn-view.flan +++ b/test/programs/dyn-view.flan @@ -13,10 +13,13 @@ ;;;; slice or a fixed array whose storage is not known to outlive the view — ;;;; a local's, a parameter's, a temporary's — and a global's is the one ;;;; storage this milestone can prove permanent: fixed in .data for the -;;;; process. test_flan.ml's checker tests carry the refusal side of this -;;;; (a local Vec, a Vec parameter, a Vec behind a Ptr, a slice rebound to a -;;;; local); this program is the acceptance side, over storage the guard -;;;; allows. +;;;; process — as is a field of one, and an ELEMENT of one when the global +;;;; is an array, whose elements sit inside its own storage. An element of a +;;;; global SLICE is not: the slice is ptr+len and says nothing about where +;;;; the data is. test_flan.ml's checker tests carry the refusal side of +;;;; this (a local Vec, a Vec parameter, a Vec behind a Ptr, a slice rebound +;;;; to a local, an element of a global slice); this program is the +;;;; acceptance side, over storage the guard allows. ;;;; ;;;; Mode 0 is the survey: a read through the view boxes the element ;;;; correctly, a write through either side is seen through the other, and a @@ -40,6 +43,13 @@ (defvar a [4 i64]) (defvar a2 [3 f64]) (defvar bv (Vec bool) (vec-new bool)) +;; A global ARRAY of Vecs. An element of this is permanent — it sits inside +;; the global's own storage at a fixed offset — and a view over it is the +;; acceptance half of the [At] arm's guard. The refusal half is the same +;; program with [[(Vec i64)]] (a global SLICE) instead, which holds only +;; ptr+len and so says nothing about where the Vecs live; test_flan.ml +;; carries that pair, because a refusal cannot run. +(defvar rows [2 (Vec i64)]) (defn main [args [string]] i32 (let [n (i32 (bytes->i64 (bytes (at args 1))))] @@ -106,6 +116,21 @@ (set (at db 1) true) (print (at bv 1)) (print "\n")) + ;; An element of the global array: a (Vec i64) living inside the + ;; global's own storage, viewed from there. A push through the view + ;; grows that element's buffer and the typed side sees it, exactly + ;; as for the plain global Vec above — the element's header never + ;; moves, because the array it sits in never does. + (push (at rows 0) 111) + (push (at rows 0) 222) + (let [dr (as-dyn (at rows 0))] + (print dr) + (print "\n") + (push dr 333) + (print (len (at rows 0))) + (print "\n") + (print (at (at rows 0) 2)) + (print "\n")) 0) (= n 1) ;; Out of range. The runtime's own message names the length. diff --git a/test/test_acceptance.ml b/test/test_acceptance.ml index 9b30e50..b25b4f0 100644 --- a/test/test_acceptance.ml +++ b/test/test_acceptance.ml @@ -3702,9 +3702,10 @@ level "1" (* ── Typed containers into dyn as views, M2 item 3 ──────────────── programs/dyn-view.flan takes its mode from argv, the way bounds.flan does, because a survey and a trap cannot share a process: mode 0 is - the survey proper (a Vec view, a fixed-array view, a slice view and a - bool Vec's view, each written through one side and read through the - other, plus a push through the Vec view that grows and moves it), and + the survey proper (a Vec view, a fixed-array view, a slice view, a + bool Vec's view and a view over a Vec that is an ELEMENT of a global + array, each written through one side and read through the other, plus + a push through the Vec view that grows and moves it), and modes 1 and 2 are the two ways a view refuses — out of range, and a write whose dyn tag does not match the element type. The expected text for mode 0 was captured from the running program. *) @@ -3712,7 +3713,8 @@ level "1" "[ 10 20 30]\n999\n777\n4\n40\n\ [ 1 2 3 4]\n100\n400\n\ [ 1.5 2.5 3.5]\n9.5\n\ - [ true false]\ntrue\n" + [ true false]\ntrue\n\ + [ 111 222]\n3\n333\n" in let dyn_view ?opt ?x86 () = let exe = compile ?opt ?x86 "programs/dyn-view.flan" in diff --git a/test/test_flan.ml b/test/test_flan.ml index a453f82..968210e 100644 --- a/test/test_flan.ml +++ b/test/test_flan.ml @@ -923,6 +923,17 @@ let () = (defn take [d dyn] i32 1)\n\ (defn main [] i32 (take m))" ~needle:"does not cross into dyn yet"; + (* Which of the two refusals wins when both apply. A LOCAL (Vec string) + fails the lifetime guard and the element check both, and the element + one has to be the one that speaks: the lifetime message names + (defvar g ...) as the spelling that works, and for a string element + the global spelling is refused too, so the other order would hand back + advice that fails when taken. *) + rejects_check "a local Vec of strings gets the element refusal, not the \ + lifetime one" + "(defn take [d dyn] i32 1)\n\ + (defn main [] i32 (let [v (vec-new string)] (take v)))" + ~needle:"does not cross into dyn yet"; (* ── The lifetime guard, added on review ───────────────────────── A local, a parameter and a temporary all answer false to [permanent_root], and each gets the same message rather than "cannot be @@ -952,6 +963,23 @@ let () = (defn take [d dyn] i32 1)\n\ (defn main [] i32 (let [s (slice xs 0 3)] (take s)))" ~needle:"does not cross into dyn as a view here"; + (* An element of a global is permanent only when the global is an ARRAY. + An array's elements are inside the global's own storage; a slice's are + not — a global [[T]] holds ptr+len and nothing more, and what they + point at may be a frame that has already returned. The refusal row + below is one word different from the acceptance row above it, which is + the point: it is the [At] arm's guard on the target's type and nothing + else deciding. Before that guard the refusal row compiled and + segfaulted with no diagnostic at all. *) + accepts "an element of a global array is permanent" + "(defvar rows [2 (Vec i64)])\n\ + (defn take [d dyn] i32 1)\n\ + (defn main [] i32 (take (at rows 0)))"; + rejects_check "an element of a global slice is not permanent" + "(defvar sv [(Vec i64)])\n\ + (defn take [d dyn] i32 1)\n\ + (defn main [] i32 (take (at sv 0)))" + ~needle:"does not cross into dyn as a view here"; (* A Vec behind a Ptr is refused even though some Ptrs really are heap-durable — the checker cannot tell this one from a Ptr taken off a local, and admitting one admits the other. *)