102 lines
4.8 KiB
Plaintext
102 lines
4.8 KiB
Plaintext
;;;; The aggregate case across the reload boundary, v1 (HANDOFF-x86-redef.md,
|
|
;;;; item 4).
|
|
;;;;
|
|
;;;; `reload.flan' proves that a redefined body is reached; every signature in
|
|
;;;; it is scalar. That is the half of the reload primitive the two backends
|
|
;;;; cannot disagree about. `lib/x86.ml' licenses its own calling convention on
|
|
;;;; the grounds that a dev build is compiled entirely by it and a release
|
|
;;;; build entirely by LLVM, and the conventions agree on every scalar and
|
|
;;;; disagree on every aggregate — here each goes by pointer with a hidden
|
|
;;;; sret, while LLVM classifies per eightbyte. So a redefined function taking
|
|
;;;; or returning a struct is the case that would expose a mismatch, and it is
|
|
;;;; the case nothing measured. This fixture is that case.
|
|
;;;;
|
|
;;;; No `main': the host is test/reload_host.c, unchanged, which links this and
|
|
;;;; then dlopens rebuilt copies. Everything aggregate happens *inside* Flan,
|
|
;;;; between the host's compiled-once call site and the redefined body. The C
|
|
;;;; boundary stays scalar on purpose — that is where the two conventions are
|
|
;;;; required to agree, and it is not what is under test.
|
|
;;;;
|
|
;;;; Four struct shapes, because SysV treats them four different ways and
|
|
;;;; x86.ml treats all four the same:
|
|
;;;;
|
|
;;;; Pair two eightbytes, both INTEGER — SysV passes it in rdi:rsi and
|
|
;;;; returns it in rax:rdx. Diverges from x86.ml in both directions.
|
|
;;;; Quad thirty-two bytes, so MEMORY — SysV copies the argument onto the
|
|
;;;; stack, where x86.ml passes a pointer. The *return* is a hidden
|
|
;;;; pointer in the first integer register for SysV too, so that half
|
|
;;;; of the matrix may well coincide; it is covered because assuming
|
|
;;;; which half coincides is exactly the kind of argument this fixture
|
|
;;;; exists to replace with a measurement.
|
|
;;;; Duo two SSE eightbytes — xmm0:xmm1.
|
|
;;;; Mix one INTEGER and one SSE — rax and xmm0, a third pattern again.
|
|
;;;;
|
|
;;;; Every field is weighted by position in the answer — a + 100b + 10000c —
|
|
;;;; rather than summed. A symmetric sum would print the right number under a
|
|
;;;; convention mismatch that merely permuted the fields, which is the way a
|
|
;;;; test like this passes while proving nothing.
|
|
|
|
(defstruct Pair [a i64 b i64])
|
|
(defstruct Quad [a i64 b i64 c i64 d i64])
|
|
(defstruct Duo [x f64 y f64])
|
|
(defstruct Mix [n i64 z f64])
|
|
|
|
;;; The state that has to survive a reload, written by a loaded module rather
|
|
;;; than by the host: a redefinition declares it external, so the store lands
|
|
;;; on the host's copy and not on a private one.
|
|
(defvar counter i64)
|
|
|
|
;;; The other direction. These are never redefined, so a module reaches each
|
|
;;; one through its cell and hands it an aggregate — module to host, where the
|
|
;;; four `step' functions below are host to module. Each is also a tripwire:
|
|
;;; v2 changes all four, and since a module declares a sibling rather than
|
|
;;; defining it, that changed text must be dead. A module that grew its own
|
|
;;; copy prints a visibly different number.
|
|
(defn weigh-pair [p Pair] i64 (+ (.a p) (* 3 (.b p))))
|
|
|
|
(defn weigh-quad [q Quad] i64
|
|
(+ (+ (.a q) (* 3 (.b q))) (+ (* 5 (.c q)) (* 7 (.d q)))))
|
|
|
|
(defn weigh-duo [d Duo] i64 (+ (i64 (.x d)) (* 3 (i64 (.y d)))))
|
|
|
|
(defn weigh-mix [m Mix] i64 (+ (.n m) (* 3 (i64 (.z m)))))
|
|
|
|
;;; The four redefined bodies. Each takes an aggregate and returns one, so a
|
|
;;; single call crosses the boundary in both directions at once.
|
|
(defn step-pair [p Pair] Pair
|
|
(println "a1")
|
|
(set counter (+ counter 1))
|
|
(Pair {.a (+ (.a p) 1) .b (+ (.b p) (weigh-pair p))}))
|
|
|
|
(defn step-quad [q Quad] Quad
|
|
(Quad {.a (+ (.a q) 1) .b (+ (.b q) 2) .c (+ (.c q) 3)
|
|
.d (+ (.d q) (weigh-quad q))}))
|
|
|
|
(defn step-duo [d Duo] Duo
|
|
(Duo {.x (+ (.x d) 1.0) .y (+ (.y d) (f64 (weigh-duo d)))}))
|
|
|
|
(defn step-mix [m Mix] Mix
|
|
(Mix {.n (+ (.n m) 1) .z (+ (.z m) (f64 (weigh-mix m)))}))
|
|
|
|
;;; The reducers the host itself calls, so that what crosses back into C is an
|
|
;;; integer and the transcript is exact.
|
|
(defn sum-pair [p Pair] i64 (+ (.a p) (* 100 (.b p))))
|
|
|
|
(defn sum-quad [q Quad] i64
|
|
(+ (+ (.a q) (* 100 (.b q))) (+ (* 10000 (.c q)) (* 1000000 (.d q)))))
|
|
|
|
(defn sum-duo [d Duo] i64 (+ (i64 (.x d)) (* 100 (i64 (.y d)))))
|
|
|
|
(defn sum-mix [m Mix] i64 (+ (.n m) (* 100 (i64 (.z m)))))
|
|
|
|
;;; The call site that has to follow a reload: compiled once, into the host,
|
|
;;; and never rebuilt. If a redefined `step-pair' runs when the host calls
|
|
;;; this, the cell is doing its job — and doing it for a signature the two
|
|
;;; conventions disagree about.
|
|
(defn outer [] i64
|
|
(let [p (step-pair (Pair {.a 1 .b 2}))
|
|
q (step-quad (Quad {.a 1 .b 2 .c 3 .d 4}))
|
|
d (step-duo (Duo {.x 1.0 .y 2.0}))
|
|
m (step-mix (Mix {.n 1 .z 2.0}))]
|
|
(+ (+ (sum-pair p) (sum-quad q)) (+ (sum-duo d) (sum-mix m)))))
|