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

A frame address stored into a global's field, array or Vec element, or pushed or put into a global container is refused with a fix that names no wrong type, and the sanitizer sweep builds at -O0 so a read of a returned frame reports

Browse Source
This commit is contained in:
Joseph Ferano 2026-09-25 21:18:48 +07:00
parent 4fa11f6360
commit ab5fe36a48
3 changed files with 92 additions and 22 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

66
lib/check.ml
View File

@ -3585,17 +3585,33 @@ let refuse_frame_escapes (f : Tast.fn) =
most one binding [Let] in the function. *)
let binds = Hashtbl.create 16 in
let unstable = Hashtbl.create 16 in
(* A place a global owns, and so one that outlives every frame: the global,
a field or array element of it, or an element of a Vec it holds — the
Vec's block is the global's for as long as the global keeps it. A slice
is not stepped through: its storage may be anyone's. *)
let rec place_global = function
| Tast.Pglobal g -> Some g
| Tast.Pfield (t, _) -> expr_global t
| Tast.Pindex (t, idx) when all_array t.Tast.ty idx -> expr_global t
| Tast.Pindex (t, idx) when owned_levels t.Tast.ty idx -> expr_global t
(* [(set (at v i) x)] on a Vec is a store through the checked element
address [vec_at] builds. Any other pointer's target is not known to
be the global's. *)
| Tast.Pderef { Tast.e = Tast.Prim (Tast.Rt "flan_vec_at", t :: _); _ } ->
expr_global t
| _ -> None
and expr_global (e : Tast.expr) =
match e.Tast.e with
| Tast.Global g -> Some g
| Tast.Field (t, _) -> expr_global t
| Tast.Prim (Tast.At, t :: idx) when all_array t.Tast.ty idx -> expr_global t
| Tast.Prim (Tast.At, t :: idx) when owned_levels t.Tast.ty idx ->
expr_global t
| _ -> None
and owned_levels ty = function
| [] -> true
| _ :: rest ->
(match ty with
| Types.Array (_, el) | Types.Vec el -> owned_levels el rest
| _ -> false)
(* [(at a i j)] is one node carrying every index; each level stepped must
be an array for the element to be inside [a]'s own bytes. *)
and all_array ty = function
@ -3765,24 +3781,46 @@ let refuse_frame_escapes (f : Tast.fn) =
^ ", instead of its address: drop the addr"))
(escapes 0 e)
in
(* Only a store into the global itself can be fixed by changing the
global's type; for a field, an element or a push, the value's type
belongs to something else. *)
let stored ~bare g v =
Option.iter
(fail ~verb:"stores" ~target:(" into the global " ^ g)
~fix_slice:(fun c ->
"Store a copy that outlives the frame: " ^ c
^ ", which puts the elements in the context allocator")
~fix_addr:(fun t ->
if bare then
"Store the value instead: declare " ^ g ^ " as " ^ t
^ " and drop the addr"
else "Store the value instead of its address"))
(escapes 0 v)
in
let returns = not (Types.equal f.Tast.ret Types.Unit) in
List.iter
(Tast.walk (fun (e : Tast.expr) ->
match e.Tast.e with
| Tast.Return (Some v) when returns -> tails v
| Tast.Set (p, v) when not (String.equal f.Tast.name "main") ->
(match place_global p with
| Some g ->
Option.iter
(fail ~verb:"stores" ~target:(" into the global " ^ g)
~fix_slice:(fun c ->
"Store a copy that outlives the frame: " ^ c
^ ", which puts the elements in the context allocator")
~fix_addr:(fun t ->
"Store the value instead: declare " ^ g ^ " as " ^ t
^ " and drop the addr"))
(escapes 0 v)
| _ -> ())
Option.iter
(fun g ->
stored ~bare:(match p with Tast.Pglobal _ -> true | _ -> false)
g v)
(place_global p)
(* A push or put into a container a global owns: the element was
bound to a slot first, and its address is what the call takes. *)
| Tast.Prim (Tast.Rt ("flan_vec_push" | "flan_map_put"), target :: rest)
when not (String.equal f.Tast.name "main") ->
Option.iter
(fun g ->
List.iter
(fun (a : Tast.expr) ->
match a.Tast.e with
| Tast.Prim (Tast.AddrOf, [ v ]) -> stored ~bare:false g v
| _ -> ())
rest)
(expr_global target)
| _ -> ()))
f.Tast.body;
if returns then

23
test/test_flan.ml
View File

@ -3405,6 +3405,29 @@ let () =
"(defonce g [i32]) \
(defn f [] () (let [a [1 2 3] b [4 5]] (set g (slice a)) (set g (slice b))))"
~needle:"f stores a slice of a into the global g";
rejects_check "a local's address into a global array's element"
"(defonce gs [2 (Ptr i32)]) \
(defn f [] () (let [x (i32 1)] (set (at gs 0) (addr x))))"
~needle:"Store the value instead of its address";
rejects_check "a local's address into a global struct's field"
"(defstruct Q [p (Ptr i32)]) (defonce gq Q) \
(defn f [] () (let [x (i32 1)] (set (.p gq) (addr x))))"
~needle:"f stores the address of x into the global gq";
rejects_check "a local's address into a global Vec's element"
"(defonce gv (Vec (Ptr i32))) \
(defn f [] () (let [x (i32 1)] (set (at gv 0) (addr x))))"
~needle:"f stores the address of x into the global gv";
rejects_check "a local's address pushed onto a global Vec"
"(defonce gv (Vec (Ptr i32))) \
(defn f [] () (let [x (i32 1)] (push gv (addr x))))"
~needle:"f stores the address of x into the global gv";
rejects_check "a local's address put into a global Map"
"(defonce gm (Map i32 (Ptr i32))) \
(defn f [] () (let [x (i32 1)] (put gm 1 (addr x))))"
~needle:"f stores the address of x into the global gm";
accepts "a pointer parameter pushed onto a global Vec"
"(defonce gv (Vec (Ptr i32))) \
(defn f [p (Ptr i32)] () (push gv p))";
rejects_check "the fix keeps the slice's bounds"
"(defn mk [a [4 i32]] [i32] (slice a 1 3))"
~needle:"(clone (slice a 1 3))";

25
test/test_sanitize.ml
View File

@ -64,7 +64,7 @@ let run exe args =
(try Sys.remove out with Sys_error _ -> ());
(code, text)
let compile ?(dev = false) ~sanitize ~checks path =
let compile ?(dev = false) ?(opt = "-O0") ~sanitize ~checks path =
let exe =
Filename.concat scratch
(Printf.sprintf "flan-san-%s%s-%s"
@ -73,10 +73,15 @@ let compile ?(dev = false) ~sanitize ~checks path =
(Filename.remove_extension (Filename.basename path)))
in
let p, csrcs, lflags = Test_support.linked ~dev path in
(* -O0 by default, both builds: detect_stack_use_after_return (see [env]) can only
report a read of a frame's variable that still has a stack slot. At -O2
the local is promoted to a register and the read folded to the value it
held, so a pointer into a returned frame reads nothing the fake stack
can poison. *)
ignore
(Build.executable
~opts:{ Build.default with checks; sanitize; dev } ~csrcs ~lflags p
~out:exe);
~opts:{ Build.default with checks; sanitize; dev; opt }
~csrcs ~lflags p ~out:exe);
exe
let contains = Test_support.contains
@ -107,6 +112,9 @@ let reported text = List.exists (contains text) markers
calc-me is here and is not in test/programs: it is the one string parser in
the corpus, which makes it the likeliest to push [scratch] or [escaped]
anywhere near their bounds. *)
(* temp-grow and condition-temp read text after a (free-temp) on purpose, to
show the dev poison, and a sanitized build reports exactly that read: they
stay out of this list. *)
let corpus =
[ (* bounds.flan selects its case from argv, and every case but 0 is one
that traps. Argument 0 is the in-bounds path — the last index of a
@ -327,7 +335,7 @@ let dyn_sweep () =
let p, csrcs, lflags = Test_support.linked path in
match
Build.executable
~opts:{ Build.default with Build.sanitize = true }
~opts:{ Build.default with Build.sanitize = true; opt = "-O0" }
~csrcs:(csrcs @ [ "dyn_ops.c" ]) ~lflags p ~out:exe
with
| exception Failure m -> fail "dyn: sanitized build: %s" m
@ -439,8 +447,8 @@ let dev_sweep () =
sanitized run must produce ASan's report and must NOT produce the
handler's line, and that is the assertion.
And it has to be built at -O0. At the sweep's -O2 a store through a null
pointer is undefined and need not fault — so a case that is about what happens
And it has to be built at -O0, as the sweep now is. At -O2 a store through
a null pointer is undefined and need not fault — so a case that is about what happens
on a fault has to be compiled where the fault happens. Same family as the
-O0/-O2 split [unchecked_controls] records for bounds.flan.
@ -592,7 +600,8 @@ let control ~expect_report ?(args = []) ~why name src =
wrong answer instead of touching a redzone. At -O0, with the load still in
the program, ASan reports it. That divergence is why [--sanitize] does not
force -O0 the way [--debug] does — the optimiser is half of what is being
measured. *)
measured — and why this one control is built at -O2 while the sweep is
not. *)
let unchecked_controls () =
let reports = [ "3"; "7"; "4" ] in
let silent =
@ -616,7 +625,7 @@ let unchecked_controls () =
here and now for a better reason. The trap itself is asserted in \
test_acceptance.ml" ]
in
match compile ~sanitize:true ~checks:false "programs/bounds.flan" with
match compile ~opt:"-O2" ~sanitize:true ~checks:false "programs/bounds.flan" with
| exception Failure m -> fail "unchecked bounds.flan: build: %s" m
| exe ->
List.iter