From 86d0c14a45a0ef5836f908ad731aa05f08fbc9d2 Mon Sep 17 00:00:00 2001 From: Joseph Ferano Date: Sat, 12 Sep 2026 10:38:40 +0700 Subject: [PATCH] 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. --- test/programs/reach-walk.flan | 53 +++++++++++++++++++++++++++++++++++ test/test_acceptance.ml | 26 +++++++++++++++++ 2 files changed, 79 insertions(+) create mode 100644 test/programs/reach-walk.flan diff --git a/test/programs/reach-walk.flan b/test/programs/reach-walk.flan new file mode 100644 index 0000000..a82c111 --- /dev/null +++ b/test/programs/reach-walk.flan @@ -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) diff --git a/test/test_acceptance.ml b/test/test_acceptance.ml index 05b46a2..af19c20 100644 --- a/test/test_acceptance.ml +++ b/test/test_acceptance.ml @@ -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