From a1111f7b3cdd9a20f74b8b961dd8a66468f08b8c Mon Sep 17 00:00:00 2001 From: Joseph Ferano Date: Sat, 19 Sep 2026 23:02:26 +0700 Subject: [PATCH] The foreign boundary is about ownership, and it was reading shape MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Three shapes hand a dyn word into memory nothing roots, and the check written last round caught one of them. A (Ptr S) return was refused; (Ptr (Ptr S)) and (Ptr [S]) were not, because the predicate it asked was dyn_anywhere, which had just been taught to stop at a pointer. Stopping there is right — a pointer is a view of storage something else roots, and that is what lets a (Vec (Ptr Cond)) be written — but it is the wrong question at a boundary where nothing roots the far side at all. So there are two predicates now. dyn_anywhere is the storage-shaped one and is unchanged; dyn_through follows pointers and slices, and only the foreign boundary asks it. The second of those shapes matters more than it looks: (Ptr [S]) is what shim.ml's own advice tells people to write when C returns an aggregate. Neither was a regression. At the commit before last there was no walk over the externs at all and all three were accepted; what landed was one level of a check that wanted to be recursive. And the direction. The refusal was justified by what C hands back and then applied to parameters as well, which made the ordinary read-only borrow unexpressible: a foreign parameter receives the address of a *place*, and a place is a frame slot, a global or an array inside one, every one of them rooted with its descriptor and marked for the whole call. So (Ptr S) and [S] as parameters are borrows and stay writable. One level down the storage is C's again — a (Ptr (Ptr S)) parameter is an out-parameter and what C writes into it is a pointer of C's own — so the parameter question is asked below the outermost level and the return question is asked from the top. Evidence, all three shapes with the check lifted, ASan: heap-use-after-free in flan_dyn_tag, freed by gc_sweep out of flan_gc_collect, allocated by the Flan frame that stored it. With the check back, all three refused by name. And the allowed direction proved rather than assumed: a C read-only borrow of a (Ptr S) and a [S] slice argument, called before and after twenty thousand allocations, dyn fields intact and clean under ASan. A Tast.extern carries its declare's location now, so these refusals point at the line rather than at :0:0. Last, the one arm of the saturation that did not saturate: a negative array length reached the multiplication as a small number, which is the exact shape the cap must never be handed. Out of range in either direction saturates. dune test --force: green, 0 failures. --- lib/check.ml | 157 ++++++++++++++++++++++++++++++++++------------ lib/dev.ml | 2 +- lib/session.ml | 14 +++-- lib/tast.ml | 4 ++ test/test_flan.ml | 56 +++++++++++++++-- 5 files changed, 181 insertions(+), 52 deletions(-) diff --git a/lib/check.ml b/lib/check.ml index 406866d..3f45eb6 100644 --- a/lib/check.ml +++ b/lib/check.ml @@ -74,6 +74,10 @@ type env = { (* Flan name -> the C symbol it is really called by. A foreign function is an ordinary entry in [fns] as well; this only records how to name it. *) externs : (string, string) Hashtbl.t; + (* Where each [declare] was written, by Flan name. A second table rather + than a pair in [externs], because every other reader of that one wants + the symbol and nothing else. *) + extern_locs : (string, Loc.t) Hashtbl.t; fns : (string, Types.t list * Types.t) Hashtbl.t; globals : (string, Types.t * bool) Hashtbl.t; (* type, is a constant *) (* Functions the checker made up: a handler-bind clause is lifted into one, @@ -139,6 +143,7 @@ let new_env () = { locs = Hashtbl.create 16; enums = Hashtbl.create 8; externs = Hashtbl.create 32; + extern_locs = Hashtbl.create 32; fns = Hashtbl.create 32; globals = Hashtbl.create 16; lifted = []; @@ -6468,7 +6473,8 @@ let collect env (decls : Ast.decl list) = List.iter (crossable "a parameter") params; crossable "the return type" ret; Hashtbl.replace env.fns fn.Ast.name (params, ret); - Hashtbl.replace env.externs fn.Ast.name csym + Hashtbl.replace env.externs fn.Ast.name csym; + Hashtbl.replace env.extern_locs fn.Ast.name loc | Ast.Defalias _ -> () | Ast.Defstruct (n, fs) -> let names = List.map (fun (f : Ast.field) -> f.Ast.fname) fs in @@ -7431,37 +7437,76 @@ let desc_offsets_max = 4096 [(Vec (Ptr Cond))] be written — a vector of pointers to condition structs holds no dyn words of its own, and refusing it with a sentence about the dyn inside it was wrong twice over. *) -let rec dyn_anywhere p seen (t : Types.t) = - let go = dyn_anywhere p seen in +let rec dyn_reach ~through p seen (t : Types.t) = + let go = dyn_reach ~through p seen in match t with | Types.Dyn -> true | Types.Array (_, e) | Types.Vec e | Types.Option e -> go e | Types.Map (k, v) -> go k || go v - | Types.Ptr _ | Types.Slice _ | Types.Fn _ -> false + | Types.Ptr e | Types.Slice e -> through && go e + | Types.Fn _ -> false | Types.Named n when not (List.mem n seen) -> let seen = n :: seen in + let field (fl : Tast.field) = dyn_reach ~through p seen fl.Tast.fty in (match List.find_opt (fun (s : Tast.structure) -> s.Tast.sname = n) p.Tast.structs with - | Some s -> - List.exists (fun (fl : Tast.field) -> dyn_anywhere p seen fl.Tast.fty) - s.Tast.fields + | Some s -> List.exists field s.Tast.fields | None -> match List.find_opt (fun (u : Tast.data) -> u.Tast.dname = n) p.Tast.datas with | Some u -> List.exists - (fun (c : Tast.variant) -> - List.exists - (fun (fl : Tast.field) -> dyn_anywhere p seen fl.Tast.fty) - c.Tast.vfields) + (fun (c : Tast.variant) -> List.exists field c.Tast.vfields) u.Tast.cases | None -> match List.find_opt (fun (u : Tast.structure) -> u.Tast.sname = n) p.Tast.unions with - | Some u -> - List.exists - (fun (fl : Tast.field) -> dyn_anywhere p seen fl.Tast.fty) - u.Tast.fields + | Some u -> List.exists field u.Tast.fields + | None -> false) + | _ -> false + +let dyn_anywhere p seen t = dyn_reach ~through:false p seen t + +(* The other question, and it is a different one: is there a dyn reachable from + here *at all*, pointers and slices followed. Only the foreign boundary asks + it, and it has to — the storage on the far side of a pointer is rooted where + it was declared when the declaration was Flan's, and is rooted nowhere at + all when it was C's. Keeping the two apart is the whole of the fix: the + narrowing above is right for a Flan type, and reusing it at the boundary + made [(Ptr (Ptr S))] and [(Ptr [S])] answer no. *) +let dyn_through p seen t = dyn_reach ~through:true p seen t + +(* Is a dyn reachable from here only by going through a pointer or a slice. + This is the parameter question. Flan supplies the storage one level down + from a foreign parameter — it passes the address of a place, and a place is + a frame slot, a global or an array inside one, all of them rooted with their + descriptor — so a [(Ptr S)] parameter is an ordinary borrow and stays + writable. What is *below* that level is C's, and a pointer or a slice found + there is a hop into storage nothing rooted. *) +let rec dyn_behind_pointer p seen (t : Types.t) = + let go = dyn_behind_pointer p seen in + match t with + | Types.Ptr e | Types.Slice e -> dyn_through p seen e + | Types.Array (_, e) | Types.Vec e | Types.Option e -> go e + | Types.Map (k, v) -> go k || go v + | Types.Dyn | Types.Fn _ -> false + | Types.Named n when not (List.mem n seen) -> + let seen = n :: seen in + let field (fl : Tast.field) = dyn_behind_pointer p seen fl.Tast.fty in + (match List.find_opt (fun (s : Tast.structure) -> s.Tast.sname = n) + p.Tast.structs with + | Some s -> List.exists field s.Tast.fields + | None -> + match List.find_opt (fun (u : Tast.data) -> u.Tast.dname = n) + p.Tast.datas with + | Some u -> + List.exists + (fun (c : Tast.variant) -> List.exists field c.Tast.vfields) + u.Tast.cases + | None -> + match List.find_opt (fun (u : Tast.structure) -> u.Tast.sname = n) + p.Tast.unions with + | Some u -> List.exists field u.Tast.fields | None -> false) | _ -> false @@ -7483,8 +7528,14 @@ let rec dyn_words p seen (t : Types.t) = | Types.Dyn -> 1 | Types.Array (n, e) -> let w = dyn_words p seen e in + (* Out of range in either direction saturates. A negative length is + nonsense and the layout refuses it further down, but this arm has to + answer *something*, and the one thing it must not answer is a small + number: [Int64.to_int (-1L) * w] is negative, which reads as under the + cap and is how the overflow above got through in the first place. *) if w = 0 then 0 - else if Int64.compare n (Int64.of_int (desc_offsets_max + 1)) > 0 then + else if Int64.compare n 0L < 0 + || Int64.compare n (Int64.of_int (desc_offsets_max + 1)) > 0 then desc_offsets_max + 1 else sat (Int64.to_int n * w) | Types.Named nm when not (List.mem nm seen) -> @@ -7574,35 +7625,56 @@ let dyn_descriptors (p : Tast.program) = what (Types.to_string t) desc_offsets_max desc_offsets_max in (* The foreign boundary, which is the one place the note above admits an - honest hole. A [(Ptr S)] is fine when the storage is this compiler's, - because every slot, global and array that can hold an S is rooted with its - descriptor. Storage that came from C is not: nothing pushed a root for it, - nothing ever will, and the dyn word sitting in it is a live value the - collector cannot see. A bare dyn is already refused by name at this - boundary for a different reason — C has no way to ask what the word means - — and this is the same sentence one level down. + honest hole. Every slot, global and array this compiler hands out for a + type that holds dyn is rooted with its descriptor. Storage that came from + C is not: nothing pushed a root for it, nothing ever will, and a dyn word + sitting in it is a live value the collector cannot see and will free. A + bare dyn is already refused by name at this boundary for a different + reason — C has no way to ask what the word means — and this is the same + sentence at one remove. - Reported at [Loc.unknown] because a [Tast.extern] carries no location; the - Flan name and the C symbol are what a reader needs to find it, and both - are in the message. *) + The rule is about *ownership* and not about shape, so the two directions + are asked different questions and the answer to "is a (Ptr S) allowed" is + "which way is it going": + + - A return, and anything reachable from it however many pointers deep, is + C's storage. [(Ptr S)], [(Ptr (Ptr S))] and [(Ptr [S])] are all refused, + and the last two are the ones a one-level check missed — following a + pointer is exactly what [dyn_anywhere] stops doing, which is right for + a Flan type and wrong here. + - A parameter's outermost level is Flan's. The compiler passes the address + of a *place*, and a place is a frame slot, a global or an array inside + one — rooted with its descriptor and marked for the whole call. So + [(Ptr S)] and [[S]] as parameters are ordinary borrows and stay + writable, which is what a read-only C inspector wants and what + shim.ml's own advice tells people to write. Below that level the + storage is C's again: a [(Ptr (Ptr S))] parameter is an out-parameter, + and what C writes into it is a pointer of C's own. *) List.iter (fun (e : Tast.extern) -> - let across what (t : Types.t) = - match t with - | Types.Ptr pointee when dyn_anywhere p [] pointee -> - Loc.failk "check/dyn-descriptor" Loc.unknown - "%s of %s (the C symbol %s) is %s, and %s holds a dyn. What C \ - hands back points at storage this compiler never rooted, so the \ - collector cannot mark that word and will free what it names — \ - pass the fields across at written types instead" - what e.Tast.ename e.Tast.esym (Types.to_string t) - (Types.to_string pointee) - | _ -> () + let refuse what (t : Types.t) why = + Loc.failk "check/dyn-descriptor" e.Tast.eloc + "%s of %s (the C symbol %s) is %s, and a dyn is reachable through \ + it. %s, so the collector cannot mark that word and will free what \ + it names — pass the fields across at written types instead" + what e.Tast.ename e.Tast.esym (Types.to_string t) why + in + (* One level in, because that level is the compiler's own: what a + foreign parameter of pointer or slice type receives is the address + of a place. Below it the question is [dyn_behind_pointer]'s again. *) + let below (t : Types.t) = + match t with Types.Ptr e | Types.Slice e -> e | t -> t in List.iteri - (fun i t -> across (Printf.sprintf "parameter %d" (i + 1)) t) + (fun i t -> + if dyn_behind_pointer p [] (below t) then + refuse (Printf.sprintf "parameter %d" (i + 1)) t + "The outermost level is this compiler's own storage and is \ + rooted, but what lies below it is C's and nothing rooted that") e.Tast.eparams; - across "the return type" e.Tast.eret) + if dyn_through p [] e.Tast.eret then + refuse "the return type" e.Tast.eret + "What C hands back points at storage this compiler never rooted") p.Tast.externs; List.iter (fun (g : Tast.global) -> @@ -7710,7 +7782,12 @@ let build_program ~keep_going (decls : Ast.decl list) : Tast.program * env = Hashtbl.fold (fun name esym acc -> let eparams, eret = Hashtbl.find env.fns name in - { Tast.ename = name; esym; eparams; eret } :: acc) + let eloc = + match Hashtbl.find_opt env.extern_locs name with + | Some l -> l + | None -> Loc.unknown + in + { Tast.ename = name; esym; eparams; eret; eloc } :: acc) env.externs [] |> List.sort (fun (a : Tast.extern) b -> String.compare a.Tast.esym b.Tast.esym) in diff --git a/lib/dev.ml b/lib/dev.ml index 8ab51e6..a3bba1a 100644 --- a/lib/dev.ml +++ b/lib/dev.ml @@ -1915,7 +1915,7 @@ let type_of_spelling t spelling : (Types.t, string) result = let addr_extern : Tast.extern = { Tast.ename = "flan/dev-addr"; esym = "flan_dev_reg_addr"; eparams = [ Types.Int Types.I64 ]; - eret = Types.Ptr (Types.Int Types.U8) } + eret = Types.Ptr (Types.Int Types.U8); eloc = Loc.unknown } (* Renders the value [(Ptr ty)] holding [addr], in the program. diff --git a/lib/session.ml b/lib/session.ml index 8fe6e1c..a724f25 100644 --- a/lib/session.ml +++ b/lib/session.ml @@ -733,8 +733,10 @@ let emit_u64 = { ename = "flan/dev-emit-u64"; ety = Types.Int Types.U64 } let emit_f64 = { ename = "flan/dev-emit-f64"; ety = Types.Float Types.F64 } let externs : Tast.extern list = + (* [Loc.unknown]: these are the session's own, built here and never written + in a source file, so there is no [declare] for a refusal to point at. *) let one e sym = { Tast.ename = e.ename; esym = sym; eparams = [ e.ety ]; - eret = Types.Unit } in + eret = Types.Unit; eloc = Loc.unknown } in [ one emit_bytes "flan_dev_emit"; one emit_str "flan_dev_emit_str"; one emit_i64 "flan_dev_emit_i64"; @@ -747,11 +749,11 @@ let externs : Tast.extern list = is. See [render_locals]. *) { Tast.ename = "flan/dev-slot"; esym = "flan_agent_frame_slot"; eparams = [ Types.Int Types.I64; Types.Int Types.I64 ]; - eret = Types.Ptr (Types.Int Types.U8) }; + eret = Types.Ptr (Types.Int Types.U8); eloc = Loc.unknown }; { Tast.ename = "flan/dev-begin"; esym = "flan_dev_result_begin"; - eparams = []; eret = Types.Unit }; + eparams = []; eret = Types.Unit; eloc = Loc.unknown }; { Tast.ename = "flan/dev-end"; esym = "flan_dev_result_end"; - eparams = []; eret = Types.Unit }; + eparams = []; eret = Types.Unit; eloc = Loc.unknown }; (* The allocation registry's two questions about an address. Both take a [(Ptr u8)] and every pointer is cast to it: the registry is asked whether a *byte* is inside a block it knows, and the type at the far @@ -768,10 +770,10 @@ let externs : Tast.extern list = never saw. *) { Tast.ename = "flan/reg-live"; esym = "flan_dev_reg_live"; eparams = [ Types.Ptr (Types.Int Types.U8) ]; - eret = Types.Int Types.I32 }; + eret = Types.Int Types.I32; eloc = Loc.unknown }; { Tast.ename = "flan/reg-emit"; esym = "flan_dev_reg_emit"; eparams = [ Types.Ptr (Types.Int Types.U8) ]; - eret = Types.Int Types.I32 } ] + eret = Types.Int Types.I32; eloc = Loc.unknown } ] (* The REPL's emitter. Each piece is one extern call: the dev runtime already has a renderer per scalar, and [flan_dev_emit_str] already quotes and diff --git a/lib/tast.ml b/lib/tast.ml index 12b85fa..6824a97 100644 --- a/lib/tast.ml +++ b/lib/tast.ml @@ -310,6 +310,10 @@ type global = { type extern = { ename : string; (* the Flan name, e.g. rl/init-window *) esym : string; (* the C symbol *) + (* Where the [declare] was written. Carried so a refusal over a foreign + signature can point at it rather than at , which is what the + dyn boundary check had to do before this field existed. *) + eloc : Loc.t; eparams : Types.t list; eret : Types.t; } diff --git a/test/test_flan.ml b/test/test_flan.ml index 1a97bc8..d530b2e 100644 --- a/test/test_flan.ml +++ b/test/test_flan.ml @@ -948,6 +948,14 @@ let () = under the cap, the declaration was accepted, and the emitter then sat building the offset list until something killed it. The count is saturated now. *) + (* And the other end of the same arm: negative rather than enormous. It + reaches the multiplication as a small number, which is exactly what the + cap must not be handed. *) + rejects_check "a negative array length" + "(defstruct S [x dyn])\n\ + (defvar neg [-1 S])\n\ + (defn main [] i32 0)" + ~needle:"the most this compiler will write out"; rejects_check "an array length that overflows the flattened count" "(defstruct S [x dyn])\n\ (defvar big [4611686018427387904 S])\n\ @@ -959,14 +967,52 @@ let () = "(defstruct Cond [why dyn])\n\ (defn f [v (Vec (Ptr Cond))] i32 0)\n\ (defn main [] i32 0)"; - (* The one honest hole, named at the boundary where it opens. Storage C - hands back was never rooted and never will be, so a dyn word in it is a - live value the collector cannot see. *) - rejects_check "a pointer to a dyn-bearing struct crossing to C" + (* The one honest hole, named at the boundary where it opens — and it is a + question about *ownership*, not about shape, so the two directions get + asked different things. + + A return, and everything reachable from it however many pointers deep, is + C's storage. All three shapes, because a check that followed one pointer + and stopped let the other two through: each of them stores a dyn into C + memory and reads it back after a collection, and each is a + heap-use-after-free in flan_dyn_tag under ASan. *) + rejects_check "a pointer to a dyn-bearing struct returned from C" "(defstruct S [x dyn])\n\ - (declare take [p (Ptr S)] () \"c_take\")\n\ + (declare grab [] (Ptr S) \"c_grab\")\n\ (defn main [] i32 0)" ~needle:"storage this compiler never rooted"; + rejects_check "a pointer to a pointer to one, returned from C" + "(defstruct S [x dyn])\n\ + (declare grab [] (Ptr (Ptr S)) \"c_grab\")\n\ + (defn main [] i32 0)" + ~needle:"storage this compiler never rooted"; + (* The shape shim.ml's own advice tells people to write for an aggregate + result, which is what made this one worth having a test of its own. *) + rejects_check "a pointer to a slice of them, returned from C" + "(defstruct S [x dyn])\n\ + (declare grab [] (Ptr [S]) \"c_grab\")\n\ + (defn main [] i32 0)" + ~needle:"storage this compiler never rooted"; + (* And an out-parameter, which is a return wearing a parameter's clothes: + the cell is this compiler's, the pointer C writes into it is C's. *) + rejects_check "an out-parameter handing back a pointer to one" + "(defstruct S [x dyn])\n\ + (declare out [p (Ptr (Ptr S))] () \"c_out\")\n\ + (defn main [] i32 0)" + ~needle:"what lies below it is C's"; + (* The other direction stays writable, and this is the half a shape-only + rule got wrong. A foreign parameter receives the address of a *place* — + a frame slot, a global, an array inside one — and every one of those is + rooted with its descriptor and marked for the whole call. So the + read-only borrow and the slice argument are ordinary and allowed. *) + accepts "a pointer to a dyn-bearing struct passed to C" + "(defstruct S [x dyn])\n\ + (declare inspect [p (Ptr S)] () \"c_inspect\")\n\ + (defn main [] i32 0)"; + accepts "a slice of them passed to C" + "(defstruct S [x dyn])\n\ + (declare take [s [S]] () \"c_take\")\n\ + (defn main [] i32 0)"; rejects_check "a dyn field under an Option" "(defstruct S [x dyn])\n\ (defn f [] (Option S) None)\n\