A redefinition carries its own handler clauses
The reload path had never seen a restart-case or a handler-bind: the acceptance table's dev build proves whole-program codegen with cells, but not Emit.redefinition, where the callees are declares or cell loads and the restart frame is an alloca in a module the process was not built with. Driving it found a hole step 1 left - a lifted clause was numbered by its position in the whole program's lifted list, so the name was neither stable against an unrelated handler-bind being added nor attributable to the function it came out of, and redefining a function that established a handler died in llc with an undefined value. A clause is now named after its parent - handler/step/0/Missing - and carries Tast.fn.fparent, which is what lets a redefinition module emit the clauses belonging to the bodies it is replacing and nothing else. They are hidden for the same reason a redefined body is: taking the address of an interposable symbol would resolve to the host's copy, so the module would install the very handler it was replacing. A clause is reached by address from its parent and from nowhere else, so it is kept out of the cell and registry machinery entirely rather than given a slot nobody uses. test_dev.ml now sends a third evaluation: step redefined to a restart-case whose frame is an alloca in the new module, whose guarded call goes through the host's cell, and whose transfer starts in a handler and crosses probe, which the host was compiled with. The transcript's fourth line is the clause's value.
This commit is contained in:
parent
7faab27ea2
commit
2fadf82e23
19
NEXT.md
19
NEXT.md
@ -998,6 +998,25 @@ Scope, each piece refused by name with its reason and a test on the reason:
|
|||||||
and located, rather than an unwind past everything. There is nowhere to
|
and located, rather than an unwind past everything. There is nowhere to
|
||||||
resume, so there is nothing else to do.
|
resume, so there is nothing else to do.
|
||||||
|
|
||||||
|
`flan_transfer_fail` covers the ordinary return path as well as the unwind one:
|
||||||
|
a defer that reaches an `invoke-restart` through a call traps either way, and
|
||||||
|
the message names the rule rather than the path, since the rule is the same.
|
||||||
|
|
||||||
|
**A lifted handler clause is named after the function it came out of** —
|
||||||
|
`handler/step/0/Missing` — and is emitted by a redefinition module alongside
|
||||||
|
the body it belongs to, hidden, for the same interposition reason the body is.
|
||||||
|
This was a hole step 1 left: the name used to be numbered by position in the
|
||||||
|
whole program's lifted list, so it was neither stable nor attributable, and a
|
||||||
|
redefinition of a function containing a `handler-bind` failed in `llc` with an
|
||||||
|
undefined value. A clause is reached by address from its parent's body and from
|
||||||
|
nowhere else, so it takes no cell and no registry slot.
|
||||||
|
|
||||||
|
`test/test_dev.ml` drives that path: a third evaluation redefines `step` to a
|
||||||
|
`restart-case` whose frame is an `alloca` in the newly loaded module, whose
|
||||||
|
guarded call goes through the host's cell, and whose transfer starts in a
|
||||||
|
handler and crosses `probe`, which the host was compiled with. Those three do
|
||||||
|
not meet anywhere else.
|
||||||
|
|
||||||
Two things found by writing it:
|
Two things found by writing it:
|
||||||
|
|
||||||
- **`{ ctx with in_handler = true }` was a latent bug.** `ctx.slots` and
|
- **`{ ctx with in_handler = true }` was a latent bug.** `ctx.slots` and
|
||||||
|
|||||||
32
lib/check.ml
32
lib/check.ml
@ -104,6 +104,11 @@ type ctx = {
|
|||||||
function's defers are already half run and the first transfer's target is
|
function's defers are already half run and the first transfer's target is
|
||||||
already in hand. Refused where it is written. *)
|
already in hand. Refused where it is written. *)
|
||||||
mutable in_defer : bool;
|
mutable in_defer : bool;
|
||||||
|
(* The function being checked, so a clause lifted out of it can be named
|
||||||
|
after it. The name has to be stable and has to say whose it is: a
|
||||||
|
redefinition module emits the clauses belonging to the bodies it is
|
||||||
|
replacing, and nothing else in the program can tell it which those are. *)
|
||||||
|
owner : string;
|
||||||
}
|
}
|
||||||
|
|
||||||
let fresh_slot ctx ty =
|
let fresh_slot ctx ty =
|
||||||
@ -552,7 +557,7 @@ and check_handler_bind ctx ?want loc clauses body =
|
|||||||
the enclosing one. *)
|
the enclosing one. *)
|
||||||
let hctx =
|
let hctx =
|
||||||
{ env = ctx.env; ret = Types.Unit; slots = 0; slot_tys = [];
|
{ env = ctx.env; ret = Types.Unit; slots = 0; slot_tys = [];
|
||||||
scope = []; defers = []; outer = ctx.scope; in_handler = true; in_frames = None; in_defer = false }
|
scope = []; defers = []; outer = ctx.scope; in_handler = true; in_frames = None; in_defer = false; owner = "<none>" }
|
||||||
in
|
in
|
||||||
(* The condition crosses as a pointer, because the handler runs while
|
(* The condition crosses as a pointer, because the handler runs while
|
||||||
the signalling frame is still alive and there is nothing to copy.
|
the signalling frame is still alive and there is nothing to copy.
|
||||||
@ -572,14 +577,22 @@ and check_handler_bind ctx ?want loc clauses body =
|
|||||||
(mk c.Ast.hloc (Types.Ptr ty) (Tast.Local pslot)))) ],
|
(mk c.Ast.hloc (Types.Ptr ty) (Tast.Local pslot)))) ],
|
||||||
hbody)) ]
|
hbody)) ]
|
||||||
in
|
in
|
||||||
let fname = Printf.sprintf "handler/%s/%d" name (type_id name land 0xffff) in
|
(* Named after the function it came out of, and numbered within it:
|
||||||
|
stable against an unrelated handler-bind being added elsewhere,
|
||||||
|
which an index into the whole program's lifted list would not be. *)
|
||||||
let fname =
|
let fname =
|
||||||
Printf.sprintf "%s/%d" fname (List.length ctx.env.lifted)
|
Printf.sprintf "handler/%s/%d/%s" ctx.owner
|
||||||
|
(List.length
|
||||||
|
(List.filter
|
||||||
|
(fun (l : Tast.fn) -> l.Tast.fparent = Some ctx.owner)
|
||||||
|
ctx.env.lifted))
|
||||||
|
name
|
||||||
in
|
in
|
||||||
ctx.env.lifted <-
|
ctx.env.lifted <-
|
||||||
{ Tast.name = fname; params = [ Types.Ptr ty ];
|
{ Tast.name = fname; params = [ Types.Ptr ty ];
|
||||||
slots = Array.of_list (List.rev hctx.slot_tys);
|
slots = Array.of_list (List.rev hctx.slot_tys);
|
||||||
ret = Types.Unit; body = hbody; fdefers = []; floc = c.Ast.hloc }
|
ret = Types.Unit; body = hbody; fdefers = [];
|
||||||
|
fparent = Some ctx.owner; floc = c.Ast.hloc }
|
||||||
:: ctx.env.lifted;
|
:: ctx.env.lifted;
|
||||||
{ Tast.htype = type_id name; hfn = fname })
|
{ Tast.htype = type_id name; hfn = fname })
|
||||||
clauses
|
clauses
|
||||||
@ -1361,7 +1374,7 @@ let collect env (decls : Ast.decl list) =
|
|||||||
run without swallowing it. *)
|
run without swallowing it. *)
|
||||||
let infer (_, v) =
|
let infer (_, v) =
|
||||||
(check { env; ret = Types.Unit; slots = 0; slot_tys = []; scope = []; defers = [];
|
(check { env; ret = Types.Unit; slots = 0; slot_tys = []; scope = []; defers = [];
|
||||||
outer = []; in_handler = false; in_frames = None; in_defer = false } v).Tast.ty
|
outer = []; in_handler = false; in_frames = None; in_defer = false; owner = "<none>" } v).Tast.ty
|
||||||
in
|
in
|
||||||
let pending = ref (List.rev !untyped) in
|
let pending = ref (List.rev !untyped) in
|
||||||
let rec settle () =
|
let rec settle () =
|
||||||
@ -1414,7 +1427,8 @@ let check_finite env =
|
|||||||
let check_fn env (fn : Ast.fn) : Tast.fn =
|
let check_fn env (fn : Ast.fn) : Tast.fn =
|
||||||
let params, ret = Hashtbl.find env.fns fn.Ast.name in
|
let params, ret = Hashtbl.find env.fns fn.Ast.name in
|
||||||
let ctx = { env; ret; slots = 0; slot_tys = []; scope = []; defers = [];
|
let ctx = { env; ret; slots = 0; slot_tys = []; scope = []; defers = [];
|
||||||
outer = []; in_handler = false; in_frames = None; in_defer = false } in
|
outer = []; in_handler = false; in_frames = None; in_defer = false;
|
||||||
|
owner = fn.Ast.name } in
|
||||||
List.iter2
|
List.iter2
|
||||||
(fun (p : Ast.field) ty ->
|
(fun (p : Ast.field) ty ->
|
||||||
if List.mem_assoc p.Ast.fname ctx.scope then
|
if List.mem_assoc p.Ast.fname ctx.scope then
|
||||||
@ -1484,11 +1498,11 @@ let check_fn env (fn : Ast.fn) : Tast.fn =
|
|||||||
slots = Array.of_list (List.rev ctx.slot_tys);
|
slots = Array.of_list (List.rev ctx.slot_tys);
|
||||||
(* The same defers again, for the transfer exit path §5 describes. The
|
(* The same defers again, for the transfer exit path §5 describes. The
|
||||||
normal path has them spliced into [body] above. *)
|
normal path has them spliced into [body] above. *)
|
||||||
ret; body; fdefers = ctx.defers; floc = fn.Ast.nloc }
|
ret; body; fdefers = ctx.defers; fparent = None; floc = fn.Ast.nloc }
|
||||||
|
|
||||||
let check_global env (d : Ast.decl) : Tast.global option =
|
let check_global env (d : Ast.decl) : Tast.global option =
|
||||||
let ctx () = { env; ret = Types.Unit; slots = 0; slot_tys = []; scope = []; defers = [];
|
let ctx () = { env; ret = Types.Unit; slots = 0; slot_tys = []; scope = []; defers = [];
|
||||||
outer = []; in_handler = false; in_frames = None; in_defer = false } in
|
outer = []; in_handler = false; in_frames = None; in_defer = false; owner = "<none>" } in
|
||||||
match d.Ast.d with
|
match d.Ast.d with
|
||||||
| Ast.Defvar (n, _, init) ->
|
| Ast.Defvar (n, _, init) ->
|
||||||
let ty, _ = Hashtbl.find env.globals n in
|
let ty, _ = Hashtbl.find env.globals n in
|
||||||
@ -1592,7 +1606,7 @@ let program (decls : Ast.decl list) : Tast.program = fst (program_with_env decls
|
|||||||
let expression env (e : Ast.expr) : Tast.expr * Types.t array =
|
let expression env (e : Ast.expr) : Tast.expr * Types.t array =
|
||||||
let ctx =
|
let ctx =
|
||||||
{ env; ret = Types.Unit; slots = 0; slot_tys = []; scope = []; defers = [];
|
{ env; ret = Types.Unit; slots = 0; slot_tys = []; scope = []; defers = [];
|
||||||
outer = []; in_handler = false; in_frames = None; in_defer = false }
|
outer = []; in_handler = false; in_frames = None; in_defer = false; owner = "<none>" }
|
||||||
in
|
in
|
||||||
let t = check ctx e in
|
let t = check ctx e in
|
||||||
(t, Array.of_list (List.rev ctx.slot_tys))
|
(t, Array.of_list (List.rev ctx.slot_tys))
|
||||||
|
|||||||
28
lib/emit.ml
28
lib/emit.ml
@ -1273,6 +1273,23 @@ let redefinition ?(checks = true) ?(dev = false) ?(known = fun _ -> true)
|
|||||||
| None -> failwith (Printf.sprintf "no such function: %s" name)
|
| None -> failwith (Printf.sprintf "no such function: %s" name)
|
||||||
in
|
in
|
||||||
let targets = List.map target fns in
|
let targets = List.map target fns in
|
||||||
|
(* A clause lifted out of one of these comes with it: its body may have
|
||||||
|
changed too, and it is reached by address from inside the module rather
|
||||||
|
than through a cell. Every other lifted clause is invisible here — it
|
||||||
|
needs no declaration, since nothing in this module names it. *)
|
||||||
|
let lifted =
|
||||||
|
List.filter
|
||||||
|
(fun (f : Tast.fn) ->
|
||||||
|
match f.Tast.fparent with
|
||||||
|
| Some p -> List.mem p fns
|
||||||
|
| None -> false)
|
||||||
|
p.Tast.fns
|
||||||
|
in
|
||||||
|
(* The rest of the program, as the cell and registry machinery below sees it.
|
||||||
|
A lifted clause has neither, so it must not appear in either. *)
|
||||||
|
let siblings =
|
||||||
|
List.filter (fun (f : Tast.fn) -> f.Tast.fparent = None) p.Tast.fns
|
||||||
|
in
|
||||||
let m = new_module ~checks ~dev ~known p in
|
let m = new_module ~checks ~dev ~known p in
|
||||||
(* A thunk the module runs itself is excluded from all of this: it is called
|
(* A thunk the module runs itself is excluded from all of this: it is called
|
||||||
directly by [flan_reload_call], so it needs no cell, must not be published
|
directly by [flan_reload_call], so it needs no cell, must not be published
|
||||||
@ -1284,7 +1301,7 @@ let redefinition ?(checks = true) ?(dev = false) ?(known = fun _ -> true)
|
|||||||
List.filter
|
List.filter
|
||||||
(fun (f : Tast.fn) ->
|
(fun (f : Tast.fn) ->
|
||||||
(not (known f.Tast.name)) && not (transient f.Tast.name))
|
(not (known f.Tast.name)) && not (transient f.Tast.name))
|
||||||
p.Tast.fns
|
siblings
|
||||||
and new_globals =
|
and new_globals =
|
||||||
List.filter (fun (g : Tast.global) -> not (known g.Tast.gname)) p.Tast.globals
|
List.filter (fun (g : Tast.global) -> not (known g.Tast.gname)) p.Tast.globals
|
||||||
in
|
in
|
||||||
@ -1313,7 +1330,7 @@ let redefinition ?(checks = true) ?(dev = false) ?(known = fun _ -> true)
|
|||||||
else
|
else
|
||||||
Printf.sprintf "%s = internal global ptr null\n"
|
Printf.sprintf "%s = internal global ptr null\n"
|
||||||
(cellptr f.Tast.name)))
|
(cellptr f.Tast.name)))
|
||||||
p.Tast.fns;
|
siblings;
|
||||||
if new_fns <> [] || new_globals <> [] then
|
if new_fns <> [] || new_globals <> [] then
|
||||||
Buffer.add_string m.out
|
Buffer.add_string m.out
|
||||||
"\ndeclare ptr @flan_dev_cell(ptr)\n\
|
"\ndeclare ptr @flan_dev_cell(ptr)\n\
|
||||||
@ -1328,7 +1345,12 @@ let redefinition ?(checks = true) ?(dev = false) ?(known = fun _ -> true)
|
|||||||
if not (List.exists (String.equal f.Tast.name) fns) then
|
if not (List.exists (String.equal f.Tast.name) fns) then
|
||||||
Buffer.add_string m.out
|
Buffer.add_string m.out
|
||||||
(Printf.sprintf "declare %s\n" (signature ~named:false f)))
|
(Printf.sprintf "declare %s\n" (signature ~named:false f)))
|
||||||
p.Tast.fns;
|
siblings;
|
||||||
|
(* Hidden for the same reason a redefined body is: default visibility in a
|
||||||
|
shared object is interposable, and that applies to taking the address too,
|
||||||
|
so a plain reference would resolve to the host's copy of the clause and
|
||||||
|
this module would install the very handler it is replacing. *)
|
||||||
|
List.iter (fun f -> emit_fn m ~hidden:true f) lifted;
|
||||||
List.iter (fun f -> emit_fn m ~hidden:dev f) targets;
|
List.iter (fun f -> emit_fn m ~hidden:dev f) targets;
|
||||||
if dev then begin
|
if dev then begin
|
||||||
(* Publishing is a separate, named function rather than a constructor: the
|
(* Publishing is a separate, named function rather than a constructor: the
|
||||||
|
|||||||
@ -573,7 +573,7 @@ let eval_expr ?(origin = "<eval>") t src : change =
|
|||||||
t.thunks <- t.thunks + 1;
|
t.thunks <- t.thunks + 1;
|
||||||
let name = Printf.sprintf "eval/%d" t.thunks in
|
let name = Printf.sprintf "eval/%d" t.thunks in
|
||||||
let thunk : Tast.fn =
|
let thunk : Tast.fn =
|
||||||
{ Tast.name; params = []; ret = Types.Unit; body; fdefers = []; floc = loc;
|
{ Tast.name; params = []; ret = Types.Unit; body; fdefers = []; fparent = None; floc = loc;
|
||||||
slots = Array.append base (Array.of_list (List.rev c.slots)) }
|
slots = Array.append base (Array.of_list (List.rev c.slots)) }
|
||||||
in
|
in
|
||||||
(* Built against the program but never spliced into it: an evaluation is not
|
(* Built against the program but never spliced into it: an evaluation is not
|
||||||
|
|||||||
@ -117,6 +117,12 @@ type fn = {
|
|||||||
which leaves through a landing block the backend builds and no form in
|
which leaves through a landing block the backend builds and no form in
|
||||||
[body] can reach. spec-conditions.md §5: they run, and errdefer does not. *)
|
[body] can reach. spec-conditions.md §5: they run, and errdefer does not. *)
|
||||||
fdefers : expr list;
|
fdefers : expr list;
|
||||||
|
(* Set on a function the checker made up rather than one anyone wrote: a
|
||||||
|
handler-bind clause, lifted out of the function named here. It is reached
|
||||||
|
by address from that function's body and from nowhere else, so it needs no
|
||||||
|
cell and no registry slot, and a redefinition of the parent carries its
|
||||||
|
own copy. *)
|
||||||
|
fparent : string option;
|
||||||
floc : Loc.t;
|
floc : Loc.t;
|
||||||
}
|
}
|
||||||
|
|
||||||
|
|||||||
@ -5,6 +5,16 @@
|
|||||||
|
|
||||||
(defvar ticks i64)
|
(defvar ticks i64)
|
||||||
|
|
||||||
|
;;; A condition and something that signals it, so that a body typed in later
|
||||||
|
;;; can establish a handler and transfer past this frame — spec-conditions.md
|
||||||
|
;;; §6. It is here rather than in the evaluated form on purpose: the guard that
|
||||||
|
;;; forwards the transfer has to be one the *host* was compiled with.
|
||||||
|
(defstruct Missing [id i32])
|
||||||
|
|
||||||
|
(defn probe [] i64
|
||||||
|
(signal (Missing {:id 1}))
|
||||||
|
0)
|
||||||
|
|
||||||
(defn step [] i64
|
(defn step [] i64
|
||||||
(set ticks (+ ticks 1))
|
(set ticks (+ ticks 1))
|
||||||
ticks)
|
ticks)
|
||||||
@ -16,4 +26,6 @@
|
|||||||
(print-i64 (step)) (newline)
|
(print-i64 (step)) (newline)
|
||||||
(while (= (agent/wait 100) 0) 0)
|
(while (= (agent/wait 100) 0) 0)
|
||||||
(print-i64 (step)) (newline)
|
(print-i64 (step)) (newline)
|
||||||
|
(while (= (agent/wait 100) 0) 0)
|
||||||
|
(print-i64 (step)) (newline)
|
||||||
0)
|
0)
|
||||||
|
|||||||
@ -129,6 +129,20 @@ let () =
|
|||||||
|
|
||||||
if not (settle 3) then fail "the second reload was never installed";
|
if not (settle 3) then fail "the second reload was never installed";
|
||||||
|
|
||||||
|
(* A restart-case in a body the process was never built with. The frame
|
||||||
|
it offers is an alloca in the newly loaded module's text, the call it
|
||||||
|
guards goes through the host's cell, and the transfer starts in a
|
||||||
|
handler and crosses [probe], which the host was compiled with. None of
|
||||||
|
those three meet anywhere else in the tests. *)
|
||||||
|
let r =
|
||||||
|
request c
|
||||||
|
"(:op \"eval\" :code \"(defn step [] i64 (restart-case (do (handler-bind [(Missing [c] (invoke-restart 'use-fallback))] (probe)) 0) (use-fallback [] 777)))\" :file \"/tmp/buf.flan\")"
|
||||||
|
in
|
||||||
|
if status r <> "ok" then
|
||||||
|
fail "a redefinition with a restart-case: %s"
|
||||||
|
(Option.value ~default:"" (Wire.string_field r "message"));
|
||||||
|
if not (settle 4) then fail "the third reload was never installed";
|
||||||
|
|
||||||
(* Expression evaluation, which is a different primitive: no name to
|
(* Expression evaluation, which is a different primitive: no name to
|
||||||
install a body into, so a thunk runs at a frame boundary and the value
|
install a body into, so a thunk runs at a frame boundary and the value
|
||||||
comes back rendered. The program has stopped reaching frame boundaries
|
comes back rendered. The program has stopped reaching frame boundaries
|
||||||
@ -140,11 +154,14 @@ let () =
|
|||||||
Unix.close c;
|
Unix.close c;
|
||||||
(* Closing the connection ends the program, and its transcript is the
|
(* Closing the connection ends the program, and its transcript is the
|
||||||
proof: 1 before any reload, 5 from a body over a var that did not
|
proof: 1 before any reload, 5 from a body over a var that did not
|
||||||
exist when it started, 105 from a second body reading the same one. *)
|
exist when it started, 105 from a second body reading the same one,
|
||||||
|
and 777 from a restart clause in a third — reached by a transfer that
|
||||||
|
started in a handler and crossed a function the host was built with. *)
|
||||||
ignore (Unix.waitpid [] pid);
|
ignore (Unix.waitpid [] pid);
|
||||||
let text = Buffer.contents output in
|
let text = Buffer.contents output in
|
||||||
if text <> "1\n5\n105\n" then
|
let wanted = "1\n5\n105\n777\n" in
|
||||||
fail "program transcript\n got: %S\n wanted: %S" text "1\n5\n105\n"
|
if text <> wanted then
|
||||||
|
fail "program transcript\n got: %S\n wanted: %S" text wanted
|
||||||
end;
|
end;
|
||||||
|
|
||||||
List.iter (fun f -> try Sys.remove f with Sys_error _ -> ()) [ sock; out ];
|
List.iter (fun f -> try Sys.remove f with Sys_error _ -> ()) [ sock; out ];
|
||||||
|
|||||||
Loading…
x
Reference in New Issue
Block a user