diff --git a/FIX.org b/FIX.org index b379cb7..3e52a03 100644 --- a/FIX.org +++ b/FIX.org @@ -420,7 +420,22 @@ 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. 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 df6400b..ec640e3 100644 --- a/lib/check.ml +++ b/lib/check.ml @@ -1441,6 +1441,39 @@ 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 — a %s 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 write through the view could plant a \ + pointer where nothing will ever trace it" + (Types.to_string elem)) + 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 +1498,35 @@ 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]. *) + | Types.Vec elem -> + (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) + | Types.Slice elem -> + (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) + | Types.Array (n, elem) -> + (match view_elem elem with + | Some k -> + 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) + | 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 +2135,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 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 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 049fbc4..c0b4a24 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 @@ -3387,6 +3396,8 @@ declare i32 @flan_dyn_need_bool(i64) ; builtin. declare i32 @flan_dyn_is_nil(i64) declare i64 @flan_dyn_need_not_nil(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 2594ed2..294bf5e 100644 --- a/runtime/flan_dyn.c +++ b/runtime/flan_dyn.c @@ -55,6 +55,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 +136,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 +179,32 @@ 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; + +/* 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,6 +220,15 @@ 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; @@ -309,7 +359,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 +457,13 @@ 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_dyn v, 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); + static void render(flan_dyn v, int depth, int nested) { char buf[64]; int32_t t = flan_dyn_tag(v); @@ -461,11 +522,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", v, 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 +618,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", v, 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; } } @@ -1255,9 +1329,128 @@ 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. */ +static void view_vec_check(const char *op, flan_dyn v, 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) { + char sv[SAY_MAX]; + say(sv, SAY_MAX, v); + 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 " + "— %s\n", + op, (long long)h->epoch, (long long)(int64_t)a->epoch, sv); + 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_dyn v, 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, v, 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); } + } +} + +/* 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", v, o)); + return flan_dyn_from_i64(o->len); + } trap1(TYPE_TRAP, "len", "only a text, a vec or a map has one", v); } @@ -1280,6 +1473,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", v, 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]; @@ -1288,13 +1487,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", v, 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; } @@ -1307,6 +1513,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 60c7208..329705e 100644 --- a/runtime/flan_dyn.h +++ b/runtime/flan_dyn.h @@ -145,6 +145,60 @@ uint8_t flan_dyn_need_bool(flan_dyn v); int32_t flan_dyn_is_nil(flan_dyn v); flan_dyn flan_dyn_need_not_nil(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: a local's slot, a global, a + * field, fixed for as long as the Vec exists. 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 diff --git a/test/dyn_ops.c b/test/dyn_ops.c index a9a1749..ca25ab2 100644 --- a/test/dyn_ops.c +++ b/test/dyn_ops.c @@ -32,6 +32,8 @@ #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); static int failures; @@ -347,6 +349,123 @@ 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 this file is exactly the mechanism that makes a + * disagreement a compile or link error rather than a silent corruption: + * there is no [flan_vec_init] to call from here (flan_rt.c is not linked + * against this main), so the header is built by hand, the same five words + * [flan_vec_grow] would leave behind after a few pushes. */ +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]"); + + /* 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 collector ─────────────────────────────────────────────────────*/ /* Allocate a great many, hold a few, and assert the heap does not grow. The @@ -734,7 +853,15 @@ 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 (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..fe59f65 --- /dev/null +++ b/test/programs/dyn-view.flan @@ -0,0 +1,111 @@ +;;;; 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. (Boxing a value AFTER passing it through an +;;;; ordinary by-value parameter would view that parameter's own copy instead +;;;; — value semantics, not a hole in this feature — so every view here is +;;;; taken where the container already lives.) +;;;; +;;;; 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 +;;;; last one 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. +;;;; +;;;; 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) + +(defn main [args [string]] i32 + (let [n (i32 (bytes->i64 (bytes (at args 1))))] + (cond + (= n 0) + (do + ;; A (Vec i64) view. + (let [v (vec-new i64)] + (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. + (let [a (array 4 i64)] + (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. + (let [a2 (array 3 f64)] + (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"))) + (let [bv (vec-new bool)] + (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"))) + 0) + (= n 1) + ;; Out of range. The runtime's own message names the length. + (do (let [v (vec-new i64)] + (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 (let [v (vec-new i64)] + (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 778396c..9b30e50 100644 --- a/test/test_acceptance.ml +++ b/test/test_acceptance.ml @@ -3699,6 +3699,57 @@ 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 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 + 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" + 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 @@ -3772,7 +3823,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..0969a9c 100644 --- a/test/test_dyn.ml +++ b/test/test_dyn.ml @@ -20,11 +20,18 @@ 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 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-five 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 +140,19 @@ 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), and 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. And a bool view and a float view, so the element dispatch is + exercised on all three kinds dyn_ops.c's [view] carries. *) + 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; + (* 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 +196,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 seven 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 d9174ec..db6e3b0 100644 --- a/test/test_flan.ml +++ b/test/test_flan.ml @@ -874,14 +874,41 @@ 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. A [(Map K V)] still refuses — it rides a different + 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" "(defn take [d dyn] i32 1)\n\ - (defn main [] i32 (let [v (vec-new i64)] (take v)))" + (defn main [] i32 (let [v (vec-new i64)] (take v)))"; + accepts "a slice boxed into dyn is a view" + "(defn take [d dyn] i32 1)\n\ + (defn main [] i32 (let [xs (array 3 i64)] (take (slice xs 0 3))))"; + accepts "a fixed array boxed into dyn is a view" + "(defn take [d dyn] i32 1)\n\ + (defn main [] i32 (let [a (array 4 i64)] (take a)))"; + accepts "a bool Vec's view" + "(defn take [d dyn] i32 1)\n\ + (defn main [] i32 (let [v (vec-new bool)] (take v)))"; + accepts "an f64 Vec's view" + "(defn take [d dyn] i32 1)\n\ + (defn main [] i32 (let [v (vec-new f64)] (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" + "(defn take [d dyn] i32 1)\n\ + (defn main [] i32 (let [v (vec-new string)] (take v)))" + ~needle:"does not cross into dyn yet"; + rejects_check "an i32 element is not one of the view's three" + "(defn take [d dyn] i32 1)\n\ + (defn main [] i32 (let [v (vec-new 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" + "(defn take [d dyn] i32 1)\n\ + (defn main [] i32 (let [m (map-new i64 i64)] (take m)))" ~needle:"does not cross into dyn yet"; (* 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 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", [];