Font: Spacing: Letters: Width:

Two Readers, and Then One of Them Poisoned

22 minadvancedModule 2: The Encoding: What the Bytes AreContinues from a64-cond

22 min · AArch64: Encoding From The Ground Up

Why this matters

The four concepts before this one made a lot of claims. Some of them were wrong — the class field was two bits, the 64-bit all-ones was encodable, the op2 cells were SET forms — and being wrong about a bit pattern is the cheap kind of wrong, because a wrong bit pattern is visibly wrong to anyone who checks it.

The expensive kind is the one this concept is about. Claim R15 in this course's own artifact says that the logical-immediate model was printing sp where the encoding says the zero register — and the word that a reader would check is a word that does not exist in the instruction. The decoder produced a plausible instruction. Nothing crashed, nothing warned, and the output looked like a disassembly.

That class of bug cannot be found by reading your own code twice. It is found by a second reader that was not written by the same hand, and — this is the part that is easy to skip and that this course insists on — the second reader is found by poisoning the first.

Two readers, and what they agree on

Every instruction in the corpus is decoded twice: once by the model chain, once by llvm-objdump-21 --triple=aarch64. Both are the same kind of thing and the two were not written by the same person.

$ ./a64dec.py --section=12 | sed -n '/object files/,/agreement/p'
  5 object files, 868 instructions, 859 named by this decoder,
  9 left unmodelled and counted.

    the two readers agree on:   859
    the two readers disagree:    0
    agreement:                   100.0000% of named instructions

Three things to take from those five lines.

868 instructions, of which this decoder names 859. The other 9 are Advanced SIMD, out of the declared subset, and they are counted rather than dropped. The agreement figure is over the 859 — named, not total — and a cross-check that quietly excluded unmodelled words and reported the exclusion nowhere would be claiming a number about a smaller set than it appeared to.
0 disagreements. Which is correct and which is also exactly what a broken cross-check looks like, and the rest of this page is about the difference.
100.0000% is printed with four decimals because the precision is the point: a number printed to two places would have been 100% with room to hide a disagreement in the rounding.

The seven normalisations, and why each one exists

The two readers agree on the word and rarely agree on the string, and every reason is a printing decision rather than a decoding decision. All seven are listed in the artifact because a cross-check that quietly normalises away a real disagreement is worse than no cross-check — you cannot tell which of your normalisations is hiding a bug unless you can see all of them.

A trailing // =1234 comment, which is the disassembler doing arithmetic a byte-level decoder does not do.
A tab between mnemonic and operands, and a space after every comma.
A symbol annotation // <sym> and a resolved address after a branch, an adr or an adrp. In a relocatable object that number is a placeholder and the real value is in an R_AARCH64_* relocation, so both sides are compared as TARGET and the displacement arithmetic is checked by hand in section 11 instead. A placeholder that both readers print identically is not a cross-check of anything.
Small immediates printed in decimal by one reader and in hex by the other, so every immediate is folded to one form.
A zero offset, which the disassembler prints as a pronoun — [x1] for [x1, #0] — and which this decoder always prints, because a decoder that omits a field it read is a decoder whose output cannot be audited.
add x0, x1, #0x1000 against add x0, x1, #0x1, lsl #12, which concept 1 measured to be the same 32 bits, folded onto the value. And told to by a register shift — add x0, x0, x0, lsl #48 — which looks identical and is not, so the fold applies only where a # precedes the shift.
The sign of an immediate, which three printers disagree about. MOVN prints the register's value (the field's complement); a logical immediate that became a MOV alias prints signed; MOVZ prints unsigned. So every #-0x... is folded onto the unsigned value at the register width.

Rule 7 is nine of the eleven failures described below, and rule 3 is the one that would have been a lie: comparing a relocation placeholder is not a weaker check, it is no check, and the file says so rather than printing a green tick for it.

98.72%, and why that was the most useful output in the file

The first run of this comparison reported 848 of 859. The eleven failures were the most valuable lines the artifact ever printed, and they were of two different kinds:

Two were a real bug in the decoder. The logical-immediate model called the register-name function with its default permission, so register 31 printed as sp where the encoding says the zero register. orr x9, sp, #0x8000000000000001 for a word the disassembler calls mov x9, #-0x7fffffffffffffff. That is not a naming difference: a logical OR against the stack pointer is a different VALUE from a logical OR against zero. The decoder wrote down a register that does not exist in that instruction. (A flag with a default is a flag nobody checks. R15.)
Nine were a normalisation rule that had been matching nothing. The MOVN fold was written as ^movn([\w,]*),#... and [\w,]* does not match the space between a mnemonic and its operands. It matched nothing, silently, and the cross-check carried on running and printed its number. A rewrite that matches nothing is the kind of bug a check cannot report, because a check that reports 11 failures and a check that reports 100% both look like working software.

