JosephFerano/flan
1
0
Fork 0
Code Issues Pull Requests Packages Projects Releases Wiki Activity

The foreign boundary is about ownership, and it was reading shape

Browse Source 
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 <unknown>: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.
This commit is contained in:
Joseph Ferano 2026-09-19 23:02:26 +07:00
parent 27b672a3d2
commit a1111f7b3c
5 changed files with 181 additions and 52 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

157
lib/check.ml
View File

@ -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

2
lib/dev.ml
View File

@ -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.

14
lib/session.ml
View File

@ -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

4
lib/tast.ml
View File

@ -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 <unknown>, which is what the
dyn boundary check had to do before this field existed. *)
eloc : Loc.t;
eparams : Types.t list;
eret : Types.t;
}

56
test/test_flan.ml
View File

@ -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\