Joseph Ferano
3f7c42257f
Relocation was proved sound and stayed sound — a Vec view holding the header's own address survives a push that grows and moves it, because there is no snapshot to invalidate. That was never the whole of the hazard. Refusing every container into dyn outright, before this lane, meant a dangling view was unreachable; the moment box stopped refusing, three routes opened at once — a view returned from the function whose frame the Vec lived in, one stashed in a dyn global and read after that frame is gone, and one left behind when a condition transfer unwinds it. All three are stack-use-after-return, reachable for the first time. The rule: a typed container crosses into dyn as a view only when its own storage is permanent — a global's. On the dynamic side Flan follows Clojure and Common Lisp, where holding a value can never hand you garbage; treating a view as a bare pointer and calling the lifetime the programmer's problem is the Odin answer, and it is the wrong trade on this side of the language. check.ml's permanent_root walks the checked expression back to its root: a global is permanent, a field or an array element of one is permanent at the same fixed offset, and a slice cut directly from one at the call site inherits it — the trace is what a slice carries, and it is lost the moment the slice is bound to a name first, so that case is refused too rather than guessed at. Everything else answers false: a local, a parameter, a temporary, and anything reached through a (Ptr T), because a heap-durable pointer and a frame's own are the same type and the checker cannot tell them apart — admitting one admits the other, which is the whole hazard this closes. An arena-held header turns out not to be a separate case at all: an arena changes where a Vec's elements live, never where its own header — the binding — lives, so it is already covered by the storage-class check above. Both directions of the F1 escape were reproduced before the fix (a genuine ASan stack-use-after-return, reproduced by building the pre-fix tree) and confirmed refused at check time after it, for all three routes. Three more findings, all in the runtime rather than the boundary: view_vec_check, on finding a stale container, rendered the very view it had just declared unsafe to read — which called back into the same check, unconditionally, an infinite recursion rather than the intended trap. Fixed by never rendering the container in the stale message at all; the sentence names the two epochs and nothing else, which is everything a reader needs and the one thing that was safe to read. dyn_equal's VEC arm read x->len and x->u.v.items regardless of kind, which for a view answers 0 and the union's other member reinterpreted as dyn words: 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, silently. vecish_len and vecish_at read either shape correctly and the arm now goes through them. obj_words gets the same explicit OBJ_VIEW case on the same reasoning, unreachable today only because mark_push's own gate already excludes the kind — this is the belt next to that brace. The three restatements of flan_vec's layout — flan_rt.c's real struct, flan_dyn.c's mirror, and dyn_ops.c's hand-built one — had a comment claiming a reorder would not compile or link, which was never true of a void*-typed forward declaration. flan_vec_layout and flan_dyn_vec_hdr_layout each report their struct's size and field offsets; dyn_ops.c's new "layout" mode compares both against offsetof on its own hand_vec, so a disagreement is a FAIL line in dune test instead of a silent corruption at whichever view reads through the wrong offset next. Also: the survey program's comment excusing a by-value parameter's view as "value semantics, not a hole" was wrong on its own terms — a write through such a view does reach the caller's storage, only growth diverges — but the question is moot now: every container the program views is a global, and the file was rewritten around that rather than patched. And an i32 element does not cross into a view either, but the refusal used to say why in words that were true only of a string element; it now says what i32 actually is and what the restriction is actually for. Rebased onto dev-loop's item-4 landing (221df5a).
124 lines
5.0 KiB
Plaintext
124 lines
5.0 KiB
Plaintext
;;;; 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. test_flan.ml's checker tests carry the refusal side of this
|
|
;;;; (a local Vec, a Vec parameter, a Vec behind a Ptr, a slice rebound to a
|
|
;;;; local); this program is the acceptance side, over storage the guard
|
|
;;;; allows.
|
|
;;;;
|
|
;;;; 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))
|
|
|
|
(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"))
|
|
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))))
|