Backend
The Fixpoint No Test Suite Can Check
Seth Wheeler Dev.to (EN Zone)
1 views
Code: Megapixel99/lambda-language
lm is a small low-level language with four independent backends: C, WebAssembly, ARM64, and bytecode for a VM. Its test suite is built around the fact that there are four of them. Every program runs through all four and the outputs are compared byte for byte against each other and against a recorded expectation, so a backend that gets something subtly wrong disagrees with three that do not.
That suite is at 94 tests: 22 lm programs and 10 examples across four backends each, 59 compile-error cases, and 3 legacy programs. It is a good suite; there is one property it cannot check at all.
Every one of those 94 tests runs a program that the JavaScript compiler built. A compiler written in lm that quietly disagreed with its own output would pass all 94, because nothing in the suite ever asks it to compile itself.
The property
stage2 emit-c.lm, compiled by the JavaScript compiler
stage3 emit-c.lm, compiled by stage2
stage4 emit-c.lm, compiled by stage3
stage3 and stage4 have to be identical. If they are, the compiler written in lm produces the same output whether it was built by the JavaScript compiler or by itself, which is what a bootstrap is supposed to establish.
$ ./selfhost/bootstrap.sh
fixpoint reached: stage3 and stage4 are byte-identical (7023 lines)
Getting there took four stages, each checked against the JavaScript it replaces rather than against a hand-written expectation. The lexer produces identical token streams on all 36 programs under all four backends; the parser produces identical syntax trees on the same 36; the emitter produces identical C, byte for byte. The checker returns the same accept-or-reject verdict on all 95 programs, 36 valid and 59 that must be rejected. Its messages match on 40 of 95, mostly in column numbers but in a handful of cases in wording, so the verdicts are exact and the diagnostics are not yet.
The corpus includes the lm files themselves, which is the part that makes the comparison worth anything: the parser reproduces the JavaScript parser's tree for its own 1,608-line source node by node, and the emitter writes the same C for the checker's 84 KB as the JavaScript backend does.
Three bugs the suite could not have found
The suite covers programs that fit on a screen. parser.lm is 1,608 lines and allocates megabytes. Each of the following was invisible to the first and unavoidable for the second.
ARM64 lost a register across memmove. The realloc copy path parked the new pointer in x4, which is caller-saved, so memmove was entitled to destroy it. There is a test covering the copy path and it passed, because the copy was eight bytes and memmove never touches x4 for something that small. The first copy large enough to matter was the token array in parser.lm reaching 64 entries, about 3 KB. Until it was fixed, every program over roughly eighty tokens failed to lex under ARM64 while the other three backends were correct.
That last clause is the interesting one. Four-way agreement is this project's whole claim to correctness, and here three backends agreed with each other and were right, one disagreed and was wrong, and no test in the suite was large enough to make the disagreement appear.
The compiler driver truncated large output. Node makes writes to a pipe asynchronous and process.exit() discards whatever is still buffered, so piping the VM's output produced 2,909 lines of 7,636 while the same run redirected to a file came out whole. Every test in the suite prints tens of lines. None of them could have noticed, and the failure is silent: you get a prefix of the right answer.
1 MiB could not hold a syntax tree. With no free, the flat memory region has to cover the sum of everything ever allocated rather than the peak live set, so a doubling array that reaches 512 KB has also left 256 KB and 128 KB behind it. Self-parsing needs about 2 MB. The region is 8 MiB now.
What the language made hard
Two of these are design consequences rather than bugs, and they are the ones I would want to know about before writing another language like this.
A growable arena and a stored address do not mix. p.nodes[n].c = parseBlock(p) is wrong; the reason is a rule lm deliberately guarantees: a store evaluates its address before its value. parseBlock allocates, allocation can move the arena, and the store lands in the block the arena used to occupy. This is not a language bug, and left-to-right evaluation is exactly what makes the four backends agree in the first place. The damage comes from the interaction with having no free: the old block is still readable, so the write appears to succeed and the field silently keeps its old value. Ten sites had that shape.
No sum types means one node layout for every kind, so the AST node has five payload fields whose meaning depends on kind, commented where they are written rather than where they are declared. C pays the same price, which was some comfort.
Why the fixpoint is a different instrument
A test suite asks whether a program produces the right answer. It is aimed outward, at the thing being compiled, and everything it knows about the compiler is inferred from the programs it produced. That inference is sound as long as the compiler under test is not also the thing producing the test inputs, and at the moment you self-host, it is.
The fixpoint asks a question with no reference answer at all. It does not check the emitted C against anything I wrote down. It checks that a compiler, run on its own source, produces something that when run on the same source produces the identical thing. Nothing external is trusted, which is why it survives being wrong about what the right answer is.
That is also its limit, and worth stating: a fixpoint does not prove the compiler is correct. A compiler that miscompiles some construct consistently, in a way that reproduces itself, is a fixpoint. The classic version of that is a compiler that has learned to insert a backdoor into its own successor. What the fixpoint establishes is self-consistency, which is a weaker property than correctness and completely independent of the one the 94 tests establish. Running both is not redundancy.
What generalises
The useful question is not "is my test suite big enough" but "what class of defect is my suite structurally unable to represent". Mine ran every program through four backends and compared them byte for byte, which sounds exhaustive, and it could not represent a program larger than a screen, an output longer than a pipe buffer, or a compiler compiling itself. Adding a ninety-fifth test of the same shape would not have moved any of those.
The three bugs above were found by one change of shape, not by more coverage: compile something big, written in the language, by the language. Every one of them had been sitting in a suite that passed.
bootstrap.sh and the per-stage comparisons are in the repository, and each check runs in one command.
Read original: https://dev.to/megapixel99/the-fixpoint-no-test-suite-can-check-31o4
← Previous
What's actually inside an image's DPI tag (and why changing it is lossless)
Next →
Posting from a shed with one bar of signal: an offline write queue in plain JS
Related
S
StyleSmuggler: Unpatched Magento Zero-Day Is Backdooring Stores Right Now
Backend
0
DEV Community
I
Is the Endpoint Free, or Just Unbilled?
Backend
0
DEV Community
A
API key design: entropy math, prefixes, and why sk_live_ is genius
Backend
0
Dev.to (EN Zone)
N
No, you can't decrypt a bcrypt hash — here's what to do instead
Backend
0
Dev.to (EN Zone)
Comments0
No comments yet — be the first