From c765aad70f952e888226129b62505207f724482c Mon Sep 17 00:00:00 2001 From: Joseph Ferano Date: Sun, 20 Sep 2026 10:49:10 +0700 Subject: [PATCH] A slice level after the first index was invisible to the lifetime rule (at g i j) is one Tast node carrying the whole index list, so the At arm's guard on target.ty settled level zero and nothing after it. A global [2 [[3 i64]]] indexed twice reached a slice's element, crossed into dyn as a view, and printed a returned frame's contents with exit 0 (ASan: stack-use-after-scope in view_box). The arm now steps each index the way [indexed] does and demands an array at every level; the Field and Slice arms inherit the fix by recursing into it. --- FIX.org | 4 +++- lib/check.ml | 37 ++++++++++++++++++++++++++----------- test/programs/dyn-view.flan | 11 +++++++---- test/test_flan.ml | 21 ++++++++++++++++++--- 4 files changed, 54 insertions(+), 19 deletions(-) diff --git a/FIX.org b/FIX.org index dd09153..91d7cdd 100644 --- a/FIX.org +++ b/FIX.org @@ -449,7 +449,9 @@ rename. typed-flan branch freezes the static language pre-dyn. [permanent_root] in check.ml decides it: a global, a field of one, an element of a permanent ARRAY (an element of a slice is NOT — a slice holds only ptr+len, and what they point at can be a frame already gone; the [At] - arm checks the target's type for exactly this), or + 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 diff --git a/lib/check.ml b/lib/check.ml index 0786a21..7016408 100644 --- a/lib/check.ml +++ b/lib/check.ml @@ -1508,11 +1508,15 @@ let view_not_yet loc (container : Types.t) (elem : Types.t) = 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, and the - [At] arm below checks the target's type for exactly that reason: a slice - is ptr+len, so a global [[T]] holds only the two words, and the storage - they point at can be a frame that has already gone. That distinction is - the whole of the arm's guard. A slice built directly from + 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 @@ -1537,10 +1541,20 @@ 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 :: _) -> - (match target.Tast.ty with - | Types.Array _ -> permanent_root target - | _ -> false) + | 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 @@ -1551,8 +1565,9 @@ let view_not_permanent loc (container : Types.t) = it is a view of, no more and no less. A global's storage does outlive \ it: (defvar g %s ...) viewed from anywhere reads storage fixed for the \ process, and so does a field or an array element of one. A local, a \ - parameter, a temporary, an element of a slice — even a global slice, \ - which holds only ptr+len and can point at a frame that is gone — or \ + 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" diff --git a/test/programs/dyn-view.flan b/test/programs/dyn-view.flan index e70af64..14b013e 100644 --- a/test/programs/dyn-view.flan +++ b/test/programs/dyn-view.flan @@ -16,10 +16,13 @@ ;;;; process — as is a field of one, and an ELEMENT of one when the global ;;;; is an array, whose elements sit inside its own storage. An element of a ;;;; global SLICE is not: the slice is ptr+len and says nothing about where -;;;; the data is. test_flan.ml's checker tests carry the refusal side of -;;;; this (a local Vec, a Vec parameter, a Vec behind a Ptr, a slice rebound -;;;; to a local, an element of a global slice); this program is the -;;;; acceptance side, over storage the guard allows. +;;;; 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 diff --git a/test/test_flan.ml b/test/test_flan.ml index 968210e..7652e7e 100644 --- a/test/test_flan.ml +++ b/test/test_flan.ml @@ -968,9 +968,9 @@ let () = not — a global [[T]] holds ptr+len and nothing more, and what they point at may be a frame that has already returned. The refusal row below is one word different from the acceptance row above it, which is - the point: it is the [At] arm's guard on the target's type and nothing - else deciding. Before that guard the refusal row compiled and - segfaulted with no diagnostic at all. *) + 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\ @@ -980,6 +980,21 @@ let () = (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. *)