diff --git a/lib/check.ml b/lib/check.ml index b14836d..d956f2e 100644 --- a/lib/check.ml +++ b/lib/check.ml @@ -226,7 +226,23 @@ 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", [ a ] -> Types.Vec (resolve env ~seen a) + | "Vec", [ a ] -> + let e = resolve env ~seen a in + (* A Vec of a Vec is representable and would be wrong. spec-memory.md + makes [clone] a deep copy and makes [free] recurse structurally into + owning fields; the type-erased runtime does neither — it memcpys, so + a clone would duplicate inner headers and a free would drop their + buffers on the floor. Recursive teardown is what step 5's [drop] + brings, and this is refused until it does rather than shipping the + shallow answer under the deep name. *) + if Types.is_move_only e then + fail loc + "(Vec %s) holds a move-only element, and the type-erased runtime \ + copies and releases elements bytewise — so clone would duplicate \ + headers instead of copying, and free would leak what they own. \ + Recursive teardown arrives with drop (step 5 in NEXT.md)" + (Types.to_string e); + Types.Vec e | "Vec", _ -> fail loc "(Vec T) takes exactly one type" | "Map", _ -> unimplemented loc "(Map K V)" 6 | "Result", _ -> unimplemented loc "(Result T E)" 6 @@ -994,6 +1010,13 @@ and check_match ctx ?want loc scrutinee arms = in let want = ref want in let saw_some = ref false and saw_none = ref false and 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 union 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) -> @@ -1009,14 +1032,24 @@ and check_match ctx ?want loc scrutinee arms = fail a.Ast.aloc "%s is not a case of Option — the cases are Some and None" c in - scoped ctx (fun () -> - let binds = List.map (fun n -> bind ctx n elem ~assignable:false) binds in - 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 ] })) + ctx.dead <- before; + let arm = + scoped ctx (fun () -> + let binds = + List.map (fun n -> bind ctx n elem ~assignable:false) binds + in + 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) arms in + ctx.dead <- !joined; if not (!saw_wild || (!saw_some && !saw_none)) then fail loc "this match is not exhaustive — Option needs both Some and None, or a \ @@ -2247,8 +2280,29 @@ let collect env (decls : Ast.decl list) = let names = List.map (fun (f : Ast.field) -> f.Ast.fname) fs in if List.length (List.sort_uniq compare names) <> List.length names then fail loc "%s declares the same field twice" n; - Hashtbl.replace env.structs n - { Tast.sname = n; fields = List.map field fs } + let fields = List.map field fs in + (* spec-memory.md: "Ownership is structural, not declared" — a struct + containing a Vec is itself move-only, and freeing one recurses into + its owning fields while (free (.items b)) is refused because it + would leave the owner partly dead. None of that transitive + machinery exists yet: it is the same recursive teardown [drop] + brings, and it lands with it. Until then the field is refused at + the declaration, where the message can say so, rather than + accepted into a struct that copies its header on assignment and + gives two owners one buffer. *) + List.iter + (fun (f : Tast.field) -> + if Types.is_move_only f.Tast.fty then + fail loc + "%s's field %s is %s, which is move-only, and a struct that \ + owns one is move-only too — transitively, with recursive \ + teardown and with a field that cannot be freed on its own. \ + That rule arrives with drop (step 5 in NEXT.md); until then \ + hold the %s in a local and pass it" + n f.Tast.fname (Types.to_string f.Tast.fty) + (Types.to_string f.Tast.fty)) + fields; + Hashtbl.replace env.structs n { Tast.sname = n; fields } | Ast.Defunion (n, vs) -> Hashtbl.replace env.unions n { Tast.uname = n; @@ -2406,12 +2460,29 @@ let check_fn env (fn : Ast.fn) : Tast.fn = normal path has them spliced into [body] above. *) ret; body; fdefers = ctx.defers; fparent = None; floc = fn.Ast.nloc } +(* A global of move-only type is refused. The dead set is per function, so two + functions each freeing the same global is a double free nothing here could + see; and within one function a global read does not go through [var]'s move + path at all, so even the local case would be accepted. Rather than half a + rule, the type is refused where it is declared. A global *Allocator* is not + this — an allocator is a copyable opaque handle — which is what makes the + handler-owns-the-arena shape in exhausted.flan expressible. *) +let no_move_only_global loc n (ty : Types.t) = + if Types.is_move_only ty then + fail loc + "the global %s is %s, which is move-only, and ownership of a global \ + cannot be tracked: the dead set is per function, so two functions each \ + freeing it is a double free nothing would catch. Hold it in a local and \ + pass it, or hold the allocator globally instead" + n (Types.to_string ty) + 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; dead = []; borrow = false; owner = "" } in match d.Ast.d with | Ast.Defvar (n, _, init) -> let ty, _ = Hashtbl.find env.globals n in + no_move_only_global d.Ast.dloc n ty; let ginit = match init with | Ast.Zeroed -> { Tast.e = Tast.Zero ty; ty; loc = d.Ast.dloc } @@ -2421,6 +2492,7 @@ let check_global env (d : Ast.decl) : Tast.global option = Some { Tast.gname = n; gty = ty; ginit; gconst = false; gfolded = false } | Ast.Defconst (n, _, v) -> let ty, _ = Hashtbl.find env.globals n in + no_move_only_global d.Ast.dloc n ty; (* [collect] already folded the integer constants, because an array length has to be known before any type resolves. Use that value here rather than the expression it came from: a global's initialiser has to be a diff --git a/lib/shim.ml b/lib/shim.ml index 7367938..b9bfbee 100644 --- a/lib/shim.ml +++ b/lib/shim.ml @@ -217,6 +217,15 @@ let rec cty env ~needed ~loc ~what (t : Ast.texpr) : string = declare (Ptr T) and say which" what | Ast.Tmap _ -> fail loc "%s is a map, which has no C representation" what + (* A Vec owns its storage, so handing its header to C hands out an owner and + there is no rule for what C would then be allowed to do with it. The + elements cross the way any other run of elements does. *) + | Ast.Tapp ("Vec", _) -> + fail loc + "%s is a Vec, which owns its storage — handing its header to C hands out \ + an owner. Pass (as-slice v) as (Ptr T) and (len v), the same shape a \ + slice crosses in" + what | Ast.Tfn _ -> fail loc "%s is a function type, and a C callback is not implemented" what | Ast.Tapp (n, _) -> diff --git a/test/programs/vec-global.flan b/test/programs/vec-global.flan new file mode 100644 index 0000000..b1be5f6 --- /dev/null +++ b/test/programs/vec-global.flan @@ -0,0 +1,9 @@ +;;;; A global of move-only type. The dead set is per function, so two functions +;;;; each freeing this is a double free nothing here could see — and a global +;;;; read does not go through the move path at all, so even the one-function +;;;; case would be accepted. Half a rule is worse than none, so the type is +;;;; refused where it is declared. A global *Allocator* is a different thing +;;;; and is allowed: an allocator is a copyable opaque handle. +(defvar everything (Vec i32)) + +(defn main [] i32 0) diff --git a/test/programs/vec-in-struct.flan b/test/programs/vec-in-struct.flan new file mode 100644 index 0000000..e0a5a08 --- /dev/null +++ b/test/programs/vec-in-struct.flan @@ -0,0 +1,9 @@ +;;;; spec-memory.md: "Ownership is structural, not declared" — a struct +;;;; containing a Vec is itself move-only, transitively, with recursive +;;;; teardown, and with a field that cannot be freed on its own. None of that +;;;; machinery exists: it is the same recursive teardown `drop` brings, and it +;;;; lands with it. Accepting the field meanwhile would give a struct that +;;;; copies its header on assignment two owners of one buffer. +(defstruct Builder [buf (Vec u8)]) + +(defn main [] i32 0) diff --git a/test/programs/vec-of-vec.flan b/test/programs/vec-of-vec.flan new file mode 100644 index 0000000..5e45125 --- /dev/null +++ b/test/programs/vec-of-vec.flan @@ -0,0 +1,10 @@ +;;;; A Vec of a Vec is representable and would be wrong. The runtime is +;;;; type-erased: it copies and releases elements bytewise, so `clone` would +;;;; duplicate the inner headers instead of copying what they own, and `free` +;;;; would drop their buffers on the floor. spec-memory.md makes clone a deep +;;;; copy and makes free recurse structurally into owning fields; recursive +;;;; teardown is what `drop` brings, and this is refused until it does rather +;;;; than shipping the shallow answer under the deep name. +(defn rows [xs (Vec (Vec i32))] i32 0) + +(defn main [] i32 0) diff --git a/test/programs/vec-to-c.flan b/test/programs/vec-to-c.flan new file mode 100644 index 0000000..8ebc429 --- /dev/null +++ b/test/programs/vec-to-c.flan @@ -0,0 +1,8 @@ +;;;; A Vec cannot cross to C. The shim flattens a struct that crosses, and a +;;;; Vec is not a struct anyone should flatten: it owns storage, and handing +;;;; its header to C hands out an owner. It falls to the same aggregate +;;;; refusal every other non-scalar declare-c parameter gets, which is the +;;;; point — nothing special was needed and nothing special was added. +(declare-c vec-sum [v (Vec i32)] i32 "vec_sum") + +(defn main [] i32 0) diff --git a/test/test_acceptance.ml b/test/test_acceptance.ml index da75f72..2587326 100644 --- a/test/test_acceptance.ml +++ b/test/test_acceptance.ml @@ -809,6 +809,21 @@ let () = 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"; + (* The three shapes ownership is not transitive through yet. Each is + refused where it is declared, naming drop as what it waits on, rather + than accepted into a path that would copy a header and hand out a + second owner. *) + refuses "a struct field that owns a Vec" "programs/vec-in-struct.flan" + "a struct that owns one is move-only too"; + refuses "a global Vec" "programs/vec-global.flan" + "the dead set is per function"; + refuses "a Vec of a Vec" "programs/vec-of-vec.flan" + "copies and releases elements bytewise"; + (* And it does not cross to C: the shim would flatten a header that owns + storage. Refused by the shim generator, where the message can say what + to pass instead. *) + refuses "a Vec crossing to C" "programs/vec-to-c.flan" + "handing its header to C hands out an owner"; (* ── wasm32 (NEXT.md, deferred item 6) ────────────────────────────── The second target, and the reason sand-headless imports no raylib. What