JosephFerano/flan
1
0
Fork 0
Code Issues Pull Requests Packages Projects Releases Wiki Activity

Form's image format, measured instead of assumed

Browse Source 
24 bytes, align 8, payload at offset 8. Those three numbers are the whole
agreement between the compiler and a dlopened macro -- the compiler writes a
Form into raw memory a field at a time and reads one back the same way -- and
they were written down in a handoff note and asserted nowhere. Nothing at run
time would notice a disagreement of one byte; the macro would simply return a
different form than it built.

So they go through the oracle the DWARF cases already use: ptrtoint of a
getelementptr through null, constant-folded by llc and read back out of the
.quad. The offsets and the size that oracle already answered. Alignment it did
not, and reading [2 x i64] out of the emitted type and concluding 8 would be
asserting the layout against itself -- the circularity BUILT.md rejected when
it turned down a _Static_assert. It is asked instead: the offset of field 1 in
{ i8, Form } is alignof(Form), because a member sits at the first offset its
own alignment allows.

Checked by breaking it both ways before restoring: 25 for the size and 16 for
the alignment each fail, and name which number moved.

The llc plumbing is now one run_oracle over a module of folded constants, with
llvm_members and llvm_align as the two questions asked through it.
This commit is contained in:
Joseph Ferano 2026-09-12 20:30:25 +07:00
parent 1ee54d6b56
commit 3ae2c089ec
1 changed files with 108 additions and 20 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

128
test/test_acceptance.ml
View File

