The refusal was about teardown, and a region has none
This commit is contained in:
commit
e9d0b99096
10
NEXT.md
10
NEXT.md
@ -1622,6 +1622,16 @@ ordinary loop inside the defer body — the manual cascade, three lines, at one
|
|||||||
else, and resource release is `defer` at the acquisition site. That idiom does not transfer directly only because
|
else, and resource release is `defer` at the acquisition site. That idiom does not transfer directly only because
|
||||||
Odin's `defer` is block-scoped; the relaxation above recovers most of it.
|
Odin's `defer` is block-scoped; the relaxation above recovers most of it.
|
||||||
|
|
||||||
|
**And it settled the recursive dynamic value too, which is the case that nearly reopened this.** A `(Vec Value)` where a
|
||||||
|
`Value` may hold a `(Vec Value)` — what an EDN reader answers with when nobody hands it a target struct type — was
|
||||||
|
refused five ways, and the argument for building `drop` was that nothing else could make it declarable. That was wrong,
|
||||||
|
and the refusals' own words say so: each of them named *teardown* as the problem, and a region has no teardown.
|
||||||
|
`free-all` takes the whole arena, inner blocks included. So the refusals moved to the allocator tier — a run-time branch
|
||||||
|
on `can-free` at construction and at every growth — rather than being answered with a hook. This is Odin's position in
|
||||||
|
full: `core:encoding/json` ships a hand-written recursive `destroy_value` in the *library* and names parsing against
|
||||||
|
`temp_allocator` plus `free_all` as the idiomatic alternative, and neither is a language feature. See spec-memory.md,
|
||||||
|
"A container of owning elements lives in a region", and `test/programs/arena-edn.flan`.
|
||||||
|
|
||||||
**The safety net, and the better use of effort: a debug tracking allocator.** ASan's leak detection covers memory
|
**The safety net, and the better use of effort: a debug tracking allocator.** ASan's leak detection covers memory
|
||||||
*instrumented* code allocated — the Flan allocator, and it is already wired up and clean. It does **not** cover a leaked
|
*instrumented* code allocated — the Flan allocator, and it is already wired up and clean. It does **not** cover a leaked
|
||||||
texture, because that memory belongs to uninstrumented raylib, which is the same reason the sanitizer sweep treats the
|
texture, because that memory belongs to uninstrumented raylib, which is the same reason the sanitizer sweep treats the
|
||||||
|
|||||||
@ -3508,10 +3508,13 @@ be written before.
|
|||||||
|
|
||||||
### `split` answers a `(Vec [u8])`, and the owning shape is unrepresentable
|
### `split` answers a `(Vec [u8])`, and the owning shape is unrepresentable
|
||||||
|
|
||||||
The fields are slices *of the input*. That is not a performance choice — `(Vec (Vec u8))` is **refused outright**
|
The fields are slices *of the input*. That was not a performance choice when this was written: `(Vec (Vec u8))` was
|
||||||
(`programs/vec-of-vec.flan`, "copies and releases elements bytewise"), so there is no owning shape to have chosen
|
**refused outright**, so there was no owning shape to have chosen instead. That refusal has since been narrowed — see
|
||||||
instead. It follows that the result dies with whatever the input pointed at, which is the same contract `trim` and
|
spec-memory.md, "A container of owning elements lives in a region" — and a `(Vec (Vec u8))` is now buildable, against
|
||||||
`split-next!` already have.
|
a region allocator and nowhere else. `split` is unchanged anyway, and now by choice rather than by refusal: an owning
|
||||||
|
`split` would have to allocate one block per field and would only be usable in the tier that can never hand one back,
|
||||||
|
while the slices cost nothing and work everywhere. It follows, as before, that the result dies with whatever the input
|
||||||
|
pointed at, which is the same contract `trim` and `split-next!` already have.
|
||||||
|
|
||||||
The rule is `split-on-byte`'s, unchanged: n separators always yield n+1 fields, so an empty input yields one empty
|
The rule is `split-on-byte`'s, unchanged: n separators always yield n+1 fields, so an empty input yields one empty
|
||||||
field and a trailing separator yields a trailing empty one. That is Odin's allocating `strings.split` and not Odin's
|
field and a trailing separator yields a trailing empty one. That is Odin's allocating `strings.split` and not Odin's
|
||||||
|
|||||||
417
lib/check.ml
417
lib/check.ml
@ -426,6 +426,69 @@ let unimplemented loc what milestone =
|
|||||||
question the compiler answers rather than a trait a user implements. *)
|
question the compiler answers rather than a trait a user implements. *)
|
||||||
let predicate_names = [ "ordered?"; "equal?"; "hashable?"; "numeric?"; "copyable?" ]
|
let predicate_names = [ "ordered?"; "equal?"; "hashable?"; "numeric?"; "copyable?" ]
|
||||||
|
|
||||||
|
(* ── What a type owns, transitively ────────────────────────────────────
|
||||||
|
spec-memory.md: "Ownership is structural, not declared." [Types.is_move_only]
|
||||||
|
answers the same question one level deep and deliberately stops there — a
|
||||||
|
[Named] is not move-only, because making it so is the transitive ownership
|
||||||
|
model that recursive teardown would need, and there is no recursive teardown.
|
||||||
|
This walk is the *other* use of the same fact, and the two must not be
|
||||||
|
collapsed: nothing here feeds the move checker, and a type this says yes
|
||||||
|
about is still copied and still tracked exactly as it was yesterday.
|
||||||
|
|
||||||
|
What it decides, and the only thing it decides, is whether a container of
|
||||||
|
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,
|
||||||
|
a fixed array, a struct or a data type's case owns whatever its payload
|
||||||
|
does.
|
||||||
|
|
||||||
|
It does not live in [Types] for the reason [Types.keyable] gives: that
|
||||||
|
module has no field table. The [seen] list is the cycle guard, and the cycle
|
||||||
|
is real — the recursive dynamic value this exists for holds a [(Vec Value)],
|
||||||
|
so [Value]'s walk reaches [Value]. Answering [false] for a name already on
|
||||||
|
the path is right rather than merely terminating: whatever made the outer
|
||||||
|
name own something was found by the arm that got here, and a name cannot
|
||||||
|
contain itself by value anyway — [check_finite] refuses that — only through
|
||||||
|
a container, which is an arm that answers for itself.
|
||||||
|
|
||||||
|
[env.unions], the untagged ones, are deliberately not consulted: a move-only
|
||||||
|
member in one is refused outright, and that refusal is not waiting on
|
||||||
|
teardown the way these were — nothing anywhere records which member is
|
||||||
|
live, so there is no fact a release could read. A region removes the
|
||||||
|
teardown question and leaves that one exactly where it was, so an untagged
|
||||||
|
union owns nothing and there is nothing here to walk. *)
|
||||||
|
let owning_fields env n =
|
||||||
|
match Hashtbl.find_opt env.structs n with
|
||||||
|
| Some s -> [ s.Tast.fields ]
|
||||||
|
| None ->
|
||||||
|
match Hashtbl.find_opt env.datas n with
|
||||||
|
| Some d -> List.map (fun (c : Tast.variant) -> c.Tast.vfields) d.Tast.cases
|
||||||
|
| None -> []
|
||||||
|
|
||||||
|
let rec owning env ?(seen = []) (t : Types.t) =
|
||||||
|
match t with
|
||||||
|
| Types.Vec _ | Types.Map _ | Types.Pool _ -> true
|
||||||
|
| Types.Option e | Types.Array (_, e) -> owning env ~seen e
|
||||||
|
| Types.Named n ->
|
||||||
|
not (List.mem n seen)
|
||||||
|
&& List.exists
|
||||||
|
(List.exists
|
||||||
|
(fun (f : Tast.field) -> owning env ~seen:(n :: seen) f.Tast.fty))
|
||||||
|
(owning_fields env n)
|
||||||
|
| _ -> false
|
||||||
|
|
||||||
|
(* Does a container of this type have to be built against an allocator that
|
||||||
|
cannot free one block? Only the half a release would have to walk is asked:
|
||||||
|
a map's key cannot own anything — [map_type] refuses one, because a key that
|
||||||
|
owned storage would hash its header rather than what it points at — so the
|
||||||
|
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.Map (_, v) -> owning env v
|
||||||
|
| _ -> false
|
||||||
|
|
||||||
(* Does a concrete type answer yes? Checked at every instantiation, against
|
(* Does a concrete type answer yes? Checked at every instantiation, against
|
||||||
the type the call site asked for. *)
|
the type the call site asked for. *)
|
||||||
let pred_holds p (t : Types.t) =
|
let pred_holds p (t : Types.t) =
|
||||||
@ -499,17 +562,12 @@ let rec move_only preds (t : Types.t) =
|
|||||||
different paths and a silent disagreement between them would be worse than
|
different paths and a silent disagreement between them would be worse than
|
||||||
saying the same thing twice. *)
|
saying the same thing twice. *)
|
||||||
let map_type ?(preds = []) loc (k : Types.t) (v : Types.t) =
|
let map_type ?(preds = []) loc (k : Types.t) (v : Types.t) =
|
||||||
(* The value. The restriction is the one [(Vec (Vec T))] already carries,
|
ignore preds;
|
||||||
for the identical reason: the runtime copies and releases entries
|
(* The value used to be refused here when it owned anything, in the same
|
||||||
bytewise, so an owning value would have its header duplicated by clone
|
words [(Vec (Vec T))] used, and the refusal is gone for the reason set out
|
||||||
and its buffer dropped on the floor by free. *)
|
over [map-new]: it was about *teardown*, and which tier this map will be
|
||||||
if move_only preds v then
|
built against is not knowable where its type is written. The question is
|
||||||
fail loc
|
asked at the construction instead, of the allocator, once. *)
|
||||||
"(Map %s %s) holds a move-only value, and the type-erased runtime \
|
|
||||||
copies entries bytewise — so clone would duplicate headers instead of \
|
|
||||||
copying, and free would leak what they own. Owned entries arrive with \
|
|
||||||
drop (step 5 in NEXT.md)"
|
|
||||||
(Types.to_string k) (Types.to_string v);
|
|
||||||
(* () has no bytes, so a slot for one is a slot of nothing: the cell
|
(* () has no bytes, so a slot for one is a slot of nothing: the cell
|
||||||
geometry divides the cache line by the element size and there is nothing
|
geometry divides the cache line by the element size and there is nothing
|
||||||
to divide by. It is also the natural spelling of a *set*, which is why
|
to divide by. It is also the natural spelling of a *set*, which is why
|
||||||
@ -600,20 +658,20 @@ let rec resolve env ?(seen = []) (t : Ast.texpr) : Types.t =
|
|||||||
| ("Ptr" | "Option"), _ -> fail loc "(%s T) takes exactly one type" name
|
| ("Ptr" | "Option"), _ -> fail loc "(%s T) takes exactly one type" name
|
||||||
| "Vec", [ a ] ->
|
| "Vec", [ a ] ->
|
||||||
let e = resolve env ~seen a in
|
let e = resolve env ~seen a in
|
||||||
(* A Vec of a Vec is representable and would be wrong. spec-memory.md
|
(* A Vec of a Vec used to be refused here, and the refusal named two
|
||||||
makes [clone] a deep copy and makes [free] recurse structurally into
|
different failures under one sentence: that [clone] would duplicate
|
||||||
owning fields; the type-erased runtime does neither — it memcpys, so
|
inner headers instead of copying, and that [free] would drop their
|
||||||
a clone would duplicate inner headers and a free would drop their
|
buffers on the floor. Only the second one was about *teardown*, and
|
||||||
buffers on the floor. Recursive teardown is what step 5's [drop]
|
only the second one an arena answers — [free-all] takes the region
|
||||||
brings, and this is refused until it does rather than shipping the
|
and the inner blocks with it, because they came out of the same
|
||||||
shallow answer under the deep name. *)
|
region. So the type is admitted, the tier is checked at the
|
||||||
if move_only env.tvpreds e then
|
construction where the allocator is a value that exists (see
|
||||||
fail loc
|
[vec-new]), and [clone] stays refused at the operation, on its own
|
||||||
"(Vec %s) holds a move-only element, and the type-erased runtime \
|
merits, in its own words.
|
||||||
copies and releases elements bytewise — so clone would duplicate \
|
|
||||||
headers instead of copying, and free would leak what they own. \
|
It cannot be refused *here* because nothing here knows the tier:
|
||||||
Recursive teardown arrives with drop (step 5 in NEXT.md)"
|
[with-allocator] rebinds a dynamic variable, so which allocator a
|
||||||
(Types.to_string e);
|
[(vec-new)] meets is not a property of where the type is written. *)
|
||||||
Types.Vec e
|
Types.Vec e
|
||||||
| "Vec", _ -> fail loc "(Vec T) takes exactly one type"
|
| "Vec", _ -> fail loc "(Vec T) takes exactly one type"
|
||||||
| "Map", [ k; v ] ->
|
| "Map", [ k; v ] ->
|
||||||
@ -623,17 +681,21 @@ let rec resolve env ?(seen = []) (t : Ast.texpr) : Types.t =
|
|||||||
| "Result", _ -> unimplemented loc "(Result T E)" 6
|
| "Result", _ -> unimplemented loc "(Result T E)" 6
|
||||||
| "Pool", [ a ] ->
|
| "Pool", [ a ] ->
|
||||||
let e = resolve env ~seen a in
|
let e = resolve env ~seen a in
|
||||||
(* The same refusal (Vec T) makes, for the same reason: the pool's
|
(* Lifted with the Vec's and pushed to the construction with it, and a
|
||||||
runtime is type-erased and copies and releases slots bytewise, so a
|
pool is the one of the three where that is not quite the same trade,
|
||||||
release would drop what an owning element owns. Recursive teardown
|
because a pool has a release point a Vec does not: [(release p h)]
|
||||||
arrives with drop. *)
|
recycles one slot while the pool lives on. In a region that costs a
|
||||||
if move_only env.tvpreds e then
|
block that stays allocated until [free-all] and is never handed back
|
||||||
fail loc
|
— the slot itself is reused, since the next insert overwrites those
|
||||||
"(Pool %s) holds a move-only element, and the type-erased runtime \
|
bytes, but whatever the dead element pointed at is stranded.
|
||||||
copies and releases slots bytewise — so releasing a slot would \
|
|
||||||
leak what it owns. Recursive teardown arrives with drop (step 5 \
|
That is a region leak bounded by the region, which is the bargain a
|
||||||
in NEXT.md)"
|
region already is: an arena's whole proposition is that nothing comes
|
||||||
(Types.to_string e);
|
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
|
Types.Pool e
|
||||||
| "Pool", _ -> fail loc "(Pool T) takes exactly one type"
|
| "Pool", _ -> fail loc "(Pool T) takes exactly one type"
|
||||||
| "Handle", [ a ] -> Types.Handle (resolve env ~seen a)
|
| "Handle", [ a ] -> Types.Handle (resolve env ~seen a)
|
||||||
@ -1124,6 +1186,65 @@ let align_of loc t = mk loc (Types.Int Types.I64) (Tast.Prim (Tast.AlignOf t, []
|
|||||||
let addr_of loc (e : Tast.expr) =
|
let addr_of loc (e : Tast.expr) =
|
||||||
mk loc (Types.Ptr e.Tast.ty) (Tast.Prim (Tast.AddrOf, [ e ]))
|
mk loc (Types.Ptr e.Tast.ty) (Tast.Prim (Tast.AddrOf, [ e ]))
|
||||||
|
|
||||||
|
(* ── The region requirement, emitted ───────────────────────────────────
|
||||||
|
spec-memory.md's arena rule, and the whole of what replaced the three
|
||||||
|
refusals a container of owning elements used to meet at its *type*. The
|
||||||
|
question those refusals asked was about teardown: the type-erased runtime
|
||||||
|
copies and releases slots bytewise, so a [free] would release the slots and
|
||||||
|
leave everything inside them stranded. A region never releases a slot —
|
||||||
|
[free-all] takes the whole thing, inner blocks included, because they came
|
||||||
|
out of the same region — so the premise does not hold there and the refusal
|
||||||
|
was over-broad.
|
||||||
|
|
||||||
|
What could not move with it is *where* the question is asked. [can-free] is
|
||||||
|
a capability on an allocator value, read at run time, and [with-allocator]
|
||||||
|
rebinds a dynamic variable, so the tier a [(vec-new)] will meet is not a
|
||||||
|
property of the place its type is written. The compile-time half is
|
||||||
|
therefore only the decision to ask — [region_only], a property of the
|
||||||
|
element type and settled here — and the run-time half is the answer.
|
||||||
|
|
||||||
|
One branch per container and never per element, which spec-memory.md fixes
|
||||||
|
and which is a performance decision before it is a safety one: the
|
||||||
|
alternative is a walk at release, and a walk at release is the registry of
|
||||||
|
destructors the frame tier's reset exists to not have.
|
||||||
|
|
||||||
|
Emitted at every site that can *allocate* for such a container, not only at
|
||||||
|
its construction, and the extra sites are not belt and braces. ZII means a
|
||||||
|
container can exist without ever passing through [vec-new]: a data type
|
||||||
|
case's field left out of a literal, a [(defvar xs (Vec Value))] a global
|
||||||
|
starts as. Those are zeroed, they have no allocator at all, and the first
|
||||||
|
[push] is what adopts the context — so a guard only at the construction
|
||||||
|
would have a hole exactly the width of ZII.
|
||||||
|
|
||||||
|
The *container* is what is asked in both places, and at a construction that
|
||||||
|
means the guard runs immediately after the init rather than before it. The
|
||||||
|
allocator is right there as an argument of the site, but naming it twice in
|
||||||
|
the emitted tree is not free: it is an arbitrary expression, and [(vec-new
|
||||||
|
Value (arena-new 4096))] would build two arenas and guard the one it threw
|
||||||
|
away. The container has recorded it by the time the init returns, so asking
|
||||||
|
the container asks that one expression exactly once. It is still the point
|
||||||
|
of construction and still before anything is put in; what a trap there costs
|
||||||
|
is the empty block just taken, on a process that is about to die.
|
||||||
|
|
||||||
|
At a growth the guard runs first, because there the container already exists
|
||||||
|
and the allocation is what has to be stopped. A zeroed one answers from the
|
||||||
|
context it is about to adopt, which is not a guess — [flan_vec_adopt] is the
|
||||||
|
code that will take it, on this same call. *)
|
||||||
|
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) =
|
||||||
|
if not (region_only env target.Tast.ty) then after
|
||||||
|
else
|
||||||
|
mk loc after.Tast.ty
|
||||||
|
(Tast.Do
|
||||||
|
[ rt loc Types.Unit (region_sym target.Tast.ty) [ target; here loc ];
|
||||||
|
after ])
|
||||||
|
|
||||||
(* Every integer index into an array or slice is i32 at milestone 2. *)
|
(* Every integer index into an array or slice is i32 at milestone 2. *)
|
||||||
let index_ty = Types.Int Types.I32
|
let index_ty = Types.Int Types.I32
|
||||||
|
|
||||||
@ -1878,16 +1999,29 @@ and moved ?ty ctx loc name slot =
|
|||||||
and traps on a stale slice whether the Vec is a global or not. *)
|
and traps on a stale slice whether the Vec is a global or not. *)
|
||||||
and global_borrow ctx loc name (ty : Types.t) =
|
and global_borrow ctx loc name (ty : Types.t) =
|
||||||
if not ctx.borrow then
|
if not ctx.borrow then
|
||||||
|
(* The last clause is conditional, because [clone] stopped being offerable
|
||||||
|
for one of these. A global whose elements own storage is admitted — a
|
||||||
|
move-only global starts zeroed and this one is no different — but
|
||||||
|
cloning it is refused, on the grounds that a bytewise copy is an alias
|
||||||
|
under a name that promises independence. Offering it anyway would send a
|
||||||
|
reader to a second refusal, and there is no other route to an
|
||||||
|
independent copy: the region owns the graph, and [free-all] is the only
|
||||||
|
thing that releases any of it. *)
|
||||||
fail loc
|
fail loc
|
||||||
"%s is %s, which is move-only, and a global of one is only ever \
|
"%s is %s, which is move-only, and a global of one is only ever \
|
||||||
borrowed: its lifetime is the process's, so nothing may take ownership \
|
borrowed: its lifetime is the process's, so nothing may take ownership \
|
||||||
of it, and this site would. A free through the new owner would leave \
|
of it, and this site would. A free through the new owner would leave \
|
||||||
every other reader of %s pointing at released memory. Read and mutate \
|
every other reader of %s pointing at released memory. Read and mutate \
|
||||||
it where it is — (len %s), (at %s i), (push %s x), (set (at %s i) x) \
|
it where it is — (len %s), (at %s i), (push %s x), (set (at %s i) x) \
|
||||||
— or take a view with (as-slice %s), a pointer with (addr %s), or an \
|
— or take a view with (as-slice %s) or a pointer with (addr %s)%s"
|
||||||
independent copy with (clone %s), which is the one of these that \
|
name (Types.to_string ty) name name name name name name name
|
||||||
something else may own"
|
(if region_only ctx.env ty then
|
||||||
name (Types.to_string ty) name name name name name name name name
|
". There is no independent copy of this one: its elements own \
|
||||||
|
storage, so a clone would alias rather than copy and is refused"
|
||||||
|
else
|
||||||
|
Printf.sprintf
|
||||||
|
", or an independent copy with (clone %s), which is the one of \
|
||||||
|
these that something else may own" name)
|
||||||
|
|
||||||
(* The target of an operation that reads a container without consuming it. Only
|
(* The target of an operation that reads a container without consuming it. Only
|
||||||
a syntactically simple target is treated as a borrow: in [(len (f v))] the
|
a syntactically simple target is treated as a borrow: in [(len (f v))] the
|
||||||
@ -3791,7 +3925,9 @@ and named_call ctx ~want loc name args =
|
|||||||
(reg_note loc "flan_dev_reg_note_vec"
|
(reg_note loc "flan_dev_reg_note_vec"
|
||||||
(mk loc (Types.Vec elem) (Tast.Local v))
|
(mk loc (Types.Vec elem) (Tast.Local v))
|
||||||
[ size_of loc elem ] elem);
|
[ size_of loc elem ] elem);
|
||||||
mk loc (Types.Vec elem) (Tast.Local v) ])))
|
region_check ctx.env loc
|
||||||
|
(mk loc (Types.Vec elem) (Tast.Local v))
|
||||||
|
(mk loc (Types.Vec elem) (Tast.Local v)) ])))
|
||||||
(* Unit, not a Result and not an ignorable error code: see [alloc_guard]. *)
|
(* Unit, not a Result and not an ignorable error code: see [alloc_guard]. *)
|
||||||
| "push" ->
|
| "push" ->
|
||||||
arity loc name 2 args;
|
arity loc name 2 args;
|
||||||
@ -3816,9 +3952,10 @@ and named_call ctx ~want loc name args =
|
|||||||
expect loc ~want
|
expect loc ~want
|
||||||
(mk loc Types.Unit
|
(mk loc Types.Unit
|
||||||
(Tast.Let ([ (e, x) ],
|
(Tast.Let ([ (e, x) ],
|
||||||
[ with_note loc (alloc_guard ctx loc attempt)
|
[ region_check ctx.env loc target
|
||||||
|
(with_note loc (alloc_guard ctx loc attempt)
|
||||||
(reg_note loc "flan_dev_reg_note_vec" target
|
(reg_note loc "flan_dev_reg_note_vec" target
|
||||||
[ size_of loc elem ] elem) ])))
|
[ size_of loc elem ] elem)) ])))
|
||||||
| _ -> assert false)
|
| _ -> assert false)
|
||||||
| "reserve" ->
|
| "reserve" ->
|
||||||
arity loc name 2 args;
|
arity loc name 2 args;
|
||||||
@ -3855,7 +3992,9 @@ and named_call ctx ~want loc name args =
|
|||||||
reg_note loc "flan_dev_reg_note_vec" target
|
reg_note loc "flan_dev_reg_note_vec" target
|
||||||
[ size_of loc elem ] elem
|
[ size_of loc elem ] elem
|
||||||
in
|
in
|
||||||
expect loc ~want (with_note loc (alloc_guard ctx loc attempt) note)
|
expect loc ~want
|
||||||
|
(region_check ctx.env loc target
|
||||||
|
(with_note loc (alloc_guard ctx loc attempt) note))
|
||||||
| _ -> assert false)
|
| _ -> assert false)
|
||||||
(* (as-slice v) and (as-slice v lo hi) — spec-memory.md, "Borrowing". The
|
(* (as-slice v) and (as-slice v lo hi) — spec-memory.md, "Borrowing". The
|
||||||
result is a non-owning view: copying it copies ptr+len and never the
|
result is a non-owning view: copying it copies ptr+len and never the
|
||||||
@ -3895,7 +4034,40 @@ and named_call ctx ~want loc name args =
|
|||||||
| "free" ->
|
| "free" ->
|
||||||
arity loc name 1 args;
|
arity loc name 1 args;
|
||||||
let target = check ctx (List.hd args) in
|
let target = check ctx (List.hd args) in
|
||||||
|
(* A container of owning elements is refused here, and a reader will
|
||||||
|
assume the opposite — that [free] recurses — so this says why it does
|
||||||
|
not and what does.
|
||||||
|
|
||||||
|
The bytes this container holds are element *headers*, and releasing the
|
||||||
|
block those headers sit in says nothing about the blocks they point at.
|
||||||
|
Nothing type-erased can walk them: the runtime sees a size and an
|
||||||
|
alignment and has never heard of the element type. That is the same
|
||||||
|
fact the type-level refusals used to state, and the arena did not change
|
||||||
|
it — what the arena changed is that it no longer matters there, because
|
||||||
|
the inner blocks came out of the same region and [free-all] takes them
|
||||||
|
with everything else.
|
||||||
|
|
||||||
|
So the honest answer is not to recurse, and it is not to release the
|
||||||
|
backing store quietly either. Releasing the outer block alone would be
|
||||||
|
"I freed it" spelt over a program that leaked everything inside, and
|
||||||
|
this file refuses that collapse everywhere else — [flan_alloc_free_all]
|
||||||
|
traps rather than no-op for the same reason. It is refused instead, at
|
||||||
|
the one place a reader is looking when they want to know.
|
||||||
|
|
||||||
|
The guard at construction is what makes the advice reachable: such a
|
||||||
|
container is region-allocated or it does not exist, so there is always a
|
||||||
|
[free-all] to point at. *)
|
||||||
(match target.Tast.ty with
|
(match target.Tast.ty with
|
||||||
|
| (Types.Vec _ | Types.Map _ | Types.Pool _)
|
||||||
|
when region_only ctx.env target.Tast.ty ->
|
||||||
|
fail loc
|
||||||
|
"%s holds elements that own storage, and free releases the block \
|
||||||
|
those elements sit in — not the blocks they point at, which nothing \
|
||||||
|
type-erased can reach. This container was built against a region \
|
||||||
|
allocator, because the guard at its construction admits no other, so \
|
||||||
|
release the region: (free-all a) takes it and everything its \
|
||||||
|
elements own, in one operation and with no per-element teardown"
|
||||||
|
(Types.to_string target.Tast.ty)
|
||||||
| Types.Vec elem ->
|
| Types.Vec elem ->
|
||||||
expect loc ~want
|
expect loc ~want
|
||||||
(rt loc Types.Unit "flan_vec_free"
|
(rt loc Types.Unit "flan_vec_free"
|
||||||
@ -3937,6 +4109,37 @@ and named_call ctx ~want loc name args =
|
|||||||
let target = borrowed ctx target (fun () -> check ctx target) in
|
let target = borrowed ctx target (fun () -> check ctx target) in
|
||||||
let a = allocator_arg ctx loc rest in
|
let a = allocator_arg ctx loc rest in
|
||||||
(match target.Tast.ty with
|
(match target.Tast.ty with
|
||||||
|
(* The refusal that did *not* come down with the type-level ones, and
|
||||||
|
the distinction is worth being exact about, because the sentence
|
||||||
|
they all used to share bundled two different failures: that a clone
|
||||||
|
would duplicate inner headers instead of copying, and that a free
|
||||||
|
would leak what those headers own. Only the second was about
|
||||||
|
teardown, and only the second is answered by a region.
|
||||||
|
|
||||||
|
What disqualifies [clone] is not that it copies a header — so do
|
||||||
|
[at] and [get], and they are fine, because they promise nothing and
|
||||||
|
hand back an alias into a region nobody individually frees. It is
|
||||||
|
that [clone] *allocates a new block and promises independence*.
|
||||||
|
spec-memory.md calls it a deep copy; what a memcpy of the slots
|
||||||
|
delivers is a second container whose elements still point into the
|
||||||
|
first one's blocks. Two containers, one set of inner buffers, under
|
||||||
|
a name that says otherwise — and putting the copy in a second arena
|
||||||
|
makes it worse, not better, because tipping that arena leaves the
|
||||||
|
copy's elements pointing into an arena that is still live while its
|
||||||
|
own storage is gone.
|
||||||
|
|
||||||
|
Refused at the operation rather than at the type, because that is
|
||||||
|
where the promise is made. *)
|
||||||
|
| (Types.Vec _ | Types.Map _) when region_only ctx.env target.Tast.ty ->
|
||||||
|
fail loc
|
||||||
|
"%s cannot be cloned: clone is a deep, independent copy, and the \
|
||||||
|
type-erased runtime copies slots bytewise — so the copy's \
|
||||||
|
elements would still point at the original's blocks, which is an \
|
||||||
|
alias under a name that promises the opposite. Nothing here can \
|
||||||
|
walk an element to copy what it owns. Build a second container \
|
||||||
|
and insert into it, or keep the one you have — a region makes \
|
||||||
|
sharing safe, not copying"
|
||||||
|
(Types.to_string target.Tast.ty)
|
||||||
(* A map's clone reinserts rather than copying the block, because the
|
(* A map's clone reinserts rather than copying the block, because the
|
||||||
seed is derived from the block's address — see flan_rt.c. That is
|
seed is derived from the block's address — see flan_rt.c. That is
|
||||||
the runtime's business; from here it is one more allocating call
|
the runtime's business; from here it is one more allocating call
|
||||||
@ -4021,7 +4224,8 @@ and named_call ctx ~want loc name args =
|
|||||||
(reg_note loc "flan_dev_reg_note_pool"
|
(reg_note loc "flan_dev_reg_note_pool"
|
||||||
(mk loc pty (Tast.Local p))
|
(mk loc pty (Tast.Local p))
|
||||||
[ size_of loc elem ] elem);
|
[ size_of loc elem ] elem);
|
||||||
mk loc pty (Tast.Local p) ])))
|
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
|
(* (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
|
inserted: a pool hands out no index and no pointer, because an index does
|
||||||
@ -4048,9 +4252,10 @@ and named_call ctx ~want loc name args =
|
|||||||
expect loc ~want
|
expect loc ~want
|
||||||
(mk loc hty
|
(mk loc hty
|
||||||
(Tast.Let ([ (e, x); (h, mk loc hty (Tast.Zero hty)) ],
|
(Tast.Let ([ (e, x); (h, mk loc hty (Tast.Zero hty)) ],
|
||||||
[ with_note loc (alloc_guard ctx loc attempt)
|
[ region_check ctx.env loc target
|
||||||
|
(with_note loc (alloc_guard ctx loc attempt)
|
||||||
(reg_note loc "flan_dev_reg_note_pool" target
|
(reg_note loc "flan_dev_reg_note_pool" target
|
||||||
[ size_of loc elem ] elem);
|
[ size_of loc elem ] elem));
|
||||||
mk loc hty (Tast.Local h) ])))
|
mk loc hty (Tast.Local h) ])))
|
||||||
| _ -> assert false)
|
| _ -> assert false)
|
||||||
|
|
||||||
@ -4235,7 +4440,8 @@ and named_call ctx ~want loc name args =
|
|||||||
(reg_note loc "flan_dev_reg_note_map"
|
(reg_note loc "flan_dev_reg_note_map"
|
||||||
(mk loc mty (Tast.Local m))
|
(mk loc mty (Tast.Local m))
|
||||||
[ size_of loc k; size_of loc v ] mty);
|
[ size_of loc k; size_of loc v ] mty);
|
||||||
mk loc mty (Tast.Local m) ])))
|
region_check ctx.env loc (mk loc mty (Tast.Local m))
|
||||||
|
(mk loc mty (Tast.Local m)) ])))
|
||||||
|
|
||||||
(* (put m k v) — the upsert. Unit, not a Result and not an ignorable error
|
(* (put m k v) — the upsert. Unit, not a Result and not an ignorable error
|
||||||
code: see [alloc_guard]. spec-memory.md is explicit that it either
|
code: see [alloc_guard]. spec-memory.md is explicit that it either
|
||||||
@ -4268,10 +4474,11 @@ and named_call ctx ~want loc name args =
|
|||||||
expect loc ~want
|
expect loc ~want
|
||||||
(mk loc Types.Unit
|
(mk loc Types.Unit
|
||||||
(Tast.Let ([ (ks, k); (vs, v) ],
|
(Tast.Let ([ (ks, k); (vs, v) ],
|
||||||
[ with_note loc (alloc_guard ctx loc attempt)
|
[ region_check ctx.env loc target
|
||||||
|
(with_note loc (alloc_guard ctx loc attempt)
|
||||||
(reg_note loc "flan_dev_reg_note_map" target
|
(reg_note loc "flan_dev_reg_note_map" target
|
||||||
[ size_of loc kt; size_of loc vt ]
|
[ size_of loc kt; size_of loc vt ]
|
||||||
target.Tast.ty) ])))
|
target.Tast.ty)) ])))
|
||||||
| _ -> assert false)
|
| _ -> assert false)
|
||||||
|
|
||||||
(* (get m k) -> (Option V). Absence is None, not an untyped nil, and the
|
(* (get m k) -> (Option V). Absence is None, not an untyped nil, and the
|
||||||
@ -5410,28 +5617,52 @@ let collect env (decls : Ast.decl list) =
|
|||||||
if List.length (List.sort_uniq compare names) <> List.length names then
|
if List.length (List.sort_uniq compare names) <> List.length names then
|
||||||
fail loc "%s declares the same field twice" n;
|
fail loc "%s declares the same field twice" n;
|
||||||
let fields = List.map field fs in
|
let fields = List.map field fs in
|
||||||
|
(* Recorded before the refusal below rather than after it, because the
|
||||||
|
refusal asks [region_only], which walks this very declaration: a
|
||||||
|
recursive value's field is a [(Vec Value)] and answering for it
|
||||||
|
means reading [Value]'s own cases back out of the table. A [fail]
|
||||||
|
aborts the whole compilation, so an entry left behind by a
|
||||||
|
declaration that is about to be refused is never read. *)
|
||||||
|
Hashtbl.replace env.structs n { Tast.sname = n; fields };
|
||||||
(* spec-memory.md: "Ownership is structural, not declared" — a struct
|
(* spec-memory.md: "Ownership is structural, not declared" — a struct
|
||||||
containing a Vec is itself move-only, and freeing one recurses into
|
containing a Vec is itself move-only, and freeing one recurses into
|
||||||
its owning fields while (free (.items b)) is refused because it
|
its owning fields while (free (.items b)) is refused because it
|
||||||
would leave the owner partly dead. None of that transitive
|
would leave the owner partly dead. None of that transitive
|
||||||
machinery exists yet: it is the same recursive teardown [drop]
|
machinery exists, and it is what [drop] would have brought. So the
|
||||||
brings, and it lands with it. Until then the field is refused at
|
field is still refused at the declaration, where the message can
|
||||||
the declaration, where the message can say so, rather than
|
say so, rather than accepted into a struct that copies its header
|
||||||
accepted into a struct that copies its header on assignment and
|
on assignment and gives two owners one buffer.
|
||||||
gives two owners one buffer. *)
|
|
||||||
|
With one exception, and it is exact: a field whose container holds
|
||||||
|
*owning* elements. That container cannot exist outside a region —
|
||||||
|
the guard at its construction is what makes sure of it (see
|
||||||
|
[vec-new]) — so the struct's field is region-allocated too,
|
||||||
|
transitively and by the same guard, and the whole graph is released
|
||||||
|
by one [free-all]. There is nothing for a teardown to recurse into
|
||||||
|
because there is no teardown, and the two-owners-one-buffer problem
|
||||||
|
is not one when the owner is the region and neither copy is it.
|
||||||
|
|
||||||
|
The plain case stays refused precisely because nothing enforces
|
||||||
|
anything there: a [(Vec i32)] field is happily built against the
|
||||||
|
heap, nothing would object, and then (free (.items b)) through two
|
||||||
|
copies of the struct is a double free with no guard between it and
|
||||||
|
the program. *)
|
||||||
List.iter
|
List.iter
|
||||||
(fun (f : Tast.field) ->
|
(fun (f : Tast.field) ->
|
||||||
if Types.is_move_only f.Tast.fty then
|
if Types.is_move_only f.Tast.fty
|
||||||
|
&& not (region_only env f.Tast.fty) then
|
||||||
fail loc
|
fail loc
|
||||||
"%s's field %s is %s, which is move-only, and a struct that \
|
"%s's field %s is %s, which is move-only, and a struct that \
|
||||||
owns one is move-only too — transitively, with recursive \
|
owns one is move-only too — transitively, with recursive \
|
||||||
teardown and with a field that cannot be freed on its own. \
|
teardown and with a field that cannot be freed on its own. \
|
||||||
That rule arrives with drop (step 5 in NEXT.md); until then \
|
That rule does not exist; hold the %s in a local and pass \
|
||||||
hold the %s in a local and pass it"
|
it. A container whose *elements* own storage is the one \
|
||||||
|
kind admitted here, because it can only have been built \
|
||||||
|
against a region allocator and a single (free-all) takes \
|
||||||
|
the whole graph"
|
||||||
n f.Tast.fname (Types.to_string f.Tast.fty)
|
n f.Tast.fname (Types.to_string f.Tast.fty)
|
||||||
(Types.to_string f.Tast.fty))
|
(Types.to_string f.Tast.fty))
|
||||||
fields;
|
fields
|
||||||
Hashtbl.replace env.structs n { Tast.sname = n; fields }
|
|
||||||
| Ast.Defdata (n, vs) ->
|
| Ast.Defdata (n, vs) ->
|
||||||
(* A data type with no cases has no value, so nothing could ever be given
|
(* A data type with no cases has no value, so nothing could ever be given
|
||||||
one, and a parameter of that type would be a function nothing can
|
one, and a parameter of that type would be a function nothing can
|
||||||
@ -5444,7 +5675,7 @@ let collect env (decls : Ast.decl list) =
|
|||||||
let cnames = List.map (fun (v : Ast.variant) -> v.Ast.vname) vs in
|
let cnames = List.map (fun (v : Ast.variant) -> v.Ast.vname) vs in
|
||||||
if List.length (List.sort_uniq compare cnames) <> List.length cnames
|
if List.length (List.sort_uniq compare cnames) <> List.length cnames
|
||||||
then fail loc "%s declares the same case twice" n;
|
then fail loc "%s declares the same case twice" n;
|
||||||
let cases =
|
let cases_with_loc =
|
||||||
List.map
|
List.map
|
||||||
(fun (v : Ast.variant) ->
|
(fun (v : Ast.variant) ->
|
||||||
let fnames =
|
let fnames =
|
||||||
@ -5455,30 +5686,52 @@ let collect env (decls : Ast.decl list) =
|
|||||||
fail v.Ast.vloc "%s.%s declares the same field twice"
|
fail v.Ast.vloc "%s.%s declares the same field twice"
|
||||||
n v.Ast.vname;
|
n v.Ast.vname;
|
||||||
let vfields = List.map field v.Ast.vfields in
|
let vfields = List.map field v.Ast.vfields in
|
||||||
(* The same refusal a struct field gets, for the same reason
|
v.Ast.vloc, { Tast.vname = v.Ast.vname; vfields })
|
||||||
and in the same words: a data type case's fields are a struct,
|
|
||||||
the data type copies bytewise on assignment, and recursive
|
|
||||||
teardown arrives with [drop]. Refusing it here rather than
|
|
||||||
at a use keeps the two declarations honest with each other
|
|
||||||
— a data type that could hold a Vec where a struct could not
|
|
||||||
would be a hole in the same rule. *)
|
|
||||||
List.iter
|
|
||||||
(fun (f : Tast.field) ->
|
|
||||||
if Types.is_move_only f.Tast.fty then
|
|
||||||
fail v.Ast.vloc
|
|
||||||
"%s.%s's field %s is %s, which is move-only, and a \
|
|
||||||
data type case that owns one makes the data type \
|
|
||||||
move-only \
|
|
||||||
too — transitively, with recursive teardown. That \
|
|
||||||
rule arrives with drop (step 5 in NEXT.md); until \
|
|
||||||
then hold the %s in a local and pass it"
|
|
||||||
n v.Ast.vname f.Tast.fname (Types.to_string f.Tast.fty)
|
|
||||||
(Types.to_string f.Tast.fty))
|
|
||||||
vfields;
|
|
||||||
{ Tast.vname = v.Ast.vname; vfields })
|
|
||||||
vs
|
vs
|
||||||
in
|
in
|
||||||
|
let cases = List.map snd cases_with_loc in
|
||||||
|
(* Registered before the field refusal below, not after, for the
|
||||||
|
reason the struct's copy of this gives: [region_only] has to read
|
||||||
|
this data type's own cases back out to answer for a [(Vec Value)]
|
||||||
|
that names [Value]. The two declarations do this identically
|
||||||
|
because a data type that could hold a container where a struct
|
||||||
|
could not would be a hole in the same rule. *)
|
||||||
Hashtbl.replace env.datas n { Tast.dname = n; cases };
|
Hashtbl.replace env.datas n { Tast.dname = n; cases };
|
||||||
|
(* The same refusal a struct field gets, for the same reason, in the
|
||||||
|
same words, and with the same one exception: a data type case's
|
||||||
|
fields are a struct, the data type copies bytewise on assignment,
|
||||||
|
and there is no recursive teardown to make that safe — except where
|
||||||
|
the field's container holds owning elements, which can only have
|
||||||
|
been built against a region and is therefore released whole.
|
||||||
|
|
||||||
|
This is the arm the recursive dynamic value needs, and it is worth
|
||||||
|
naming what it buys: a [Value] with a [(Vec Value)] case and a
|
||||||
|
[(Map string Value)] case is now declarable, parsed into an arena,
|
||||||
|
walked, and released by one [free-all] with no per-element teardown
|
||||||
|
anywhere. What it costs is that a [Value] is copied bytewise like
|
||||||
|
any other data value, so two copies share the inner blocks. In a
|
||||||
|
region that is aliasing and not a double free, because neither copy
|
||||||
|
owns anything — the region does. *)
|
||||||
|
List.iter
|
||||||
|
(fun (vloc, (c : Tast.variant)) ->
|
||||||
|
List.iter
|
||||||
|
(fun (f : Tast.field) ->
|
||||||
|
if Types.is_move_only f.Tast.fty
|
||||||
|
&& not (region_only env f.Tast.fty) then
|
||||||
|
fail vloc
|
||||||
|
"%s.%s's field %s is %s, which is move-only, and a \
|
||||||
|
data type case that owns one makes the data type \
|
||||||
|
move-only too — transitively, with recursive teardown. \
|
||||||
|
That rule does not exist; hold the %s in a local and \
|
||||||
|
pass it. A \
|
||||||
|
container whose *elements* own storage is the one kind \
|
||||||
|
admitted here, because it can only have been built \
|
||||||
|
against a region allocator and a single (free-all) \
|
||||||
|
takes the whole graph"
|
||||||
|
n c.Tast.vname f.Tast.fname (Types.to_string f.Tast.fty)
|
||||||
|
(Types.to_string f.Tast.fty))
|
||||||
|
c.Tast.vfields)
|
||||||
|
cases_with_loc;
|
||||||
List.iter
|
List.iter
|
||||||
(fun (c : Tast.variant) ->
|
(fun (c : Tast.variant) ->
|
||||||
Hashtbl.replace env.cases (n ^ "." ^ c.Tast.vname) (n, c);
|
Hashtbl.replace env.cases (n ^ "." ^ c.Tast.vname) (n, c);
|
||||||
|
|||||||
@ -2735,6 +2735,9 @@ declare void @flan_context_restore(ptr)
|
|||||||
declare ptr @flan_arena_new(i64)
|
declare ptr @flan_arena_new(i64)
|
||||||
declare void @flan_arena_destroy(ptr)
|
declare void @flan_arena_destroy(ptr)
|
||||||
declare void @flan_alloc_free_all(ptr, ptr, i64)
|
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(ptr)
|
||||||
declare i8 @flan_alloc_can_free_all(ptr)
|
declare i8 @flan_alloc_can_free_all(ptr)
|
||||||
declare i64 @flan_alloc_epoch(ptr)
|
declare i64 @flan_alloc_epoch(ptr)
|
||||||
|
|||||||
@ -1143,6 +1143,65 @@ _Noreturn void flan_free_all_fail(const uint8_t *loc, int64_t loclen) {
|
|||||||
rt_die();
|
rt_die();
|
||||||
}
|
}
|
||||||
|
|
||||||
|
/* ── The region requirement, spec-memory.md's arena rule ───────────────
|
||||||
|
*
|
||||||
|
* A container whose elements themselves own storage — a `(Vec Value)` where a
|
||||||
|
* `Value` may hold a `(Vec Value)` — may allocate only from an allocator that
|
||||||
|
* cannot release one block. The reason is the one the checker's refusal used
|
||||||
|
* to give and is worth restating where the branch actually is: this runtime is
|
||||||
|
* type-erased, so `flan_vec_free` memcpys and releases slots bytewise and has
|
||||||
|
* no way to reach inside a slot. Against the heap that is a leak of everything
|
||||||
|
* the elements own. Against a region it is not a question at all, because no
|
||||||
|
* individual slot is ever released: `free-all` takes the whole arena, inner
|
||||||
|
* blocks included, and there is nothing left for a bytewise release to get
|
||||||
|
* wrong.
|
||||||
|
*
|
||||||
|
* So the capability set is what decides it, and `can-free` is the bit: an
|
||||||
|
* allocator that can free one block is one on which the leak is expressible,
|
||||||
|
* and an allocator that cannot is one on which it is not. The question is
|
||||||
|
* asked of the capability rather than of "is this an arena" because a fixed
|
||||||
|
* backing buffer someone writes later is the same answer for the same reason.
|
||||||
|
*
|
||||||
|
* ONE BRANCH PER CONTAINER, not per element. spec-memory.md fixes that and it
|
||||||
|
* is a performance decision before it is a safety one: the alternative is
|
||||||
|
* letting such a container into the general tier and having something walk it
|
||||||
|
* at release, which is the registry of destructors the frame tier's reset
|
||||||
|
* exists to not have.
|
||||||
|
*
|
||||||
|
* It is a run-time branch and not a compile-time refusal because there is
|
||||||
|
* nothing static to refuse against. `with-allocator` rebinds a dynamic
|
||||||
|
* variable, so which tier a `(vec-new)` meets is not knowable where it is
|
||||||
|
* written, and `context/allocator` is a value read at run time. The checker
|
||||||
|
* decides *whether to ask* — that part is a property of the element type and
|
||||||
|
* is settled at compile time — and this decides the answer.
|
||||||
|
*
|
||||||
|
* Nothing the compiler emits calls this one directly. The three container
|
||||||
|
* wrappers below it do, and they are what the emitted code names, because a
|
||||||
|
* container answers for the allocator it recorded — or, having recorded none,
|
||||||
|
* for the one it is about to adopt. Asking through the container is also what
|
||||||
|
* keeps the allocator expression at a construction site from being named
|
||||||
|
* twice; see [Check.region_check]. */
|
||||||
|
_Noreturn void flan_region_only_fail(const uint8_t *loc, int64_t loclen);
|
||||||
|
|
||||||
|
void flan_alloc_region_only(flan_allocator *a, const uint8_t *loc,
|
||||||
|
int64_t loclen) {
|
||||||
|
if (!a) flan_null_alloc_fail(loc, loclen);
|
||||||
|
if (a->caps & FLAN_CAN_FREE) flan_region_only_fail(loc, loclen);
|
||||||
|
}
|
||||||
|
|
||||||
|
_Noreturn void flan_region_only_fail(const uint8_t *loc, int64_t loclen) {
|
||||||
|
fflush(stdout);
|
||||||
|
fprintf(stderr,
|
||||||
|
"%.*s: this container's elements own storage, and this allocator can "
|
||||||
|
"free one block — so a free here would release the slots and leak "
|
||||||
|
"everything inside them, and nothing type-erased can walk them. "
|
||||||
|
"Build it against a region allocator, whose free-all takes the "
|
||||||
|
"inner blocks too: (with-allocator context/temp ...) or an "
|
||||||
|
"(arena-new n)\n",
|
||||||
|
(int)loclen, (const char *)loc);
|
||||||
|
rt_die();
|
||||||
|
}
|
||||||
|
|
||||||
/* ── (Vec T), spec-memory.md ────────────────────────────────────────────
|
/* ── (Vec T), spec-memory.md ────────────────────────────────────────────
|
||||||
*
|
*
|
||||||
* One type-erased runtime over (size, align), which is Odin's arrangement
|
* One type-erased runtime over (size, align), which is Odin's arrangement
|
||||||
@ -1240,6 +1299,26 @@ static flan_allocator *flan_vec_adopt(flan_vec *v) {
|
|||||||
return v->alloc;
|
return v->alloc;
|
||||||
}
|
}
|
||||||
|
|
||||||
|
/* The region requirement asked of a container rather than of a named
|
||||||
|
* allocator, which is the form every *growth* site needs. A Vec that was built
|
||||||
|
* by (vec-new) has its allocator already and answers from it; one that was
|
||||||
|
* zeroed — a data type case's field left out of a literal, a (defvar xs (Vec
|
||||||
|
* Value)) that a global starts as — has none yet, and the allocator it is
|
||||||
|
* about to adopt is the context. Asking the context in that case is not a
|
||||||
|
* guess: [flan_vec_adopt], three lines up, is the code that will take it, and
|
||||||
|
* it runs on this same call.
|
||||||
|
*
|
||||||
|
* Without this the construction guard would have a hole exactly the width of
|
||||||
|
* ZII: every zeroed container skips (vec-new) entirely and reaches storage
|
||||||
|
* through its first push. */
|
||||||
|
void flan_alloc_region_only(flan_allocator *a, const uint8_t *loc,
|
||||||
|
int64_t loclen);
|
||||||
|
|
||||||
|
void flan_vec_region_only(flan_vec *v, const uint8_t *loc, int64_t loclen) {
|
||||||
|
flan_alloc_region_only(v->alloc ? v->alloc : flan_context_allocator(),
|
||||||
|
loc, loclen);
|
||||||
|
}
|
||||||
|
|
||||||
static int8_t flan_vec_grow(flan_vec *v, int64_t want, int64_t size,
|
static int8_t flan_vec_grow(flan_vec *v, int64_t want, int64_t size,
|
||||||
int64_t align) {
|
int64_t align) {
|
||||||
flan_allocator *a = flan_vec_adopt(v);
|
flan_allocator *a = flan_vec_adopt(v);
|
||||||
@ -1465,6 +1544,13 @@ static void flan_pool_check(flan_pool *p, const uint8_t *loc, int64_t loclen) {
|
|||||||
}
|
}
|
||||||
}
|
}
|
||||||
|
|
||||||
|
/* 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) {
|
static flan_allocator *flan_pool_adopt(flan_pool *p) {
|
||||||
if (!p->alloc) {
|
if (!p->alloc) {
|
||||||
p->alloc = flan_context_allocator();
|
p->alloc = flan_context_allocator();
|
||||||
@ -2043,6 +2129,15 @@ static void flan_map_check(flan_map *m, const uint8_t *loc, int64_t loclen) {
|
|||||||
}
|
}
|
||||||
}
|
}
|
||||||
|
|
||||||
|
/* The same guard a Vec gets, at the same place and for the same reason — see
|
||||||
|
* the note above [flan_vec_region_only]. Only the *value* half of a map can
|
||||||
|
* own anything: a key that owned storage would hash its header rather than
|
||||||
|
* what it points at, and [map_type] has always refused one. */
|
||||||
|
void flan_map_region_only(flan_map *m, const uint8_t *loc, int64_t loclen) {
|
||||||
|
flan_alloc_region_only(m->alloc ? m->alloc : flan_context_allocator(),
|
||||||
|
loc, loclen);
|
||||||
|
}
|
||||||
|
|
||||||
static flan_allocator *flan_map_adopt(flan_map *m) {
|
static flan_allocator *flan_map_adopt(flan_map *m) {
|
||||||
if (!m->alloc) {
|
if (!m->alloc) {
|
||||||
m->alloc = flan_context_allocator();
|
m->alloc = flan_context_allocator();
|
||||||
|
|||||||
109
spec-memory.md
109
spec-memory.md
@ -56,9 +56,14 @@ them from:
|
|||||||
replaces. `(set (get m k) v)` is not map syntax.
|
replaces. `(set (get m k) v)` is not map syntax.
|
||||||
|
|
||||||
The first Map implementation admits copyable keys and values only, so `get`
|
The first Map implementation admits copyable keys and values only, so `get`
|
||||||
returns a copy. Move-aware lookup, removal, and owned entries are deferred until
|
returns a copy. Move-aware lookup and removal are deferred; the map itself
|
||||||
`Vec`/`Map` values are supported in maps; the map itself remains an owning,
|
remains an owning, move-only container.
|
||||||
move-only container.
|
|
||||||
|
A value that **owns storage** is admitted, and only in a region — see "A
|
||||||
|
container of owning elements lives in a region" below, which is also where what
|
||||||
|
`get` hands back in that case is settled. The key half is not relaxed and will
|
||||||
|
not be: a key that owned storage would hash its header rather than what it
|
||||||
|
points at.
|
||||||
|
|
||||||
## Copying is always explicit
|
## Copying is always explicit
|
||||||
|
|
||||||
@ -72,6 +77,16 @@ no `drop` hook** (see Allocators). A `drop` hook makes a type move-only for the
|
|||||||
same reason a `Vec` field does — exactly one owner, so the hook fires exactly
|
same reason a `Vec` field does — exactly one owner, so the hook fires exactly
|
||||||
once — and a type with one cannot be `clone`d.
|
once — and a type with one cannot be `clone`d.
|
||||||
|
|
||||||
|
**With one exception, and it is the one that makes a recursive dynamic value
|
||||||
|
expressible.** A field whose container holds *owning* elements does not make
|
||||||
|
its struct or `defdata` case move-only: such an aggregate stays **copyable**,
|
||||||
|
and copies alias into the region rather than duplicating anything. That is
|
||||||
|
sound for the reason the whole arrangement is — the container can only have
|
||||||
|
been built against a region, so neither copy owns the blocks and the region
|
||||||
|
does. Transitive move-only is what recursive teardown would have needed, and
|
||||||
|
there is no recursive teardown; see "A container of owning elements lives in a
|
||||||
|
region" for the rule that stands in its place and for what it costs.
|
||||||
|
|
||||||
## Borrowing
|
## Borrowing
|
||||||
|
|
||||||
- `(as-slice v)` / `(as-slice v lo hi)` view a `Vec` or fixed array as `[T]`.
|
- `(as-slice v)` / `(as-slice v lo hi)` view a `Vec` or fixed array as `[T]`.
|
||||||
@ -359,7 +374,77 @@ when it is destroyed.
|
|||||||
|
|
||||||
**`free` applies to a whole owner.** It recurses structurally into owning
|
**`free` applies to a whole owner.** It recurses structurally into owning
|
||||||
fields. A field is never freed on its own: `(free (.textures e))` is refused,
|
fields. A field is never freed on its own: `(free (.textures e))` is refused,
|
||||||
because it would leave `e` partly dead with no way to say so.
|
because it would leave `e` partly dead with no way to say so. The recursion is
|
||||||
|
the half of this that is not built — see the next section, which says what is
|
||||||
|
built instead and what `free` does where the recursion would have been.
|
||||||
|
|
||||||
|
### A container of owning elements lives in a region
|
||||||
|
|
||||||
|
A `(Vec Value)` where a `Value` may itself hold a `(Vec Value)` — the recursive
|
||||||
|
dynamic value an EDN reader has to answer with when it is handed no target
|
||||||
|
struct type — was refused outright while this spec described only the recursion
|
||||||
|
above. The reason given was always the same one: the container runtime is
|
||||||
|
type-erased, so it copies and releases slots **bytewise** and cannot reach
|
||||||
|
inside a slot. A `free` would release the slots and leave every block they
|
||||||
|
point at stranded.
|
||||||
|
|
||||||
|
That reason is about **teardown**, and it does not hold for a region. `free-all`
|
||||||
|
never releases an individual slot; it takes the whole region, and every block
|
||||||
|
the elements own is in it, because they came out of it. So the refusal was
|
||||||
|
over-broad, and the rule is now narrower:
|
||||||
|
|
||||||
|
> **A container whose element type owns storage, transitively, may only
|
||||||
|
> allocate from an allocator that lacks `can-free`.** Checked at the point of
|
||||||
|
> construction and at any later growth: one branch per container, never per
|
||||||
|
> element.
|
||||||
|
|
||||||
|
Three things follow, and each is a decision rather than a consequence:
|
||||||
|
|
||||||
|
- **It is a run-time branch, not a compile-time refusal.** `can-free` is a
|
||||||
|
capability on an allocator *value*, and `with-allocator` rebinds a dynamic
|
||||||
|
variable, so which tier a `(vec-new)` will meet is not a property of the
|
||||||
|
place it is written. What is decided at compile time is only *whether to
|
||||||
|
ask* — that is a property of the element type. The question is asked of
|
||||||
|
`can-free` rather than of "is this an arena" so that a fixed backing buffer
|
||||||
|
written later answers it the same way for the same reason.
|
||||||
|
- **`free` on such a container is refused, not silently shallow.** It cannot
|
||||||
|
recurse — that is the whole premise — and releasing the outer block alone
|
||||||
|
would be "I freed it" written over a program that stranded everything
|
||||||
|
inside. A reader will assume recursion, so the refusal names `free-all`
|
||||||
|
instead, which is reachable by construction: such a container is
|
||||||
|
region-allocated or it does not exist.
|
||||||
|
- **`clone` on such a container is not possible and stays refused.** This is
|
||||||
|
the half a region does *not* answer, and it is a different failure from the
|
||||||
|
teardown one the two were once stated together as. `clone` promises a deep,
|
||||||
|
independent copy; a bytewise one hands back a second container whose elements
|
||||||
|
still point into the first one's blocks. Cloning into a *second* region is
|
||||||
|
worse rather than better, because releasing that region leaves the copy's
|
||||||
|
elements pointing into a region that is still live. `at` and `get` are
|
||||||
|
untouched: they promise nothing, and the alias they hand back is an alias
|
||||||
|
into storage nobody individually owns, which is the bargain a region is.
|
||||||
|
|
||||||
|
A **struct field or a `defdata` case's field** of such a container type is
|
||||||
|
admitted for the same reason and only for that reason — the field's container
|
||||||
|
can only have been built against a region, so the aggregate's whole graph is
|
||||||
|
released by one `free-all`. The aggregate itself **stays copyable**: ownership
|
||||||
|
is not made transitive through a name, because that is the model recursive
|
||||||
|
teardown would have needed. So a `Value` is copied bytewise like any other
|
||||||
|
value, and two copies share the inner blocks. In a region that is aliasing and
|
||||||
|
not a double free — and mutating through one alias is visible through the
|
||||||
|
other, which is a logic bug and the price of the bargain, exactly as it is in
|
||||||
|
Odin. A field holding a container whose elements own
|
||||||
|
*nothing* stays refused: nothing would force that one into a region, and two
|
||||||
|
copies of the aggregate would be two headers over one heap block. An untagged
|
||||||
|
`defunion` is not part of this at all: a move-only member in one is refused for
|
||||||
|
a reason that is not teardown — nothing records which member is live, so there
|
||||||
|
is no fact a release could read — and a region answers the teardown question
|
||||||
|
without touching that one.
|
||||||
|
|
||||||
|
A `Pool` is admitted with the others, and it is the one where the trade is not
|
||||||
|
identical, because `(release p h)` recycles a slot while the pool lives on.
|
||||||
|
Whatever the dead element owned stays allocated until `free-all`. That is a
|
||||||
|
region leak bounded by the region, which is what a region already is; it is not
|
||||||
|
a use-after-free, because nothing was released.
|
||||||
|
|
||||||
### Dev builds detect a released region
|
### Dev builds detect a released region
|
||||||
|
|
||||||
@ -371,6 +456,13 @@ counter from the per-`Vec` generation word that catches stale slices; the two
|
|||||||
answer different questions and must not be conflated. Both are dev-only: the
|
answer different questions and must not be conflated. Both are dev-only: the
|
||||||
release layout of a `Vec` is `ptr + len + cap + allocator` and nothing more.
|
release layout of a `Vec` is `ptr + len + cap + allocator` and nothing more.
|
||||||
|
|
||||||
|
This is what covers a use after `free-all`, including the case the section
|
||||||
|
above makes reachable: an inner container's header copied *out* of an
|
||||||
|
arena-held element into a local before the release still traps on the next
|
||||||
|
operation. It works because an `Allocator` is a **pointer** to the allocator
|
||||||
|
and not a copy of one — a copied-by-value allocator would give each copy its
|
||||||
|
own epoch, and a copy taken before the bump would never notice it.
|
||||||
|
|
||||||
### `drop` — owning something that is not memory
|
### `drop` — owning something that is not memory
|
||||||
|
|
||||||
A type may name one hook:
|
A type may name one hook:
|
||||||
@ -407,7 +499,14 @@ than replacing it. Flan takes that arrangement unchanged.
|
|||||||
an arena.** Constructing a container whose element type transitively has a
|
an arena.** Constructing a container whose element type transitively has a
|
||||||
`drop` hook, or allocating such a value, against an allocator that lacks
|
`drop` hook, or allocating such a value, against an allocator that lacks
|
||||||
`can-free` is **refused at the point of construction**: one branch per
|
`can-free` is **refused at the point of construction**: one branch per
|
||||||
container, not per element. `free-all` therefore never has to walk a list of
|
container, not per element. This is the rule the section on containers of
|
||||||
|
owning elements already states and already implements, with one difference that
|
||||||
|
matters if `drop` is ever built: a hook is the case a region *cannot* answer —
|
||||||
|
releasing the region does not close the socket — so a hooked element would have
|
||||||
|
to be refused against an arena rather than *required* to be in one. The two
|
||||||
|
questions must stay apart. Asking "does this element own anything" where "does
|
||||||
|
it have a hook" was meant would refuse nested containers in the frame tier,
|
||||||
|
which is precisely the case the frame tier exists for. `free-all` therefore never has to walk a list of
|
||||||
registered destructors, which is what keeps the frame tier's reset genuinely
|
registered destructors, which is what keeps the frame tier's reset genuinely
|
||||||
free (plan.org's memory table) and keeps a destructor list — an allocation
|
free (plan.org's memory table) and keeps a destructor list — an allocation
|
||||||
nobody wrote — out of the core.
|
nobody wrote — out of the core.
|
||||||
|
|||||||
175
test/programs/arena-edn.flan
Normal file
175
test/programs/arena-edn.flan
Normal file
@ -0,0 +1,175 @@
|
|||||||
|
;;;; An EDN document read into a dynamic value, against an arena.
|
||||||
|
;;;;
|
||||||
|
;;;; This is the other half of programs/edn.flan. That one reads a document
|
||||||
|
;;;; whose shape is known into a struct, by hand, which is what the compiler's
|
||||||
|
;;;; (read-edn Enemy bytes) will emit. This one is what a reader handed *no*
|
||||||
|
;;;; target type has to answer with: a data type naming itself through a
|
||||||
|
;;;; (Vec Value) and a (Map string Value), holding whatever was in the file.
|
||||||
|
;;;;
|
||||||
|
;;;; ── The allocator story, which is the point of the program ───────────
|
||||||
|
;;;;
|
||||||
|
;;;; read-value below takes no allocator and names none. It does not need to:
|
||||||
|
;;;; spec-memory.md puts the allocator in the calling convention, so every
|
||||||
|
;;;; (vec-new) and (map-new) inside it takes the *context*, and the caller
|
||||||
|
;;;; chooses the tier with (with-allocator ...) around the call. An explicit
|
||||||
|
;;;; allocator at a construction site overrides that, which is how a reader
|
||||||
|
;;;; would take one as a parameter if it wanted to — but the existing idiom
|
||||||
|
;;;; already does the job, so there is no new machinery here and none needed.
|
||||||
|
;;;;
|
||||||
|
;;;; The tier has to be a region and not the heap, and that is enforced rather
|
||||||
|
;;;; than documented: a (Vec Value) whose elements own storage traps at its
|
||||||
|
;;;; construction against any allocator that can free one block. See
|
||||||
|
;;;; programs/arena-region.flan.
|
||||||
|
;;;;
|
||||||
|
;;;; ── What the region buys, said plainly ───────────────────────────────
|
||||||
|
;;;;
|
||||||
|
;;;; The document below is four levels deep and every level allocates. There is
|
||||||
|
;;;; no teardown anywhere in this file: no drop, no destructor, no recursive
|
||||||
|
;;;; free, not even a (free) call. One (free-all frame) at the bottom of main
|
||||||
|
;;;; releases every Vec block, every Map block and every entry in them, because
|
||||||
|
;;;; they all came out of the same region.
|
||||||
|
;;;;
|
||||||
|
;;;; Odin's core:encoding/json ships a hand-written recursive destroy_value in
|
||||||
|
;;;; the *library* for the heap case, and names parsing against temp_allocator
|
||||||
|
;;;; and calling free_all as the idiomatic alternative. This is that
|
||||||
|
;;;; alternative, and it needs nothing from the language that was not already
|
||||||
|
;;;; there.
|
||||||
|
;;;;
|
||||||
|
;;;; ── One lifetime that is not the region's ────────────────────────────
|
||||||
|
;;;;
|
||||||
|
;;;; A Token's text is a slice INTO the source buffer, and (string ...) over it
|
||||||
|
;;;; is a view and not a copy — so every Text, every Key and every map key here
|
||||||
|
;;;; points at `src`, not at the arena. The document outlives free-all in that
|
||||||
|
;;;; one respect and dies with the buffer instead. That is edn.flan's stated
|
||||||
|
;;;; contract and not a new one; it is repeated because a reader looking at a
|
||||||
|
;;;; value that survived a free-all would otherwise think the region had
|
||||||
|
;;;; leaked.
|
||||||
|
|
||||||
|
(import edn "vendor:edn")
|
||||||
|
|
||||||
|
(defvar frame Allocator)
|
||||||
|
|
||||||
|
(defdata Value
|
||||||
|
[(Nil [])
|
||||||
|
(Bool [b bool])
|
||||||
|
(Int [n i64])
|
||||||
|
(Float [x f64])
|
||||||
|
(Text [s string])
|
||||||
|
(Key [s string])
|
||||||
|
(List [items (Vec Value)])
|
||||||
|
(Table [entries (Map string Value)])])
|
||||||
|
|
||||||
|
;; One token in hand, and the cursor for whatever the token opens. A vector and
|
||||||
|
;; a map recurse; everything else is a leaf.
|
||||||
|
(defn read-value [c (Ptr edn/Cursor) t edn/Token] Value
|
||||||
|
(cond
|
||||||
|
(= (.kind t) edn/tok-bool)
|
||||||
|
(Value.Bool {.b (match (edn/bool-of t) (Some v) v None false)})
|
||||||
|
(= (.kind t) edn/tok-int)
|
||||||
|
(Value.Int {.n (match (edn/int-of t) (Some v) v None (i64 0))})
|
||||||
|
(= (.kind t) edn/tok-float)
|
||||||
|
(Value.Float {.x (match (edn/float-of t) (Some v) v None 0.0)})
|
||||||
|
(= (.kind t) edn/tok-string) (Value.Text {.s (string (.text t))})
|
||||||
|
(= (.kind t) edn/tok-keyword) (Value.Key {.s (string (.text t))})
|
||||||
|
(= (.kind t) edn/tok-symbol) (Value.Key {.s (string (.text t))})
|
||||||
|
|
||||||
|
(= (.kind t) edn/tok-vec-open)
|
||||||
|
(let [items (vec-new Value)
|
||||||
|
u (edn/next c)]
|
||||||
|
(while (and (edn/ok? c)
|
||||||
|
(!= (.kind u) edn/tok-vec-close)
|
||||||
|
(!= (.kind u) edn/tok-eof))
|
||||||
|
(push items (read-value c u))
|
||||||
|
(set u (edn/next c)))
|
||||||
|
(Value.List {.items items}))
|
||||||
|
|
||||||
|
;; A map's key is whatever token is there — a keyword here, and its text
|
||||||
|
;; slice is the key. The value is read by the same recursion, so a map of
|
||||||
|
;; vectors of maps is one call per level and no special case.
|
||||||
|
(= (.kind t) edn/tok-map-open)
|
||||||
|
(let [entries (map-new string Value)
|
||||||
|
k (edn/next c)]
|
||||||
|
(while (and (edn/ok? c)
|
||||||
|
(!= (.kind k) edn/tok-map-close)
|
||||||
|
(!= (.kind k) edn/tok-eof))
|
||||||
|
(let [v (edn/next c)]
|
||||||
|
(put entries (string (.text k)) (read-value c v)))
|
||||||
|
(set k (edn/next c)))
|
||||||
|
(Value.Table {.entries entries}))
|
||||||
|
|
||||||
|
:else Value.Nil))
|
||||||
|
|
||||||
|
;; Walking it back. (at v i) addresses an element in place and (get m k)
|
||||||
|
;; answers a copy of the value's bytes; in a region the two are the same thing,
|
||||||
|
;; an alias into storage nobody individually owns, so a document is read back
|
||||||
|
;; with the operations that were already there.
|
||||||
|
(defn count-leaves [v Value] i32
|
||||||
|
(match v
|
||||||
|
(List items)
|
||||||
|
(let [n 0]
|
||||||
|
(dotimes [i (len items)]
|
||||||
|
(set n (+ n (count-leaves (at items i)))))
|
||||||
|
n)
|
||||||
|
;; map-next! fills an out-parameter with a copy of the value's bytes,
|
||||||
|
;; which for a Value holding a container is a second header over the same
|
||||||
|
;; block. In a region that is an alias and not a second owner — nothing
|
||||||
|
;; here owns anything, the arena does — so walking a map is the ordinary
|
||||||
|
;; iteration and needs no accessor of its own.
|
||||||
|
(Table entries)
|
||||||
|
(let [n 0
|
||||||
|
cur (i64 0)
|
||||||
|
k ""
|
||||||
|
v Value.Nil]
|
||||||
|
(while (map-next! entries (addr cur) (addr k) (addr v))
|
||||||
|
(set n (+ n (count-leaves v))))
|
||||||
|
n)
|
||||||
|
_ 1))
|
||||||
|
|
||||||
|
(defn sum-ints [v Value] i64
|
||||||
|
(match v
|
||||||
|
(Int n) n
|
||||||
|
(List items)
|
||||||
|
(let [t (i64 0)]
|
||||||
|
(dotimes [i (len items)]
|
||||||
|
(set t (+ t (sum-ints (at items i)))))
|
||||||
|
t)
|
||||||
|
(Table entries)
|
||||||
|
(match (get entries "xs") (Some x) (sum-ints x) None (i64 0))
|
||||||
|
_ (i64 0)))
|
||||||
|
|
||||||
|
(defn describe [v Value] string
|
||||||
|
(match v
|
||||||
|
Nil "nil" (Bool _b) "bool" (Int _n) "int" (Float _x) "float"
|
||||||
|
(Text _s) "string" (Key _s) "keyword" (List _i) "vector" (Table _e) "map"))
|
||||||
|
|
||||||
|
(defn read-doc [src string] Value
|
||||||
|
(let [b (bytes src)
|
||||||
|
c (edn/cursor b)
|
||||||
|
t (edn/next (addr c))]
|
||||||
|
(read-value (addr c) t)))
|
||||||
|
|
||||||
|
(defconst doc
|
||||||
|
"{:name \"level-1\"
|
||||||
|
:xs [1 2 3]
|
||||||
|
:spawns [{:kind :grunt :at [10 20]}
|
||||||
|
{:kind :boss :at [30 40]}]
|
||||||
|
:gravity 9.8
|
||||||
|
:looping true}")
|
||||||
|
|
||||||
|
(defn main [] i32
|
||||||
|
(set frame (arena-new 65536))
|
||||||
|
(with-allocator frame
|
||||||
|
(let [v (read-doc doc)]
|
||||||
|
(println (describe v))
|
||||||
|
(println (count-leaves v))
|
||||||
|
(println (sum-ints v))
|
||||||
|
(match v
|
||||||
|
(Table entries)
|
||||||
|
(match (get entries "name")
|
||||||
|
(Some n) (println (describe n))
|
||||||
|
None (println "missing"))
|
||||||
|
_ (println "not a map"))))
|
||||||
|
;; The whole document, in one operation and with no per-element teardown.
|
||||||
|
(free-all frame)
|
||||||
|
(arena-destroy frame)
|
||||||
|
0)
|
||||||
109
test/programs/arena-region.flan
Normal file
109
test/programs/arena-region.flan
Normal file
@ -0,0 +1,109 @@
|
|||||||
|
;;;; spec-memory.md's arena rule, which is the run-time half of what replaced
|
||||||
|
;;;; the three type-level refusals a container of owning elements used to meet.
|
||||||
|
;;;;
|
||||||
|
;;;; "Constructing a container whose element type owns storage, against an
|
||||||
|
;;;; allocator that lacks can-free, is refused at the point of construction:
|
||||||
|
;;;; one branch per container, not per element." One branch and not a walk,
|
||||||
|
;;;; because the alternative is something that inspects the graph at release,
|
||||||
|
;;;; and that is the registry of destructors the frame tier's reset exists to
|
||||||
|
;;;; not have.
|
||||||
|
;;;;
|
||||||
|
;;;; It is a run-time branch and not a compile-time refusal because there is
|
||||||
|
;;;; nothing static to refuse against: with-allocator rebinds a dynamic
|
||||||
|
;;;; variable, so which tier a (vec-new) meets is not knowable where it is
|
||||||
|
;;;; written. The compiler decides only whether to *ask*.
|
||||||
|
;;;;
|
||||||
|
;;;; Argument 0 is everything that must work, argument 1 and argument 2 are the
|
||||||
|
;;;; two ways this dies. Each death is the whole test of its case, so they are
|
||||||
|
;;;; separate runs rather than one program that could pass by dying early.
|
||||||
|
|
||||||
|
(defvar frame Allocator)
|
||||||
|
|
||||||
|
(defalias Row (Vec i32))
|
||||||
|
|
||||||
|
(defdata Value [Nil (Int [n i64]) (List [items (Vec Value)])])
|
||||||
|
|
||||||
|
(defn main [args [string]] i32
|
||||||
|
(set frame (arena-new 4096))
|
||||||
|
(let [which (if (> (len args) 1) (i32 (bytes->i64 (bytes (at args 1)))) 0)]
|
||||||
|
(cond
|
||||||
|
(= which 1)
|
||||||
|
;; The refusal. The context here is the heap, which can free one
|
||||||
|
;; block, and a (Vec Value) against it is a free that would release
|
||||||
|
;; the slots and strand every inner Vec — so the construction dies
|
||||||
|
;; rather than the free three hundred lines later.
|
||||||
|
(let [bad (vec-new Value)]
|
||||||
|
(println (len bad)))
|
||||||
|
|
||||||
|
(= which 2)
|
||||||
|
;; Use after free-all, which is a different mechanism and worth
|
||||||
|
;; pinning separately: the allocator's epoch moves on every free-all
|
||||||
|
;; and every container records the epoch it was made at. The header
|
||||||
|
;; below was copied *out* of the arena container into a local before
|
||||||
|
;; the release, which is the case the check has to cover and the
|
||||||
|
;; reason spec-memory.md makes an Allocator a pointer rather than a
|
||||||
|
;; copied value — a copied allocator would carry its own epoch and
|
||||||
|
;; the copy would never notice.
|
||||||
|
(let [outer (vec-new Value frame)]
|
||||||
|
(let [inner (vec-new Value frame)]
|
||||||
|
(push inner (Value.Int {.n (i64 7)}))
|
||||||
|
(push outer (Value.List {.items inner})))
|
||||||
|
(match (at outer 0)
|
||||||
|
(List items)
|
||||||
|
(do (println (len items))
|
||||||
|
(free-all frame)
|
||||||
|
(println (len items)))
|
||||||
|
_ (println 0)))
|
||||||
|
|
||||||
|
(= which 3)
|
||||||
|
;; ZII, which is the hole a guard only at the construction would have
|
||||||
|
;; left. The items field is omitted from the literal, so it is a zeroed
|
||||||
|
;; Vec with no allocator at all — it never went near (vec-new) — and
|
||||||
|
;; the first push is what adopts the context. So the branch is emitted
|
||||||
|
;; at every growth too, and there it asks the container, which answers
|
||||||
|
;; from the allocator it will adopt when it has none of its own.
|
||||||
|
(let [v (Value.List {})]
|
||||||
|
(match v
|
||||||
|
(List items)
|
||||||
|
(do (push items (Value.Int {.n (i64 1)}))
|
||||||
|
(println (len items)))
|
||||||
|
_ (println 0)))
|
||||||
|
|
||||||
|
:else
|
||||||
|
(do
|
||||||
|
;; The control, and it is the case the frame tier exists for: a
|
||||||
|
;; (Vec (Vec i32)) owns storage at two levels and is perfectly happy
|
||||||
|
;; in a region, because free-all releases every block the region
|
||||||
|
;; handed out and the inner ones are among them. The rule asks about
|
||||||
|
;; the *allocator*, never "does this element own anything", so this
|
||||||
|
;; must be built without complaint.
|
||||||
|
(with-allocator frame
|
||||||
|
(let [rows (vec-new Row)]
|
||||||
|
(let [row (vec-new i32)]
|
||||||
|
(push row 1)
|
||||||
|
(push row 2)
|
||||||
|
(push rows row))
|
||||||
|
(println (len rows))
|
||||||
|
(println (len (at rows 0)))))
|
||||||
|
(free-all frame)
|
||||||
|
;; And the same container against the heap dies — asserted from the
|
||||||
|
;; other side in run 1 above; here the point is only that the region
|
||||||
|
;; run above got no complaint.
|
||||||
|
(with-allocator frame
|
||||||
|
(let [vs (vec-new Value)]
|
||||||
|
(push vs (Value.Int {.n (i64 41)}))
|
||||||
|
(println (len vs))))
|
||||||
|
(free-all frame)
|
||||||
|
;; And the zeroed field of run 3, this time in the region: the growth
|
||||||
|
;; guard has to pass here as surely as it has to fail there, or every
|
||||||
|
;; ZII container in an arena would be unusable.
|
||||||
|
(with-allocator frame
|
||||||
|
(let [v (Value.List {})]
|
||||||
|
(match v
|
||||||
|
(List items)
|
||||||
|
(do (push items (Value.Int {.n (i64 1)}))
|
||||||
|
(println (len items)))
|
||||||
|
_ (println 0))))
|
||||||
|
(free-all frame))))
|
||||||
|
(arena-destroy frame)
|
||||||
|
0)
|
||||||
91
test/programs/arena-value.flan
Normal file
91
test/programs/arena-value.flan
Normal file
@ -0,0 +1,91 @@
|
|||||||
|
;;;; The recursive dynamic value, held in an arena and released by one
|
||||||
|
;;;; free-all. A reader handed no target struct type has to answer *something*,
|
||||||
|
;;;; and the something is this: a data type naming itself through a (Vec Value)
|
||||||
|
;;;; and a (Map string Value).
|
||||||
|
;;;;
|
||||||
|
;;;; Five refusals used to stand between here and a type like this, and every
|
||||||
|
;;;; one of them gave the same reason: the type-erased runtime copies and
|
||||||
|
;;;; releases slots bytewise, so a free would release the slots and leave what
|
||||||
|
;;;; they point at stranded. That reason is about *teardown*, and an arena has
|
||||||
|
;;;; none — free-all takes the whole region, and the inner blocks are in it
|
||||||
|
;;;; because they came out of it. So the refusals moved from the type, where
|
||||||
|
;;;; the allocator is not knowable, to the construction, where it is a value.
|
||||||
|
;;;;
|
||||||
|
;;;; There is no drop, no destructor, no finalizer and no per-element teardown
|
||||||
|
;;;; anywhere below. The release at the bottom of main is one call.
|
||||||
|
|
||||||
|
(defvar frame Allocator)
|
||||||
|
|
||||||
|
(defdata Value
|
||||||
|
[(Nil [])
|
||||||
|
(Int [n i64])
|
||||||
|
(Text [s string])
|
||||||
|
(List [items (Vec Value)])
|
||||||
|
(Table [entries (Map string Value)])])
|
||||||
|
|
||||||
|
;; [0 1 .. n-1] as a dynamic list. No allocator is named: with-allocator in
|
||||||
|
;; main has rebound the context, and spec-memory.md puts the allocator in the
|
||||||
|
;; calling convention precisely so that a builder like this need not carry one
|
||||||
|
;; through its signature.
|
||||||
|
(defn number-list [n i32] Value
|
||||||
|
(let [items (vec-new Value)]
|
||||||
|
(dotimes [i n]
|
||||||
|
(push items (Value.Int {.n (i64 i)})))
|
||||||
|
(Value.List {.items items})))
|
||||||
|
|
||||||
|
;; A table whose values are themselves lists, so the graph is three levels
|
||||||
|
;; deep before it reaches a leaf: Table -> Vec -> List -> Vec -> Int.
|
||||||
|
(defn a-table [] Value
|
||||||
|
(let [entries (map-new string Value)]
|
||||||
|
(put entries "xs" (number-list 3))
|
||||||
|
(put entries "ys" (number-list 5))
|
||||||
|
(put entries "name" (Value.Text {.s "edn"}))
|
||||||
|
(Value.Table {.entries entries})))
|
||||||
|
|
||||||
|
;; Reading it back. (at v i) addresses the element in place and (get m k)
|
||||||
|
;; answers a copy of the value's bytes, and in a region both are the same
|
||||||
|
;; thing: an alias into storage nobody individually owns. That is the bargain
|
||||||
|
;; a region is, and it is why no accessor beyond the two already here is
|
||||||
|
;; needed to walk a parsed document.
|
||||||
|
(defn total [v Value] i64
|
||||||
|
(match v
|
||||||
|
(Int n) n
|
||||||
|
(List items)
|
||||||
|
(let [t (i64 0)]
|
||||||
|
(dotimes [i (len items)]
|
||||||
|
(set t (+ t (total (at items i)))))
|
||||||
|
t)
|
||||||
|
(Table entries)
|
||||||
|
(+ (match (get entries "xs") (Some x) (total x) None (i64 0))
|
||||||
|
(match (get entries "ys") (Some y) (total y) None (i64 0)))
|
||||||
|
_ (i64 0)))
|
||||||
|
|
||||||
|
(defn build [] i64
|
||||||
|
(let [outer (vec-new Value)]
|
||||||
|
(dotimes [i 3]
|
||||||
|
(push outer (number-list (+ i 2))))
|
||||||
|
(push outer (a-table))
|
||||||
|
(push outer Value.Nil)
|
||||||
|
(println (len outer))
|
||||||
|
(let [t (i64 0)]
|
||||||
|
(dotimes [i (len outer)]
|
||||||
|
(set t (+ t (total (at outer i)))))
|
||||||
|
t)))
|
||||||
|
|
||||||
|
(defn main [] i32
|
||||||
|
(set frame (arena-new 65536))
|
||||||
|
(with-allocator frame
|
||||||
|
(println (build)))
|
||||||
|
;; The whole graph, in one operation. Every Vec block, every Map block and
|
||||||
|
;; every string the values point at came out of this region, so this is all
|
||||||
|
;; of it — and the epoch moves, so anything still holding one of those
|
||||||
|
;; headers traps rather than reading released bytes.
|
||||||
|
(free-all frame)
|
||||||
|
;; And the region is reusable, which is what makes it the frame tier: the
|
||||||
|
;; pages stayed, the offset went back to zero, and a second document builds
|
||||||
|
;; in the same bytes the first one used.
|
||||||
|
(with-allocator frame
|
||||||
|
(println (build)))
|
||||||
|
(free-all frame)
|
||||||
|
(arena-destroy frame)
|
||||||
|
0)
|
||||||
@ -1,10 +0,0 @@
|
|||||||
;;;; A Vec of a Vec is representable and would be wrong. The runtime is
|
|
||||||
;;;; type-erased: it copies and releases elements bytewise, so `clone` would
|
|
||||||
;;;; duplicate the inner headers instead of copying what they own, and `free`
|
|
||||||
;;;; would drop their buffers on the floor. spec-memory.md makes clone a deep
|
|
||||||
;;;; copy and makes free recurse structurally into owning fields; recursive
|
|
||||||
;;;; teardown is what `drop` brings, and this is refused until it does rather
|
|
||||||
;;;; than shipping the shallow answer under the deep name.
|
|
||||||
(defn rows [xs (Vec (Vec i32))] i32 0)
|
|
||||||
|
|
||||||
(defn main [] i32 0)
|
|
||||||
@ -407,6 +407,17 @@ let () =
|
|||||||
name m needle
|
name m needle
|
||||||
end
|
end
|
||||||
in
|
in
|
||||||
|
(* The other half of [refuses_src], for a declaration that used to be
|
||||||
|
refused and is not any more: "it compiles" is the whole claim, and a
|
||||||
|
row that only ever asserted the refusal would have been deleted rather
|
||||||
|
than inverted, which loses the record of what changed. *)
|
||||||
|
let accepts_src name src =
|
||||||
|
match Check.program (Parse.program (Reader.read_all ~file:"<accepts>" src)) with
|
||||||
|
| _ -> ()
|
||||||
|
| exception Loc.Error { Loc.dmsg = m; _ } ->
|
||||||
|
incr failures;
|
||||||
|
Printf.printf "FAIL %s\n it was refused: %S\n" name m
|
||||||
|
in
|
||||||
(* The name is still a quoted symbol, and now it is the *first* of several
|
(* The name is still a quoted symbol, and now it is the *first* of several
|
||||||
things, so an unquoted one has to say what the form is rather than read
|
things, so an unquoted one has to say what the form is rather than read
|
||||||
as a call with a spare argument. *)
|
as a call with a spare argument. *)
|
||||||
@ -464,6 +475,95 @@ let () =
|
|||||||
outputs "allocators" "programs/allocators.flan" allocators_out;
|
outputs "allocators" "programs/allocators.flan" allocators_out;
|
||||||
outputs ~opt:"-O0" "allocators, -O0" "programs/allocators.flan" allocators_out;
|
outputs ~opt:"-O0" "allocators, -O0" "programs/allocators.flan" allocators_out;
|
||||||
outputs ~dev:true "allocators, dev" "programs/allocators.flan" allocators_out;
|
outputs ~dev:true "allocators, dev" "programs/allocators.flan" allocators_out;
|
||||||
|
|
||||||
|
(* The recursive dynamic value in an arena, spec-memory.md's arena rule and
|
||||||
|
the thing it exists to make possible: a data type naming itself through a
|
||||||
|
(Vec Value) and a (Map string Value), built several levels deep, read
|
||||||
|
back, and released by one free-all with no per-element teardown
|
||||||
|
anywhere. The five refusals that used to stand between here and a type
|
||||||
|
like this were all about *teardown*, and a region has none.
|
||||||
|
|
||||||
|
The numbers are the assertion that a run which did nothing cannot pass:
|
||||||
|
five top-level values, 23 summed across every leaf in the graph. Printed
|
||||||
|
twice because the second build happens in the region the first one was
|
||||||
|
released from — free-all is retain-capacity, so the same bytes hold the
|
||||||
|
second document, and a stale header surviving the reset would show up
|
||||||
|
as a different total rather than as nothing at all. *)
|
||||||
|
let arena_value_out = "5\n23\n5\n23\n" in
|
||||||
|
outputs "a dynamic value in an arena" "programs/arena-value.flan"
|
||||||
|
arena_value_out;
|
||||||
|
outputs ~opt:"-O0" "a dynamic value in an arena, -O0"
|
||||||
|
"programs/arena-value.flan" arena_value_out;
|
||||||
|
outputs ~dev:true "a dynamic value in an arena, dev"
|
||||||
|
"programs/arena-value.flan" arena_value_out;
|
||||||
|
|
||||||
|
(* And the same thing over a real document, which is what the arena route
|
||||||
|
was taken for: the EDN tokenizer is a non-allocating cursor over a
|
||||||
|
[u8], and the reader above it builds a (Vec Value) and a
|
||||||
|
(Map string Value) against whichever allocator the *caller* bound. It
|
||||||
|
takes no allocator parameter and names none — spec-memory.md puts the
|
||||||
|
allocator in the calling convention, so (with-allocator a (read-doc s))
|
||||||
|
is the whole of "read-edn taking an allocator", and there is no new
|
||||||
|
machinery to add for it.
|
||||||
|
|
||||||
|
The numbers are structural: "map" is the document's shape, 12 is every
|
||||||
|
leaf in it, 6 is [1 2 3] summed, and "string" is :name's value read back
|
||||||
|
through the map. A reader that flattened a level or dropped a nested
|
||||||
|
map would miss on the leaf count. *)
|
||||||
|
let arena_edn_out = "map\n12\n6\nstring\n" in
|
||||||
|
outputs "an EDN document in an arena" "programs/arena-edn.flan"
|
||||||
|
arena_edn_out;
|
||||||
|
outputs ~opt:"-O0" "an EDN document in an arena, -O0"
|
||||||
|
"programs/arena-edn.flan" arena_edn_out;
|
||||||
|
|
||||||
|
(* And the branch that makes it safe, which needs a program that dies to
|
||||||
|
say anything — the shape bounds.flan uses, and for the same reason.
|
||||||
|
Run 0 is the control and must not trap: a (Vec (Vec i32)) in the region
|
||||||
|
is exactly the nested-container case the frame tier exists for, and the
|
||||||
|
rule asks about the allocator rather than about what the element owns,
|
||||||
|
so it has to be built without complaint. *)
|
||||||
|
let region ?opt () =
|
||||||
|
let exe = compile ?opt "programs/arena-region.flan" in
|
||||||
|
let code, text = run exe (Some "0") in
|
||||||
|
if text <> "1\n2\n1\n1\n" || code <> 0 then begin
|
||||||
|
incr failures;
|
||||||
|
Printf.printf
|
||||||
|
"FAIL nested containers in a region\n got: %S (exit %d)\n"
|
||||||
|
text code
|
||||||
|
end;
|
||||||
|
let traps name arg reason =
|
||||||
|
let code, text = run exe (Some arg) in
|
||||||
|
if code <> 134
|
||||||
|
|| not (contains text "programs/arena-region.flan:")
|
||||||
|
|| not (contains text reason)
|
||||||
|
then begin
|
||||||
|
incr failures;
|
||||||
|
Printf.printf
|
||||||
|
"FAIL %s\n got: %S (exit %d)\n wanted: %S (exit 134)\n"
|
||||||
|
name text code reason
|
||||||
|
end
|
||||||
|
in
|
||||||
|
(* At the construction, and not at the free it would have gone wrong in:
|
||||||
|
one branch per container, where the allocator is still a value the
|
||||||
|
site is holding. *)
|
||||||
|
traps "a container of owning elements against the heap" "1"
|
||||||
|
"this allocator can free one block";
|
||||||
|
(* A different mechanism, pinned separately: the epoch, and specifically
|
||||||
|
an inner header copied *out* of its container before the release. It
|
||||||
|
traps because an Allocator is a pointer — a copied-by-value one would
|
||||||
|
carry its own epoch and the copy would never notice the bump. *)
|
||||||
|
traps "an inner header used after free-all" "2"
|
||||||
|
"this container's allocator was released";
|
||||||
|
(* And the hole a guard only at the construction would have left: ZII
|
||||||
|
means a container can exist without ever reaching (vec-new), and the
|
||||||
|
first push is what adopts the context. Pinned from both sides — run 0
|
||||||
|
above grows the same zeroed field in a region and must not trap. *)
|
||||||
|
traps "a zeroed field of owning elements grown against the heap" "3"
|
||||||
|
"this allocator can free one block";
|
||||||
|
(try Sys.remove exe with Sys_error _ -> ())
|
||||||
|
in
|
||||||
|
region ();
|
||||||
|
region ~opt:"-O0" ();
|
||||||
(* The allocation registry, NEXT.md. Two expectations rather than one, and
|
(* The allocation registry, NEXT.md. Two expectations rather than one, and
|
||||||
the difference between them *is* the assertion: a dev build answers for
|
the difference between them *is* the assertion: a dev build answers for
|
||||||
an address at each of the three tiers and a release build answers 0 to
|
an address at each of the three tiers and a release build answers 0 to
|
||||||
@ -1764,16 +1864,19 @@ let () =
|
|||||||
there is nothing to infer from — and guessing is the alternative. *)
|
there is nothing to infer from — and guessing is the alternative. *)
|
||||||
refuses "vec-new with nothing saying what of" "programs/vec-untyped.flan"
|
refuses "vec-new with nothing saying what of" "programs/vec-untyped.flan"
|
||||||
"write the element type";
|
"write the element type";
|
||||||
(* The two shapes ownership is not transitive through yet. Each is refused
|
(* The shape ownership is still not transitive through. A global used to be
|
||||||
where it is declared, naming drop as what it waits on, rather than
|
one of these and a Vec of a Vec used to be another; neither is now. The
|
||||||
accepted into a path that would copy a header and hand out a second
|
global's rule is [Check.global_borrow] — see "a global Vec" above — and
|
||||||
owner. A global used to be the third; it is not any more, and the
|
the Vec of a Vec is a run-time question about the allocator instead, so
|
||||||
program that was this row is now an accepted one — see "a global Vec"
|
its program runs rather than being refused (programs/arena-region.flan).
|
||||||
above, and [Check.global_borrow] for the rule that replaced it. *)
|
|
||||||
|
This one stays, and the narrowing is exactly why: a [(Vec u8)] field
|
||||||
|
holds elements that own nothing, so nothing forces it into a region,
|
||||||
|
and two copies of the struct would be two headers over one heap buffer.
|
||||||
|
A container whose *elements* own storage is the case that is admitted,
|
||||||
|
because that one can only have been built against a region. *)
|
||||||
refuses "a struct field that owns a Vec" "programs/vec-in-struct.flan"
|
refuses "a struct field that owns a Vec" "programs/vec-in-struct.flan"
|
||||||
"a struct that owns one is move-only too";
|
"a struct that owns one is move-only too";
|
||||||
refuses "a Vec of a Vec" "programs/vec-of-vec.flan"
|
|
||||||
"copies and releases elements bytewise";
|
|
||||||
(* And it does not cross to C: the shim would flatten a header that owns
|
(* And it does not cross to C: the shim would flatten a header that owns
|
||||||
storage. Refused by the shim generator, where the message can say what
|
storage. Refused by the shim generator, where the message can say what
|
||||||
to pass instead. *)
|
to pass instead. *)
|
||||||
@ -2287,8 +2390,13 @@ ERR@7 unexpected token: not the kind the caller was reading
|
|||||||
"(defn f [m (Map f32 i32)] () 0)" "is not a map key";
|
"(defn f [m (Map f32 i32)] () 0)" "is not a map key";
|
||||||
refuses_src "a Ptr is not a map key"
|
refuses_src "a Ptr is not a map key"
|
||||||
"(defn f [m (Map (Ptr i32) i32)] () 0)" "hash an address";
|
"(defn f [m (Map (Ptr i32) i32)] () 0)" "hash an address";
|
||||||
refuses_src "a map value may not own storage"
|
(* A map value that owns storage is no longer refused at the type: that
|
||||||
"(defn f [m (Map i32 (Vec i32))] () 0)" "holds a move-only value";
|
refusal was about teardown, and which tier the map will meet is not
|
||||||
|
knowable where its type is written. What it became is a branch on the
|
||||||
|
allocator at (map-new) — programs/arena-region.flan. The key half is
|
||||||
|
untouched and is the two rows above. *)
|
||||||
|
accepts_src "a map value may own storage"
|
||||||
|
"(defn f [m (Map i32 (Vec i32))] () 0)";
|
||||||
refuses_src "a map value may not be ()"
|
refuses_src "a map value may not be ()"
|
||||||
"(defn f [m (Map i32 ())] () 0)" "cannot be ()";
|
"(defn f [m (Map i32 ())] () 0)" "cannot be ()";
|
||||||
refuses_src "map-new with nothing to say what it maps"
|
refuses_src "map-new with nothing to say what it maps"
|
||||||
|
|||||||
@ -970,10 +970,49 @@ let () =
|
|||||||
~needle:"exactly one type";
|
~needle:"exactly one type";
|
||||||
rejects_check "Pool takes one type" "(defn f [x (Pool i32 i32)] ())"
|
rejects_check "Pool takes one type" "(defn f [x (Pool i32 i32)] ())"
|
||||||
~needle:"exactly one type";
|
~needle:"exactly one type";
|
||||||
(* A pool of an owning element, refused where a Vec of a Vec is refused and
|
(* A pool of an owning element used to be refused here, with the Vec's and
|
||||||
for the same reason: the runtime copies and releases slots bytewise. *)
|
the Map's, and the three came down together: the reason all of them gave
|
||||||
rejects_check "a pool of a Vec"
|
was teardown, and a region has none. What replaced them is a run-time
|
||||||
"(defn f [x (Pool (Vec i32))] ())" ~needle:"move-only element";
|
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
|
||||||
|
see: which declarations are admitted, and which are still refused. The
|
||||||
|
run-time half — the branch that decides whether a given construction site
|
||||||
|
met a region allocator — is programs/arena-region.flan, because it needs
|
||||||
|
a program that dies to say anything. *)
|
||||||
|
(* The recursive dynamic value, which is the whole point: a union naming
|
||||||
|
itself through a container. Admitted because such a container can only
|
||||||
|
have been built against a region, and one free-all takes the graph. *)
|
||||||
|
accepts "a data type case holding a Vec of itself"
|
||||||
|
"(defdata Value [Nil (List [items (Vec Value)])])";
|
||||||
|
accepts "a data type case holding a Map of itself"
|
||||||
|
"(defdata Value [Nil (Table [entries (Map string Value)])])";
|
||||||
|
(* And the narrowing is exact, which is what these two are for. A container
|
||||||
|
whose elements own *nothing* is not forced into a region by anything, so
|
||||||
|
it would sit in a copyable aggregate on the heap with two headers and one
|
||||||
|
buffer between them — the double free the original refusal existed to
|
||||||
|
prevent. It stays refused, in a struct and in a union alike. *)
|
||||||
|
rejects_check "a data type case holding a plain Vec"
|
||||||
|
"(defdata Value [Nil (Bytes [bs (Vec u8)])])"
|
||||||
|
~needle:"makes the data type move-only";
|
||||||
|
rejects_check "a struct field holding a plain Vec"
|
||||||
|
"(defstruct B [buf (Vec u8)])"
|
||||||
|
~needle:"a struct that owns one is move-only too";
|
||||||
|
(* free does not recurse and does not quietly release the outer block: it
|
||||||
|
names free-all, which is the operation that actually releases the graph. *)
|
||||||
|
rejects_check "free on a container of owning elements"
|
||||||
|
"(defdata V [Nil (L [xs (Vec V)])])\n\
|
||||||
|
(defn f [v (Vec V)] () (free v))"
|
||||||
|
~needle:"(free-all a) takes it";
|
||||||
|
(* clone is refused for a reason the region does *not* dissolve: it promises
|
||||||
|
an independent copy and a bytewise one is an alias. *)
|
||||||
|
rejects_check "clone on a container of owning elements"
|
||||||
|
"(defdata V [Nil (L [xs (Vec V)])])\n\
|
||||||
|
(defn f [v (Vec V)] () (let [c (clone v)] (free c)))"
|
||||||
|
~needle:"cannot be cloned";
|
||||||
|
|
||||||
(* ── A move-only global ─────────────────────────────────────────────
|
(* ── A move-only global ─────────────────────────────────────────────
|
||||||
Legal now, and legal because of one rule: reading one is always a borrow.
|
Legal now, and legal because of one rule: reading one is always a borrow.
|
||||||
|
|||||||
@ -117,6 +117,8 @@ let corpus =
|
|||||||
*no* argument reads args[1] of a one-element argv, which is a bug in
|
*no* argument reads args[1] of a one-element argv, which is a bug in
|
||||||
the harness rather than in anything under test. *)
|
the harness rather than in anything under test. *)
|
||||||
"programs/bounds.flan", [ "0" ];
|
"programs/bounds.flan", [ "0" ];
|
||||||
|
"programs/arena-value.flan", [];
|
||||||
|
"programs/arena-edn.flan", [];
|
||||||
"programs/bytes2.flan", [];
|
"programs/bytes2.flan", [];
|
||||||
"programs/cleanup.flan", [];
|
"programs/cleanup.flan", [];
|
||||||
"programs/conditions.flan", [];
|
"programs/conditions.flan", [];
|
||||||
|
|||||||
@ -183,8 +183,8 @@ let check label path args ~checks =
|
|||||||
- dev-* and reload-*, which need a host process or a dlopen harness.
|
- dev-* and reload-*, which need a host process or a dlopen harness.
|
||||||
- the compile-time refusals: nth-gone, pkg-hidden-main, pkg-two-aliases,
|
- the compile-time refusals: nth-gone, pkg-hidden-main, pkg-two-aliases,
|
||||||
pkg-two-mains, pkg-cycle, pkg-alias-clash, user-allocator, and the whole
|
pkg-two-mains, pkg-cycle, pkg-alias-clash, user-allocator, and the whole
|
||||||
vec-moved / vec-double-free / vec-in-struct / vec-global / vec-of-vec /
|
vec-moved / vec-double-free / vec-in-struct / vec-global / vec-to-c /
|
||||||
vec-to-c / vec-untyped family. These never produce a binary at all: the
|
vec-untyped family. These never produce a binary at all: the
|
||||||
checker refuses them, which is the point of them. There is nothing for
|
checker refuses them, which is the point of them. There is nothing for
|
||||||
memcheck to run.
|
memcheck to run.
|
||||||
- shadow-pkg.flan, which is a package fragment with no main and does not
|
- shadow-pkg.flan, which is a package fragment with no main and does not
|
||||||
@ -199,6 +199,7 @@ let check label path args ~checks =
|
|||||||
bugs this tool hunts, and a trap that stopped firing would be silent. *)
|
bugs this tool hunts, and a trap that stopped firing would be silent. *)
|
||||||
let corpus =
|
let corpus =
|
||||||
[ "programs/allocators.flan", [];
|
[ "programs/allocators.flan", [];
|
||||||
|
"programs/arena-value.flan", [];
|
||||||
"programs/bounds.flan", [ "0" ];
|
"programs/bounds.flan", [ "0" ];
|
||||||
"programs/bytes2.flan", [];
|
"programs/bytes2.flan", [];
|
||||||
"programs/cleanup.flan", [];
|
"programs/cleanup.flan", [];
|
||||||
|
|||||||
Loading…
x
Reference in New Issue
Block a user