Merge branch 'worktree-agent-a03eb07b90913c874' into dev-loop
This commit is contained in:
commit
70e95119e9
159
HANDOFF-x86-aggregates.md
Normal file
159
HANDOFF-x86-aggregates.md
Normal file
@ -0,0 +1,159 @@
|
||||
# Handoff — the aggregate case across the reload boundary
|
||||
|
||||
Branch `dev-loop`, from `957ba07`. This closes item 4 of `HANDOFF-x86-redef.md`: a redefined function that
|
||||
takes and returns a struct, which is the one case the two backends' conventions disagree about and the reason
|
||||
`X86.redefinition` exists at all rather than reusing `Emit.redefinition`.
|
||||
|
||||
**The claim is now measured and it holds.** An `--x86` host dlopening `--x86` modules gets the right answer
|
||||
when four redefined functions each take a struct and return one. The same fixture, built and reloaded entirely
|
||||
through LLVM, prints the same transcript. And the crossed pair — an `--x86` host given LLVM-built modules —
|
||||
dies with SIGSEGV on the first such call, which is the measurement the "same-convention-by-construction"
|
||||
argument was standing in for.
|
||||
|
||||
## What was built
|
||||
|
||||
| file | what |
|
||||
|---|---|
|
||||
| `test/programs/reload-agg.flan` | the fixture. No `main`, so `test/reload_host.c` is the host, unchanged |
|
||||
| `test/programs/reload-agg-v2.flan` | the same four signatures with different arithmetic |
|
||||
| `test/test_reload.ml` | the aggregate section, run on both backends against one transcript, plus the two refusal checks |
|
||||
| `lib/build.ml` — `shared`, `shared_x86` | a symmetric refusal when the option record names the other backend. Two `failwith`s and their comments; nothing else in the file moved |
|
||||
|
||||
Nothing in `lib/x86.ml` was touched.
|
||||
|
||||
## The fixture, and why it is shaped this way
|
||||
|
||||
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, `check.ml`
|
||||
already refuses an aggregate in a `declare` signature, and it is not what is under test. `outer` returns `i64`
|
||||
and `counter` is `i64`, so `reload_host.c` needed no change at all.
|
||||
|
||||
Four struct shapes, because SysV treats them four different ways and `x86.ml` treats all four the same:
|
||||
|
||||
- `Pair` — two INTEGER eightbytes; SysV passes in `rdi`:`rsi` and returns in `rax`:`rdx`.
|
||||
- `Quad` — thirty-two bytes, so MEMORY.
|
||||
- `Duo` — two SSE eightbytes, `xmm0`:`xmm1`.
|
||||
- `Mix` — one INTEGER and one SSE.
|
||||
|
||||
Each of the four redefined `step-*` takes its struct and returns it, so a single call crosses the boundary in
|
||||
both directions. Each calls a `weigh-*` the module does *not* define, which hands an aggregate the other way —
|
||||
module to host — and doubles as the tripwire `reload.flan`'s `helper` is: v2's text for all four `weigh`
|
||||
functions multiplies by ten, and since a module declares a sibling rather than defining it, that text has to be
|
||||
dead. A module that grew its own copy would print 12411 where the expected transcript says 1611.
|
||||
|
||||
Every field is weighted by position in the answer (`a + 100b + 10000c + 1000000d`) 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.
|
||||
|
||||
The `defstruct` blocks are byte-identical between the two files and must stay that way. Layout is computed per
|
||||
module, so a field reordered in v2 would make host and module disagree about offsets — a real bug, but one
|
||||
wearing this test's clothes and indistinguishable in the transcript from the thing the fixture is for.
|
||||
|
||||
The arithmetic in the test is derived in a comment rather than read off a run, and both backends are held to
|
||||
the same string. The LLVM row is not decoration: a wrong expected number would otherwise be indistinguishable
|
||||
from a backend that is right, and two independently-built agreements on one transcript are what rule that out.
|
||||
|
||||
## The transcript
|
||||
|
||||
```
|
||||
a1
|
||||
host 54063108
|
||||
a1
|
||||
after1 54063108
|
||||
a2
|
||||
after2 104337044
|
||||
counter 12
|
||||
```
|
||||
|
||||
Identical from `Emit.redefinition` + `Build.shared` and from `X86.redefinition` + `Build.shared_x86`.
|
||||
`counter` is stepped from inside the redefined body — by one in v1, by ten in v2 — so 1 + 1 + 10 = 12 is the
|
||||
host's global written by three different bodies in turn.
|
||||
|
||||
## The mismatch, measured
|
||||
|
||||
The same run crossed: an `--x86` host, LLVM-built modules.
|
||||
|
||||
```
|
||||
FAIL cross aggregate reload
|
||||
got: "a1\nhost 54063108\na1\n" (exit 139)
|
||||
wanted: "a1\nhost 54063108\na1\nafter1 54063108\na2\nafter2 104337044\ncounter 12\n"
|
||||
```
|
||||
|
||||
Exit 139 is SIGSEGV. It dies on the first call into a redefined aggregate body, before `after1` is printed.
|
||||
|
||||
Note what this does and does not say. It says the crossed pair is fatal. It does **not** give a per-shape
|
||||
breakdown: `step-pair` is called first and kills the process, so `step-quad`, `step-duo` and `step-mix` never
|
||||
run under the crossed pair at all. Whether the MEMORY-return half of the matrix happens to coincide between the
|
||||
two conventions is still unmeasured, and would need four crossed runs isolating one `step` at a time. Nothing
|
||||
in this lane needs the answer; the four shapes earn their place as *all four cross correctly on a matched
|
||||
pair*, which is what was asked for.
|
||||
|
||||
This case is not in `dune test`. It is undefined behaviour, and what it prints is a property of whichever LLVM
|
||||
is installed; a test that pinned it would be pinning the shape of a crash.
|
||||
|
||||
## The serious finding: nothing refuses a mismatched pair, and the CLI can build one
|
||||
|
||||
There is no check anywhere that a redefinition module was built by the same backend as its host.
|
||||
`Build.shared` and `Build.shared_x86` are unrelated functions, neither looked at `opts.x86`, and the loaded
|
||||
object carries no mark saying which backend made it.
|
||||
|
||||
**It is reachable from the CLI, by a user doing nothing unusual.** `bin/main.ml:441` reads `--x86` for
|
||||
`flan build` only. `flan reload` (`bin/main.ml:506`–523) hardcodes `Build.shared` with
|
||||
`{ default with dev = true; debug }` and has no `--x86` spelling at all. So:
|
||||
|
||||
```
|
||||
flan build game.flan --x86 --dev -o game # an --x86 host, with cells
|
||||
flan reload game.flan changed.flan -o v2.so # an LLVM module, silently
|
||||
```
|
||||
|
||||
and the agent in `vendor/agent/flan_agent.c` dlopens `v2.so` into that host. If any redefined function in
|
||||
`changed.flan` takes or returns a struct, that is the exit-139 above, at a call site, in a running game, with
|
||||
nothing anywhere having said a word.
|
||||
|
||||
### What was done about it
|
||||
|
||||
`Build.shared` now refuses an option record with `x86` set, and `Build.shared_x86` refuses one without it, each
|
||||
naming the reason. Both refusals are asserted in `test/test_reload.ml`.
|
||||
|
||||
**That guard does not close the hole, and it was re-measured after landing to be sure.** The crossed run above
|
||||
passes both refusals — it hands `Build.shared` an honest LLVM option record and simply loads the result into an
|
||||
x86 host — and it still segfaults. The guard catches a caller holding *one* option record and reaching for the
|
||||
wrong builder, which is the accident a lane wiring item 3 would make. It cannot catch a caller holding two, and
|
||||
`flan reload` is exactly that caller.
|
||||
|
||||
### The recommended complete fix, not done here
|
||||
|
||||
A marker symbol. `X86.program` defines `flan.abi.x86` and `X86.redefinition` emits an undefined reference to
|
||||
it; `Emit.program` defines `flan.abi.llvm` and `Emit.redefinition` references that. A crossed pair then fails
|
||||
at `dlopen` with an undefined-symbol message naming the ABI, before a single instruction of the new body runs —
|
||||
the loader refusing the pair rather than the processor refusing it at a call. It costs one symbol in each of
|
||||
four functions and nothing at run time.
|
||||
|
||||
It was not done here because it needs edits in `lib/x86.ml`, which two other lanes are in, and because a
|
||||
refusal at the wrong moment is worse than a loud one slightly later. It should be done next, together with item
|
||||
3 of `HANDOFF-x86-redef.md` — when `flan dev` and `flan reload` learn to choose host and module backend
|
||||
together, the marker is what makes the choice checkable rather than merely intended.
|
||||
|
||||
## Baseline, before and after
|
||||
|
||||
| | before | after |
|
||||
|---|---|---|
|
||||
| `spike/x86/survey.sh` | 99 MATCH / 0 DIFFER / 0 REFUSED / 0 NOX86 | **99 / 0 / 0 / 0** |
|
||||
| skip breakdown | 28 does-not-compile / 6 no-main / 2 runs-forever | 28 / **8** / 2 |
|
||||
| `spike/x86/cells.sh` | 4/4 ok | **4/4 ok** |
|
||||
| `dune test --root .` | exit 0 | **exit 0** |
|
||||
|
||||
The `no-main` count moving from 6 to 8 is the two new fixtures existing: `survey.sh` globs
|
||||
`test/programs/*.flan`, and a program with no `main` fails the LLVM link and is classified there, before the
|
||||
x86 build is attempted. The MATCH count is what must not move, and it did not.
|
||||
|
||||
One thing to know if you re-run the survey to check this: the shell expands that glob once, when the loop
|
||||
starts. A survey launched before the fixtures were written will report 6 and look like a contradiction.
|
||||
|
||||
## What remains
|
||||
|
||||
- The marker symbol above, and item 3 of `HANDOFF-x86-redef.md` with it.
|
||||
- A per-shape crossed measurement, if anyone ever wants to know *which* of the four disagree and how. Four runs
|
||||
isolating one `step` at a time. Nothing depends on it.
|
||||
- Items 1, 2 and 5 of `HANDOFF-x86-redef.md`, untouched: the new-name path, the transient thunk, and items 2–7
|
||||
of `HANDOFF-x86-rt.md` §6.
|
||||
31
lib/build.ml
31
lib/build.ml
@ -879,6 +879,29 @@ let run what cmd =
|
||||
|
||||
let shared ?(opts = default) ~ir ~out () : timing =
|
||||
let opts = if opts.debug then { opts with opt = "-O0" } else opts in
|
||||
(* An [--x86] host must get [--x86] modules, and this is the one place that
|
||||
can say so cheaply. The two backends' conventions agree on every scalar
|
||||
and disagree on every aggregate, so a crossed pair links, loads, and then
|
||||
dies at the first call into a redefined function that takes or returns a
|
||||
struct — measured as SIGSEGV, in test_reload.ml's aggregate section. The
|
||||
option record is where the backend choice lives, so a builder handed the
|
||||
other backend's record refuses by name rather than producing that object.
|
||||
|
||||
Be clear about how little this catches, because a guard that reads wider
|
||||
than it is is worse than none. It catches a caller holding one option
|
||||
record and reaching for the wrong builder. It does not catch a caller
|
||||
holding two and picking the wrong one — the crossed pair that was measured
|
||||
segfaulting passes this check and still segfaults, because it hands an
|
||||
LLVM record to the LLVM builder and simply loads the result into an x86
|
||||
host. [flan reload] is precisely that caller. The complete answer is a
|
||||
marker symbol the host defines and a module references, so the loader
|
||||
refuses the pair at dlopen rather than the processor refusing it at a
|
||||
call. See HANDOFF-x86-aggregates.md. *)
|
||||
if opts.x86 then
|
||||
failwith
|
||||
"--x86: Build.shared is the LLVM redefinition path, and an --x86 host \
|
||||
must get --x86 modules — the two calling conventions disagree on every \
|
||||
aggregate. Use Build.shared_x86 with X86.redefinition.";
|
||||
if wasm_target opts then
|
||||
failwith
|
||||
((if web_target opts then "web" else "wasm32")
|
||||
@ -928,6 +951,14 @@ let shared ?(opts = default) ~ir ~out () : timing =
|
||||
let assembler = try Sys.getenv "FLAN_AS" with Not_found -> "as"
|
||||
|
||||
let shared_x86 ?(opts = default) ~asm ~out () : timing =
|
||||
(* The other half of the same guard, and it is the half that costs nothing to
|
||||
get right: a module built here for a host that was built by LLVM is the
|
||||
same mismatch seen from the other side. *)
|
||||
if not opts.x86 then
|
||||
failwith
|
||||
"Build.shared_x86 is the --x86 redefinition path and was handed an LLVM \
|
||||
option record — an --x86 host must get --x86 modules, and an LLVM host \
|
||||
must get LLVM ones. Set [x86] on the options, or use Build.shared.";
|
||||
let dir = workdir () in
|
||||
let base = Filename.remove_extension (Filename.basename out) in
|
||||
let src = Filename.concat dir (base ^ ".s") in
|
||||
|
||||
69
test/programs/reload-agg-v2.flan
Normal file
69
test/programs/reload-agg-v2.flan
Normal file
@ -0,0 +1,69 @@
|
||||
;;;; The aggregate case across the reload boundary, v2.
|
||||
;;;;
|
||||
;;;; The same four signatures with different arithmetic, so that the host's
|
||||
;;;; un-rebuilt `outer' printing a different number can only mean its call
|
||||
;;;; sites followed four redefined bodies that take and return structs.
|
||||
;;;;
|
||||
;;;; The `defstruct' blocks are byte-identical to v1's and must stay that way.
|
||||
;;;; Layout is computed per module, so a field reordered here would make the
|
||||
;;;; host and the module disagree about offsets — a real bug, but one wearing
|
||||
;;;; this test's clothes, and it would be indistinguishable in the transcript
|
||||
;;;; from the convention mismatch the fixture exists to detect.
|
||||
;;;;
|
||||
;;;; The four `weigh' functions are changed and the change must be dead text: a
|
||||
;;;; module declares a sibling rather than defining it, so each call has to
|
||||
;;;; land on the host's copy. With the bodies identical nothing at run time
|
||||
;;;; would notice a module that grew its own; multiplied by ten, it is the
|
||||
;;;; difference between 1611 and 12411 in the first term alone.
|
||||
;;;;
|
||||
;;;; Nothing here introduces a name the host was not built with. X86.redefinition
|
||||
;;;; refuses those by name — that is the registry path, and it is item 1 of
|
||||
;;;; HANDOFF-x86-redef.md's "what remains" rather than anything to do with
|
||||
;;;; aggregates.
|
||||
|
||||
(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])
|
||||
|
||||
(defvar counter i64)
|
||||
|
||||
(defn weigh-pair [p Pair] i64 (+ (.a p) (* 30 (.b p))))
|
||||
|
||||
(defn weigh-quad [q Quad] i64
|
||||
(+ (+ (.a q) (* 30 (.b q))) (+ (* 50 (.c q)) (* 70 (.d q)))))
|
||||
|
||||
(defn weigh-duo [d Duo] i64 (+ (i64 (.x d)) (* 30 (i64 (.y d)))))
|
||||
|
||||
(defn weigh-mix [m Mix] i64 (+ (.n m) (* 30 (i64 (.z m)))))
|
||||
|
||||
(defn step-pair [p Pair] Pair
|
||||
(println "a2")
|
||||
(set counter (+ counter 10))
|
||||
(Pair {.a (+ (.a p) 10) .b (+ (.b p) (* 2 (weigh-pair p)))}))
|
||||
|
||||
(defn step-quad [q Quad] Quad
|
||||
(Quad {.a (+ (.a q) 10) .b (+ (.b q) 20) .c (+ (.c q) 30)
|
||||
.d (+ (.d q) (* 2 (weigh-quad q)))}))
|
||||
|
||||
(defn step-duo [d Duo] Duo
|
||||
(Duo {.x (+ (.x d) 10.0) .y (+ (.y d) (f64 (* 2 (weigh-duo d))))}))
|
||||
|
||||
(defn step-mix [m Mix] Mix
|
||||
(Mix {.n (+ (.n m) 10) .z (+ (.z m) (f64 (* 2 (weigh-mix m))))}))
|
||||
|
||||
(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)))))
|
||||
|
||||
(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)))))
|
||||
101
test/programs/reload-agg.flan
Normal file
101
test/programs/reload-agg.flan
Normal file
@ -0,0 +1,101 @@
|
||||
;;;; 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)))))
|
||||
@ -252,6 +252,130 @@ let () =
|
||||
| _ -> fail "x86 redefinition accepted a name the host does not have"
|
||||
| exception X86.Unsupported _ -> ());
|
||||
|
||||
(* The aggregate case, which is the whole reason X86.redefinition exists
|
||||
rather than an --x86 host dlopening what Emit.redefinition made.
|
||||
|
||||
Everything above this point is scalar, and scalars are the half of the
|
||||
calling convention the two backends cannot disagree about. They disagree
|
||||
on every aggregate: x86.ml passes each one by pointer and returns it
|
||||
through a hidden sret, LLVM classifies per eightbyte. So a redefined
|
||||
function taking or returning a struct is the case that would expose a
|
||||
mismatch, and until now the claim that an --x86 host plus --x86 modules
|
||||
is same-convention-by-construction was an argument rather than a
|
||||
measurement.
|
||||
|
||||
programs/reload-agg.flan crosses the boundary in four shapes at once —
|
||||
two integer eightbytes, thirty-two bytes of MEMORY, two SSE eightbytes,
|
||||
and one of each — because SysV treats those four differently and this
|
||||
backend treats them identically, so a single shape would measure a
|
||||
quarter of the disagreement and read like all of it. Each `step' takes
|
||||
an aggregate and returns one, so a single call crosses in both
|
||||
directions, and each calls a `weigh' the module does not define, which
|
||||
hands an aggregate the other way.
|
||||
|
||||
Both backends run the same fixture and are compared against the same
|
||||
transcript. The LLVM row is not decoration: a wrong expected number
|
||||
would otherwise be indistinguishable from a backend that is right, and
|
||||
two independently-built agreements on one string are what rule that
|
||||
out. *)
|
||||
let a1 = checked "programs/reload-agg.flan" in
|
||||
let a2 = checked "programs/reload-agg-v2.flan" in
|
||||
let agg_known =
|
||||
let names =
|
||||
List.map (fun (f : Tast.fn) -> f.Tast.name) a1.Tast.fns
|
||||
@ List.map (fun (g : Tast.global) -> g.Tast.gname) a1.Tast.globals
|
||||
in
|
||||
fun n -> List.exists (String.equal n) names
|
||||
in
|
||||
let agg_fns = [ "step-pair"; "step-quad"; "step-duo"; "step-mix" ] in
|
||||
(* The arithmetic, derived rather than observed, because a number read off
|
||||
a run is a record of what happened and not a statement of what should:
|
||||
|
||||
v1 Pair {1,2} -> weigh 1+3*2 = 7, so {2, 2+7} and 2 + 100*9 = 902
|
||||
Quad {1,2,3,4} -> weigh (1+6)+(15+28) = 50, so {2,4,6,54} and
|
||||
2 + 400 + 60000 + 54000000 = 54060402
|
||||
Duo {1,2} -> weigh 7, so {2.0, 9.0} and 902
|
||||
Mix {1,2} -> weigh 7, so {2, 9.0} and 902
|
||||
total 54063108
|
||||
v2 Pair -> weigh is still the *host's* 7, so {11, 2+14} and 1611
|
||||
Quad -> weigh still 50, so {11,22,33,104} and
|
||||
11 + 2200 + 330000 + 104000000 = 104332211
|
||||
Duo -> {11.0, 16.0} and 1611
|
||||
Mix -> {11, 16.0} and 1611
|
||||
total 104337044
|
||||
|
||||
1611 rather than 12411 in the first term is the tripwire: v2's text for
|
||||
`weigh-pair' multiplies by thirty, and a module that grew its own copy
|
||||
of a sibling rather than reaching the host's through a cell would say
|
||||
so here. `counter' is stepped from inside the redefined body, by one in
|
||||
v1 and by ten in v2, so 1 + 1 + 10 = 12 is the host's global being
|
||||
written by three different bodies in turn. *)
|
||||
let agg_want =
|
||||
"a1\nhost 54063108\na1\nafter1 54063108\na2\nafter2 104337044\n\
|
||||
counter 12\n"
|
||||
in
|
||||
let agg_run label opts mkmod =
|
||||
let h = tmp ("agg-host-" ^ label) in
|
||||
ignore
|
||||
(Build.executable ~opts ~csrcs:[ "reload_host.c" ] ~lflags:[ "-ldl" ]
|
||||
a1 ~out:h);
|
||||
let m1 = mkmod a1 ("agg-" ^ label ^ "-1.so") in
|
||||
let m2 = mkmod a2 ("agg-" ^ label ^ "-2.so") in
|
||||
let o = tmp ("agg-out-" ^ label) and e = tmp ("agg-err-" ^ label) in
|
||||
let code =
|
||||
Sys.command
|
||||
(Printf.sprintf "%s %s %s > %s 2> %s" (Filename.quote h)
|
||||
(Filename.quote m1) (Filename.quote m2) (Filename.quote o)
|
||||
(Filename.quote e))
|
||||
in
|
||||
let text = In_channel.with_open_bin o In_channel.input_all in
|
||||
if code <> 0 || text <> agg_want then
|
||||
fail "%s aggregate reload\n got: %S (exit %d)\n wanted: %S"
|
||||
label text code agg_want;
|
||||
List.iter (fun p -> try Sys.remove p with Sys_error _ -> ())
|
||||
[ h; m1; m2; o; e ]
|
||||
in
|
||||
agg_run "llvm" dev (fun q name ->
|
||||
let o = tmp name in
|
||||
let ir = Emit.redefinition ~dev:true ~known:agg_known q ~fns:agg_fns in
|
||||
ignore (Build.shared ~opts:dev ~ir ~out:o ());
|
||||
o);
|
||||
agg_run "x86" x86 (fun q name ->
|
||||
let o = tmp name in
|
||||
let asm =
|
||||
X86.redefinition ~checks:true ~dev:true ~known:agg_known q ~fns:agg_fns
|
||||
in
|
||||
ignore (Build.shared_x86 ~opts:x86 ~asm ~out:o ());
|
||||
o);
|
||||
(* The mismatch, which is the same measurement run crossed. An --x86 host
|
||||
given LLVM-built modules dies with SIGSEGV on the first call into a
|
||||
redefined aggregate body — measured, not argued:
|
||||
|
||||
got: "a1\nhost 54063108\na1\n" (exit 139)
|
||||
|
||||
That is not asserted here. It is undefined behaviour and what it prints
|
||||
is a property of whichever LLVM is installed; a test that pins it would
|
||||
be pinning the shape of a crash.
|
||||
|
||||
What is asserted is narrower, and the gap between the two is the finding
|
||||
rather than a caveat on it: [Build.opts] is where the backend choice
|
||||
lives, so a builder handed the *other* backend's option record refuses.
|
||||
The crossed run above passes both refusals — it hands [Build.shared] an
|
||||
LLVM record and never calls [Build.shared_x86] at all — and it still
|
||||
segfaults with this guard in place, re-measured after it landed. The
|
||||
guard catches a caller holding one option record; it cannot catch a
|
||||
caller holding two, and [flan reload] is exactly that caller. See
|
||||
HANDOFF-x86-aggregates.md. *)
|
||||
(match Build.shared ~opts:x86 ~ir:"" ~out:(tmp "never.so") () with
|
||||
| _ -> fail "Build.shared accepted an --x86 option record"
|
||||
| exception Failure m when has m "--x86" -> ()
|
||||
| exception Failure m -> fail "Build.shared refused for the wrong reason: %s" m);
|
||||
(match Build.shared_x86 ~opts:dev ~asm:"" ~out:(tmp "never.so") () with
|
||||
| _ -> fail "Build.shared_x86 accepted an LLVM option record"
|
||||
| exception Failure m when has m "--x86" -> ()
|
||||
| exception Failure m ->
|
||||
fail "Build.shared_x86 refused for the wrong reason: %s" m);
|
||||
|
||||
(* The layout-drift guard, which needs a process of its own because what it
|
||||
does is abort one. [extra] does not exist in the host: v3 introduced it
|
||||
at run time, so flan_dev.c allocated its storage and recorded its size,
|
||||
|
||||
Loading…
x
Reference in New Issue
Block a user