@ -1966,28 +1966,24 @@ ERR@7 unexpected token: not the kind the caller was reading
(* LLVM's own answer, for the same struct type text the DWARF describes.
The type definitions are lifted straight out of the emitted module, so
there is no second spelling of the layout to get wrong. *)
let llvm_members ir sname nfields =
let tydefs =
lines_of ir
|> List.filter (fun l ->
String.length l > 0 && l.[0] = '%' && index_of l " = type " >= 0)
in
let sty = Printf.sprintf "%%\"%s\"" sname in
let b = Buffer.create 512 in
List.iter (fun l -> Buffer.add_string b (l ^ "\n")) tydefs;
for i = 0 to nfields - 1 do
Buffer.add_string b
(Printf.sprintf
"@o%d = constant i64 ptrtoint (ptr getelementptr (%s, ptr null, i32 0, i32 %d) to i64)\n"
i sty i)
done;
Buffer.add_string b
(Printf.sprintf
"@sz = constant i64 ptrtoint (ptr getelementptr (%s, ptr null, i32 1) to i64)\n"
sty);
(* The type definitions lifted straight out of an emitted module, so the
oracle never carries a second spelling of a layout. *)
let tydefs_of ir =
lines_of ir
|> List.filter (fun l ->
String.length l > 0 && l.[0] = '%' && index_of l " = type " >= 0)
|> List.map (fun l -> l ^ "\n")
|> String.concat ""
in
(* Hand LLVM a module of constant-folded ptrtoint expressions and read the
.quad it writes for each. Every layout question below is asked this way:
the answer comes from the backend that lays the type out, not from a
table written beside the code that would have to be wrong in the same
way to agree. *)
let run_oracle src =
let ll = Filename.concat scratch "flan-dwarf-oracle.ll" in
let asm = Filename.concat scratch "flan-dwarf-oracle.s" in
Out_channel.with_open_bin ll (fun ch -> Out_channel.output_string ch (Buffer.contents b));
Out_channel.with_open_bin ll (fun ch -> Out_channel.output_string ch src);
let llc = try Sys.getenv "FLAN_LLC" with Not_found -> "llc" in
let code =
Sys.command
@ -2026,6 +2022,40 @@ ERR@7 unexpected token: not the kind the caller was reading
Some (List.rev !acc)
end
in
(* Every member's byte offset and the whole type's size, LLVM's answer. *)
let llvm_members ir sname nfields =
let sty = Printf.sprintf "%%\"%s\"" sname in
let b = Buffer.create 512 in
Buffer.add_string b (tydefs_of ir);
for i = 0 to nfields - 1 do
Buffer.add_string b
(Printf.sprintf
"@o%d = constant i64 ptrtoint (ptr getelementptr (%s, ptr null, i32 0, i32 %d) to i64)\n"
i sty i)
done;
Buffer.add_string b
(Printf.sprintf
"@sz = constant i64 ptrtoint (ptr getelementptr (%s, ptr null, i32 1) to i64)\n"
sty);
run_oracle (Buffer.contents b)
in
(* Alignment, which no getelementptr states directly. Put the type after a
single byte and ask where it lands: a struct member sits at the first
offset its own alignment allows, so the offset of field 1 in
{ i8, T } *is* alignof(T). Reading [2 x i64] out of the emitted type and
concluding 8 would be asserting the layout against itself, which is the
circularity BUILT.md already rejected for _Static_assert. *)
let llvm_align ir sname =
let sty = Printf.sprintf "%%\"%s\"" sname in
let b = Buffer.create 512 in
Buffer.add_string b (tydefs_of ir);
Buffer.add_string b (Printf.sprintf "%%alignprobe = type { i8, %s }\n" sty);
Buffer.add_string b
"@al = constant i64 ptrtoint (ptr getelementptr (%alignprobe, ptr null, i32 0, i32 1) to i64)\n";
match run_oracle (Buffer.contents b) with
| None -> None
| Some qs -> List.assoc_opt "al" qs
in
(* The case itself: the DWARF a source text produces must agree with LLVM
on every member's offset, and on the struct's size. *)
let layout_case name src sname fields =
@ -2105,6 +2135,64 @@ ERR@7 unexpected token: not the kind the caller was reading
(defn main [] i32 (let [n (N.A {.x 3})] (match n (A x) x _ 1)))\n")
"N" [ "tag"; "payload" ];
(* -- Form: the one layout two programs have to agree on --------
Every layout above is checked because a debugger reads it. This one is
checked because the *compiler* reads it. A macro is compiled into a .so
and dlopened into the compiler, and the compiler then writes a Form into
raw memory a field at a time and reads one back the same way; nothing at
run time would notice if the two sides disagreed by a byte. The image
format is three numbers -- 24 bytes, align 8, payload at offset 8 -- and
the marshaller in lib/expand.ml is written to them, so here is where they
stop being an assumption.
They are not arbitrary. Form's widest cases are (Str [s string]) and
(List [xs [Form]]); a string and a slice are both ptr+len, 16 bytes at
align 8. So the tag is 4 padded to 8, the payload is 16, and the total
is 24. Adding a case with a wider member -- two f64s and a pointer, say
-- moves every one of these numbers, and this is what says so before the
first macro hands back a Form the compiler misreads. *)
let form_src =
"(defn shape [f Form] i32\n\
\ (match f (Int _n) 1 (Str _s) 2 (List xs) (i32 (len xs)) _ 0))\n\
(defn main [] i32 (shape (Form.Int {.i 1})))\n"
in
layout_case "DWARF offsets agree with LLVM: Form" form_src
"Form" [ "tag"; "payload" ];
(* The three numbers by name, so a failure says which one moved rather than
leaving it to be read out of an offset table. *)
(let ir = debug_ir form_src in
let want =
[ ("o0", 0, "the tag is at byte"); ("o1", 8, "the payload is at byte");
("sz", 24, "a Form is this many bytes wide:") ]
in
match llvm_members ir "Form" 2 with
| None -> Printf.printf "acceptance: Form's image format - llc unavailable, unchecked\n"
| Some oracle ->
List.iter
(fun (k, expect, what) ->
match List.assoc_opt k oracle with
| Some got when got <> expect ->
incr failures;
Printf.printf
"FAIL Form's image format\n %s %d, the marshaller says %d\n"
what got expect
| Some _ -> ()
| None ->
incr failures;
Printf.printf
"FAIL Form's image format\n the oracle gave no %s\n" k)
want;
(match llvm_align ir "Form" with
| Some 8 -> ()
| Some got ->
incr failures;
Printf.printf
"FAIL Form's image format\n align %d, the marshaller says 8\n" got
| None ->
incr failures;
print_endline
"FAIL Form's image format\n the oracle gave no alignment"));
(* Permuting the fields must actually move them. Asserting that the two
orderings disagree is what makes the two cases above a test: an offset
table that ignored declaration order would satisfy both. *)