Three edges of Reach's walk that nothing called
An index expression inside a place, a place under addr, and a restart-case clause body are each the only route to a function in reach-walk.flan. Drop any one of the three from the walk and the function is not emitted, so the program stops linking rather than answering wrong; each mutation was planted and watched fail here. The addr case goes through a deref place on purpose, so the index case cannot stand in for it.
This commit is contained in:
parent
9549d386a1
commit
86d0c14a45
53
test/programs/reach-walk.flan
Normal file
53
test/programs/reach-walk.flan
Normal file
@ -0,0 +1,53 @@
|
||||
;;;; Three edges of Reach's walk, each the only route to one function.
|
||||
;;;;
|
||||
;;;; A release build is pruned: a function nothing reachable from main or from
|
||||
;;;; a global initialiser calls is not emitted at all. So an edge the walk
|
||||
;;;; forgets does not produce a wrong answer — it produces a program that does
|
||||
;;;; not link, with a message about a symbol nobody wrote. Each of the three
|
||||
;;;; functions below is called from exactly one place, and that place is an
|
||||
;;;; edge no other program in the corpus exercises:
|
||||
;;;;
|
||||
;;;; index-of the index expression of a place, (set (at a (f)) v)
|
||||
;;;; through a place under (addr ...), here a (deref ...) so that it is
|
||||
;;;; the addr edge and not the index one again
|
||||
;;;; placeholder a restart-case clause body, which is reached by a transfer
|
||||
;;;; and never by a call the walk can see from the body
|
||||
;;;;
|
||||
;;;; Nothing here is about the values; the values are how the test notices that
|
||||
;;;; the program was built and ran at all.
|
||||
|
||||
(defvar cells [4 i32])
|
||||
(defvar slot i32)
|
||||
|
||||
(defstruct Nope [id i32])
|
||||
|
||||
(defn index-of [] i32 2)
|
||||
|
||||
(defn through [] (Ptr i32) (addr slot))
|
||||
|
||||
(defn placeholder [] i32 42)
|
||||
|
||||
;;; Signals with nothing to return, so the clause body is the only way past.
|
||||
(defn missing [] i32
|
||||
(error (Nope {:id 1})))
|
||||
|
||||
(defn pick [] i32
|
||||
(restart-case (missing)
|
||||
(use-placeholder [] (placeholder))))
|
||||
|
||||
(defn main [] i32
|
||||
;; The index of a place is an expression, and it can call.
|
||||
(set (at cells (index-of)) 10)
|
||||
(print (at cells 2)) (println "")
|
||||
|
||||
;; (addr (deref p)) is p, so this is the addr edge over a place whose own
|
||||
;; walk is Pderef rather than Pindex — the index case above cannot stand in
|
||||
;; for it.
|
||||
(let [q (addr (deref (through)))]
|
||||
(set (deref q) 20))
|
||||
(print slot) (println "")
|
||||
|
||||
;; The clause body, reached only because the handler transfers into it.
|
||||
(handler-bind [(Nope [c] (invoke-restart 'use-placeholder))]
|
||||
(print (pick)) (println ""))
|
||||
0)
|
||||
@ -661,6 +661,32 @@ let () =
|
||||
outputs "a package reached along two routes" "programs/pkg-shared.flan"
|
||||
"ok\n";
|
||||
|
||||
(* Reach's walk, edge by edge. Pruning is what makes the link follow the
|
||||
program, and the cost of getting it wrong is not a wrong answer: a
|
||||
function the walk fails to reach is not emitted, and the build dies in
|
||||
the linker naming a symbol nobody wrote. reach-walk.flan calls three
|
||||
functions from three places that are each the only route to them — the
|
||||
index expression of a place, a place under [addr], and a restart-case
|
||||
clause body — so a walk that forgets any one of the three fails to build
|
||||
here. Caught rather than raised, because a build that dies takes the
|
||||
rest of the table with it. *)
|
||||
(match compile "programs/reach-walk.flan" with
|
||||
| exception Failure m ->
|
||||
incr failures;
|
||||
Printf.printf
|
||||
"FAIL Reach's walk: it did not build, which is what a pruned function looks like\n%s\n"
|
||||
m
|
||||
| exe ->
|
||||
let code, text = run exe None in
|
||||
let want = "10\n20\n42\n" in
|
||||
if text <> want || code <> 0 then begin
|
||||
incr failures;
|
||||
Printf.printf
|
||||
"FAIL Reach's walk\n got: %S (exit %d)\n wanted: %S\n"
|
||||
text code want
|
||||
end;
|
||||
(try Sys.remove exe with Sys_error _ -> ()));
|
||||
|
||||
(* The refusals. Each is a thing that would otherwise fail later and
|
||||
elsewhere — as a name the checker says is unknown, or as a collision
|
||||
nobody wrote — so what is asserted is the *reason*, at the form that
|
||||
|
||||
Loading…
x
Reference in New Issue
Block a user