Pool and Handle leave the language: two containers are enough, and a slab is a Vec you free less often
This commit is contained in:
parent
9d73900f3e
commit
c46fd56447
328
lib/check.ml
328
lib/check.ml
@ -425,7 +425,7 @@ let predicate_names = [ "ordered?"; "equal?"; "hashable?"; "numeric?"; "copyable
|
||||
this element type has to be built against a region allocator — see
|
||||
[region_only] below and [flan_alloc_region_only] in the runtime. That is a
|
||||
question about *release*, so it is asked of every arm a release would have
|
||||
to reach and would not: a Vec, Map or Pool owns a block outright; an Option,
|
||||
to reach and would not: a Vec or Map owns a block outright; an Option,
|
||||
a fixed array, a struct or a data type's case owns whatever its payload
|
||||
does.
|
||||
|
||||
@ -454,7 +454,7 @@ let owning_fields env n =
|
||||
|
||||
let rec owning env ?(seen = []) (t : Types.t) =
|
||||
match t with
|
||||
| Types.Vec _ | Types.Map _ | Types.Pool _ -> true
|
||||
| Types.Vec _ | Types.Map _ -> true
|
||||
| Types.Option e | Types.Array (_, e) -> owning env ~seen e
|
||||
| Types.Named n ->
|
||||
not (List.mem n seen)
|
||||
@ -471,7 +471,7 @@ let rec owning env ?(seen = []) (t : Types.t) =
|
||||
value is the whole of the question there. *)
|
||||
let region_only env (t : Types.t) =
|
||||
match t with
|
||||
| Types.Vec e | Types.Pool e -> owning env e
|
||||
| Types.Vec e -> owning env e
|
||||
| Types.Map (_, v) -> owning env v
|
||||
| _ -> false
|
||||
|
||||
@ -528,7 +528,7 @@ let tyvar_of (t : Types.t) = match t with Types.Var v -> Some v | _ -> None
|
||||
|
||||
In the body this means a generic may not use a parameter twice without
|
||||
declaring [copyable?]. Since the repeal this gates the structural rules
|
||||
only — what a struct, union or pool may own — not any use of a binding.
|
||||
only — what a struct or union may own — not any use of a binding.
|
||||
|
||||
A [Var] only ever survives the abstract pass. Inside an instantiation
|
||||
[env.subst] has made everything concrete, so this is [Types.is_move_only]
|
||||
@ -664,27 +664,6 @@ let rec resolve env ?(seen = []) (t : Ast.texpr) : Types.t =
|
||||
(resolve env ~seen v)
|
||||
| "Map", _ -> fail loc "(Map K V) takes exactly two types"
|
||||
| "Result", _ -> unimplemented loc "(Result T E)" 6
|
||||
| "Pool", [ a ] ->
|
||||
let e = resolve env ~seen a in
|
||||
(* Lifted with the Vec's and pushed to the construction with it, and a
|
||||
pool is the one of the three where that is not quite the same trade,
|
||||
because a pool has a release point a Vec does not: [(release p h)]
|
||||
recycles one slot while the pool lives on. In a region that costs a
|
||||
block that stays allocated until [free-all] and is never handed back
|
||||
— the slot itself is reused, since the next insert overwrites those
|
||||
bytes, but whatever the dead element pointed at is stranded.
|
||||
|
||||
That is a region leak bounded by the region, which is the bargain a
|
||||
region already is: an arena's whole proposition is that nothing comes
|
||||
back before the reset. It is not the unbounded leak the heap would
|
||||
take, and it is not a use-after-free — nothing is released twice
|
||||
because nothing is released once. Said here rather than left for a
|
||||
reader to work out, because "reuse" is the word that makes a pool
|
||||
look different from a Vec and it deserves an answer. *)
|
||||
Types.Pool e
|
||||
| "Pool", _ -> fail loc "(Pool T) takes exactly one type"
|
||||
| "Handle", [ a ] -> Types.Handle (resolve env ~seen a)
|
||||
| "Handle", _ -> fail loc "(Handle T) takes exactly one type"
|
||||
| _ ->
|
||||
fail loc
|
||||
"%s takes no type arguments — generics are milestone 5" name)
|
||||
@ -857,8 +836,6 @@ let rec bind_ty subst (pat : Types.t) (arg : Types.t) =
|
||||
| Types.Slice p, Types.Slice a
|
||||
| Types.Ptr p, Types.Ptr a
|
||||
| Types.Vec p, Types.Vec a
|
||||
| Types.Pool p, Types.Pool a
|
||||
| Types.Handle p, Types.Handle a
|
||||
| Types.Option p, Types.Option a -> bind_ty subst p a
|
||||
| Types.Array (n, p), Types.Array (m, a) -> Int64.equal n m && bind_ty subst p a
|
||||
| Types.Map (k, v), Types.Map (k', v') ->
|
||||
@ -878,8 +855,6 @@ let rec subst_ty subst (t : Types.t) =
|
||||
| Types.Map (k, v) -> Types.Map (subst_ty subst k, subst_ty subst v)
|
||||
| Types.Ptr e -> Types.Ptr (subst_ty subst e)
|
||||
| Types.Vec e -> Types.Vec (subst_ty subst e)
|
||||
| Types.Pool e -> Types.Pool (subst_ty subst e)
|
||||
| Types.Handle e -> Types.Handle (subst_ty subst e)
|
||||
| Types.Option e -> Types.Option (subst_ty subst e)
|
||||
| Types.Fn (ps, r) -> Types.Fn (List.map (subst_ty subst) ps, subst_ty subst r)
|
||||
| t -> t
|
||||
@ -889,7 +864,7 @@ let rec generic_ty (t : Types.t) =
|
||||
match t with
|
||||
| Types.Var _ -> true
|
||||
| Types.Slice e | Types.Array (_, e) | Types.Ptr e | Types.Vec e
|
||||
| Types.Pool e | Types.Handle e | Types.Option e -> generic_ty e
|
||||
| Types.Option e -> generic_ty e
|
||||
| Types.Map (k, v) -> generic_ty k || generic_ty v
|
||||
| Types.Fn (ps, r) -> List.exists generic_ty ps || generic_ty r
|
||||
| _ -> false
|
||||
@ -933,8 +908,6 @@ let rec mangle_ty (t : Types.t) =
|
||||
| Types.Map (k, v) -> Printf.sprintf "map-%s-%s" (mangle_ty k) (mangle_ty v)
|
||||
| Types.Ptr e -> "ptr-" ^ mangle_ty e
|
||||
| Types.Vec e -> "vec-" ^ mangle_ty e
|
||||
| Types.Pool e -> "pool-" ^ mangle_ty e
|
||||
| Types.Handle e -> "handle-" ^ mangle_ty e
|
||||
| Types.Option e -> "opt-" ^ mangle_ty e
|
||||
| Types.Fn (ps, r) ->
|
||||
Printf.sprintf "fn-%s-to-%s"
|
||||
@ -972,7 +945,7 @@ let rec occurs_in ~needle (t : Types.t) =
|
||||
||
|
||||
match t with
|
||||
| Types.Slice e | Types.Array (_, e) | Types.Ptr e | Types.Vec e
|
||||
| Types.Pool e | Types.Handle e | Types.Option e -> occurs_in ~needle e
|
||||
| Types.Option e -> occurs_in ~needle e
|
||||
| Types.Map (k, v) -> occurs_in ~needle k || occurs_in ~needle v
|
||||
| Types.Fn (ps, r) ->
|
||||
List.exists (occurs_in ~needle) ps || occurs_in ~needle r
|
||||
@ -1251,7 +1224,6 @@ let region_sym (t : Types.t) =
|
||||
match t with
|
||||
| Types.Vec _ -> "flan_vec_region_only"
|
||||
| Types.Map _ -> "flan_map_region_only"
|
||||
| Types.Pool _ -> "flan_pool_region_only"
|
||||
| _ -> assert false
|
||||
|
||||
let region_check env loc (target : Tast.expr) (after : Tast.expr) =
|
||||
@ -1974,7 +1946,7 @@ and var ctx loc ~want name =
|
||||
|
||||
(* What remains of spec-memory.md's ownership section after the repeal of
|
||||
2026-09-18 is entirely in the types: move-only decides what may be copied,
|
||||
the struct/union/pool rules below decide what may own what, and the
|
||||
the struct/union rules below decide what may own what, and the
|
||||
allocator's capability decides what a free means at run time. Which frees
|
||||
run, and in what order, is the program's own business — the same contract
|
||||
Odin ships with — and the dev build's generation words are the net under
|
||||
@ -3398,42 +3370,6 @@ and map_new_types ctx ~want loc args =
|
||||
"nothing here says what (map-new) maps — write the key and value \
|
||||
types, as (map-new string i32), or give the binding a type")
|
||||
|
||||
(* The element type for [pool-new]. The same rule [vec-new] uses and for the
|
||||
same reason: a [let] has no type annotation, so a local pool has nowhere
|
||||
else to say what it holds. *)
|
||||
and pool_new_elem ctx ~want loc args =
|
||||
let named =
|
||||
match args with
|
||||
| { Ast.e = Ast.Var n; _ } :: rest
|
||||
when lookup ctx n = None
|
||||
&& (not (Hashtbl.mem ctx.env.globals n))
|
||||
&& type_named ctx n ->
|
||||
Some (resolve_name ctx.env ~seen:[] loc n, rest)
|
||||
| _ -> None
|
||||
in
|
||||
match named with
|
||||
| Some (t, rest) ->
|
||||
if move_only ctx.env.tvpreds t then
|
||||
fail loc
|
||||
"(Pool %s) holds a move-only element, and the type-erased runtime \
|
||||
copies and releases slots bytewise. Recursive teardown arrives with \
|
||||
drop (step 5 in NEXT.md)"
|
||||
(Types.to_string t);
|
||||
t, rest
|
||||
| None ->
|
||||
(match want with
|
||||
| Some (Types.Pool t) -> t, args
|
||||
| _ ->
|
||||
fail loc
|
||||
"nothing here says what (pool-new) is a Pool of — write the element \
|
||||
type, as (pool-new Enemy), or give the binding a type")
|
||||
|
||||
(* The element type, or the reason this is not a Pool. *)
|
||||
and pool_elem loc what (t : Types.t) =
|
||||
match t with
|
||||
| Types.Pool e -> e
|
||||
| other -> fail loc "%s takes a (Pool T), found %s" what (Types.to_string other)
|
||||
|
||||
(* The element type, or the reason this is not a Vec. *)
|
||||
and vec_elem loc what (t : Types.t) =
|
||||
match t with
|
||||
@ -3955,7 +3891,7 @@ and named_call ctx ~want loc name args =
|
||||
container is region-allocated or it does not exist, so there is always a
|
||||
[free-all] to point at. *)
|
||||
(match target.Tast.ty with
|
||||
| (Types.Vec _ | Types.Map _ | Types.Pool _)
|
||||
| (Types.Vec _ | Types.Map _)
|
||||
when region_only ctx.env target.Tast.ty ->
|
||||
fail loc
|
||||
"%s holds elements that own storage, and free releases the block \
|
||||
@ -3973,20 +3909,6 @@ and named_call ctx ~want loc name args =
|
||||
expect loc ~want
|
||||
(rt loc Types.Unit "flan_map_free"
|
||||
[ target; size_of loc k; size_of loc v; here loc ])
|
||||
(* The owner, not a slot. Every handle into it is stale afterwards and
|
||||
answers None, which is a strictly better afterlife than a Vec's
|
||||
binding gets — that one is a compile error and this one is a run-time
|
||||
answer, because handles are copies and the checker cannot see them
|
||||
all. That asymmetry is the reason handles exist. *)
|
||||
| Types.Pool elem ->
|
||||
expect loc ~want
|
||||
(rt loc Types.Unit "flan_pool_free"
|
||||
[ target; size_of loc elem; align_of loc elem; here loc ])
|
||||
| Types.Handle _ ->
|
||||
fail loc
|
||||
"free takes the owner, and a handle owns nothing — it is a copyable \
|
||||
number, so consuming one copy would say nothing about the others. \
|
||||
(release p h) recycles one slot; (free p) releases the pool"
|
||||
| other ->
|
||||
(* A field is never freed on its own: it would leave its owner partly
|
||||
dead with no way to say so. *)
|
||||
@ -4064,18 +3986,6 @@ and named_call ctx ~want loc name args =
|
||||
(mk loc mty (Tast.Local d))
|
||||
[ size_of loc k; size_of loc v ] mty);
|
||||
mk loc mty (Tast.Local d) ])))
|
||||
(* Refused by name rather than falling through to "clone takes a
|
||||
(Vec T)". Copying a pool would duplicate every slot *and* every
|
||||
generation counter, so a handle into the original would resolve in
|
||||
the copy too — two live entities behind one identity, which is the
|
||||
exact confusion the type exists to prevent. If a program wants a
|
||||
second world it builds one and inserts into it, and the new handles
|
||||
say they are new. *)
|
||||
| Types.Pool _ ->
|
||||
fail loc
|
||||
"a pool cannot be cloned: the copy would carry the same slot \
|
||||
generations, so one handle would resolve in both and name two \
|
||||
different things. Build a second pool and insert into it"
|
||||
| _ ->
|
||||
let elem = vec_elem loc "clone" target.Tast.ty in
|
||||
let d = fresh_slot ctx (Types.Vec elem) in
|
||||
@ -4095,219 +4005,6 @@ and named_call ctx ~want loc name args =
|
||||
mk loc (Types.Vec elem) (Tast.Local d) ]))))
|
||||
| _ -> fail loc "clone is (clone v) or (clone v allocator)")
|
||||
|
||||
(* ── (Pool T) and (Handle T), spec-memory.md ───────────────────── *)
|
||||
(* The same type-erased shape the Vec has, for the same reason: size_of and
|
||||
align_of are produced here because here is where the concrete element
|
||||
type is known, and nothing below the call site has ever heard of it. *)
|
||||
|
||||
(* (pool-new), (pool-new T), (pool-new a), (pool-new T a). *)
|
||||
| "pool-new" ->
|
||||
let elem, args = pool_new_elem ctx ~want loc args in
|
||||
let a = allocator_arg ctx loc args in
|
||||
let pty = Types.Pool elem in
|
||||
let p = fresh_slot ctx pty in
|
||||
(* [flan_pool_init] cannot fail — a pool with no slots allocates nothing —
|
||||
but it goes under the guard anyway, so that the day it does allocate
|
||||
the site is already the one that signals. *)
|
||||
let attempt =
|
||||
rt loc (Types.Int Types.I8) "flan_pool_init"
|
||||
[ mk loc pty (Tast.Local p); a; size_of loc elem; align_of loc elem;
|
||||
here loc ]
|
||||
in
|
||||
expect loc ~want
|
||||
(mk loc pty
|
||||
(Tast.Let ([ (p, mk loc pty (Tast.Zero pty)) ],
|
||||
[ with_note loc (alloc_guard ctx loc attempt)
|
||||
(reg_note loc "flan_dev_reg_note_pool"
|
||||
(mk loc pty (Tast.Local p))
|
||||
[ size_of loc elem ] elem);
|
||||
region_check ctx.env loc (mk loc pty (Tast.Local p))
|
||||
(mk loc pty (Tast.Local p)) ])))
|
||||
|
||||
(* (insert p x) -> (Handle T). The handle is the *only* way back to what was
|
||||
inserted: a pool hands out no index and no pointer, because an index does
|
||||
not notice a reuse and that is the entire point. *)
|
||||
| "insert" ->
|
||||
arity loc name 2 args;
|
||||
(match args with
|
||||
| [ target; x ] ->
|
||||
let target = check ctx target in
|
||||
let elem = pool_elem loc "insert" target.Tast.ty in
|
||||
let x = check ctx ~want:elem x in
|
||||
let hty = Types.Handle elem in
|
||||
(* The element is bound before the loop so that a [retry] re-attempts
|
||||
the allocation and not the expression that produced the value —
|
||||
[push]'s rule, and for the same reason. *)
|
||||
let e = fresh_slot ctx elem in
|
||||
let h = fresh_slot ctx hty in
|
||||
let attempt =
|
||||
rt loc (Types.Int Types.I8) "flan_pool_insert"
|
||||
[ target; addr_of loc (mk loc elem (Tast.Local e));
|
||||
addr_of loc (mk loc hty (Tast.Local h));
|
||||
size_of loc elem; align_of loc elem; here loc ]
|
||||
in
|
||||
expect loc ~want
|
||||
(mk loc hty
|
||||
(Tast.Let ([ (e, x); (h, mk loc hty (Tast.Zero hty)) ],
|
||||
[ region_check ctx.env loc target
|
||||
(with_note loc (alloc_guard ctx loc attempt)
|
||||
(reg_note loc "flan_dev_reg_note_pool" target
|
||||
[ size_of loc elem ] elem));
|
||||
mk loc hty (Tast.Local h) ])))
|
||||
| _ -> assert false)
|
||||
|
||||
(* (resolve p h) -> (Option (Ptr T)).
|
||||
|
||||
A pointer and not a value, and spec-memory.md settles it rather than this
|
||||
lane guessing: its worked example under "Mutating something you matched"
|
||||
is written out as (Option (Ptr Enemy)), for the reason stated a line
|
||||
above it — "pattern bindings bind values, so a matched struct is a copy",
|
||||
and a copy cannot be written back. Mutating the pooled thing in place is
|
||||
what a pool is for, so (Option T) would answer a question nobody asked.
|
||||
|
||||
An [Option] rather than a trap because the whole thesis is that a stale
|
||||
reference *reports* — the same shape (get m k) has, and for the same
|
||||
reason: absence is an answer, not a failure.
|
||||
|
||||
The hole, said plainly: the (Ptr T) is invalidated by any [insert] that
|
||||
grows the pool, exactly as a slice is invalidated by a [push]. The handle
|
||||
survives that and the pointer does not. It is spec-memory.md's explicit
|
||||
Zig/Odin contract one level down, and it is worth naming because it is
|
||||
the silent-wrong-answer mode the handle just removed, reintroduced for
|
||||
anyone who keeps the pointer across an insert. Chunked never-moving
|
||||
storage is the fix and it costs code; taking the contract is the smaller
|
||||
correct thing, given [as-slice] already established it. *)
|
||||
| "resolve" ->
|
||||
arity loc name 2 args;
|
||||
(match args with
|
||||
| [ target; h ] ->
|
||||
let target = check ctx target in
|
||||
let elem = pool_elem loc "resolve" target.Tast.ty in
|
||||
let h = check ctx ~want:(Types.Handle elem) h in
|
||||
(match h.Tast.ty with
|
||||
| Types.Handle e when Types.equal e elem -> ()
|
||||
| other ->
|
||||
fail loc "resolve takes a (Handle %s), found %s"
|
||||
(Types.to_string elem) (Types.to_string other));
|
||||
let pty = Types.Ptr elem in
|
||||
let oty = Types.Option pty in
|
||||
let out = fresh_slot ctx pty in
|
||||
let got =
|
||||
rt loc pty "flan_pool_resolve"
|
||||
[ target; h; size_of loc elem; here loc ]
|
||||
in
|
||||
(* The runtime answers a pointer or NULL and the Option is built here,
|
||||
which is [get]'s arrangement: the runtime has no idea what an
|
||||
Option's layout is, and keeping it that way is what lets one entry
|
||||
point serve every element type. *)
|
||||
let cond =
|
||||
mk loc Types.Bool
|
||||
(Tast.Prim (Tast.Ne,
|
||||
[ mk loc (Types.Int Types.I64)
|
||||
(Tast.Prim (Tast.Cast (Types.Int Types.I64),
|
||||
[ mk loc pty (Tast.Local out) ]));
|
||||
mk loc (Types.Int Types.I64) (Tast.Int (0L, Types.I64)) ]))
|
||||
in
|
||||
let some = mk loc oty (Tast.Some_ (mk loc pty (Tast.Local out))) in
|
||||
let none = mk loc oty Tast.None_ in
|
||||
expect loc ~want
|
||||
(mk loc oty
|
||||
(Tast.Let ([ (out, got) ],
|
||||
[ mk loc oty (Tast.If (cond, some, none)) ])))
|
||||
| _ -> assert false)
|
||||
|
||||
(* (release p h) -> bool: true if this call released it, false if the handle
|
||||
was already gone.
|
||||
|
||||
This is how a pooled value dies, and it is not [free]. [free] consumes
|
||||
its argument as a move, and a handle is a copyable number that owns
|
||||
nothing — consuming one copy would say nothing about the others. The pool
|
||||
is the owner, so the release operation is on the pool and takes the
|
||||
handle as an ordinary argument. spec-memory.md's two release points are
|
||||
untouched: (free p) is release point 1 applied to the owner, and a
|
||||
free-all of the region takes the pool with everything else. This is a
|
||||
third thing and it is not a release point — it recycles a slot inside
|
||||
storage the pool still owns.
|
||||
|
||||
It answers a bool rather than () because the generational scheme makes a
|
||||
double release *detectable*, which is worth handing to the caller: this
|
||||
is the one place in the language where freeing something twice is an
|
||||
answer instead of a refusal. *)
|
||||
| "release" ->
|
||||
arity loc name 2 args;
|
||||
(match args with
|
||||
| [ target; h ] ->
|
||||
let target = check ctx target in
|
||||
let elem = pool_elem loc "release" target.Tast.ty in
|
||||
let h = check ctx ~want:(Types.Handle elem) h in
|
||||
(match h.Tast.ty with
|
||||
| Types.Handle e when Types.equal e elem -> ()
|
||||
| other ->
|
||||
fail loc "release takes a (Handle %s), found %s"
|
||||
(Types.to_string elem) (Types.to_string other));
|
||||
let got = rt loc (Types.Int Types.I8) "flan_pool_release"
|
||||
[ target; h; here loc ] in
|
||||
expect loc ~want
|
||||
(mk loc Types.Bool
|
||||
(Tast.Prim (Tast.Ne,
|
||||
[ got;
|
||||
mk loc (Types.Int Types.I8) (Tast.Int (0L, Types.I8)) ])))
|
||||
| _ -> assert false)
|
||||
|
||||
(* (live p) — how many slots are live now. (len p) is the *slot high-water*,
|
||||
which is deliberately the other number: 0..(len p) are the indices
|
||||
(pool-handle p i) accepts, so a loop bounded by [len] visits every live
|
||||
entry. Bounding it by the live count instead would silently skip entries
|
||||
the moment anything had been released, which is precisely the kind of
|
||||
quiet wrong answer this whole type exists to remove. *)
|
||||
| "live" ->
|
||||
arity loc name 1 args;
|
||||
let target = check ctx (List.hd args) in
|
||||
ignore (pool_elem loc "live" target.Tast.ty);
|
||||
let n = rt loc (Types.Int Types.I64) "flan_pool_live" [ target; here loc ] in
|
||||
expect loc ~want (mk loc index_ty (Tast.Prim (Tast.Cast index_ty, [ n ])))
|
||||
|
||||
(* (pool-handle p i) -> (Option (Handle T)): the handle of slot [i], or None
|
||||
if that slot is dead. This plus (len p) is the whole of iteration, and
|
||||
iteration is not a convenience — migrate-instances has to *enumerate*
|
||||
live instances, and a pool behind generational handles gives that by
|
||||
construction where a world arena and an owned region do not. It is the
|
||||
reason plan.org's three storage strategies are not a free choice.
|
||||
|
||||
An index out of 0..(len p) traps, exactly as (at v i) traps: an index is
|
||||
an index here, and answering None for one would hide a bug rather than a
|
||||
death. *)
|
||||
| "pool-handle" ->
|
||||
arity loc name 2 args;
|
||||
(match args with
|
||||
| [ target; i ] ->
|
||||
let target = check ctx target in
|
||||
let elem = pool_elem loc "pool-handle" target.Tast.ty in
|
||||
let i = check ctx ~want:index_ty i in
|
||||
let hty = Types.Handle elem in
|
||||
let oty = Types.Option hty in
|
||||
let out = fresh_slot ctx hty in
|
||||
let got = rt loc hty "flan_pool_handle" [ target; i; here loc ] in
|
||||
(* 0 is the never-valid handle — generation 0 is even, and a live slot's
|
||||
generation is odd — so the runtime says "dead" with it and needs no
|
||||
second return value. *)
|
||||
let cond =
|
||||
mk loc Types.Bool
|
||||
(Tast.Prim (Tast.Ne,
|
||||
[ mk loc (Types.Int Types.I64)
|
||||
(Tast.Prim (Tast.Cast (Types.Int Types.I64),
|
||||
[ mk loc hty (Tast.Local out) ]));
|
||||
mk loc (Types.Int Types.I64) (Tast.Int (0L, Types.I64)) ]))
|
||||
in
|
||||
expect loc ~want
|
||||
(mk loc oty
|
||||
(Tast.Let ([ (out, got) ],
|
||||
[ mk loc oty
|
||||
(Tast.If (cond,
|
||||
mk loc oty (Tast.Some_ (mk loc hty (Tast.Local out))),
|
||||
mk loc oty Tast.None_)) ])))
|
||||
| _ -> assert false)
|
||||
|
||||
(* ── (Map K V), spec-memory.md ─────────────────────────────────── *)
|
||||
(* Every one of these is a named call over the same type-erased runtime the
|
||||
Vec uses, with the two sizes and the key's hash and equality pair produced
|
||||
@ -4816,16 +4513,9 @@ and named_call ctx ~want loc name args =
|
||||
| Types.Map _ ->
|
||||
let n = rt loc (Types.Int Types.I64) "flan_map_len" [ a; here loc ] in
|
||||
expect loc ~want (mk loc index_ty (Tast.Prim (Tast.Cast index_ty, [ n ])))
|
||||
(* A pool's [len] is its slot high-water, not its live count, so that
|
||||
0..(len p) stays the range of valid indices the way it is for every
|
||||
other container here. (live p) is the other number. *)
|
||||
| Types.Pool _ ->
|
||||
let n = rt loc (Types.Int Types.I64) "flan_pool_len" [ a; here loc ] in
|
||||
expect loc ~want (mk loc index_ty (Tast.Prim (Tast.Cast index_ty, [ n ])))
|
||||
| other ->
|
||||
fail loc
|
||||
"len takes an array, a slice, a string, a Vec, a Map or a Pool, \
|
||||
found %s"
|
||||
"len takes an array, a slice, a string, a Vec or a Map, found %s"
|
||||
(Types.to_string other))
|
||||
| "at" ->
|
||||
(match args with
|
||||
|
||||
@ -1462,11 +1462,10 @@ let reg_at t ~addr : (reg_entry option, string) result =
|
||||
anywhere, so nothing can fall behind [Types.to_string].
|
||||
|
||||
And it is allowed to fail, which matters more than it looks. Not every
|
||||
recorded name is a type: [flan_rt.c] notes a pool's slot headers as
|
||||
"pool slots", because after a free-all an address landing in them must not
|
||||
come back as an element. That string is not Flan source and must not
|
||||
become one — so a name that does not resolve is refused with the name
|
||||
quoted, and never defaulted to bytes. *)
|
||||
recorded name need be a type this session can spell — a note's name is
|
||||
whatever string the noting site chose, not Flan source — so a name that
|
||||
does not resolve is refused with the name quoted, and never defaulted to
|
||||
bytes. *)
|
||||
let type_of_spelling t spelling : (Types.t, string) result =
|
||||
let refuse why =
|
||||
Error
|
||||
|
||||
56
lib/emit.ml
56
lib/emit.ml
@ -124,15 +124,6 @@ let rec ll (t : Types.t) =
|
||||
map's address — so the shape exists only so that a slot, a struct field
|
||||
and a copy in the IR are the right number of bytes. *)
|
||||
| Types.Map _ -> "%map"
|
||||
(* items + slots + len + cap + live + free + allocator + epoch. Nothing here
|
||||
reads a field of one either — every operation is a runtime call taking
|
||||
the pool's address. *)
|
||||
| Types.Pool _ -> "%pool"
|
||||
(* A handle is one 64-bit number: the slot index in the low half and that
|
||||
slot's generation in the high half. Packed rather than a two-field struct
|
||||
so that copying, zeroing and [=] are what they are for an integer, with no
|
||||
backend arm anywhere except the one comparison below. *)
|
||||
| Types.Handle _ -> "i64"
|
||||
| Types.Option e -> Printf.sprintf "{ i8, %s }" (ll e)
|
||||
| Types.Var _ ->
|
||||
(* The checker rejects it by name — nothing reaches here. *)
|
||||
@ -297,8 +288,6 @@ let rec lay m (t : Types.t) : int * int =
|
||||
| Types.Alloc -> 8, 8
|
||||
| Types.Fn _ -> 8, 8
|
||||
| Types.Vec _ | Types.Map _ -> 48, 8
|
||||
| Types.Pool _ -> 64, 8
|
||||
| Types.Handle _ -> 8, 8
|
||||
(* [n x T] adds no padding of its own: T's size already carries its tail. *)
|
||||
| Types.Array (n, e) -> let s, a = lay m e in Int64.to_int n * s, a
|
||||
| Types.Option e -> let s, a, _ = lay_fields m [ Types.Int Types.I8; e ] in s, a
|
||||
@ -543,19 +532,6 @@ let rec dty m d (t : Types.t) : int =
|
||||
("allocator", Types.Alloc); ("gen", Types.Int Types.I64);
|
||||
("epoch", Types.Int Types.I64) ]
|
||||
|> fun n -> ignore k; ignore v; n
|
||||
(* Eight fields, shown as eight, for the reason the two above are. *)
|
||||
| Types.Pool e ->
|
||||
composite (Types.to_string t)
|
||||
[ ("items", Types.Ptr e);
|
||||
("slots", Types.Ptr (Types.Int Types.U8));
|
||||
("len", Types.Int Types.I64); ("cap", Types.Int Types.I64);
|
||||
("live", Types.Int Types.I64); ("free", Types.Int Types.I64);
|
||||
("allocator", Types.Alloc); ("epoch", Types.Int Types.I64) ]
|
||||
(* An i64 under lldb, which is what it is. Splitting it into a two-field
|
||||
composite would be describing a struct that is not there: the packing
|
||||
is the runtime's, and [p h] answering with the number is honest. *)
|
||||
| Types.Handle _ ->
|
||||
basic (Types.to_string t) 64 "DW_ATE_unsigned"
|
||||
(* A pointer to code, and lldb is told exactly that and no more. DWARF
|
||||
has DW_TAG_subroutine_type for the signature behind it, and spelling
|
||||
one out here would buy a reader nothing they cannot get from the
|
||||
@ -2043,11 +2019,6 @@ and prim f (e : Tast.expr) (p : Tast.prim) (args : Tast.expr list) =
|
||||
location. Signed, because a member may be declared negative. *)
|
||||
| Types.Enum _ ->
|
||||
ins f "%s = icmp %s %s %s, %s" t (icmp_op true p) (ll x.Tast.ty) a b
|
||||
(* [Types.is_equatable] admits a handle and [is_comparable] does not, so
|
||||
only [Eq]/[Ne] arrive here — one unsigned integer compare over the
|
||||
packed (index, generation) pair. *)
|
||||
| Types.Handle _ ->
|
||||
ins f "%s = icmp %s i64 %s, %s" t (icmp_op false p) a b
|
||||
| t' -> failwith ("comparison on " ^ Types.to_string t'));
|
||||
t
|
||||
| (Tast.BitAnd | Tast.BitOr | Tast.BitXor | Tast.Shl | Tast.Shr), [ x; y ] ->
|
||||
@ -2254,7 +2225,7 @@ and prim f (e : Tast.expr) (p : Tast.prim) (args : Tast.expr list) =
|
||||
lets an operation mutate the caller's container in place.
|
||||
Passing the header by value here would hand the runtime a
|
||||
copy to grow and leave the caller's untouched. *)
|
||||
| Types.Vec _ | Types.Map _ | Types.Pool _ -> [ "ptr " ^ addr f a ]
|
||||
| Types.Vec _ | Types.Map _ -> [ "ptr " ^ addr f a ]
|
||||
| t -> [ ll t ^ " " ^ value f a ])
|
||||
args)
|
||||
in
|
||||
@ -2325,11 +2296,6 @@ and cast f ~guard (x : Tast.expr) target =
|
||||
let concrete (t : Types.t) =
|
||||
match t with
|
||||
| Types.Enum _ -> Types.Int Types.I32
|
||||
(* A handle already *is* an i64 — see [ll] — so a cast involving one
|
||||
changes the reading and never the bits. [pool-handle] tests one against
|
||||
the never-valid zero, and the renderer splits one into its index and
|
||||
its generation. Unsigned, because both halves are. *)
|
||||
| Types.Handle _ -> Types.Int Types.U64
|
||||
| t -> t
|
||||
in
|
||||
let src = concrete x.Tast.ty and target = concrete target in
|
||||
@ -2360,7 +2326,7 @@ and cast f ~guard (x : Tast.expr) target =
|
||||
it, both sides being [ptr]. *)
|
||||
| Types.Ptr _, Types.Ptr _ -> "bitcast"
|
||||
(* Also not written in the surface language. [resolve] needs it: the
|
||||
pool answers a pointer or NULL and the Option is built in the
|
||||
runtime answers a pointer or NULL and the Option is built in the
|
||||
checker, so the null test is one integer compare on the address. *)
|
||||
| Types.Ptr _, Types.Int Types.I64 -> "ptrtoint"
|
||||
| _ -> failwith "unsupported cast"
|
||||
@ -2707,10 +2673,6 @@ let header = {|; Generated by flan. The layout is C's: no object headers anywher
|
||||
; nor value type appears in it, for the same reason: one type-erased runtime,
|
||||
; handed the two sizes and a hash/equality pair at each call site.
|
||||
%map = type { ptr, i64, i64, ptr, i64, i64 }
|
||||
; (Pool T) — slab storage handed out behind (Handle T). Type-erased in exactly
|
||||
; the same way; the element type is nowhere in it. items and slots are grown
|
||||
; together and share one cap, so a slot index is an index into both.
|
||||
%pool = type { ptr, ptr, i64, i64, i64, i64, ptr, i64 }
|
||||
; A handler frame: the one it displaced, the condition type it matches, and
|
||||
; the lifted function that runs. Allocated on the establishing frame's stack.
|
||||
%handler = type { ptr, i32, ptr }
|
||||
@ -2775,7 +2737,6 @@ declare void @flan_arena_destroy(ptr)
|
||||
declare void @flan_alloc_free_all(ptr, ptr, i64)
|
||||
declare void @flan_vec_region_only(ptr, ptr, i64)
|
||||
declare void @flan_map_region_only(ptr, ptr, i64)
|
||||
declare void @flan_pool_region_only(ptr, ptr, i64)
|
||||
declare i8 @flan_alloc_can_free(ptr)
|
||||
declare i8 @flan_alloc_can_free_all(ptr)
|
||||
declare i64 @flan_alloc_epoch(ptr)
|
||||
@ -2788,7 +2749,6 @@ declare i64 @flan_alloc_budget(ptr)
|
||||
declare void @flan_alloc_set_budget(ptr, i64)
|
||||
declare void @flan_dev_reg_enable()
|
||||
declare void @flan_dev_reg_note_vec(ptr, i64, ptr, i64)
|
||||
declare void @flan_dev_reg_note_pool(ptr, i64, ptr, i64)
|
||||
declare void @flan_dev_reg_note_map(ptr, i64, i64, ptr, i64)
|
||||
declare i8 @flan_vec_init(ptr, ptr, i64, i64, i64, ptr, i64)
|
||||
declare i8 @flan_vec_reserve(ptr, i64, i64, i64, ptr, i64)
|
||||
@ -2801,18 +2761,6 @@ declare i64 @flan_vec_len(ptr, ptr, i64)
|
||||
declare ptr @flan_vec_at(ptr, i32, i64, ptr, i64, ptr)
|
||||
declare void @flan_vec_as_slice(ptr, ptr, i32, i32, i64, ptr, i64, ptr)
|
||||
declare void @flan_vec_free(ptr, i64, i64, ptr, i64)
|
||||
; (Pool T) and (Handle T). A handle crosses as the i64 it is; the pool, like
|
||||
; every other owning container, crosses as its address. [resolve] answers a
|
||||
; pointer or null and [pool-handle] answers a packed handle or the never-valid
|
||||
; zero, so neither needs a second return value.
|
||||
declare i8 @flan_pool_init(ptr, ptr, i64, i64, ptr, i64)
|
||||
declare i8 @flan_pool_insert(ptr, ptr, ptr, i64, i64, ptr, i64)
|
||||
declare ptr @flan_pool_resolve(ptr, i64, i64, ptr, i64)
|
||||
declare i8 @flan_pool_release(ptr, i64, ptr, i64)
|
||||
declare i64 @flan_pool_len(ptr, ptr, i64)
|
||||
declare i64 @flan_pool_live(ptr, ptr, i64)
|
||||
declare i64 @flan_pool_handle(ptr, i32, ptr, i64)
|
||||
declare void @flan_pool_free(ptr, i64, i64, ptr, i64)
|
||||
; (Map K V). The two ptr arguments before the location on put/get/clone are the
|
||||
; hash and equality pair, which the checker emits per key type and passes here
|
||||
; the way Odin hangs them off Map_Info.
|
||||
|
||||
10
lib/js.ml
10
lib/js.ml
@ -116,7 +116,7 @@
|
||||
{1 What is refused, and why each}
|
||||
|
||||
Pointers and [deref], [free], allocators and [with-allocator], [Map],
|
||||
[Pool] and [(Handle T)], [declare-c] and the FFI, [embed], conditions and
|
||||
[declare-c] and the FFI, [embed], conditions and
|
||||
restarts ([signal], [handler-bind], [restart-case], [invoke-restart]), and
|
||||
the type-erased container runtime's own entry points. The first group has
|
||||
no counterpart in a garbage-collected object graph; the FFI and [embed]
|
||||
@ -235,14 +235,6 @@ let rec refuse_ty loc (t : Types.t) =
|
||||
"(Map K V) is not in the JS dialect yet — Odin's open-addressed map is a \
|
||||
type-erased runtime over raw bytes and the JS answer is a Map keyed by \
|
||||
a structural key, which is its own lane"
|
||||
| Types.Pool _ ->
|
||||
at loc
|
||||
"(Pool T) is not in the JS dialect — a pool hands out slot indices into \
|
||||
storage it owns, which is the memory model this dialect leaves behind"
|
||||
| Types.Handle _ ->
|
||||
at loc
|
||||
"(Handle T) is not in the JS dialect — a handle is an index into a Pool, \
|
||||
and there is no Pool here"
|
||||
| Types.Var n ->
|
||||
at loc "a type variable (%s) reached the backend, which cannot happen" n
|
||||
|
||||
|
||||
@ -187,33 +187,6 @@ let rec render c depth (e : Tast.expr) : Tast.expr list =
|
||||
does not own, and the walk is what [as-slice] is for: (print (as-slice
|
||||
v)) prints the elements and says at the call site that it borrowed. *)
|
||||
| Types.Vec _ -> [ lit "<vec>" ]
|
||||
(* Opaque for the reason a Vec is: the slots are storage this function does
|
||||
not own, and a walk over them would print the dead ones too — there is
|
||||
no way to say "dead" inside a rendered element. (pool-handle p i) and
|
||||
(resolve p h) are how a program looks, and they say it. *)
|
||||
| Types.Pool _ -> [ lit "<pool>" ]
|
||||
(* Its identity, which is what spec-memory.md says a handle prints —
|
||||
"Ptr and Handle print their address or identity rather than recursively
|
||||
dereferencing". Shown as index:generation rather than as the packed
|
||||
number, because those are the two things a reader is trying to tell
|
||||
apart when two handles disagree. *)
|
||||
| Types.Handle _ ->
|
||||
let h = cast (Types.Int Types.U64) e in
|
||||
let u64 v = { Tast.e = v; ty = Types.Int Types.U64; loc } in
|
||||
let idx =
|
||||
u64 (Tast.Prim (Tast.BitAnd,
|
||||
[ h; u64 (Tast.Int (0xFFFFFFFFL, Types.U64)) ]))
|
||||
in
|
||||
let gen =
|
||||
u64 (Tast.Prim (Tast.Shr, [ h; u64 (Tast.Int (32L, Types.U64)) ]))
|
||||
in
|
||||
[ do_ [ lit "<handle "; c.emit.eu64 idx; lit ":"; c.emit.eu64 gen;
|
||||
lit ">" ] ]
|
||||
(* A function value is a code address, and printing the address would make
|
||||
an inspection depend on where the image loaded. The signature is what a
|
||||
reader can act on, so that is what is shown — and the inspector reaches
|
||||
every local of a stopped frame, so a frame holding one has to render
|
||||
rather than refuse. *)
|
||||
| Types.Fn _ as ft -> [ lit ("<" ^ Types.to_string ft ^ ">") ]
|
||||
| Types.Option t ->
|
||||
let tag = { Tast.e = Tast.Field (e, 0); ty = Types.Int Types.I8; loc } in
|
||||
|
||||
42
lib/types.ml
42
lib/types.ml
@ -44,25 +44,6 @@ type t =
|
||||
so this is a container without generics — the concrete type is known only
|
||||
at the call site, which is exactly where the two numbers are produced. *)
|
||||
| Vec of t
|
||||
(* [(Pool T)]: slab storage handed out behind [(Handle T)]. Owning and
|
||||
move-only exactly as a [Vec] is, and built on the same type-erased
|
||||
runtime over (size, align). It is not a second [Vec]: a [Vec]'s indices
|
||||
shift when something is removed and a [Pool]'s slot index never moves,
|
||||
which is the whole reason a handle into one stays meaningful. *)
|
||||
| Pool of t
|
||||
(* [(Handle T)]: a reference to something that can die, which reports that
|
||||
it died rather than silently resolving to whatever reused its slot
|
||||
(spec-memory.md, "Borrowing" — "Cross-referencing long-lived objects uses
|
||||
(Handle a) into a pool, never a raw pointer or slice. A stale handle is
|
||||
detectable").
|
||||
|
||||
It is a plain 64-bit number — a slot index in the low 32 bits and that
|
||||
slot's generation counter in the high 32 — so it copies, compares and
|
||||
zeroes like an integer and owns nothing. A zeroed handle is generation 0,
|
||||
and a live slot's generation is always odd, so [Zero] of a handle is a
|
||||
handle that resolves to nothing rather than one that resolves to slot 0.
|
||||
See runtime/flan_rt.c's pool section for the packing. *)
|
||||
| Handle of t
|
||||
| Option of t (* (Option T) *)
|
||||
| Fn of t list * t (* (Fn [T ...] R) *)
|
||||
| Var of string (* a type variable — milestone 5 *)
|
||||
@ -113,8 +94,6 @@ let rec equal a b =
|
||||
| Ptr x, Ptr y -> equal x y
|
||||
| Alloc, Alloc -> true
|
||||
| Vec x, Vec y -> equal x y
|
||||
| Pool x, Pool y -> equal x y
|
||||
| Handle x, Handle y -> equal x y
|
||||
| Option x, Option y -> equal x y
|
||||
| Fn (ps, r), Fn (ps', r') ->
|
||||
List.length ps = List.length ps'
|
||||
@ -137,8 +116,6 @@ let rec to_string = function
|
||||
| Ptr t -> "(Ptr " ^ to_string t ^ ")"
|
||||
| Alloc -> "Allocator"
|
||||
| Vec t -> "(Vec " ^ to_string t ^ ")"
|
||||
| Pool t -> "(Pool " ^ to_string t ^ ")"
|
||||
| Handle t -> "(Handle " ^ to_string t ^ ")"
|
||||
| Option t -> "(Option " ^ to_string t ^ ")"
|
||||
| Fn (ps, r) ->
|
||||
Printf.sprintf "(Fn [%s] %s)"
|
||||
@ -153,10 +130,7 @@ let is_numeric = function Int _ | Float _ -> true | _ -> false
|
||||
[free] needs no analysis of its own. A struct that owns one is move-only
|
||||
too; that arrives with [drop], which is the step after this one. *)
|
||||
let rec is_move_only = function
|
||||
(* A [Pool] owns its storage; a [Handle] into one owns nothing, which is the
|
||||
point of it — handles are copied freely, and the pool is the single
|
||||
owner that [free] applies to. *)
|
||||
| Vec _ | Map _ | Pool _ -> true
|
||||
| Vec _ | Map _ -> true
|
||||
| Option t -> is_move_only t
|
||||
| Array (_, t) -> is_move_only t
|
||||
| _ -> false
|
||||
@ -179,11 +153,6 @@ let rec keyable = function
|
||||
| Float _ -> false (* NaN /= NaN, and 0.0 and -0.0 differ bytewise *)
|
||||
| Array (_, t) -> keyable t
|
||||
| Named _ -> true (* [Check] decides, by walking the fields *)
|
||||
(* A [Handle] is not a map key, for the reason a [Ptr] is not: hashing an
|
||||
identity is a different operation from hashing what it names, and a
|
||||
handle whose slot has been reused hashes the same as it always did while
|
||||
naming nothing. The type exists to make that difference visible, so
|
||||
burying it under a key is the one thing it must not do. *)
|
||||
| _ -> false
|
||||
|
||||
(* Ordering and equality are defined on machine types and on nothing else at
|
||||
@ -191,14 +160,7 @@ let rec keyable = function
|
||||
unconstrained type supports only what every type supports (plan.org, Types). *)
|
||||
let is_comparable = function Enum _ -> true | t -> is_numeric t
|
||||
|
||||
(* [=] and [!=] admit one more type than [<] does. A [Handle] is a pair of
|
||||
numbers in a 64-bit word, so "is this the same entity" is one integer
|
||||
compare and is worth having — two handles are equal exactly when they name
|
||||
the same slot at the same generation, so a stale handle is never equal to
|
||||
the live one that replaced it. Ordering handles would compare a slot index,
|
||||
which means nothing: allocation order is a free-list artefact. Hence two
|
||||
predicates rather than one. *)
|
||||
let is_equatable = function Handle _ -> true | t -> is_comparable t
|
||||
let is_equatable = is_comparable
|
||||
|
||||
(* [Never] is the type of an expression that does not produce a value: return,
|
||||
an early-returning `some`, exit. It fits anywhere, and that is the only
|
||||
|
||||
14
lib/x86.ml
14
lib/x86.ml
@ -461,10 +461,10 @@ let alignof md t = snd (Emit.lay md t)
|
||||
let is_agg (t : Types.t) =
|
||||
match t with
|
||||
| Types.Int _ | Types.Float _ | Types.Bool | Types.Ptr _ | Types.Enum _
|
||||
| Types.Alloc | Types.Handle _ | Types.Fn _ -> false
|
||||
| Types.Alloc | Types.Fn _ -> false
|
||||
| Types.Unit | Types.Never -> false
|
||||
| Types.String | Types.Slice _ | Types.Array _ | Types.Map _ | Types.Vec _
|
||||
| Types.Pool _ | Types.Option _ | Types.Named _ -> true
|
||||
| Types.Option _ | Types.Named _ -> true
|
||||
| Types.Var v -> unsupported "type variable %s" v
|
||||
|
||||
let is_void (t : Types.t) = match t with Types.Unit | Types.Never -> true | _ -> false
|
||||
@ -1300,7 +1300,7 @@ let classify_c (l : loc) (t : Types.t) =
|
||||
match t with
|
||||
| Types.String | Types.Slice _ -> [ Aint (l, Types.Ptr Types.Unit); Alen l ]
|
||||
| Types.Unit | Types.Never -> []
|
||||
| Types.Vec _ | Types.Map _ | Types.Pool _ -> [ Aptr l ]
|
||||
| Types.Vec _ | Types.Map _ -> [ Aptr l ]
|
||||
| _ when is_agg t ->
|
||||
unsupported "aggregate %s across the C boundary" (Types.to_string t)
|
||||
| _ when is_float t -> [ Aflt (l, t) ]
|
||||
@ -2481,7 +2481,7 @@ and call_rt f ~sym ~args ~rty dst =
|
||||
call_native f ~sym ~chan:(rt_signals sym) ~args ~rty dst
|
||||
|
||||
and call_native f ~sym ?(chan = false) ~(args : Tast.expr list) ~rty dst =
|
||||
(* A Vec, a Map and a Pool are move-only and cross to the runtime as their
|
||||
(* A Vec and a Map cross to the runtime as their
|
||||
*address*, which is what lets an operation mutate the caller's container
|
||||
in place. [eval] would hand over the address of a copy, and the runtime
|
||||
would grow that and leave the caller's header at length zero — which is
|
||||
@ -2492,7 +2492,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 _ | Types.Pool _ -> lvalue f a
|
||||
| Types.Vec _ | Types.Map _ -> lvalue f a
|
||||
| _ -> eval f a), a.Tast.ty)
|
||||
args
|
||||
in
|
||||
@ -2515,7 +2515,7 @@ and call_native f ~sym ?(chan = false) ~(args : Tast.expr list) ~rty dst =
|
||||
counter-example and is not: [check.ml] builds it as [rt loc
|
||||
Types.Unit] and [flan_rt.c] writes the two words through [void *out].
|
||||
Every other [rt] builder in the file answers [Unit], an [Int], a
|
||||
[Ptr], an [Alloc] or a [Handle].
|
||||
[Ptr] or an [Alloc].
|
||||
- [crossable], which admits [String] and [Slice _] only as "a
|
||||
parameter" and refuses an aggregate return from a [declare] outright.
|
||||
|
||||
@ -2766,7 +2766,7 @@ and prim f (e : Tast.expr) (p : Tast.prim) (args : Tast.expr list) dst =
|
||||
touched until [call_rt], so answering [()] is already early enough. The
|
||||
test is [emit.ml]'s byte for byte, strict [>] included: bare
|
||||
[flan_dev_reg_note] is the runtime's own entry point and is never a
|
||||
[Tast.Rt]; what [check.ml] builds is the [_vec], [_map] and [_pool]
|
||||
[Tast.Rt]; what [check.ml] builds is the [_vec] and [_map]
|
||||
wrappers, each of which is longer than the prefix. The node's type is
|
||||
[Unit], so there is nothing to store and [dst] is untouched. *)
|
||||
| Tast.Rt sym, _
|
||||
|
||||
@ -1663,284 +1663,6 @@ int8_t flan_vec_clone(flan_vec *dst, flan_vec *src, flan_allocator *a,
|
||||
return 1;
|
||||
}
|
||||
|
||||
/* ── (Pool T) and (Handle T), spec-memory.md ─────────────────────────
|
||||
*
|
||||
* A handle is a reference to something that can die, which reports that it
|
||||
* died rather than silently resolving to whatever reused its slot. That is
|
||||
* the whole design, and every decision below follows from it.
|
||||
*
|
||||
* THE PACKING. A handle is one int64_t: the slot index in the low 32 bits and
|
||||
* that slot's generation counter in the high 32. One word, so it copies,
|
||||
* zeroes and compares like the integer it is, and owns nothing — the pool is
|
||||
* the single owner. 32 bits of index because a Vec's index is an i32 here and
|
||||
* widening indices is one change across every container, not a pool question.
|
||||
*
|
||||
* LIVE IS ODD. A slot's generation starts at 0 and is bumped on every
|
||||
* allocation and on every release, so an odd generation means live and an
|
||||
* even one means dead. Two things fall out of that and both are load-bearing:
|
||||
* a zeroed handle is generation 0, which is even, so it resolves to nothing
|
||||
* rather than to slot 0 — ZII gives a handle field the right meaning for
|
||||
* free; and iteration can ask a slot whether it is live without a second
|
||||
* array or a spare bit.
|
||||
*
|
||||
* WRAPPING RETIRES THE SLOT. 32 bits is 2^31 allocate/release pairs on one
|
||||
* slot — every frame at 60fps for a year and a bit — but "rare" is not an
|
||||
* answer when the failure is the silent wrong one this type exists to
|
||||
* prevent. So a release from generation 0xFFFFFFFF bumps to 0 and does *not*
|
||||
* put the slot back on the free list. The slot is retired: dead forever, its
|
||||
* payload leaked, and no future handle can ever collide with an old one.
|
||||
* Leaking is defined behaviour here (spec-memory.md, "Leaking is defined
|
||||
* behaviour") and one slot is a bounded price for making the collision
|
||||
* unrepresentable rather than unlikely.
|
||||
*
|
||||
* TWO FAILURES, KEPT APART. A stale handle answers "gone" — it is an answer,
|
||||
* not an error. A pool whose allocator was released traps, through the same
|
||||
* epoch check a Vec gets. They answer different questions and must not be
|
||||
* conflated, exactly as the Vec's generation and epoch words must not be.
|
||||
*
|
||||
* GROWTH IS TRANSACTIONAL, and that is not tidiness. spec-memory.md's
|
||||
* StorageExhausted restart re-attempts *the same call*, so a failed grow has
|
||||
* to leave the pool byte for byte as it was — including a cap that still
|
||||
* agrees with the real block sizes, since the next attempt passes cap as the
|
||||
* allocator's old_size. Two blocks grow together, so a resize-in-place of the
|
||||
* first followed by a failure on the second would leave cap describing
|
||||
* neither. Allocate both, copy, then release the old pair: the only state
|
||||
* mutated after the last thing that can fail.
|
||||
*/
|
||||
|
||||
typedef struct flan_pool_slot {
|
||||
uint32_t gen; /* odd: live. even: dead. 0: never allocated, or retired. */
|
||||
int32_t next; /* free-list link, -1 for the end. Meaningless while live. */
|
||||
} flan_pool_slot;
|
||||
|
||||
typedef struct flan_pool {
|
||||
void *items; /* cap payloads, size bytes each */
|
||||
flan_pool_slot *slots; /* cap slot headers, index-parallel with items */
|
||||
int64_t len; /* slot high-water: 0..len have ever been handed out */
|
||||
int64_t cap;
|
||||
int64_t live; /* how many of those are live now */
|
||||
int64_t free; /* head of the free list, -1 when empty */
|
||||
flan_allocator *alloc;
|
||||
int64_t epoch;
|
||||
} flan_pool;
|
||||
|
||||
static int64_t flan_handle_pack(int64_t i, uint32_t gen) {
|
||||
return (int64_t)(((uint64_t)gen << 32) | (uint64_t)(uint32_t)i);
|
||||
}
|
||||
|
||||
static int64_t flan_handle_index(int64_t h) {
|
||||
return (int64_t)(uint32_t)(uint64_t)h;
|
||||
}
|
||||
|
||||
static uint32_t flan_handle_gen(int64_t h) {
|
||||
return (uint32_t)((uint64_t)h >> 32);
|
||||
}
|
||||
|
||||
/* The same epoch check a Vec gets, and for the same reason. A pool that never
|
||||
* allocated has no allocator and nothing to check. */
|
||||
static void flan_pool_check(flan_pool *p, const uint8_t *loc, int64_t loclen) {
|
||||
if (p->alloc) {
|
||||
int64_t now = (int64_t)p->alloc->epoch;
|
||||
if (now != p->epoch) flan_vec_stale_fail(loc, loclen, p->epoch, now);
|
||||
}
|
||||
}
|
||||
|
||||
/* The same guard a Vec gets, at the same place and for the same reason — see
|
||||
* the note above [flan_vec_region_only]. */
|
||||
void flan_pool_region_only(flan_pool *p, const uint8_t *loc, int64_t loclen) {
|
||||
flan_alloc_region_only(p->alloc ? p->alloc : flan_context_allocator(),
|
||||
loc, loclen);
|
||||
}
|
||||
|
||||
static flan_allocator *flan_pool_adopt(flan_pool *p) {
|
||||
if (!p->alloc) {
|
||||
p->alloc = flan_context_allocator();
|
||||
p->epoch = (int64_t)p->alloc->epoch;
|
||||
}
|
||||
return p->alloc;
|
||||
}
|
||||
|
||||
static int8_t flan_pool_grow(flan_pool *p, int64_t want, int64_t size,
|
||||
int64_t align) {
|
||||
flan_allocator *a = flan_pool_adopt(p);
|
||||
int64_t cap = p->cap, sslot = (int64_t)sizeof(flan_pool_slot);
|
||||
int64_t ibytes, sbytes, total;
|
||||
void *ni, *ns;
|
||||
if (want <= cap) return 1;
|
||||
/* Doubling from four, exactly as the Vec grows. */
|
||||
if (cap < 4) cap = 4;
|
||||
while (cap < want) {
|
||||
if (cap > (int64_t)1 << 40) { cap = want; break; }
|
||||
cap *= 2;
|
||||
}
|
||||
/* Two products and their sum, all three checked: the pool asks for the items
|
||||
* and the slots as separate blocks but reports them as one number, and a
|
||||
* wrap in either half is the same memcpy past the end the Vec's is. */
|
||||
if (!flan_mul_bytes(cap, size, &ibytes)
|
||||
|| !flan_mul_bytes(cap, sslot, &sbytes)
|
||||
|| !flan_add_bytes(ibytes, sbytes, &total)) {
|
||||
flan_fail_bytes = FLAN_BYTES_UNREPRESENTABLE;
|
||||
flan_fail_align = align;
|
||||
flan_fail_id = (int64_t)(intptr_t)a;
|
||||
return 0;
|
||||
}
|
||||
flan_fail_bytes = total;
|
||||
flan_fail_align = align;
|
||||
flan_fail_id = (int64_t)(intptr_t)a;
|
||||
ni = a->proc(a, FLAN_ALLOC_ALLOC, NULL, 0, ibytes, align);
|
||||
if (!ni) return 0;
|
||||
ns = a->proc(a, FLAN_ALLOC_ALLOC, NULL, 0, sbytes, 8);
|
||||
if (!ns) {
|
||||
/* An allocator without can-free leaks the first block here. That is the
|
||||
* defined outcome and not a new one: the request failed because the
|
||||
* region is exhausted, and the region is about to be released whole or
|
||||
* the ceiling raised and the call re-attempted. */
|
||||
if (a->caps & FLAN_CAN_FREE)
|
||||
a->proc(a, FLAN_ALLOC_FREE, ni, ibytes, 0, align);
|
||||
return 0;
|
||||
}
|
||||
if (p->len > 0) {
|
||||
memcpy(ni, p->items, (size_t)(p->len * size));
|
||||
memcpy(ns, p->slots, (size_t)(p->len * sslot));
|
||||
}
|
||||
if (p->items && (a->caps & FLAN_CAN_FREE)) {
|
||||
a->proc(a, FLAN_ALLOC_FREE, p->items, p->cap * size, 0, align);
|
||||
a->proc(a, FLAN_ALLOC_FREE, p->slots, p->cap * sslot, 0, 8);
|
||||
}
|
||||
p->items = ni;
|
||||
p->slots = ns;
|
||||
p->cap = cap;
|
||||
return 1;
|
||||
}
|
||||
|
||||
int8_t flan_pool_init(flan_pool *p, flan_allocator *a, int64_t size,
|
||||
int64_t align, const uint8_t *loc, int64_t loclen) {
|
||||
(void)size; (void)align;
|
||||
/* Null for the same reason and with the same answer flan_vec_init gives:
|
||||
* the no-allocator-named case never arrives here as NULL. */
|
||||
if (!a) flan_null_alloc_fail(loc, loclen);
|
||||
p->items = NULL;
|
||||
p->slots = NULL;
|
||||
p->len = 0;
|
||||
p->cap = 0;
|
||||
p->live = 0;
|
||||
p->free = -1;
|
||||
p->alloc = a;
|
||||
p->epoch = (int64_t)a->epoch;
|
||||
return 1;
|
||||
}
|
||||
|
||||
/* 1/0 for "did it fit", like every other allocating entry point. The handle
|
||||
* goes out through [out] rather than being returned, so that the compiler's
|
||||
* alloc_guard reads the answer and the handle separately. */
|
||||
int8_t flan_pool_insert(flan_pool *p, const void *elem, int64_t *out,
|
||||
int64_t size, int64_t align, const uint8_t *loc,
|
||||
int64_t loclen) {
|
||||
int64_t i;
|
||||
flan_pool_check(p, loc, loclen);
|
||||
if (p->free >= 0) {
|
||||
i = p->free;
|
||||
p->free = p->slots[i].next;
|
||||
} else {
|
||||
if (p->len + 1 > p->cap && !flan_pool_grow(p, p->len + 1, size, align))
|
||||
return 0;
|
||||
i = p->len++;
|
||||
p->slots[i].gen = 0;
|
||||
p->slots[i].next = -1;
|
||||
}
|
||||
p->slots[i].gen++; /* even -> odd: this slot is live */
|
||||
p->live++;
|
||||
memcpy((uint8_t *)p->items + i * size, elem, (size_t)size);
|
||||
*out = flan_handle_pack(i, p->slots[i].gen);
|
||||
return 1;
|
||||
}
|
||||
|
||||
/* NULL when the handle names nothing, which the compiler turns into None. The
|
||||
* index is bounded with the unsigned comparison flan_vec_at uses, because the
|
||||
* low half of a handle can be any 32 bits at all. */
|
||||
void *flan_pool_resolve(flan_pool *p, int64_t h, int64_t size,
|
||||
const uint8_t *loc, int64_t loclen) {
|
||||
int64_t i = flan_handle_index(h);
|
||||
uint32_t g = flan_handle_gen(h);
|
||||
flan_pool_check(p, loc, loclen);
|
||||
if (!(g & 1u)) return NULL; /* a zeroed or dead handle */
|
||||
if ((uint64_t)i >= (uint64_t)p->len) return NULL;
|
||||
if (p->slots[i].gen != g) return NULL; /* the slot was reused */
|
||||
return (uint8_t *)p->items + i * size;
|
||||
}
|
||||
|
||||
/* 1 if this call released it, 0 if the handle was already gone. Releasing
|
||||
* twice is therefore an answer rather than undefined behaviour — which is the
|
||||
* generational scheme paying for itself a second time, since a pool is the
|
||||
* one place a double free is *detectable* rather than merely refused. */
|
||||
int8_t flan_pool_release(flan_pool *p, int64_t h, const uint8_t *loc,
|
||||
int64_t loclen) {
|
||||
int64_t i = flan_handle_index(h);
|
||||
uint32_t g = flan_handle_gen(h), was;
|
||||
flan_pool_check(p, loc, loclen);
|
||||
if (!(g & 1u)) return 0;
|
||||
if ((uint64_t)i >= (uint64_t)p->len) return 0;
|
||||
if (p->slots[i].gen != g) return 0;
|
||||
was = p->slots[i].gen;
|
||||
p->slots[i].gen = was + 1; /* odd -> even: dead, and every old handle with it */
|
||||
p->live--;
|
||||
/* The wrap. See the header: the slot is retired rather than reissued. */
|
||||
if (was != 0xFFFFFFFFu) {
|
||||
p->slots[i].next = (int32_t)p->free;
|
||||
p->free = i;
|
||||
}
|
||||
return 1;
|
||||
}
|
||||
|
||||
int64_t flan_pool_len(flan_pool *p, const uint8_t *loc, int64_t loclen) {
|
||||
flan_pool_check(p, loc, loclen);
|
||||
return p->len;
|
||||
}
|
||||
|
||||
int64_t flan_pool_live(flan_pool *p, const uint8_t *loc, int64_t loclen) {
|
||||
flan_pool_check(p, loc, loclen);
|
||||
return p->live;
|
||||
}
|
||||
|
||||
/* The handle of slot [i], or 0 — the never-valid handle — if that slot is
|
||||
* dead. This plus (len p) is the whole of enumeration, which is what
|
||||
* migrate-instances needs and what a Vec behind an index cannot give: a Vec's
|
||||
* indices shift under a removal and a pool's never do. Out of range traps
|
||||
* rather than answering 0, because an index is an index here and 0..len are
|
||||
* the valid ones. */
|
||||
int64_t flan_pool_handle(flan_pool *p, int32_t i, const uint8_t *loc,
|
||||
int64_t loclen) {
|
||||
uint32_t g;
|
||||
flan_pool_check(p, loc, loclen);
|
||||
if ((uint64_t)(int64_t)i >= (uint64_t)p->len)
|
||||
flan_vec_bounds_fail(loc, loclen, (int64_t)i, p->len);
|
||||
g = p->slots[i].gen;
|
||||
if (!(g & 1u)) return 0;
|
||||
return flan_handle_pack((int64_t)i, g);
|
||||
}
|
||||
|
||||
/* spec-memory.md's first release point, applied to the owner. Zeroed rather
|
||||
* than left dangling, for the reason flan_vec_free zeroes. Every handle into
|
||||
* it is stale afterwards and says so: len goes to 0, so the bound check
|
||||
* answers "gone" for all of them. */
|
||||
void flan_pool_free(flan_pool *p, int64_t size, int64_t align,
|
||||
const uint8_t *loc, int64_t loclen) {
|
||||
flan_pool_check(p, loc, loclen);
|
||||
if (p->items && p->alloc && (p->alloc->caps & FLAN_CAN_FREE)) {
|
||||
p->alloc->proc(p->alloc, FLAN_ALLOC_FREE, p->items, p->cap * size, 0, align);
|
||||
p->alloc->proc(p->alloc, FLAN_ALLOC_FREE, p->slots,
|
||||
p->cap * (int64_t)sizeof(flan_pool_slot), 0, 8);
|
||||
}
|
||||
p->items = NULL;
|
||||
p->slots = NULL;
|
||||
p->len = 0;
|
||||
p->cap = 0;
|
||||
p->live = 0;
|
||||
p->free = -1;
|
||||
p->alloc = NULL;
|
||||
p->epoch = 0;
|
||||
}
|
||||
|
||||
/* ── (Map K V), spec-memory.md ──────────────────────────────────────────
|
||||
*
|
||||
* Odin's map, followed deliberately: open-addressed Robin Hood hashing at a
|
||||
@ -2848,9 +2570,8 @@ int8_t flan_map_clone(flan_map *dst, flan_map *src, flan_allocator *a,
|
||||
*
|
||||
* The type name comes from the compiler; the *extent* comes from here, because
|
||||
* the header is the only thing that knows where the storage landed and how
|
||||
* much of it there is. Three entry points rather than one because three
|
||||
* headers are three layouts, and a pool is two blocks that are allocated and
|
||||
* released together but are not adjacent.
|
||||
* much of it there is. Two entry points rather than one because the two
|
||||
* headers are two layouts.
|
||||
*
|
||||
* Each is called immediately after the operation that may have allocated —
|
||||
* every one of them, not only the first — because storage moves. A note is an
|
||||
@ -2865,18 +2586,6 @@ void flan_dev_reg_note_vec(flan_vec *v, int64_t size, const char *type,
|
||||
if (v) flan_dev_reg_note(v->ptr, v->cap * size, size, type, typelen);
|
||||
}
|
||||
|
||||
void flan_dev_reg_note_pool(flan_pool *p, int64_t size, const char *type,
|
||||
int64_t typelen) {
|
||||
if (!p) return;
|
||||
flan_dev_reg_note(p->items, p->cap * size, size, type, typelen);
|
||||
/* The slot headers are the pool's own bookkeeping and not the element type,
|
||||
so they are named for what they are. Recording them matters for the same
|
||||
reason the items do: after a free-all their bytes are still readable and
|
||||
an address landing in them must not come back as an element. */
|
||||
flan_dev_reg_note(p->slots, p->cap * (int64_t)sizeof(flan_pool_slot),
|
||||
(int64_t)sizeof(flan_pool_slot), "pool slots", 11);
|
||||
}
|
||||
|
||||
void flan_dev_reg_note_map(flan_map *m, int64_t ksize, int64_t vsize,
|
||||
const char *type, int64_t typelen) {
|
||||
if (!m || !m->data) return;
|
||||
|
||||
@ -71,9 +71,7 @@
|
||||
(do d (t x)))
|
||||
|
||||
;; The builtins that take a *type name* as an argument, over a variable. Each
|
||||
;; reaches the one list of what names a type, so all three came at once.
|
||||
;; (pool-new t) and (map-new t i32) are the other two; a Pool of a variable
|
||||
;; needs it not to be move-only, which [copyable?] is.
|
||||
;; reaches the one list of what names a type; (map-new t i32) is the other.
|
||||
(defn one-of [x $t] (Vec $t)
|
||||
{:where (copyable? $t)}
|
||||
(let [v (vec-new t)]
|
||||
|
||||
@ -1,103 +0,0 @@
|
||||
;;;; (Handle T) and (Pool T), spec-memory.md — "Cross-referencing long-lived
|
||||
;;;; objects uses (Handle a) into a pool, never a raw pointer or slice. A
|
||||
;;;; stale handle is detectable."
|
||||
;;;;
|
||||
;;;; The thesis, in one program: something holds a reference to an entity; the
|
||||
;;;; entity dies; the slot is reused by a different entity; and the old
|
||||
;;;; reference answers "gone" instead of answering wrong. Every other case
|
||||
;;;; here is secondary to that one.
|
||||
;;;;
|
||||
;;;; It is all one function because a Pool is move-only exactly as a Vec is,
|
||||
;;;; so passing one to a helper *consumes* it — there is no borrowing
|
||||
;;;; parameter in the language yet. That is not a pool question and this
|
||||
;;;; program does not work around it; see docs/BUILT.md.
|
||||
|
||||
(defstruct Enemy [hp i32 kind i32])
|
||||
|
||||
;; The projectile does not hold an Enemy and does not hold an index. It holds
|
||||
;; a handle, which is a number that owns nothing and copies freely — which is
|
||||
;; why a struct may contain one where it may not contain a Vec.
|
||||
(defstruct Projectile [target (Handle Enemy) damage i32])
|
||||
|
||||
(defn main [] i32
|
||||
(let [pool (pool-new Enemy)]
|
||||
(let [a (insert pool (Enemy {.hp 10 .kind 1}))
|
||||
b (insert pool (Enemy {.hp 20 .kind 2}))
|
||||
c (insert pool (Enemy {.hp 30 .kind 3}))
|
||||
sum 0]
|
||||
(println (len pool)) ; 3 slots handed out
|
||||
(println (live pool)) ; 3 of them live
|
||||
|
||||
;; Enumeration, which is what a world arena and an owned region do not
|
||||
;; give and which migrate-instances will need. (len p) is the slot
|
||||
;; high-water, so 0..(len p) visits every slot ever handed out, and
|
||||
;; (pool-handle p i) says which of them are still live.
|
||||
(dotimes [i (len pool)]
|
||||
(match (pool-handle pool i)
|
||||
(Some h) (match (resolve pool h)
|
||||
;; resolve yields a *pointer*, not a copy: mutating the
|
||||
;; pooled thing in place is what a pool is for, and a
|
||||
;; pattern binding binds a value.
|
||||
(Some e) (set sum (+ sum (.hp e)))
|
||||
None (do))
|
||||
None (do)))
|
||||
(println sum) ; 60
|
||||
|
||||
;; A write through a resolved pointer is a write to the pooled entity.
|
||||
(match (resolve pool b)
|
||||
(Some e) (set (.hp e) 21)
|
||||
None (do))
|
||||
(match (resolve pool b)
|
||||
(Some e) (println (.hp e)) ; 21
|
||||
None (println -1))
|
||||
|
||||
;; ── The thesis ────────────────────────────────────────────────
|
||||
;; A projectile chasing b. b dies. The slot is reused by a fourth
|
||||
;; enemy, which lands in exactly that slot — and the projectile's
|
||||
;; handle says so rather than chasing the newcomer.
|
||||
(let [shot (Projectile {.target b .damage 5})]
|
||||
(println (release pool b)) ; true — this call released it
|
||||
(println (release pool b)) ; false — it was already gone
|
||||
(println (live pool)) ; 2
|
||||
(let [d (insert pool (Enemy {.hp 99 .kind 4}))]
|
||||
;; Printed as index:generation. Same slot, later generation — the
|
||||
;; two halves of the answer, visible.
|
||||
(println b)
|
||||
(println d)
|
||||
(println (= d b)) ; false
|
||||
(println (= d d)) ; true
|
||||
(match (resolve pool (.target shot))
|
||||
(Some e) (println (.hp e))
|
||||
None (println -1)) ; -1, not 99
|
||||
(match (resolve pool d)
|
||||
(Some e) (println (.hp e)) ; 99
|
||||
None (println -1))
|
||||
(println (len pool)) ; still 3 slots
|
||||
(println (live pool)) ; 3 live
|
||||
|
||||
;; A zeroed handle is generation 0, which is even, and a live slot's
|
||||
;; generation is always odd — so ZII gives a handle field the right
|
||||
;; meaning for free rather than pointing it at slot 0.
|
||||
(let [z (Projectile {.damage 1})]
|
||||
(println (.target z))
|
||||
(match (resolve pool (.target z))
|
||||
(Some e) (println (.hp e))
|
||||
None (println -1))) ; -1
|
||||
|
||||
;; a and c are untouched by any of it.
|
||||
(match (resolve pool a)
|
||||
(Some e) (println (.hp e)) ; 10
|
||||
None (println -1))
|
||||
(match (resolve pool c)
|
||||
(Some e) (println (.hp e)) ; 30
|
||||
None (println -1))
|
||||
|
||||
;; spec-memory.md's first release point, applied to the owner. The
|
||||
;; runtime leaves the pool empty, so a handle into it would resolve
|
||||
;; to None rather than into released storage — but that is not
|
||||
;; demonstrable from here and this program does not pretend it is:
|
||||
;; free consumes pool, so a resolve on the next line is a compile
|
||||
;; error. The runtime property is real and the checker makes it
|
||||
;; unreachable.
|
||||
(free pool)
|
||||
0)))))
|
||||
@ -1,25 +0,0 @@
|
||||
;;;; The epoch trap on the pool's side. spec-memory.md, "Dev builds detect a
|
||||
;;;; released region".
|
||||
;;;;
|
||||
;;;; This is deliberately the *other* failure from a stale handle, and the two
|
||||
;;;; must not be conflated — the same rule that keeps a Vec's generation word
|
||||
;;;; and its epoch word apart. A stale handle is an answer: the entity died,
|
||||
;;;; resolve says None, the program carries on. A released region is not an
|
||||
;;;; answer at all: the storage the pool sits in is gone, the slot array with
|
||||
;;;; it, and there is nothing left to ask. So one returns None and the other
|
||||
;;;; traps naming the site.
|
||||
(defn main [] i32
|
||||
(let [a (arena-new 4096)]
|
||||
(let [p (pool-new i32 a)]
|
||||
(let [h (insert p 7)]
|
||||
(match (resolve p h)
|
||||
(Some x) (println (deref x))
|
||||
None (println -1))
|
||||
;; The region goes. p is still in scope, still looks fine, and h is
|
||||
;; still a perfectly well-formed handle — which is exactly the case a
|
||||
;; static rule cannot see.
|
||||
(free-all a)
|
||||
(match (resolve p h)
|
||||
(Some x) (println (deref x))
|
||||
None (println -1)))))
|
||||
0)
|
||||
@ -4,7 +4,7 @@
|
||||
;;;; nothing at run time can say what is at an address. The registry sidesteps
|
||||
;;;; that: the allocator's *caller* knew the type, and a dev build writes it
|
||||
;;;; down. What is asserted here is the consequence a program can see without
|
||||
;;;; an inspector — whether an address is still live — and the three ways
|
||||
;;;; an inspector — whether an address is still live — and the two ways
|
||||
;;;; storage dies underneath one.
|
||||
;;;;
|
||||
;;;; This program is deliberately readable in a release build too, and prints
|
||||
@ -48,17 +48,6 @@
|
||||
(free-all frame)
|
||||
(println (reg-live q)))) ; 0 either way
|
||||
|
||||
;; 3. And the pool, whose storage is the one place a (Ptr T) is handed to a
|
||||
;; program by name: (resolve p h) points into the middle of the items
|
||||
;; array, never at its base. Nothing but a containment lookup can answer
|
||||
;; for it.
|
||||
(let [pool (pool-new i32)]
|
||||
(let [h (insert pool 5)]
|
||||
(match (resolve pool h)
|
||||
(Some ip) (println (reg-live ip)) ; dev: 1
|
||||
None (println -1))
|
||||
(free pool)))
|
||||
|
||||
;; Nothing is live by now except whatever the arena's own destroy leaves, so
|
||||
;; the count is a statement about the table rather than about one address.
|
||||
(arena-destroy frame)
|
||||
|
||||
@ -634,11 +634,11 @@ let () =
|
||||
— memcheck still says nothing — it makes the same read *answerable*, by
|
||||
a different tool. The two must not be blurred. *)
|
||||
outputs "registry, dev" ~dev:true "programs/registry.flan"
|
||||
"1\n1\n0\n1\n0\n1\n0\n";
|
||||
"1\n1\n0\n1\n0\n0\n";
|
||||
outputs "registry, release" "programs/registry.flan"
|
||||
"0\n0\n0\n0\n0\n0\n0\n";
|
||||
"0\n0\n0\n0\n0\n0\n";
|
||||
outputs "registry, release -O0" ~opt:"-O0" "programs/registry.flan"
|
||||
"0\n0\n0\n0\n0\n0\n0\n";
|
||||
"0\n0\n0\n0\n0\n0\n";
|
||||
(* free-all on an allocator that does not offer it traps rather than doing
|
||||
nothing, because "I released the region" and "I leaked the region" must
|
||||
not be the same program text. Its own case for the same reason the
|
||||
@ -953,39 +953,7 @@ let () =
|
||||
end;
|
||||
(try Sys.remove exe with Sys_error _ -> ());
|
||||
|
||||
(* (Handle T) and (Pool T), spec-memory.md. The thesis is one line of this
|
||||
output and the rest is scaffolding for it: the same slot prints as
|
||||
<handle 1:1> before a death and <handle 1:3> after the reuse, and the
|
||||
projectile still holding the first is told -1 rather than the
|
||||
newcomer's 99. At -O0 as well, because the null test resolve is built
|
||||
out of is exactly the kind of control flow an optimiser launders, and
|
||||
as a dev build, because a pool then lives in a frame the reload path
|
||||
has to agree with on 64 bytes. *)
|
||||
let handles_out =
|
||||
"3\n3\n60\n21\ntrue\nfalse\n2\n<handle 1:1>\n<handle 1:3>\nfalse\ntrue\n-1\n99\n3\n3\n<handle 0:0>\n-1\n10\n30\n"
|
||||
in
|
||||
outputs "handles" "programs/handles.flan" handles_out;
|
||||
outputs ~opt:"-O0" "handles, -O0" "programs/handles.flan" handles_out;
|
||||
outputs ~dev:true "handles, dev" "programs/handles.flan" handles_out;
|
||||
|
||||
(* The epoch trap on the pool's side, and it is deliberately the *other*
|
||||
failure from a stale handle. A stale handle is an answer and resolve
|
||||
returns None; a released region is not an answer at all, because the
|
||||
slot array went with the storage, so it traps. The two must not be
|
||||
conflated, which is the same rule that keeps a Vec's generation word
|
||||
and its epoch word apart. *)
|
||||
let exe = compile "programs/pool-stale-region.flan" in
|
||||
let code, text = run exe None in
|
||||
if code <> 134 || not (contains text "programs/pool-stale-region.flan:")
|
||||
|| not (contains text "allocator was released")
|
||||
|| not (contains text "7")
|
||||
then begin
|
||||
incr failures;
|
||||
Printf.printf
|
||||
"FAIL a pool used after its region was released\n\
|
||||
\ got: %S (exit %d)\n wanted: exit 134, naming the site\n"
|
||||
text code
|
||||
end;
|
||||
(try Sys.remove exe with Sys_error _ -> ());
|
||||
|
||||
(* The same trap on the Map's side, and it is not the same code path: a
|
||||
|
||||
@ -1026,19 +1026,6 @@ let () =
|
||||
~needle:"exactly two types";
|
||||
rejects_check "Result is milestone 6" "(defn f [] (Result i32 i32) None)"
|
||||
~needle:"milestone 6";
|
||||
(* (Handle T) and (Pool T) are built. What stays refused is the arity, for
|
||||
the reason Vec's and Map's arities are, and the four shapes below — each
|
||||
of which is a way of losing the one property the type exists to have. *)
|
||||
rejects_check "Handle takes one type" "(defn f [x (Handle i32 i32)] ())"
|
||||
~needle:"exactly one type";
|
||||
rejects_check "Pool takes one type" "(defn f [x (Pool i32 i32)] ())"
|
||||
~needle:"exactly one type";
|
||||
(* A pool of an owning element used to be refused here, with the Vec's and
|
||||
the Map's, and the three came down together: the reason all of them gave
|
||||
was teardown, and a region has none. What replaced them is a run-time
|
||||
branch on the allocator's can-free at the construction, so the *type* is
|
||||
ordinary and only the tier is a question. See the arena rows below. *)
|
||||
accepts "a pool of a Vec" "(defn f [x (Pool (Vec i32))] ())";
|
||||
|
||||
(* ── The region rule, spec-memory.md's arena rule ────────────────────
|
||||
The compile-time half of it, which is the only half a checker row can
|
||||
@ -1102,22 +1089,6 @@ let () =
|
||||
"(defvar g (Vec u8)) \
|
||||
(defn f [] () (set g (vec-new u8)) (push g 1) (set (at g 0) 2) \
|
||||
(println (len (as-slice g))) (let [c (clone g)] (free c)))";
|
||||
(* Ordering handles would order a slot index, which is a free-list artefact.
|
||||
Equality is admitted and ordering is not, which is why there are two
|
||||
predicates in Types rather than one. *)
|
||||
rejects_check "handles do not order"
|
||||
"(defn f [a (Handle i32) b (Handle i32)] bool (< a b))"
|
||||
~needle:"no built-in comparison";
|
||||
(* free takes the owner. A handle is a copyable number that owns nothing, so
|
||||
consuming one copy would say nothing about the others — which is why a
|
||||
slot is recycled by (release p h) and not by free. *)
|
||||
rejects_check "free of a handle"
|
||||
"(defn f [h (Handle i32)] () (free h))" ~needle:"a handle owns nothing";
|
||||
(* Cloning a pool would duplicate the generation counters with the slots, so
|
||||
one handle would resolve in both copies and name two different things. *)
|
||||
rejects_check "a pool cannot be cloned"
|
||||
"(defn f [p (Pool i32)] () (let [q (clone p)] (do)))"
|
||||
~needle:"cannot be cloned";
|
||||
rejects_check "try is milestone 6" "(defn f [] i32 (try 1))"
|
||||
~needle:"milestone 6";
|
||||
(* dotimes and defer are implemented, and a defer in a [let] is now one of
|
||||
|
||||
@ -138,7 +138,6 @@ let corpus =
|
||||
same directory; the new C here is three more path buffers, which is
|
||||
exactly what this tool is for. *)
|
||||
"programs/files.flan", [];
|
||||
"programs/handles.flan", [];
|
||||
"programs/machine.flan", [];
|
||||
"programs/math.flan", [];
|
||||
"programs/math3.flan", [];
|
||||
|
||||
@ -191,7 +191,7 @@ let check label path args ~checks =
|
||||
link on its own.
|
||||
|
||||
The seven programs here that abort by design — error, exhausted-unhandled,
|
||||
free-all-refused, map-stale-region, pool-stale-region, slurp-unhandled,
|
||||
free-all-refused, map-stale-region, slurp-unhandled,
|
||||
stale-region — are
|
||||
kept. A trap is a controlled abort after an fprintf, and "the trap still
|
||||
fires, in the same place, with the same message, under memcheck" is worth
|
||||
@ -217,14 +217,12 @@ let corpus =
|
||||
"programs/exhausted-unhandled.flan", [];
|
||||
"programs/files.flan", [];
|
||||
"programs/free-all-refused.flan", [];
|
||||
"programs/handles.flan", [];
|
||||
"programs/machine.flan", [];
|
||||
"programs/map-exhausted.flan", [];
|
||||
"programs/map-stale-region.flan", [];
|
||||
"programs/maps.flan", [];
|
||||
"programs/math.flan", [];
|
||||
"programs/math3.flan", [];
|
||||
"programs/pool-stale-region.flan", [];
|
||||
"programs/pkg-macro.flan", [];
|
||||
"programs/pkg-diamond.flan", [];
|
||||
"programs/pkg-return.flan", [];
|
||||
|
||||
@ -25,11 +25,10 @@
|
||||
# bytes a previous round wrote before the reset reports. test_valgrind.ml
|
||||
# asserts it as a control — it produced nothing before the runtime change
|
||||
# and six errors after. The corpus stayed clean across that change, and
|
||||
# the sharp end of that is stale-region.flan, map-stale-region.flan and
|
||||
# pool-stale-region.flan: all three read through a pointer into an arena
|
||||
# that has been reset, all three are now reading bytes memcheck knows are
|
||||
# undefined, and none of them reports — because the epoch trap fires
|
||||
# first. The runtime's own guard beats the read. Interior overruns are
|
||||
# the sharp end of that is stale-region.flan and map-stale-region.flan:
|
||||
# both read through a pointer into an arena that has been reset, both are
|
||||
# reading bytes memcheck knows are undefined, and neither reports —
|
||||
# because the epoch trap fires first. The runtime's own guard beats the read. Interior overruns are
|
||||
# still invisible, for the structural reason above.
|
||||
#
|
||||
# 2. Hand-written LLVM IR. Expected to confuse the tool. It does not, and it
|
||||
|
||||
Loading…
x
Reference in New Issue
Block a user