From a7e1208ee42ded5a578ae57694589a56159071be Mon Sep 17 00:00:00 2001 From: Joseph Ferano Date: Sat, 19 Sep 2026 04:32:15 +0700 Subject: [PATCH] A stopped x86 program says where it is, and what its frames hold The backend had a full dev story for everything except the one thing the break loop reads: emit.ml pushes a shadow-stack frame on entry to every body in a dev build and x86.ml pushed none, so an --x86 session answered backtrace, locals, inspect and globals with "this program was not built with --dev", which was false of it. emit_fn now builds the same four words runtime/flan_dev.c describes -- the previous head, a static descriptor, and a table of one address per slot, null until the binding that fills it has run. The push is emitted at the head of the body buffer rather than into the prologue's, because the prologue is where the incoming registers still hold the arguments and every instruction of it clobbers rax. The pop is one store at the epilogue label: this backend has one epilogue and a return, the body's tail and the transfer exit all arrive there, where emit.ml needs the same restore at five separate rets. Two decisions are taken from emit.ml rather than reasoned out again, so that the two dev builds answer a stopped frame identically. A function with no named slot gets no table and reports no slots -- there the gate buys mem2reg an alloca that does not escape, here it buys nothing but agreement, and agreement is the only thing the break loop can check. And the descriptor's bytes do not go through string_const: that counter is what decides whether an expression thunk's module may be unloaded, and counting a descriptor in it would pin every C-x C-e module's mapping for ever. The descriptors are the one constant this backend emits that holds an address, so they go in .data.rel.ro and not .rodata -- a relocation the loader applies needs a section it may write, and a redefinition module is such an object. Verified on an assembled module: R_X86_64_RELATIVE for the two pointers, flan_frame_head through the GOT, no TEXTREL. layout_ctx fills its globals table, which it never had to before. Reach's ref_fingerprint asks whether a name is a global, and with an empty table no name is one -- every frame would carry the hash of the empty set, the daemon would recompute the real one, and the globals section would refuse a body nobody had touched while its locals still read. Release builds gain nothing: all of it is behind md.dev, and three corpus programs emit byte-identical assembly before and after. The new coverage stands up an --x86 daemon on dev-locals.flan and asks the four questions, against the values the LLVM block above asserts of that same program -- the claim is that the answers are the same and not merely plausible. The existing --x86 two-process daemon gains one more: a backtrace through a redefined body, which reports the installed body's own file, since that descriptor travels in the module and a frame pointing at the host's would name the body it replaced. --- lib/x86.ml | 205 +++++++++++++++++++++++++++++++++++++++++++++-- test/test_dev.ml | 187 ++++++++++++++++++++++++++++++++++++++++++ 2 files changed, 386 insertions(+), 6 deletions(-) diff --git a/lib/x86.ml b/lib/x86.ml index 923d591..516ef08 100644 --- a/lib/x86.ml +++ b/lib/x86.ml @@ -448,8 +448,18 @@ let layout_ctx ~checks ~dev (p : Tast.program) : Emit.m = p.Tast.datas; List.iter (fun (u : Tast.structure) -> Hashtbl.replace unions u.Tast.sname u) p.Tast.unions; + (* The globals table is filled and not left empty, which it was for as long + as nothing here asked a question about a name. [Reach.ref_fingerprint] + does: it hashes the set of *globals* a body names, and with an empty table + no name is a global, so every frame descriptor would carry the hash of the + empty set while the daemon recomputes it against the real one. The frames + would then all read as superseded and the break loop would refuse the + locals of a body nobody had touched. *) + let globals = Hashtbl.create 16 in + List.iter (fun (g : Tast.global) -> Hashtbl.replace globals g.Tast.gname g.Tast.gty) + p.Tast.globals; { Emit.out = Buffer.create 1; strs = Buffer.create 1; structs; datas; unions; - globals = Hashtbl.create 1; externs = Hashtbl.create 1; checks; + globals; externs = Hashtbl.create 1; checks; dev; known = (fun _ -> true); dbg = None; sanitize = false; nstr = 0; nfi = 0 } @@ -616,6 +626,22 @@ type fnctx = { mutable xfer_off : int; (* the incoming transfer channel pointer *) mutable sret_off : int; (* where the hidden return pointer was put *) mutable retval : int; (* the scalar return value's temporary *) + (* The shadow-stack record this function pushes, in a dev build: three words + at [rbp+dframe], holding the previous head, the static description, and + the slot table. [None] in a release build, where there is no record and + the epilogue below restores nothing. *) + mutable dframe : int option; + (* Where a dev build records each named slot's address, so that a stopped + frame's locals can be read: one word per Tast slot at [rbp+dslotv]. [None] + in a release build and in a function with no named slot at all — the same + gate [emit.ml] applies, and for a reason that is LLVM's rather than ours + (an alloca whose address escapes stops being promotable). Keeping the gate + anyway is what makes the two backends' frames answer identically, which is + the only thing the break loop can check. *) + mutable dslotv : int option; + (* [fn.snames], carried so [bind_slot] can ask whether a slot has a name to + show without the whole [Tast.fn] being threaded to every binding site. *) + snames : string option array; mutable frame : int; (* bytes currently allocated below rbp *) mutable maxframe : int; mutable outgoing : int; (* bytes the widest call needs for stack args *) @@ -936,6 +962,71 @@ let float_const f (x : float) ~f64 = (Printf.sprintf "\t.align 4\n%s:\n\t.long 0x%lx\n" l (Int32.bits_of_float x)); l +(* ── The shadow stack's descriptors ──────────────────────────────────── *) + +(* One [flan_fninfo] (runtime/flan_dev.c) per function in a dev build: the + name and the location as bytes and lengths, how many slots the frame has, + and the two fingerprints the daemon compares a frame against. Static data — + nothing about a function changes between two calls to it — so the record a + call pushes is three words and points at this. + + Not through [string_const], and that is the whole reason this has its own + emitter rather than borrowing that one. [string_const] bumps [md.nstr], + which is the test [redefinition] applies before it lets an expression + thunk's module say nothing points into it: a literal in the image may be + held by the program afterwards, so a module with one keeps its mapping. A + descriptor is not held — the frames naming it were popped on the way out and + the break loop copies the bytes it shows. Counting these there would stop + every C-x C-e module from ever being unloaded, which is [emit.ml]'s [m.nfi] + comment and the same trap on this side. + + The bytes carry no NUL and are not meant to: every reader takes the length + beside the pointer. *) +let fi_bytes f s = + let l = rodata_label f in + Buffer.add_string f.rodata (Printf.sprintf "\t.align 1\n%s:\n" l); + if String.length s > 0 then + Buffer.add_string f.rodata (Printf.sprintf "\t.byte %s\n" (escape_bytes s)); + l, String.length s + +(* [.data.rel.ro] and not [.rodata], which every other constant here goes in. + This is the only constant this backend emits that holds an *address*, and an + address in a shared object is a relocation the loader applies at load time — + so the section has to be one the loader may write. A redefinition module is + exactly such an object. The section is switched back afterwards because the + caller's buffer is emitted inside [.rodata] and everything after this in it + belongs there. *) +let fninfo f (fn : Tast.fn) ~nslots = + let nlbl, nlen = fi_bytes f fn.Tast.name in + let llbl, llen = fi_bytes f (Loc.to_string fn.Tast.floc) in + let l = rodata_label f in + Buffer.add_string f.rodata + (Printf.sprintf + "\t.section\t.data.rel.ro,\"aw\"\n\t.align 8\n%s:\n\ + \t.quad\t%s\n\t.quad\t%d\n\t.quad\t%s\n\t.quad\t%d\n\ + \t.long\t%d\n\t.long\t%d\n\t.long\t%d\n\t.long\t0\n\ + \t.section\t.rodata\n" + l nlbl nlen llbl llen nslots (Emit.slot_fingerprint fn) + (Reach.ref_fingerprint ~is_global:(Hashtbl.mem f.md.Emit.globals) fn)); + l + +(* The store that says "this slot is bound now", and it is the address rather + than a flag for [emit.ml]'s reason: the reader needs the address anyway, so + one store carries both facts, and a slot the control flow has not reached + reads as null rather than as a plausible value at an address nobody wrote. + + rax is free at every site that calls this — each one has just finished + moving a value into the slot, and nothing in this backend is live in a + register across a statement. *) +let bind_slot f i = + match f.dslotv with + | None -> () + | Some sv -> + if i < Array.length f.snames && f.snames.(i) <> None then begin + lea f.b ~dst:rax ~mm:(Frame f.slots.(i)); + store_int f.b ~src:rax ~mm:(Frame (sv + (8 * i))) ~size:8 + end + (* ── Locations ───────────────────────────────────────────────────────── *) (* Where a value lives. Every value in this backend lives in memory, so the @@ -1476,7 +1567,8 @@ and lower_at f (e : Tast.expr) (dst : loc) : unit = | Tast.Let (bs, body) -> List.iter (fun (slot, (v : Tast.expr)) -> - scoped f (fun () -> lower f v (Lf f.slots.(slot)))) + scoped f (fun () -> lower f v (Lf f.slots.(slot))); + bind_slot f slot) bs; block f body dst t | Tast.If (c, a, b) -> @@ -1847,7 +1939,8 @@ and emit_restart_case f clauses body dst t = List.iteri (fun i (slot_i, ty) -> move f ~dst:(Lf f.slots.(slot_i)) - ~src:(Lp (bufp, List.nth offs i)) ty) + ~src:(Lp (bufp, List.nth offs i)) ty; + bind_slot f slot_i) c.Tast.rparams); scoped f (fun () -> block f c.Tast.rbody dst t); jmp_lbl f.b ld; @@ -2045,7 +2138,8 @@ and emit_match f (scrut : Tast.expr) (arms : Tast.arm list) dst t = let src, fty = bind_at (match a.Tast.acase with Some c -> c | None -> "") k in - move f ~dst:(Lf f.slots.(slot)) ~src fty) + move f ~dst:(Lf f.slots.(slot)) ~src fty; + bind_slot f slot) a.Tast.binds; block f a.Tast.abody dst t; jmp_lbl f.b lend; @@ -2935,7 +3029,8 @@ let where_from = function | Istk d -> Printf.sprintf "from the caller's stack, at rbp+0x%x" d let frame_map (md : Emit.m) (fn : Tast.fn) ~slots ~fixed ~total ~outgoing - ~xfer_off ~sret_off ~retval ~sret ~sret_at ~param_at ~xfer_at = + ~xfer_off ~sret_off ~retval ~dframe ~dslotv ~sret ~sret_at ~param_at + ~xfer_at = let b = Buffer.create 1024 in let line s = Buffer.add_string b (if s = "" then "#\n" else "# " ^ s ^ "\n") in (* The prose paragraphs wrap; the table below does not, because its columns @@ -3053,6 +3148,18 @@ let frame_map (md : Emit.m) (fn : Tast.fn) ~slots ~fixed ~total ~outgoing if (not sret) && not (is_void fn.Tast.ret) then row retval "" (Types.to_string fn.Tast.ret) "the return value the epilogue loads"; + (* Present in a dev build and absent from a release one, and the map says + which build this is by saying nothing when there is nothing there. *) + (match dframe with + | Some off -> + row off "" "ptr[3]" + "the shadow-stack record: the previous head, the description, the slots" + | None -> ()); + (match dslotv with + | Some off -> + row off "" "ptr[]" + "one address per slot, null until the binding that fills it has run" + | None -> ()); para (Printf.sprintf "Everything below -0x%x is a temporary. They are bump-allocated and reclaimed \ at the end of the form that made them, so a later form reuses the bytes and \ @@ -3069,6 +3176,7 @@ let emit_fn (md : Emit.m) ~externs ~fns ?(ext = fun _ -> false) { b; md; fnname = fn.Tast.name; retlbl = ""; fret = fn.Tast.ret; slots = Array.make nslots 0; xfer_off = 0; sret_off = 0; retval = 0; + dframe = None; dslotv = None; snames = fn.Tast.snames; frame = 0; maxframe = 0; outgoing = 0; loops = []; pads = []; xfer_lbl = ""; unwound = false; rodata = Buffer.create 64; externs; fns; ext; slot; dw; @@ -3111,6 +3219,24 @@ let emit_fn (md : Emit.m) ~externs ~fns ?(ext = fun _ -> false) f.xfer_off <- ptmp f; if sret then f.sret_off <- ptmp f; if (not sret) && not (is_void fn.Tast.ret) then f.retval <- tmp f fn.Tast.ret; + (* The shadow stack's storage, in a dev build and nowhere else: three words + for the record and one per slot for the table. Allocated here, beside the + channel and the return temporary, so that they sit above [fixed] and the + frame map has somewhere to name them; and allocated outside every [scoped] + so nothing below reuses the bytes. + + Only a function with at least one *named* slot gets a table, which is the + gate [emit.ml] applies. There it buys an optimisation — an alloca whose + address escapes is one mem2reg cannot promote — and nothing here promotes + anything, so on this side it buys only the stores. It is kept because the + two backends have to answer a stopped frame identically: a function whose + every slot the compiler invented reports no slots on LLVM, and a listing + that differed by backend is the one thing the break loop cannot check. *) + if md.Emit.dev then begin + if nslots > 0 && Array.exists (fun n -> n <> None) fn.Tast.snames then + f.dslotv <- Some (alloc f (8 * nslots) 8); + f.dframe <- Some (alloc f 24 8) + end; f.retlbl <- new_label f "ret"; f.xfer_lbl <- new_label f "xfer"; (* Where the named part of the frame ends and the nameless part begins. Read @@ -3132,6 +3258,55 @@ let emit_fn (md : Emit.m) ~externs ~fns ?(ext = fun _ -> false) | _ -> None) fn.Tast.params param_at in + (* The shadow stack's push, and the pop is in the epilogue. plan.org has had + *Frames: shadow stack* in the dev column since the beginning; [emit.ml] + builds the same four words on the LLVM side and this is the x86 one, down + to which fields are written and when, so that a break loop cannot tell + which backend it stopped. + + Inline rather than a call, for [emit.ml]'s reason: this is on every call in + a dev build, and a call made to record a call would be most of what it + costs. What it does cost here is a handful of stores — the table's zeroing, + three words of record, one head store, and one [lea]+store per named + parameter. + + Emitted into the body buffer rather than the prologue's, and that is not a + detail: the prologue is where the incoming registers still hold the + arguments, and every instruction below clobbers rax. The body buffer's + first byte is the first point at which they are all safely in the frame. + + One push per [emit_fn] and no more. [emit_main], [emit_globals_init] and + [flan_reload_install] build their context by hand and push nothing, which + is what [emit.ml] does too: they are C's frames, not the program's, and a + backtrace that named them would be naming the runtime. *) + (match f.dframe with + | None -> () + | Some fr -> + if ann then set_ind f.b ""; + note f + "The shadow stack's push — runtime/flan_dev.c. Dev builds only, and it is what \ + lets a stopped program say where it is. The pop is the first thing in the \ + epilogue, so a transfer out of this frame pops it too."; + (* Every entry, not only the named ones: "null means not bound" has to + hold at every index, or a reader has to know which indices it may + trust, and that is a second thing to keep in step. *) + (match f.dslotv with + | Some sv -> zero_frame f ~dst:sv (8 * nslots) + | None -> ()); + let head = sym_loc f "flan_frame_head" in + load_int f.b ~dst:rax ~mm:(lmem f head ~scratch:r11) ~size:8 ~signed:false; + store_int f.b ~src:rax ~mm:(Frame fr) ~size:8; + addr_into f ~reg:rax (Lg (fninfo f fn ~nslots:(if f.dslotv = None then 0 else nslots), 0)); + store_int f.b ~src:rax ~mm:(Frame (fr + 8)) ~size:8; + (match f.dslotv with + | Some sv -> lea f.b ~dst:rax ~mm:(Frame sv) + | None -> xor_rr f.b ~dst:rax ~src:rax); + store_int f.b ~src:rax ~mm:(Frame (fr + 16)) ~size:8; + lea f.b ~dst:rax ~mm:(Frame fr); + store_int f.b ~src:rax ~mm:(lmem f head ~scratch:r11) ~size:8; + (* The parameters are bound before the body starts, so they are recorded + here rather than at a binding site there is none of. *) + List.iteri (fun i _ -> bind_slot f i) fn.Tast.params); (* The body. Lowered into its own buffer, because the prologue's [sub] needs a frame size only the body can decide, and every relocation this backend emits is an assembler expression — so nothing has to be patched. *) @@ -3292,6 +3467,21 @@ let emit_fn (md : Emit.m) ~externs ~fns ?(ext = fun _ -> false) "The epilogue, and every return and every transfer out of this frame arrives here, \ so the frame is torn down once."; lbl f.b f.retlbl; + (* The shadow stack's pop, and it is one store because this backend has one + epilogue: a [return], the fall through the body's tail, and the transfer + exit all arrive at this label, so the head is restored on the unwinding + path as well as on the normal one. [emit.ml] needs the same restore at + five separate [ret]s and routes them through its [ret] for exactly that + reason — a pop written only on the normal path leaves a dead frame behind + every handled condition, and the next backtrace is a lie. + + Before the return value is loaded, because it is loaded into rax. *) + (match f.dframe with + | None -> () + | Some fr -> + load_int f.b ~dst:rax ~mm:(Frame fr) ~size:8 ~signed:false; + store_int f.b ~src:rax + ~mm:(lmem f (sym_loc f "flan_frame_head") ~scratch:r11) ~size:8); if sret then load_int f.b ~dst:rax ~mm:(Frame f.sret_off) ~size:8 ~signed:false else if not (is_void fn.Tast.ret) then load_scalar f ~reg:(if is_float fn.Tast.ret then xmm0 else rax) @@ -3307,7 +3497,8 @@ let emit_fn (md : Emit.m) ~externs ~fns ?(ext = fun _ -> false) Buffer.add_string out (frame_map md fn ~slots:f.slots ~fixed ~total:(frame_bytes f) ~outgoing:f.outgoing ~xfer_off:f.xfer_off ~sret_off:f.sret_off - ~retval:f.retval ~sret ~sret_at ~param_at ~xfer_at); + ~retval:f.retval ~dframe:f.dframe ~dslotv:f.dslotv ~sret ~sret_at + ~param_at ~xfer_at); Buffer.add_string out (Printf.sprintf "\t.globl\t%s\n" sym); (* [emit.ml:2072] says this is load-bearing and it is: default visibility in a shared object is interposable, and that applies to taking the address @@ -3423,6 +3614,7 @@ let emit_globals_init ?(cfi = false) ?(ann = false) (md : Emit.m) ~externs ~fns let f = { b; md; fnname = ""; retlbl = new_label () "ginit"; fret = Types.Unit; slots = [||]; xfer_off = 0; sret_off = 0; retval = 0; + dframe = None; dslotv = None; snames = [||]; frame = 0; maxframe = 0; outgoing = 0; loops = []; pads = []; xfer_lbl = ""; unwound = false; rodata = Buffer.create 64; externs; fns; ext = (fun _ -> false); @@ -4088,6 +4280,7 @@ let redefinition ~checks ?(dev = true) ?(known = fun _ -> true) let f = { b = ib; md; fnname = ""; retlbl = new_label () "install"; fret = Types.Unit; slots = [||]; xfer_off = 0; sret_off = 0; retval = 0; + dframe = None; dslotv = None; snames = [||]; frame = 0; maxframe = 0; outgoing = 0; loops = []; pads = []; xfer_lbl = ""; unwound = false; rodata = Buffer.create 256; externs; fns = fnstbl; ext; slot; dw = None; diff --git a/test/test_dev.ml b/test/test_dev.ml index 4486060..cbe8dbe 100644 --- a/test/test_dev.ml +++ b/test/test_dev.ml @@ -4030,10 +4030,197 @@ let () = if status r <> "ok" then fail "x86 new name round trip: %s" (said r) else if value r <> "82" then fail "x86 (twice fresh) answered %S, so the registry lookups did not resolve" (value r); + (* And a backtrace *through* a redefined body, which is the one frame a + module has to get right on its own: the descriptor a body points at + travels in the object that body was compiled into, so a module that + pushed no frame would leave a gap where the redefinition ran, and one + that pointed at the host's descriptor would report the location of the + body it replaced. The installed body's own file is what says which + happened. Last in this block deliberately — it stops the program. *) + let r = + request c + "(:op \"eval\" :code \"(defn step [] i64 (let [n (+ ticks 1)] (error (Missing {.id 3})) n))\" :file \"/tmp/x86redef.flan\")" + in + if status r <> "ok" then fail "x86 redefined-body backtrace, install: %s" (said r) + else if not (await (fun () -> + match Wire.field (request c "(:op \"describe\")") "stopped" with + | Some { Form.v = Form.Sym "t"; _ } -> true + | _ -> false)) + then fail "the --x86 program never stopped in the redefined body" + else begin + let r = request c "(:op \"backtrace\")" in + let top = + match Wire.field r "frames" with + | Some { Form.v = Form.List ({ Form.v = Form.List + ({ Form.v = Form.Str n; _ } + :: { Form.v = Form.Str loc; _ } :: _); _ } + :: _); _ } -> Some (n, loc) + | _ -> None + in + match top with + | Some ("step", loc) when contains_sub loc "x86redef.flan" -> () + | Some (n, loc) -> fail "x86 backtrace through a redefined body: %s at %S" n loc + | None -> fail "x86 backtrace through a redefined body: %s" (said r) + end; ignore (request c "(:op \"close\")"); (try Unix.close c with Unix.Unix_error _ -> ()); (try ignore (Unix.waitpid [] xpid2) with Unix.Unix_error _ -> ()) end; + + (* ── The inspector, on the other backend ──────────────────────────── *) + + (* The break loop's four questions asked of an [--x86] host. They are the + ones that go through the shadow stack rather than through a module: the + frame chain gives the depth and the names, and the addresses in it are + what a render thunk reads the locals and the globals out of. Until + [X86.emit_fn] pushed a frame this daemon answered every one of them with + "this program was not built with --dev", which was false of it. + + [programs/dev-locals.flan] and not a fixture of its own, deliberately: + the LLVM block above asks these same questions of that same program, so + the two sets of answers can be read against each other, and what is + being claimed is that they are the *same* answers rather than merely + plausible ones. A backend the break loop can tell apart is a backend the + break loop cannot be trusted on. *) + let isock = tmp "x86locals.sock" and iout = tmp "x86locals.out" in + (try Sys.remove isock with Sys_error _ -> ()); + let ifd = + Unix.openfile iout [ Unix.O_WRONLY; Unix.O_CREAT; Unix.O_TRUNC ] 0o600 + in + let ipid = + Unix.create_process flan + [| flan; "dev"; "programs/dev-locals.flan"; "-s"; isock; "--x86" |] + Unix.stdin ifd Unix.stderr + in + Unix.close ifd; + if not (listening ~pid:ipid isock) then begin + fail "the --x86 inspector daemon %s (%S)" !listen_why + (In_channel.with_open_bin iout In_channel.input_all); + (try Unix.kill ipid Sys.sigkill with Unix.Unix_error _ -> ()) + end + else begin + let c = connect isock in + let said r = Option.value ~default:"" (Wire.string_field r "message") in + let stopped r = + match Wire.field r "stopped" with + | Some { Form.v = Form.Sym "t"; _ } -> true + | _ -> false + in + if not (await (fun () -> stopped (request c "(:op \"describe\")"))) then + fail "the --x86 inspector program never stopped" + else begin + (* The backtrace first, because everything below names a frame by the + index this listing gives. Two frames and not one: [main] called + [look], so a chain with only the innermost on it would mean the push + happened and the previous head was not saved. *) + let r = request c "(:op \"backtrace\")" in + let frames = + match Wire.field r "frames" with + | Some { Form.v = Form.List l; _ } -> + List.filter_map + (fun (e : Form.t) -> + match e.Form.v with + | Form.List ({ Form.v = Form.Str n; _ } + :: { Form.v = Form.Str loc; _ } + :: { Form.v = Form.Str origin; _ } :: _) -> + Some (n, loc, origin) + | _ -> None) + l + | _ -> [] + in + if status r <> "ok" then fail "x86 backtrace: %s" (said r) + else + (match frames with + | [ ("look", l0, "program"); ("main", _, "program") ] -> + (* The location travels in the frame's own descriptor, so a wrong + one is a descriptor built from the wrong function rather than a + cosmetic slip. *) + if not (contains_sub l0 "dev-locals.flan:14") then + fail "x86 backtrace put look at %S" l0 + | _ -> + fail "x86 backtrace: %s" + (String.concat ", " + (List.map (fun (n, _, o) -> n ^ "/" ^ o) frames))); + let triples r key = + match Wire.field r key with + | Some { Form.v = Form.List l; _ } -> + List.filter_map + (fun (e : Form.t) -> + match e.Form.v with + | Form.List ({ Form.v = Form.Str a; _ } + :: { Form.v = Form.Str b; _ } :: rest) -> + Some (a, b, + match rest with + | { Form.v = Form.Str c; _ } :: _ -> c + | _ -> "") + | _ -> None) + l + | _ -> [] + in + (* The locals of the stopped frame, and this is the claim the slot + table exists for: the values are the ones [look] was called with and + bound to, read at the addresses the frame recorded, under this + backend's own frame layout. A wrong address renders whatever those + bytes happen to be, so matching the LLVM listing exactly is the + check and a shape-only assertion would not be. *) + let r = request c "(:op \"locals\" :frame 0)" in + if status r <> "ok" then fail "x86 locals: %s" (said r) + else begin + let want = + [ ("n", "i64", "3"); + ("label", "string", "\"hello\""); + ("p", "Point", "(Point {.x 1.5 .y 2.5})"); + ("xs", "[3 i32]", "[ 10 20 30]"); + ("flag", "bool", "true") ] + in + let got = triples r "locals" in + if got <> want then + fail "x86 locals of the stopped frame: %s" + (String.concat ", " + (List.map (fun (n, ty, v) -> n ^ " " ^ ty ^ " = " ^ v) got)); + (* [after] is bound past the error, so nothing wrote its entry and it + is still the null the push stored. That null is the whole of how + "not bound yet" is told from "bound" on this side too — there is no + liveness analysis behind it — so a frame whose table were left + uninitialised would render this one from stack litter. *) + match List.filter (fun (n, _, _) -> n = "after") (triples r "refused") with + | [ (_, why, _) ] when why <> "" -> () + | _ -> + fail "x86: a slot bound after the error was not refused by name: %s" + (String.concat ", " + (List.map (fun (n, w, _) -> n ^ ": " ^ w) (triples r "refused"))) + end; + (* One slot by index, which is the inspector's own root rather than + [locals]' listing, and an aggregate for it: an x86 frame passes every + aggregate by pointer, so a struct is where a recorded address could + most easily be the caller's copy instead of this frame's. *) + let r = request c "(:op \"inspect\" :frame 0 :slot 2)" in + if status r <> "ok" then fail "x86 inspect: %s" (said r) + else if Wire.string_field r "value" <> Some "(Point {.x 1.5 .y 2.5})" then + fail "x86 inspect of slot 2 answered %S" + (Option.value ~default:"" (Wire.string_field r "value")); + (* And the globals, which are not in the frame at all -- they are found + through the same descriptor's fingerprint, and a frame whose + [refsig] disagreed with what the daemon recomputes would refuse + every one of them while the locals above still read. That is the + failure an empty globals table in [X86.layout_ctx] produces, and it + is why this question is asked here and not left to the LLVM block. *) + let r = request c "(:op \"globals\")" in + if status r <> "ok" then fail "x86 globals: %s" (said r) + else + (match triples r "globals" with + | [ ("ticks", "i64", v) ] when v <> "" -> () + | got -> + fail "x86 globals: %s" + (String.concat ", " + (List.map (fun (n, ty, v) -> n ^ " " ^ ty ^ " = " ^ v) got))) + end; + ignore (request c "(:op \"close\")"); + (try Unix.close c with Unix.Unix_error _ -> ()); + (try ignore (Unix.waitpid [] ipid) with Unix.Unix_error _ -> ()) + end; + List.iter (fun f -> try Sys.remove f with Sys_error _ -> ()) [ isock; iout ]; + (* And the *merged* daemon on this backend, which used to be refused by name and is the case the refusal was standing in for.