handler-bind has a value, and both backends now say the same one
(defn compute [] i64 (handler-bind [...] (risky))) printed 0 through LLVM and 2 through --x86, and neither was the restart's answer. The divergence was real and the cause was in neither backend: check_handler_bind wrote [ignore want] and typed the form Unit, so a unit in value position was never checked against the expectation that would have refused it. Both lowerings then answered a caller that had no business asking -- emit.ml a literal zeroinitializer, x86.ml whatever the body's last form had left in the destination slot. One of those looked like a value. Unit was the wrong answer anyway. Every use of handler-bind in value position in this repository -- restarts.flan, cleanup.flan, p6-transfer.flan, p10-defer-transfer.flan -- writes it as a restart-case body, where §3 requires the body and the clauses to agree in type; making the form unit refuses all four. So it takes with-allocator's shape, which is the same shape for the same reason: the body's last form is the value, threaded through [expect] like any other. handler-case, whose value is the handler's rather than the body's, is untouched and still refused by name in parse.ml -- that difference is the whole of what separates the two, and it is not this one. emit.ml returns [last] with no phi and no slot: the pad terminates at current_pad and never at the join, so the join has one predecessor and the body's value dominates it. x86.ml needed no change at all -- it had been passing dst and the type through to the body all along. p12-handler-value.flan is the shape the survey could not see, plus the neighbours a divergence usually travels with: a clause parameter, nested restart-cases, a defer between the signal and the restart-case, and f64 and string across the transfer. All six already agreed; the handler-bind value was alone. @x86 MATCH 128 -> 129, DIFFER 0.
This commit is contained in:
parent
f885e1abfa
commit
2ec12c064d
32
lib/check.ml
32
lib/check.ml
@ -2354,7 +2354,6 @@ and check_fn ctx ~want loc (params : string list) body =
|
||||
it, and an early exit would leave them on the stack pointing into a function
|
||||
that has gone. *)
|
||||
and check_handler_bind ctx ?want loc clauses body =
|
||||
ignore want;
|
||||
let frames =
|
||||
List.map
|
||||
(fun (c : Ast.hclause) ->
|
||||
@ -2422,11 +2421,36 @@ and check_handler_bind ctx ?want loc clauses body =
|
||||
collide. *)
|
||||
let saved = ctx.in_frames in
|
||||
ctx.in_frames <- Some "handler-bind";
|
||||
let body =
|
||||
barrier ctx "a handler-bind" (fun () -> map_lr (fun e -> check ctx e) body)
|
||||
(* The body's last form is the form's value, which is [with-allocator]'s
|
||||
shape and for the same reason: both wrap a body in something established
|
||||
around it and taken off after, and neither is a reason for the body to
|
||||
stop being an expression. §3 needs it — a [restart-case] whose body is a
|
||||
[handler-bind] has to agree in type with its clauses, which is how all
|
||||
four of this repository's crossing probes are written — and it is what
|
||||
[handler-case] will *not* be: that one's value is the handler's, which is
|
||||
the whole difference between the two and is why it is still refused by
|
||||
name in [parse.ml].
|
||||
|
||||
This used to be [ignore want] and a flat [Types.Unit], and nothing
|
||||
complained, because a unit in value position is only caught where the
|
||||
expectation is checked. So the two backends each answered a caller that
|
||||
asked anyway, and answered differently: [emit.ml] a literal zero, this
|
||||
machine whatever the body's last form had left in the slot. Neither was a
|
||||
value; one of them merely looked like one. *)
|
||||
let body, ty =
|
||||
barrier ctx "a handler-bind" (fun () ->
|
||||
let rec go = function
|
||||
| [] -> [ unit_at loc ], Types.Unit
|
||||
| [ last ] -> let l = check ctx ?want last in [ l ], l.Tast.ty
|
||||
| e :: rest ->
|
||||
let e = check ctx e in
|
||||
let rest, ty = go rest in
|
||||
e :: rest, ty
|
||||
in
|
||||
go body)
|
||||
in
|
||||
ctx.in_frames <- saved;
|
||||
mk loc Types.Unit (Tast.Handled (frames, body))
|
||||
expect loc ~want (mk loc ty (Tast.Handled (frames, body)))
|
||||
|
||||
(* (restart-case BODY (name [] BODY-1) ...) — spec-conditions.md §3 and §6.
|
||||
|
||||
|
||||
15
lib/emit.ml
15
lib/emit.ml
@ -1700,7 +1700,6 @@ and emit_handled f frames body =
|
||||
f.pads <- (pad, used) :: f.pads;
|
||||
let last = block f body in
|
||||
f.pads <- List.tl f.pads;
|
||||
ignore last;
|
||||
let reached = f.live in
|
||||
if f.live then begin pop (); term f "br label %%%s" ld end;
|
||||
(* A transfer passing through: these frames are on the establishing
|
||||
@ -1713,7 +1712,19 @@ and emit_handled f frames body =
|
||||
term f "br label %%%s" (current_pad f)
|
||||
end;
|
||||
if not reached then begin f.live <- false; "zeroinitializer" end
|
||||
else begin label f ld; "zeroinitializer" end
|
||||
else begin
|
||||
label f ld;
|
||||
(* The body's own value, and no [phi] or slot to carry it, unlike
|
||||
[emit_with_alloc] next door: [ld] has exactly one predecessor. The pad
|
||||
terminates at [current_pad] and never at [ld], so the only edge into it
|
||||
is the [br] above, and [last] is computed in the block that ends with
|
||||
that [br] — it dominates every use here.
|
||||
|
||||
This used to answer "zeroinitializer" and drop [last] on the floor, from
|
||||
when the checker typed this form [unit] and no caller was supposed to be
|
||||
able to ask. One could, and the constant zero is what it got. *)
|
||||
last
|
||||
end
|
||||
|
||||
(* A clause's parameters, as one LLVM struct: what the invoker stores into and
|
||||
what the clause loads out of. The two ends never see each other, so the
|
||||
|
||||
95
spike/x86/p12-handler-value.flan
Normal file
95
spike/x86/p12-handler-value.flan
Normal file
@ -0,0 +1,95 @@
|
||||
;;;; A handler-bind in value position, and the shapes around it.
|
||||
;;;;
|
||||
;;;; This is here because for a long time nothing in the corpus asked a
|
||||
;;;; [handler-bind] what its value was. [check.ml] typed the form [unit] and
|
||||
;;;; dropped the expectation without checking it, so a caller that asked got an
|
||||
;;;; answer anyway -- and the two backends had picked different ones. [emit.ml]
|
||||
;;;; answered a literal zero; the hand-written backend answered whatever the
|
||||
;;;; body's last form had left in the destination slot. The program below
|
||||
;;;; printed 0 through LLVM and 2 through --x86, and neither number was the
|
||||
;;;; restart's.
|
||||
;;;;
|
||||
;;;; The four programs that did write a [handler-bind] in value position all
|
||||
;;;; wrote it as a [restart-case] body -- restarts.flan, cleanup.flan,
|
||||
;;;; p6-transfer.flan, p10-defer-transfer.flan -- where §3 makes the types
|
||||
;;;; agree but a transfer always leaves before the fall-through is reached. So
|
||||
;;;; the value was never read and the hole stayed open. Here it is read:
|
||||
;;;; [answered] returns through the handler-bind, and its value has to be the
|
||||
;;;; clause's.
|
||||
;;;;
|
||||
;;;; The rest are the neighbouring shapes, because a divergence is rarely
|
||||
;;;; alone: a clause parameter, two nested restart-cases, a defer between the
|
||||
;;;; signal and the restart-case, and three types wider than the i32 the
|
||||
;;;; condition corpus is written in.
|
||||
(defstruct Oops [id i32])
|
||||
|
||||
(defvar trace i64)
|
||||
|
||||
;;; The shape that had no answer. The handler-bind is this function's last
|
||||
;;; form, so what it yields is what the function returns, two frames above the
|
||||
;;; restart-case the transfer lands in.
|
||||
(defn risky [] i64
|
||||
(restart-case (do (signal (Oops {.id 1})) 7)
|
||||
(use-zero [] 42)))
|
||||
|
||||
(defn answered [] i64
|
||||
(handler-bind [(Oops [c] (invoke-restart 'use-zero))]
|
||||
(risky)))
|
||||
|
||||
;;; The fall-through half of the same shape: nothing handles the signal, so the
|
||||
;;; body's own value is the one that comes back out through both forms.
|
||||
(defn unanswered [] i64
|
||||
(handler-bind [(Oops [c] (set trace (+ trace 100)))]
|
||||
(risky)))
|
||||
|
||||
;;; §3's parameter, crossing into an i64 clause.
|
||||
(defn supplied [] i64
|
||||
(restart-case (do (signal (Oops {.id 2})) 7)
|
||||
(use-value [v i64] (* v 3))))
|
||||
|
||||
;;; §4: the inner frame wins, and the arithmetic written around it still runs.
|
||||
(defn nested [] i64
|
||||
(restart-case
|
||||
(+ (restart-case (do (signal (Oops {.id 3})) 7)
|
||||
(use-zero [] 10))
|
||||
1000)
|
||||
(use-zero [] 20)))
|
||||
|
||||
;;; §5: a defer between the signal and the restart-case runs on the way out,
|
||||
;;; before the clause body starts.
|
||||
(defn mid [] i64
|
||||
(defer (set trace (+ trace 1)))
|
||||
(signal (Oops {.id 4}))
|
||||
7)
|
||||
|
||||
(defn deferred [] i64
|
||||
(restart-case (mid) (use-zero [] 9)))
|
||||
|
||||
;;; Two widths the condition corpus does not otherwise carry across a transfer:
|
||||
;;; a float, which travels in the other register file, and a string, which is a
|
||||
;;; pointer and a length rather than one machine word.
|
||||
(defn floating [] f64
|
||||
(restart-case (do (signal (Oops {.id 5})) 1.5)
|
||||
(use-value [v f64] (* v 2.0))))
|
||||
|
||||
(defn spelled [] string
|
||||
(restart-case (do (signal (Oops {.id 6})) "fell-through")
|
||||
(use-value [v string] v)))
|
||||
|
||||
(defn main [] i32
|
||||
(handler-bind [(Oops [c] (invoke-restart 'use-zero))]
|
||||
(println (answered))) ; 42
|
||||
(println (unanswered)) ; 7
|
||||
(println trace) ; 100
|
||||
(handler-bind [(Oops [c] (invoke-restart 'use-value (i64 5)))]
|
||||
(println (supplied))) ; 15
|
||||
(handler-bind [(Oops [c] (invoke-restart 'use-zero))]
|
||||
(println (nested))) ; 1010
|
||||
(handler-bind [(Oops [c] (invoke-restart 'use-zero))]
|
||||
(println (deferred))) ; 9
|
||||
(println trace) ; 101 — the defer ran
|
||||
(handler-bind [(Oops [c] (invoke-restart 'use-value 2.5))]
|
||||
(println (floating))) ; 5
|
||||
(handler-bind [(Oops [c] (invoke-restart 'use-value "supplied"))]
|
||||
(println (spelled))) ; supplied
|
||||
0)
|
||||
Loading…
x
Reference in New Issue
Block a user