Joseph Ferano
c765aad70f
(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.
152 lines
6.5 KiB
Plaintext
152 lines
6.5 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 — 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))))
|