Merge: Pool, the move-only concept, and the gen word follow the repeal
This commit is contained in:
commit
41a794c255
27
FIX.org
27
FIX.org
@ -256,3 +256,30 @@ NEXT.md are annotated at their live claims.
|
||||
Two of the day's fix lanes were cancelled with this (borrowed-flag, region
|
||||
element); the while-condition fix merged in the morning is deleted again by
|
||||
the repeal, and its pin with it.
|
||||
|
||||
* The second round, 2026-09-18 — Pool, move-only, and the gen word
|
||||
|
||||
Ordered by the author after the ownership repeal, on the same argument: the
|
||||
Odin position, full stop.
|
||||
|
||||
- Pool and (Handle T) are gone — types, checker arms, runtime section,
|
||||
fixtures. Two containers are enough; a slab with generational handles is a
|
||||
library over a Vec when a program wants one.
|
||||
- The move-only concept is gone: everything copies as its header, copyable?
|
||||
left the predicate list (four remain), and the struct/defdata/defunion
|
||||
owning-field refusals are lifted. The region rule stands untouched — a
|
||||
container of owning elements is still built against a region and released
|
||||
by one free-all.
|
||||
- The gen word left both container headers (read by nothing since it was
|
||||
written). A Vec is ptr len cap allocator epoch; the epoch trap stays.
|
||||
- Container globals keep both declaration rules, reworded: they start zeroed
|
||||
(a global initialiser is a compile-time constant, and a container's only
|
||||
constant is the empty one), and a defconst container is refused since a
|
||||
constant is not an assignable place. sand.flan's experiment line would now
|
||||
be refused with the reworded sentence.
|
||||
|
||||
Everything verified together: dune test --force 232/0 with zero suite FAILs,
|
||||
@x86 122 MATCH / 0 DIFFER, @sanitize clean, and the whole-repo check sweep
|
||||
against the parent differs only where it should: the two negative fixtures
|
||||
now accepted (vec-in-struct, the clause-less generics corpus), the two pool
|
||||
fixtures deleted.
|
||||
|
||||
4
NEXT.md
4
NEXT.md
@ -195,7 +195,7 @@ Worth stating because the notes elsewhere may still read the old way:
|
||||
an `Int`, a `Ptr`, an `Alloc` or a `Handle`, with aggregates leaving through an out-pointer, and
|
||||
`crossable` refuses an aggregate return from a `declare` outright. The refusal in `call_native` is
|
||||
unreachable and building sret behind it would have been *wrong* — that path is the C boundary, where
|
||||
SysV returns a 16-byte slice in `rax:rdx` rather than by hidden pointer. `Vec`, `Map` and `Pool` all
|
||||
SysV returns a 16-byte slice in `rax:rdx` rather than by hidden pointer. `Vec`, `Map` and `Pool` (since removed) all
|
||||
match; item 16's "unexercised" line was stale.
|
||||
- **The header check is not opt-in.** `vendor/raylib/raylib-5.5.h` is committed and
|
||||
`vendor/raylib/headers` names it directly. There is no `FLAN_RAYLIB_H`.
|
||||
@ -321,7 +321,7 @@ the easy half. What is left is conditions, and the measurement moved them from '
|
||||
doing first. Do that before item 1, not after.
|
||||
|
||||
3. **`Rt` with an aggregate return**, and with it most of the container runtime. `Vec`, `Map` and
|
||||
`Pool` have not been exercised through this backend at all.
|
||||
`Pool` (since removed) have not been exercised through this backend at all.
|
||||
|
||||
4. **`Fnval`'s indirection cell.** `FnAddr (Fnval n)` emits the symbol, which is right for a
|
||||
whole-program build and wrong the instant anything is redefined into it. There are no cells and no
|
||||
|
||||
@ -2910,6 +2910,16 @@ is still right: a union has a C layout and still may not cross to C by value, be
|
||||
|
||||
## `(Handle T)` and the pool, which is what a stale reference answers with
|
||||
|
||||
**Removed 2026-09-18**, in the second round of the repeal: two containers are
|
||||
enough, the corpus's only pools were its own fixtures, and a slab behind
|
||||
generational handles is a library over a `Vec` when a program wants one —
|
||||
which is where Odin keeps it. The `gen` word on `Vec` and `Map` went the same
|
||||
day (maintained, read by nothing; the header is `ptr len cap allocator
|
||||
epoch` now), and so did the move-only concept itself — everything copies, and
|
||||
`copyable?` left the predicate list. spec-memory.md, "The repeal", carries
|
||||
all three amendments. The section below is kept as the record of what was
|
||||
built.
|
||||
|
||||
A handle is a reference to something that can die, which reports that it died rather than silently resolving to
|
||||
whatever reused its slot. `check.ml` refused `(Handle T)` by name as milestone 6; this is what it stood for, and the
|
||||
pool came with it because the pool is what makes the report possible.
|
||||
|
||||
@ -144,8 +144,8 @@ The containers, strings/UTF-8, sequences, random, and printing layers are decent
|
||||
`flan_transfer_fail`, `flan_null_alloc_fail`, `flan_free_all_fail` → `rt_die`). Bounds
|
||||
and arithmetic already park via the break-loop hook; these should too.
|
||||
- **Unchecked `malloc` in `flan_argv`** (`flan_rt.c:162`) — the one in the file.
|
||||
- **`v->gen` stale-slice word is maintained and never consulted** (`flan_rt.c:1347`) —
|
||||
either implement the check or delete the field before someone trusts it.
|
||||
- ~~**`v->gen` stale-slice word is maintained and never consulted**~~ — deleted
|
||||
2026-09-18 with the second round of the repeal; the header is five words now.
|
||||
- **`flan_slurp_into` conflates elements and bytes and skips `flan_vec_check`**
|
||||
(`flan_rt.c:2746`) — safe only because check.ml pins slurp to `(Vec u8)`; a latent trap.
|
||||
- **`flan run` swallows build flags as program arguments** (`bin/main.ml:634-651`) —
|
||||
|
||||
680
lib/check.ml
680
lib/check.ml
@ -406,26 +406,20 @@ let unimplemented loc what milestone =
|
||||
|
||||
Odin's [where] clause is the same shape ([core/slice/slice.odin:289] is
|
||||
[where intrinsics.type_is_ordered(T)]) with forty-one predicates against
|
||||
these five. The fifth, [copyable?], has no Odin counterpart at all: Odin
|
||||
has no move semantics, so [$T] never has to answer the question. The prior
|
||||
art there is Rust's [T: Copy], with the difference that [copyable?] is a
|
||||
question the compiler answers rather than a trait a user implements. *)
|
||||
let predicate_names = [ "ordered?"; "equal?"; "hashable?"; "numeric?"; "copyable?" ]
|
||||
these four. There is no [copyable?] any more and no Odin counterpart
|
||||
either: Odin has no move semantics, and since the repeal neither does this
|
||||
language, so [$T] never has to answer the question. *)
|
||||
let predicate_names = [ "ordered?"; "equal?"; "hashable?"; "numeric?" ]
|
||||
|
||||
(* ── 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.
|
||||
The one structural ownership question that survived the repeal, because it
|
||||
is not about copying at all.
|
||||
|
||||
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,
|
||||
to reach and would not: a Vec or Map owns a block outright; an Option,
|
||||
a fixed array, a struct or a data type's case owns whatever its payload
|
||||
does.
|
||||
|
||||
@ -438,12 +432,11 @@ let predicate_names = [ "ordered?"; "equal?"; "hashable?"; "numeric?"; "copyable
|
||||
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. *)
|
||||
[env.unions], the untagged ones, are deliberately not consulted: nothing
|
||||
anywhere records which member of one is live, so there is no fact this
|
||||
walk could read — an untagged union is treated as owning nothing, and what
|
||||
its members point at is the program's, through whatever tag it keeps
|
||||
beside the union. *)
|
||||
let owning_fields env n =
|
||||
match Hashtbl.find_opt env.structs n with
|
||||
| Some s -> [ s.Tast.fields ]
|
||||
@ -454,7 +447,7 @@ let owning_fields env n =
|
||||
|
||||
let rec owning env ?(seen = []) (t : Types.t) =
|
||||
match t with
|
||||
| Types.Vec _ | Types.Map _ | Types.Pool _ -> true
|
||||
| Types.Vec _ | Types.Map _ -> true
|
||||
| Types.Option e | Types.Array (_, e) -> owning env ~seen e
|
||||
| Types.Named n ->
|
||||
not (List.mem n seen)
|
||||
@ -471,7 +464,7 @@ let rec owning env ?(seen = []) (t : Types.t) =
|
||||
value is the whole of the question there. *)
|
||||
let region_only env (t : Types.t) =
|
||||
match t with
|
||||
| Types.Vec e | Types.Pool e -> owning env e
|
||||
| Types.Vec e -> owning env e
|
||||
| Types.Map (_, v) -> owning env v
|
||||
| _ -> false
|
||||
|
||||
@ -488,23 +481,20 @@ let pred_holds p (t : Types.t) =
|
||||
[key_pair]. *)
|
||||
| "hashable?" -> Types.keyable t
|
||||
| "numeric?" -> Types.is_numeric t
|
||||
| "copyable?" -> not (Types.is_move_only t)
|
||||
| _ -> false
|
||||
|
||||
(* What one declared predicate *also* gives you. These are entailments over
|
||||
the type system as it stands, not conveniences: every type [is_comparable]
|
||||
admits is a number or an enum, so it is equatable and it is not move-only.
|
||||
The table is only sound while that is true — an ordered move-only type, or
|
||||
an ordered type with no [=], would make it wrong — so it lives in one place
|
||||
and says so. The gain is real ergonomics: [{:where (ordered? $t)}] is
|
||||
enough for a [sort!] that also compares and reads its elements twice,
|
||||
rather than three predicates on one line. *)
|
||||
admits is a number or an enum, so it is equatable. The table is only sound
|
||||
while that is true — an ordered type with no [=] would make it wrong — so
|
||||
it lives in one place and says so. The gain is real ergonomics:
|
||||
[{:where (ordered? $t)}] is enough for a [sort!] that also compares,
|
||||
rather than two predicates on one line. *)
|
||||
let pred_entails ~declared ~wanted =
|
||||
String.equal declared wanted
|
||||
|| match wanted, declared with
|
||||
| "ordered?", "numeric?" -> true
|
||||
| "equal?", ("numeric?" | "ordered?") -> true
|
||||
| "copyable?", ("numeric?" | "ordered?" | "equal?" | "hashable?") -> true
|
||||
| _ -> false
|
||||
|
||||
let declares preds v wanted =
|
||||
@ -518,27 +508,6 @@ let declares preds v wanted =
|
||||
properties are the Vec's. *)
|
||||
let tyvar_of (t : Types.t) = match t with Types.Var v -> Some v | _ -> None
|
||||
|
||||
(* ── Move-only, with a type variable defaulting to move ────────────────
|
||||
[Types.is_move_only (Var _)] is [false] and cannot be anything else: the
|
||||
same variable is [i32] at one instantiation and [(Vec i32)] at the next, so
|
||||
the property is not decidable abstractly. The author's decision is to
|
||||
default to **move**, because move is the *stricter* rule: assuming it can
|
||||
only refuse a program that would have been fine, never admit one that
|
||||
double-frees. [copyable?] is the opt-out, exactly as Rust's [T: Copy] is.
|
||||
|
||||
In the body this means a generic may not use a parameter twice without
|
||||
declaring [copyable?]. Since the repeal this gates the structural rules
|
||||
only — what a struct, union or pool may own — not any use of a binding.
|
||||
|
||||
A [Var] only ever survives the abstract pass. Inside an instantiation
|
||||
[env.subst] has made everything concrete, so this is [Types.is_move_only]
|
||||
there and the strictness costs nothing at a call site. *)
|
||||
let rec move_only preds (t : Types.t) =
|
||||
match t with
|
||||
| Types.Var v -> not (declares preds v "copyable?")
|
||||
| Types.Option e | Types.Array (_, e) -> move_only preds e
|
||||
| t -> Types.is_move_only t
|
||||
|
||||
(* ── (Map K V), spec-memory.md ──────────────────────────────────────────
|
||||
Both halves are checked where the type is written, not where an operation
|
||||
is, so that a map nothing ever uses is still refused if it cannot work.
|
||||
@ -567,8 +536,8 @@ let map_type ?(preds = []) loc (k : Types.t) (v : Types.t) =
|
||||
(* The key, as far as the type alone can say. A struct passes here and is
|
||||
decided at the operation, by [key_pair], which walks its fields — the
|
||||
struct table is not necessarily complete while a type is being resolved,
|
||||
and every map that exists reaches an operation anyway, because a global of
|
||||
move-only type is refused and a local needs (map-new). *)
|
||||
and every map that exists reaches an operation anyway, because a global
|
||||
map starts zeroed and a local needs (map-new). *)
|
||||
(* A type variable is a map key exactly when the [where] clause says it is
|
||||
hashable. Nothing else about it is knowable here, and falling through to
|
||||
[Types.keyable] would answer no for a variable that is about to be
|
||||
@ -664,27 +633,6 @@ let rec resolve env ?(seen = []) (t : Ast.texpr) : Types.t =
|
||||
(resolve env ~seen v)
|
||||
| "Map", _ -> fail loc "(Map K V) takes exactly two types"
|
||||
| "Result", _ -> unimplemented loc "(Result T E)" 6
|
||||
| "Pool", [ a ] ->
|
||||
let e = resolve env ~seen a in
|
||||
(* Lifted with the Vec's and pushed to the construction with it, and a
|
||||
pool is the one of the three where that is not quite the same trade,
|
||||
because a pool has a release point a Vec does not: [(release p h)]
|
||||
recycles one slot while the pool lives on. In a region that costs a
|
||||
block that stays allocated until [free-all] and is never handed back
|
||||
— the slot itself is reused, since the next insert overwrites those
|
||||
bytes, but whatever the dead element pointed at is stranded.
|
||||
|
||||
That is a region leak bounded by the region, which is the bargain a
|
||||
region already is: an arena's whole proposition is that nothing comes
|
||||
back before the reset. It is not the unbounded leak the heap would
|
||||
take, and it is not a use-after-free — nothing is released twice
|
||||
because nothing is released once. Said here rather than left for a
|
||||
reader to work out, because "reuse" is the word that makes a pool
|
||||
look different from a Vec and it deserves an answer. *)
|
||||
Types.Pool e
|
||||
| "Pool", _ -> fail loc "(Pool T) takes exactly one type"
|
||||
| "Handle", [ a ] -> Types.Handle (resolve env ~seen a)
|
||||
| "Handle", _ -> fail loc "(Handle T) takes exactly one type"
|
||||
| _ ->
|
||||
fail loc
|
||||
"%s takes no type arguments — generics are milestone 5" name)
|
||||
@ -857,8 +805,6 @@ let rec bind_ty subst (pat : Types.t) (arg : Types.t) =
|
||||
| Types.Slice p, Types.Slice a
|
||||
| Types.Ptr p, Types.Ptr a
|
||||
| Types.Vec p, Types.Vec a
|
||||
| Types.Pool p, Types.Pool a
|
||||
| Types.Handle p, Types.Handle a
|
||||
| Types.Option p, Types.Option a -> bind_ty subst p a
|
||||
| Types.Array (n, p), Types.Array (m, a) -> Int64.equal n m && bind_ty subst p a
|
||||
| Types.Map (k, v), Types.Map (k', v') ->
|
||||
@ -878,8 +824,6 @@ let rec subst_ty subst (t : Types.t) =
|
||||
| Types.Map (k, v) -> Types.Map (subst_ty subst k, subst_ty subst v)
|
||||
| Types.Ptr e -> Types.Ptr (subst_ty subst e)
|
||||
| Types.Vec e -> Types.Vec (subst_ty subst e)
|
||||
| Types.Pool e -> Types.Pool (subst_ty subst e)
|
||||
| Types.Handle e -> Types.Handle (subst_ty subst e)
|
||||
| Types.Option e -> Types.Option (subst_ty subst e)
|
||||
| Types.Fn (ps, r) -> Types.Fn (List.map (subst_ty subst) ps, subst_ty subst r)
|
||||
| t -> t
|
||||
@ -889,7 +833,7 @@ let rec generic_ty (t : Types.t) =
|
||||
match t with
|
||||
| Types.Var _ -> true
|
||||
| Types.Slice e | Types.Array (_, e) | Types.Ptr e | Types.Vec e
|
||||
| Types.Pool e | Types.Handle e | Types.Option e -> generic_ty e
|
||||
| Types.Option e -> generic_ty e
|
||||
| Types.Map (k, v) -> generic_ty k || generic_ty v
|
||||
| Types.Fn (ps, r) -> List.exists generic_ty ps || generic_ty r
|
||||
| _ -> false
|
||||
@ -933,8 +877,6 @@ let rec mangle_ty (t : Types.t) =
|
||||
| Types.Map (k, v) -> Printf.sprintf "map-%s-%s" (mangle_ty k) (mangle_ty v)
|
||||
| Types.Ptr e -> "ptr-" ^ mangle_ty e
|
||||
| Types.Vec e -> "vec-" ^ mangle_ty e
|
||||
| Types.Pool e -> "pool-" ^ mangle_ty e
|
||||
| Types.Handle e -> "handle-" ^ mangle_ty e
|
||||
| Types.Option e -> "opt-" ^ mangle_ty e
|
||||
| Types.Fn (ps, r) ->
|
||||
Printf.sprintf "fn-%s-to-%s"
|
||||
@ -972,7 +914,7 @@ let rec occurs_in ~needle (t : Types.t) =
|
||||
||
|
||||
match t with
|
||||
| Types.Slice e | Types.Array (_, e) | Types.Ptr e | Types.Vec e
|
||||
| Types.Pool e | Types.Handle e | Types.Option e -> occurs_in ~needle e
|
||||
| Types.Option e -> occurs_in ~needle e
|
||||
| Types.Map (k, v) -> occurs_in ~needle k || occurs_in ~needle v
|
||||
| Types.Fn (ps, r) ->
|
||||
List.exists (occurs_in ~needle) ps || occurs_in ~needle r
|
||||
@ -1251,7 +1193,6 @@ let region_sym (t : Types.t) =
|
||||
match t with
|
||||
| Types.Vec _ -> "flan_vec_region_only"
|
||||
| Types.Map _ -> "flan_map_region_only"
|
||||
| Types.Pool _ -> "flan_pool_region_only"
|
||||
| _ -> assert false
|
||||
|
||||
let region_check env loc (target : Tast.expr) (after : Tast.expr) =
|
||||
@ -1972,16 +1913,17 @@ and var ctx loc ~want name =
|
||||
| None -> captured ctx loc name;
|
||||
Loc.failk "check/unknown-name" loc "unknown name %s" name)
|
||||
|
||||
(* What remains of spec-memory.md's ownership section after the repeal of
|
||||
2026-09-18 is entirely in the types: move-only decides what may be copied,
|
||||
the struct/union/pool rules below decide what may own what, and the
|
||||
allocator's capability decides what a free means at run time. Which frees
|
||||
run, and in what order, is the program's own business — the same contract
|
||||
Odin ships with — and the dev build's generation words are the net under
|
||||
it. The flow analysis that used to live here (a per-function dead set, a
|
||||
borrow flag over container reads, a loop-iteration diff) tracked use-after-
|
||||
move and double-free statically; it was repealed rather than repaired when
|
||||
its holes proved structural. See spec-memory.md, "The repeal". *)
|
||||
(* What remains of spec-memory.md's ownership section after the repeals of
|
||||
2026-09-18 is the allocator's side alone: the region rule decides where a
|
||||
container of owning elements may be built, and the allocator's capability
|
||||
decides what a free means at run time. Everything copies — a container as
|
||||
its header, the copies aliasing one buffer — and which frees run, and in
|
||||
what order, is the program's own business, the same contract Odin ships
|
||||
with; the dev build's epoch words are the net under it. The flow analysis
|
||||
that used to live here (a per-function dead set, a borrow flag, a
|
||||
loop-iteration diff) went in the first repeal; the move-only concept
|
||||
itself — copy refusals, [copyable?], the struct/union owning rules — went
|
||||
in the second. See spec-memory.md, "The repeal". *)
|
||||
|
||||
(* [defer_ok] is granted again before *every* form, not once before the block:
|
||||
[check] withdraws it as it starts, so granting it once would let the first
|
||||
@ -3398,42 +3340,6 @@ and map_new_types ctx ~want loc args =
|
||||
"nothing here says what (map-new) maps — write the key and value \
|
||||
types, as (map-new string i32), or give the binding a type")
|
||||
|
||||
(* The element type for [pool-new]. The same rule [vec-new] uses and for the
|
||||
same reason: a [let] has no type annotation, so a local pool has nowhere
|
||||
else to say what it holds. *)
|
||||
and pool_new_elem ctx ~want loc args =
|
||||
let named =
|
||||
match args with
|
||||
| { Ast.e = Ast.Var n; _ } :: rest
|
||||
when lookup ctx n = None
|
||||
&& (not (Hashtbl.mem ctx.env.globals n))
|
||||
&& type_named ctx n ->
|
||||
Some (resolve_name ctx.env ~seen:[] loc n, rest)
|
||||
| _ -> None
|
||||
in
|
||||
match named with
|
||||
| Some (t, rest) ->
|
||||
if move_only ctx.env.tvpreds t then
|
||||
fail loc
|
||||
"(Pool %s) holds a move-only element, and the type-erased runtime \
|
||||
copies and releases slots bytewise. Recursive teardown arrives with \
|
||||
drop (step 5 in NEXT.md)"
|
||||
(Types.to_string t);
|
||||
t, rest
|
||||
| None ->
|
||||
(match want with
|
||||
| Some (Types.Pool t) -> t, args
|
||||
| _ ->
|
||||
fail loc
|
||||
"nothing here says what (pool-new) is a Pool of — write the element \
|
||||
type, as (pool-new Enemy), or give the binding a type")
|
||||
|
||||
(* The element type, or the reason this is not a Pool. *)
|
||||
and pool_elem loc what (t : Types.t) =
|
||||
match t with
|
||||
| Types.Pool e -> e
|
||||
| other -> fail loc "%s takes a (Pool T), found %s" what (Types.to_string other)
|
||||
|
||||
(* The element type, or the reason this is not a Vec. *)
|
||||
and vec_elem loc what (t : Types.t) =
|
||||
match t with
|
||||
@ -3925,9 +3831,9 @@ and named_call ctx ~want loc name args =
|
||||
(* spec-memory.md's first release point. Since the repeal, what it consumes
|
||||
it consumes at run time only: nothing marks the binding dead, so a second
|
||||
[free] or a read after this one type-checks and misbehaves at run time —
|
||||
the allocator aborts on a double free it can see, and the dev build's
|
||||
generation word traps a stale read. That is the Odin contract: free is a
|
||||
thing you write, and writing it twice is yours to not do. *)
|
||||
the allocator aborts on a double free it can see, and the epoch word
|
||||
traps a read through a released region. That is the Odin contract: free
|
||||
is a thing you write, and writing it twice is yours to not do. *)
|
||||
| "free" ->
|
||||
arity loc name 1 args;
|
||||
let target = check ctx (List.hd args) in
|
||||
@ -3955,7 +3861,7 @@ and named_call ctx ~want loc name args =
|
||||
container is region-allocated or it does not exist, so there is always a
|
||||
[free-all] to point at. *)
|
||||
(match target.Tast.ty with
|
||||
| (Types.Vec _ | Types.Map _ | Types.Pool _)
|
||||
| (Types.Vec _ | Types.Map _)
|
||||
when region_only ctx.env target.Tast.ty ->
|
||||
fail loc
|
||||
"%s holds elements that own storage, and free releases the block \
|
||||
@ -3973,27 +3879,12 @@ and named_call ctx ~want loc name args =
|
||||
expect loc ~want
|
||||
(rt loc Types.Unit "flan_map_free"
|
||||
[ target; size_of loc k; size_of loc v; here loc ])
|
||||
(* The owner, not a slot. Every handle into it is stale afterwards and
|
||||
answers None, which is a strictly better afterlife than a Vec's
|
||||
binding gets — that one is a compile error and this one is a run-time
|
||||
answer, because handles are copies and the checker cannot see them
|
||||
all. That asymmetry is the reason handles exist. *)
|
||||
| Types.Pool elem ->
|
||||
expect loc ~want
|
||||
(rt loc Types.Unit "flan_pool_free"
|
||||
[ target; size_of loc elem; align_of loc elem; here loc ])
|
||||
| Types.Handle _ ->
|
||||
fail loc
|
||||
"free takes the owner, and a handle owns nothing — it is a copyable \
|
||||
number, so consuming one copy would say nothing about the others. \
|
||||
(release p h) recycles one slot; (free p) releases the pool"
|
||||
| other ->
|
||||
(* A field is never freed on its own: it would leave its owner partly
|
||||
dead with no way to say so. *)
|
||||
fail loc
|
||||
"free takes a move-only value — a Vec, a Map, or a struct that owns \
|
||||
one — found %s. A resource type with a drop hook is step 5 and does \
|
||||
not exist yet"
|
||||
"free takes an owning container — a Vec or a Map — found %s. A \
|
||||
resource type with a drop hook is step 5 and does not exist yet"
|
||||
(Types.to_string other))
|
||||
(* (clone v) uses the current allocator, (clone v a) names one. A deep,
|
||||
independent copy: spec-memory.md's "copying is always explicit". *)
|
||||
@ -4064,18 +3955,6 @@ and named_call ctx ~want loc name args =
|
||||
(mk loc mty (Tast.Local d))
|
||||
[ size_of loc k; size_of loc v ] mty);
|
||||
mk loc mty (Tast.Local d) ])))
|
||||
(* Refused by name rather than falling through to "clone takes a
|
||||
(Vec T)". Copying a pool would duplicate every slot *and* every
|
||||
generation counter, so a handle into the original would resolve in
|
||||
the copy too — two live entities behind one identity, which is the
|
||||
exact confusion the type exists to prevent. If a program wants a
|
||||
second world it builds one and inserts into it, and the new handles
|
||||
say they are new. *)
|
||||
| Types.Pool _ ->
|
||||
fail loc
|
||||
"a pool cannot be cloned: the copy would carry the same slot \
|
||||
generations, so one handle would resolve in both and name two \
|
||||
different things. Build a second pool and insert into it"
|
||||
| _ ->
|
||||
let elem = vec_elem loc "clone" target.Tast.ty in
|
||||
let d = fresh_slot ctx (Types.Vec elem) in
|
||||
@ -4095,219 +3974,6 @@ and named_call ctx ~want loc name args =
|
||||
mk loc (Types.Vec elem) (Tast.Local d) ]))))
|
||||
| _ -> fail loc "clone is (clone v) or (clone v allocator)")
|
||||
|
||||
(* ── (Pool T) and (Handle T), spec-memory.md ───────────────────── *)
|
||||
(* The same type-erased shape the Vec has, for the same reason: size_of and
|
||||
align_of are produced here because here is where the concrete element
|
||||
type is known, and nothing below the call site has ever heard of it. *)
|
||||
|
||||
(* (pool-new), (pool-new T), (pool-new a), (pool-new T a). *)
|
||||
| "pool-new" ->
|
||||
let elem, args = pool_new_elem ctx ~want loc args in
|
||||
let a = allocator_arg ctx loc args in
|
||||
let pty = Types.Pool elem in
|
||||
let p = fresh_slot ctx pty in
|
||||
(* [flan_pool_init] cannot fail — a pool with no slots allocates nothing —
|
||||
but it goes under the guard anyway, so that the day it does allocate
|
||||
the site is already the one that signals. *)
|
||||
let attempt =
|
||||
rt loc (Types.Int Types.I8) "flan_pool_init"
|
||||
[ mk loc pty (Tast.Local p); a; size_of loc elem; align_of loc elem;
|
||||
here loc ]
|
||||
in
|
||||
expect loc ~want
|
||||
(mk loc pty
|
||||
(Tast.Let ([ (p, mk loc pty (Tast.Zero pty)) ],
|
||||
[ with_note loc (alloc_guard ctx loc attempt)
|
||||
(reg_note loc "flan_dev_reg_note_pool"
|
||||
(mk loc pty (Tast.Local p))
|
||||
[ size_of loc elem ] elem);
|
||||
region_check ctx.env loc (mk loc pty (Tast.Local p))
|
||||
(mk loc pty (Tast.Local p)) ])))
|
||||
|
||||
(* (insert p x) -> (Handle T). The handle is the *only* way back to what was
|
||||
inserted: a pool hands out no index and no pointer, because an index does
|
||||
not notice a reuse and that is the entire point. *)
|
||||
| "insert" ->
|
||||
arity loc name 2 args;
|
||||
(match args with
|
||||
| [ target; x ] ->
|
||||
let target = check ctx target in
|
||||
let elem = pool_elem loc "insert" target.Tast.ty in
|
||||
let x = check ctx ~want:elem x in
|
||||
let hty = Types.Handle elem in
|
||||
(* The element is bound before the loop so that a [retry] re-attempts
|
||||
the allocation and not the expression that produced the value —
|
||||
[push]'s rule, and for the same reason. *)
|
||||
let e = fresh_slot ctx elem in
|
||||
let h = fresh_slot ctx hty in
|
||||
let attempt =
|
||||
rt loc (Types.Int Types.I8) "flan_pool_insert"
|
||||
[ target; addr_of loc (mk loc elem (Tast.Local e));
|
||||
addr_of loc (mk loc hty (Tast.Local h));
|
||||
size_of loc elem; align_of loc elem; here loc ]
|
||||
in
|
||||
expect loc ~want
|
||||
(mk loc hty
|
||||
(Tast.Let ([ (e, x); (h, mk loc hty (Tast.Zero hty)) ],
|
||||
[ region_check ctx.env loc target
|
||||
(with_note loc (alloc_guard ctx loc attempt)
|
||||
(reg_note loc "flan_dev_reg_note_pool" target
|
||||
[ size_of loc elem ] elem));
|
||||
mk loc hty (Tast.Local h) ])))
|
||||
| _ -> assert false)
|
||||
|
||||
(* (resolve p h) -> (Option (Ptr T)).
|
||||
|
||||
A pointer and not a value, and spec-memory.md settles it rather than this
|
||||
lane guessing: its worked example under "Mutating something you matched"
|
||||
is written out as (Option (Ptr Enemy)), for the reason stated a line
|
||||
above it — "pattern bindings bind values, so a matched struct is a copy",
|
||||
and a copy cannot be written back. Mutating the pooled thing in place is
|
||||
what a pool is for, so (Option T) would answer a question nobody asked.
|
||||
|
||||
An [Option] rather than a trap because the whole thesis is that a stale
|
||||
reference *reports* — the same shape (get m k) has, and for the same
|
||||
reason: absence is an answer, not a failure.
|
||||
|
||||
The hole, said plainly: the (Ptr T) is invalidated by any [insert] that
|
||||
grows the pool, exactly as a slice is invalidated by a [push]. The handle
|
||||
survives that and the pointer does not. It is spec-memory.md's explicit
|
||||
Zig/Odin contract one level down, and it is worth naming because it is
|
||||
the silent-wrong-answer mode the handle just removed, reintroduced for
|
||||
anyone who keeps the pointer across an insert. Chunked never-moving
|
||||
storage is the fix and it costs code; taking the contract is the smaller
|
||||
correct thing, given [as-slice] already established it. *)
|
||||
| "resolve" ->
|
||||
arity loc name 2 args;
|
||||
(match args with
|
||||
| [ target; h ] ->
|
||||
let target = check ctx target in
|
||||
let elem = pool_elem loc "resolve" target.Tast.ty in
|
||||
let h = check ctx ~want:(Types.Handle elem) h in
|
||||
(match h.Tast.ty with
|
||||
| Types.Handle e when Types.equal e elem -> ()
|
||||
| other ->
|
||||
fail loc "resolve takes a (Handle %s), found %s"
|
||||
(Types.to_string elem) (Types.to_string other));
|
||||
let pty = Types.Ptr elem in
|
||||
let oty = Types.Option pty in
|
||||
let out = fresh_slot ctx pty in
|
||||
let got =
|
||||
rt loc pty "flan_pool_resolve"
|
||||
[ target; h; size_of loc elem; here loc ]
|
||||
in
|
||||
(* The runtime answers a pointer or NULL and the Option is built here,
|
||||
which is [get]'s arrangement: the runtime has no idea what an
|
||||
Option's layout is, and keeping it that way is what lets one entry
|
||||
point serve every element type. *)
|
||||
let cond =
|
||||
mk loc Types.Bool
|
||||
(Tast.Prim (Tast.Ne,
|
||||
[ mk loc (Types.Int Types.I64)
|
||||
(Tast.Prim (Tast.Cast (Types.Int Types.I64),
|
||||
[ mk loc pty (Tast.Local out) ]));
|
||||
mk loc (Types.Int Types.I64) (Tast.Int (0L, Types.I64)) ]))
|
||||
in
|
||||
let some = mk loc oty (Tast.Some_ (mk loc pty (Tast.Local out))) in
|
||||
let none = mk loc oty Tast.None_ in
|
||||
expect loc ~want
|
||||
(mk loc oty
|
||||
(Tast.Let ([ (out, got) ],
|
||||
[ mk loc oty (Tast.If (cond, some, none)) ])))
|
||||
| _ -> assert false)
|
||||
|
||||
(* (release p h) -> bool: true if this call released it, false if the handle
|
||||
was already gone.
|
||||
|
||||
This is how a pooled value dies, and it is not [free]. [free] consumes
|
||||
its argument as a move, and a handle is a copyable number that owns
|
||||
nothing — consuming one copy would say nothing about the others. The pool
|
||||
is the owner, so the release operation is on the pool and takes the
|
||||
handle as an ordinary argument. spec-memory.md's two release points are
|
||||
untouched: (free p) is release point 1 applied to the owner, and a
|
||||
free-all of the region takes the pool with everything else. This is a
|
||||
third thing and it is not a release point — it recycles a slot inside
|
||||
storage the pool still owns.
|
||||
|
||||
It answers a bool rather than () because the generational scheme makes a
|
||||
double release *detectable*, which is worth handing to the caller: this
|
||||
is the one place in the language where freeing something twice is an
|
||||
answer instead of a refusal. *)
|
||||
| "release" ->
|
||||
arity loc name 2 args;
|
||||
(match args with
|
||||
| [ target; h ] ->
|
||||
let target = check ctx target in
|
||||
let elem = pool_elem loc "release" target.Tast.ty in
|
||||
let h = check ctx ~want:(Types.Handle elem) h in
|
||||
(match h.Tast.ty with
|
||||
| Types.Handle e when Types.equal e elem -> ()
|
||||
| other ->
|
||||
fail loc "release takes a (Handle %s), found %s"
|
||||
(Types.to_string elem) (Types.to_string other));
|
||||
let got = rt loc (Types.Int Types.I8) "flan_pool_release"
|
||||
[ target; h; here loc ] in
|
||||
expect loc ~want
|
||||
(mk loc Types.Bool
|
||||
(Tast.Prim (Tast.Ne,
|
||||
[ got;
|
||||
mk loc (Types.Int Types.I8) (Tast.Int (0L, Types.I8)) ])))
|
||||
| _ -> assert false)
|
||||
|
||||
(* (live p) — how many slots are live now. (len p) is the *slot high-water*,
|
||||
which is deliberately the other number: 0..(len p) are the indices
|
||||
(pool-handle p i) accepts, so a loop bounded by [len] visits every live
|
||||
entry. Bounding it by the live count instead would silently skip entries
|
||||
the moment anything had been released, which is precisely the kind of
|
||||
quiet wrong answer this whole type exists to remove. *)
|
||||
| "live" ->
|
||||
arity loc name 1 args;
|
||||
let target = check ctx (List.hd args) in
|
||||
ignore (pool_elem loc "live" target.Tast.ty);
|
||||
let n = rt loc (Types.Int Types.I64) "flan_pool_live" [ target; here loc ] in
|
||||
expect loc ~want (mk loc index_ty (Tast.Prim (Tast.Cast index_ty, [ n ])))
|
||||
|
||||
(* (pool-handle p i) -> (Option (Handle T)): the handle of slot [i], or None
|
||||
if that slot is dead. This plus (len p) is the whole of iteration, and
|
||||
iteration is not a convenience — migrate-instances has to *enumerate*
|
||||
live instances, and a pool behind generational handles gives that by
|
||||
construction where a world arena and an owned region do not. It is the
|
||||
reason plan.org's three storage strategies are not a free choice.
|
||||
|
||||
An index out of 0..(len p) traps, exactly as (at v i) traps: an index is
|
||||
an index here, and answering None for one would hide a bug rather than a
|
||||
death. *)
|
||||
| "pool-handle" ->
|
||||
arity loc name 2 args;
|
||||
(match args with
|
||||
| [ target; i ] ->
|
||||
let target = check ctx target in
|
||||
let elem = pool_elem loc "pool-handle" target.Tast.ty in
|
||||
let i = check ctx ~want:index_ty i in
|
||||
let hty = Types.Handle elem in
|
||||
let oty = Types.Option hty in
|
||||
let out = fresh_slot ctx hty in
|
||||
let got = rt loc hty "flan_pool_handle" [ target; i; here loc ] in
|
||||
(* 0 is the never-valid handle — generation 0 is even, and a live slot's
|
||||
generation is odd — so the runtime says "dead" with it and needs no
|
||||
second return value. *)
|
||||
let cond =
|
||||
mk loc Types.Bool
|
||||
(Tast.Prim (Tast.Ne,
|
||||
[ mk loc (Types.Int Types.I64)
|
||||
(Tast.Prim (Tast.Cast (Types.Int Types.I64),
|
||||
[ mk loc hty (Tast.Local out) ]));
|
||||
mk loc (Types.Int Types.I64) (Tast.Int (0L, Types.I64)) ]))
|
||||
in
|
||||
expect loc ~want
|
||||
(mk loc oty
|
||||
(Tast.Let ([ (out, got) ],
|
||||
[ mk loc oty
|
||||
(Tast.If (cond,
|
||||
mk loc oty (Tast.Some_ (mk loc hty (Tast.Local out))),
|
||||
mk loc oty Tast.None_)) ])))
|
||||
| _ -> assert false)
|
||||
|
||||
(* ── (Map K V), spec-memory.md ─────────────────────────────────── *)
|
||||
(* Every one of these is a named call over the same type-erased runtime the
|
||||
Vec uses, with the two sizes and the key's hash and equality pair produced
|
||||
@ -4379,7 +4045,8 @@ and named_call ctx ~want loc name args =
|
||||
| _ -> assert false)
|
||||
|
||||
(* (get m k) -> (Option V). Absence is None, not an untyped nil, and the
|
||||
first implementation admits copyable values only, so this is a copy.
|
||||
answer is a copy of the value's bytes — for an owning value, a copy of
|
||||
its header, aliasing what the map's slot points at.
|
||||
There is no allocation here and therefore no guard: a lookup that finds
|
||||
nothing is an answer, not a failure. *)
|
||||
| "get" ->
|
||||
@ -4816,16 +4483,9 @@ and named_call ctx ~want loc name args =
|
||||
| Types.Map _ ->
|
||||
let n = rt loc (Types.Int Types.I64) "flan_map_len" [ a; here loc ] in
|
||||
expect loc ~want (mk loc index_ty (Tast.Prim (Tast.Cast index_ty, [ n ])))
|
||||
(* A pool's [len] is its slot high-water, not its live count, so that
|
||||
0..(len p) stays the range of valid indices the way it is for every
|
||||
other container here. (live p) is the other number. *)
|
||||
| Types.Pool _ ->
|
||||
let n = rt loc (Types.Int Types.I64) "flan_pool_len" [ a; here loc ] in
|
||||
expect loc ~want (mk loc index_ty (Tast.Prim (Tast.Cast index_ty, [ n ])))
|
||||
| other ->
|
||||
fail loc
|
||||
"len takes an array, a slice, a string, a Vec, a Map or a Pool, \
|
||||
found %s"
|
||||
"len takes an array, a slice, a string, a Vec or a Map, found %s"
|
||||
(Types.to_string other))
|
||||
| "at" ->
|
||||
(match args with
|
||||
@ -4892,11 +4552,10 @@ and named_call ctx ~want loc name args =
|
||||
and a reader who sees it has already been told where the promise comes
|
||||
from.
|
||||
|
||||
**It owns nothing.** The result is a [Types.Slice], which is not
|
||||
move-only, carries no allocator, and is the same non-owning view
|
||||
(as-slice v) answers — so [free] refuses it by the rule it already had
|
||||
("free takes a move-only value"), and nothing in the move analysis needed
|
||||
to learn about this form. *)
|
||||
**It owns nothing.** The result is a [Types.Slice], which carries no
|
||||
allocator and is the same non-owning view (as-slice v) answers — so
|
||||
[free] refuses it by the rule it already had ("free takes an owning
|
||||
container"). *)
|
||||
| "slice-from-ptr" ->
|
||||
arity loc name 2 args;
|
||||
(match args with
|
||||
@ -5239,8 +4898,8 @@ and named_call ctx ~want loc name args =
|
||||
| Some b -> (match b.bty with Types.Fn _ -> true | _ -> false)
|
||||
| None -> false) ->
|
||||
(* The binding the guard already found, read directly. Going back through
|
||||
[check] would repeat the lookup and walk the move and capture paths for
|
||||
a type that is neither move-only nor capturable. *)
|
||||
[check] would repeat the lookup and walk the capture path for a type
|
||||
that is not capturable. *)
|
||||
(match lookup ctx name with
|
||||
| Some b -> call_value ctx ~want loc (mk loc b.bty (Tast.Local b.slot)) args
|
||||
| None -> assert false)
|
||||
@ -5345,7 +5004,7 @@ and generic_call ctx ~want loc name vars pats pret args =
|
||||
code the caller did not write, which is the thing the pass exists to
|
||||
avoid. So the caller has to declare at least what the callee asks for,
|
||||
and [pred_entails] means [ordered?] covers a callee wanting
|
||||
[copyable?] without anyone writing both. *)
|
||||
[equal?] without anyone writing both. *)
|
||||
(match Hashtbl.find_opt ctx.env.generics name with
|
||||
| None -> ()
|
||||
| Some gfn ->
|
||||
@ -5656,45 +5315,16 @@ let collect env (decls : Ast.decl list) =
|
||||
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
|
||||
containing a Vec is itself move-only, and freeing one recurses into
|
||||
its owning fields while (free (.items b)) is refused because it
|
||||
would leave the owner partly dead. None of that transitive
|
||||
machinery exists, and it is what [drop] would have brought. So the
|
||||
field is still refused at the declaration, where the message can
|
||||
say so, rather than accepted into a struct that copies its header
|
||||
on assignment and gives two owners one buffer.
|
||||
(* A struct field may own storage. Since the repeal a struct
|
||||
holding a [(Vec i32)] is an ordinary value: assignment copies the
|
||||
header bytes, the copies alias one buffer, and freeing through
|
||||
two copies is the program's bug — Odin's contract, kept whole.
|
||||
|
||||
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
|
||||
(fun (f : Tast.field) ->
|
||||
if Types.is_move_only f.Tast.fty
|
||||
&& not (region_only env f.Tast.fty) then
|
||||
fail loc
|
||||
"%s's field %s is %s, which is move-only, and a struct that \
|
||||
owns one is move-only too — transitively, with recursive \
|
||||
teardown and with a field that cannot be freed on its own. \
|
||||
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 f.Tast.fname (Types.to_string f.Tast.fty)
|
||||
(Types.to_string f.Tast.fty))
|
||||
fields
|
||||
The region rule is separate and survives on its own ground: a
|
||||
field whose container holds *owning* elements can only have been
|
||||
built against a region allocator — the guard at its construction
|
||||
is what makes sure of it (see [vec-new]) — so that graph is
|
||||
released by one [free-all] and no teardown recurses anywhere. *)
|
||||
| Ast.Defdata (n, vs) ->
|
||||
(* 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
|
||||
@ -5729,115 +5359,23 @@ let collect env (decls : Ast.decl list) =
|
||||
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 };
|
||||
(* 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;
|
||||
(* A case's fields are a struct and may own storage, on the struct's
|
||||
terms since the repeal: copies alias, and the free is the
|
||||
program's to write. The region rule still applies on its own
|
||||
ground — a [(Vec Value)] case field can only have been built
|
||||
against a region, so the recursive dynamic value parses into an
|
||||
arena and one [free-all] releases the graph, no teardown
|
||||
anywhere. *)
|
||||
List.iter
|
||||
(fun (c : Tast.variant) ->
|
||||
Hashtbl.replace env.cases (n ^ "." ^ c.Tast.vname) (n, c);
|
||||
Hashtbl.replace env.cases c.Tast.vname (n, c))
|
||||
cases
|
||||
(* ── The untagged union ──────────────────────────────────────────
|
||||
C's semantics, deliberately and in full: the members overlay one
|
||||
storage, the size is the largest of them, the alignment the
|
||||
strictest, and nothing anywhere records which member was written
|
||||
last.
|
||||
|
||||
{2 What Flan says about reading a member that was not written}
|
||||
|
||||
It reads the bytes that are there, through that member's type. Not
|
||||
undefined behaviour, and not a refusal either — a *definition*, and
|
||||
this is the one place in the checker that chooses bytes over safety
|
||||
on purpose, so it is worth saying why.
|
||||
|
||||
Refusing it was the alternative, and it would have made the feature
|
||||
nothing: type punning *is* reading the member that was not written,
|
||||
and both uses this type exists for are that read. Binding a C header
|
||||
means holding the union the library holds and reading whichever
|
||||
member the library's own tag says is live — a tag Flan cannot see,
|
||||
because it is a field of the enclosing struct and the rule that
|
||||
relates them is prose in a manual. Overlaying an f32 on a u32 to look
|
||||
at its bits is the other use and is the same read. A checker that
|
||||
refused it would be refusing the type.
|
||||
|
||||
So the promise is the one C's implementations actually make and
|
||||
C's standard does not: the layout is the target's, the bytes are the
|
||||
bytes, and a read is a reinterpretation of them. What is *not*
|
||||
promised is anything about bytes never written — a member larger
|
||||
than the one last stored reads its own size, and the tail is
|
||||
indeterminate exactly as a struct's padding is. That is the honest
|
||||
line, and it is narrower than it sounds: the ZII rule means a union
|
||||
starts all-bytes-zero unless [uninit] says otherwise, so the tail is
|
||||
zero rather than garbage in every program that did not ask for
|
||||
garbage.
|
||||
|
||||
{2 uninit}
|
||||
|
||||
Allowed, unlike on a data type. The refusal there is not about
|
||||
garbage — [uninit] is garbage everywhere and says so — it is that a
|
||||
data type's tag *steers*, and a tag no case names falls past every
|
||||
comparison in a [match] into a block LLVM is entitled to treat as
|
||||
unreachable. An untagged union steers nothing. Reading a member of
|
||||
one is already a reinterpretation of whatever bytes are there, so
|
||||
[uninit] makes those bytes arbitrary and changes nothing else, which
|
||||
is exactly what it means on an [i64].
|
||||
|
||||
{2 Why bool is not a member}
|
||||
|
||||
An [i1] loaded out of a byte that is neither 0 nor 1 is not a
|
||||
[false], it is a value the optimiser is entitled to assume cannot
|
||||
exist, and a union is the one type that can hand it one — write the
|
||||
[u8] member 2, read the [bool] member. Nothing about that is visible
|
||||
at the read, so it cannot be refused there. The alternative was to
|
||||
load a union's bool as an [i8] and compare it against zero in both
|
||||
backends, which is a correct answer and a real cost paid by every
|
||||
bool in the language to make one type safe. Refused at the
|
||||
declaration instead, where the message can name the replacement:
|
||||
[u8], compared explicitly. The check below is recursive, because a
|
||||
bool inside a struct member is the same byte.
|
||||
|
||||
{2 Why no member may be move-only}
|
||||
|
||||
Because nothing knows which member is live, so nothing can tear one
|
||||
down. That is not a limitation of today's compiler, which is what
|
||||
the struct and data type refusals above say about themselves; it is
|
||||
a property of the type, and it does not go away when recursive
|
||||
teardown lands. A [drop] of a union would have to free whichever
|
||||
member is live and there is no such fact — freeing the wrong one is
|
||||
a free of a pointer that was an f64 a moment ago. *)
|
||||
| Ast.Defunion (n, ms) ->
|
||||
(* Nothing records which member of a union is live, so nothing — the
|
||||
program included — can free the right one through the union itself.
|
||||
Since the repeal that is a fact about the value and not a refusal:
|
||||
a member may own storage, and freeing it is done through whatever
|
||||
tag the program keeps beside the union, as C does. *) | Ast.Defunion (n, ms) ->
|
||||
if ms = [] then
|
||||
fail loc
|
||||
"%s declares no members, so it has no size and nothing could be \
|
||||
@ -5846,20 +5384,6 @@ let collect env (decls : Ast.decl list) =
|
||||
if List.length (List.sort_uniq compare names) <> List.length names then
|
||||
fail loc "%s declares the same member twice" n;
|
||||
let fields = List.map field ms in
|
||||
List.iter
|
||||
(fun (f : Tast.field) ->
|
||||
if Types.is_move_only f.Tast.fty then
|
||||
fail loc
|
||||
"%s's member %s is %s, which is move-only, and a union may \
|
||||
not own one: the members overlay one storage and nothing \
|
||||
records which was written, so nothing can free the right \
|
||||
one. Unlike a struct's, this is not waiting on recursive \
|
||||
teardown — there is no fact for teardown to read. Hold the \
|
||||
%s beside the union, or in a struct with a tag you check \
|
||||
yourself"
|
||||
n f.Tast.fname (Types.to_string f.Tast.fty)
|
||||
(Types.to_string f.Tast.fty))
|
||||
fields;
|
||||
Hashtbl.replace env.unions n { Tast.sname = n; fields }
|
||||
| Ast.Defn fn ->
|
||||
(* A signature that introduces a type variable is a *pattern*, not a
|
||||
@ -6133,9 +5657,7 @@ let rec check_fn env (fn : Ast.fn) : Tast.fn =
|
||||
whichever call site happened to instantiate it at a type that worked.
|
||||
|
||||
The holes in it are real and are the report's business: [println] is
|
||||
plan.org's one compiler-provided exception and this pass rejects it, and
|
||||
move-only-ness is not decidable abstractly at all — [Types.is_move_only
|
||||
(Var _)] is false, but the same variable at [(Vec i32)] is move-only. *)
|
||||
plan.org's one compiler-provided exception and this pass rejects it. *)
|
||||
and check_generic env (fn : Ast.fn) =
|
||||
let vars, params, ret = Hashtbl.find env.gsigs fn.Ast.name in
|
||||
let saved_lifted = env.lifted and saved_vars = env.tyvars
|
||||
@ -6160,14 +5682,12 @@ and check_generic env (fn : Ast.fn) =
|
||||
checking a function. *)
|
||||
let () = check_fn_ref := check_fn
|
||||
|
||||
(* A global of move-only type is legal. Before the repeal what made it legal
|
||||
was a flow rule — reading one was always a borrow, so nothing could take
|
||||
or free it. That rule is gone with the rest of the flow analysis: a global
|
||||
Vec may now be handed to a function, bound, or freed, and keeping its
|
||||
process-long lifetime honest is the program's business, on the same terms
|
||||
as every other free.
|
||||
(* A container's only compile-time constant is the zeroed one: a Vec's or a
|
||||
Map's real value exists at run time, behind an allocator. That is a fact
|
||||
about initialisers and it survived both repeals untouched — nothing here
|
||||
is about copying or moving.
|
||||
|
||||
What this pass still decides is how such a global may be *started*, and the
|
||||
What this pass decides is how such a global may be *started*, and the
|
||||
answer is zeroed and nothing else. A zeroed Vec is a real empty Vec — null
|
||||
block, zero length, zero capacity — so the ZII value is the value a program
|
||||
would have written anyway, and filling it is an ordinary (set g (slurp
|
||||
@ -6190,15 +5710,21 @@ let () = check_fn_ref := check_fn
|
||||
A global *Allocator* is not any of this — an allocator is a copyable opaque
|
||||
handle — which is what makes the handler-owns-the-arena shape in
|
||||
exhausted.flan expressible. *)
|
||||
let move_only_global_init loc n (ty : Types.t) (init : Ast.init) =
|
||||
if Types.is_move_only ty then
|
||||
let rec zero_only (t : Types.t) =
|
||||
match t with
|
||||
| Types.Vec _ | Types.Map _ -> true
|
||||
| Types.Option e | Types.Array (_, e) -> zero_only e
|
||||
| _ -> false
|
||||
|
||||
let container_global_init loc n (ty : Types.t) (init : Ast.init) =
|
||||
if zero_only ty then
|
||||
match init with
|
||||
| Ast.Zeroed -> ()
|
||||
| _ ->
|
||||
fail loc
|
||||
"the global %s is %s, which is move-only, and a move-only global \
|
||||
starts zeroed: a global's initialiser is a compile-time constant and \
|
||||
%s is not one. Write (defvar %s %s) with no initialiser — a zeroed \
|
||||
"the global %s is %s, and such a global starts zeroed: a global's \
|
||||
initialiser is a compile-time constant, %s is not one, and a \
|
||||
container's only constant value is the empty one. Write (defvar %s %s) with no initialiser — a zeroed \
|
||||
%s is an empty one, and that is a value, not a placeholder — then \
|
||||
load it with (set %s ...) in the function that loads it, which runs \
|
||||
once and whose result outlives every call to main"
|
||||
@ -6206,19 +5732,21 @@ let move_only_global_init loc n (ty : Types.t) (init : Ast.init) =
|
||||
(match init with Ast.Uninit -> "uninit" | _ -> "this initialiser")
|
||||
n (Types.to_string ty) (Types.to_string ty) n
|
||||
|
||||
(* A move-only global has to be a [defvar]. A [defconst] is not an assignable
|
||||
place — [check_place] refuses one by name — so a constant Vec could only
|
||||
ever hold the zeroed value it was declared with, and nothing could ever put
|
||||
the file's bytes in it. Refused here, where the fix is one keyword, rather
|
||||
than at the (set ...) that discovers it three forms later. *)
|
||||
let no_move_only_defconst loc n (ty : Types.t) =
|
||||
if Types.is_move_only ty then
|
||||
(* A container global has to be a [defvar]. A [defconst] is not an assignable
|
||||
place — [check_place] refuses one by name — and a container's only constant
|
||||
is the zeroed one, so a constant Vec could only ever hold the empty value
|
||||
it was declared with: nothing could ever put the file's bytes in it.
|
||||
Refused here, where the fix is one keyword, rather than at the (set ...)
|
||||
that discovers it three forms later. *)
|
||||
let no_container_defconst loc n (ty : Types.t) =
|
||||
if zero_only ty then
|
||||
fail loc
|
||||
"the global %s is %s, which is move-only, and a move-only global is a \
|
||||
defvar and not a defconst: a constant is not an assignable place, so \
|
||||
nothing could ever load this one — it would stay the empty %s it was \
|
||||
declared as. Write (defvar %s %s) and fill it in a function"
|
||||
n (Types.to_string ty) (Types.to_string ty) n (Types.to_string ty)
|
||||
"the global %s is %s, and a %s global is a defvar and not a defconst: \
|
||||
a constant is not an assignable place, so nothing could ever load \
|
||||
this one — it would stay the empty %s it was declared as. Write \
|
||||
(defvar %s %s) and fill it in a function"
|
||||
n (Types.to_string ty) (Types.to_string ty) (Types.to_string ty)
|
||||
n (Types.to_string ty)
|
||||
|
||||
(* A union member written into a global would have to be encoded into the blob
|
||||
at link time, which is the byte-level encoder a data type case does not have
|
||||
@ -6249,7 +5777,7 @@ let check_global env (d : Ast.decl) : Tast.global option =
|
||||
| Ast.Defvar (n, _, init) ->
|
||||
let ty, _ = Hashtbl.find env.globals n in
|
||||
no_zeroed_fn d.Ast.dloc (Printf.sprintf "the global %s" n) ty;
|
||||
move_only_global_init d.Ast.dloc n ty init;
|
||||
container_global_init d.Ast.dloc n ty init;
|
||||
let ginit =
|
||||
match init with
|
||||
| Ast.Zeroed -> { Tast.e = Tast.Zero ty; ty; loc = d.Ast.dloc }
|
||||
@ -6282,7 +5810,7 @@ let check_global env (d : Ast.decl) : Tast.global option =
|
||||
| Ast.Defconst (n, _, v) ->
|
||||
let ty, _ = Hashtbl.find env.globals n in
|
||||
no_zeroed_fn d.Ast.dloc (Printf.sprintf "the global %s" n) ty;
|
||||
no_move_only_defconst d.Ast.dloc n ty;
|
||||
no_container_defconst d.Ast.dloc n ty;
|
||||
(* [collect] already folded the integer constants, because an array length
|
||||
has to be known before any type resolves. Use that value here rather
|
||||
than the expression it came from: a global's initialiser has to be a
|
||||
|
||||
@ -1462,11 +1462,10 @@ let reg_at t ~addr : (reg_entry option, string) result =
|
||||
anywhere, so nothing can fall behind [Types.to_string].
|
||||
|
||||
And it is allowed to fail, which matters more than it looks. Not every
|
||||
recorded name is a type: [flan_rt.c] notes a pool's slot headers as
|
||||
"pool slots", because after a free-all an address landing in them must not
|
||||
come back as an element. That string is not Flan source and must not
|
||||
become one — so a name that does not resolve is refused with the name
|
||||
quoted, and never defaulted to bytes. *)
|
||||
recorded name need be a type this session can spell — a note's name is
|
||||
whatever string the noting site chose, not Flan source — so a name that
|
||||
does not resolve is refused with the name quoted, and never defaulted to
|
||||
bytes. *)
|
||||
let type_of_spelling t spelling : (Types.t, string) result =
|
||||
let refuse why =
|
||||
Error
|
||||
|
||||
75
lib/emit.ml
75
lib/emit.ml
@ -124,15 +124,6 @@ let rec ll (t : Types.t) =
|
||||
map's address — so the shape exists only so that a slot, a struct field
|
||||
and a copy in the IR are the right number of bytes. *)
|
||||
| Types.Map _ -> "%map"
|
||||
(* items + slots + len + cap + live + free + allocator + epoch. Nothing here
|
||||
reads a field of one either — every operation is a runtime call taking
|
||||
the pool's address. *)
|
||||
| Types.Pool _ -> "%pool"
|
||||
(* A handle is one 64-bit number: the slot index in the low half and that
|
||||
slot's generation in the high half. Packed rather than a two-field struct
|
||||
so that copying, zeroing and [=] are what they are for an integer, with no
|
||||
backend arm anywhere except the one comparison below. *)
|
||||
| Types.Handle _ -> "i64"
|
||||
| Types.Option e -> Printf.sprintf "{ i8, %s }" (ll e)
|
||||
| Types.Var _ ->
|
||||
(* The checker rejects it by name — nothing reaches here. *)
|
||||
@ -296,9 +287,7 @@ let rec lay m (t : Types.t) : int * int =
|
||||
| Types.Ptr _ -> 8, 8
|
||||
| Types.Alloc -> 8, 8
|
||||
| Types.Fn _ -> 8, 8
|
||||
| Types.Vec _ | Types.Map _ -> 48, 8
|
||||
| Types.Pool _ -> 64, 8
|
||||
| Types.Handle _ -> 8, 8
|
||||
| Types.Vec _ | Types.Map _ -> 40, 8
|
||||
(* [n x T] adds no padding of its own: T's size already carries its tail. *)
|
||||
| Types.Array (n, e) -> let s, a = lay m e in Int64.to_int n * s, a
|
||||
| Types.Option e -> let s, a, _ = lay_fields m [ Types.Int Types.I8; e ] in s, a
|
||||
@ -523,15 +512,15 @@ let rec dty m d (t : Types.t) : int =
|
||||
| Types.Alloc ->
|
||||
dnode d
|
||||
"!DIDerivedType(tag: DW_TAG_pointer_type, name: \"Allocator\", baseType: null, size: 64)"
|
||||
(* Shown as what it is. The two dev words are in the layout and so they
|
||||
are here too: a debugger that showed four fields of a six-field struct
|
||||
would put the reader's offsets out by two. *)
|
||||
(* Shown as what it is. The epoch word is in the layout and so it is
|
||||
here too: a debugger that showed four fields of a five-field struct
|
||||
would put the reader's offsets out by one. *)
|
||||
| Types.Vec e ->
|
||||
composite (Types.to_string t)
|
||||
[ ("ptr", Types.Ptr e); ("len", Types.Int Types.I64);
|
||||
("cap", Types.Int Types.I64); ("allocator", Types.Alloc);
|
||||
("gen", Types.Int Types.I64); ("epoch", Types.Int Types.I64) ]
|
||||
(* Six fields again, and shown as six for the same reason: a debugger
|
||||
("epoch", Types.Int Types.I64) ]
|
||||
(* Five fields again, and shown as five for the same reason: a debugger
|
||||
that showed fewer would put the reader's offsets out. [log2cap] is
|
||||
shown rather than a capacity because that is what is stored — the
|
||||
capacity is 1 << it, and a debugger that invented the shift would be
|
||||
@ -540,22 +529,8 @@ let rec dty m d (t : Types.t) : int =
|
||||
composite (Types.to_string t)
|
||||
[ ("data", Types.Ptr (Types.Int Types.U8));
|
||||
("len", Types.Int Types.I64); ("log2cap", Types.Int Types.I64);
|
||||
("allocator", Types.Alloc); ("gen", Types.Int Types.I64);
|
||||
("epoch", Types.Int Types.I64) ]
|
||||
|> fun n -> ignore k; ignore v; n
|
||||
(* Eight fields, shown as eight, for the reason the two above are. *)
|
||||
| Types.Pool e ->
|
||||
composite (Types.to_string t)
|
||||
[ ("items", Types.Ptr e);
|
||||
("slots", Types.Ptr (Types.Int Types.U8));
|
||||
("len", Types.Int Types.I64); ("cap", Types.Int Types.I64);
|
||||
("live", Types.Int Types.I64); ("free", Types.Int Types.I64);
|
||||
("allocator", Types.Alloc); ("epoch", Types.Int Types.I64) ]
|
||||
(* An i64 under lldb, which is what it is. Splitting it into a two-field
|
||||
composite would be describing a struct that is not there: the packing
|
||||
is the runtime's, and [p h] answering with the number is honest. *)
|
||||
| Types.Handle _ ->
|
||||
basic (Types.to_string t) 64 "DW_ATE_unsigned"
|
||||
|> fun n -> ignore k; ignore v; n
|
||||
(* A pointer to code, and lldb is told exactly that and no more. DWARF
|
||||
has DW_TAG_subroutine_type for the signature behind it, and spelling
|
||||
one out here would buy a reader nothing they cannot get from the
|
||||
@ -2043,11 +2018,6 @@ and prim f (e : Tast.expr) (p : Tast.prim) (args : Tast.expr list) =
|
||||
location. Signed, because a member may be declared negative. *)
|
||||
| Types.Enum _ ->
|
||||
ins f "%s = icmp %s %s %s, %s" t (icmp_op true p) (ll x.Tast.ty) a b
|
||||
(* [Types.is_equatable] admits a handle and [is_comparable] does not, so
|
||||
only [Eq]/[Ne] arrive here — one unsigned integer compare over the
|
||||
packed (index, generation) pair. *)
|
||||
| Types.Handle _ ->
|
||||
ins f "%s = icmp %s i64 %s, %s" t (icmp_op false p) a b
|
||||
| t' -> failwith ("comparison on " ^ Types.to_string t'));
|
||||
t
|
||||
| (Tast.BitAnd | Tast.BitOr | Tast.BitXor | Tast.Shl | Tast.Shr), [ x; y ] ->
|
||||
@ -2254,7 +2224,7 @@ and prim f (e : Tast.expr) (p : Tast.prim) (args : Tast.expr list) =
|
||||
lets an operation mutate the caller's container in place.
|
||||
Passing the header by value here would hand the runtime a
|
||||
copy to grow and leave the caller's untouched. *)
|
||||
| Types.Vec _ | Types.Map _ | Types.Pool _ -> [ "ptr " ^ addr f a ]
|
||||
| Types.Vec _ | Types.Map _ -> [ "ptr " ^ addr f a ]
|
||||
| t -> [ ll t ^ " " ^ value f a ])
|
||||
args)
|
||||
in
|
||||
@ -2325,11 +2295,6 @@ and cast f ~guard (x : Tast.expr) target =
|
||||
let concrete (t : Types.t) =
|
||||
match t with
|
||||
| Types.Enum _ -> Types.Int Types.I32
|
||||
(* A handle already *is* an i64 — see [ll] — so a cast involving one
|
||||
changes the reading and never the bits. [pool-handle] tests one against
|
||||
the never-valid zero, and the renderer splits one into its index and
|
||||
its generation. Unsigned, because both halves are. *)
|
||||
| Types.Handle _ -> Types.Int Types.U64
|
||||
| t -> t
|
||||
in
|
||||
let src = concrete x.Tast.ty and target = concrete target in
|
||||
@ -2360,7 +2325,7 @@ and cast f ~guard (x : Tast.expr) target =
|
||||
it, both sides being [ptr]. *)
|
||||
| Types.Ptr _, Types.Ptr _ -> "bitcast"
|
||||
(* Also not written in the surface language. [resolve] needs it: the
|
||||
pool answers a pointer or NULL and the Option is built in the
|
||||
runtime answers a pointer or NULL and the Option is built in the
|
||||
checker, so the null test is one integer compare on the address. *)
|
||||
| Types.Ptr _, Types.Int Types.I64 -> "ptrtoint"
|
||||
| _ -> failwith "unsupported cast"
|
||||
@ -2702,15 +2667,11 @@ let header = {|; Generated by flan. The layout is C's: no object headers anywher
|
||||
%slice = type { ptr, i64 }
|
||||
; (Vec T), spec-memory.md. The element type is nowhere in it: the runtime is
|
||||
; type-erased and every operation is handed size and align at its call site.
|
||||
%vec = type { ptr, i64, i64, ptr, i64, i64 }
|
||||
%vec = type { ptr, i64, i64, ptr, i64 }
|
||||
; (Map K V), spec-memory.md — Odin's open-addressed Robin Hood map. Neither key
|
||||
; nor value type appears in it, for the same reason: one type-erased runtime,
|
||||
; handed the two sizes and a hash/equality pair at each call site.
|
||||
%map = type { ptr, i64, i64, ptr, i64, i64 }
|
||||
; (Pool T) — slab storage handed out behind (Handle T). Type-erased in exactly
|
||||
; the same way; the element type is nowhere in it. items and slots are grown
|
||||
; together and share one cap, so a slot index is an index into both.
|
||||
%pool = type { ptr, ptr, i64, i64, i64, i64, ptr, i64 }
|
||||
%map = type { ptr, i64, i64, ptr, i64 }
|
||||
; A handler frame: the one it displaced, the condition type it matches, and
|
||||
; the lifted function that runs. Allocated on the establishing frame's stack.
|
||||
%handler = type { ptr, i32, ptr }
|
||||
@ -2775,7 +2736,6 @@ declare void @flan_arena_destroy(ptr)
|
||||
declare void @flan_alloc_free_all(ptr, ptr, i64)
|
||||
declare void @flan_vec_region_only(ptr, ptr, i64)
|
||||
declare void @flan_map_region_only(ptr, ptr, i64)
|
||||
declare void @flan_pool_region_only(ptr, ptr, i64)
|
||||
declare i8 @flan_alloc_can_free(ptr)
|
||||
declare i8 @flan_alloc_can_free_all(ptr)
|
||||
declare i64 @flan_alloc_epoch(ptr)
|
||||
@ -2788,7 +2748,6 @@ declare i64 @flan_alloc_budget(ptr)
|
||||
declare void @flan_alloc_set_budget(ptr, i64)
|
||||
declare void @flan_dev_reg_enable()
|
||||
declare void @flan_dev_reg_note_vec(ptr, i64, ptr, i64)
|
||||
declare void @flan_dev_reg_note_pool(ptr, i64, ptr, i64)
|
||||
declare void @flan_dev_reg_note_map(ptr, i64, i64, ptr, i64)
|
||||
declare i8 @flan_vec_init(ptr, ptr, i64, i64, i64, ptr, i64)
|
||||
declare i8 @flan_vec_reserve(ptr, i64, i64, i64, ptr, i64)
|
||||
@ -2801,18 +2760,6 @@ declare i64 @flan_vec_len(ptr, ptr, i64)
|
||||
declare ptr @flan_vec_at(ptr, i32, i64, ptr, i64, ptr)
|
||||
declare void @flan_vec_as_slice(ptr, ptr, i32, i32, i64, ptr, i64, ptr)
|
||||
declare void @flan_vec_free(ptr, i64, i64, ptr, i64)
|
||||
; (Pool T) and (Handle T). A handle crosses as the i64 it is; the pool, like
|
||||
; every other owning container, crosses as its address. [resolve] answers a
|
||||
; pointer or null and [pool-handle] answers a packed handle or the never-valid
|
||||
; zero, so neither needs a second return value.
|
||||
declare i8 @flan_pool_init(ptr, ptr, i64, i64, ptr, i64)
|
||||
declare i8 @flan_pool_insert(ptr, ptr, ptr, i64, i64, ptr, i64)
|
||||
declare ptr @flan_pool_resolve(ptr, i64, i64, ptr, i64)
|
||||
declare i8 @flan_pool_release(ptr, i64, ptr, i64)
|
||||
declare i64 @flan_pool_len(ptr, ptr, i64)
|
||||
declare i64 @flan_pool_live(ptr, ptr, i64)
|
||||
declare i64 @flan_pool_handle(ptr, i32, ptr, i64)
|
||||
declare void @flan_pool_free(ptr, i64, i64, ptr, i64)
|
||||
; (Map K V). The two ptr arguments before the location on put/get/clone are the
|
||||
; hash and equality pair, which the checker emits per key type and passes here
|
||||
; the way Odin hangs them off Map_Info.
|
||||
|
||||
10
lib/js.ml
10
lib/js.ml
@ -116,7 +116,7 @@
|
||||
{1 What is refused, and why each}
|
||||
|
||||
Pointers and [deref], [free], allocators and [with-allocator], [Map],
|
||||
[Pool] and [(Handle T)], [declare-c] and the FFI, [embed], conditions and
|
||||
[declare-c] and the FFI, [embed], conditions and
|
||||
restarts ([signal], [handler-bind], [restart-case], [invoke-restart]), and
|
||||
the type-erased container runtime's own entry points. The first group has
|
||||
no counterpart in a garbage-collected object graph; the FFI and [embed]
|
||||
@ -235,14 +235,6 @@ let rec refuse_ty loc (t : Types.t) =
|
||||
"(Map K V) is not in the JS dialect yet — Odin's open-addressed map is a \
|
||||
type-erased runtime over raw bytes and the JS answer is a Map keyed by \
|
||||
a structural key, which is its own lane"
|
||||
| Types.Pool _ ->
|
||||
at loc
|
||||
"(Pool T) is not in the JS dialect — a pool hands out slot indices into \
|
||||
storage it owns, which is the memory model this dialect leaves behind"
|
||||
| Types.Handle _ ->
|
||||
at loc
|
||||
"(Handle T) is not in the JS dialect — a handle is an index into a Pool, \
|
||||
and there is no Pool here"
|
||||
| Types.Var n ->
|
||||
at loc "a type variable (%s) reached the backend, which cannot happen" n
|
||||
|
||||
|
||||
@ -228,29 +228,16 @@ let source = {flan|
|
||||
;; variable supports only what it is declared to support — an unconstrained
|
||||
;; one is refused at the *definition*, not at some later call site — and
|
||||
;; [ordered?] is the predicate that admits [<], [<=], [>], [>=], [min] and
|
||||
;; [max]. It admits [=] and [copyable?] too: every type the language orders is
|
||||
;; a number or an enum, so it is equatable and it is not move-only.
|
||||
;; [max]. It admits [=] too: every type the language orders is a number or an
|
||||
;; enum, so it is equatable.
|
||||
;;
|
||||
;; [{:where (copyable? $t)}] is the opt-out from the other default. A type
|
||||
;; variable is **move-only** until it says otherwise, because move is the
|
||||
;; stricter rule and assuming it can only refuse a valid program rather than
|
||||
;; admit a broken one: [reduce]'s accumulator is read into [f] and then
|
||||
;; assigned again, which is correct at [i32] and a double move at [(Vec i32)],
|
||||
;; and the checker cannot tell which until it substitutes.
|
||||
;;
|
||||
;; **Two of these ten are forced and the rest are convention, and the
|
||||
;; difference is worth knowing.** [filter] and [reduce] do not check without
|
||||
;; [copyable?]: the first returns a [(Vec $t)], and a Vec of an owning element
|
||||
;; is refused, and the second holds its accumulator in a local and reads it
|
||||
;; twice. [swap!], [reverse!], [map!] and [sort-by!] check *without* it,
|
||||
;; because the move analysis tracks locals and parameters and does not track a
|
||||
;; read out of a slice — so [(let [t (at s i)] ... (set (at s j) t))] is not
|
||||
;; seen as a move even when the element owns storage. They declare it anyway,
|
||||
;; and should: at [[(Vec i32)]] those bodies would duplicate a header. It is
|
||||
;; the one place move-by-default is not conservative, and until element-level
|
||||
;; moves are tracked, a [copyable?] on a body that moves elements between
|
||||
;; slots is a convention the reader has to keep rather than a fact the checker
|
||||
;; enforces.
|
||||
;; There is no [copyable?] any more. Since the repeal every value copies —
|
||||
;; a container copies as its header, the copies alias one buffer, and what
|
||||
;; the copies then do is the program's business, as it is in Odin. A body
|
||||
;; that reads an element into a local and writes it into another slot is
|
||||
;; duplicating a header when the element owns storage, and nothing here
|
||||
;; says otherwise any more: that sentence moved from a predicate into this
|
||||
;; comment, which is where Odin keeps it too.
|
||||
;;
|
||||
;; **What did not collapse, and why it should not.** [sum-i32] and [sum-f32]
|
||||
;; widen their element into [i64] and [f64]; "the wider type $t accumulates
|
||||
@ -263,13 +250,11 @@ let source = {flan|
|
||||
;; keeping attached to something.
|
||||
|
||||
(defn swap! [s [$t] i i32 j i32] ()
|
||||
{:where (copyable? $t)}
|
||||
(let [t (at s i)]
|
||||
(set (at s i) (at s j))
|
||||
(set (at s j) t)))
|
||||
|
||||
(defn reverse! [s [$t]] ()
|
||||
{:where (copyable? $t)}
|
||||
(let [i 0
|
||||
j (- (len s) 1)]
|
||||
(while (< i j)
|
||||
@ -317,7 +302,6 @@ let source = {flan|
|
||||
;; predicates existed, and it stays because passing a comparison is a real
|
||||
;; thing to want and not only a workaround.
|
||||
(defn sort-by! [s [$t] before? (Fn [$t $t] bool)] ()
|
||||
{:where (copyable? $t)}
|
||||
(let [i 1]
|
||||
(while (< i (len s))
|
||||
(let [j i]
|
||||
@ -369,7 +353,6 @@ let source = {flan|
|
||||
;; here: it is two type variables and a second signature, and nothing has
|
||||
;; wanted it.
|
||||
(defn map! [s [$t] f (Fn [$t] $t)] ()
|
||||
{:where (copyable? $t)}
|
||||
(dotimes [i (len s)]
|
||||
(set (at s i) (f (at s i)))))
|
||||
|
||||
@ -377,7 +360,6 @@ let source = {flan|
|
||||
;; in. The accumulator comes first in the step, which is the order that reads
|
||||
;; as (f acc x) and the order Odin's slice.reduce uses.
|
||||
(defn reduce [s [$t] init $t f (Fn [$t $t] $t)] $t
|
||||
{:where (copyable? $t)}
|
||||
(let [acc init]
|
||||
(dotimes [i (len s)]
|
||||
(set acc (f acc (at s i))))
|
||||
@ -391,7 +373,6 @@ let source = {flan|
|
||||
;; runtime needed no change at all, because SizeOf and AlignOf are computed at
|
||||
;; the instantiation site, where the element type is concrete.
|
||||
(defn filter [s [$t] keep? (Fn [$t] bool)] (Vec $t)
|
||||
{:where (copyable? $t)}
|
||||
(let [v (vec-new t)]
|
||||
(dotimes [i (len s)]
|
||||
(when (keep? (at s i))
|
||||
|
||||
@ -187,33 +187,6 @@ let rec render c depth (e : Tast.expr) : Tast.expr list =
|
||||
does not own, and the walk is what [as-slice] is for: (print (as-slice
|
||||
v)) prints the elements and says at the call site that it borrowed. *)
|
||||
| Types.Vec _ -> [ lit "<vec>" ]
|
||||
(* Opaque for the reason a Vec is: the slots are storage this function does
|
||||
not own, and a walk over them would print the dead ones too — there is
|
||||
no way to say "dead" inside a rendered element. (pool-handle p i) and
|
||||
(resolve p h) are how a program looks, and they say it. *)
|
||||
| Types.Pool _ -> [ lit "<pool>" ]
|
||||
(* Its identity, which is what spec-memory.md says a handle prints —
|
||||
"Ptr and Handle print their address or identity rather than recursively
|
||||
dereferencing". Shown as index:generation rather than as the packed
|
||||
number, because those are the two things a reader is trying to tell
|
||||
apart when two handles disagree. *)
|
||||
| Types.Handle _ ->
|
||||
let h = cast (Types.Int Types.U64) e in
|
||||
let u64 v = { Tast.e = v; ty = Types.Int Types.U64; loc } in
|
||||
let idx =
|
||||
u64 (Tast.Prim (Tast.BitAnd,
|
||||
[ h; u64 (Tast.Int (0xFFFFFFFFL, Types.U64)) ]))
|
||||
in
|
||||
let gen =
|
||||
u64 (Tast.Prim (Tast.Shr, [ h; u64 (Tast.Int (32L, Types.U64)) ]))
|
||||
in
|
||||
[ do_ [ lit "<handle "; c.emit.eu64 idx; lit ":"; c.emit.eu64 gen;
|
||||
lit ">" ] ]
|
||||
(* A function value is a code address, and printing the address would make
|
||||
an inspection depend on where the image loaded. The signature is what a
|
||||
reader can act on, so that is what is shown — and the inspector reaches
|
||||
every local of a stopped frame, so a frame holding one has to render
|
||||
rather than refuse. *)
|
||||
| Types.Fn _ as ft -> [ lit ("<" ^ Types.to_string ft ^ ">") ]
|
||||
| Types.Option t ->
|
||||
let tag = { Tast.e = Tast.Field (e, 0); ty = Types.Int Types.I8; loc } in
|
||||
|
||||
51
lib/types.ml
51
lib/types.ml
@ -44,25 +44,6 @@ type t =
|
||||
so this is a container without generics — the concrete type is known only
|
||||
at the call site, which is exactly where the two numbers are produced. *)
|
||||
| Vec of t
|
||||
(* [(Pool T)]: slab storage handed out behind [(Handle T)]. Owning and
|
||||
move-only exactly as a [Vec] is, and built on the same type-erased
|
||||
runtime over (size, align). It is not a second [Vec]: a [Vec]'s indices
|
||||
shift when something is removed and a [Pool]'s slot index never moves,
|
||||
which is the whole reason a handle into one stays meaningful. *)
|
||||
| Pool of t
|
||||
(* [(Handle T)]: a reference to something that can die, which reports that
|
||||
it died rather than silently resolving to whatever reused its slot
|
||||
(spec-memory.md, "Borrowing" — "Cross-referencing long-lived objects uses
|
||||
(Handle a) into a pool, never a raw pointer or slice. A stale handle is
|
||||
detectable").
|
||||
|
||||
It is a plain 64-bit number — a slot index in the low 32 bits and that
|
||||
slot's generation counter in the high 32 — so it copies, compares and
|
||||
zeroes like an integer and owns nothing. A zeroed handle is generation 0,
|
||||
and a live slot's generation is always odd, so [Zero] of a handle is a
|
||||
handle that resolves to nothing rather than one that resolves to slot 0.
|
||||
See runtime/flan_rt.c's pool section for the packing. *)
|
||||
| Handle of t
|
||||
| Option of t (* (Option T) *)
|
||||
| Fn of t list * t (* (Fn [T ...] R) *)
|
||||
| Var of string (* a type variable — milestone 5 *)
|
||||
@ -113,8 +94,6 @@ let rec equal a b =
|
||||
| Ptr x, Ptr y -> equal x y
|
||||
| Alloc, Alloc -> true
|
||||
| Vec x, Vec y -> equal x y
|
||||
| Pool x, Pool y -> equal x y
|
||||
| Handle x, Handle y -> equal x y
|
||||
| Option x, Option y -> equal x y
|
||||
| Fn (ps, r), Fn (ps', r') ->
|
||||
List.length ps = List.length ps'
|
||||
@ -137,8 +116,6 @@ let rec to_string = function
|
||||
| Ptr t -> "(Ptr " ^ to_string t ^ ")"
|
||||
| Alloc -> "Allocator"
|
||||
| Vec t -> "(Vec " ^ to_string t ^ ")"
|
||||
| Pool t -> "(Pool " ^ to_string t ^ ")"
|
||||
| Handle t -> "(Handle " ^ to_string t ^ ")"
|
||||
| Option t -> "(Option " ^ to_string t ^ ")"
|
||||
| Fn (ps, r) ->
|
||||
Printf.sprintf "(Fn [%s] %s)"
|
||||
@ -147,20 +124,6 @@ let rec to_string = function
|
||||
|
||||
let is_numeric = function Int _ | Float _ -> true | _ -> false
|
||||
|
||||
(* Move-only: binding, passing or returning one transfers ownership and the
|
||||
source binding is dead afterwards (spec-memory.md, "The four container
|
||||
types"). That rule is what makes a double free unrepresentable, which is why
|
||||
[free] needs no analysis of its own. A struct that owns one is move-only
|
||||
too; that arrives with [drop], which is the step after this one. *)
|
||||
let rec is_move_only = function
|
||||
(* A [Pool] owns its storage; a [Handle] into one owns nothing, which is the
|
||||
point of it — handles are copied freely, and the pool is the single
|
||||
owner that [free] applies to. *)
|
||||
| Vec _ | Map _ | Pool _ -> true
|
||||
| Option t -> is_move_only t
|
||||
| Array (_, t) -> is_move_only t
|
||||
| _ -> false
|
||||
|
||||
(* The key types the first Map implementation admits (spec-memory.md, "Maps —
|
||||
first implementation"): integers, enums, strings, fixed arrays, and value
|
||||
structs composed recursively from those. Equality and hashing for them are
|
||||
@ -179,11 +142,6 @@ let rec keyable = function
|
||||
| Float _ -> false (* NaN /= NaN, and 0.0 and -0.0 differ bytewise *)
|
||||
| Array (_, t) -> keyable t
|
||||
| Named _ -> true (* [Check] decides, by walking the fields *)
|
||||
(* A [Handle] is not a map key, for the reason a [Ptr] is not: hashing an
|
||||
identity is a different operation from hashing what it names, and a
|
||||
handle whose slot has been reused hashes the same as it always did while
|
||||
naming nothing. The type exists to make that difference visible, so
|
||||
burying it under a key is the one thing it must not do. *)
|
||||
| _ -> false
|
||||
|
||||
(* Ordering and equality are defined on machine types and on nothing else at
|
||||
@ -191,14 +149,7 @@ let rec keyable = function
|
||||
unconstrained type supports only what every type supports (plan.org, Types). *)
|
||||
let is_comparable = function Enum _ -> true | t -> is_numeric t
|
||||
|
||||
(* [=] and [!=] admit one more type than [<] does. A [Handle] is a pair of
|
||||
numbers in a 64-bit word, so "is this the same entity" is one integer
|
||||
compare and is worth having — two handles are equal exactly when they name
|
||||
the same slot at the same generation, so a stale handle is never equal to
|
||||
the live one that replaced it. Ordering handles would compare a slot index,
|
||||
which means nothing: allocation order is a free-list artefact. Hence two
|
||||
predicates rather than one. *)
|
||||
let is_equatable = function Handle _ -> true | t -> is_comparable t
|
||||
let is_equatable = is_comparable
|
||||
|
||||
(* [Never] is the type of an expression that does not produce a value: return,
|
||||
an early-returning `some`, exit. It fits anywhere, and that is the only
|
||||
|
||||
14
lib/x86.ml
14
lib/x86.ml
@ -461,10 +461,10 @@ let alignof md t = snd (Emit.lay md t)
|
||||
let is_agg (t : Types.t) =
|
||||
match t with
|
||||
| Types.Int _ | Types.Float _ | Types.Bool | Types.Ptr _ | Types.Enum _
|
||||
| Types.Alloc | Types.Handle _ | Types.Fn _ -> false
|
||||
| Types.Alloc | Types.Fn _ -> false
|
||||
| Types.Unit | Types.Never -> false
|
||||
| Types.String | Types.Slice _ | Types.Array _ | Types.Map _ | Types.Vec _
|
||||
| Types.Pool _ | Types.Option _ | Types.Named _ -> true
|
||||
| Types.Option _ | Types.Named _ -> true
|
||||
| Types.Var v -> unsupported "type variable %s" v
|
||||
|
||||
let is_void (t : Types.t) = match t with Types.Unit | Types.Never -> true | _ -> false
|
||||
@ -1300,7 +1300,7 @@ let classify_c (l : loc) (t : Types.t) =
|
||||
match t with
|
||||
| Types.String | Types.Slice _ -> [ Aint (l, Types.Ptr Types.Unit); Alen l ]
|
||||
| Types.Unit | Types.Never -> []
|
||||
| Types.Vec _ | Types.Map _ | Types.Pool _ -> [ Aptr l ]
|
||||
| Types.Vec _ | Types.Map _ -> [ Aptr l ]
|
||||
| _ when is_agg t ->
|
||||
unsupported "aggregate %s across the C boundary" (Types.to_string t)
|
||||
| _ when is_float t -> [ Aflt (l, t) ]
|
||||
@ -2481,7 +2481,7 @@ and call_rt f ~sym ~args ~rty dst =
|
||||
call_native f ~sym ~chan:(rt_signals sym) ~args ~rty dst
|
||||
|
||||
and call_native f ~sym ?(chan = false) ~(args : Tast.expr list) ~rty dst =
|
||||
(* A Vec, a Map and a Pool are move-only and cross to the runtime as their
|
||||
(* A Vec and a Map cross to the runtime as their
|
||||
*address*, which is what lets an operation mutate the caller's container
|
||||
in place. [eval] would hand over the address of a copy, and the runtime
|
||||
would grow that and leave the caller's header at length zero — which is
|
||||
@ -2492,7 +2492,7 @@ and call_native f ~sym ?(chan = false) ~(args : Tast.expr list) ~rty dst =
|
||||
List.map
|
||||
(fun (a : Tast.expr) ->
|
||||
(match a.Tast.ty with
|
||||
| Types.Vec _ | Types.Map _ | Types.Pool _ -> lvalue f a
|
||||
| Types.Vec _ | Types.Map _ -> lvalue f a
|
||||
| _ -> eval f a), a.Tast.ty)
|
||||
args
|
||||
in
|
||||
@ -2515,7 +2515,7 @@ and call_native f ~sym ?(chan = false) ~(args : Tast.expr list) ~rty dst =
|
||||
counter-example and is not: [check.ml] builds it as [rt loc
|
||||
Types.Unit] and [flan_rt.c] writes the two words through [void *out].
|
||||
Every other [rt] builder in the file answers [Unit], an [Int], a
|
||||
[Ptr], an [Alloc] or a [Handle].
|
||||
[Ptr] or an [Alloc].
|
||||
- [crossable], which admits [String] and [Slice _] only as "a
|
||||
parameter" and refuses an aggregate return from a [declare] outright.
|
||||
|
||||
@ -2766,7 +2766,7 @@ and prim f (e : Tast.expr) (p : Tast.prim) (args : Tast.expr list) dst =
|
||||
touched until [call_rt], so answering [()] is already early enough. The
|
||||
test is [emit.ml]'s byte for byte, strict [>] included: bare
|
||||
[flan_dev_reg_note] is the runtime's own entry point and is never a
|
||||
[Tast.Rt]; what [check.ml] builds is the [_vec], [_map] and [_pool]
|
||||
[Tast.Rt]; what [check.ml] builds is the [_vec] and [_map]
|
||||
wrappers, each of which is longer than the prefix. The node's type is
|
||||
[Unit], so there is nothing to store and [dst] is untouched. *)
|
||||
| Tast.Rt sym, _
|
||||
|
||||
@ -906,8 +906,7 @@ struct flan_allocator {
|
||||
void *data;
|
||||
uint32_t caps;
|
||||
/* Bumped on every free-all. A container records it and traps if it moved:
|
||||
* spec-memory.md, "Dev builds detect a released region". Separate from the
|
||||
* per-Vec generation word, which answers a different question. */
|
||||
* spec-memory.md, "Dev builds detect a released region". */
|
||||
uint64_t epoch;
|
||||
/* Dev accounting for the general-purpose tier: "did you forget to free" is
|
||||
* an allocator-tier question and this is the allocator's answer. */
|
||||
@ -1392,30 +1391,26 @@ _Noreturn void flan_region_only_fail(const uint8_t *loc, int64_t loclen) {
|
||||
* produce the numbers, and it passes them in. There are no generics here and
|
||||
* none are needed.
|
||||
*
|
||||
* Header, and it is six words rather than the spec's four:
|
||||
* Header, and it is five words rather than the spec's four:
|
||||
*
|
||||
* ptr len cap allocator the release layout spec-memory.md fixes
|
||||
* gen bumped on every reallocation — the stale-slice
|
||||
* word spec-memory.md asks for. It has no reader
|
||||
* and cannot have one as things stand, which is
|
||||
* the part "not yet" used to hide: a slice is
|
||||
* ptr+len, so it carries neither the Vec it came
|
||||
* from nor the generation it was taken at, and
|
||||
* the check has nothing to compare. Giving it a
|
||||
* reader is a third word on every slice in the
|
||||
* language, not a change to this file. Nothing
|
||||
* here or anywhere else reads it; do not write
|
||||
* code that trusts it. See docs/BUILT.md.
|
||||
* epoch the allocator's epoch when this Vec last
|
||||
* touched it. Any operation on a container whose
|
||||
* recorded epoch has moved traps.
|
||||
*
|
||||
* The two dev words are present in every build, not only a dev one, and that
|
||||
* There used to be a sixth word, gen, the stale-slice generation
|
||||
* spec-memory.md once asked for. It was bumped on every reallocation and
|
||||
* consulted by nothing — a slice is ptr+len and carries neither the Vec it
|
||||
* came from nor the generation it was taken at, so the check it promised had
|
||||
* nothing to compare — and Odin's header (data, len, cap, allocator, and
|
||||
* nothing else) is the model this one follows. Deleted 2026-09-18 with the
|
||||
* ownership repeal; see docs/BUILT.md.
|
||||
*
|
||||
* The epoch word is present in every build, not only a dev one, and that
|
||||
* is not laziness: a redefinition module is built by llc and ld against a host
|
||||
* that was built separately, and nothing makes the two agree on a struct size.
|
||||
* A layout that changes with a build flag is a layout that can disagree across
|
||||
* that boundary silently. Dropping them in release is deferred and docs/BUILT.md
|
||||
* says what it is blocked on.
|
||||
* that boundary silently.
|
||||
*
|
||||
* Every entry point returns int8_t 1/0 for "did it fit", and never reports
|
||||
* failure any other way: the condition, the restart and the message are the
|
||||
@ -1426,7 +1421,6 @@ typedef struct flan_vec {
|
||||
int64_t len;
|
||||
int64_t cap;
|
||||
flan_allocator *alloc;
|
||||
int64_t gen;
|
||||
int64_t epoch;
|
||||
} flan_vec;
|
||||
|
||||
@ -1546,7 +1540,6 @@ static int8_t flan_vec_grow(flan_vec *v, int64_t want, int64_t size,
|
||||
v->cap = cap;
|
||||
/* Any slice taken before this points at storage that may have moved. The
|
||||
* word is bumped here and read nowhere yet; see docs/BUILT.md. */
|
||||
v->gen++;
|
||||
return 1;
|
||||
}
|
||||
|
||||
@ -1565,7 +1558,6 @@ int8_t flan_vec_init(flan_vec *v, flan_allocator *a, int64_t cap, int64_t size,
|
||||
v->ptr = NULL;
|
||||
v->len = 0;
|
||||
v->cap = 0;
|
||||
v->gen = 0;
|
||||
v->alloc = a;
|
||||
v->epoch = (int64_t)v->alloc->epoch;
|
||||
if (cap <= 0) return 1;
|
||||
@ -1649,7 +1641,6 @@ void flan_vec_free(flan_vec *v, int64_t size, int64_t align,
|
||||
v->len = 0;
|
||||
v->cap = 0;
|
||||
v->alloc = NULL;
|
||||
v->gen++;
|
||||
v->epoch = 0;
|
||||
}
|
||||
|
||||
@ -1663,284 +1654,6 @@ int8_t flan_vec_clone(flan_vec *dst, flan_vec *src, flan_allocator *a,
|
||||
return 1;
|
||||
}
|
||||
|
||||
/* ── (Pool T) and (Handle T), spec-memory.md ─────────────────────────
|
||||
*
|
||||
* A handle is a reference to something that can die, which reports that it
|
||||
* died rather than silently resolving to whatever reused its slot. That is
|
||||
* the whole design, and every decision below follows from it.
|
||||
*
|
||||
* THE PACKING. A handle is one int64_t: the slot index in the low 32 bits and
|
||||
* that slot's generation counter in the high 32. One word, so it copies,
|
||||
* zeroes and compares like the integer it is, and owns nothing — the pool is
|
||||
* the single owner. 32 bits of index because a Vec's index is an i32 here and
|
||||
* widening indices is one change across every container, not a pool question.
|
||||
*
|
||||
* LIVE IS ODD. A slot's generation starts at 0 and is bumped on every
|
||||
* allocation and on every release, so an odd generation means live and an
|
||||
* even one means dead. Two things fall out of that and both are load-bearing:
|
||||
* a zeroed handle is generation 0, which is even, so it resolves to nothing
|
||||
* rather than to slot 0 — ZII gives a handle field the right meaning for
|
||||
* free; and iteration can ask a slot whether it is live without a second
|
||||
* array or a spare bit.
|
||||
*
|
||||
* WRAPPING RETIRES THE SLOT. 32 bits is 2^31 allocate/release pairs on one
|
||||
* slot — every frame at 60fps for a year and a bit — but "rare" is not an
|
||||
* answer when the failure is the silent wrong one this type exists to
|
||||
* prevent. So a release from generation 0xFFFFFFFF bumps to 0 and does *not*
|
||||
* put the slot back on the free list. The slot is retired: dead forever, its
|
||||
* payload leaked, and no future handle can ever collide with an old one.
|
||||
* Leaking is defined behaviour here (spec-memory.md, "Leaking is defined
|
||||
* behaviour") and one slot is a bounded price for making the collision
|
||||
* unrepresentable rather than unlikely.
|
||||
*
|
||||
* TWO FAILURES, KEPT APART. A stale handle answers "gone" — it is an answer,
|
||||
* not an error. A pool whose allocator was released traps, through the same
|
||||
* epoch check a Vec gets. They answer different questions and must not be
|
||||
* conflated, exactly as the Vec's generation and epoch words must not be.
|
||||
*
|
||||
* GROWTH IS TRANSACTIONAL, and that is not tidiness. spec-memory.md's
|
||||
* StorageExhausted restart re-attempts *the same call*, so a failed grow has
|
||||
* to leave the pool byte for byte as it was — including a cap that still
|
||||
* agrees with the real block sizes, since the next attempt passes cap as the
|
||||
* allocator's old_size. Two blocks grow together, so a resize-in-place of the
|
||||
* first followed by a failure on the second would leave cap describing
|
||||
* neither. Allocate both, copy, then release the old pair: the only state
|
||||
* mutated after the last thing that can fail.
|
||||
*/
|
||||
|
||||
typedef struct flan_pool_slot {
|
||||
uint32_t gen; /* odd: live. even: dead. 0: never allocated, or retired. */
|
||||
int32_t next; /* free-list link, -1 for the end. Meaningless while live. */
|
||||
} flan_pool_slot;
|
||||
|
||||
typedef struct flan_pool {
|
||||
void *items; /* cap payloads, size bytes each */
|
||||
flan_pool_slot *slots; /* cap slot headers, index-parallel with items */
|
||||
int64_t len; /* slot high-water: 0..len have ever been handed out */
|
||||
int64_t cap;
|
||||
int64_t live; /* how many of those are live now */
|
||||
int64_t free; /* head of the free list, -1 when empty */
|
||||
flan_allocator *alloc;
|
||||
int64_t epoch;
|
||||
} flan_pool;
|
||||
|
||||
static int64_t flan_handle_pack(int64_t i, uint32_t gen) {
|
||||
return (int64_t)(((uint64_t)gen << 32) | (uint64_t)(uint32_t)i);
|
||||
}
|
||||
|
||||
static int64_t flan_handle_index(int64_t h) {
|
||||
return (int64_t)(uint32_t)(uint64_t)h;
|
||||
}
|
||||
|
||||
static uint32_t flan_handle_gen(int64_t h) {
|
||||
return (uint32_t)((uint64_t)h >> 32);
|
||||
}
|
||||
|
||||
/* The same epoch check a Vec gets, and for the same reason. A pool that never
|
||||
* allocated has no allocator and nothing to check. */
|
||||
static void flan_pool_check(flan_pool *p, const uint8_t *loc, int64_t loclen) {
|
||||
if (p->alloc) {
|
||||
int64_t now = (int64_t)p->alloc->epoch;
|
||||
if (now != p->epoch) flan_vec_stale_fail(loc, loclen, p->epoch, now);
|
||||
}
|
||||
}
|
||||
|
||||
/* The same guard a Vec gets, at the same place and for the same reason — see
|
||||
* the note above [flan_vec_region_only]. */
|
||||
void flan_pool_region_only(flan_pool *p, const uint8_t *loc, int64_t loclen) {
|
||||
flan_alloc_region_only(p->alloc ? p->alloc : flan_context_allocator(),
|
||||
loc, loclen);
|
||||
}
|
||||
|
||||
static flan_allocator *flan_pool_adopt(flan_pool *p) {
|
||||
if (!p->alloc) {
|
||||
p->alloc = flan_context_allocator();
|
||||
p->epoch = (int64_t)p->alloc->epoch;
|
||||
}
|
||||
return p->alloc;
|
||||
}
|
||||
|
||||
static int8_t flan_pool_grow(flan_pool *p, int64_t want, int64_t size,
|
||||
int64_t align) {
|
||||
flan_allocator *a = flan_pool_adopt(p);
|
||||
int64_t cap = p->cap, sslot = (int64_t)sizeof(flan_pool_slot);
|
||||
int64_t ibytes, sbytes, total;
|
||||
void *ni, *ns;
|
||||
if (want <= cap) return 1;
|
||||
/* Doubling from four, exactly as the Vec grows. */
|
||||
if (cap < 4) cap = 4;
|
||||
while (cap < want) {
|
||||
if (cap > (int64_t)1 << 40) { cap = want; break; }
|
||||
cap *= 2;
|
||||
}
|
||||
/* Two products and their sum, all three checked: the pool asks for the items
|
||||
* and the slots as separate blocks but reports them as one number, and a
|
||||
* wrap in either half is the same memcpy past the end the Vec's is. */
|
||||
if (!flan_mul_bytes(cap, size, &ibytes)
|
||||
|| !flan_mul_bytes(cap, sslot, &sbytes)
|
||||
|| !flan_add_bytes(ibytes, sbytes, &total)) {
|
||||
flan_fail_bytes = FLAN_BYTES_UNREPRESENTABLE;
|
||||
flan_fail_align = align;
|
||||
flan_fail_id = (int64_t)(intptr_t)a;
|
||||
return 0;
|
||||
}
|
||||
flan_fail_bytes = total;
|
||||
flan_fail_align = align;
|
||||
flan_fail_id = (int64_t)(intptr_t)a;
|
||||
ni = a->proc(a, FLAN_ALLOC_ALLOC, NULL, 0, ibytes, align);
|
||||
if (!ni) return 0;
|
||||
ns = a->proc(a, FLAN_ALLOC_ALLOC, NULL, 0, sbytes, 8);
|
||||
if (!ns) {
|
||||
/* An allocator without can-free leaks the first block here. That is the
|
||||
* defined outcome and not a new one: the request failed because the
|
||||
* region is exhausted, and the region is about to be released whole or
|
||||
* the ceiling raised and the call re-attempted. */
|
||||
if (a->caps & FLAN_CAN_FREE)
|
||||
a->proc(a, FLAN_ALLOC_FREE, ni, ibytes, 0, align);
|
||||
return 0;
|
||||
}
|
||||
if (p->len > 0) {
|
||||
memcpy(ni, p->items, (size_t)(p->len * size));
|
||||
memcpy(ns, p->slots, (size_t)(p->len * sslot));
|
||||
}
|
||||
if (p->items && (a->caps & FLAN_CAN_FREE)) {
|
||||
a->proc(a, FLAN_ALLOC_FREE, p->items, p->cap * size, 0, align);
|
||||
a->proc(a, FLAN_ALLOC_FREE, p->slots, p->cap * sslot, 0, 8);
|
||||
}
|
||||
p->items = ni;
|
||||
p->slots = ns;
|
||||
p->cap = cap;
|
||||
return 1;
|
||||
}
|
||||
|
||||
int8_t flan_pool_init(flan_pool *p, flan_allocator *a, int64_t size,
|
||||
int64_t align, const uint8_t *loc, int64_t loclen) {
|
||||
(void)size; (void)align;
|
||||
/* Null for the same reason and with the same answer flan_vec_init gives:
|
||||
* the no-allocator-named case never arrives here as NULL. */
|
||||
if (!a) flan_null_alloc_fail(loc, loclen);
|
||||
p->items = NULL;
|
||||
p->slots = NULL;
|
||||
p->len = 0;
|
||||
p->cap = 0;
|
||||
p->live = 0;
|
||||
p->free = -1;
|
||||
p->alloc = a;
|
||||
p->epoch = (int64_t)a->epoch;
|
||||
return 1;
|
||||
}
|
||||
|
||||
/* 1/0 for "did it fit", like every other allocating entry point. The handle
|
||||
* goes out through [out] rather than being returned, so that the compiler's
|
||||
* alloc_guard reads the answer and the handle separately. */
|
||||
int8_t flan_pool_insert(flan_pool *p, const void *elem, int64_t *out,
|
||||
int64_t size, int64_t align, const uint8_t *loc,
|
||||
int64_t loclen) {
|
||||
int64_t i;
|
||||
flan_pool_check(p, loc, loclen);
|
||||
if (p->free >= 0) {
|
||||
i = p->free;
|
||||
p->free = p->slots[i].next;
|
||||
} else {
|
||||
if (p->len + 1 > p->cap && !flan_pool_grow(p, p->len + 1, size, align))
|
||||
return 0;
|
||||
i = p->len++;
|
||||
p->slots[i].gen = 0;
|
||||
p->slots[i].next = -1;
|
||||
}
|
||||
p->slots[i].gen++; /* even -> odd: this slot is live */
|
||||
p->live++;
|
||||
memcpy((uint8_t *)p->items + i * size, elem, (size_t)size);
|
||||
*out = flan_handle_pack(i, p->slots[i].gen);
|
||||
return 1;
|
||||
}
|
||||
|
||||
/* NULL when the handle names nothing, which the compiler turns into None. The
|
||||
* index is bounded with the unsigned comparison flan_vec_at uses, because the
|
||||
* low half of a handle can be any 32 bits at all. */
|
||||
void *flan_pool_resolve(flan_pool *p, int64_t h, int64_t size,
|
||||
const uint8_t *loc, int64_t loclen) {
|
||||
int64_t i = flan_handle_index(h);
|
||||
uint32_t g = flan_handle_gen(h);
|
||||
flan_pool_check(p, loc, loclen);
|
||||
if (!(g & 1u)) return NULL; /* a zeroed or dead handle */
|
||||
if ((uint64_t)i >= (uint64_t)p->len) return NULL;
|
||||
if (p->slots[i].gen != g) return NULL; /* the slot was reused */
|
||||
return (uint8_t *)p->items + i * size;
|
||||
}
|
||||
|
||||
/* 1 if this call released it, 0 if the handle was already gone. Releasing
|
||||
* twice is therefore an answer rather than undefined behaviour — which is the
|
||||
* generational scheme paying for itself a second time, since a pool is the
|
||||
* one place a double free is *detectable* rather than merely refused. */
|
||||
int8_t flan_pool_release(flan_pool *p, int64_t h, const uint8_t *loc,
|
||||
int64_t loclen) {
|
||||
int64_t i = flan_handle_index(h);
|
||||
uint32_t g = flan_handle_gen(h), was;
|
||||
flan_pool_check(p, loc, loclen);
|
||||
if (!(g & 1u)) return 0;
|
||||
if ((uint64_t)i >= (uint64_t)p->len) return 0;
|
||||
if (p->slots[i].gen != g) return 0;
|
||||
was = p->slots[i].gen;
|
||||
p->slots[i].gen = was + 1; /* odd -> even: dead, and every old handle with it */
|
||||
p->live--;
|
||||
/* The wrap. See the header: the slot is retired rather than reissued. */
|
||||
if (was != 0xFFFFFFFFu) {
|
||||
p->slots[i].next = (int32_t)p->free;
|
||||
p->free = i;
|
||||
}
|
||||
return 1;
|
||||
}
|
||||
|
||||
int64_t flan_pool_len(flan_pool *p, const uint8_t *loc, int64_t loclen) {
|
||||
flan_pool_check(p, loc, loclen);
|
||||
return p->len;
|
||||
}
|
||||
|
||||
int64_t flan_pool_live(flan_pool *p, const uint8_t *loc, int64_t loclen) {
|
||||
flan_pool_check(p, loc, loclen);
|
||||
return p->live;
|
||||
}
|
||||
|
||||
/* The handle of slot [i], or 0 — the never-valid handle — if that slot is
|
||||
* dead. This plus (len p) is the whole of enumeration, which is what
|
||||
* migrate-instances needs and what a Vec behind an index cannot give: a Vec's
|
||||
* indices shift under a removal and a pool's never do. Out of range traps
|
||||
* rather than answering 0, because an index is an index here and 0..len are
|
||||
* the valid ones. */
|
||||
int64_t flan_pool_handle(flan_pool *p, int32_t i, const uint8_t *loc,
|
||||
int64_t loclen) {
|
||||
uint32_t g;
|
||||
flan_pool_check(p, loc, loclen);
|
||||
if ((uint64_t)(int64_t)i >= (uint64_t)p->len)
|
||||
flan_vec_bounds_fail(loc, loclen, (int64_t)i, p->len);
|
||||
g = p->slots[i].gen;
|
||||
if (!(g & 1u)) return 0;
|
||||
return flan_handle_pack((int64_t)i, g);
|
||||
}
|
||||
|
||||
/* spec-memory.md's first release point, applied to the owner. Zeroed rather
|
||||
* than left dangling, for the reason flan_vec_free zeroes. Every handle into
|
||||
* it is stale afterwards and says so: len goes to 0, so the bound check
|
||||
* answers "gone" for all of them. */
|
||||
void flan_pool_free(flan_pool *p, int64_t size, int64_t align,
|
||||
const uint8_t *loc, int64_t loclen) {
|
||||
flan_pool_check(p, loc, loclen);
|
||||
if (p->items && p->alloc && (p->alloc->caps & FLAN_CAN_FREE)) {
|
||||
p->alloc->proc(p->alloc, FLAN_ALLOC_FREE, p->items, p->cap * size, 0, align);
|
||||
p->alloc->proc(p->alloc, FLAN_ALLOC_FREE, p->slots,
|
||||
p->cap * (int64_t)sizeof(flan_pool_slot), 0, 8);
|
||||
}
|
||||
p->items = NULL;
|
||||
p->slots = NULL;
|
||||
p->len = 0;
|
||||
p->cap = 0;
|
||||
p->live = 0;
|
||||
p->free = -1;
|
||||
p->alloc = NULL;
|
||||
p->epoch = 0;
|
||||
}
|
||||
|
||||
/* ── (Map K V), spec-memory.md ──────────────────────────────────────────
|
||||
*
|
||||
* Odin's map, followed deliberately: open-addressed Robin Hood hashing at a
|
||||
@ -1979,11 +1692,11 @@ void flan_pool_free(flan_pool *p, int64_t size, int64_t align,
|
||||
* data one allocation: keys | values | hashes | scratch
|
||||
* len live entries
|
||||
* log2cap 0 until something is allocated; never 1 or 2 after
|
||||
* allocator gen epoch as on a Vec, and checked the same way
|
||||
* allocator epoch as on a Vec, and checked the same way
|
||||
*
|
||||
* Odin stuffs log2cap into the low six bits of the data pointer because its
|
||||
* Raw_Map must be three words. This header already carries an allocator, a
|
||||
* generation and an epoch, so the bit-stuffing would buy nothing and cost a
|
||||
* Raw_Map must be three words. This header already carries an allocator and
|
||||
* an epoch, so the bit-stuffing would buy nothing and cost a
|
||||
* mask on every access — and, more usefully, not tagging means correctness
|
||||
* never depends on the block being 64-byte aligned. It is requested as 64, and
|
||||
* cell packing pays off when the request is honoured, but an arena whose base
|
||||
@ -2035,7 +1748,6 @@ typedef struct flan_map {
|
||||
int64_t len;
|
||||
int64_t log2cap;
|
||||
flan_allocator *alloc;
|
||||
int64_t gen;
|
||||
int64_t epoch;
|
||||
} flan_map;
|
||||
|
||||
@ -2552,7 +2264,7 @@ static int8_t flan_map_grow(flan_map *m, int64_t want, int64_t ksize,
|
||||
if (log2cap <= m->log2cap && m->data) return 1;
|
||||
|
||||
fresh.data = NULL; fresh.len = 0; fresh.log2cap = 0;
|
||||
fresh.alloc = a; fresh.gen = 0; fresh.epoch = (int64_t)a->epoch;
|
||||
fresh.alloc = a; fresh.epoch = (int64_t)a->epoch;
|
||||
if (!flan_map_alloc(&fresh, a, log2cap, ksize, vsize)) return 0;
|
||||
|
||||
if (m->data) {
|
||||
@ -2580,7 +2292,6 @@ static int8_t flan_map_grow(flan_map *m, int64_t want, int64_t ksize,
|
||||
m->len = fresh.len;
|
||||
/* Every key and value moved, so any pointer into the old block is stale —
|
||||
* the same word, bumped for the same reason, as a Vec's reallocation. */
|
||||
m->gen++;
|
||||
return 1;
|
||||
}
|
||||
|
||||
@ -2591,7 +2302,6 @@ int8_t flan_map_init(flan_map *m, flan_allocator *a, int64_t ksize,
|
||||
m->data = NULL;
|
||||
m->len = 0;
|
||||
m->log2cap = 0;
|
||||
m->gen = 0;
|
||||
m->alloc = a;
|
||||
m->epoch = (int64_t)a->epoch;
|
||||
/* No block until something is put in it: an empty map that is never written
|
||||
@ -2807,7 +2517,6 @@ void flan_map_free(flan_map *m, int64_t ksize, int64_t vsize,
|
||||
m->len = 0;
|
||||
m->log2cap = 0;
|
||||
m->alloc = NULL;
|
||||
m->gen++;
|
||||
m->epoch = 0;
|
||||
}
|
||||
|
||||
@ -2848,9 +2557,8 @@ int8_t flan_map_clone(flan_map *dst, flan_map *src, flan_allocator *a,
|
||||
*
|
||||
* The type name comes from the compiler; the *extent* comes from here, because
|
||||
* the header is the only thing that knows where the storage landed and how
|
||||
* much of it there is. Three entry points rather than one because three
|
||||
* headers are three layouts, and a pool is two blocks that are allocated and
|
||||
* released together but are not adjacent.
|
||||
* much of it there is. Two entry points rather than one because the two
|
||||
* headers are two layouts.
|
||||
*
|
||||
* Each is called immediately after the operation that may have allocated —
|
||||
* every one of them, not only the first — because storage moves. A note is an
|
||||
@ -2865,18 +2573,6 @@ void flan_dev_reg_note_vec(flan_vec *v, int64_t size, const char *type,
|
||||
if (v) flan_dev_reg_note(v->ptr, v->cap * size, size, type, typelen);
|
||||
}
|
||||
|
||||
void flan_dev_reg_note_pool(flan_pool *p, int64_t size, const char *type,
|
||||
int64_t typelen) {
|
||||
if (!p) return;
|
||||
flan_dev_reg_note(p->items, p->cap * size, size, type, typelen);
|
||||
/* The slot headers are the pool's own bookkeeping and not the element type,
|
||||
so they are named for what they are. Recording them matters for the same
|
||||
reason the items do: after a free-all their bytes are still readable and
|
||||
an address landing in them must not come back as an element. */
|
||||
flan_dev_reg_note(p->slots, p->cap * (int64_t)sizeof(flan_pool_slot),
|
||||
(int64_t)sizeof(flan_pool_slot), "pool slots", 11);
|
||||
}
|
||||
|
||||
void flan_dev_reg_note_map(flan_map *m, int64_t ksize, int64_t vsize,
|
||||
const char *type, int64_t typelen) {
|
||||
if (!m || !m->data) return;
|
||||
|
||||
@ -29,11 +29,10 @@ facility (see plan.org, "Managed classes").
|
||||
or a literal in read-only memory. Copying a slice copies ptr+len, never the
|
||||
elements. A slice may be `const`-qualified; freeing through one is not possible
|
||||
because a slice has no allocator and no `cap`.
|
||||
- `(Vec T)` and `(Map K V)` are **move-only**. Assignment hands over the one
|
||||
header rather than copying it — there is no implicit shallow copy, so two
|
||||
owners never arise from an assignment; `(clone x)` is the only spelling of a
|
||||
second, independent one. Since the repeal, using the source binding again is
|
||||
not a compile error: the header is still there, and a program that frees
|
||||
- `(Vec T)` and `(Map K V)` **were move-only**; the second repeal removed the
|
||||
concept. Assignment copies the header, the copies alias one buffer, and
|
||||
`(clone x)` is the spelling of an independent one. Using a binding after
|
||||
assigning it away is ordinary: the header is still there, and a program that frees
|
||||
through it twice or reads through it after a free misbehaves at run time,
|
||||
where the allocator and the dev build's generation word are the net.
|
||||
|
||||
@ -78,7 +77,10 @@ points at.
|
||||
allocator; `(clone x alloc)` names one. Value types (`[n T]`, structs of value
|
||||
types, primitives) need no `clone` — assignment already copies them.
|
||||
|
||||
A struct containing a `Vec` field is itself move-only. Ownership is structural,
|
||||
A struct containing a `Vec` field was itself move-only until the second
|
||||
repeal; since it, the field is admitted and the struct copies like any other
|
||||
(see "The repeal"). The paragraphs below record the rule as designed.
|
||||
Ownership is structural,
|
||||
not declared: a type is a value type iff all of its fields are **and it declares
|
||||
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
|
||||
@ -106,12 +108,13 @@ region" for the rule that stands in its place and for what it costs.
|
||||
- A future lightweight provenance pass may reject the obvious mistakes (a
|
||||
borrow of a local escaping, use after an owner moves, and reallocation with a
|
||||
live borrow). It must not require Rust-style lifetime annotations or dictate
|
||||
an ECS-shaped object model. Long-lived graph links use `(Handle a)`; temporary
|
||||
graphs may use explicitly managed, stable region storage.
|
||||
- Cross-referencing long-lived objects uses `(Handle a)` into a pool, never a
|
||||
raw pointer or slice. A stale handle is detectable.
|
||||
an ECS-shaped object model.
|
||||
- Cross-referencing long-lived objects used `(Handle a)` into a `Pool` until
|
||||
the second repeal (below) removed both: two containers proved enough, and a
|
||||
program that wants generational indirection builds it over a `Vec`, as an
|
||||
Odin program does.
|
||||
|
||||
## Globals of move-only type
|
||||
## Container globals
|
||||
|
||||
A global may be a `Vec` or a `Map`. Its intended lifetime is the process's — it
|
||||
is loaded once and never released — and before the repeal a flow rule enforced
|
||||
@ -127,10 +130,9 @@ take their target as a borrow, so a global `(Vec u8)` is filled and grown where
|
||||
it stands. The aliasing contract is the one above and nothing more — a push that
|
||||
reallocates invalidates a slice taken before it, and that is the programmer's
|
||||
whether the owner is a local or a global. Globals get no borrow rule locals do
|
||||
not have; the dev build's generation word lives on the `Vec`, so the stale-slice
|
||||
trap works the same either way.
|
||||
not have.
|
||||
|
||||
A move-only global **starts zeroed** — a zeroed `Vec` is an empty `Vec` — and is
|
||||
A container global **starts zeroed** — a zeroed `Vec` is an empty `Vec` — and is
|
||||
loaded by whichever function loads it, with an ordinary assignment:
|
||||
|
||||
```
|
||||
@ -147,6 +149,9 @@ first block and leaks it; there is no `drop`, and freeing is a thing you write.
|
||||
|
||||
## The repeal — 2026-09-18
|
||||
|
||||
(Extended the same day by a second round; see the amendments at the end of
|
||||
this section.)
|
||||
|
||||
The first implementation carried a static flow analysis: a per-function dead
|
||||
set recording moved-out bindings, a borrow flag over the container-reading
|
||||
operations, an iteration diff for loops, and a borrowed-never-moved rule for
|
||||
@ -162,17 +167,31 @@ believed.
|
||||
What the language promises after the repeal is Odin's contract, which is the
|
||||
model this memory design was built from in the first place:
|
||||
|
||||
- **The types** still decide what may be copied and what may own what: move-only
|
||||
assignment hands over the header, `clone` is the only copy, and the
|
||||
struct/union/pool ownership rules all stand.
|
||||
- **The allocator** still decides what a free means: `can-free`, regions,
|
||||
- **The allocator** decides what a free means: `can-free`, regions,
|
||||
`free-all`, and the region-only rules for containers of owning elements all
|
||||
stand.
|
||||
- **Which frees run, and when, is the program's.** `defer` is the tool, and a
|
||||
double free or use-after-free is a run-time misbehaviour, not a compile
|
||||
error.
|
||||
- **The dev build detects.** The generation word on `Vec`, the region epoch
|
||||
trap, and the block registry are the net, where a game is actually run.
|
||||
- **The dev build detects.** The region epoch trap and the block registry are
|
||||
the net, where a game is actually run.
|
||||
|
||||
The same day, the rest of the concept followed, on the same argument carried
|
||||
to its end:
|
||||
|
||||
- **The move-only concept itself is gone.** Everything copies — a container as
|
||||
its header, the copies aliasing one buffer. The `copyable?` predicate went
|
||||
with it (four predicates remain), as did the struct, data-type and union
|
||||
owning-field refusals: a struct may hold a `Vec`, and the two-headers-one-
|
||||
buffer aliasing that buys is the program's, exactly as it is in Odin.
|
||||
- **`Pool` and `(Handle a)` are gone.** Two containers are enough; a slab with
|
||||
generational handles is a library a program writes over a `Vec` when it
|
||||
wants one, which is where Odin keeps it too.
|
||||
- **The `gen` word is gone from both headers.** It was bumped on every
|
||||
reallocation and read by nothing — the stale-slice check it promised needs a
|
||||
third word on every slice, not a word here. A `Vec` is now
|
||||
`ptr len cap allocator epoch`; the epoch word stays because free-all
|
||||
detection reads it on every operation.
|
||||
|
||||
A future provenance pass (the "Open" section at the end of this document, and
|
||||
plan.org #3) remains the door back to static checking. It is additive: nothing
|
||||
@ -235,13 +254,13 @@ instantiates it:
|
||||
> field-free storage. It does **not** support `=`, `<`, `+`, or `hash`.
|
||||
|
||||
What makes that liveable is a `where` clause of compile-time type predicates,
|
||||
written as a map at the head of the body. There are five — `ordered?`, `equal?`,
|
||||
`hashable?`, `numeric?`, `copyable?` — they are not type classes because a
|
||||
written as a map at the head of the body. There are four — `ordered?`,
|
||||
`equal?`, `hashable?`, `numeric?` — they are not type classes because a
|
||||
predicate carries no implementations and merely gates a builtin the compiler
|
||||
already has, and they entail one another in one direction, so one clause usually
|
||||
does. A variable is move-only by default and `copyable?` is the opt-out, because
|
||||
whether a variable moves is not decidable abstractly. plan.org's Types section
|
||||
has the full account.
|
||||
already has, and they entail one another in one direction, so one clause
|
||||
usually does. (`copyable?` was the fifth until the second repeal removed the
|
||||
move concept it opted out of.) plan.org's Types section has the full
|
||||
account.
|
||||
|
||||
```
|
||||
(defn sort! [s [$t]] ()
|
||||
@ -480,7 +499,8 @@ 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
|
||||
A `Pool` was admitted with the others while it existed (the second repeal
|
||||
removed the type), and it was 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
|
||||
@ -611,7 +631,11 @@ practice: a union is all-bytes-zero unless `uninit` says otherwise.
|
||||
|
||||
Three things a union may not do, and each for a reason that does not expire:
|
||||
|
||||
- **No move-only member.** Nothing knows which member is live, so nothing can
|
||||
- **No owning member** — until the second repeal, which admits one: nothing
|
||||
records which member is live, and since nothing (the program included) can
|
||||
free the right one through the union itself, the tag the program keeps
|
||||
beside it is the way, C's way. The rest of this entry records the rule as
|
||||
designed. Nothing knows which member is live, so nothing can
|
||||
tear one down. Unlike the struct and `defdata` refusals, this is not waiting
|
||||
on recursive teardown — there is no fact for teardown to read, and freeing
|
||||
the wrong member is a free of a pointer that was an `f64` a moment ago.
|
||||
|
||||
@ -3,7 +3,6 @@
|
||||
;; prelude; it is the same bodies, over $t, checked and run.
|
||||
|
||||
(defn keep [s [$t] keep? (Fn [$t] bool)] (Vec $t)
|
||||
{:where (copyable? $t)}
|
||||
(let [v (vec-new t)]
|
||||
(dotimes [i (len s)]
|
||||
(when (keep? (at s i))
|
||||
@ -15,7 +14,6 @@
|
||||
(set (at s i) (f (at s i)))))
|
||||
|
||||
(defn fold [s [$t] init $t f (Fn [$t $t] $t)] t
|
||||
{:where (copyable? $t)}
|
||||
(let [acc init]
|
||||
(dotimes [i (len s)]
|
||||
(set acc (f acc (at s i))))
|
||||
|
||||
@ -5,6 +5,6 @@
|
||||
;;;; Session.eval runs the same code the thing that hung was C-c C-c with the
|
||||
;;;; dev daemon wedged behind it. The refusal names the chain of
|
||||
;;;; instantiations rather than a depth it gave up at.
|
||||
(defn grow [x $t] () {:where (copyable? $t)} (grow [x x]))
|
||||
(defn grow [x $t] () (grow [x x]))
|
||||
|
||||
(defn main [] () (grow 1))
|
||||
|
||||
@ -21,13 +21,11 @@
|
||||
;; The variable is bound *inside* a type constructor, which is a structural
|
||||
;; walk rather than a name match.
|
||||
(defn first-or [s [$t] d $t] $t
|
||||
{:where (copyable? $t)}
|
||||
(if (= (len s) 0) d (at s 0)))
|
||||
|
||||
;; A generic calling a generic at its own variable: the copy of [swap!] is
|
||||
;; generated when [rotate!] is instantiated and not before.
|
||||
(defn rotate! [s [$t]] ()
|
||||
{:where (copyable? $t)}
|
||||
(dotimes [i (- (len s) 1)]
|
||||
(swap! s i (+ i 1))))
|
||||
|
||||
@ -37,7 +35,7 @@
|
||||
(+ x x))
|
||||
|
||||
;; equal? admits = and !=; ordered? admits < <= > >= min max, and entails
|
||||
;; equal? and copyable?.
|
||||
;; equal?.
|
||||
(defn count-of [s [$t] x $t] i32
|
||||
{:where (equal? $t)}
|
||||
(let [n 0]
|
||||
@ -52,14 +50,12 @@
|
||||
|
||||
;; Two variables, and the second is determined by its own argument.
|
||||
(defn fst [a $t b $u] $t
|
||||
{:where [(copyable? $t) (copyable? $u)]}
|
||||
(do b a))
|
||||
|
||||
;; println over a type variable is the one form the abstract pass defers to
|
||||
;; the instantiation, because its legality is only decidable after
|
||||
;; substituting. The structural printer is selected per copy.
|
||||
(defn show [x $t] ()
|
||||
{:where (copyable? $t)}
|
||||
(println x))
|
||||
|
||||
;; A cast to a type variable. [(t x)] is not a name [is_cast] knows — [t] is
|
||||
@ -71,11 +67,8 @@
|
||||
(do d (t x)))
|
||||
|
||||
;; The builtins that take a *type name* as an argument, over a variable. Each
|
||||
;; reaches the one list of what names a type, so all three came at once.
|
||||
;; (pool-new t) and (map-new t i32) are the other two; a Pool of a variable
|
||||
;; needs it not to be move-only, which [copyable?] is.
|
||||
;; reaches the one list of what names a type; (map-new t i32) is the other.
|
||||
(defn one-of [x $t] (Vec $t)
|
||||
{:where (copyable? $t)}
|
||||
(let [v (vec-new t)]
|
||||
(push v x)
|
||||
v))
|
||||
@ -83,7 +76,6 @@
|
||||
;; (zeroed) takes its type from the position it is written in, so a variable
|
||||
;; in that position is answered by the instantiation like any other type.
|
||||
(defn zero-of [x $t] $t
|
||||
{:where (copyable? $t)}
|
||||
(do x (zeroed)))
|
||||
|
||||
;; The map operations over a key that is a type variable. The hash and the
|
||||
|
||||
@ -1,103 +0,0 @@
|
||||
;;;; (Handle T) and (Pool T), spec-memory.md — "Cross-referencing long-lived
|
||||
;;;; objects uses (Handle a) into a pool, never a raw pointer or slice. A
|
||||
;;;; stale handle is detectable."
|
||||
;;;;
|
||||
;;;; The thesis, in one program: something holds a reference to an entity; the
|
||||
;;;; entity dies; the slot is reused by a different entity; and the old
|
||||
;;;; reference answers "gone" instead of answering wrong. Every other case
|
||||
;;;; here is secondary to that one.
|
||||
;;;;
|
||||
;;;; It is all one function because a Pool is move-only exactly as a Vec is,
|
||||
;;;; so passing one to a helper *consumes* it — there is no borrowing
|
||||
;;;; parameter in the language yet. That is not a pool question and this
|
||||
;;;; program does not work around it; see docs/BUILT.md.
|
||||
|
||||
(defstruct Enemy [hp i32 kind i32])
|
||||
|
||||
;; The projectile does not hold an Enemy and does not hold an index. It holds
|
||||
;; a handle, which is a number that owns nothing and copies freely — which is
|
||||
;; why a struct may contain one where it may not contain a Vec.
|
||||
(defstruct Projectile [target (Handle Enemy) damage i32])
|
||||
|
||||
(defn main [] i32
|
||||
(let [pool (pool-new Enemy)]
|
||||
(let [a (insert pool (Enemy {.hp 10 .kind 1}))
|
||||
b (insert pool (Enemy {.hp 20 .kind 2}))
|
||||
c (insert pool (Enemy {.hp 30 .kind 3}))
|
||||
sum 0]
|
||||
(println (len pool)) ; 3 slots handed out
|
||||
(println (live pool)) ; 3 of them live
|
||||
|
||||
;; Enumeration, which is what a world arena and an owned region do not
|
||||
;; give and which migrate-instances will need. (len p) is the slot
|
||||
;; high-water, so 0..(len p) visits every slot ever handed out, and
|
||||
;; (pool-handle p i) says which of them are still live.
|
||||
(dotimes [i (len pool)]
|
||||
(match (pool-handle pool i)
|
||||
(Some h) (match (resolve pool h)
|
||||
;; resolve yields a *pointer*, not a copy: mutating the
|
||||
;; pooled thing in place is what a pool is for, and a
|
||||
;; pattern binding binds a value.
|
||||
(Some e) (set sum (+ sum (.hp e)))
|
||||
None (do))
|
||||
None (do)))
|
||||
(println sum) ; 60
|
||||
|
||||
;; A write through a resolved pointer is a write to the pooled entity.
|
||||
(match (resolve pool b)
|
||||
(Some e) (set (.hp e) 21)
|
||||
None (do))
|
||||
(match (resolve pool b)
|
||||
(Some e) (println (.hp e)) ; 21
|
||||
None (println -1))
|
||||
|
||||
;; ── The thesis ────────────────────────────────────────────────
|
||||
;; A projectile chasing b. b dies. The slot is reused by a fourth
|
||||
;; enemy, which lands in exactly that slot — and the projectile's
|
||||
;; handle says so rather than chasing the newcomer.
|
||||
(let [shot (Projectile {.target b .damage 5})]
|
||||
(println (release pool b)) ; true — this call released it
|
||||
(println (release pool b)) ; false — it was already gone
|
||||
(println (live pool)) ; 2
|
||||
(let [d (insert pool (Enemy {.hp 99 .kind 4}))]
|
||||
;; Printed as index:generation. Same slot, later generation — the
|
||||
;; two halves of the answer, visible.
|
||||
(println b)
|
||||
(println d)
|
||||
(println (= d b)) ; false
|
||||
(println (= d d)) ; true
|
||||
(match (resolve pool (.target shot))
|
||||
(Some e) (println (.hp e))
|
||||
None (println -1)) ; -1, not 99
|
||||
(match (resolve pool d)
|
||||
(Some e) (println (.hp e)) ; 99
|
||||
None (println -1))
|
||||
(println (len pool)) ; still 3 slots
|
||||
(println (live pool)) ; 3 live
|
||||
|
||||
;; A zeroed handle is generation 0, which is even, and a live slot's
|
||||
;; generation is always odd — so ZII gives a handle field the right
|
||||
;; meaning for free rather than pointing it at slot 0.
|
||||
(let [z (Projectile {.damage 1})]
|
||||
(println (.target z))
|
||||
(match (resolve pool (.target z))
|
||||
(Some e) (println (.hp e))
|
||||
None (println -1))) ; -1
|
||||
|
||||
;; a and c are untouched by any of it.
|
||||
(match (resolve pool a)
|
||||
(Some e) (println (.hp e)) ; 10
|
||||
None (println -1))
|
||||
(match (resolve pool c)
|
||||
(Some e) (println (.hp e)) ; 30
|
||||
None (println -1))
|
||||
|
||||
;; spec-memory.md's first release point, applied to the owner. The
|
||||
;; runtime leaves the pool empty, so a handle into it would resolve
|
||||
;; to None rather than into released storage — but that is not
|
||||
;; demonstrable from here and this program does not pretend it is:
|
||||
;; free consumes pool, so a resolve on the next line is a compile
|
||||
;; error. The runtime property is real and the checker makes it
|
||||
;; unreachable.
|
||||
(free pool)
|
||||
0)))))
|
||||
@ -1,25 +0,0 @@
|
||||
;;;; The epoch trap on the pool's side. spec-memory.md, "Dev builds detect a
|
||||
;;;; released region".
|
||||
;;;;
|
||||
;;;; This is deliberately the *other* failure from a stale handle, and the two
|
||||
;;;; must not be conflated — the same rule that keeps a Vec's generation word
|
||||
;;;; and its epoch word apart. A stale handle is an answer: the entity died,
|
||||
;;;; resolve says None, the program carries on. A released region is not an
|
||||
;;;; answer at all: the storage the pool sits in is gone, the slot array with
|
||||
;;;; it, and there is nothing left to ask. So one returns None and the other
|
||||
;;;; traps naming the site.
|
||||
(defn main [] i32
|
||||
(let [a (arena-new 4096)]
|
||||
(let [p (pool-new i32 a)]
|
||||
(let [h (insert p 7)]
|
||||
(match (resolve p h)
|
||||
(Some x) (println (deref x))
|
||||
None (println -1))
|
||||
;; The region goes. p is still in scope, still looks fine, and h is
|
||||
;; still a perfectly well-formed handle — which is exactly the case a
|
||||
;; static rule cannot see.
|
||||
(free-all a)
|
||||
(match (resolve p h)
|
||||
(Some x) (println (deref x))
|
||||
None (println -1)))))
|
||||
0)
|
||||
@ -4,7 +4,7 @@
|
||||
;;;; nothing at run time can say what is at an address. The registry sidesteps
|
||||
;;;; that: the allocator's *caller* knew the type, and a dev build writes it
|
||||
;;;; down. What is asserted here is the consequence a program can see without
|
||||
;;;; an inspector — whether an address is still live — and the three ways
|
||||
;;;; an inspector — whether an address is still live — and the two ways
|
||||
;;;; storage dies underneath one.
|
||||
;;;;
|
||||
;;;; This program is deliberately readable in a release build too, and prints
|
||||
@ -48,17 +48,6 @@
|
||||
(free-all frame)
|
||||
(println (reg-live q)))) ; 0 either way
|
||||
|
||||
;; 3. And the pool, whose storage is the one place a (Ptr T) is handed to a
|
||||
;; program by name: (resolve p h) points into the middle of the items
|
||||
;; array, never at its base. Nothing but a containment lookup can answer
|
||||
;; for it.
|
||||
(let [pool (pool-new i32)]
|
||||
(let [h (insert pool 5)]
|
||||
(match (resolve pool h)
|
||||
(Some ip) (println (reg-live ip)) ; dev: 1
|
||||
None (println -1))
|
||||
(free pool)))
|
||||
|
||||
;; Nothing is live by now except whatever the arena's own destroy leaves, so
|
||||
;; the count is a statement about the table rather than about one address.
|
||||
(arena-destroy frame)
|
||||
|
||||
@ -11,13 +11,11 @@
|
||||
(defvar counter i64)
|
||||
|
||||
(defn put! [xs [$t] i i32 v $t] ()
|
||||
{:where (copyable? $t)}
|
||||
(set (at xs i) v))
|
||||
|
||||
;;; Calls [put!] at its own variable, so the copy of [put!] is generated when
|
||||
;;; [hold!] is instantiated and not before.
|
||||
(defn hold! [xs [$t] v $t] ()
|
||||
{:where (copyable? $t)}
|
||||
(put! xs 0 v))
|
||||
|
||||
(defn pick [xs [$t]] $t
|
||||
|
||||
@ -1,9 +1,7 @@
|
||||
;;;; spec-memory.md: "Ownership is structural, not declared" — a struct
|
||||
;;;; containing a Vec is itself move-only, transitively, with recursive
|
||||
;;;; teardown, and with a field that cannot be freed on its own. None of that
|
||||
;;;; machinery exists: it is the same recursive teardown `drop` brings, and it
|
||||
;;;; lands with it. Accepting the field meanwhile would give a struct that
|
||||
;;;; copies its header on assignment two owners of one buffer.
|
||||
;;;; A struct may own a Vec since the second repeal: the field is header
|
||||
;;;; bytes, assignment copies them, and the two copies alias one buffer.
|
||||
;;;; Which copy's free runs is the program's business — Odin's contract.
|
||||
;;;; This used to be a negative fixture; now it pins the admission.
|
||||
(defstruct Builder [buf (Vec u8)])
|
||||
|
||||
(defn main [] i32 0)
|
||||
|
||||
@ -634,11 +634,11 @@ let () =
|
||||
— memcheck still says nothing — it makes the same read *answerable*, by
|
||||
a different tool. The two must not be blurred. *)
|
||||
outputs "registry, dev" ~dev:true "programs/registry.flan"
|
||||
"1\n1\n0\n1\n0\n1\n0\n";
|
||||
"1\n1\n0\n1\n0\n0\n";
|
||||
outputs "registry, release" "programs/registry.flan"
|
||||
"0\n0\n0\n0\n0\n0\n0\n";
|
||||
"0\n0\n0\n0\n0\n0\n";
|
||||
outputs "registry, release -O0" ~opt:"-O0" "programs/registry.flan"
|
||||
"0\n0\n0\n0\n0\n0\n0\n";
|
||||
"0\n0\n0\n0\n0\n0\n";
|
||||
(* free-all on an allocator that does not offer it traps rather than doing
|
||||
nothing, because "I released the region" and "I leaked the region" must
|
||||
not be the same program text. Its own case for the same reason the
|
||||
@ -762,7 +762,7 @@ let () =
|
||||
let dbg = Emit.program ~debug:true (Check.program
|
||||
(Parse.program (Reader.read_file "programs/vec.flan"))) in
|
||||
if not (contains dbg "name: \"Allocator\"")
|
||||
|| not (contains dbg "name: \"(Vec i32)\", size: 384")
|
||||
|| not (contains dbg "name: \"(Vec i32)\", size: 320")
|
||||
then begin
|
||||
incr failures;
|
||||
print_endline "FAIL debug info for Allocator and (Vec T)"
|
||||
@ -953,39 +953,7 @@ let () =
|
||||
end;
|
||||
(try Sys.remove exe with Sys_error _ -> ());
|
||||
|
||||
(* (Handle T) and (Pool T), spec-memory.md. The thesis is one line of this
|
||||
output and the rest is scaffolding for it: the same slot prints as
|
||||
<handle 1:1> before a death and <handle 1:3> after the reuse, and the
|
||||
projectile still holding the first is told -1 rather than the
|
||||
newcomer's 99. At -O0 as well, because the null test resolve is built
|
||||
out of is exactly the kind of control flow an optimiser launders, and
|
||||
as a dev build, because a pool then lives in a frame the reload path
|
||||
has to agree with on 64 bytes. *)
|
||||
let handles_out =
|
||||
"3\n3\n60\n21\ntrue\nfalse\n2\n<handle 1:1>\n<handle 1:3>\nfalse\ntrue\n-1\n99\n3\n3\n<handle 0:0>\n-1\n10\n30\n"
|
||||
in
|
||||
outputs "handles" "programs/handles.flan" handles_out;
|
||||
outputs ~opt:"-O0" "handles, -O0" "programs/handles.flan" handles_out;
|
||||
outputs ~dev:true "handles, dev" "programs/handles.flan" handles_out;
|
||||
|
||||
(* The epoch trap on the pool's side, and it is deliberately the *other*
|
||||
failure from a stale handle. A stale handle is an answer and resolve
|
||||
returns None; a released region is not an answer at all, because the
|
||||
slot array went with the storage, so it traps. The two must not be
|
||||
conflated, which is the same rule that keeps a Vec's generation word
|
||||
and its epoch word apart. *)
|
||||
let exe = compile "programs/pool-stale-region.flan" in
|
||||
let code, text = run exe None in
|
||||
if code <> 134 || not (contains text "programs/pool-stale-region.flan:")
|
||||
|| not (contains text "allocator was released")
|
||||
|| not (contains text "7")
|
||||
then begin
|
||||
incr failures;
|
||||
Printf.printf
|
||||
"FAIL a pool used after its region was released\n\
|
||||
\ got: %S (exit %d)\n wanted: exit 134, naming the site\n"
|
||||
text code
|
||||
end;
|
||||
(try Sys.remove exe with Sys_error _ -> ());
|
||||
|
||||
(* The same trap on the Map's side, and it is not the same code path: a
|
||||
@ -2024,13 +1992,10 @@ let () =
|
||||
the Vec of a Vec is a run-time question about the allocator instead, so
|
||||
its program runs rather than being refused (programs/arena-region.flan).
|
||||
|
||||
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"
|
||||
"a struct that owns one is move-only too";
|
||||
Since the second repeal the plain field is admitted: two copies of
|
||||
the struct are two headers over one buffer, and that is the program's
|
||||
to manage — Odin's contract. The program compiles and runs. *)
|
||||
outputs "a struct field that owns a Vec" "programs/vec-in-struct.flan" "";
|
||||
(* 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
|
||||
to pass instead. *)
|
||||
@ -2821,9 +2786,6 @@ ERR@7 unexpected token: not the kind the caller was reading
|
||||
refuses_src "a data type with no cases"
|
||||
"(defdata U [])\n(defn f [u U] () 0)"
|
||||
"declares no cases";
|
||||
refuses_src "a data type case that owns a Vec"
|
||||
"(defdata U [(A [v (Vec i32)])])\n(defn f [u U] () 0)"
|
||||
"which is move-only";
|
||||
(* At the operation, not at the type: a struct key is decided by walking
|
||||
its fields and the struct table is not necessarily complete while a
|
||||
type is resolving, so both are answered where the hash and equality
|
||||
|
||||
@ -896,12 +896,12 @@ let () =
|
||||
rejects_check "slice-from-ptr with a negative literal length"
|
||||
"(defn f [p (Ptr i32)] i32 (len (slice-from-ptr p -1)))"
|
||||
~needle:"is negative";
|
||||
(* The storage stays C's. A slice is not move-only and carries no allocator,
|
||||
so free refuses one by the rule it already had — this pins that the new
|
||||
form did not become a thing anybody could hand to free. *)
|
||||
(* The storage stays C's. A slice carries no allocator, so free refuses one
|
||||
by the rule it already had — this pins that the new form did not become
|
||||
a thing anybody could hand to free. *)
|
||||
rejects_check "free of a slice made from a pointer"
|
||||
"(defn f [p (Ptr i32)] () (free (slice-from-ptr p 3)))"
|
||||
~needle:"free takes a move-only value";
|
||||
~needle:"free takes an owning container";
|
||||
|
||||
(* ── Structs, fields and auto-deref ────────────────────────────── *)
|
||||
let cursor = "(defstruct Cursor [src [u8] pos i32]) " in
|
||||
@ -1026,19 +1026,6 @@ let () =
|
||||
~needle:"exactly two types";
|
||||
rejects_check "Result is milestone 6" "(defn f [] (Result i32 i32) None)"
|
||||
~needle:"milestone 6";
|
||||
(* (Handle T) and (Pool T) are built. What stays refused is the arity, for
|
||||
the reason Vec's and Map's arities are, and the four shapes below — each
|
||||
of which is a way of losing the one property the type exists to have. *)
|
||||
rejects_check "Handle takes one type" "(defn f [x (Handle i32 i32)] ())"
|
||||
~needle:"exactly one type";
|
||||
rejects_check "Pool takes one type" "(defn f [x (Pool i32 i32)] ())"
|
||||
~needle:"exactly one type";
|
||||
(* A pool of an owning element used to be refused here, with the Vec's and
|
||||
the Map's, and the three came down together: the reason all of them gave
|
||||
was teardown, and a region has none. What replaced them is a run-time
|
||||
branch on the allocator's can-free at the construction, so the *type* is
|
||||
ordinary and only the tier is a question. See the arena rows below. *)
|
||||
accepts "a pool of a Vec" "(defn f [x (Pool (Vec i32))] ())";
|
||||
|
||||
(* ── The region rule, spec-memory.md's arena rule ────────────────────
|
||||
The compile-time half of it, which is the only half a checker row can
|
||||
@ -1053,17 +1040,14 @@ let () =
|
||||
"(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";
|
||||
(* Since the second repeal the plain case is admitted too: a struct or a
|
||||
case holding a heap-backed Vec copies as bytes, the copies alias one
|
||||
buffer, and a free through two copies is the program's bug — Odin's
|
||||
contract exactly. These pin the admission. *)
|
||||
accepts "a data type case holding a plain Vec"
|
||||
"(defdata Value [Nil (Bytes [bs (Vec u8)])])";
|
||||
accepts "a struct field holding a plain Vec"
|
||||
"(defstruct B [buf (Vec u8)])";
|
||||
(* 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"
|
||||
@ -1102,22 +1086,6 @@ let () =
|
||||
"(defvar g (Vec u8)) \
|
||||
(defn f [] () (set g (vec-new u8)) (push g 1) (set (at g 0) 2) \
|
||||
(println (len (as-slice g))) (let [c (clone g)] (free c)))";
|
||||
(* Ordering handles would order a slot index, which is a free-list artefact.
|
||||
Equality is admitted and ordering is not, which is why there are two
|
||||
predicates in Types rather than one. *)
|
||||
rejects_check "handles do not order"
|
||||
"(defn f [a (Handle i32) b (Handle i32)] bool (< a b))"
|
||||
~needle:"no built-in comparison";
|
||||
(* free takes the owner. A handle is a copyable number that owns nothing, so
|
||||
consuming one copy would say nothing about the others — which is why a
|
||||
slot is recycled by (release p h) and not by free. *)
|
||||
rejects_check "free of a handle"
|
||||
"(defn f [h (Handle i32)] () (free h))" ~needle:"a handle owns nothing";
|
||||
(* Cloning a pool would duplicate the generation counters with the slots, so
|
||||
one handle would resolve in both copies and name two different things. *)
|
||||
rejects_check "a pool cannot be cloned"
|
||||
"(defn f [p (Pool i32)] () (let [q (clone p)] (do)))"
|
||||
~needle:"cannot be cloned";
|
||||
rejects_check "try is milestone 6" "(defn f [] i32 (try 1))"
|
||||
~needle:"milestone 6";
|
||||
(* dotimes and defer are implemented, and a defer in a [let] is now one of
|
||||
@ -1651,12 +1619,11 @@ let () =
|
||||
rejects_check "a union that contains itself by value"
|
||||
"(defunion U [a i32 b U])\n(defn f [u U] i32 0)"
|
||||
~needle:"contains itself by value";
|
||||
(* Not waiting on drop, unlike the struct and data type refusals: nothing
|
||||
records which member is live, so there is no fact recursive teardown
|
||||
could read. *)
|
||||
rejects_check "a union member that is move-only"
|
||||
"(defunion U [n i64 v (Vec i32)])\n(defn f [u U] i32 0)"
|
||||
~needle:"nothing records which was written";
|
||||
(* Nothing records which member is live, and since the second repeal that
|
||||
is the program's fact to keep rather than a refusal: a union member may
|
||||
own storage, C's way. *)
|
||||
accepts "a union member that owns storage"
|
||||
"(defunion U [n i64 v (Vec i32)])\n(defn f [u U] i32 0)";
|
||||
(* And the one the optimiser would otherwise be handed: a byte that is
|
||||
neither 0 nor 1 read as an i1. Refused at any depth, which is why the
|
||||
second row goes through a struct. *)
|
||||
@ -2633,7 +2600,7 @@ let () =
|
||||
accepts "a map return type, written the one way there is"
|
||||
"(defn f [] (Map string i32) (map-new string i32))";
|
||||
accepts "a map return type followed by a constraint map"
|
||||
"(defn f [x $t] (Map string i32) {:where (copyable? $t)} \
|
||||
"(defn f [x $t] (Map string i32) {:where (equal? $t)} \
|
||||
(do x (map-new string i32)))";
|
||||
rejects_check "braces in type position say where the spelling went"
|
||||
~needle:"written (Map K V)"
|
||||
@ -2650,13 +2617,13 @@ let () =
|
||||
~needle:"nothing here says t is ordered?"
|
||||
"(defn less [a $t b $t] bool {:where (equal? $t)} (< a b))";
|
||||
(* The entailments, which are the reason a signature is one predicate long
|
||||
rather than three. Every type the language orders is a number or an enum,
|
||||
so it is equatable and it is not move-only. *)
|
||||
rather than two. Every type the language orders is a number or an enum,
|
||||
so it is equatable. *)
|
||||
accepts "ordered? entails equal?"
|
||||
"(defn same [a $t b $t] bool {:where (ordered? $t)} (= a b))";
|
||||
accepts "numeric? entails ordered?"
|
||||
"(defn less [a $t b $t] bool {:where (numeric? $t)} (< a b))";
|
||||
accepts "ordered? entails copyable?"
|
||||
accepts "a variable read twice under one predicate"
|
||||
"(defn twice [a $t] bool {:where (ordered? $t)} (< a a))";
|
||||
rejects_check "a predicate nobody has heard of"
|
||||
~needle:"is not a type predicate"
|
||||
@ -2665,12 +2632,13 @@ let () =
|
||||
~needle:"is not a type variable of f"
|
||||
"(defn f [a i32] i32 {:where (ordered? $t)} a)";
|
||||
|
||||
(* Move-only by default still decides the structural rules for a $t — what
|
||||
may own one — but since the repeal a double use of a binding is not
|
||||
checked, so both of these are accepted with and without the clause. *)
|
||||
accepts "a type variable is usable twice without copyable?"
|
||||
(* Everything copies since the second repeal, so a double use of a binding
|
||||
needs no clause at all — and [copyable?] itself is gone, refused the way
|
||||
any unknown predicate is, which is this pin's job to remember. *)
|
||||
accepts "a type variable is usable twice with no clause"
|
||||
"(defn twice [a $t b (Fn [$t $t] $t)] $t (b a a))";
|
||||
accepts "and copyable? is still a clause a signature may state"
|
||||
rejects_check "copyable? is no longer a predicate"
|
||||
~needle:"is not a type predicate"
|
||||
"(defn twice [a $t b (Fn [$t $t] $t)] $t {:where (copyable? $t)} (b a a))";
|
||||
|
||||
(* The allow-list, and it has two members. println over a type variable is
|
||||
@ -2678,16 +2646,16 @@ let () =
|
||||
after substituting — which is the one thing the abstract pass otherwise
|
||||
refuses to do. *)
|
||||
accepts "println over a type variable is deferred"
|
||||
"(defn show [x $t] () {:where (copyable? $t)} (println x))";
|
||||
"(defn show [x $t] () {:where (equal? $t)} (println x))";
|
||||
accepts "and so is print"
|
||||
"(defn show [x $t] () {:where (copyable? $t)} (print x))";
|
||||
"(defn show [x $t] () {:where (equal? $t)} (print x))";
|
||||
|
||||
(* A predicate a body relies on has to be carried by every signature between
|
||||
it and the call site, or the refusal moves into code the caller did not
|
||||
write. *)
|
||||
rejects_check "a predicate is not carried through a generic call"
|
||||
~needle:"has to be carried by every signature"
|
||||
"(defn outer [s [$t]] () {:where (copyable? $t)} (sort! s))";
|
||||
"(defn outer [s [$t]] () {:where (equal? $t)} (sort! s))";
|
||||
accepts "and is accepted when it is"
|
||||
"(defn outer [s [$t]] () {:where (ordered? $t)} (sort! s))";
|
||||
|
||||
@ -2699,7 +2667,7 @@ let () =
|
||||
itself is refused where it is written, at the definition. *)
|
||||
rejects_check "a map keyed by a type variable that is not hashable?"
|
||||
~needle:"is not a map key"
|
||||
"(defn f [m (Map $t i32)] i32 {:where (copyable? $t)} (len m))";
|
||||
"(defn f [m (Map $t i32)] i32 {:where (numeric? $t)} (len m))";
|
||||
accepts "and hashable? is what says it is"
|
||||
"(defn f [m (Map $t i32)] i32 {:where (hashable? $t)} (len m))";
|
||||
accepts "and under it the operations are deferred, not refused"
|
||||
|
||||
@ -138,7 +138,6 @@ let corpus =
|
||||
same directory; the new C here is three more path buffers, which is
|
||||
exactly what this tool is for. *)
|
||||
"programs/files.flan", [];
|
||||
"programs/handles.flan", [];
|
||||
"programs/machine.flan", [];
|
||||
"programs/math.flan", [];
|
||||
"programs/math3.flan", [];
|
||||
|
||||
@ -791,7 +791,7 @@ let () =
|
||||
installed nothing and did not say anything had gone wrong. Both copies
|
||||
have to be named, and the copy of [put!] that [hold!] pulls in has to be
|
||||
there too, which is transitivity. *)
|
||||
(match Session.eval (gen ()) "(defn hold! [xs [$t] v $t] () {:where (copyable? $t)} (put! xs 0 v) (put! xs 0 v))" with
|
||||
(match Session.eval (gen ()) "(defn hold! [xs [$t] v $t] () (put! xs 0 v) (put! xs 0 v))" with
|
||||
| c ->
|
||||
if not c.Session.installs then
|
||||
fail "redefining a generic installed nothing";
|
||||
@ -814,7 +814,7 @@ let () =
|
||||
instantiation that generated them was transitive, and finding them again
|
||||
is one table lookup rather than a walk, because a whole-program check has
|
||||
already regenerated all of them. *)
|
||||
(match Session.eval (gen ()) "(defn put! [xs [$t] i i32 v $t] () {:where (copyable? $t)} (set (at xs i) v))" with
|
||||
(match Session.eval (gen ()) "(defn put! [xs [$t] i i32 v $t] () (set (at xs i) v))" with
|
||||
| c ->
|
||||
List.iter
|
||||
(fun want ->
|
||||
@ -884,7 +884,7 @@ let () =
|
||||
caller. *)
|
||||
(match
|
||||
Session.eval (gen ())
|
||||
"(defn put! [xs [$t] i i64 v $t] () {:where (copyable? $t)} \
|
||||
"(defn put! [xs [$t] i i64 v $t] () \
|
||||
(set (at xs (i32 i)) v))"
|
||||
with
|
||||
| _ -> fail "a generic's changed parameter type was accepted"
|
||||
@ -902,7 +902,7 @@ let () =
|
||||
long before the session is asked anything. *)
|
||||
(match
|
||||
Session.eval (gen ())
|
||||
"(defn pick [xs [$t]] $t {:where [(ordered? $t) (copyable? $t)]} (at xs 0))"
|
||||
"(defn pick [xs [$t]] $t {:where (ordered? $t)} (at xs 0))"
|
||||
with
|
||||
| c ->
|
||||
if not (List.mem "pick-i32" c.Session.fns) then
|
||||
|
||||
@ -191,7 +191,7 @@ let check label path args ~checks =
|
||||
link on its own.
|
||||
|
||||
The seven programs here that abort by design — error, exhausted-unhandled,
|
||||
free-all-refused, map-stale-region, pool-stale-region, slurp-unhandled,
|
||||
free-all-refused, map-stale-region, slurp-unhandled,
|
||||
stale-region — are
|
||||
kept. A trap is a controlled abort after an fprintf, and "the trap still
|
||||
fires, in the same place, with the same message, under memcheck" is worth
|
||||
@ -217,14 +217,12 @@ let corpus =
|
||||
"programs/exhausted-unhandled.flan", [];
|
||||
"programs/files.flan", [];
|
||||
"programs/free-all-refused.flan", [];
|
||||
"programs/handles.flan", [];
|
||||
"programs/machine.flan", [];
|
||||
"programs/map-exhausted.flan", [];
|
||||
"programs/map-stale-region.flan", [];
|
||||
"programs/maps.flan", [];
|
||||
"programs/math.flan", [];
|
||||
"programs/math3.flan", [];
|
||||
"programs/pool-stale-region.flan", [];
|
||||
"programs/pkg-macro.flan", [];
|
||||
"programs/pkg-diamond.flan", [];
|
||||
"programs/pkg-return.flan", [];
|
||||
|
||||
@ -25,11 +25,10 @@
|
||||
# bytes a previous round wrote before the reset reports. test_valgrind.ml
|
||||
# asserts it as a control — it produced nothing before the runtime change
|
||||
# and six errors after. The corpus stayed clean across that change, and
|
||||
# the sharp end of that is stale-region.flan, map-stale-region.flan and
|
||||
# pool-stale-region.flan: all three read through a pointer into an arena
|
||||
# that has been reset, all three are now reading bytes memcheck knows are
|
||||
# undefined, and none of them reports — because the epoch trap fires
|
||||
# first. The runtime's own guard beats the read. Interior overruns are
|
||||
# the sharp end of that is stale-region.flan and map-stale-region.flan:
|
||||
# both read through a pointer into an arena that has been reset, both are
|
||||
# reading bytes memcheck knows are undefined, and neither reports —
|
||||
# because the epoch trap fires first. The runtime's own guard beats the read. Interior overruns are
|
||||
# still invisible, for the structural reason above.
|
||||
#
|
||||
# 2. Hand-written LLVM IR. Expected to confuse the tool. It does not, and it
|
||||
|
||||
@ -886,11 +886,10 @@ type as an argument — <code>(vec-new t)</code>, <code>(map-new t i32)</code>,
|
||||
(min (max x lo) hi))
|
||||
|
||||
(defn first-or [s [$t] d $t] $t ; the variable inside a slice type
|
||||
{:where (copyable? $t)}
|
||||
{:where (equal? $t)}
|
||||
(if (= (len s) 0) d (at s 0)))
|
||||
|
||||
(defn one-of [x $t] (Vec $t) ; bare t is the type-name argument
|
||||
{:where (copyable? $t)}
|
||||
(let [v (vec-new t)]
|
||||
(push v x)
|
||||
v))
|
||||
@ -927,8 +926,8 @@ $t)} at the head of the body, or take the operation as a parameter — a
|
||||
|
||||
<p>What makes that liveable is a <code>where</code> clause, written as a Clojure-style
|
||||
map at the head of the body — <code>{:where (ordered? $t)}</code>, or a vector when
|
||||
there is more than one: <code>{:where [(copyable? $t) (copyable? $u)]}</code>. There
|
||||
are five predicates, and each gates builtins the compiler already has:</p>
|
||||
there is more than one: <code>{:where [(ordered? $t) (hashable? $u)]}</code>. There
|
||||
are four predicates, and each gates builtins the compiler already has:</p>
|
||||
|
||||
<div class="scroll">
|
||||
<table>
|
||||
@ -937,30 +936,19 @@ are five predicates, and each gates builtins the compiler already has:</p>
|
||||
<tr><td><code>ordered?</code></td><td><code><</code> <code><=</code> <code>></code> <code>>=</code> <code>min</code> <code>max</code></td></tr>
|
||||
<tr><td><code>equal?</code></td><td><code>=</code> and <code>!=</code></td></tr>
|
||||
<tr><td><code>hashable?</code></td><td>the variable as a <code>Map</code> key — <code>(map-new t V)</code>, <code>get</code>, <code>put</code>, <code>has-key?</code></td></tr>
|
||||
<tr><td><code>copyable?</code></td><td>reading the value more than once; <code>Pool</code> and <code>Vec</code> element positions</td></tr>
|
||||
</table>
|
||||
</div>
|
||||
|
||||
<p>They entail each other in one direction, so one clause usually does:
|
||||
<code>numeric?</code> gives <code>ordered?</code>, <code>ordered?</code> gives
|
||||
<code>equal?</code>, and any of the four gives <code>copyable?</code>. A
|
||||
<code>sort!</code> that compares its elements and reads them twice declares
|
||||
<code>numeric?</code> gives <code>ordered?</code>, and <code>ordered?</code> gives
|
||||
<code>equal?</code>. A <code>sort!</code> that compares its elements declares
|
||||
<code>ordered?</code> and nothing else.</p>
|
||||
|
||||
<p><strong>A type variable is move-only by default</strong>, and
|
||||
<code>copyable?</code> is the opt-out. <code>Types.is_move_only</code> of a variable is
|
||||
not decidable abstractly — the same variable is <code>i32</code> at one instantiation
|
||||
and <code>(Vec i32)</code> at the next — so the checker assumes the stricter rule,
|
||||
which can only refuse a program that would have been fine and never admit one that
|
||||
double-frees. It is Rust's <code>T: Copy</code>, with the difference that the compiler
|
||||
answers the question rather than a user implementing a trait. So
|
||||
<code>(defn twice [x $t] $t (+ x x))</code> does not merely want
|
||||
<code>numeric?</code>; reading <code>x</code> a second time is a use after move:</p>
|
||||
|
||||
<pre><code class="sh">x was moved at twice.flan:1:26 and cannot be used again — t is move-only, so
|
||||
binding, passing or returning one transfers ownership and the source binding is
|
||||
dead afterwards (spec-memory.md). That rule is what makes a double free
|
||||
unrepresentable; (clone x) if you wanted a second one</code></pre>
|
||||
<p><strong>Every value copies.</strong> There used to be a fifth predicate,
|
||||
<code>copyable?</code>, gating a second read of a move-only variable; the move
|
||||
concept was repealed on 2026-09-18 — a container copies as its header, the
|
||||
copies alias one buffer, and which free runs is the program's business, as it
|
||||
is in Odin — so the predicate went with it.</p>
|
||||
|
||||
<p>Each instantiation then checks the concrete type against what the signature declared,
|
||||
and refuses the <em>call site</em> when it does not answer:</p>
|
||||
|
||||
Loading…
x
Reference in New Issue
Block a user