diff --git a/lib/check.ml b/lib/check.ml index 4635e68..ca3dc2a 100644 --- a/lib/check.ml +++ b/lib/check.ml @@ -289,20 +289,6 @@ 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 *data type* 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 @@ -541,9 +527,8 @@ let tyvar_of (t : Types.t) = match t with Types.Var v -> Some v | _ -> None 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?]: [(defn twice [x $t] $t (+ x x))] is refused, which - is right — correct at [i32], a double read of a moved value at [(Vec i32)], - and the checker cannot tell which until it substitutes. + 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] @@ -1368,7 +1353,7 @@ let invented_ctx env ret = { env; ret; slots = 0; slot_tys = []; slot_names = []; scope = []; defers = []; outer = []; outer_what = None; in_frames = None; loops = []; tail = false; in_defer = false; defer_ok = false; defer_block = "a nested form"; - dead = []; borrow = false; owner = "" } + owner = "" } (* The address of field [i] of the struct the pointer in slot [p] points at. *) let field_addr_of loc sty fty p i = @@ -1687,24 +1672,11 @@ let rec check ctx ?want (e : Ast.expr) : Tast.expr = | Ast.If (c, t, e') -> check_if ctx ~tail ?want loc c t e' | Ast.While (label, c, body) -> (* The condition is part of the loop even though it is written outside the - braces: emit puts it in the header block, so it is re-evaluated at the - top of every trip, and a condition that gives a value away frees it once - per trip. So it is held to the loop's rule on moves and to nothing else - the loop changes: it stays outside [in_loop], because a [break] in a - condition still means the enclosing loop and a [defer] there is still - the outer block's, but its moves are diffed against the same dead set. - [dotimes]' count and a [loop]'s initial values are checked outside this - regime on purpose: they are evaluated exactly once, before the first - trip, so giving one away there is no more than giving it away before - the loop. *) - let before = ctx.dead in - let outer = List.map (fun (_, b) -> b.slot) ctx.scope in + braces — emit puts it in the header block, so it is re-evaluated at the + top of every trip — but it stays outside [in_loop], because a [break] + in a condition still means the enclosing loop and a [defer] there is + still the outer block's. *) let c = check ctx ~want:Types.Bool c in - moved_across_iterations ctx ~before ~outer - "this while condition moves a value that was bound outside the loop, and \ - the condition is evaluated again at the top of every trip, so the second \ - one would use what the first gave away. Move it out of the loop, or \ - test something the loop does not give away"; let body = in_loop ctx ?label (fun () -> scoped ctx (fun () -> map_lr (fun b -> check ctx b) body)) in @@ -1951,13 +1923,10 @@ and var ctx loc ~want name = | _ -> match lookup ctx name with | Some b -> - if move_only ctx.env.tvpreds b.bty then - moved ~ty:b.bty 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, _) -> - if Types.is_move_only ty then global_borrow ctx loc name ty; expect loc ~want (mk loc ty (Tast.Global name)) | None -> match Hashtbl.find_opt ctx.env.cases name with @@ -2003,95 +1972,16 @@ and var ctx loc ~want name = | None -> captured ctx loc name; Loc.failk "check/unknown-name" loc "unknown name %s" name) -(* 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 ?ty 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 — %s 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) - (match ty with Some t -> Types.to_string t | None -> "a Vec") name - | None -> ()); - if not ctx.borrow then ctx.dead <- (slot, loc) :: ctx.dead - -(* Reading a move-only *global*, which is the same fork as [moved] with the - other answer: a global is never moved out of, so a site that would have - taken ownership is refused rather than recorded. - - The rule this enforces is one sentence — reading a move-only global is - always a borrow. It is sound for a reason that does not generalise to - locals: the lifetime question, which ownership tracking exists to answer, - has a constant answer here. A global lives as long as the process, so - nothing may free it and nothing needs to; there is no frame whose exit it - could outlive and no second owner to disagree with. What would break the - argument is exactly one thing — someone taking ownership — and that is a - move, and every move reaches this function because [ctx.borrow] is false - everywhere except the operations that said they only look. - - So the dead set is not consulted and not extended. A global cannot be dead: - two functions reading the same one are both borrowing it, which is why the - per-function dead set that the declaration site used to argue from was - never the obstacle it looked like. It could not track a global's ownership; - with this rule there is no ownership to track. - - Mutation is not a move and is not refused. [push], [put] and [set] all take - their target through [borrowed], so a global (Vec u8) is filled and grown in - place, and the aliasing that raises — a push that reallocates invalidating a - slice into the same Vec — is the programmer's, exactly as it is for a local - (spec-memory.md, "Borrowing", and the note on [as-slice] below). Globals get - no rule locals do not have: the dev build's generation word lives on the Vec - and traps on a stale slice whether the Vec is a global or not. *) -and global_borrow ctx loc name (ty : Types.t) = - if not ctx.borrow then - (* The last clause is conditional, because [clone] stopped being offerable - for one of these. A global whose elements own storage is admitted — a - move-only global starts zeroed and this one is no different — but - cloning it is refused, on the grounds that a bytewise copy is an alias - under a name that promises independence. Offering it anyway would send a - reader to a second refusal, and there is no other route to an - independent copy: the region owns the graph, and [free-all] is the only - thing that releases any of it. *) - fail loc - "%s is %s, which is move-only, and a global of one is only ever \ - borrowed: its lifetime is the process's, so nothing may take ownership \ - of it, and this site would. A free through the new owner would leave \ - every other reader of %s pointing at released memory. Read and mutate \ - it where it is — (len %s), (at %s i), (push %s x), (set (at %s i) x) \ - — or take a view with (as-slice %s) or a pointer with (addr %s)%s" - name (Types.to_string ty) name name name name name name name - (if region_only ctx.env ty then - ". There is no independent copy of this one: its elements own \ - storage, so a clone would alias rather than copy and is refused" - else - Printf.sprintf - ", or an independent copy with (clone %s), which is the one of \ - these that something else may own" name) - -(* The target of an operation that reads a container without consuming it. Only - 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 +(* 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". *) (* [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 @@ -2170,7 +2060,7 @@ and check_fn ctx ~want loc (params : string list) body = scope = []; defers = []; outer = ctx.scope; outer_what = Some "an fn"; in_frames = None; loops = []; tail = false; in_defer = false; defer_ok = false; defer_block = "a nested form"; - dead = []; borrow = false; owner = ctx.owner } + owner = ctx.owner } in List.iter2 (fun n t -> ignore (bind fctx n t ~assignable:false)) params pts; @@ -2244,7 +2134,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; outer_what = Some "a handler"; in_frames = None; loops = []; tail = false; in_defer = false; defer_ok = false; defer_block = "a nested form"; dead = []; borrow = false; owner = "" } + scope = []; defers = []; outer = ctx.scope; outer_what = Some "a handler"; in_frames = None; loops = []; tail = false; in_defer = false; defer_ok = false; defer_block = "a nested form"; owner = "" } in (* The condition crosses as a pointer, because the handler runs while the signalling frame is still alive and there is nothing to copy. @@ -2422,53 +2312,24 @@ and check_let ctx ?(tail = false) ?want ?(defer_ok = false) 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 ?label ?entry ?(fresh = []) f = - let outer_slots = - List.filter (fun s -> not (List.mem s fresh)) - (List.map (fun (_, b) -> b.slot) ctx.scope) - in - let before = ctx.dead in +(* What a loop still contributes to checking after the repeal is scoping, not + ownership: the entry below is what [break] and [continue] resolve against, + and the defer_block name is what makes a [defer] in here refused as "a loop + body" — it would fire once at function exit rather than once per iteration, + and the message says so. [fresh] and the iteration move-diff that used it + are gone with the flow analysis. *) +and in_loop ctx ?label ?entry f = (* The loop goes on the stack before the body is checked and comes off after, so a [break] inside it can see it and one outside it cannot. *) let loops = ctx.loops in - (* [fresh] is a [loop]'s own names. They are bound before the entry is pushed - — their initial values are evaluated once, outside — but [recur] writes - every one of them on the way round, so the next iteration never sees what - this one gave away and the rule below is not about them. *) ctx.loops <- (match entry with Some e -> e | None -> Lloop label) :: loops; - (* Named so that a defer written in here is refused as "a loop body" rather - than as a nested form: the reason is specific — it would fire once at - function exit rather than once per iteration — and the message says it. *) let blocker = ctx.defer_block in ctx.defer_block <- "a loop body"; let r = f () in ctx.defer_block <- blocker; ctx.loops <- loops; - moved_across_iterations ctx ~before ~outer:outer_slots - "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"; r -(* The rule a loop adds to the move checker, in one place because two forms - need it and they need it for the same reason. Everything that runs more - than once runs against the dead set it left behind last time: a slot that - was live on the way in and is dead on the way out was given away by code - that is about to run again, and the second run would be using what the - first one released. Slots bound inside the repeated region are not in - [outer] and are not the question — they are born again every trip. *) -and moved_across_iterations ctx ~before ~outer why = - List.iter - (fun (slot, where) -> - if (not (List.mem_assoc slot before)) && List.mem slot outer then - fail where "%s" why) - ctx.dead - (* Which loop a [break] or a [continue] means, as a count of loops outwards from the innermost — which is what [Tast.Break] carries and what [emit] indexes. Refuses three things, each by its own reason: nothing to break out @@ -2606,7 +2467,7 @@ and check_loop ctx ?want loc bs body = is therefore monomorphic, and every other caller hands it a list. *) let tbody = match - in_loop ctx ~entry:(Lrecur names) ~fresh:(List.map fst binds) (fun () -> + in_loop ctx ~entry:(Lrecur names) (fun () -> [ scoped ctx (fun () -> (* The body's last form is the loop's tail, which is the only place a [recur] may stand. [block] distributes it. *) @@ -2704,15 +2565,7 @@ and check_if ctx ?(tail = false) ?want loc c t e = let t = branch ctx (fun () -> in_tail (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 data type 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 = branch ctx (fun () -> in_tail (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 = @@ -2721,9 +2574,6 @@ and check_if ctx ?(tail = false) ?want loc c t e = | None -> if t.Tast.ty = Types.Never then None else Some t.Tast.ty in let e = branch ctx (fun () -> in_tail (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 @@ -3030,13 +2880,6 @@ and check_match ctx ?(tail = false) ?want loc scrutinee arms = let want = ref want in let seen = Hashtbl.create 8 in let saw_wild = ref false in - (* The same rule as [if], and for the same reason: the arms are alternatives, - so each is checked from the state before the match and the data type of what - they moved survives the join. Checked in sequence against one mutating set - they would report the second arm's (free v) as a use after the first arm's - move, which is a legal program refused. *) - let before = ctx.dead in - let joined = ref [] in let arms = map_lr (fun (a : Ast.arm) -> @@ -3047,28 +2890,20 @@ and check_match ctx ?(tail = false) ?want loc scrutinee arms = if Hashtbl.mem seen c then fail a.Ast.aloc "this match has two %s arms" c; Hashtbl.add seen c ()); - ctx.dead <- before; - let arm = - branch ctx (fun () -> - let binds = - List.map - (fun (n, ty) -> bind ctx n ty ~assignable:false) binds - in - (* Every arm is the tail, exactly as an [if]'s two arms are. - Restored here because checking the scrutinee withdrew it. *) - ctx.tail <- tail; - let body = block ctx ?want:!want a.Ast.aloc a.Ast.body in - if !want = None && body.Tast.ty <> Types.Never then - want := Some body.Tast.ty; - { Tast.acase = ctor; binds; abody = [ body ] }) - in - joined := - !joined - @ List.filter (fun (k, _) -> not (List.mem_assoc k !joined)) ctx.dead; - arm) + branch ctx (fun () -> + let binds = + List.map + (fun (n, ty) -> bind ctx n ty ~assignable:false) binds + in + (* Every arm is the tail, exactly as an [if]'s two arms are. + Restored here because checking the scrutinee withdrew it. *) + ctx.tail <- tail; + let body = block ctx ?want:!want a.Ast.aloc a.Ast.body in + if !want = None && body.Tast.ty <> Types.Never then + want := Some body.Tast.ty; + { Tast.acase = ctor; binds; abody = [ body ] })) arms in - ctx.dead <- !joined; (* Exhaustiveness is refused, not defaulted. A match that silently fell through would have to produce a value of the match's type out of nothing, and there is no such value for most types; and the case a data type grows @@ -3161,7 +2996,7 @@ and check_place ctx loc (p : Ast.place) : Tast.place * Types.t = "%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 = borrowed ctx target (fun () -> check ctx target) in + let target = 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 @@ -3993,7 +3828,7 @@ and named_call ctx ~want loc name args = arity loc name 2 args; (match args with | [ target; x ] -> - let target = borrowed ctx target (fun () -> check ctx target) in + let target = 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 @@ -4021,7 +3856,7 @@ and named_call ctx ~want loc name args = arity loc name 2 args; (match args with | [ target; n ] -> - let target = borrowed ctx target (fun () -> check ctx target) in + let target = check ctx target 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 ])) @@ -4064,7 +3899,7 @@ and named_call ctx ~want loc name args = | "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 target = check ctx target in let elem = vec_elem loc "as-slice" target.Tast.ty in let lo, hi = match rest with @@ -4087,10 +3922,12 @@ and named_call ctx ~want loc name args = (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. *) + (* 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. *) | "free" -> arity loc name 1 args; let target = check ctx (List.hd args) in @@ -4166,7 +4003,7 @@ and named_call ctx ~want loc name args = (* Checked once, then dispatched on what it turned out to be: checking it inside a guard as well would allocate the target's slots twice and evaluate whatever it was written as twice. *) - let target = borrowed ctx target (fun () -> check ctx target) in + let target = check ctx target in let a = allocator_arg ctx loc rest in (match target.Tast.ty with (* The refusal that did *not* come down with the type-level ones, and @@ -4294,7 +4131,7 @@ and named_call ctx ~want loc name args = arity loc name 2 args; (match args with | [ target; x ] -> - let target = borrowed ctx target (fun () -> check ctx target) in + 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 @@ -4344,7 +4181,7 @@ and named_call ctx ~want loc name args = arity loc name 2 args; (match args with | [ target; h ] -> - let target = borrowed ctx target (fun () -> check ctx target) in + 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 @@ -4400,7 +4237,7 @@ and named_call ctx ~want loc name args = arity loc name 2 args; (match args with | [ target; h ] -> - let target = borrowed ctx target (fun () -> check ctx target) in + 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 @@ -4425,7 +4262,7 @@ and named_call ctx ~want loc name args = quiet wrong answer this whole type exists to remove. *) | "live" -> arity loc name 1 args; - let target = borrowed ctx (List.hd args) (fun () -> check ctx (List.hd args)) in + 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 ]))) @@ -4444,7 +4281,7 @@ and named_call ctx ~want loc name args = arity loc name 2 args; (match args with | [ target; i ] -> - let target = borrowed ctx target (fun () -> check ctx target) in + 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 @@ -4510,7 +4347,7 @@ and named_call ctx ~want loc name args = arity loc name 3 args; (match args with | [ target; k; v ] -> - let target = borrowed ctx target (fun () -> check ctx target) in + let target = check ctx target in let kt, vt = map_kv loc "put" target.Tast.ty in let k = check ctx ~want:kt k in let v = check ctx ~want:vt v in @@ -4549,7 +4386,7 @@ and named_call ctx ~want loc name args = arity loc name 2 args; (match args with | [ target; k ] -> - let target = borrowed ctx target (fun () -> check ctx target) in + let target = check ctx target in let kt, vt = map_kv loc "get" target.Tast.ty in let k = check ctx ~want:kt k in (* Deferred, and the placeholder is [None] rather than [Unit]: this @@ -4607,7 +4444,7 @@ and named_call ctx ~want loc name args = arity loc name 2 args; (match args with | [ target; k ] -> - let target = borrowed ctx target (fun () -> check ctx target) in + let target = check ctx target in let kt, vt = map_kv loc "map-remove!" target.Tast.ty in let k = check ctx ~want:kt k in (* Deferred exactly as [get] is, and with [None] for the same reason: @@ -4668,7 +4505,7 @@ and named_call ctx ~want loc name args = arity loc name 4 args; (match args with | [ target; cur; k; v ] -> - let target = borrowed ctx target (fun () -> check ctx target) in + let target = check ctx target in let kt, vt = map_kv loc "map-next!" target.Tast.ty in let cur = check ctx ~want:(Types.Ptr (Types.Int Types.I64)) cur in let k = check ctx ~want:(Types.Ptr kt) k in @@ -4692,7 +4529,7 @@ and named_call ctx ~want loc name args = arity loc name 2 args; (match args with | [ target; k ] -> - let target = borrowed ctx target (fun () -> check ctx target) in + let target = check ctx target in let kt, vt = map_kv loc "has-key?" target.Tast.ty in let k = check ctx ~want:kt k in (* Deferred, and the placeholder is a [bool] — the form a condition @@ -4967,7 +4804,7 @@ and named_call ctx ~want loc name args = | "len" -> arity loc name 1 args; let target = List.hd args in - let a = borrowed ctx target (fun () -> check ctx target) in + let a = check ctx target in (match a.Tast.ty with | Types.Array _ | Types.Slice _ | Types.String -> prim Tast.Len index_ty [ a ] @@ -4993,7 +4830,7 @@ and named_call ctx ~want loc name args = | "at" -> (match args with | target :: idx when idx <> [] -> - let target = borrowed ctx target (fun () -> check ctx target) in + let target = check ctx target in (match target.Tast.ty with | Types.Vec _ -> let p, elem = vec_at ctx loc target idx in @@ -5208,7 +5045,7 @@ and named_call ctx ~want loc name args = nothing. Without this, (println v) would consume a Vec and every printing of one would be its last. *) let target = List.hd args in - let a = borrowed ctx target (fun () -> check ctx target) in + let a = check ctx target in (* ── The allow-list, and what it takes to get on it ─────────────── plan.org names [println] as the one compiler-provided exception — it "selects a structural printer at each concrete instantiation" — and @@ -6081,7 +5918,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 = []; outer_what = None; in_frames = None; loops = []; tail = false; in_defer = false; defer_ok = false; defer_block = "a nested form"; dead = []; borrow = false; owner = "" } v).Tast.ty + outer = []; outer_what = None; in_frames = None; loops = []; tail = false; in_defer = false; defer_ok = false; defer_block = "a nested form"; owner = "" } v).Tast.ty in let pending = ref (List.rev !untyped) in let rec settle () = @@ -6204,7 +6041,7 @@ let check_union_members env = let rec 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 = []; outer_what = None; in_frames = None; loops = []; tail = false; in_defer = false; defer_ok = false; defer_block = "a nested form"; dead = []; borrow = false; + outer = []; outer_what = None; in_frames = None; loops = []; tail = false; in_defer = false; defer_ok = false; defer_block = "a nested form"; owner = fn.Ast.name } in List.iter2 (fun (p : Ast.field) ty -> @@ -6323,10 +6160,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, and what makes it legal is [var]'s - refusal rather than anything here: reading one is always a borrow, so no - function can take it, and none can free it. See [global_borrow] for why that - one sentence is enough where a general ownership model would not be. +(* 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. What this pass still 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 @@ -6405,7 +6244,7 @@ let no_union_init env loc n what (v : Tast.expr) = 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 = []; outer_what = None; in_frames = None; loops = []; tail = false; in_defer = false; defer_ok = false; defer_block = "a nested form"; dead = []; borrow = false; owner = "" } in + outer = []; outer_what = None; in_frames = None; loops = []; tail = false; in_defer = false; defer_ok = false; defer_block = "a nested form"; owner = "" } in match d.Ast.d with | Ast.Defvar (n, _, init) -> let ty, _ = Hashtbl.find env.globals n in @@ -6668,7 +6507,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 = []; outer_what = None; in_frames = None; loops = []; tail = false; in_defer = false; defer_ok = false; defer_block = "a nested form"; dead = []; borrow = false; owner = "" } + outer = []; outer_what = None; in_frames = None; loops = []; tail = false; in_defer = false; defer_ok = false; defer_block = "a nested form"; owner = "" } in let t = check ctx e in (t, Array.of_list (List.rev ctx.slot_tys), diff --git a/test/test_acceptance.ml b/test/test_acceptance.ml index 6451bb8..48df08c 100644 --- a/test/test_acceptance.ml +++ b/test/test_acceptance.ml @@ -1958,17 +1958,11 @@ let () = pointer-width. Two reasons, both named, neither a function value. *) refuses "a user-written allocator" "programs/user-allocator.flan" "is no longer what is missing"; - (* 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"; + (* Move-only, spec-memory.md, since the repeal: the three fixtures that + were refused here — a use after a pass, a double free, a move inside a + loop — now compile, and what they do at run time is the allocator's and + the dev build's to catch. They are kept as programs (the double-free + one is what the sanitize sweep watches) but no longer as refusals. *) (* 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" @@ -2537,11 +2531,6 @@ ERR@7 unexpected token: not the kind the caller was reading refuses_src "map-new with nothing to say what it maps" "(defn main [] i32 (let [m (map-new)] (free m)) 0)" "nothing here says what (map-new) maps"; - (* A map is move-only like a Vec, and the refusal names the type that was - moved rather than saying "a Vec" whatever it was. *) - refuses_src "a map used after it was moved" - "(defn main [] i32 (let [m (map-new i32 i32)] (free m) (put m 1 2)) 0)" - "cannot be used again"; (* ── Data type values ─────────────────────────────────────────── defdata parsed and its shape was checked; naming the type and constructing a value were refused as milestone 6. The program covers a diff --git a/test/test_flan.ml b/test/test_flan.ml index 167c9c1..c8292b5 100644 --- a/test/test_flan.ml +++ b/test/test_flan.ml @@ -1078,26 +1078,11 @@ let () = ~needle:"cannot be cloned"; (* ── A move-only global ───────────────────────────────────────────── - Legal now, and legal because of one rule: reading one is always a borrow. - The accepted side is programs/vec-global.flan, which has to run to say - anything; these are the four things the rule refuses, and between them - they are the whole of it. - - The first two are the rule itself. Ownership is what may not be taken, and - the two ways to take it — hand the global to something that owns its - parameter, or bind it to a local that owns it — are the same refusal at - the read, because that is where a move would have been recorded for a - local. [free] is the third of them and reaches it the same way: it does - not borrow its target, so nothing special had to be written for it. *) - rejects_check "passing a global Vec to a function" - "(defvar g (Vec u8)) (defn eat [v (Vec u8)] () (free v)) (defn f [] () (eat g))" - ~needle:"only ever borrowed"; - rejects_check "freeing a global Vec" - "(defvar g (Vec u8)) (defn f [] () (free g))" - ~needle:"only ever borrowed"; - rejects_check "binding a global Vec to a local" - "(defvar g (Vec u8)) (defn f [] () (let [v g] (free v)))" - ~needle:"only ever borrowed"; + Legal, started zeroed, and since the repeal of the flow analysis it is + ownable like anything else: passing, binding and freeing one all + type-check, and the process-long lifetime is the program's to keep. The + accepted side is programs/vec-global.flan. What is still refused about + one is declaration-shaped, below. *) (* And the two declaration shapes. A computed initialiser would have to run before main, which is a path [Emit.const] does not have and which [x86.ml] deliberately leaves out of a reload module; a defconst could @@ -1224,14 +1209,7 @@ let () = rejects_check "a labelled break may not leave a loop" "(defn f [] () (while :o true (loop [i 0] (break :o))))" ~needle:"no value to give"; - (* A while's condition runs once per trip, so it lives under the same rule - as the body: what it gives away, it gives away again next time round. - Before this was checked the program below compiled and aborted in free(). *) - rejects_check "a while condition may not move what the loop is standing on" - "(defn eat [v (Vec i32)] bool (do (free v) true)) \ - (defn f [] () (let [v (vec-new i32)] (while (eat v) (break))))" - ~needle:"evaluated again at the top of every trip"; - accepts "a condition that only looks at what it tests is fine" + accepts "a while condition is an ordinary expression" "(defn f [] () (let [v (vec-new i32) n 0] \ (while (and (< n 10) (> (len v) 0)) (set n (+ n 1))) (free v)))"; rejects_check "loop takes no label" @@ -2687,16 +2665,12 @@ let () = ~needle:"is not a type variable of f" "(defn f [a i32] i32 {:where (ordered? $t)} a)"; - (* Move-only by default, which is the other half of the where clause and the - one with no Odin counterpart: Odin has no move semantics, so its $T never - has to answer. The prior art is Rust's T: Copy, and the difference is - that copyable? is a question the compiler answers rather than a trait a - user implements. Conservative in the safe direction — move is the - stricter rule, so assuming it can only refuse a valid program. *) - rejects_check "a type variable is move-only until it says otherwise" - ~needle:"cannot be used again" + (* 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?" "(defn twice [a $t b (Fn [$t $t] $t)] $t (b a a))"; - accepts "and copyable? is the opt-out" + accepts "and copyable? is still a clause a signature may state" "(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