Joseph Ferano
9ce51ba94e
as-slice was a warning, not an operation. The input type already decides which of the two things happens — a Vec can only be borrowed, an array or a string can only be viewed, and no call site picks between them — so the second name expressed no choice a reader could make. And it warned at the moment the view is taken, which is the one moment nothing is wrong; the danger arrives later, at the push. slice now takes a Vec at all three arities and as-slice is gone. (slice v lo) was free, and is the arity the Vec never had: the runtime already reads a hi of -1 as "to the end", so the tail form passes the caller's lo and the same -1 — no slot, no length read, no second evaluation. The merge is entirely in the checker; the Vec path builds the flan_vec_as_slice call it always built and neither backend has a line about any of it. A Vec a call returned is refused at every arity, and not for the array's reason. (slice (mk)) over an array dangles. (slice (make-vec)) does not — the storage outlives the expression — but the header is a temporary, so nothing can ever free the block. The refusal says that and names the let. The name's own refusal sits in ordinary_call after every table, so a program that defines an as-slice still reaches its own. It reads for somebody who has never heard of the old name and writes the call back out, spelling each argument that is a name or a number. The warning moved to where it bites: BUILT.md gains a section beside the Vec table and the push row points at it, spec-memory.md's Borrowing says the same. Investigated and deliberately not built — a diagnostic for a live view at the push. (reserve v 100) then a slice, a push and a read is correct code under the contract the spec chose, so any flag on it is a false positive by the language's own semantics rather than by an approximation. FIX.org has the finding and the syntactic sketch that does not work.
59 lines
2.2 KiB
Plaintext
59 lines
2.2 KiB
Plaintext
;;;; A global of move-only type, which is allowed, and the one rule that makes
|
|
;;;; it allowed: reading a global Vec is always a borrow and never a move. The
|
|
;;;; lifetime question ownership tracking exists to answer has a constant
|
|
;;;; answer here — the process's — so nothing may take the global and nothing
|
|
;;;; may free it, and with no owner to hand over there is no double free to
|
|
;;;; catch. The refusals that enforce that are in test_flan.ml.
|
|
;;;;
|
|
;;;; A zeroed Vec is a real empty Vec, so the global starts as one and is
|
|
;;;; loaded by whoever loads it. What this program pins is that the loading
|
|
;;;; happens once and survives: [entry] is called twice, the way a re-entered
|
|
;;;; main would be, and the second call finds the data the first one left.
|
|
(defonce the-data (Vec u8))
|
|
(defonce counts (Map u8 i64))
|
|
|
|
;; Reading it here is a borrow. So is reading it in [total] below, which is the
|
|
;; case the old rule could not express: two functions holding the same global
|
|
;; at once is fine exactly because neither of them can free it.
|
|
(defn loaded? [] bool (> (len the-data) 0))
|
|
|
|
(defn load [] ()
|
|
(when (not (loaded?))
|
|
(set the-data (vec-new u8))
|
|
(dotimes [i 5] (push the-data (u8 (* i 3))))))
|
|
|
|
(defn total [] i64
|
|
(let [s (i64 0)]
|
|
(dotimes [i (len the-data)] (set s (+ s (i64 (at the-data i)))))
|
|
s))
|
|
|
|
;; Mutating in place, through the global rather than through a copy of it. The
|
|
;; aliasing contract is the one every Vec has (spec-memory.md, "Borrowing"): a
|
|
;; push may reallocate and invalidate a slice taken before it, and that is the
|
|
;; programmer's, here as much as for a local.
|
|
(defn bump [] ()
|
|
(set (at the-data 0) (+ (at the-data 0) 1))
|
|
(push the-data 100))
|
|
|
|
(defn entry [] ()
|
|
(load)
|
|
(bump)
|
|
(put counts 1 (total))
|
|
(println (len the-data))
|
|
(println (total))
|
|
(match (get counts 1) (Some v) (println v) None (println "?")))
|
|
|
|
(defn main [] i32
|
|
(entry)
|
|
;; The second run. Nothing re-initialises the global between them, so the
|
|
;; length keeps climbing and the loaded data is the same block it was.
|
|
(entry)
|
|
(println (len (slice the-data)))
|
|
;; A copy is the one thing something else may own, and freeing that copy
|
|
;; leaves the global untouched.
|
|
(let [c (clone the-data)]
|
|
(println (len c))
|
|
(free c))
|
|
(println (len the-data))
|
|
0)
|