So the general form, which is the whole argument of this concept: 100% is what a check that has been normalised until it cannot fail looks like, and so is a check whose normalisation was quietly broken. The only way to tell the two apart is to look at what the failures were, which is why the history is printed rather than fixed in silence.

And a rule 6 that was green while being wrong

Worth one paragraph on its own, because it is the purest example in the collection. Rule 6 folds ,lsl#12 into the preceding value, and the first version applied it to every,lsl#N — including register shifts. One branch of that fold turned a register name into a number, so:

    add x0, x0, x0, lsl #48      cross-checked as   add x0, x0, #0x3000000

  The cross-check ran, reported 100% agreement, and was comparing
  a REGISTER against a CONSTANT.

The poison: the control that cannot fail is not a control

Agreement to 100% is what a broken cross-check looks like, so the model table is then broken on purpose, the same bytes go through the same loop, and the number is read again.

$ ./a64dec.py --section=12 | sed -n '/largest model/,/control doing its job/p'
  The largest model in the corpus is m_ldst_uimm, and it alone claims 142
  words.  A representative word it claims is 0xb9400820, which is
  `ldr	w0, [x1, #0x8]` -- asked of the oracle, not of this file.

    with the table intact:              ldr      w0, [x1, #8]
    with m_ldst_uimm poisoned:     (op 0xb9400820)  Loads and Stores

    the cross-check BEFORE the poison: 859 agree, 0 disagree, of 859
    the cross-check AFTER  the poison: 717 agree, 0 disagree, of 717

    VERDICT: the number MOVED, by 142 instructions, which is the
    control doing its job.  The unpoisoned agreement was read off
    this decoder and not off something else.

Read the two numbers, because the arithmetic is the evidence. The poison removed one model, so 142 words stopped being named; 859 − 142 = 717, and 717 − 717 = 0. The cross-check did not disagree about anything — it agreed about strictly fewer things, and exactly the things the poison touched. That is the shape a real bug has. A broken loop moves everything or nothing; a real corruption moves a localisable set.

And the first version of the poison was a no-op, which is the most instructive failure in this section. It prepended a model that claims nothing instead of removing one, so the victim was still in the list and still claimed every word it had claimed before. The number was 859 before and 859 after, and the line above it said the word POISONED. A control that cannot move the number it is measuring is not a control — it is a comment that says the word POISONED.

What the two readers share, which is a real weakness

Both readers ultimately come from one LLVM tree, because clang assembled the corpus and llvm-objdump-21 disassembled it. An independent second assembler does not exist on this host and GNU binutils has no AArch64 target installed. So the cross-check establishes that this decoder and one other piece of software agree on what the bytes mean — not that either agrees with silicon. Section 15 of the artifact says so again in its own words, and the landing page's limits block says it a third time. Three times is not redundancy; it is the number of places a reader is likely to stop reading.

There is one more limitation with a name, and it cost this course a whole afternoon: llvm-objdump in this collection has no -b binary option.--triple=aarch64 -D -b binary f prints error: unknown argument '-b'. The ISA course's harness uses GNU objdump, which does have it, so the technique worked there and does not work here. Every single-word probe in this artifact is therefore assembled into a real object file and asked about in a section the disassembler already knows how to read. A cross-check that quietly substituted a different disassembler for the convenience of a script would have been a claim about a tool that is not installed.

Three things that are cheaper to state than to prove

Each was asserted in a draft of this course. Each was measured. Each was retracted in public, and the history is printed by the artifact rather than fixed in silence.

98.72% was the most useful output in the file. The eleven disagreements were two real decoder bugs and nine failures of a normalisation rule that had been matching nothing. A check that reports eleven and a check that reports 100% both look like working software; the difference is a list you can read and a tick you cannot.
100% is what a broken cross-check looks like, so the control has to be able to fail. The first poison prepended a no-op model instead of removing one, the number did not move, and the line above it said POISONED. A control that cannot move the number it is measuring is a comment that says the word POISONED.
Both readers come from one LLVM tree.clang assembled the corpus and llvm-objdump-21 disassembled it, GNU binutils has no AArch64 target installed, and there is no second assembler on this host. The cross-check establishes that two programs agree about the bytes — not that either agrees with the silicon. This is said in three places, which is not redundancy: it is the number of places a reader stops reading.

Worked: the harness

crosscheck.py reads the recorded output and re-asks the claims. It does not re-measure anything: it has no assembler, no object files and no decoder of its own, and that is deliberate. A harness that can re-measure can disagree with the artifact for reasons that have nothing to do with whether the artifact's sentences are still true, and then it teaches its reader to ignore it.

So the split is this. a64dec.py runs the toolchain and produces numbers. crosscheck.py reads the numbers and asserts what must be true of them. A compiler upgrade changes the numbers and the harness notices; a prose edit that drops a retraction changes the text and the harness notices. Neither can hide.

$ python3 crosscheck.py courses/a64asm/assets/samples/a64dec.out
  ... 243 checks in 15 groups
  ========================================================================
  all 243 checks passed
  ========================================================================

Almost everything the artifact prints is exact — bit patterns, counts, assembler refusals, the reach of a signed displacement field — so the harness asserts those as exact numbers, and it is not being clever, it is the only honest thing to do with an exact quantity. Three things are worth reading about the harness itself:

It asserts all seventeen retractions as text. A course that quietly dropped one would pass every other check in the file, because the retraction is a claim about a number that is otherwise fine. Presence is asserted, in order, R1 to R17 with no gap.
It asserts the density comparison as a SHAPE, not a value. The four ratios come from one compiler version and a compiler upgrade moves them, so the harness asserts that the sign changes between -O0 and -O1 — which is the finding — and not what any of the four numbers is. A check whose threshold is a bare number is a check that fails on a busier machine and teaches its reader to ignore it.
It asserts that the poison moved the number. A harness that only ever reads the 100% is the harness this course retracted in R14 and R17, and a harness that has retracted something should not commit the same mistake in its own code.

And the reason the harness ships the recorded run: a course whose claims can only be verified by first rebuilding its own artifact is a course whose claims are only verifiable on the machine that wrote them — which is the same mistake as quoting a remembered number, wearing a different hat. a64dec.out, fields.txt, run1.txt and run2.txt are all committed, and the two runs are byte-identical.

Apply it

Break a guard by one bit and watch the poisoned number move. This is the manifest's completion criterion. In a64dec.py, in m_logical_imm, change reg(rn, sf, allow_sp=False, allow_zr=True) to reg(rn, sf) — the exact mistake R15 records. (Expect the cross-check to report 2 disagreements, both of the form orr x9, sp, #... against mov x9, #..., and expect the poison verdict to stay green because the poison moved by the same 142 either way. Then change the poison itself: replace the victim replacement with a prepend, and expect the verdict line to read DID NOT MOVE. You have now broken the cross-check and the control in the two ways that matter, and the second one is the one that would have shipped.)
Break a normalisation rule and notice what you cannot see. In normalise_objdump, change the MOVN rule's class from [\w,\s] back to [\w,]. (Expect the cross-check to report 0 disagreements, because the broken rule matches nothing and the artifacts both fall through to the same normalisation — and expect section 12 to keep printing 100.0000%. You have just reproduced the nine failures of the first run, and nothing in the output will tell you. That is why the rules are listed rather than trusted, and why R17 exists.)
Count the disagreements your own cross-check would miss. Take the 9 unmodelled words in the corpus and ask what happens to each of them in your pipeline. (Expect nothing to happen: they are counted, they are outside the declared subset, and the agreement figure is over the 859 named ones rather than the 868 total. Now subtract them instead and report 859/859 as 100% — and notice that a reader of that sentence has been told a different thing from a reader of the real one. The distinction between “agrees on everything it models” and “agrees on everything” is four numbers long and it is the whole difference.)

Connect

Backwards, all four concepts, and specifically concept 4: the cset inversion produces output that is 0 or 1 either way, and this is the only instrument in the collection that finds it. Concept 2 is where the register-31 mistake lived and where the field map that made it visible is measured.

Outward, and the models here are the ones the rest of this collection is built on. The x86-64 map audit is the same experiment on a variable-length encoding — 768 opcode slots read twice, with and without a prefix — and it has the same structure: a table, a second reader, and a control. The ISA course's decoder is the ancestor of this artifact's, and the difference in their declared subsets is the difference between a subset of lengths and a subset of names. The execution course's harness and the privilege course's are the other two verification models this one is a fourth instance of, and all three were written by a hand that had already broken a harness.

Forward, and this course ends here — the next link in the chain is not another AArch64 concept. Everything on the previous four pages is checkable with a hex editor, which is the design: a bit pattern, a count of bit patterns, an arithmetic identity, and a refusal from a real assembler do not go stale when a compiler changes and do not need a machine to verify. The parts of the chain that need silicon — whether a select is cheaper than a branch, whether a load hits, whether a bitfield is one instruction or two — are somebody else's course, and this one says in section 15 exactly which ones they are.

Keyboard Shortcuts