(Vec T) over a type-erased runtime, with StorageExhausted going in beside it
Two element types, one runtime, and the element type appears nowhere below the call site: size_of and align_of are produced where the concrete type is known, which without generics is simply the concrete call site. That is Odin's arrangement and it is what spec-memory.md specifies. `at` and `len` were already the names for a fixed array and a slice, so a Vec extends them rather than adding a parallel pair — the asymmetry `nth` was removed for — and the value form and the place form go through one helper so they cannot drift apart. StorageExhausted lands with step 2 rather than after it, because the signatures depend on it: `push` and `reserve` are Unit, `clone` is the container, and nothing grows a Result. It is built out of nodes that already existed — a while, a restart-case and an error — so the backend learned nothing about allocation. The restart is established at the failing allocation, which spec-memory.md names as the exception to "restarts go at the resync point, once", and the element a push was given is bound to a slot before the loop so a retry re-attempts the allocation and not the expression. Move-only is a dead set on the checker context, and it is flow-sensitive at an `if`: both arms start from the same set and the union survives the join, so `(if c (free v) (free v))` is legal and a one-armed free still kills the binding. The case a dead set cannot answer is a move inside a loop — merged once at the end of the body it counts one move, not two — so that is a rule, refused with its reason. Four decisions the spec did not settle: The Vec header is six words in every build, not four in release. A layout that changes with a build flag can disagree across the reload boundary silently: a redefinition module is built by llc and ld against a host built separately, and nothing makes the two agree on a struct size. The 32-byte release layout is deferred on that. A zeroed Vec has a null allocator, and the first operation needing storage adopts the context allocator. Odin's behaviour. The alternative was refusing a Vec-typed struct field until drop lands; shipping the null was a null deref on the first push. A Vec's length and index are i32, like every other length here. Widening indices is one change across all the containers, not a Vec question. `let` has no type annotation, so a local Vec has nowhere to say what it holds and the element type is written at the call: `(vec-new i32)`. This is not the explicit instantiation syntax the generics section rules out — nothing here is generic and the name resolves as an ordinary type. Where the context says, it may be left out. The allocator grew a budget: a ceiling on live bytes, 0 for none. The retry restart is only answerable by a handler that can make the *same* request succeed, and for a fixed backing store the handler that works is the one that raises the ceiling — releasing the region a container lives in invalidates the container, which is what the epoch check catches. The spec's "grows the arena and then invokes retry" needed something to grow. The generation word is bumped on every reallocation and read by nothing. The stale-slice trap it is for needs a slice that can carry the Vec's identity, and a slice is ptr+len. Said plainly rather than implied by the word's presence.
This commit is contained in:
parent
74c6489020
commit
af8d291154
461
lib/check.ml
461
lib/check.ml
@ -109,6 +109,20 @@ type ctx = {
|
||||
function's defers are already half run and the first transfer's target is
|
||||
already in hand. Refused where it is written. *)
|
||||
mutable in_defer : bool;
|
||||
(* Move tracking, spec-memory.md's "(Vec T) and (Map K V) are move-only".
|
||||
[dead] is the slots whose value has been moved out, with where it went, so
|
||||
that a second use names the first rather than reporting a type error about
|
||||
nothing. It is flow-sensitive at an [if]: the two arms are checked from
|
||||
the same starting set and the *union* survives the join, so moving in one
|
||||
arm only is still a move afterwards — and moving in both arms, which is
|
||||
legal, is not two errors.
|
||||
|
||||
[borrow] is set only while checking the *target* of an operation that
|
||||
reads a container without consuming it ([at], [len], [as-slice], [push],
|
||||
[reserve], [clone]). Without it every one of those would look like a move
|
||||
and no program could push twice. *)
|
||||
mutable dead : (int * Loc.t) list;
|
||||
mutable borrow : bool;
|
||||
(* The function being checked, so a clause lifted out of it can be named
|
||||
after it. The name has to be stable and has to say whose it is: a
|
||||
redefinition module emits the clauses belonging to the bodies it is
|
||||
@ -212,7 +226,8 @@ let rec resolve env ?(seen = []) (t : Ast.texpr) : Types.t =
|
||||
| "Ptr", [ a ] -> Types.Ptr (resolve env ~seen a)
|
||||
| "Option", [ a ] -> Types.Option (resolve env ~seen a)
|
||||
| ("Ptr" | "Option"), _ -> fail loc "(%s T) takes exactly one type" name
|
||||
| "Vec", _ -> unimplemented loc "(Vec T)" 6
|
||||
| "Vec", [ a ] -> Types.Vec (resolve env ~seen a)
|
||||
| "Vec", _ -> fail loc "(Vec T) takes exactly one type"
|
||||
| "Map", _ -> unimplemented loc "(Map K V)" 6
|
||||
| "Result", _ -> unimplemented loc "(Result T E)" 6
|
||||
| "Handle", _ -> unimplemented loc "(Handle T)" 6
|
||||
@ -332,6 +347,21 @@ let unit_at loc = mk loc Types.Unit Tast.Unit
|
||||
crosses as ptr+len like any other. *)
|
||||
let here loc = mk loc Types.String (Tast.Str (Loc.to_string loc))
|
||||
|
||||
(* A runtime call, with the result type spelled at the site. *)
|
||||
let rt loc ty sym args = mk loc ty (Tast.Prim (Tast.Rt sym, args))
|
||||
|
||||
let i64_at loc n = mk loc (Types.Int Types.I64) (Tast.Int (n, Types.I64))
|
||||
|
||||
(* spec-memory.md, "Alignment": the number is produced where the concrete
|
||||
element type is known, which without generics is simply the call site. *)
|
||||
let size_of loc t = mk loc (Types.Int Types.I64) (Tast.Prim (Tast.SizeOf t, []))
|
||||
let align_of loc t = mk loc (Types.Int Types.I64) (Tast.Prim (Tast.AlignOf t, []))
|
||||
|
||||
(* The address of an expression, place or not: the type-erased runtime takes
|
||||
the element [push] copies by pointer. *)
|
||||
let addr_of loc (e : Tast.expr) =
|
||||
mk loc (Types.Ptr e.Tast.ty) (Tast.Prim (Tast.AddrOf, [ e ]))
|
||||
|
||||
(* Every integer index into an array or slice is i32 at milestone 2. *)
|
||||
let index_ty = Types.Int Types.I32
|
||||
|
||||
@ -405,7 +435,9 @@ let rec check ctx ?want (e : Ast.expr) : Tast.expr =
|
||||
| Ast.If (c, t, e') -> check_if ctx ?want loc c t e'
|
||||
| Ast.While (c, body) ->
|
||||
let c = check ctx ~want:Types.Bool c in
|
||||
let body = scoped ctx (fun () -> map_lr (fun b -> check ctx b) body) in
|
||||
let body = in_loop ctx (fun () ->
|
||||
scoped ctx (fun () -> map_lr (fun b -> check ctx b) body))
|
||||
in
|
||||
expect loc ~want (mk loc Types.Unit (Tast.While (c, body)))
|
||||
| Ast.Return v when ctx.in_frames <> None ->
|
||||
ignore v;
|
||||
@ -585,7 +617,9 @@ and var ctx loc ~want name =
|
||||
(mk loc Types.Alloc (Tast.Prim (Tast.Rt "flan_context_temp", [])))
|
||||
| _ ->
|
||||
match lookup ctx name with
|
||||
| Some b -> expect loc ~want (mk loc b.bty (Tast.Local b.slot))
|
||||
| Some b ->
|
||||
if Types.is_move_only b.bty then moved ctx loc name b.slot;
|
||||
expect loc ~want (mk loc b.bty (Tast.Local b.slot))
|
||||
| None ->
|
||||
match Hashtbl.find_opt ctx.env.globals name with
|
||||
| Some (ty, _) -> expect loc ~want (mk loc ty (Tast.Global name))
|
||||
@ -595,6 +629,42 @@ and var ctx loc ~want name =
|
||||
(Printf.sprintf "the function value %s (a name used as a value)" name) 5
|
||||
else begin captured ctx loc name; fail loc "unknown name %s" name end
|
||||
|
||||
(* Reading a move-only local. Every read is a move unless the site said it was
|
||||
a borrow, which is the conservative direction: passing one to a function,
|
||||
binding it, returning it and [free]ing it are all moves and all reach here,
|
||||
and the handful of operations that only look at a container say so. *)
|
||||
and moved ctx loc name slot =
|
||||
(match List.assoc_opt slot ctx.dead with
|
||||
| Some where ->
|
||||
fail loc
|
||||
"%s was moved at %s and cannot be used again — a Vec 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 %s) if you wanted a second one"
|
||||
name (Loc.to_string where) name
|
||||
| None -> ());
|
||||
if not ctx.borrow then ctx.dead <- (slot, loc) :: ctx.dead
|
||||
|
||||
(* The target of an operation that reads a container without consuming it. Only
|
||||
a syntactically simple target is treated as a borrow: in [(len (f v))] the
|
||||
call still moves [v], and setting the flag over the whole subexpression
|
||||
would have hidden that. *)
|
||||
and borrowed ctx (a : Ast.expr) f =
|
||||
let simple =
|
||||
match a.Ast.e with
|
||||
| Ast.Var _ | Ast.Field _ -> true
|
||||
| Ast.Call ({ Ast.e = Ast.Var "at"; _ }, _) -> true
|
||||
| _ -> false
|
||||
in
|
||||
if not simple then f ()
|
||||
else begin
|
||||
let saved = ctx.borrow in
|
||||
ctx.borrow <- true;
|
||||
let r = f () in
|
||||
ctx.borrow <- saved;
|
||||
r
|
||||
end
|
||||
|
||||
and block ctx ?want loc body =
|
||||
match body with
|
||||
| [] -> expect loc ~want (unit_at loc)
|
||||
@ -638,7 +708,7 @@ and check_handler_bind ctx ?want loc clauses body =
|
||||
the enclosing one. *)
|
||||
let hctx =
|
||||
{ env = ctx.env; ret = Types.Unit; slots = 0; slot_tys = []; slot_names = [];
|
||||
scope = []; defers = []; outer = ctx.scope; in_handler = true; in_frames = None; in_defer = false; owner = "<none>" }
|
||||
scope = []; defers = []; outer = ctx.scope; in_handler = true; in_frames = None; in_defer = false; dead = []; borrow = false; owner = "<none>" }
|
||||
in
|
||||
(* The condition crosses as a pointer, because the handler runs while
|
||||
the signalling frame is still alive and there is nothing to copy.
|
||||
@ -761,12 +831,31 @@ and check_let ctx ?want loc bs body =
|
||||
and the bound to a hidden slot — [n] is evaluated once, before the loop, so
|
||||
a body that changes it cannot change the trip count — then step [i] at the
|
||||
end of the body. [i] is not assignable, so the step below is the only writer. *)
|
||||
(* A loop body that moves a binding declared outside the loop is refused, and
|
||||
this is the one place the dead set cannot answer on its own: the second
|
||||
iteration would use what the first moved, and a set that is merged once at
|
||||
the end of the body sees one move, not two. So it is a rule rather than an
|
||||
inference, stated as one. *)
|
||||
and in_loop ctx f =
|
||||
let outer_slots = List.map (fun (_, b) -> b.slot) ctx.scope in
|
||||
let before = ctx.dead in
|
||||
let r = f () in
|
||||
List.iter
|
||||
(fun (slot, where) ->
|
||||
if (not (List.mem_assoc slot before)) && List.mem slot outer_slots then
|
||||
fail where
|
||||
"this moves a value that was bound outside the loop, so the next \
|
||||
iteration would use what this one gave away. Move it out of the \
|
||||
loop, or bind a fresh value inside it")
|
||||
ctx.dead;
|
||||
r
|
||||
|
||||
and check_dotimes ctx ~want loc name count body =
|
||||
let count = check ctx ~want:index_ty count in
|
||||
scoped ctx (fun () ->
|
||||
let i = bind ctx name index_ty ~assignable:false in
|
||||
let limit = fresh_slot ctx index_ty in
|
||||
let body = map_lr (fun b -> check ctx b) body in
|
||||
let body = in_loop ctx (fun () -> map_lr (fun b -> check ctx b) body) in
|
||||
let iv = mk loc index_ty (Tast.Local i) in
|
||||
let one = mk loc index_ty (Tast.Int (1L, Types.I32)) in
|
||||
let cond =
|
||||
@ -792,7 +881,15 @@ and check_if ctx ?want loc c t e =
|
||||
let t = scoped ctx (fun () -> check ctx t) in
|
||||
expect loc ~want (mk loc Types.Unit (Tast.If (c, t, unit_at loc)))
|
||||
| Some e ->
|
||||
(* Both arms start from the same dead set and the union survives: moving in
|
||||
one arm only still kills the binding afterwards, and moving in both —
|
||||
which is legal and common — is not reported twice. A flat set would have
|
||||
refused [(if c (free v) (free v))] and allowed the use after a one-armed
|
||||
move, which are the two ways to be wrong here. *)
|
||||
let before = ctx.dead in
|
||||
let t = scoped ctx (fun () -> check ctx ?want t) in
|
||||
let after_then = ctx.dead in
|
||||
ctx.dead <- before;
|
||||
(* With no expectation the then-branch supplies one for the else-branch,
|
||||
unless it diverges, in which case the else-branch decides. *)
|
||||
let ewant =
|
||||
@ -801,6 +898,9 @@ and check_if ctx ?want loc c t e =
|
||||
| None -> if t.Tast.ty = Types.Never then None else Some t.Tast.ty
|
||||
in
|
||||
let e = scoped ctx (fun () -> check ctx ?want:ewant e) in
|
||||
ctx.dead <-
|
||||
after_then
|
||||
@ List.filter (fun (k, _) -> not (List.mem_assoc k after_then)) ctx.dead;
|
||||
let ty =
|
||||
if t.Tast.ty = Types.Never then e.Tast.ty
|
||||
else if e.Tast.ty = Types.Never then t.Tast.ty
|
||||
@ -960,9 +1060,18 @@ and check_place ctx loc (p : Ast.place) : Tast.place * Types.t =
|
||||
| None -> fail loc "%s has no field %s" sname name
|
||||
| Some i -> Tast.Pfield (target, i), (List.nth s.Tast.fields i).Tast.fty)
|
||||
| Ast.Pindex (target, idx) ->
|
||||
let target = check ctx target in
|
||||
let idx, ty = indexed ctx target idx in
|
||||
Tast.Pindex (target, idx), ty
|
||||
let target = borrowed ctx target (fun () -> check ctx target) in
|
||||
(match target.Tast.ty with
|
||||
(* The same bounds and epoch check the value form gets, through the same
|
||||
helper: an element of a Vec is a place because a Vec element is
|
||||
assignable, and a set that skipped the checks would be the asymmetry
|
||||
[nth] was removed for. *)
|
||||
| Types.Vec _ ->
|
||||
let p, ty = vec_at ctx loc target idx in
|
||||
Tast.Pderef p, ty
|
||||
| _ ->
|
||||
let idx, ty = indexed ctx target idx in
|
||||
Tast.Pindex (target, idx), ty)
|
||||
| Ast.Pderef target ->
|
||||
let target = check ctx target in
|
||||
(match target.Tast.ty with
|
||||
@ -1097,6 +1206,138 @@ and fold_left_prim ctx ~want loc name p ok what args =
|
||||
in
|
||||
expect loc ~want acc
|
||||
|
||||
(* ── Allocation failure, spec-memory.md ────────────────────────────────
|
||||
No allocating operation returns an error and none can fail silently. When
|
||||
the allocator cannot satisfy a request the operation signals
|
||||
|
||||
(StorageExhausted {:bytes n :align a :allocator id})
|
||||
|
||||
with [error] — whose type is Never — inside a [restart-case] offering
|
||||
[retry]. That is one rule over every allocating operation, which is what
|
||||
keeps [push] and [reserve] at Unit, [clone] at the container, and no
|
||||
signature anywhere growing a Result. Odin's [append] returns an ignorable
|
||||
Allocator_Error and its type-erased path returns the old length on a failed
|
||||
reserve; an append that appends nothing and says nothing is the outcome this
|
||||
rule exists to make impossible.
|
||||
|
||||
It is *compiler-emitted at the point of failure*, which spec-memory.md names
|
||||
as the exception to plan.org's "restarts go at the resync point, once": a
|
||||
restart established at a parser's top-level loop cannot re-attempt an
|
||||
allocation, and only the allocation site can.
|
||||
|
||||
The shape is built out of nodes that already exist — a while, a restart-case
|
||||
and an error — so the backend learns nothing new about allocation:
|
||||
|
||||
(let [ok false]
|
||||
(while (not ok)
|
||||
(restart-case
|
||||
(do (set ok ATTEMPT)
|
||||
(if (not ok) (error (StorageExhausted {...}))))
|
||||
(retry []))))
|
||||
|
||||
A handler that frees something, releases a scratch region or grows the arena
|
||||
and then invokes [retry] lands in the clause, the clause falls through, and
|
||||
the while re-tests and re-attempts the *same* request. With nothing handling
|
||||
it, [error] stops the program on the frame that erred, as §2 says.
|
||||
|
||||
[attempt] must be a call that can be repeated: every argument to it is bound
|
||||
to a slot before the loop, so a retry does not re-evaluate the element
|
||||
expression a push was given. *)
|
||||
and alloc_guard ctx loc (attempt : Tast.expr) =
|
||||
let ok = fresh_slot ctx Types.Bool in
|
||||
let okv = mk loc Types.Bool (Tast.Local ok) in
|
||||
let notok () = mk loc Types.Bool (Tast.Prim (Tast.Not, [ okv ])) in
|
||||
let i8 n = mk loc (Types.Int Types.I8) (Tast.Int (n, Types.I8)) in
|
||||
(* The runtime answers 1 or 0 and never reports failure any other way. *)
|
||||
let attempt = mk loc Types.Bool (Tast.Prim (Tast.Ne, [ attempt; i8 0L ])) in
|
||||
(* A value struct on the signalling frame's stack, with fixed numeric fields
|
||||
and no rendered message: formatting would allocate, and this is the one
|
||||
path that must not. Rendering happens in the handler or the break loop,
|
||||
where a working allocator is known. *)
|
||||
let cond =
|
||||
mk loc (Types.Named "StorageExhausted")
|
||||
(Tast.Make
|
||||
("StorageExhausted",
|
||||
[ rt loc (Types.Int Types.I64) "flan_alloc_fail_bytes" [];
|
||||
rt loc (Types.Int Types.I64) "flan_alloc_fail_align" [];
|
||||
rt loc (Types.Int Types.I64) "flan_alloc_fail_id" [] ]))
|
||||
in
|
||||
let signal =
|
||||
mk loc Types.Never
|
||||
(Tast.Signal (Tast.Serror, type_id "StorageExhausted", cond))
|
||||
in
|
||||
let attempt_then_signal =
|
||||
mk loc Types.Unit
|
||||
(Tast.Do
|
||||
[ mk loc Types.Unit (Tast.Set (Tast.Plocal ok, attempt));
|
||||
mk loc Types.Unit (Tast.If (notok (), signal, unit_at loc)) ])
|
||||
in
|
||||
let clause =
|
||||
{ Tast.rname_id = type_id "retry"; rname = "retry"; rbody = [ unit_at loc ] }
|
||||
in
|
||||
let body =
|
||||
mk loc Types.Unit (Tast.RestartCase ([ clause ], attempt_then_signal))
|
||||
in
|
||||
mk loc Types.Unit
|
||||
(Tast.Let ([ (ok, mk loc Types.Bool (Tast.Bool false)) ],
|
||||
[ mk loc Types.Unit (Tast.While (notok (), [ body ])) ]))
|
||||
|
||||
(* The element type for [vec-new]: a leading bare symbol naming a type, or the
|
||||
expectation at the site. A bare symbol shadowed by a local or a global is
|
||||
that binding — an allocator, in practice — and not a type. *)
|
||||
and vec_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))
|
||||
&& (List.mem n Types.primitive_names
|
||||
|| Hashtbl.mem ctx.env.structs n
|
||||
|| Hashtbl.mem ctx.env.enums n
|
||||
|| Hashtbl.mem ctx.env.aliases n) ->
|
||||
Some (resolve_name ctx.env ~seen:[] loc n, rest)
|
||||
| _ -> None
|
||||
in
|
||||
match named with
|
||||
| Some (t, rest) -> t, rest
|
||||
| None ->
|
||||
(match want with
|
||||
| Some (Types.Vec t) -> t, args
|
||||
| _ ->
|
||||
fail loc
|
||||
"nothing here says what (vec-new) is a Vec of — write the element \
|
||||
type, as (vec-new i32), or give the binding a type")
|
||||
|
||||
(* The element type, or the reason this is not a Vec. *)
|
||||
and vec_elem loc what (t : Types.t) =
|
||||
match t with
|
||||
| Types.Vec e -> e
|
||||
| other -> fail loc "%s takes a (Vec T), found %s" what (Types.to_string other)
|
||||
|
||||
(* The allocator an operation uses: the one named at the site, or the current
|
||||
implicit one. spec-memory.md: an operation never falls back to a hidden
|
||||
global allocator, and an explicit allocator can override the context. *)
|
||||
and allocator_arg ctx loc = function
|
||||
| [] -> rt loc Types.Alloc "flan_context_allocator" []
|
||||
| [ a ] -> check ctx ~want:Types.Alloc a
|
||||
| _ -> fail loc "at most one allocator may be named here"
|
||||
|
||||
(* The address of an element, bounds-checked, with the allocator's epoch
|
||||
checked first. Both the value form [(at v i)] and the place form
|
||||
[(set (at v i) x)] come through here, so they cannot drift apart — which is
|
||||
the asymmetry [nth] was removed for. *)
|
||||
and vec_at ctx loc (target : Tast.expr) (idx : Ast.expr list) =
|
||||
let elem = vec_elem loc "at" target.Tast.ty in
|
||||
match idx with
|
||||
| [ i ] ->
|
||||
let i = index_expr ctx i in
|
||||
rt loc (Types.Ptr elem) "flan_vec_at"
|
||||
[ target; i; size_of loc elem; here loc ], elem
|
||||
| _ ->
|
||||
fail loc
|
||||
"a Vec takes exactly one index — (at v i) — and its element is indexed \
|
||||
separately"
|
||||
|
||||
and named_call ctx ~want loc name args =
|
||||
let prim p ty args = expect loc ~want (mk loc ty (Tast.Prim (p, args))) in
|
||||
match name with
|
||||
@ -1335,6 +1576,36 @@ and named_call ctx ~want loc name args =
|
||||
expect loc ~want
|
||||
(mk loc (Types.Int Types.I64)
|
||||
(Tast.Prim (Tast.Rt "flan_alloc_epoch", [ a ])))
|
||||
(* The allocator's identity — its address — which is what the condition's
|
||||
:allocator field carries, so a handler holding several regions can tell
|
||||
which one ran out. *)
|
||||
| "alloc-id" ->
|
||||
arity loc name 1 args;
|
||||
let a = check ctx ~want:Types.Alloc (List.hd args) in
|
||||
expect loc ~want
|
||||
(mk loc (Types.Int Types.I64) (Tast.Prim (Tast.Rt "flan_alloc_id", [ a ])))
|
||||
(* A ceiling on live bytes, 0 for none. spec-memory.md's retry restart is
|
||||
answerable only by a handler that can make the *same* request succeed, and
|
||||
for a fixed backing store the handler that works is the one that grows it:
|
||||
releasing the region a container lives in invalidates the container, which
|
||||
is what the epoch check catches. So the spec's "grows the arena and then
|
||||
invokes retry" needs a ceiling to raise, and this is it. It is also how a
|
||||
program exhausts an allocator on purpose. *)
|
||||
| "alloc-budget" ->
|
||||
arity loc name 1 args;
|
||||
let a = check ctx ~want:Types.Alloc (List.hd args) in
|
||||
expect loc ~want
|
||||
(mk loc (Types.Int Types.I64)
|
||||
(Tast.Prim (Tast.Rt "flan_alloc_budget", [ a ])))
|
||||
| "set-alloc-budget" ->
|
||||
arity loc name 2 args;
|
||||
(match args with
|
||||
| [ a; n ] ->
|
||||
let a = check ctx ~want:Types.Alloc a in
|
||||
let n = check ctx ~want:(Types.Int Types.I64) n in
|
||||
expect loc ~want
|
||||
(mk loc Types.Unit (Tast.Prim (Tast.Rt "flan_alloc_set_budget", [ a; n ])))
|
||||
| _ -> assert false)
|
||||
(* "Did you forget to free" is an allocator-tier question and this is the
|
||||
tier answering it — spec-memory.md, "Leaking is defined behaviour". *)
|
||||
| "alloc-live-blocks" ->
|
||||
@ -1369,21 +1640,171 @@ and named_call ctx ~want loc name args =
|
||||
in
|
||||
expect loc ~want (mk loc ty (Tast.WithAlloc (a, body))))
|
||||
|
||||
(* ── (Vec T), spec-memory.md ───────────────────────────────────── *)
|
||||
(* Every one of these is a named call over a type-erased runtime, with
|
||||
size_of and align_of produced here because here is where the concrete
|
||||
element type is known. No generics are involved and none are needed. *)
|
||||
(* (vec-new), (vec-new T), (vec-new a), (vec-new T a).
|
||||
[let] has no type annotation — parse.ml settles that a triple binding is
|
||||
ambiguous and types are inferred — so a local Vec has nowhere to say what
|
||||
it holds, and the element type is written at the call instead. This is not
|
||||
the explicit instantiation syntax the generics section rules out: nothing
|
||||
here is generic, and the name is resolved as an ordinary type, not bound
|
||||
to a type variable. Where the context does say — a defvar's type, a
|
||||
function's return type, an argument — it is not needed and may be left
|
||||
out. *)
|
||||
| "vec-new" ->
|
||||
let elem, args = vec_new_elem ctx ~want loc args in
|
||||
let a = allocator_arg ctx loc args in
|
||||
let v = fresh_slot ctx (Types.Vec elem) in
|
||||
let attempt =
|
||||
rt loc (Types.Int Types.I8) "flan_vec_init"
|
||||
[ mk loc (Types.Vec elem) (Tast.Local v); a; i64_at loc 0L;
|
||||
size_of loc elem; align_of loc elem ]
|
||||
in
|
||||
expect loc ~want
|
||||
(mk loc (Types.Vec elem)
|
||||
(Tast.Let ([ (v, mk loc (Types.Vec elem) (Tast.Zero (Types.Vec elem))) ],
|
||||
[ alloc_guard ctx loc attempt;
|
||||
mk loc (Types.Vec elem) (Tast.Local v) ])))
|
||||
(* Unit, not a Result and not an ignorable error code: see [alloc_guard]. *)
|
||||
| "push" ->
|
||||
arity loc name 2 args;
|
||||
(match args with
|
||||
| [ target; x ] ->
|
||||
let target = borrowed ctx target (fun () -> check ctx target) in
|
||||
let elem = vec_elem loc "push" target.Tast.ty in
|
||||
let x = check ctx ~want:elem x in
|
||||
(* The element is bound before the loop so that a [retry] re-attempts
|
||||
the allocation and not the expression that produced the value. *)
|
||||
let e = fresh_slot ctx elem in
|
||||
let attempt =
|
||||
rt loc (Types.Int Types.I8) "flan_vec_push"
|
||||
[ target; addr_of loc (mk loc elem (Tast.Local e));
|
||||
size_of loc elem; align_of loc elem; here loc ]
|
||||
in
|
||||
expect loc ~want
|
||||
(mk loc Types.Unit
|
||||
(Tast.Let ([ (e, x) ], [ alloc_guard ctx loc attempt ])))
|
||||
| _ -> assert false)
|
||||
| "reserve" ->
|
||||
arity loc name 2 args;
|
||||
(match args with
|
||||
| [ target; n ] ->
|
||||
let target = borrowed ctx target (fun () -> check ctx target) in
|
||||
let elem = vec_elem loc "reserve" target.Tast.ty in
|
||||
let n = check ctx ~want:index_ty n in
|
||||
let n64 =
|
||||
mk loc (Types.Int Types.I64) (Tast.Prim (Tast.Cast (Types.Int Types.I64), [ n ]))
|
||||
in
|
||||
let attempt =
|
||||
rt loc (Types.Int Types.I8) "flan_vec_reserve"
|
||||
[ target; n64; size_of loc elem; align_of loc elem; here loc ]
|
||||
in
|
||||
expect loc ~want (alloc_guard ctx loc attempt)
|
||||
| _ -> assert false)
|
||||
(* (as-slice v) and (as-slice v lo hi) — spec-memory.md, "Borrowing". The
|
||||
result is a non-owning view: copying it copies ptr+len and never the
|
||||
elements, and it carries no allocator, so freeing through one is not
|
||||
expressible. A push, a put or a reserve may invalidate it; that is the
|
||||
explicit Zig/Odin contract the spec chose over a borrow checker. *)
|
||||
| "as-slice" ->
|
||||
(match args with
|
||||
| target :: rest when List.length rest = 0 || List.length rest = 2 ->
|
||||
let target = borrowed ctx target (fun () -> check ctx target) in
|
||||
let elem = vec_elem loc "as-slice" target.Tast.ty in
|
||||
let lo, hi =
|
||||
match rest with
|
||||
| [] ->
|
||||
mk loc index_ty (Tast.Int (0L, Types.I32)),
|
||||
(* -1 is "to the end": (as-slice v) has no static length to pass. *)
|
||||
mk loc index_ty (Tast.Int (-1L, Types.I32))
|
||||
| [ lo; hi ] -> index_expr ctx lo, index_expr ctx hi
|
||||
| _ -> assert false
|
||||
in
|
||||
let out = fresh_slot ctx (Types.Slice elem) in
|
||||
let fill =
|
||||
rt loc Types.Unit "flan_vec_as_slice"
|
||||
[ target; addr_of loc (mk loc (Types.Slice elem) (Tast.Local out));
|
||||
lo; hi; size_of loc elem; here loc ]
|
||||
in
|
||||
expect loc ~want
|
||||
(mk loc (Types.Slice elem)
|
||||
(Tast.Let ([ (out, mk loc (Types.Slice elem)
|
||||
(Tast.Zero (Types.Slice elem))) ],
|
||||
[ fill; mk loc (Types.Slice elem) (Tast.Local out) ])))
|
||||
| _ -> fail loc "as-slice is (as-slice v) or (as-slice v lo hi)")
|
||||
(* spec-memory.md's first release point. It consumes its argument exactly as
|
||||
any other move does — the source binding is dead afterwards and using it
|
||||
is a compile error — which is the rule that already makes a double free
|
||||
unrepresentable, so [free] needs no analysis of its own. *)
|
||||
| "free" ->
|
||||
arity loc name 1 args;
|
||||
let target = check ctx (List.hd args) in
|
||||
(match target.Tast.ty with
|
||||
| Types.Vec elem ->
|
||||
expect loc ~want
|
||||
(rt loc Types.Unit "flan_vec_free"
|
||||
[ target; size_of loc elem; align_of loc elem; here loc ])
|
||||
| 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, or a struct that owns one — \
|
||||
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". *)
|
||||
| "clone" ->
|
||||
(match args with
|
||||
| target :: rest when List.length rest <= 1 ->
|
||||
let target = borrowed ctx target (fun () -> check ctx target) in
|
||||
let elem = vec_elem loc "clone" target.Tast.ty in
|
||||
let a = allocator_arg ctx loc rest in
|
||||
let d = fresh_slot ctx (Types.Vec elem) in
|
||||
let attempt =
|
||||
rt loc (Types.Int Types.I8) "flan_vec_clone"
|
||||
[ mk loc (Types.Vec elem) (Tast.Local d); target; a;
|
||||
size_of loc elem; align_of loc elem; here loc ]
|
||||
in
|
||||
expect loc ~want
|
||||
(mk loc (Types.Vec elem)
|
||||
(Tast.Let ([ (d, mk loc (Types.Vec elem) (Tast.Zero (Types.Vec elem))) ],
|
||||
[ alloc_guard ctx loc attempt;
|
||||
mk loc (Types.Vec elem) (Tast.Local d) ])))
|
||||
| _ -> fail loc "clone is (clone v) or (clone v allocator)")
|
||||
|
||||
(* ── containers ────────────────────────────────────────────────── *)
|
||||
(* [at] and [len] were already the names for a fixed array and a slice, so a
|
||||
Vec extends them rather than adding a parallel pair — which is the
|
||||
asymmetry [nth] was removed for. A Vec's length is i32 like every other
|
||||
length here (index_ty): widening indices is one change across all of them
|
||||
and not a Vec question. *)
|
||||
| "len" ->
|
||||
arity loc name 1 args;
|
||||
let a = check ctx (List.hd args) in
|
||||
let target = List.hd args in
|
||||
let a = borrowed ctx target (fun () -> check ctx target) in
|
||||
(match a.Tast.ty with
|
||||
| Types.Array _ | Types.Slice _ | Types.String -> ()
|
||||
| other -> fail loc "len takes an array, a slice or a string, found %s"
|
||||
(Types.to_string other));
|
||||
prim Tast.Len index_ty [ a ]
|
||||
| Types.Array _ | Types.Slice _ | Types.String ->
|
||||
prim Tast.Len index_ty [ a ]
|
||||
| Types.Vec _ ->
|
||||
let n = rt loc (Types.Int Types.I64) "flan_vec_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 or a Vec, found %s"
|
||||
(Types.to_string other))
|
||||
| "at" ->
|
||||
(match args with
|
||||
| target :: idx when idx <> [] ->
|
||||
let target = check ctx target in
|
||||
let idx, ty = indexed ctx target idx in
|
||||
prim Tast.At ty (target :: idx)
|
||||
let target = borrowed ctx target (fun () -> check ctx target) in
|
||||
(match target.Tast.ty with
|
||||
| Types.Vec _ ->
|
||||
let p, elem = vec_at ctx loc target idx in
|
||||
expect loc ~want (mk loc elem (Tast.Deref p))
|
||||
| _ ->
|
||||
let idx, ty = indexed ctx target idx in
|
||||
prim Tast.At ty (target :: idx))
|
||||
| _ -> fail loc "%s is (%s collection index ...)" name name)
|
||||
| "slice" ->
|
||||
arity loc name 3 args;
|
||||
@ -1858,7 +2279,7 @@ let collect env (decls : Ast.decl list) =
|
||||
run without swallowing it. *)
|
||||
let infer (_, v) =
|
||||
(check { env; ret = Types.Unit; slots = 0; slot_tys = []; slot_names = []; scope = []; defers = [];
|
||||
outer = []; in_handler = false; in_frames = None; in_defer = false; owner = "<none>" } v).Tast.ty
|
||||
outer = []; in_handler = false; in_frames = None; in_defer = false; dead = []; borrow = false; owner = "<none>" } v).Tast.ty
|
||||
in
|
||||
let pending = ref (List.rev !untyped) in
|
||||
let rec settle () =
|
||||
@ -1911,7 +2332,7 @@ let check_finite env =
|
||||
let check_fn env (fn : Ast.fn) : Tast.fn =
|
||||
let params, ret = Hashtbl.find env.fns fn.Ast.name in
|
||||
let ctx = { env; ret; slots = 0; slot_tys = []; slot_names = []; scope = []; defers = [];
|
||||
outer = []; in_handler = false; in_frames = None; in_defer = false;
|
||||
outer = []; in_handler = false; in_frames = None; in_defer = false; dead = []; borrow = false;
|
||||
owner = fn.Ast.name } in
|
||||
List.iter2
|
||||
(fun (p : Ast.field) ty ->
|
||||
@ -1987,7 +2408,7 @@ let check_fn env (fn : Ast.fn) : Tast.fn =
|
||||
|
||||
let check_global env (d : Ast.decl) : Tast.global option =
|
||||
let ctx () = { env; ret = Types.Unit; slots = 0; slot_tys = []; slot_names = []; scope = []; defers = [];
|
||||
outer = []; in_handler = false; in_frames = None; in_defer = false; owner = "<none>" } in
|
||||
outer = []; in_handler = false; in_frames = None; in_defer = false; dead = []; borrow = false; owner = "<none>" } in
|
||||
match d.Ast.d with
|
||||
| Ast.Defvar (n, _, init) ->
|
||||
let ty, _ = Hashtbl.find env.globals n in
|
||||
@ -2097,7 +2518,7 @@ let expression env (e : Ast.expr) :
|
||||
Tast.expr * Types.t array * string option array =
|
||||
let ctx =
|
||||
{ env; ret = Types.Unit; slots = 0; slot_tys = []; slot_names = []; scope = []; defers = [];
|
||||
outer = []; in_handler = false; in_frames = None; in_defer = false; owner = "<none>" }
|
||||
outer = []; in_handler = false; in_frames = None; in_defer = false; dead = []; borrow = false; owner = "<none>" }
|
||||
in
|
||||
let t = check ctx e in
|
||||
(t, Array.of_list (List.rev ctx.slot_tys),
|
||||
|
||||
39
lib/emit.ml
39
lib/emit.ml
@ -96,6 +96,12 @@ let rec ll (t : Types.t) =
|
||||
(* An [Allocator] is a pointer to the runtime's [flan_allocator] and never a
|
||||
copy of one: see Types. Opaque here in the same sense [ptr] is. *)
|
||||
| Types.Alloc -> "ptr"
|
||||
(* ptr + len + cap + allocator, and two more words the runtime owns: see
|
||||
flan_rt.c's (Vec T) header for why they are in every build. Nothing in
|
||||
this file reads a field of one — every operation is a runtime call taking
|
||||
the Vec's address — so the shape is here only so that a slot, a struct
|
||||
field and a copy in the IR are the right number of bytes. *)
|
||||
| Types.Vec _ -> "%vec"
|
||||
| Types.Option e -> Printf.sprintf "{ i8, %s }" (ll e)
|
||||
| Types.Map _ | Types.Fn _ | Types.Var _ ->
|
||||
(* The checker rejects each of these by name — nothing reaches here. *)
|
||||
@ -233,6 +239,7 @@ let rec lay m (t : Types.t) : int * int =
|
||||
| Types.Enum _ -> 4, 4
|
||||
| Types.Ptr _ -> 8, 8
|
||||
| Types.Alloc -> 8, 8
|
||||
| Types.Vec _ -> 48, 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
|
||||
@ -354,6 +361,14 @@ 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. *)
|
||||
| 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) ]
|
||||
| Types.Map _ | Types.Fn _ | Types.Var _ ->
|
||||
failwith ("no debug type for " ^ Types.to_string t)
|
||||
in
|
||||
@ -1310,6 +1325,10 @@ and prim f (e : Tast.expr) (p : Tast.prim) (args : Tast.expr list) =
|
||||
let p, n = explode f a in
|
||||
[ "ptr " ^ p; "i64 " ^ n ]
|
||||
| Types.Unit | Types.Never -> []
|
||||
(* A Vec is move-only and never copied, so it crosses to the
|
||||
runtime as its address — which is also what lets an operation
|
||||
mutate the caller's Vec in place. *)
|
||||
| Types.Vec _ -> [ "ptr " ^ addr f a ]
|
||||
| t -> [ ll t ^ " " ^ value f a ])
|
||||
args)
|
||||
in
|
||||
@ -1322,6 +1341,9 @@ and prim f (e : Tast.expr) (p : Tast.prim) (args : Tast.expr list) =
|
||||
ins f "%s = call %s @%s(%s)" t (ll e.Tast.ty) sym args';
|
||||
t
|
||||
end
|
||||
| Tast.SizeOf t, [] -> Printf.sprintf "%d" (fst (lay f.md t))
|
||||
| Tast.AlignOf t, [] -> Printf.sprintf "%d" (snd (lay f.md t))
|
||||
| Tast.AddrOf, [ x ] -> addr f x
|
||||
| Tast.Cast target, [ x ] -> cast f x target
|
||||
| _ -> failwith "malformed primitive"
|
||||
|
||||
@ -1613,6 +1635,9 @@ let header = {|; Generated by flan. The layout is C's: no object headers anywher
|
||||
; so a Flan struct is exactly its C struct and nothing marshals.
|
||||
|
||||
%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 }
|
||||
; 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 }
|
||||
@ -1655,6 +1680,20 @@ declare i8 @flan_alloc_can_free(ptr)
|
||||
declare i8 @flan_alloc_can_free_all(ptr)
|
||||
declare i64 @flan_alloc_epoch(ptr)
|
||||
declare i64 @flan_alloc_live_blocks(ptr)
|
||||
declare i64 @flan_alloc_id(ptr)
|
||||
declare i64 @flan_alloc_fail_bytes()
|
||||
declare i64 @flan_alloc_fail_align()
|
||||
declare i64 @flan_alloc_fail_id()
|
||||
declare i64 @flan_alloc_budget(ptr)
|
||||
declare void @flan_alloc_set_budget(ptr, i64)
|
||||
declare i8 @flan_vec_init(ptr, ptr, i64, i64, i64)
|
||||
declare i8 @flan_vec_reserve(ptr, i64, i64, i64, ptr, i64)
|
||||
declare i8 @flan_vec_push(ptr, ptr, i64, i64, ptr, i64)
|
||||
declare i8 @flan_vec_clone(ptr, ptr, ptr, i64, i64, ptr, i64)
|
||||
declare i64 @flan_vec_len(ptr, ptr, i64)
|
||||
declare ptr @flan_vec_at(ptr, i32, i64, ptr, i64)
|
||||
declare void @flan_vec_as_slice(ptr, ptr, i32, i32, i64, ptr, i64)
|
||||
declare void @flan_vec_free(ptr, i64, i64, ptr, i64)
|
||||
|}
|
||||
|
||||
(* C's main, adapting to whichever of the four shapes Flan's main has: argv and
|
||||
|
||||
@ -31,6 +31,19 @@
|
||||
it actually holds. *)
|
||||
|
||||
let source = {flan|
|
||||
;; The condition every allocating operation signals when the allocator cannot
|
||||
;; satisfy a request — spec-memory.md, "Allocation failure". It is here rather
|
||||
;; than built by the checker because it is an ordinary value struct and the
|
||||
;; checker already knows how to build one of those; nothing about it is
|
||||
;; special except who signals it.
|
||||
;;
|
||||
;; Fixed numeric fields and no rendered message, because formatting would
|
||||
;; allocate and this is the one path that must not. :allocator is the
|
||||
;; allocator's address, which is its identity — the same thing the epoch hangs
|
||||
;; off — so a handler can tell which region ran out. Rendering happens in the
|
||||
;; handler or the break loop, where a working allocator is known.
|
||||
(defstruct StorageExhausted [bytes i64 align i64 allocator i64])
|
||||
|
||||
;; A seeded PRNG in Flan rather than libc's, because a grid hash is only a
|
||||
;; regression test if the sequence is byte-identical on native and wasm32
|
||||
;; (plan.org, RNG is ours). PCG-XSH-RR 32: one u64 LCG step per draw, folded
|
||||
|
||||
@ -114,6 +114,10 @@ let rec render c depth (e : Tast.expr) : Tast.expr list =
|
||||
runtime's, its address is not stable across runs, and printing either
|
||||
would make an acceptance test's output depend on the heap. *)
|
||||
| Types.Alloc -> [ lit "<allocator>" ]
|
||||
(* Printing a Vec structurally would be a walk over storage this function
|
||||
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>" ]
|
||||
| Types.Option t ->
|
||||
let tag = { Tast.e = Tast.Field (e, 0); ty = Types.Int Types.I8; loc } in
|
||||
let some = { Tast.e = Tast.Field (e, 1); ty = t; loc } in
|
||||
|
||||
12
lib/tast.ml
12
lib/tast.ml
@ -45,6 +45,18 @@ type prim =
|
||||
same rule as every other shim here. No transfer guard follows one: a
|
||||
transfer cannot cross a C frame. *)
|
||||
| Rt of string
|
||||
(* spec-memory.md, "Alignment": a property of the type, computed at the call
|
||||
site, passed as a parameter to the type-erased allocator — all three, and
|
||||
they are not alternatives. The checker builds these at the site where the
|
||||
concrete element type is known and the backend fills in the number from
|
||||
the same layout calculator DWARF uses. *)
|
||||
| SizeOf of Types.t
|
||||
| AlignOf of Types.t
|
||||
(* The address of any expression, not only of a place: the element a [push]
|
||||
copies may be a computed value, and the runtime takes it by pointer
|
||||
because it is type-erased. The backend already spills a non-place to a
|
||||
temporary for exactly this. *)
|
||||
| AddrOf
|
||||
| Cast of Types.t
|
||||
|
||||
type expr = { e : expr_kind; ty : Types.t; loc : Loc.t }
|
||||
|
||||
18
lib/types.ml
18
lib/types.ml
@ -39,6 +39,11 @@ type t =
|
||||
the capability set and the epoch have to be shared by every container
|
||||
made from it, and a copy would give each its own. *)
|
||||
| Alloc
|
||||
(* [(Vec T)]: ptr + len + cap + allocator, owning and move-only. One
|
||||
type-erased runtime over (size, align) stands behind every instantiation,
|
||||
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
|
||||
| Option of t (* (Option T) *)
|
||||
| Fn of t list * t (* (Fn [T ...] R) *)
|
||||
| Var of string (* a type variable — milestone 5 *)
|
||||
@ -85,6 +90,7 @@ let rec equal a b =
|
||||
| Map (k, v), Map (k', v') -> equal k k' && equal v v'
|
||||
| Ptr x, Ptr y -> equal x y
|
||||
| Alloc, Alloc -> true
|
||||
| Vec x, Vec y -> equal x y
|
||||
| Option x, Option y -> equal x y
|
||||
| Fn (ps, r), Fn (ps', r') ->
|
||||
List.length ps = List.length ps'
|
||||
@ -106,6 +112,7 @@ let rec to_string = function
|
||||
| Map (k, v) -> Printf.sprintf "{%s %s}" (to_string k) (to_string v)
|
||||
| Ptr t -> "(Ptr " ^ to_string t ^ ")"
|
||||
| Alloc -> "Allocator"
|
||||
| Vec t -> "(Vec " ^ to_string t ^ ")"
|
||||
| Option t -> "(Option " ^ to_string t ^ ")"
|
||||
| Fn (ps, r) ->
|
||||
Printf.sprintf "(Fn [%s] %s)"
|
||||
@ -114,6 +121,17 @@ 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
|
||||
| Vec _ -> true
|
||||
| Option t -> is_move_only t
|
||||
| Array (_, t) -> is_move_only t
|
||||
| _ -> false
|
||||
|
||||
(* Ordering and equality are defined on machine types and on nothing else at
|
||||
milestone 2 — strings, structs and slices have no built-in [=], because an
|
||||
unconstrained type supports only what every type supports (plan.org, Types). *)
|
||||
|
||||
@ -477,8 +477,22 @@ struct flan_allocator {
|
||||
* an allocator-tier question and this is the allocator's answer. */
|
||||
int64_t live_blocks;
|
||||
int64_t live_bytes;
|
||||
/* A cap on live bytes, or 0 for none. It is here because
|
||||
* spec-memory.md's retry restart is only answerable by a handler that can
|
||||
* make the *same* request succeed, and for a fixed backing buffer the only
|
||||
* such handler is one that raises the ceiling: releasing the region a
|
||||
* container lives in invalidates the container, which is what the epoch
|
||||
* check exists to catch. So "grow the arena and then invoke retry", which
|
||||
* the spec names as the handler that works, needs a ceiling to raise. It
|
||||
* doubles as the knob a test exhausts an allocator with on purpose. */
|
||||
int64_t budget;
|
||||
};
|
||||
|
||||
/* Would this request put the allocator over its budget? */
|
||||
static int flan_over_budget(flan_allocator *a, int64_t size) {
|
||||
return a->budget > 0 && a->live_bytes + size > a->budget;
|
||||
}
|
||||
|
||||
/* -- The heap allocator: malloc, realloc, free. ---------------------- */
|
||||
|
||||
static void *flan_heap_proc(flan_allocator *a, int32_t mode, void *p,
|
||||
@ -488,6 +502,7 @@ static void *flan_heap_proc(flan_allocator *a, int32_t mode, void *p,
|
||||
void *q = NULL;
|
||||
size_t al, sz;
|
||||
if (size <= 0) return NULL;
|
||||
if (flan_over_budget(a, size)) return NULL;
|
||||
al = (size_t)(align < (int64_t)sizeof(void *) ? (int64_t)sizeof(void *) : align);
|
||||
sz = (size_t)size;
|
||||
/* aligned_alloc requires a size that is a multiple of the alignment. */
|
||||
@ -500,7 +515,9 @@ static void *flan_heap_proc(flan_allocator *a, int32_t mode, void *p,
|
||||
/* aligned_alloc has no realloc, so growth is a new block and a copy. The
|
||||
* caller passes old_size for exactly this reason, and it is the one
|
||||
* number a wrong answer here would read off the end of. */
|
||||
void *q = flan_heap_proc(a, FLAN_ALLOC_ALLOC, NULL, 0, size, align);
|
||||
void *q;
|
||||
if (flan_over_budget(a, size - old_size)) return NULL;
|
||||
q = flan_heap_proc(a, FLAN_ALLOC_ALLOC, NULL, 0, size, align);
|
||||
if (!q) return NULL;
|
||||
if (p && old_size > 0)
|
||||
memcpy(q, p, (size_t)(old_size < size ? old_size : size));
|
||||
@ -519,7 +536,7 @@ static void *flan_heap_proc(flan_allocator *a, int32_t mode, void *p,
|
||||
static flan_allocator flan_heap = {
|
||||
flan_heap_proc, NULL,
|
||||
FLAN_CAN_ALLOC | FLAN_CAN_RESIZE | FLAN_CAN_FREE,
|
||||
0, 0, 0
|
||||
0, 0, 0, 0
|
||||
};
|
||||
|
||||
/* -- The arena: one fixed backing buffer and a bump offset. ----------
|
||||
@ -552,6 +569,7 @@ static void *flan_arena_proc(flan_allocator *a, int32_t mode, void *p,
|
||||
case FLAN_ALLOC_ALLOC: {
|
||||
int64_t start, end;
|
||||
if (size <= 0) return NULL;
|
||||
if (flan_over_budget(a, size)) return NULL;
|
||||
if (align < 1) align = 1;
|
||||
start = flan_align_up(ar->offset, align);
|
||||
end = start + size;
|
||||
@ -680,6 +698,12 @@ int64_t flan_alloc_live_blocks(flan_allocator *a) {
|
||||
return a ? a->live_blocks : 0;
|
||||
}
|
||||
|
||||
int64_t flan_alloc_budget(flan_allocator *a) { return a ? a->budget : 0; }
|
||||
|
||||
void flan_alloc_set_budget(flan_allocator *a, int64_t n) {
|
||||
if (a) a->budget = n < 0 ? 0 : n;
|
||||
}
|
||||
|
||||
_Noreturn void flan_free_all_fail(const uint8_t *loc, int64_t loclen);
|
||||
_Noreturn void flan_null_alloc_fail(const uint8_t *loc, int64_t loclen);
|
||||
|
||||
@ -714,3 +738,216 @@ _Noreturn void flan_free_all_fail(const uint8_t *loc, int64_t loclen) {
|
||||
(int)loclen, (const char *)loc);
|
||||
rt_die();
|
||||
}
|
||||
|
||||
/* ── (Vec T), spec-memory.md ────────────────────────────────────────────
|
||||
*
|
||||
* One type-erased runtime over (size, align), which is Odin's arrangement
|
||||
* (base/runtime/dynamic_array_internal.odin): the monomorphised wrapper is the
|
||||
* only place the concrete type is known, so it is the only place that can
|
||||
* 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:
|
||||
*
|
||||
* ptr len cap allocator the release layout spec-memory.md fixes
|
||||
* gen bumped on every reallocation — the stale-slice
|
||||
* word. It has no reader yet; see 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
|
||||
* 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 BUILT.md
|
||||
* says what it is blocked on.
|
||||
*
|
||||
* 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
|
||||
* compiler's job (see Check's alloc_guard). */
|
||||
|
||||
typedef struct flan_vec {
|
||||
void *ptr;
|
||||
int64_t len;
|
||||
int64_t cap;
|
||||
flan_allocator *alloc;
|
||||
int64_t gen;
|
||||
int64_t epoch;
|
||||
} flan_vec;
|
||||
|
||||
/* The request that did not fit, for the condition the compiler builds at the
|
||||
* failing site. A pair of globals rather than out-parameters because the
|
||||
* condition is a value struct on the signalling frame's stack with fixed
|
||||
* numeric fields and no rendered message — spec-memory.md is explicit that
|
||||
* this is the one path that must not allocate, and reading two words is the
|
||||
* cheapest way to carry the numbers out. */
|
||||
static int64_t flan_fail_bytes = 0;
|
||||
static int64_t flan_fail_align = 0;
|
||||
static int64_t flan_fail_id = 0;
|
||||
|
||||
int64_t flan_alloc_fail_bytes(void) { return flan_fail_bytes; }
|
||||
int64_t flan_alloc_fail_align(void) { return flan_fail_align; }
|
||||
int64_t flan_alloc_fail_id(void) { return flan_fail_id; }
|
||||
|
||||
/* The allocator's identity, for the condition's :allocator field. The pointer
|
||||
* is the identity — the same thing the epoch hangs off. */
|
||||
int64_t flan_alloc_id(flan_allocator *a) { return (int64_t)(intptr_t)a; }
|
||||
|
||||
_Noreturn void flan_vec_stale_fail(const uint8_t *loc, int64_t loclen,
|
||||
int64_t was, int64_t now) {
|
||||
fflush(stdout);
|
||||
fprintf(stderr,
|
||||
"%.*s: this container's allocator was released — it was made at "
|
||||
"epoch %lld and the allocator is at %lld now\n",
|
||||
(int)loclen, (const char *)loc, (long long)was, (long long)now);
|
||||
rt_die();
|
||||
}
|
||||
|
||||
_Noreturn void flan_vec_bounds_fail(const uint8_t *loc, int64_t loclen,
|
||||
int64_t i, int64_t len) {
|
||||
fflush(stdout);
|
||||
fprintf(stderr, "%.*s: index %lld is out of bounds for length %lld\n",
|
||||
(int)loclen, (const char *)loc, (long long)i, (long long)len);
|
||||
rt_die();
|
||||
}
|
||||
|
||||
/* spec-memory.md, "Dev builds detect a released region". This is the check
|
||||
* that makes the epoch word worth carrying, and it runs on every operation,
|
||||
* not only in a dev build — see the header on why the words are unconditional.
|
||||
* A Vec that never allocated has no allocator and nothing to check. */
|
||||
static void flan_vec_check(flan_vec *v, const uint8_t *loc, int64_t loclen) {
|
||||
if (v->alloc) {
|
||||
int64_t now = (int64_t)v->alloc->epoch;
|
||||
if (now != v->epoch) flan_vec_stale_fail(loc, loclen, v->epoch, now);
|
||||
}
|
||||
}
|
||||
|
||||
/* A zeroed Vec — a struct field nobody assigned, or a (defvar xs (Vec i32)) —
|
||||
* has a null allocator, and the first operation that needs storage adopts the
|
||||
* context allocator. That is Odin's behaviour, and the alternative was to
|
||||
* refuse a Vec-typed struct field outright until step 5. Shipping the null
|
||||
* silently was not an option: it is a null deref on the first push. */
|
||||
static flan_allocator *flan_vec_adopt(flan_vec *v) {
|
||||
if (!v->alloc) {
|
||||
v->alloc = flan_context_allocator();
|
||||
v->epoch = (int64_t)v->alloc->epoch;
|
||||
}
|
||||
return v->alloc;
|
||||
}
|
||||
|
||||
static int8_t flan_vec_grow(flan_vec *v, int64_t want, int64_t size,
|
||||
int64_t align) {
|
||||
flan_allocator *a = flan_vec_adopt(v);
|
||||
int64_t cap = v->cap;
|
||||
void *p;
|
||||
if (want <= cap) return 1;
|
||||
/* Doubling, from four. Four rather than one because the three reallocations
|
||||
* a growing-from-one Vec does before it holds anything are pure cost, and
|
||||
* doubling because it is what makes n pushes amortised O(n). */
|
||||
if (cap < 4) cap = 4;
|
||||
while (cap < want) {
|
||||
if (cap > (int64_t)1 << 40) { cap = want; break; }
|
||||
cap *= 2;
|
||||
}
|
||||
flan_fail_bytes = cap * size;
|
||||
flan_fail_align = align;
|
||||
flan_fail_id = (int64_t)(intptr_t)a;
|
||||
if (v->ptr)
|
||||
p = a->proc(a, FLAN_ALLOC_RESIZE, v->ptr, v->cap * size, cap * size, align);
|
||||
else
|
||||
p = a->proc(a, FLAN_ALLOC_ALLOC, NULL, 0, cap * size, align);
|
||||
if (!p) return 0;
|
||||
v->ptr = p;
|
||||
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 BUILT.md. */
|
||||
v->gen++;
|
||||
return 1;
|
||||
}
|
||||
|
||||
int8_t flan_vec_init(flan_vec *v, flan_allocator *a, int64_t cap, int64_t size,
|
||||
int64_t align) {
|
||||
v->ptr = NULL;
|
||||
v->len = 0;
|
||||
v->cap = 0;
|
||||
v->gen = 0;
|
||||
v->alloc = a ? a : flan_context_allocator();
|
||||
v->epoch = (int64_t)v->alloc->epoch;
|
||||
if (cap <= 0) return 1;
|
||||
return flan_vec_grow(v, cap, size, align);
|
||||
}
|
||||
|
||||
int8_t flan_vec_reserve(flan_vec *v, int64_t n, int64_t size, int64_t align,
|
||||
const uint8_t *loc, int64_t loclen) {
|
||||
flan_vec_check(v, loc, loclen);
|
||||
if (n <= v->cap) return 1;
|
||||
return flan_vec_grow(v, n, size, align);
|
||||
}
|
||||
|
||||
int8_t flan_vec_push(flan_vec *v, const void *elem, int64_t size,
|
||||
int64_t align, const uint8_t *loc, int64_t loclen) {
|
||||
flan_vec_check(v, loc, loclen);
|
||||
if (v->len + 1 > v->cap && !flan_vec_grow(v, v->len + 1, size, align))
|
||||
return 0;
|
||||
memcpy((uint8_t *)v->ptr + v->len * size, elem, (size_t)size);
|
||||
v->len++;
|
||||
return 1;
|
||||
}
|
||||
|
||||
int64_t flan_vec_len(flan_vec *v, const uint8_t *loc, int64_t loclen) {
|
||||
flan_vec_check(v, loc, loclen);
|
||||
return v->len;
|
||||
}
|
||||
|
||||
void *flan_vec_at(flan_vec *v, int32_t i, int64_t size, const uint8_t *loc,
|
||||
int64_t loclen) {
|
||||
flan_vec_check(v, loc, loclen);
|
||||
/* The same unsigned comparison the fixed-array bounds check uses: a negative
|
||||
* index sign-extends to a huge unsigned and is caught by the one test. */
|
||||
if ((uint64_t)(int64_t)i >= (uint64_t)v->len)
|
||||
flan_vec_bounds_fail(loc, loclen, (int64_t)i, v->len);
|
||||
return (uint8_t *)v->ptr + (int64_t)i * size;
|
||||
}
|
||||
|
||||
/* [hi] of -1 means "to the end": (as-slice v) has no static length to write. */
|
||||
void flan_vec_as_slice(flan_vec *v, void *out, int32_t lo, int32_t hi,
|
||||
int64_t size, const uint8_t *loc, int64_t loclen) {
|
||||
struct { void *p; int64_t n; } s;
|
||||
int64_t l = lo, h = (hi < 0) ? v->len : hi;
|
||||
flan_vec_check(v, loc, loclen);
|
||||
if (l < 0 || h > v->len || l > h) flan_vec_bounds_fail(loc, loclen, l, v->len);
|
||||
s.p = (uint8_t *)v->ptr + l * size;
|
||||
s.n = h - l;
|
||||
memcpy(out, &s, sizeof s);
|
||||
}
|
||||
|
||||
/* spec-memory.md's first release point. The Vec is left zeroed rather than
|
||||
* dangling — the checker has already made using it afterwards a compile error,
|
||||
* and zeroing costs nothing and makes a bug that slips past the checker a null
|
||||
* deref rather than a use-after-free. An allocator without can-free keeps the
|
||||
* block: releasing it is free-all's job, and pretending otherwise here is the
|
||||
* silent-no-op this file refuses elsewhere. */
|
||||
void flan_vec_free(flan_vec *v, int64_t size, int64_t align,
|
||||
const uint8_t *loc, int64_t loclen) {
|
||||
flan_vec_check(v, loc, loclen);
|
||||
if (v->ptr && v->alloc && (v->alloc->caps & FLAN_CAN_FREE))
|
||||
v->alloc->proc(v->alloc, FLAN_ALLOC_FREE, v->ptr, v->cap * size, 0, align);
|
||||
(void)align;
|
||||
v->ptr = NULL;
|
||||
v->len = 0;
|
||||
v->cap = 0;
|
||||
v->alloc = NULL;
|
||||
v->gen++;
|
||||
v->epoch = 0;
|
||||
}
|
||||
|
||||
int8_t flan_vec_clone(flan_vec *dst, flan_vec *src, flan_allocator *a,
|
||||
int64_t size, int64_t align, const uint8_t *loc,
|
||||
int64_t loclen) {
|
||||
flan_vec_check(src, loc, loclen);
|
||||
if (!flan_vec_init(dst, a, src->len, size, align)) return 0;
|
||||
if (src->len > 0) memcpy(dst->ptr, src->ptr, (size_t)(src->len * size));
|
||||
dst->len = src->len;
|
||||
return 1;
|
||||
}
|
||||
|
||||
12
test/programs/exhausted-unhandled.flan
Normal file
12
test/programs/exhausted-unhandled.flan
Normal file
@ -0,0 +1,12 @@
|
||||
;;;; An exhausted allocator with nothing handling it. §2: `error` is the
|
||||
;;;; diverging variant — a handler that returns normally has not answered it,
|
||||
;;;; and with no handler at all the program stops on the frame that erred
|
||||
;;;; rather than carrying on with a push that appended nothing.
|
||||
(defn main [] i32
|
||||
(let [a (arena-new 32)]
|
||||
(let [v (vec-new i32 a)]
|
||||
(println "before")
|
||||
(dotimes [i 64] (push v i))
|
||||
(println "unreachable")
|
||||
(free v)))
|
||||
0)
|
||||
92
test/programs/exhausted.flan
Normal file
92
test/programs/exhausted.flan
Normal file
@ -0,0 +1,92 @@
|
||||
;;;; StorageExhausted and retry — spec-memory.md, "Allocation failure".
|
||||
;;;;
|
||||
;;;; No allocating operation returns an error and none can fail silently. The
|
||||
;;;; operation signals StorageExhausted with `error`, whose type is Never,
|
||||
;;;; inside a restart-case offering `retry` — so push stays Unit, clone stays
|
||||
;;;; the container, and no signature anywhere grows a Result. Odin's append
|
||||
;;;; returns an ignorable Allocator_Error; an append that appends nothing and
|
||||
;;;; says nothing is the outcome this rule exists to make impossible.
|
||||
;;;;
|
||||
;;;; This is also the named exception to plan.org's "restarts go at the resync
|
||||
;;;; point, once": the restart is established *at the failing allocation*,
|
||||
;;;; because a restart at an outer loop cannot re-attempt an allocation and
|
||||
;;;; only the allocation site can.
|
||||
;;;;
|
||||
;;;; The handler that works is the one that raises the ceiling and retries.
|
||||
;;;; Releasing the region the container lives in does not work and must not be
|
||||
;;;; written: it invalidates the container, which the epoch check then catches
|
||||
;;;; — and that case is its own program, stale-region.flan.
|
||||
|
||||
;; Globals, because a handler cannot see the locals of the function that
|
||||
;; established it: check.ml's `captured` refuses one by name and says to use a
|
||||
;; global. That refusal is the accumulation pattern, and it is not built.
|
||||
(defvar tight Allocator)
|
||||
(defvar failures i64)
|
||||
(defvar last-bytes i64)
|
||||
(defvar last-align i64)
|
||||
(defvar same-allocator bool)
|
||||
|
||||
(defn main [] i32
|
||||
;; The general-purpose tier, with a ceiling on it. 32 bytes is four i32 and
|
||||
;; the doubling past it is not.
|
||||
(set tight (heap-allocator))
|
||||
(set-alloc-budget tight 32)
|
||||
|
||||
(handler-bind
|
||||
[(StorageExhausted [c]
|
||||
(set failures (+ failures 1))
|
||||
;; The condition is a value struct with fixed numeric fields and no
|
||||
;; rendered message: formatting would allocate, and this is the one path
|
||||
;; that must not. Rendering happens here, where a working allocator is
|
||||
;; known.
|
||||
(set last-bytes (.bytes c))
|
||||
(set last-align (.align c))
|
||||
;; It names which region ran out, so a handler holding several can tell
|
||||
;; them apart.
|
||||
(set same-allocator (= (.allocator c) (alloc-id tight)))
|
||||
;; Grow it, then re-attempt the same request. The Vec is untouched and
|
||||
;; its allocator is unchanged, which is why this retry can succeed.
|
||||
(set-alloc-budget tight (* 4 (alloc-budget tight)))
|
||||
(invoke-restart 'retry))]
|
||||
(let [v (vec-new i32 tight)]
|
||||
;; Somewhere in here the ceiling is hit, the handler raises it, and the
|
||||
;; push that failed is re-attempted. No push is lost: a failed push
|
||||
;; appends nothing and the retry appends exactly once.
|
||||
(dotimes [i 64] (push v (* i 2)))
|
||||
(println (len v)) ; 64
|
||||
(println (at v 0)) ; 0
|
||||
(println (at v 63)) ; 126
|
||||
(free v)))
|
||||
|
||||
;; The handler ran, more than once, and what it saw were the numbers of the
|
||||
;; request that did not fit.
|
||||
(println (> failures 1)) ; true
|
||||
(println (> last-bytes 0)) ; true
|
||||
(println last-align) ; 4 — align-of i32, from the call site
|
||||
(println same-allocator) ; true
|
||||
|
||||
;; Every allocating operation, not only push. reserve asks for the whole
|
||||
;; block at once, and clone asks the new allocator for the source's length.
|
||||
(set-alloc-budget tight 32)
|
||||
(set failures 0)
|
||||
(handler-bind
|
||||
[(StorageExhausted [c]
|
||||
(set failures (+ failures 1))
|
||||
(set-alloc-budget tight 4096)
|
||||
(invoke-restart 'retry))]
|
||||
(let [v (vec-new i32 tight)]
|
||||
(reserve v 256)
|
||||
(println (len v)) ; 0
|
||||
(dotimes [i 8] (push v i))
|
||||
(set-alloc-budget tight 4128)
|
||||
(let [w (clone v)]
|
||||
(println (len w)) ; 8
|
||||
(println (at w 7)) ; 7
|
||||
(free w))
|
||||
(free v)))
|
||||
(println (> failures 0)) ; true
|
||||
|
||||
;; And the restart is not once-per-program: it is established at each
|
||||
;; allocation, so a later one offers it again.
|
||||
(set-alloc-budget tight 0)
|
||||
0)
|
||||
22
test/programs/stale-region.flan
Normal file
22
test/programs/stale-region.flan
Normal file
@ -0,0 +1,22 @@
|
||||
;;;; spec-memory.md, "Dev builds detect a released region".
|
||||
;;;;
|
||||
;;;; A Vec records the epoch of the allocator it was made with, and free-all
|
||||
;;;; bumps that counter. Any operation on a container whose recorded epoch has
|
||||
;;;; moved traps, naming the site. This is the shipping answer to the section
|
||||
;;;; the spec leaves open — detection, loud and immediate, rather than the
|
||||
;;;; static prevention that with-allocator and context/allocator deny.
|
||||
;;;;
|
||||
;;;; It is a separate counter from the per-Vec generation word, which answers a
|
||||
;;;; different question (a stale slice), and the two must not be conflated.
|
||||
(defn main [] i32
|
||||
(let [a (arena-new 4096)]
|
||||
(let [v (vec-new i32 a)]
|
||||
(push v 1)
|
||||
(push v 2)
|
||||
(println (at v 1))
|
||||
;; The region goes. v is still in scope and still looks fine — nothing
|
||||
;; is released at scope exit and nothing marked v — which is exactly the
|
||||
;; case a static rule cannot see.
|
||||
(free-all a)
|
||||
(println (at v 1))))
|
||||
0)
|
||||
8
test/programs/vec-double-free.flan
Normal file
8
test/programs/vec-double-free.flan
Normal file
@ -0,0 +1,8 @@
|
||||
;;;; `free` consumes its argument exactly as any other move does, so the second
|
||||
;;;; one is a compile error rather than a runtime crash. Nothing analyses this
|
||||
;;;; specially: it is the same dead-binding rule as passing one to a function.
|
||||
(defn main [] i32
|
||||
(let [v (vec-new i32)]
|
||||
(free v)
|
||||
(free v)
|
||||
0))
|
||||
8
test/programs/vec-moved-in-loop.flan
Normal file
8
test/programs/vec-moved-in-loop.flan
Normal file
@ -0,0 +1,8 @@
|
||||
;;;; A loop body that moves a binding declared outside the loop: the second
|
||||
;;;; iteration would use what the first gave away. The dead set alone cannot
|
||||
;;;; see this — merged once at the end of the body it counts one move, not two
|
||||
;;;; — so it is a rule, and it is refused with the reason.
|
||||
(defn main [] i32
|
||||
(let [v (vec-new i32)]
|
||||
(dotimes [i 3] (free v))
|
||||
0))
|
||||
15
test/programs/vec-moved.flan
Normal file
15
test/programs/vec-moved.flan
Normal file
@ -0,0 +1,15 @@
|
||||
;;;; A Vec is move-only: passing one to a function transfers ownership, and the
|
||||
;;;; source binding is dead afterwards. That rule is what makes a double free
|
||||
;;;; unrepresentable, which is why `free` needs no analysis of its own.
|
||||
(defn take [v (Vec i32)] i32
|
||||
(let [n (len v)]
|
||||
(free v)
|
||||
n))
|
||||
|
||||
(defn main [] i32
|
||||
(let [v (vec-new i32)]
|
||||
(push v 1)
|
||||
(println (take v))
|
||||
;; v went with the call. Being refused here is the whole test.
|
||||
(println (len v))
|
||||
0))
|
||||
8
test/programs/vec-untyped.flan
Normal file
8
test/programs/vec-untyped.flan
Normal file
@ -0,0 +1,8 @@
|
||||
;;;; `let` has no type annotation — parse.ml settles that a triple binding is
|
||||
;;;; ambiguous and that types are inferred — so a local Vec has nowhere to say
|
||||
;;;; what it holds, and the element type is written at the call instead. With
|
||||
;;;; neither, this is refused rather than guessed at.
|
||||
(defn main [] i32
|
||||
(let [v (vec-new)]
|
||||
(free v)
|
||||
0))
|
||||
102
test/programs/vec.flan
Normal file
102
test/programs/vec.flan
Normal file
@ -0,0 +1,102 @@
|
||||
;;;; (Vec T) — spec-memory.md, "The four container types" and "Allocators".
|
||||
;;;;
|
||||
;;;; ptr + len + cap + allocator, owning and move-only, over one type-erased
|
||||
;;;; runtime. The element type appears nowhere in that runtime: size_of and
|
||||
;;;; align_of are produced at the call site, which without generics is simply
|
||||
;;;; the concrete call site. So this file being two element types with one
|
||||
;;;; runtime behind them is the whole claim.
|
||||
|
||||
(defstruct Point [x i32 y i32])
|
||||
|
||||
;;; Ownership transfers on the call. The caller's binding is dead after this,
|
||||
;;; which is what the refusal cases in test_acceptance assert.
|
||||
(defn consume [v (Vec i32)] i32
|
||||
(let [n (len v)]
|
||||
(free v)
|
||||
n))
|
||||
|
||||
;;; A Vec is returned by moving it out, so the callee's binding is the
|
||||
;;; caller's. Nothing is released at function exit — there is no scope-end
|
||||
;;; anything in this language.
|
||||
(defn make [n i32] (Vec i32)
|
||||
(let [v (vec-new i32)]
|
||||
(dotimes [i n] (push v (* i i)))
|
||||
v))
|
||||
|
||||
(defn sum [xs [i32]] i32
|
||||
(let [total 0]
|
||||
(dotimes [i (len xs)] (set total (+ total (at xs i))))
|
||||
total))
|
||||
|
||||
(defn main [] i32
|
||||
(let [v (vec-new i32)]
|
||||
(println (len v)) ; 0
|
||||
(push v 10)
|
||||
(push v 20)
|
||||
(push v 30)
|
||||
(println (len v)) ; 3
|
||||
(println (at v 0)) ; 10
|
||||
(println (at v 2)) ; 30
|
||||
;; A Vec element is a place, and the same bounds and epoch check stands
|
||||
;; behind the value form and the place form.
|
||||
(set (at v 1) 99)
|
||||
(println (at v 1)) ; 99
|
||||
|
||||
;; as-slice is a non-owning view: it copies ptr+len and never the
|
||||
;; elements, and it carries no allocator, so nothing can be freed through
|
||||
;; one. [at] and [len] over it are the array operations, unchanged.
|
||||
(println (sum (as-slice v))) ; 139
|
||||
(println (len (as-slice v 1 3))) ; 2
|
||||
(println (at (as-slice v 1 3) 0)) ; 99
|
||||
|
||||
;; clone is the only copy: assignment moves. The copy is independent, and
|
||||
;; freeing it leaves the original alone.
|
||||
(let [w (clone v)]
|
||||
(set (at w 0) -1)
|
||||
(println (at w 0)) ; -1
|
||||
(println (at v 0)) ; 10
|
||||
(free w))
|
||||
|
||||
;; reserve does not change the length, only the capacity, so a reserve
|
||||
;; that succeeds is invisible except that the pushes after it do not grow.
|
||||
(reserve v 64)
|
||||
(println (len v)) ; 3
|
||||
(push v 40)
|
||||
(println (len v)) ; 4
|
||||
|
||||
(free v))
|
||||
|
||||
;; A second element type over the same runtime, and a struct element, so
|
||||
;; that size_of and align_of are doing work rather than both being 4.
|
||||
(let [ps (vec-new Point)]
|
||||
(push ps (Point {:x 1 :y 2}))
|
||||
(push ps (Point {:x 3 :y 4}))
|
||||
(println (len ps)) ; 2
|
||||
(println (.y (at ps 1))) ; 4
|
||||
(free ps))
|
||||
|
||||
;; A Vec made against an explicit allocator records it, so free and clone
|
||||
;; never need it named again. An arena cannot free one block, so this free
|
||||
;; keeps the block — releasing it is free-all's job, and that is the
|
||||
;; difference the capability set exists to state.
|
||||
(let [a (arena-new 4096)]
|
||||
(let [v (vec-new i32 a)]
|
||||
(push v 7)
|
||||
(println (at v 0)) ; 7
|
||||
(free v))
|
||||
(println (can-free? a)) ; false
|
||||
(free-all a)
|
||||
(arena-destroy a))
|
||||
|
||||
;; The pushes go into whatever the context names, with nothing passed.
|
||||
(let [a (arena-new 4096)]
|
||||
(with-allocator a
|
||||
(let [v (vec-new i32)]
|
||||
(push v 5)
|
||||
(push v 6)
|
||||
(println (+ (at v 0) (at v 1))) ; 11
|
||||
(free v)))
|
||||
(arena-destroy a))
|
||||
|
||||
(println (consume (make 5))) ; 5
|
||||
0)
|
||||
@ -293,6 +293,68 @@ let () =
|
||||
end;
|
||||
(try Sys.remove exe with Sys_error _ -> ());
|
||||
|
||||
(* (Vec T), spec-memory.md. Two element types over one type-erased
|
||||
runtime, which is the whole claim: size_of and align_of are produced at
|
||||
the concrete call site and nothing below it knows the element type. The
|
||||
moves are here too — into a call and out of one — because a Vec that
|
||||
cannot be handed to a function is not a container anyone can use. *)
|
||||
let vec_out =
|
||||
"0\n3\n10\n30\n99\n139\n2\n99\n-1\n10\n3\n4\n2\n4\n7\nfalse\n11\n5\n"
|
||||
in
|
||||
outputs "vec" "programs/vec.flan" vec_out;
|
||||
outputs ~opt:"-O0" "vec, -O0" "programs/vec.flan" vec_out;
|
||||
outputs ~dev:true "vec, dev" "programs/vec.flan" vec_out;
|
||||
|
||||
(* StorageExhausted and retry. The allocator is genuinely exhausted — a
|
||||
ceiling on live bytes, hit repeatedly — and the handler raises it and
|
||||
invokes retry, so the same request is re-attempted and no push is lost.
|
||||
Every allocating operation is covered, not only push: reserve asks for
|
||||
the whole block at once and clone asks for the source's length.
|
||||
At -O0 because the retry loop and the guard after the error are control
|
||||
flow an optimiser would otherwise launder. *)
|
||||
let exhausted_out = "64\n0\n126\ntrue\ntrue\n4\ntrue\n0\n8\n7\ntrue\n" in
|
||||
outputs "storage exhausted, retried" "programs/exhausted.flan" exhausted_out;
|
||||
outputs ~opt:"-O0" "storage exhausted, retried, -O0" "programs/exhausted.flan"
|
||||
exhausted_out;
|
||||
outputs ~dev:true "storage exhausted, retried, dev" "programs/exhausted.flan"
|
||||
exhausted_out;
|
||||
|
||||
(* The same exhaustion with nothing handling it. [error] is the diverging
|
||||
variant: the program stops on the frame that erred rather than carrying
|
||||
on with a push that appended nothing, which is the Odin outcome the rule
|
||||
exists to make impossible. *)
|
||||
let exe = compile "programs/exhausted-unhandled.flan" in
|
||||
let code, text = run exe None in
|
||||
if code <> 134 || not (contains text "before")
|
||||
|| not (contains text "unhandled StorageExhausted")
|
||||
|| contains text "unreachable"
|
||||
then begin
|
||||
incr failures;
|
||||
Printf.printf
|
||||
"FAIL an unhandled StorageExhausted stops the program\n\
|
||||
\ got: %S (exit %d)\n wanted: exit 134, naming the condition\n"
|
||||
text code
|
||||
end;
|
||||
(try Sys.remove exe with Sys_error _ -> ());
|
||||
|
||||
(* The epoch trap: a container whose allocator has been released. This is
|
||||
spec-memory.md's shipping answer to "Open: catching a use-after-release
|
||||
statically" — detection, loud and immediate, rather than a static rule
|
||||
that with-allocator and context/allocator deny the knowledge for. What
|
||||
is asserted is the reason and the site, not the line. *)
|
||||
let exe = compile "programs/stale-region.flan" in
|
||||
let code, text = run exe None in
|
||||
if code <> 134 || not (contains text "programs/stale-region.flan:")
|
||||
|| not (contains text "allocator was released")
|
||||
then begin
|
||||
incr failures;
|
||||
Printf.printf
|
||||
"FAIL a container 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 _ -> ());
|
||||
|
||||
(* §2's other half, which cannot be an [outputs] case because it does not
|
||||
exit 0: a handler runs, returns normally, and has still not answered the
|
||||
error, so the program stops and names the condition. *)
|
||||
@ -732,6 +794,21 @@ let () =
|
||||
5; this row is the other half of that claim. *)
|
||||
refuses "a user-written allocator" "programs/user-allocator.flan"
|
||||
"a defn's name in value position";
|
||||
(* Move-only, spec-memory.md. Each of these would otherwise be a double
|
||||
free or a use-after-free at run time, and each is refused at the second
|
||||
use with the first one's location in the message. *)
|
||||
refuses "a Vec used after it was passed" "programs/vec-moved.flan"
|
||||
"was moved at";
|
||||
refuses "a Vec freed twice" "programs/vec-double-free.flan"
|
||||
"double free unrepresentable";
|
||||
(* The one case the dead set cannot answer on its own: merged once at the
|
||||
end of the body it counts one move, not two. *)
|
||||
refuses "a Vec moved inside a loop" "programs/vec-moved-in-loop.flan"
|
||||
"the next iteration would use what this one gave away";
|
||||
(* let has no type annotation, so with no element type and no expectation
|
||||
there is nothing to infer from — and guessing is the alternative. *)
|
||||
refuses "vec-new with nothing saying what of" "programs/vec-untyped.flan"
|
||||
"write the element type";
|
||||
|
||||
(* ── wasm32 (NEXT.md, deferred item 6) ──────────────────────────────
|
||||
The second target, and the reason sand-headless imports no raylib. What
|
||||
|
||||
@ -606,8 +606,11 @@ let () =
|
||||
(* ── Unconstrained operators, and everything past milestone 2 ──── *)
|
||||
rejects_check "no built-in = on strings"
|
||||
"(defn f [] bool (= \"a\" \"b\"))" ~needle:"no built-in comparison";
|
||||
rejects_check "Vec is milestone 6" "(defn f [x (Vec i32)])"
|
||||
~needle:"milestone 6";
|
||||
(* (Vec T) is built. What is still refused is the arity: one element type,
|
||||
and a near-miss there would otherwise resolve to a type variable and come
|
||||
back as generics. *)
|
||||
rejects_check "Vec takes one type" "(defn f [x (Vec i32 i32)])"
|
||||
~needle:"exactly one type";
|
||||
rejects_check "Map is milestone 6" "(defn f [x {string i32}])"
|
||||
~needle:"milestone 6";
|
||||
rejects_check "Result is milestone 6" "(defn f [] (Result i32 i32) None)"
|
||||
|
||||
Loading…
x
Reference in New Issue
Block a user