The break loop meets a bad index, and the test says so rather than the reasoning
This commit is contained in:
parent
542bc6a65c
commit
e80e79b3fd
14
BUILT.md
14
BUILT.md
@ -4002,6 +4002,20 @@ inherited. It now splits:
|
|||||||
`bounds-condition.flan` asserts the first of those directly: five `defer`s across five abandoned and finished frames,
|
`bounds-condition.flan` asserts the first of those directly: five `defer`s across five abandoned and finished frames,
|
||||||
counted.
|
counted.
|
||||||
|
|
||||||
|
### Both halves are tested, and they are different tests
|
||||||
|
|
||||||
|
`bounds-condition.flan` (acceptance table, at `-O2`, `-O0` and as a dev build) is the **answered** half: a
|
||||||
|
`handler-bind` over five routes to a bad index, taking the frame loop's `continue` each time. It does not import the
|
||||||
|
agent, so `flan_break_hook` is NULL in all three rows and nothing there says anything about the break loop.
|
||||||
|
|
||||||
|
`dev-break-bounds.flan` (`test_dev.ml`) is the half the change is actually for: **nothing handles it**, so the signal
|
||||||
|
walks the handlers, finds none, and reaches the hook. The daemon sees a program that stopped without being told to;
|
||||||
|
`BoundsError` is what the break reports; its own name resolves to a layout whose fields are `low`, `high`, `length`,
|
||||||
|
so the conditions buffer shows the numbers with nothing special-cased for it; the restart list is exactly
|
||||||
|
`continue` — the *program's* own, which is the visible consequence of establishing none at the site — and taking it
|
||||||
|
resumes, with an ordinary evaluation working on the far side. That last step is the whole claim: the session outlived
|
||||||
|
the index.
|
||||||
|
|
||||||
### Vec and Map
|
### Vec and Map
|
||||||
|
|
||||||
`(at v i)` and `(at arr i)` are the same form in the source, so shipping one signalling and the other exiting would
|
`(at v i)` and `(at arr i)` are the same form in the source, so shipping one signalling and the other exiting would
|
||||||
|
|||||||
6
NEXT.md
6
NEXT.md
@ -26,6 +26,12 @@ shape — which is on the restart stack and on the break loop's list without any
|
|||||||
followed from: an answered bounds failure leaves through the function's unwind block, which is `return`'s path, so it
|
followed from: an answered bounds failure leaves through the function's unwind block, which is `return`'s path, so it
|
||||||
runs the defers; an unanswered one still runs none. `test/programs/bounds-condition.flan` counts them.
|
runs the defers; an unanswered one still runs none. `test/programs/bounds-condition.flan` counts them.
|
||||||
|
|
||||||
|
Two tests, because there are two paths. `bounds-condition.flan` is the *answered* half — a `handler-bind` taking
|
||||||
|
`continue` over five routes to a bad index, at `-O2`, `-O0` and as a dev build. `dev-break-bounds.flan` in
|
||||||
|
`test_dev.ml` is the half this was built for: nothing handles it, the break loop reports `BoundsError`, the layout for
|
||||||
|
that name resolves to `low`/`high`/`length`, the only restart on offer is the program's own `continue`, and taking it
|
||||||
|
resumes with the session intact.
|
||||||
|
|
||||||
**Still dying, deliberately:** a `Map`'s bounds check and `flan_vec_stale_fail`. The stale-allocator case is a
|
**Still dying, deliberately:** a `Map`'s bounds check and `flan_vec_stale_fail`. The stale-allocator case is a
|
||||||
different kind of failure — the region the container lived in was released — and there is no frame to go back to that
|
different kind of failure — the region the container lived in was released — and there is no frame to go back to that
|
||||||
would not read freed memory. The map path was left alone rather than converted half-way.
|
would not read freed memory. The map path was left alone rather than converted half-way.
|
||||||
|
|||||||
@ -316,9 +316,12 @@ another name. Two things are missing behind it:
|
|||||||
> same message only if nothing answered. The site establishes **no restart** — nothing
|
> same message only if nothing answered. The site establishes **no restart** — nothing
|
||||||
> a handler can do makes a bad index good, so there is no attempt to re-run — and what
|
> a handler can do makes a bad index good, so there is no attempt to re-run — and what
|
||||||
> answers it is the restart the program already had, which is exactly the frame loop's
|
> answers it is the restart the program already had, which is exactly the frame loop's
|
||||||
> `continue` this section is about. `BUILT.md` has the reasoning and
|
> `continue` this section is about. `BUILT.md` has the reasoning,
|
||||||
> `test/programs/bounds-condition.flan` has the worked case. Item 1 below, the
|
> `test/programs/bounds-condition.flan` has the handled case, and
|
||||||
> rollback, is now the whole of what is left here.
|
> `test/programs/dev-break-bounds.flan` drives the break loop over an
|
||||||
|
> *un*handled one from the editor's side — stopped, restarts listed,
|
||||||
|
> `continue` taken, session intact. Item 1 below, the rollback, is now the
|
||||||
|
> whole of what is left here.
|
||||||
|
|
||||||
That is not theoretical for this game. `game.clj`'s `update-game` computes `row` and
|
That is not theoretical for this game. `game.clj`'s `update-game` computes `row` and
|
||||||
`col` straight from the mouse position and indexes the grid with them, with no bounds
|
`col` straight from the mouse position and indexes the grid with them, with no bounds
|
||||||
|
|||||||
@ -709,7 +709,7 @@ let fninfo m (fn : Tast.fn) ~nslots =
|
|||||||
one arrives here as a huge unsigned value: an unsigned comparison catches
|
one arrives here as a huge unsigned value: an unsigned comparison catches
|
||||||
the negative and the too-large case in a single test.
|
the negative and the too-large case in a single test.
|
||||||
|
|
||||||
This is the *trapping* shape and it still has four users: the restart
|
This is the *trapping* shape and it still has three users: the restart
|
||||||
lookups and the unarmed-clause check, none of which is recoverable — there
|
lookups and the unarmed-clause check, none of which is recoverable — there
|
||||||
is nowhere to resume a transfer whose target does not exist. The two bounds
|
is nowhere to resume a transfer whose target does not exist. The two bounds
|
||||||
checks moved off it; see [signal_block]. *)
|
checks moved off it; see [signal_block]. *)
|
||||||
|
|||||||
52
test/programs/dev-break-bounds.flan
Normal file
52
test/programs/dev-break-bounds.flan
Normal file
@ -0,0 +1,52 @@
|
|||||||
|
;;;; A program that stops on a bad index, for driving the break loop over one.
|
||||||
|
;;;;
|
||||||
|
;;;; bounds-condition.flan is the other half of the same change and covers the
|
||||||
|
;;;; path where a `handler-bind` answers. This one covers the path the change
|
||||||
|
;;;; is actually *for*: **nothing handles it**, so the signal walks the
|
||||||
|
;;;; handlers, finds none, and reaches `flan_break_hook` — which is where an
|
||||||
|
;;;; editor picks up a stopped program with the stack, the locals and the
|
||||||
|
;;;; globals readable and the restarts on offer.
|
||||||
|
;;;;
|
||||||
|
;;;; That is the claim `PORTING.md` said was missing, and it is worth testing
|
||||||
|
;;;; end to end rather than reasoning about: before this, a bad index called
|
||||||
|
;;;; exit(134), and with `flan dev` running as one process that took the
|
||||||
|
;;;; compiler and the session with it.
|
||||||
|
;;;;
|
||||||
|
;;;; The shape is a frame loop's: one `restart-case` offering `continue` around
|
||||||
|
;;;; the work, which is sand.flan's shape and the game's. No restart is
|
||||||
|
;;;; established at the failing index — nothing a handler could do would make
|
||||||
|
;;;; index 9 valid for a length-4 array — so `continue` is the *program's* own
|
||||||
|
;;;; restart, found by the ordinary walk, and taking it is the proof that a
|
||||||
|
;;;; bounds failure now lands somewhere a session can be recovered from.
|
||||||
|
(import agent "vendor:agent")
|
||||||
|
|
||||||
|
(defvar grid [4 i32])
|
||||||
|
(defvar skipped i64)
|
||||||
|
|
||||||
|
;;; One frame deep under the restart-case, so the transfer has something to
|
||||||
|
;;; cross and the backtrace has something to show.
|
||||||
|
(defn touch [i i32] ()
|
||||||
|
(set (at grid i) 1))
|
||||||
|
|
||||||
|
(defn frame [i i32] ()
|
||||||
|
(restart-case
|
||||||
|
(do (touch i) (println "frame done"))
|
||||||
|
(continue [] (set skipped (+ skipped 1)))))
|
||||||
|
|
||||||
|
(defvar ticks i64)
|
||||||
|
|
||||||
|
(defn main [] i32
|
||||||
|
(agent/start "/tmp/flan-dev-break-bounds-fallback.sock")
|
||||||
|
;; Out of bounds on the first frame, with nothing handling it: the daemon
|
||||||
|
;; meets a program that has already stopped, which is the state an editor
|
||||||
|
;; has to cope with and the hardest one to arrange later.
|
||||||
|
(frame 9)
|
||||||
|
;; 1 once `continue` was taken. Printing it is how the transcript says which
|
||||||
|
;; way the program left the break, rather than that it left.
|
||||||
|
(print skipped) (println "")
|
||||||
|
;; And it keeps polling on the far side, because the claim worth testing is
|
||||||
|
;; that everything still works after a break over a bad index.
|
||||||
|
(dotimes [i 4000]
|
||||||
|
(agent/wait 5)
|
||||||
|
(set ticks (+ ticks 1)))
|
||||||
|
0)
|
||||||
@ -1152,9 +1152,15 @@ let () =
|
|||||||
slices, with `low` and `high` equal for an index and the two ends for a
|
slices, with `low` and `high` equal for an index and the two ends for a
|
||||||
range, which is why there is one condition type and not two.
|
range, which is why there is one condition type and not two.
|
||||||
|
|
||||||
Also at -O0 and as a dev build: the dev build is the one with the break
|
Also at -O0 and as a dev build. The dev build is here for the reason
|
||||||
loop hook installed, and a handler that transfers must reach the
|
the rest of the dev rows are — every call goes through a cell and a
|
||||||
transfer before the hook rather than after it. *)
|
shadow-stack frame is pushed per call — so this pins that the
|
||||||
|
indirection does not change where a transfer lands. It says nothing
|
||||||
|
about the break loop: this program does not import the agent, so
|
||||||
|
flan_break_hook is NULL in all three rows and the handler is what
|
||||||
|
answers. The break loop over a bad index is its own case, in
|
||||||
|
test_dev.ml, over programs/dev-break-bounds.flan, with nothing
|
||||||
|
handling it at all. *)
|
||||||
let bounds_cond_out =
|
let bounds_cond_out =
|
||||||
"read 12\nlow 7\nlength 4\nlow -1\nwrote 99\nlow 4\n\
|
"read 12\nlow 7\nlength 4\nlow -1\nwrote 99\nlow 4\n\
|
||||||
slice 3\nlow 2\nhigh 9\nlength 5\nlow 3\nhigh 1\n\
|
slice 3\nlow 2\nhigh 9\nlength 5\nlow 3\nhigh 1\n\
|
||||||
|
|||||||
136
test/test_dev.ml
136
test/test_dev.ml
@ -764,6 +764,142 @@ let () =
|
|||||||
(try ignore (Unix.waitpid [] bpid) with Unix.Unix_error _ -> ())
|
(try ignore (Unix.waitpid [] bpid) with Unix.Unix_error _ -> ())
|
||||||
end
|
end
|
||||||
end;
|
end;
|
||||||
|
(* ── A break over a bad index ──────────────────────────────────── *)
|
||||||
|
|
||||||
|
(* The block above stops on an [error] the program wrote. This one stops on
|
||||||
|
one nobody wrote: an out-of-bounds index, which until now printed its
|
||||||
|
location and called exit(134) — taking the compiler and the session with
|
||||||
|
it, since [flan dev] is one process.
|
||||||
|
|
||||||
|
Three claims, and the third is the point. The condition arrives named
|
||||||
|
[BoundsError] and its name resolves to a layout, so the conditions
|
||||||
|
buffer can show the numbers without anything special-casing it. The
|
||||||
|
restart on offer is the *program's* own [continue] — nothing is
|
||||||
|
established at the failing index, deliberately, because nothing a
|
||||||
|
handler could do would make index 9 valid for a length-4 array. And
|
||||||
|
taking it resumes: the transcript says 1, which is what [continue]'s
|
||||||
|
clause set, and the program goes on polling on the far side.
|
||||||
|
|
||||||
|
Its own daemon and its own program, for the reason every block here has
|
||||||
|
one: these claims are about one frame of one program. *)
|
||||||
|
let xsock = tmp "break-bounds.sock" and xout = tmp "break-bounds.out" in
|
||||||
|
(try Sys.remove xsock with Sys_error _ -> ());
|
||||||
|
let xfd =
|
||||||
|
Unix.openfile xout [ Unix.O_WRONLY; Unix.O_CREAT; Unix.O_TRUNC ] 0o600
|
||||||
|
in
|
||||||
|
let xpid =
|
||||||
|
Unix.create_process flan
|
||||||
|
[| flan; "dev"; "programs/dev-break-bounds.flan"; "-s"; xsock |]
|
||||||
|
Unix.stdin xfd Unix.stderr
|
||||||
|
in
|
||||||
|
Unix.close xfd;
|
||||||
|
if not (await (fun () -> Sys.file_exists xsock)) then begin
|
||||||
|
fail "the bad-index daemon never listened";
|
||||||
|
(try Unix.kill xpid Sys.sigkill with Unix.Unix_error _ -> ())
|
||||||
|
end
|
||||||
|
else begin
|
||||||
|
let xoutput = Buffer.create 256 in
|
||||||
|
let c = connect xsock in
|
||||||
|
let ask sexp =
|
||||||
|
let r = Wire.parse (Wire.send c sexp; Wire.recv c) in
|
||||||
|
(match Wire.string_field r "output" with
|
||||||
|
| Some t -> Buffer.add_string xoutput t
|
||||||
|
| None -> ());
|
||||||
|
r
|
||||||
|
in
|
||||||
|
let stopped r =
|
||||||
|
match Wire.field r "stopped" with
|
||||||
|
| Some { Form.v = Form.Sym "t"; _ } -> true
|
||||||
|
| _ -> false
|
||||||
|
in
|
||||||
|
let last = ref (ask "(:op \"describe\")") in
|
||||||
|
if not
|
||||||
|
(await (fun () -> last := ask "(:op \"describe\")"; stopped !last))
|
||||||
|
then fail "a bad index never stopped the program"
|
||||||
|
else begin
|
||||||
|
let cname =
|
||||||
|
match Wire.string_field !last "condition" with Some c -> c | None -> ""
|
||||||
|
in
|
||||||
|
if cname <> "BoundsError" then
|
||||||
|
fail "a bad index is reported as %S, wanted %S" cname "BoundsError";
|
||||||
|
(* The same round trip the block above makes: the name the break
|
||||||
|
reports is handed straight back as [:type], because that is the
|
||||||
|
conditions buffer's whole path. Three i64s — low, high and length —
|
||||||
|
with low and high the same index for an [at] and the two ends of a
|
||||||
|
range for a [slice], which is why there is one condition type and
|
||||||
|
not two. *)
|
||||||
|
let r =
|
||||||
|
ask (Printf.sprintf "(:op \"layout\" :type %s)" (Wire.quote cname))
|
||||||
|
in
|
||||||
|
if status r <> "ok" then
|
||||||
|
fail "BoundsError did not resolve to a layout: %s"
|
||||||
|
(Option.value ~default:"" (Wire.string_field r "message"))
|
||||||
|
else
|
||||||
|
(match Wire.field r "fields" with
|
||||||
|
| Some { Form.v = Form.List fs; _ } ->
|
||||||
|
let names =
|
||||||
|
List.filter_map
|
||||||
|
(fun (e : Form.t) ->
|
||||||
|
match e.Form.v with
|
||||||
|
| Form.List ({ Form.v = Form.Str n; _ } :: _) -> Some n
|
||||||
|
| _ -> None)
|
||||||
|
fs
|
||||||
|
in
|
||||||
|
if names <> [ "low"; "high"; "length" ] then
|
||||||
|
fail "BoundsError's fields: %s" (String.concat ", " names)
|
||||||
|
| _ -> fail "BoundsError's layout has no fields");
|
||||||
|
(* Only the program's own restart is on offer. Nothing is pushed at the
|
||||||
|
failing index, so a list with anything else on it would mean a site
|
||||||
|
restart had been established after all. *)
|
||||||
|
let r = ask "(:op \"break\")" in
|
||||||
|
if status r <> "ok" then fail "break over a bad index: %s" (status r);
|
||||||
|
(match Wire.field r "restarts" with
|
||||||
|
| Some { Form.v = Form.List l; _ } ->
|
||||||
|
let names =
|
||||||
|
List.filter_map
|
||||||
|
(fun (n : Form.t) ->
|
||||||
|
match n.Form.v with Form.Str x -> Some x | _ -> None)
|
||||||
|
l
|
||||||
|
in
|
||||||
|
if names <> [ "continue" ] then
|
||||||
|
fail "restarts at a bad index: %s" (String.concat ", " names)
|
||||||
|
| _ -> fail "break over a bad index listed no restarts");
|
||||||
|
(* And the payoff: taking it resumes, which is the difference between a
|
||||||
|
stop you can recover from and a dead session. *)
|
||||||
|
let r = ask "(:op \"restart\" :name \"continue\")" in
|
||||||
|
if status r <> "ok" then
|
||||||
|
fail "continuing past a bad index: %s"
|
||||||
|
(Option.value ~default:"" (Wire.string_field r "message"));
|
||||||
|
let printed () =
|
||||||
|
ignore (ask "(:op \"describe\")");
|
||||||
|
List.exists (String.equal "1")
|
||||||
|
(String.split_on_char '\n' (Buffer.contents xoutput))
|
||||||
|
in
|
||||||
|
if not (await printed) then
|
||||||
|
fail "the program never resumed past a bad index";
|
||||||
|
(* Ordinary work on the far side of it, which is the whole claim: the
|
||||||
|
session outlived the index. *)
|
||||||
|
let r =
|
||||||
|
ask "(:op \"eval-expr\" :code \"(+ 2 2)\" :file \"/tmp/buf.flan\")"
|
||||||
|
in
|
||||||
|
if Wire.string_field r "value" <> Some "4" then
|
||||||
|
fail "an expression after a bad index: %s"
|
||||||
|
(Option.value ~default:(status r) (Wire.string_field r "message"))
|
||||||
|
end;
|
||||||
|
ignore (ask "(:op \"close\")");
|
||||||
|
Unix.close c;
|
||||||
|
if not
|
||||||
|
(await ~ms:5000 (fun () ->
|
||||||
|
match Unix.waitpid [ Unix.WNOHANG ] xpid with
|
||||||
|
| 0, _ -> false
|
||||||
|
| _ -> true
|
||||||
|
| exception Unix.Unix_error _ -> true))
|
||||||
|
then begin
|
||||||
|
(try Unix.kill xpid Sys.sigkill with Unix.Unix_error _ -> ());
|
||||||
|
(try ignore (Unix.waitpid [] xpid) with Unix.Unix_error _ -> ())
|
||||||
|
end
|
||||||
|
end;
|
||||||
|
|
||||||
(* ── The locals of a stopped frame ─────────────────────────────── *)
|
(* ── The locals of a stopped frame ─────────────────────────────── *)
|
||||||
|
|
||||||
(* A third daemon, over a program that stops with something worth looking
|
(* A third daemon, over a program that stops with something worth looking
|
||||||
|
|||||||
Loading…
x
Reference in New Issue
Block a user