diff --git a/FIX.org b/FIX.org index 1e50077..3e83526 100644 --- a/FIX.org +++ b/FIX.org @@ -420,7 +420,85 @@ rename. typed-flan branch freezes the static language pre-dyn. Left open until the lane is built: whether the descriptor points at the container or is a fattened slice stored beside it. That only bites if the container can grow and move, which would leave a push through dyn holding - a stale pointer. + a stale pointer. — LANDED. Settled: a Vec view holds the address of the + Vec's own header and reads its ptr/len live on every operation, so a push + that reallocates cannot go stale — there is no snapshot to invalidate, + because flan_vec_grow overwrites that same header in place. A slice and a + fixed array cannot grow, so a flat view snapshots pointer and length once, + which is sound for both and is not the weaker half of an asymmetric + choice — pointing a flat view at its own value's slot instead would be + worse, since a slot's lifetime is not the slice's. The element set is i64, + f64 and bool only: a string element's dyn form is a pointer into the + collector's heap, and a typed container's storage is memory the collector + never scans, so a wider set would let a write plant a live reference + nothing traces. (Vec string) and (Map K V) keep the refusal [box] already + gave every container. Both backends, runtime/flan_dyn.c and .h, checker + tests, an acceptance row per backend, and a survey program + (dyn-view.flan) proving the view against both a growing Vec and a fixed + array/slice, plus its own two trap modes. + + REVIEW, 2026-09-20: relocation was proved sound but relocation was not + the hazard that mattered — a view can outlive the frame its Vec header + sits in, which nothing could reach before this lane because [box] + 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 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 steps every index of a multi-index [(at g i j)] the way [indexed] does + and demands an array at each level, because the whole index list rides on + one node and reading the target's type alone settled level zero only), 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 + the defvar spelling that works. A heap-held header is not expressible + 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. + + 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 + to read (fixed by never rendering it — the sentence names the epochs and + nothing else); [dyn_equal]'s VEC arm read raw [len]/[items] regardless of + kind, so two views with different contents compared equal and a map keyed + by a view collided with every other view (fixed with view-aware + length/element readers, [vecish_len]/[vecish_at]); and the three + restatements of flan_vec's layout (flan_rt.c, flan_dyn.c, dyn_ops.c) had + nothing tying them together despite a comment's claim that they did — a + [layout] probe on each, compared field by field in dyn_ops.c's new + "layout" mode, makes a disagreement a FAIL line instead of a silent + corruption. 4. nil: arrives with maps. nil <-> None at (Option T) boundaries, trap at bare T, (Some nil) unconstructible. — LANDED, 3c1fb1b. The bare-T trap is split: a literal nil the checker can see is refused at compile time, in diff --git a/lib/check.ml b/lib/check.ml index 6c520ac..5727857 100644 --- a/lib/check.ml +++ b/lib/check.ml @@ -1441,6 +1441,138 @@ let no_dyn_yet loc ~into t extra = "%s does not cross into %s yet%s" (Types.to_string t) (if into then "dyn" else "a written type") extra +(* M2 item 3: a typed container crossing into dyn as a view. The element set + is exactly [unboxable] above — i64, f64, bool — and that is not a smaller + version of the same cut for the same reason: every other element type + would need [box] to run on IT too, and a string element's dyn form is a + pointer into the collector's heap, while a typed container's storage is + arena or stack memory the collector never scans. Writing that pointer + into memory nobody roots is a live reference the collector could free out + from under — the hazard runtime/flan_dyn.h's view section states at + length — and i64/f64/bool carry no pointer, so a view restricted to them + cannot manufacture it. It is a compile-time refusal here rather than a + run-time one because the element type is exactly what the checker already + knows at the crossing. The FLAN_VIEW_* constants are runtime/flan_dyn.h's; + this is the compiler's one copy of the same table. *) +let view_elem (t : Types.t) : int64 option = + match t with + | Types.Int Types.I64 -> Some 0L (* FLAN_VIEW_I64 *) + | Types.Float Types.F64 -> Some 1L (* FLAN_VIEW_F64 *) + | Types.Bool -> Some 2L (* FLAN_VIEW_BOOL *) + | _ -> None + +let view_elem_lit loc (k : int64) = + mk loc (Types.Int Types.I32) (Tast.Int (k, Types.I32)) + +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, 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 + address into the container's own storage, chased fresh on every + operation, which is what makes a Vec's growth safe — but it is also what + makes a *dangling* container's storage a live hazard nothing catches + until somebody reads through the view. A view returned from the function + whose frame the Vec lived in, stashed in a global and read after that + frame is gone, or left behind when a condition transfer unwinds it, are + all stack-use-after-return once box stopped refusing containers outright + — reachable now for the first time, not a pre-existing hole this lane + merely inherited. + + 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 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: 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. The [At] arm below is where + that distinction is made, and it is made per index rather than once: an + [(at g i j)] is a single node carrying the whole index list, so the arm + steps the list the way [indexed] does and an array level at every step is + what it demands. Reading only the target's type would settle level zero + and let a slice at any later level through — which it did, and the + accepted program printed a returned frame's contents. 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 + keeps it is to view the slice expression directly, the way this file's + own survey program does. + + Everything else — a local, a parameter, a temporary, anything reached + through a [Ptr] — answers false. A [Ptr] is refused rather than trusted + because a heap-allocated block and a frame slot are the same type: a + [(Ptr (Vec i64))] taken from a heap allocation would be sound to view, but + the same type is what [(addr some-local)] answers too, and the checker + cannot tell the two apart. Admitting one admits the other, which is the + whole hazard this guard exists to close — so until a Flan type exists + that says "durably heap-owned" and a [Ptr] does not, a container reached + through one is refused rather than guessed at. An arena-held container is + not a separate case: an arena changes where a Vec's *elements* live, never + where its own header — the value a name is bound to — lives, so a Vec + grown from an arena is exactly as permanent as the binding that holds it, + already covered by the cases above. *) +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 :: idx) -> + (* [(at g i j)] is ONE node carrying every index, so the target's own type + is only level zero and asking about it alone misses a slice reached at + any later level. Step the list the way [indexed] does — that walk is + the definition of which levels exist — and require every level stepped + to be an array. *) + let rec all_array ty = function + | [] -> true + | _ :: rest -> + (match ty with + | Types.Array (_, elem) -> all_array elem rest + | _ -> false) + in + all_array target.Tast.ty idx && permanent_root target + | 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 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, anything reached through a slice at any index \ + level — even a global one, 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 = let dyn sym args = rt loc Types.Dyn sym args in match e.Tast.ty with @@ -1465,11 +1597,47 @@ let box loc (e : Tast.expr) : Tast.expr = nothing a dyn could hold. The absent dyn value is nil, which is a \ literal here: write nil" | Types.Never -> e - | Types.Vec _ | Types.Map _ | Types.Slice _ | Types.Array _ -> + (* A view, not a copy: the box holds one word naming where the elements + live and what one of them is, and every read or write goes straight + through to the container's own storage — see runtime/flan_dyn.h's + view section for the whole of the argument, including why the + descriptor points AT the container (a Vec's own header address) + rather than snapshotting its ptr+len. That is what makes a push + through the view safe even though a Vec can grow and move: there is + 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 -> + (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 -> + (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) -> + (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 ]) + | Types.Map _ -> no_dyn_yet loc ~into:true e.Tast.ty ". The dyn container at this milestone is the runtime's own, from \ - (vec-new dyn); a typed container has a representation the dyn runtime \ - cannot walk" + (map-new dyn); a typed (Map K V) has a representation the dyn \ + runtime cannot walk" (* [Option] is on this list in name only: [expect] intercepts it before [box] ever sees one — [box_option] is the real answer, M2 item 4 — so this arm only fires for a direct caller that hands [box] an Option @@ -2078,6 +2246,36 @@ let rec check ctx ?want (e : Ast.expr) : Tast.expr = (match ctx.defers with | [] -> r | ds -> mk loc Types.Never (Tast.Do (ds @ [ r ]))) + (* (set (at target i) x) against a dyn target — a dyn vec from (vec-new + dyn), or a typed container's own view (M2 item 3) — is a call and not a + place: [flan_dyn_set_at] tag-checks [x]'s dyn tag against what the vec + or the view holds and traps on a mismatch, which is not a memory write + [Tast.Set] could express through a pointer. [target] is checked once, + here, and handed to [vec_at]/[indexed] unchecked in the [else] branch + below rather than re-checked by [check_place] — checking it twice would + evaluate a target with a side effect twice. A dyn target indexed more + than once — nothing in this milestone builds one — still falls to the + ordinary [Ast.Set] arm below, and [indexed] refuses it by name. *) + | Ast.Set (Ast.Pindex (target, [ idx ]), v) -> + let target = check ctx target in + if target.Tast.ty = Types.Dyn then + let i = check ctx ~want:Types.Dyn idx in + let v = check ctx ~want:Types.Dyn v in + expect ctx loc ~want + (rt loc Types.Unit "flan_dyn_set_at" [ target; i; v ]) + else begin + let p, pty = + match target.Tast.ty with + | Types.Vec _ -> + let pp, ty = vec_at ctx loc target [ idx ] in + Tast.Pderef pp, ty + | _ -> + let iidx, ty = indexed ctx target [ idx ] in + Tast.Pindex (target, iidx), ty + in + let v = check ctx ~want:pty v in + expect ctx loc ~want (mk loc Types.Unit (Tast.Set (p, v))) + end | Ast.Set (p, v) -> let p, pty = check_place ctx loc p in let v = check ctx ~want:pty v in diff --git a/lib/emit.ml b/lib/emit.ml index 08afc7c..1f16ef1 100644 --- a/lib/emit.ml +++ b/lib/emit.ml @@ -2640,6 +2640,15 @@ and prim f (e : Tast.expr) (p : Tast.prim) (args : Tast.expr list) = Passing the header by value here would hand the runtime a copy to grow and leave the caller's untouched. *) | Types.Vec _ | Types.Map _ -> [ "ptr " ^ addr f a ] + (* A fixed array crossing into a dyn view (M2 item 3) needs its + address for the same reason a Vec or a Map does here — the + view reads through it live, and passing the value would hand + the runtime a copy nothing writes back through. Every other + [Rt] caller of an array argument is [flan_dyn_view_flat], + which takes the address and never mutates the array's shape, + so this is not the move-only argument Vec/Map's comment is + about — it is simply the only way to view rather than copy. *) + | Types.Array _ -> [ "ptr " ^ addr f a ] | t -> [ ll t ^ " " ^ value f a ]) args) in @@ -3388,6 +3397,8 @@ declare i32 @flan_dyn_need_bool(i64) declare i32 @flan_dyn_is_nil(i64) declare i64 @flan_dyn_need_not_nil(i64) declare i32 @flan_dyn_truthy(i64) +declare i64 @flan_dyn_view_vec(ptr, i32) +declare i64 @flan_dyn_view_flat(ptr, i64, i32) declare void @flan_dyn_root_push(ptr) declare void @flan_dyn_root_push_desc(ptr, ptr) declare void @flan_dyn_root_pop(i64) diff --git a/lib/x86.ml b/lib/x86.ml index ecfae3c..2b30dd6 100644 --- a/lib/x86.ml +++ b/lib/x86.ml @@ -1461,6 +1461,13 @@ let classify_c (l : loc) (t : Types.t) = | Types.String | Types.Slice _ -> [ Aint (l, Types.Ptr Types.Unit); Alen l ] | Types.Unit | Types.Never -> [] | Types.Vec _ | Types.Map _ -> [ Aptr l ] + (* A fixed array crossing into a dyn view (M2 item 3) needs its address for + the same reason: the view reads through it live and a copy would leave + the caller's own array unseen by later writes through the view. Every + [Rt] call that takes an array argument is [flan_dyn_view_flat], which + never mutates the array's shape, so this is not the move-only case + Vec/Map is. *) + | Types.Array _ -> [ Aptr l ] | _ when is_agg t -> unsupported "aggregate %s across the C boundary" (Types.to_string t) | _ when is_float t -> [ Aflt (l, t) ] @@ -2708,7 +2715,7 @@ and call_native f ~sym ?(chan = false) ~(args : Tast.expr list) ~rty dst = List.map (fun (a : Tast.expr) -> (match a.Tast.ty with - | Types.Vec _ | Types.Map _ -> lvalue f a + | Types.Vec _ | Types.Map _ | Types.Array _ -> lvalue f a | _ -> eval f a), a.Tast.ty) args in diff --git a/runtime/flan_dyn.c b/runtime/flan_dyn.c index 0aadc59..d57ca65 100644 --- a/runtime/flan_dyn.c +++ b/runtime/flan_dyn.c @@ -34,6 +34,7 @@ */ #include +#include #include #include #include @@ -55,6 +56,16 @@ void flan_write_stdout(const uint8_t *p, int64_t n); * only one of. So flan_rt.c exports a thin wrapper and this calls it. */ _Noreturn void flan_trap(const uint8_t *name, int64_t namelen); +/* Growing a Vec through a dyn view borrows flan_rt.c's own growth: doubling, + * allocator adoption and the epoch check all live in [flan_vec_push], and + * re-implementing any of that here would be a second copy of logic the + * duplicity doctrine (docs/SPIKE-DUPLICITY.md) says belongs on one side only. + * [v] is declared [void *] rather than [flan_vec *] so this file need not + * name flan_rt.c's type; the two structs' layouts must agree, which is + * [flan_dyn_vec_hdr] below, restated for the same reason [flan_desc] is. */ +int8_t flan_vec_push(void *v, const void *elem, int64_t size, int64_t align, + const uint8_t *loc, int64_t loclen); + /* ── The representation ──────────────────────────────────────────────── * * NaN-boxed, in a word. A double is *itself*: the 2^64 minus a NaN's worth of @@ -126,6 +137,11 @@ typedef struct flan_desc { * already opens with, never a memcmp. */ #define BOX_KW 4u +/* Restated from flan_dyn.h — a view's element kind. */ +#define FLAN_VIEW_I64 0 +#define FLAN_VIEW_F64 1 +#define FLAN_VIEW_BOOL 2 + /* Spelled as a negated positive rather than as a shift of -1: shifting a * negative value left is undefined, and this file is swept by UBSan. */ #define DYN_INT_MAX (((int64_t)1 << 47) - 1) @@ -164,6 +180,45 @@ static inline flan_dyn dyn_make(unsigned tag, uint64_t payload) { #define OBJ_VEC 1 #define OBJ_INT 2 /* an i64 too wide for the payload */ #define OBJ_MAP 3 /* keys and values interleaved: k0 v0 k1 v1 ... */ +#define OBJ_VIEW 4 /* a typed container crossing into dyn as a view */ + +/* flan_vec, restated. This file must not name flan_rt.c's [flan_vec] — see + * the "if either table changes, change both" note above [flan_vec_push] — + * so a view over a [(Vec T)] is built from an address whose first five words + * this mirrors exactly. Only [ptr], [len] and [epoch]/[alloc] are ever read + * through it; nothing here writes one. */ +typedef struct flan_dyn_vec_hdr { + void *ptr; + int64_t len; + int64_t cap; + void *alloc; + int64_t epoch; +} flan_dyn_vec_hdr; + +/* This mirror's own layout, reported the same way flan_rt.c's + * [flan_vec_layout] reports the original's — see that function's comment + * for what ties the two together and why nothing at compile time otherwise + * does. */ +void flan_dyn_vec_hdr_layout(int64_t out[6]) { + out[0] = (int64_t)sizeof(flan_dyn_vec_hdr); + out[1] = (int64_t)offsetof(flan_dyn_vec_hdr, ptr); + out[2] = (int64_t)offsetof(flan_dyn_vec_hdr, len); + out[3] = (int64_t)offsetof(flan_dyn_vec_hdr, cap); + out[4] = (int64_t)offsetof(flan_dyn_vec_hdr, alloc); + out[5] = (int64_t)offsetof(flan_dyn_vec_hdr, epoch); +} + +/* flan_allocator's prefix, far enough to read the one word a stale-container + * check needs. The struct has more fields after [epoch]; this file never + * touches them; and the alignment of a leading same-typed prefix is the same + * in any translation unit that agrees on the field order, which is the + * "change both" this comment is the other half of. */ +typedef struct flan_dyn_alloc_hdr { + void *proc; + void *data; + uint32_t caps; + uint64_t epoch; +} flan_dyn_alloc_hdr; typedef struct flan_obj { struct flan_obj *next; /* every object ever allocated, newest first */ @@ -179,13 +234,32 @@ typedef struct flan_obj { entries and [cap] counting entries too. Sharing the arm is what lets the marker and the sweep treat the two kinds with one load and a doubled count rather than a second field to keep in step. */ + /* OBJ_VIEW: a typed container's elements, native words this file did not + allocate and does not own. [is_vec] set means [base] is a + [flan_dyn_vec_hdr *] and [len] here is unused — the live length is + read from the header on every operation, which is the whole of why a + Vec growing through the view cannot go stale. [is_vec] clear means + [base] is the first element's address and [len] is the snapshot taken + at the crossing, for a slice or a fixed array, neither of which moves. + [elem] is one of FLAN_VIEW_I64/F64/BOOL. */ + struct { void *base; int64_t len; int32_t elem; int32_t is_vec; } view; /* OBJ_TEXT's bytes trail the header; see [obj_text_bytes]. */ } u; } flan_obj; /* How many dyn words hang off an object's items block — the count the marker - * walks and the sweep charges. A map holds two per entry. */ + * walks and the sweep charges. A map holds two per entry. + * + * OBJ_VIEW answers 0 explicitly rather than falling into the [o->len] arm. + * [mark_push] never puts a view on the mark stack — it traces only + * OBJ_VEC/OBJ_MAP — so this is not reachable today, but [o->u.view.base] + * aliases [o->u.v.items] in the union, and a native array of i64 or f64 + * reinterpreted as dyn words is exactly the kind of thing this file's + * roots contract exists to prevent happening by accident. Answering 0 here + * is what keeps a future change to the marking gate from silently trusting + * this function's default arm instead of failing loudly. */ static inline int64_t obj_words(flan_obj *o) { + if (o->kind == OBJ_VIEW) return 0; return o->kind == OBJ_MAP ? o->len * 2 : o->len; } @@ -309,7 +383,11 @@ int32_t flan_dyn_tag(flan_dyn v) { if (o == NULL) return FLAN_DYN_TAG_NIL; switch (o->kind) { case OBJ_TEXT: return FLAN_DYN_TAG_TEXT; + /* A view answers the same tag a heap vec does: from a dyn program's + side there is nothing to tell them apart by, which is the point of a + view being indistinguishable rather than a fourth kind of vec. */ case OBJ_VEC: return FLAN_DYN_TAG_VEC; + case OBJ_VIEW: return FLAN_DYN_TAG_VEC; case OBJ_MAP: return FLAN_DYN_TAG_MAP; default: return FLAN_DYN_TAG_INT; } @@ -403,6 +481,19 @@ static void emit_escaped(const uint8_t *p, int64_t n) { static int64_t dyn_int_value(flan_dyn v); /* forward: both int shapes */ static double dyn_num_value(flan_dyn v); +/* forward: the view helpers, needed by [render] and [say_render] above where + * they are defined, alongside the container operations below */ +static int64_t view_len(const char *op, flan_obj *o); +static void *view_base(flan_obj *o); +static flan_dyn view_box(int32_t elem, const uint8_t *p); +static int64_t view_elem_size(int32_t elem); + +/* forward: needed by [dyn_equal] below, defined alongside the view helpers + * further down — a length and an element reader that answer correctly + * whether [o] is an ordinary heap vec or a view over a typed container. */ +static int64_t vecish_len(flan_obj *o); +static flan_dyn vecish_at(flan_obj *o, int64_t i); + static void render(flan_dyn v, int depth, int nested) { char buf[64]; int32_t t = flan_dyn_tag(v); @@ -461,11 +552,17 @@ static void render(flan_dyn v, int depth, int nested) { } default: { flan_obj *o = dyn_obj(v); - int64_t i; + int64_t i, n = o->kind == OBJ_VIEW ? view_len("print", o) : o->len; emit("["); - for (i = 0; i < o->len; i++) { + for (i = 0; i < n; i++) { emit(" "); - render(o->u.v.items[i], depth + 1, 1); + if (o->kind == OBJ_VIEW) + render(view_box(o->u.view.elem, + (const uint8_t *)view_base(o) + + i * view_elem_size(o->u.view.elem)), + depth + 1, 1); + else + render(o->u.v.items[i], depth + 1, 1); } emit("]"); return; @@ -551,14 +648,21 @@ static void say_render(sayer *s, flan_dyn v, int depth) { } default: { flan_obj *o = dyn_obj(v); - int64_t i; + int64_t i, n = o->kind == OBJ_VIEW ? view_len("print", o) : o->len; if (depth >= 2) { say_puts(s, "[...]"); return; } say_puts(s, "["); - for (i = 0; i < o->len && s->n < s->cap - 8; i++) { + for (i = 0; i < n && s->n < s->cap - 8; i++) { say_puts(s, " "); - say_render(s, o->u.v.items[i], depth + 1); + if (o->kind == OBJ_VIEW) + say_render(s, + view_box(o->u.view.elem, + (const uint8_t *)view_base(o) + + i * view_elem_size(o->u.view.elem)), + depth + 1); + else + say_render(s, o->u.v.items[i], depth + 1); } - say_puts(s, i < o->len ? " ...]" : "]"); + say_puts(s, i < n ? " ...]" : "]"); return; } } @@ -1211,12 +1315,23 @@ static int dyn_equal(flan_dyn a, flan_dyn b, int depth) { } if (ta == FLAN_DYN_TAG_VEC) { flan_obj *x = dyn_obj(a), *y = dyn_obj(b); - int64_t i; + int64_t i, xn, yn; if (x == y) return 1; if (depth >= EQ_DEPTH) return 0; - if (x->len != y->len) return 0; - for (i = 0; i < x->len; i++) - if (!dyn_equal(x->u.v.items[i], y->u.v.items[i], depth + 1)) return 0; + /* [x]/[y] may each be an ordinary heap vec or a view (M2 item 3) — the + tag does not say which, so [vecish_len]/[vecish_at] below read either + shape correctly. Reading raw through [x->u.v.items] the way this arm + used to is wrong for a view: nothing sets [len] for OBJ_VIEW, so it + reads back 0, and the elements alias [u.view.base] reinterpreted as + dyn words — two views with different contents would compare equal, a + view and an equal heap vec would compare unequal, and a map keyed by + any view would collide with every other view, silently, with nothing + to crash. */ + xn = vecish_len(x); + yn = vecish_len(y); + if (xn != yn) return 0; + for (i = 0; i < xn; i++) + if (!dyn_equal(vecish_at(x, i), vecish_at(y, i), depth + 1)) return 0; return 1; } /* Two maps are equal when they hold the same keys and each key answers an @@ -1265,9 +1380,156 @@ static inline int is_map(flan_dyn v) { return flan_dyn_tag(v) == FLAN_DYN_TAG_MAP; } +/* ── Typed containers as views ───────────────────────────────────────── + * + * Every entry point below already dispatches on [flan_dyn_tag], which does + * not distinguish a view from a heap vec — see [flan_dyn_tag]'s switch — so + * [flan_dyn_len], [flan_dyn_at], [flan_dyn_set_at], [flan_dyn_push] and the + * printer each add one branch for [OBJ_VIEW] beside the existing [OBJ_VEC] + * one. What follows is that branch's machinery. */ + +static int64_t view_elem_size(int32_t elem) { + return elem == FLAN_VIEW_BOOL ? 1 : 8; +} + +/* The stale-container check flan_rt.c's [flan_vec_check] runs for a typed + * Vec, restated for a view's own trap rather than reused: the duplicity + * doctrine's dyn side gets its own spelling (docs/SPIKE-DUPLICITY.md), and a + * dyn program that hits this wants the same park-and-inspect [flan_trap] + * gives every other dyn mistake, not the typed side's [rt_die]. A Vec with + * no allocator yet — one nobody has pushed to — has nothing to check. + * + * The message never renders the view it just declared unsafe to read — + * review's second finding, and it was not a decoration this dropped for + * safety's sake, it was a real infinite recursion: [say] on a view calls + * [say_render]'s view branch, which calls [view_len], which calls back in + * here, unconditionally, because the epoch is still stale. Every render of + * this same view would hit the same check and take the same branch, so + * nothing about depth or a visited set closes it — the fix is that a + * stale-container check must never read the container it has just refused + * to trust, not even to describe it in the sentence explaining why. */ +static void view_vec_check(const char *op, flan_dyn_vec_hdr *h) { + if (h->alloc) { + flan_dyn_alloc_hdr *a = (flan_dyn_alloc_hdr *)h->alloc; + if ((int64_t)a->epoch != h->epoch) { + fflush(stdout); + fprintf(stderr, + "dyn %s: this view's container's allocator was released — the " + "Vec was made at epoch %lld and the allocator is at %lld now\n", + op, (long long)h->epoch, (long long)(int64_t)a->epoch); + flan_trap((const uint8_t *)"DynRange", 8); + } + } +} + +/* [len] and [base], read live for a Vec view (so a push that grows and + * moves the underlying Vec is seen the very next operation) and read from + * the snapshot for a flat one. */ +static int64_t view_len(const char *op, flan_obj *o) { + if (o->u.view.is_vec) { + flan_dyn_vec_hdr *h = (flan_dyn_vec_hdr *)o->u.view.base; + view_vec_check(op, h); + return h->len; + } + return o->u.view.len; +} + +static void *view_base(flan_obj *o) { + if (o->u.view.is_vec) return ((flan_dyn_vec_hdr *)o->u.view.base)->ptr; + return o->u.view.base; +} + +/* Reads box the element on the way out — the runtime already knows how to + * box an i64, an f64 or a bool, so this is that, from raw bytes rather than + * from a C value already in hand. */ +static flan_dyn view_box(int32_t elem, const uint8_t *p) { + switch (elem) { + case FLAN_VIEW_I64: { int64_t x; memcpy(&x, p, 8); return flan_dyn_from_i64(x); } + case FLAN_VIEW_F64: { double x; memcpy(&x, p, 8); return flan_dyn_from_f64(x); } + default: { uint8_t b = *p; return flan_dyn_from_bool(b); } + } +} + +/* A length and an element reader that answer correctly whether [o] is an + * ordinary heap vec (OBJ_VEC, elements are dyn words) or a view over a + * typed container (OBJ_VIEW, elements are native bytes boxed on the way + * out) — the pair [dyn_equal]'s VEC arm needs so that a view compares + * correctly against another view and against an ordinary vec alike. Reading + * [o->len]/[o->u.v.items] directly, the way that arm used to, answers 0 and + * garbage for a view: nothing sets [len] for OBJ_VIEW, and its elements + * alias [u.view.base] reinterpreted as dyn words rather than the native + * bytes they are. */ +static int64_t vecish_len(flan_obj *o) { + return o->kind == OBJ_VIEW ? view_len("=", o) : o->len; +} + +static flan_dyn vecish_at(flan_obj *o, int64_t i) { + if (o->kind == OBJ_VIEW) + return view_box(o->u.view.elem, + (const uint8_t *)view_base(o) + + i * view_elem_size(o->u.view.elem)); + return o->u.v.items[i]; +} + +/* Writes tag-check on the way in: the dyn value's tag must be the one this + * view's element type wants, or this traps by name and never coerces or + * truncates a mismatched value into the slot. [v] is the view, for the + * sentence's container half; [x] is the value that was refused. */ +static void view_unbox(const char *op, flan_dyn v, int32_t elem, flan_dyn x, + uint8_t *p) { + switch (elem) { + case FLAN_VIEW_I64: { + int64_t n; + if (flan_dyn_tag(x) != FLAN_DYN_TAG_INT) + trap2(TYPE_TRAP, op, "this view's elements are int", v, x); + n = dyn_int_value(x); + memcpy(p, &n, 8); + return; + } + case FLAN_VIEW_F64: { + double d; + if (flan_dyn_tag(x) != FLAN_DYN_TAG_FLOAT) + trap2(TYPE_TRAP, op, "this view's elements are float", v, x); + d = dyn_num_value(x); + memcpy(p, &d, 8); + return; + } + default: { + uint8_t b; + if (flan_dyn_tag(x) != FLAN_DYN_TAG_BOOL) + trap2(TYPE_TRAP, op, "this view's elements are bool", v, x); + b = dyn_payload(x) ? 1 : 0; + *p = b; + return; + } + } +} + +flan_dyn flan_dyn_view_vec(void *hdr, int32_t elem) { + flan_obj *o = gc_alloc(OBJ_VIEW, 0); + o->u.view.base = hdr; + o->u.view.len = 0; + o->u.view.elem = elem; + o->u.view.is_vec = 1; + return dyn_make(BOX_OBJ, (uint64_t)(uintptr_t)o); +} + +flan_dyn flan_dyn_view_flat(void *data, int64_t len, int32_t elem) { + flan_obj *o = gc_alloc(OBJ_VIEW, 0); + o->u.view.base = data; + o->u.view.len = len; + o->u.view.elem = elem; + o->u.view.is_vec = 0; + return dyn_make(BOX_OBJ, (uint64_t)(uintptr_t)o); +} + flan_dyn flan_dyn_len(flan_dyn v) { - if (is_text(v) || is_vec(v) || is_map(v)) - return flan_dyn_from_i64(dyn_obj(v)->len); + if (is_text(v) || is_map(v)) return flan_dyn_from_i64(dyn_obj(v)->len); + if (is_vec(v)) { + flan_obj *o = dyn_obj(v); + if (o->kind == OBJ_VIEW) return flan_dyn_from_i64(view_len("len", o)); + return flan_dyn_from_i64(o->len); + } trap1(TYPE_TRAP, "len", "only a text, a vec or a map has one", v); } @@ -1290,6 +1552,12 @@ flan_dyn flan_dyn_at(flan_dyn v, flan_dyn i) { trap2(TYPE_TRAP, "at", "only a text or a vec is indexed", v, i); k = need_index("at", v, i); o = dyn_obj(v); + if (o->kind == OBJ_VIEW) { + int64_t len = view_len("at", o); + if (k < 0 || k >= len) trap_range("at", v, k, len); + return view_box(o->u.view.elem, + (const uint8_t *)view_base(o) + k * view_elem_size(o->u.view.elem)); + } if (k < 0 || k >= o->len) trap_range("at", v, k, o->len); if (o->kind == OBJ_TEXT) return flan_dyn_from_i64(obj_text_bytes(o)[k]); return o->u.v.items[k]; @@ -1298,13 +1566,20 @@ flan_dyn flan_dyn_at(flan_dyn v, flan_dyn i) { void flan_dyn_set_at(flan_dyn v, flan_dyn i, flan_dyn x) { int64_t k; flan_obj *o; - (void)x; if (is_text(v)) trap2(TYPE_TRAP, "set-at", "a text is immutable — build another one", v, i); if (!is_vec(v)) trap2(TYPE_TRAP, "set-at", "only a vec is assigned into", v, i); k = need_index("set-at", v, i); o = dyn_obj(v); + if (o->kind == OBJ_VIEW) { + int64_t len = view_len("set-at", o); + uint8_t *p; + if (k < 0 || k >= len) trap_range("set-at", v, k, len); + p = (uint8_t *)view_base(o) + k * view_elem_size(o->u.view.elem); + view_unbox("set-at", v, o->u.view.elem, x, p); + return; + } if (k < 0 || k >= o->len) trap_range("set-at", v, k, o->len); o->u.v.items[k] = x; } @@ -1317,6 +1592,20 @@ void flan_dyn_push(flan_dyn v, flan_dyn x) { trap2(TYPE_TRAP, "push", "only a vec is pushed to", v, x); } o = dyn_obj(v); + if (o->kind == OBJ_VIEW) { + uint8_t buf[8]; + static const uint8_t push_loc[] = "(dyn push)"; + int64_t size; + if (!o->u.view.is_vec) + trap2(TYPE_TRAP, "push", + "this view is a slice or an array and cannot grow", v, x); + size = view_elem_size(o->u.view.elem); + view_unbox("push", v, o->u.view.elem, x, buf); + if (!flan_vec_push(o->u.view.base, buf, size, size, push_loc, + (int64_t)sizeof(push_loc) - 1)) + trap_oom(size); + return; + } if (o->len == o->u.v.cap) { int64_t cap = o->u.v.cap ? o->u.v.cap * 2 : 8; flan_dyn *items = diff --git a/runtime/flan_dyn.h b/runtime/flan_dyn.h index 390599a..c5aee07 100644 --- a/runtime/flan_dyn.h +++ b/runtime/flan_dyn.h @@ -151,6 +151,64 @@ flan_dyn flan_dyn_need_not_nil(flan_dyn v); * "", an empty vec, an empty map, and any keyword. Never traps. */ uint8_t flan_dyn_truthy(flan_dyn v); +/* ── Typed containers as views — M2 item 3 ───────────────────────────── + * + * A [(Vec T)], a [T] slice, or a fixed [n T] array crossing into dyn is a + * VIEW, not a copy: the box holds a small heap record naming where the + * elements live and what one of them is, and every read or write goes + * straight through to the container's own storage. [flan_dyn_at] boxes an + * element on the way out; [flan_dyn_set_at] tag-checks the dyn value it is + * given against the element type on the way in and traps, by [flan_trap], + * on a mismatch — never a silent coercion. + * + * T is restricted to i64, f64 and bool — exactly the set [flan_dyn_need_i64] + * and friends already treat as crossing the typed boundary both ways. That + * is not an arbitrary cut: the excluded case that matters is a string + * element, whose dyn form is a pointer into this collector's heap, while a + * typed container's storage is arena or stack memory the collector never + * scans. Writing such a pointer into that memory would be a live reference + * nothing ever traces — a use-after-free the collector cannot see coming, + * not a bug in this file but a hazard the type admits. i64, f64 and bool + * carry no such pointer, so a view restricted to them cannot manufacture + * it. [box] in lib/check.ml keeps the "does not cross into dyn yet" refusal + * for every other element type, and this paragraph is why. + * + * Two kinds, because the containers split exactly here: a [(Vec T)] can grow + * and move (a push may reallocate), a slice and a fixed array cannot. + * + * [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, 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 + * what makes the failure the open design question worried about + * (a push through dyn holding a dangling pointer) impossible rather than + * merely unlikely: there is nothing captured at the crossing for a later + * push to invalidate. + * + * [flan_dyn_view_flat] takes a data address and a length captured once, at + * the crossing — sound for a slice and for a fixed array because neither + * ever moves or grows. Note the asymmetry is not an oversight: pointing + * *this* case at the value's own slot instead would be worse than a + * snapshot, because a slot's lifetime is not the slice's, and a slice taken + * from a Vec is already one push away from dangling on its own account + * (flan_vec_grow's own comment says so) — the view is exactly as + * stale-safe as the thing it is a view of, no more and no less. + */ +#define FLAN_VIEW_I64 0 +#define FLAN_VIEW_F64 1 +#define FLAN_VIEW_BOOL 2 + +flan_dyn flan_dyn_view_vec(void *hdr, int32_t elem); +flan_dyn flan_dyn_view_flat(void *data, int64_t len, int32_t elem); + /* ── The collector ───────────────────────────────────────────────────── * * Mark-sweep, precise, and never moving. [flan_gc_init] is idempotent, and the @@ -261,6 +319,14 @@ const char *flan_dyn_tag_name(int32_t tag); int64_t flan_gc_count(void); void flan_gc_set_floor(int64_t bytes); +/* Reports flan_dyn.c's own mirror of flan_rt.c's [flan_vec] — [size, then + * the offset of ptr, len, cap, alloc, epoch] — for test/dyn_ops.c's + * "layout" mode to compare against flan_rt.c's [flan_vec_layout] and + * against its own hand-built mirror. See [flan_vec_layout]'s comment in + * flan_rt.c for what this ties together and why nothing at compile time + * otherwise does. */ +void flan_dyn_vec_hdr_layout(int64_t out[6]); + #ifdef __cplusplus } #endif diff --git a/runtime/flan_rt.c b/runtime/flan_rt.c index f080aa4..0883940 100644 --- a/runtime/flan_rt.c +++ b/runtime/flan_rt.c @@ -12,6 +12,7 @@ */ #include +#include #include #include #include @@ -1490,6 +1491,27 @@ typedef struct flan_vec { int64_t epoch; } 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 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 + * struct's real size and field offsets, and test/dyn_ops.c's "layout" mode + * compares them against its own [hand_vec]'s and against flan_dyn.c's + * [flan_dyn_vec_hdr_layout], so a disagreement is a FAIL line in `dune test` + * rather than a silent corruption the next line over. */ +void flan_vec_layout(int64_t out[6]) { + out[0] = (int64_t)sizeof(flan_vec); + out[1] = (int64_t)offsetof(flan_vec, ptr); + out[2] = (int64_t)offsetof(flan_vec, len); + out[3] = (int64_t)offsetof(flan_vec, cap); + out[4] = (int64_t)offsetof(flan_vec, alloc); + out[5] = (int64_t)offsetof(flan_vec, epoch); +} + /* The request that did not fit, for the condition the compiler builds at the * failing site. A pair of globals rather than out-parameters because the * condition is a value struct on the signalling frame's stack with fixed diff --git a/test/dyn_ops.c b/test/dyn_ops.c index 2c0360a..77fe965 100644 --- a/test/dyn_ops.c +++ b/test/dyn_ops.c @@ -32,6 +32,9 @@ #include "flan_dyn.h" void flan_rt_init(int32_t argc, char **argv); +void flan_vec_free(void *v, int64_t size, int64_t align, const uint8_t *loc, + int64_t loclen); +void flan_vec_layout(int64_t out[6]); static int failures; @@ -361,6 +364,203 @@ static void ops(void) { (void)s; } +/* 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]) — 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] + * and compares both against [offsetof] on this very struct, so a field + * reordered in any one of the three is a FAIL line here rather than a + * silent corruption at whatever call site next dereferences the wrong + * offset. A declared-as-[void*] prototype on its own proves nothing about + * layout — it was named as if it did in an earlier version of this + * comment, which was wrong, and [layout] is what makes the claim true. */ +typedef struct { + void *ptr; + int64_t len; + int64_t cap; + void *alloc; + int64_t epoch; +} hand_vec; + +/* The runtime's half of M2 item 3: a typed container crossing into dyn as a + * view, driven directly with no compiler in the loop — [flan_dyn_view_vec] + * and [flan_dyn_view_flat] built by hand over a [hand_vec] and a plain + * array, exactly as the checker's [box] will build them over a real [(Vec + * i64)] and a real [[4]i64]. */ +static void view(void) { + int64_t buf[4] = { 10, 20, 30, 40 }; + flan_dyn flat = flan_dyn_nil(), vv = flan_dyn_nil(); + flan_dyn_root_push(&flat); + flan_dyn_root_push(&vv); + + /* A flat view over a fixed array: reads box, writes tag-check, and the + storage really is the array's own — a write through the view is read + back through the C array with no call into this file at all. */ + flat = flan_dyn_view_flat(buf, 4, FLAN_VIEW_I64); + check(flan_dyn_tag(flat) == FLAN_DYN_TAG_VEC, "a view tags as a vec"); + check(num(flan_dyn_len(flat)) == 4, "flat view len"); + check(num(flan_dyn_at(flat, flan_dyn_from_i64(2))) == 30, "flat view at"); + flan_dyn_set_at(flat, flan_dyn_from_i64(2), flan_dyn_from_i64(99)); + check(buf[2] == 99, "flat view write reaches the array"); + buf[3] = 7; + check(num(flan_dyn_at(flat, flan_dyn_from_i64(3))) == 7, + "the array's own write reaches the view — it is not a copy"); + prints(flat, "[ 10 20 99 7]"); + + /* Structural equality, view-aware — review's third finding. [dyn_equal]'s + VEC arm used to read [x->len]/[x->u.v.items] regardless of kind, which + for a view answers 0 and garbage: two views with different contents + compared equal, a view and an equal heap vec compared unequal, and a + map keyed by any view collided with every other view. [buf] now reads + [ 10 20 99 7]; [same] is a second, independent view over the identical + bytes, and [other] a view over one differing element. */ + { + int64_t same_buf[4] = { 10, 20, 99, 7 }; + int64_t diff_buf[4] = { 10, 20, 99, 8 }; + flan_dyn same = flan_dyn_view_flat(same_buf, 4, FLAN_VIEW_I64); + flan_dyn other = flan_dyn_view_flat(diff_buf, 4, FLAN_VIEW_I64); + flan_dyn heap = flan_dyn_vec_new(); + flan_dyn_root_push(&same); + flan_dyn_root_push(&other); + flan_dyn_root_push(&heap); + check(truth(flan_dyn_eq(flat, same)), + "two views over equal bytes are equal"); + check(!truth(flan_dyn_eq(flat, other)), + "two views over different bytes are not equal"); + flan_dyn_push(heap, flan_dyn_from_i64(10)); + flan_dyn_push(heap, flan_dyn_from_i64(20)); + flan_dyn_push(heap, flan_dyn_from_i64(99)); + flan_dyn_push(heap, flan_dyn_from_i64(7)); + check(truth(flan_dyn_eq(flat, heap)), + "a view and an equal heap vec are equal"); + flan_dyn_set_at(heap, flan_dyn_from_i64(3), flan_dyn_from_i64(0)); + check(!truth(flan_dyn_eq(flat, heap)), + "a view and a differing heap vec are not equal"); + flan_dyn_root_pop(3); + } + + /* A vec view: points at the header's own address, so a push that grows + and moves it is seen on the very next read — there is no snapshot to + go stale. */ + { + hand_vec hv; + hv.ptr = NULL; hv.len = 0; hv.cap = 0; hv.alloc = NULL; hv.epoch = 0; + vv = flan_dyn_view_vec(&hv, FLAN_VIEW_I64); + check(num(flan_dyn_len(vv)) == 0, "vec view starts empty"); + { + int i; + for (i = 0; i < 20; i++) flan_dyn_push(vv, flan_dyn_from_i64(i)); + } + check(num(flan_dyn_len(vv)) == 20, "vec view len after growth"); + check(num(flan_dyn_at(vv, flan_dyn_from_i64(0))) == 0, + "first element survived the growth and the move"); + check(num(flan_dyn_at(vv, flan_dyn_from_i64(19))) == 19, + "pushed element reachable after the header's ptr moved"); + /* [hv]'s own fields moved under the view's feet, by construction — the + view never captured [hv.ptr]; it captured [&hv]. */ + check(hv.len == 20 && hv.cap >= 20, "the hand-built header itself grew"); + flan_dyn_set_at(vv, flan_dyn_from_i64(0), flan_dyn_from_i64(-1)); + check(((int64_t *)hv.ptr)[0] == -1, "write through the view reaches hv"); + flan_vec_free(&hv, 8, 8, (const uint8_t *)"view", 4); + } + + /* A bool view and a float view, so the element-tag dispatch is exercised + on all three kinds and not only i64. */ + { + uint8_t bools[2] = { 1, 0 }; + double floats[2] = { 1.5, -2.0 }; + flan_dyn bv = flan_dyn_view_flat(bools, 2, FLAN_VIEW_BOOL); + flan_dyn fv = flan_dyn_view_flat(floats, 2, FLAN_VIEW_F64); + check(truth(flan_dyn_at(bv, flan_dyn_from_i64(0))), "bool view at true"); + check(!truth(flan_dyn_at(bv, flan_dyn_from_i64(1))), "bool view at false"); + flan_dyn_set_at(bv, flan_dyn_from_i64(1), flan_dyn_from_bool(1)); + check(bools[1] == 1, "bool view write"); + check(flan_dyn_need_f64(flan_dyn_at(fv, flan_dyn_from_i64(0))) == 1.5, + "float view at"); + flan_dyn_set_at(fv, flan_dyn_from_i64(0), flan_dyn_from_f64(3.25)); + check(floats[0] == 3.25, "float view write"); + } + + flan_dyn_root_pop(2); + printf(failures == 0 ? "view ok\n" : "view failed\n"); +} + +/* Every wrong way to use a view: out of range, a mismatched write on each of + * the three element kinds, and a push against a fixed-size (flat) view. Each + * is its own mode because each ends the process. */ +static void refuse_view(const char *what) { + static int64_t buf[2] = { 1, 2 }; + flan_dyn v; + if (strcmp(what, "range") == 0) { + v = flan_dyn_view_flat(buf, 2, FLAN_VIEW_I64); + (void)flan_dyn_at(v, flan_dyn_from_i64(2)); + } else if (strcmp(what, "wrongwrite") == 0) { + v = flan_dyn_view_flat(buf, 2, FLAN_VIEW_I64); + flan_dyn_set_at(v, flan_dyn_from_i64(0), text("nope")); + } else if (strcmp(what, "wrongbool") == 0) { + static uint8_t bb[1]; + v = flan_dyn_view_flat(bb, 1, FLAN_VIEW_BOOL); + flan_dyn_set_at(v, flan_dyn_from_i64(0), flan_dyn_from_i64(1)); + } else if (strcmp(what, "wrongfloat") == 0) { + static double ff[1]; + v = flan_dyn_view_flat(ff, 1, FLAN_VIEW_F64); + flan_dyn_set_at(v, flan_dyn_from_i64(0), flan_dyn_from_i64(1)); + } else if (strcmp(what, "flatpush") == 0) { + v = flan_dyn_view_flat(buf, 2, FLAN_VIEW_I64); + flan_dyn_push(v, flan_dyn_from_i64(9)); + } else { + printf("no such refusal: %s\n", what); + exit(2); + } + printf("did not trap\n"); + exit(3); +} + +/* The three restatements of flan_vec's layout, compared — see [hand_vec]'s + * comment for why nothing at compile time otherwise ties them together. + * [offsetof] on [hand_vec] itself is this file's half; [flan_vec_layout] + * and [flan_dyn_vec_hdr_layout] are the other two's. */ +static void layout(void) { + int64_t rt[6], dyn[6]; + int64_t here[6] = { + (int64_t)sizeof(hand_vec), + (int64_t)offsetof(hand_vec, ptr), + (int64_t)offsetof(hand_vec, len), + (int64_t)offsetof(hand_vec, cap), + (int64_t)offsetof(hand_vec, alloc), + (int64_t)offsetof(hand_vec, epoch) + }; + static const char *const names[6] = + { "sizeof", "offset of ptr", "offset of len", "offset of cap", + "offset of alloc", "offset of epoch" }; + int i; + char msg[128]; + flan_vec_layout(rt); + flan_dyn_vec_hdr_layout(dyn); + for (i = 0; i < 6; i++) { + if (rt[i] != here[i]) { + snprintf(msg, sizeof msg, "flan_vec vs. hand_vec's %s: %lld vs. %lld", + names[i], (long long)rt[i], (long long)here[i]); + fail(msg); + } + if (dyn[i] != here[i]) { + snprintf(msg, sizeof msg, + "flan_dyn_vec_hdr vs. hand_vec's %s: %lld vs. %lld", + names[i], (long long)dyn[i], (long long)here[i]); + fail(msg); + } + } + printf(failures == 0 ? "layout ok\n" : "layout failed\n"); +} + /* ── The collector ─────────────────────────────────────────────────────*/ /* Allocate a great many, hold a few, and assert the heap does not grow. The @@ -748,7 +948,19 @@ int main(int argc, char **argv) { if (strcmp(argv[1], "sharing") == 0) { sharing(); return 0; } if (strcmp(argv[1], "unrooted") == 0) { unrooted(); return 0; } if (strcmp(argv[1], "desc") == 0) { desc(); return 0; } + if (strcmp(argv[1], "view") == 0) { + view(); + return failures == 0 ? 0 : 1; + } + if (strcmp(argv[1], "layout") == 0) { + layout(); + return failures == 0 ? 0 : 1; + } if (strncmp(argv[1], "refuse:", 7) == 0) { refuse(argv[1] + 7); return 0; } + if (strncmp(argv[1], "refuseview:", 11) == 0) { + refuse_view(argv[1] + 11); + return 0; + } printf("no such mode: %s\n", argv[1]); return 2; } diff --git a/test/programs/dyn-view.flan b/test/programs/dyn-view.flan new file mode 100644 index 0000000..14b013e --- /dev/null +++ b/test/programs/dyn-view.flan @@ -0,0 +1,151 @@ +;;;; M2 item 3: a typed container crossing into dyn is a VIEW, not a copy. +;;;; +;;;; [as-dyn]'s parameter is unannotated dyn and its argument is a typed +;;;; (Vec i64), a fixed array or a slice — the box happens at the call, on the +;;;; caller's own value, which is what makes [dv] below the SAME storage [v] +;;;; is and not a copy of it. +;;;; +;;;; Every container viewed below is a GLOBAL, and that is not incidental to +;;;; this program — it is the lifetime guard review added after the first +;;;; landing: a view's descriptor chases the container's own address on every +;;;; operation, which is what makes a Vec's growth safe, but it is also what +;;;; makes a DANGLING container's address a live hazard. box refuses a Vec, a +;;;; 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 — 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 — and that holds at every index of a multi-index (at g i j), +;;;; not just the first, so one slice level anywhere in the walk refuses. +;;;; 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, and an element reached through a slice at a +;;;; later index level); 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 +;;;; push through the view — which can only mean the Vec case, since neither +;;;; a slice nor a fixed array can grow — moves the Vec's backing storage and +;;;; the typed side still sees the grown length and the new element. That is +;;;; the design's central claim: the view's descriptor points AT the Vec's +;;;; own header rather than snapshotting its pointer and length, so there is +;;;; no snapshot for the growth to invalidate — and the header itself is the +;;;; global's, which never moves even though the buffer behind it does. +;;;; +;;;; Modes 1 and 2 are the two traps a view can throw: an index outside its +;;;; length, and a write whose dyn tag does not match the element type the +;;;; view was built over. Both come from the runtime, by name, and both end +;;;; the process — a survey program can show at most one trap, so each gets +;;;; its own mode the way test/programs/bounds.flan's do. + +(defn as-dyn [d dyn] dyn d) + +(defvar v (Vec i64) (vec-new i64)) +(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))))] + (cond + (= n 0) + (do + ;; A (Vec i64) view, over the global. + (push v 10) + (push v 20) + (push v 30) + (let [dv (as-dyn v)] + (print dv) + (print "\n") + ;; Write through the view, read through the typed side. + (set (at dv 1) 999) + (print (at v 1)) + (print "\n") + ;; Write through the typed side, read through the view. + (set (at v 2) 777) + (print (at dv 2)) + (print "\n") + ;; Grow through the view. flan_vec_grow reallocates v's backing + ;; storage and overwrites v's own header in place, which is the + ;; same header the view points at — so the typed side, asked + ;; afterwards, already agrees with the push it never made itself. + (push dv 40) + (print (len v)) + (print "\n") + (print (at v 3)) + (print "\n")) + ;; A fixed array's view: nothing here can grow, so a snapshot taken + ;; once at the crossing is sound — there is no move to go stale over. + (set (at a 0) 1) + (set (at a 1) 2) + (set (at a 2) 3) + (set (at a 3) 4) + (let [da (as-dyn a)] + (print da) + (print "\n") + (set (at da 0) 100) + (print (at a 0)) + (print "\n") + (set (at a 3) 400) + (print (at da 3)) + (print "\n")) + ;; A slice's view, over f64 elements, and a bool Vec's view — the + ;; other two of the three element kinds a view can hold. The slice + ;; is cut directly from the global at the call, which is what keeps + ;; its trace back to permanent storage visible to the checker. + (set (at a2 0) 1.5) + (set (at a2 1) 2.5) + (set (at a2 2) 3.5) + (let [ds (as-dyn (slice a2 0 3))] + (print ds) + (print "\n") + (set (at ds 0) 9.5) + (print (at a2 0)) + (print "\n")) + (push bv true) + (push bv false) + (let [db (as-dyn bv)] + (print db) + (print "\n") + (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. + (do (push v 1) + (let [dv (as-dyn v)] + (print (at dv 5))) + 0) + (= n 2) + ;; Wrong type on write: a text where the view holds i64. Tag-checked + ;; and refused, never coerced and never silently stored. + (do (push v 1) + (let [dv (as-dyn v)] + (set (at dv 0) "nope")) + 0) + :else (do (println "?") 1)))) diff --git a/test/test_acceptance.ml b/test/test_acceptance.ml index 33b02f7..6037878 100644 --- a/test/test_acceptance.ml +++ b/test/test_acceptance.ml @@ -3737,6 +3737,59 @@ level "1" some_nil ~opt:"-O0" (); some_nil ~x86:true (); + (* ── 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, 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. *) + let dyn_view_out = + "[ 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\ + [ 111 222]\n3\n333\n" + in + let dyn_view ?opt ?x86 () = + let exe = compile ?opt ?x86 "programs/dyn-view.flan" in + let name suffix = + "dyn: a typed container's view" ^ suffix + ^ (match opt with Some o -> ", " ^ o | None -> "") + ^ (match x86 with Some true -> ", --x86" | _ -> "") + in + let code, text = run exe (Some "0") in + if code <> 0 || text <> dyn_view_out then begin + incr failures; + Printf.printf + "FAIL %s\n got: %S (exit %d)\n wanted: %S (exit 0)\n" + (name "") text code dyn_view_out + end; + let code, text = run exe (Some "1") in + if code <> 134 || not (contains text "index 5 is out of bounds") + then begin + incr failures; + Printf.printf + "FAIL %s\n got: %S (exit %d)\n wanted a range trap \ + (exit 134)\n" (name ", out of range") text code + end; + let code, text = run exe (Some "2") in + if code <> 134 || not (contains text "this view's elements are int") + then begin + incr failures; + Printf.printf + "FAIL %s\n got: %S (exit %d)\n wanted a tag-check \ + trap (exit 134)\n" (name ", wrong-type write") text code + end; + (try Sys.remove exe with Sys_error _ -> ()) + in + dyn_view (); + dyn_view ~opt:"-O0" (); + dyn_view ~x86:true (); + (* The root count, which is the part of this feature the runs above cannot check — and the reason has outlived the stub it was first written about. flan_dyn.c's trigger has a one-megabyte floor, and not one @@ -3810,7 +3863,7 @@ level "1" [ "programs/dyn-basic.flan"; "programs/dyn-vec.flan"; "programs/dyn-struct.flan"; "programs/dyn-global.flan"; "programs/dyn-boundary.flan"; - "programs/dyn-defer.flan"; + "programs/dyn-defer.flan"; "programs/dyn-view.flan"; (* Included for the same reason every dyn program is, though this check cannot see the slot M2 item 4 actually added: [%dx]/[%ax] are the pool-ran-dry fallback for a temporary [root_plan] COUNTED diff --git a/test/test_dyn.ml b/test/test_dyn.ml index 394cb83..a5c4fa1 100644 --- a/test/test_dyn.ml +++ b/test/test_dyn.ml @@ -20,11 +20,25 @@ nested a chain of vecs sixty-four deep, traced through one root sharing one object held three times — written through one path and read through another, and swept once when the last goes + view M2 item 3: a typed container's view, driven directly over a + hand-built flan_vec header and a plain C array — the runtime + half of "typed containers into dyn as views", with no + compiler in the loop. Also carries the view-aware equality + review's third finding asked for: two views, a view against + a heap vec, equal contents and differing ones + layout the three restatements of flan_vec's layout — flan_rt.c's + real one, flan_dyn.c's mirror, and this file's [hand_vec] — + compared field by field, which is what turns a struct any one + of the three reorders into a FAIL line here instead of a + silent corruption at whichever view next reads through it refuse:* twenty-four refusals, one process each, asserted on the sentence as well as on the status: a process that died some other way is not the guard firing, and the exit code cannot tell them apart + refuseview:* five more refusals, the view's own: out of range and a + mismatched write on each of the three element kinds, and a + push against a flat (slice or array) view - One binary, built once, run twenty-nine times. The build is the expensive + One binary, built once, run thirty-six times. The build is the expensive part and the runs are milliseconds, which is what keeps this inside `dune test` rather than behind an alias. *) @@ -133,6 +147,30 @@ let () = fail "interior sharing\n got: %S (exit %d)\n wanted: %S" out code want_sh; + (* M2 item 3, the runtime's half: a flat view over a fixed C array (reads + box, writes tag-check, and a write through the view is the array's own + write and vice versa — proving it is a view and not a copy), a Vec + view over a hand-built header, pushed through twenty times so the + header's own [ptr] moves under it — the case that says the descriptor + pointing AT the header rather than snapshotting it is what survives a + growth — a bool view and a float view, so the element dispatch is + exercised on all three kinds dyn_ops.c's [view] carries, and + [dyn_equal] made view-aware: two views over equal bytes, two views + over different bytes, a view against an equal heap vec and against a + differing one. *) + let code, out, err = run "view" in + if code <> 0 || out <> "view ok\n" then + fail "a typed container's view\n got: %S (exit %d, err %S)" + out code err; + + (* The three restatements of flan_vec's layout, compared field by field — + see dyn_ops.c's [layout] and [hand_vec]'s comment for what ties them + together and why nothing at compile time otherwise does. *) + let code, out, err = run "layout" in + if code <> 0 || out <> "layout ok\n" then + fail "flan_vec's three restatements\n got: %S (exit %d, err %S)" + out code err; + (* Every refusal. The pair is (mode, a phrase the sentence must contain); the phrase is chosen to be the part that says *which* mistake it was, so a message that named the wrong operation or the wrong tag would not @@ -176,11 +214,34 @@ let () = fail "%s did not say %S; it said %S" mode phrase err) refusals; + (* The view's own refusals: an index outside it, a write whose dyn tag + does not match the element the view holds — once per element kind, so + the tag-check is asserted on int, on float and on bool separately and + not only on the one this file happens to build first — and a push + against a flat (slice or array) view, which cannot grow by + construction and says so rather than corrupting whatever follows it + in memory. *) + let view_refusals = + [ ("range", "index 2 is out of bounds for vec of length 2"); + ("wrongwrite", "this view's elements are int"); + ("wrongbool", "this view's elements are bool"); + ("wrongfloat", "this view's elements are float"); + ("flatpush", "this view is a slice or an array and cannot grow") ] + in + List.iter + (fun (mode, phrase) -> + let code, out, err = run ("refuseview:" ^ mode) in + if code = 0 then + fail "%s returned rather than trapping: %S" mode out + else if not (has err phrase) then + fail "%s did not say %S; it said %S" mode phrase err) + view_refusals; + (try Sys.remove exe with Sys_error _ -> ()); (* A line on the way out, because a test that says nothing when it passes is a test nobody can tell from a test that did not run. *) if !failures = 0 then - Printf.printf " ok the dyn runtime: %d refusals and six runs\n" - (List.length refusals) + Printf.printf " ok the dyn runtime: %d refusals and eight runs\n" + (List.length refusals + List.length view_refusals) else exit 1 | _ -> print_endline "SKIP test_dyn: no clang" diff --git a/test/test_flan.ml b/test/test_flan.ml index 9846fd8..857c050 100644 --- a/test/test_flan.ml +++ b/test/test_flan.ml @@ -945,15 +945,135 @@ let () = rejects_check "a parameter named after a type" "(defn f [i64 x] ())" ~needle:"cannot also be this parameter's name"; - (* The three "not yet" refusals, each by name and each for its own reason. - - A typed container does not box: [(Vec i64)] has a representation the dyn - runtime cannot walk, and the heterogeneous container at this milestone is - the runtime's own from [(vec-new dyn)]. *) - rejects_check "a typed container boxed into dyn" + (* M2 item 3 lifted the container-into-dyn refusal: a [(Vec T)], a slice or + a fixed array with an i64/f64/bool element now crosses as a VIEW rather + than refusing — but only when its storage is permanent, a global's, + which review added after the first landing: a view's descriptor chases + the container's own address on every operation, and a container whose + address dies with a frame is exactly the dangling dyn value the dynamic + side refuses to hand back. Every accepting row below views a global. A + [(Map K V)] still refuses regardless of storage — it rides a + representation this milestone does not give a view — and so does any + container whose element is outside the three the view can hold. *) + accepts "a typed Vec boxed into dyn is a view, not a refusal" + "(defvar v (Vec i64) (vec-new i64))\n\ + (defn take [d dyn] i32 1)\n\ + (defn main [] i32 (take v))"; + accepts "a slice boxed into dyn is a view" + "(defvar xs [3 i64])\n\ + (defn take [d dyn] i32 1)\n\ + (defn main [] i32 (take (slice xs 0 3)))"; + accepts "a fixed array boxed into dyn is a view" + "(defvar a [4 i64])\n\ + (defn take [d dyn] i32 1)\n\ + (defn main [] i32 (take a))"; + accepts "a bool Vec's view" + "(defvar v (Vec bool) (vec-new bool))\n\ + (defn take [d dyn] i32 1)\n\ + (defn main [] i32 (take v))"; + accepts "an f64 Vec's view" + "(defvar v (Vec f64) (vec-new f64))\n\ + (defn take [d dyn] i32 1)\n\ + (defn main [] i32 (take v))"; + (* The element restriction is still refused, and by name: a string element + would need a dyn string's own boxing, whose payload is a pointer into + the collector's heap, planted where nothing will ever trace it. *) + rejects_check "a Vec of strings does not view into dyn yet" + "(defvar v (Vec string) (vec-new string))\n\ + (defn take [d dyn] i32 1)\n\ + (defn main [] i32 (take v))" + ~needle:"does not cross into dyn yet"; + rejects_check "an i32 element is not one of the view's three" + "(defvar v (Vec i32) (vec-new i32))\n\ + (defn take [d dyn] i32 1)\n\ + (defn main [] i32 (take v))" + ~needle:"does not cross into dyn yet"; + (* A typed (Map K V) is unrelated to item 3 and keeps its own refusal. *) + rejects_check "a typed Map still refuses into dyn" + "(defvar m (Map i64 i64) (map-new i64 i64))\n\ + (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 + indexed" or some other accident of which path noticed. *) + rejects_check "a local Vec does not view into dyn — its frame ends" "(defn take [d dyn] i32 1)\n\ (defn main [] i32 (let [v (vec-new i64)] (take v)))" - ~needle:"does not cross into dyn yet"; + ~needle:"does not cross into dyn as a view here"; + rejects_check "a Vec parameter does not view into dyn" + "(defn take [d dyn] i32 1)\n\ + (defn give [v (Vec i64)] i32 (take v))\n\ + (defn main [] i32 0)" + ~needle:"does not cross into dyn as a view here"; + rejects_check "a fixed array local does not view into dyn" + "(defn take [d dyn] i32 1)\n\ + (defn main [] i32 (let [a (array 4 i64)] (take a)))" + ~needle:"does not cross into dyn as a view here"; + (* A slice cut from a global is permanent; the same slice expression + rebound to a local first loses the trace back to it and is refused — + conservative rather than wrong, and the message says what does work. *) + accepts "a slice cut from a global inline is still permanent" + "(defvar xs [3 i64])\n\ + (defn take [d dyn] i32 1)\n\ + (defn main [] i32 (take (slice xs 0 3)))"; + rejects_check "a slice rebound to a local loses the trace and is refused" + "(defvar xs [3 i64])\n\ + (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 demand for an array at the level being + indexed 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"; + (* [(at g i j)] is ONE typed node holding both indices, not two nested + ones, so a guard that reads the target's type alone sees level zero and + nothing after it. These two rows pin the multi-index spelling on both + sides: every level an array is permanent, and a slice at ANY level is + not — including the second, which the one-level guard accepted and + which then printed a dead frame's contents with exit 0. *) + accepts "an element of a global array of arrays is permanent" + "(defvar rows [2 [3 (Vec i64)]])\n\ + (defn take [d dyn] i32 1)\n\ + (defn main [] i32 (take (at rows 0 1)))"; + rejects_check "an element reached through a slice level is not permanent" + "(defvar g [2 [[3 i64]]])\n\ + (defn take [d dyn] i32 1)\n\ + (defn main [] i32 (take (at g 0 1)))" + ~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. *) + rejects_check "a Vec behind a Ptr does not view into dyn" + "(defn take [d dyn] i32 1)\n\ + (defn use [p (Ptr (Vec i64))] i32 (take (deref p)))\n\ + (defn main [] i32 0)" + ~needle:"does not cross into dyn as a view here"; (* A bracket *literal* is not a typed container yet, and where a dyn is wanted it builds the runtime's own vec instead — the lowering the map literal's values ride on, and what makes {:xs [1 2]} mean what it diff --git a/test/test_sanitize.ml b/test/test_sanitize.ml index dab72f8..22ce7eb 100644 --- a/test/test_sanitize.ml +++ b/test/test_sanitize.ml @@ -213,6 +213,17 @@ let corpus = ASan's build being asked to trap the same way the plain build does. *) "programs/nil-option.flan", []; "programs/some-nil.flan", []; + (* M2 item 3: a typed container's view. Mode 0, the survey — the modes + that trap are exercised as C refusals in test_dyn.ml's [refuseview:*] + instead, the same split [bounds.flan]'s "0" argument makes above. A + view's storage is a plain array or a Vec's own malloc block, neither + one this collector allocates, so there is nothing here for ASan to + catch that the runtime tests above did not already exercise directly + — this row is about the *compiler* lane: the address the checker + hands the runtime at the crossing, and whether a push through the + view that grows and moves the Vec leaves anything for ASan's + use-after-free detection to find. *) + "programs/dyn-view.flan", [ "0" ]; "../spike/x86/p13-dyn-collect.flan", []; "programs/sand-headless.flan", []; "programs/signedness.flan", [];