#!/usr/bin/env python3 """modrm11.py -- check the mod=11 half of the 16-bit ModR/M table. Establishes the register identities for ModRM mod=11 by asking GNU `as` (.code16) to ENCODE the register moves, FCML to decode what came out, and requiring all of that to agree with both the hard-coded byte sequences below and the table recorded in Runtime.mod. See probe/modrm11.s for why the assembler is the right oracle here, and why the obvious qemu probe for this half cannot work. The table --------- ModRM is mod:b7b6 reg:b5b4b3 r/m:b2b1b0. In mod=11 both fields name a register, in the same order, with the same list: code 000 001 010 011 100 101 110 111 reg AX CX DX BX SP BP SI DI r/m AX CX DX BX SP BP SI DI Which of the two operands a field names depends on the opcode, and this is the part that has to be right or the whole table comes out shifted: 88 /r MOV r/m8, r8 89 /r MOV r/m16, r16 reg is the SOURCE 8A /r MOV r8, r/m8 8B /r MOV r16, r/m16 reg is the TARGET So for `movw %bx, %si` (AT&T: source BX, destination SI) the reg field is BX and the r/m field is SI -- and SI lands in the low three bits as 110. The memorable version of the r/m column drops AX off the front and invents a duplicate BX at the end, which shifts every code down by one cell. That is how "MovSiBx" came to be written 89 DC, which is MOV SP,BX. The shifted version gets 100 right by luck (SP is at 100 either way), so the error hides until you check a register below it, and every wrong byte still decodes cleanly -- a structural check and a disassembly golden both accept it. That is the entire reason this file exists. Non-vacuity ----------- Groups 1-3 of the .s compare that file against the assembler, which on its own cannot fail for a reason other than "someone edited the claims": edit the .s and the assembler faithfully re-encodes the new claim. Two things stop that. Every instruction's bytes are also hard-coded in EXPECT below, so editing the .s to contradict the table fails even though the encoder agrees. And group 4 of the .s is four anchors nobody types by hand -- ADD SP,8 / ADD SI,2 / MOV BP,SP / MOV SP,BP -- whose cells are asserted against the table directly, so a table shifted by one cell cannot satisfy them. Both failure modes are exercised by probe/README.md's non-vacuity runs. Usage: modrm11.py [-v] # -v prints the table """ import os import re import subprocess import sys HERE = os.path.dirname(os.path.abspath(__file__)) sys.path.insert(0, HERE) sys.path.insert(0, os.path.dirname(HERE)) # disasm16.py lives one level up import disasm16 # noqa: E402 SRC = os.path.join(HERE, "modrm11.s") # The word-form register list, used for BOTH the reg field and the r/m field # in mod=11. Index is the code. REG = ["Ax", "Cx", "Dx", "Bx", "Sp", "Bp", "Si", "Di"] # The 8-bit list, which differs from REG at index 4 only: AH, not SP. REG8 = ["Al", "Cl", "Dl", "Bl", "Ah", "Ch", "Dh", "Bh"] # Group boundaries in the .s, as (first, count). G_RM, G_REG, G_BYTE, G_ANCHOR = 0, 8, 16, 22 # The bytes every instruction in the .s must assemble to, in order. These are # the point of the file: they are asserted independently of the .s text, so # the .s cannot be edited into agreement with a wrong table. EXPECT = [ "89 D9", "89 DA", "89 DB", "89 DC", "89 DD", "89 DE", "89 DF", "89 DB", "89 C7", "89 CF", "89 D7", "89 DF", "89 E7", "89 EF", "89 F7", "89 FF", "88 C6", "88 F0", "88 C2", "88 D0", "88 C3", "88 D8", "83 C4 08", "83 C6 02", "8B EC", "8B E5", ] # The anchors, each with the decode its .s comment claims and the table cells # it pins. (index into REG, register). The opcode's reg field carries the # operation (/0 = ADD) for the first two, so only their r/m fields say # anything about the register list; the two MOV anchors pin both fields. ANCHORS = [ ("ADD SP, 8", "add sp,8h", [(4, "Sp")]), ("ADD SI, 2", "add si,2h", [(6, "Si")]), ("MOV BP, SP", "mov bp,sp", [(5, "Bp"), (4, "Sp")]), ("MOV SP, BP", "mov sp,bp", [(4, "Sp"), (5, "Bp")]), ] RE_INSN = re.compile(r"^\s*([a-z]+)\s+([^,]+),\s*([^#;]+?)\s*(?:#.*|;.*)?$") def build(): """assemble and objcopy, returning the .text bytes""" # scratch beside the tree, not in /tmp; HERE is shell/tests/probe tmp = os.path.normpath(os.path.join(HERE, "..", "..", "..", "tmp")) os.makedirs(tmp, exist_ok=True) o = os.path.join(tmp, "modrm11.o") b = os.path.join(tmp, "modrm11.bin") subprocess.run(["as", "--32", "-o", o, SRC], check=True) subprocess.run(["objcopy", "-O", "binary", "-j", ".text", o, b], check=True) with open(b, "rb") as f: return f.read() def source_instructions(): """the (mnemonic, src, dst) list the .s file asks for, in order. The four anchor instructions are literal .byte directives, so they do not appear here; they are checked from EXPECT and ANCHORS instead. """ out = [] with open(SRC) as f: for line in f: m = RE_INSN.match(line) if m and m.group(1) in ("movw", "movb"): # strip the AT&T sigils: FCML prints Intel order, without them out.append((m.group(1), m.group(2).strip().lstrip("%"), m.group(3).strip().lstrip("%"))) return out def decode_all(text, problems): """linear sweep, returning [(hexbytes, inteltext)] per instruction""" got = [] off = 0 while off < len(text): t, n = disasm16.decode(text[off:], off) if n == 0: problems.append("decode error at +%d (%s)" % (off, text[off:off + 6].hex(" ").upper())) break got.append((text[off:off + n].hex(" ").upper(), (t or "?").lower())) off += n return got def main(argv): verbose = "-v" in argv problems = [] want = source_instructions() if not want: print("FAIL: no instructions parsed out of %s" % SRC) return 1 if len(want) != len(EXPECT) - len(ANCHORS): print("FAIL: %s asks for %d mnemonic lines; EXPECT has %d entries " "less %d anchors" % (SRC, len(want), len(EXPECT), len(ANCHORS))) return 1 text = build() got = decode_all(text, problems) if len(got) != len(EXPECT): problems.append("assembled %d instructions, expected %d" % (len(got), len(EXPECT))) if problems: print("FAIL: %d problem(s)" % len(problems)) for p in problems: print(" - %s" % p) return 1 def field(i, shift): """the 3-bit ModRM field of instruction i""" return (int(got[i][0].split()[1], 16) >> shift) & 7 # --- the bytes must be the ones recorded here, not merely self-consistent for i, exp in enumerate(EXPECT): if got[i][0] != exp: # instructions at or past G_ANCHOR are literal .byte directives and # so have no source line to name them by label = (" ".join(want[i]) if i < G_ANCHOR else "anchor %d" % (i - G_ANCHOR)) problems.append("instruction %d (%s): assembled %s, expected %s" % (i, label, got[i][0], exp)) # --- every mnemonic line must decode to what the .s asked for --------- for i in range(G_ANCHOR): mne, src, dst = want[i] want_txt = "mov %s,%s" % (dst.lower(), src.lower()) if got[i][1] != want_txt: problems.append("instruction %d: asked for AT&T `%s %s, %s`, " "as+fcml gave Intel %r" % (i, mne, src, dst, got[i][1])) # --- group 1: the r/m column, low three bits, naming the DESTINATION -- for i in range(G_RM, G_RM + 8): mne, src, dst = want[i] c = field(i, 0) if REG[c].lower() != dst.lower(): problems.append("r/m %d: %s has ModRM r/m=%d, table says %s but " "the .s asked for %s" % (i - G_RM, got[i][0], c, REG[c], dst)) # --- group 2: the reg column, bits 5..3, naming the SOURCE ----------- for i in range(G_REG, G_REG + 8): mne, src, dst = want[i] c = field(i, 3) if REG[c].lower() != src.lower(): problems.append("reg %d: %s has ModRM reg=%d, table says %s but " "the .s asked for %s" % (i - G_REG, got[i][0], c, REG[c], src)) # --- group 3: the 8-bit list, and the direction the opcode implies --- for i in range(G_BYTE, G_BYTE + 6): mne, src, dst = want[i] op = int(got[i][0].split()[0], 16) if op not in (0x88, 0x8A): problems.append("byte move %d: opcode %02X, expected 88 or 8A" % (i - G_BYTE, op)) continue # 88 is MOV r/m8,r8 (r/m is the destination); 8A is MOV r8,r/m8 # (r/m is the source). The ModRM byte is identical either way, so # only the opcode says which way the data goes. rmf = field(i, 0) rmf_reg = dst if op == 0x88 else src if REG8[rmf].lower() != rmf_reg.lower(): problems.append("byte move %d: %s has r/m=%d, table says %s but " "the .s asked for %s" % (i - G_BYTE, got[i][0], rmf, REG8[rmf], rmf_reg)) # --- group 4: the anchors, against the table directly ---------------- # The anchors are literal .byte directives, so there is no source line to # cross-check: their bytes come from EXPECT and their decode comes from # here, and both are asserted. What they add is a table cell that this # file's author did not choose. for k, (label, want_txt, cells) in enumerate(ANCHORS): i = G_ANCHOR + k ghex, gtext = got[i] if gtext != want_txt: problems.append("anchor %s (%s): FCML decodes %r, the .s comment " "claims %r" % (label, ghex, gtext, want_txt)) for c, reg in cells: if REG[c].lower() != reg.lower(): problems.append("anchor %s (%s): ModRM code %d must be %s, " "table says %s" % (label, ghex, c, reg, REG[c])) if not any(REG[c].lower() == reg.lower() for c, reg in cells): problems.append("anchor %s (%s) pins no live cell -- the anchor " "has stopped testing anything" % (label, ghex)) if verbose: print("mod=11 r/m field. 89 is MOV r/m,r, so reg is pinned to BX and") print("the low three bits ARE the r/m code, naming the destination.") for i in range(G_RM, G_RM + 8): print(" r/m %03d asked %-4s %s code %d table %-4s %s" % (i - G_RM, want[i][2], got[i][0], field(i, 0), REG[field(i, 0)], "ok" if REG[field(i, 0)].lower() == want[i][2].lower() else "MISMATCH")) print("mod=11 reg field. rm is pinned to DI, bits 5..3 are the reg") print("code, and for 89 that is the source.") for i in range(G_REG, G_REG + 8): print(" reg %03d asked %-4s %s code %d table %-4s %s" % (i - G_REG, want[i][1], got[i][0], field(i, 3), REG[field(i, 3)], "ok" if REG[field(i, 3)].lower() == want[i][1].lower() else "MISMATCH")) print("8-bit mod=11: same shape, list differs at 100 (AH not SP),") print("and the opcode alone says which way the data goes.") for i in range(G_BYTE, G_BYTE + 6): print(" asked %-4s -> %-4s %s r/m %d = %s" % (want[i][1], want[i][2], got[i][0], field(i, 0), REG8[field(i, 0)])) print("anchors: encodings nobody types by hand, asserted against the") print("table. A table shifted by one cell cannot satisfy these.") for k, (label, _, cells) in enumerate(ANCHORS): i = G_ANCHOR + k print(" %-10s %-9s %-12s pins %s" % (label, got[i][0], got[i][1], ", ".join("%d=%s" % (c, reg) for c, reg in cells))) print("mod=11 table: %d r/m codes, %d reg codes, %d byte moves and %d " "anchors all agree -- as encoding, FCML decode, the hard-coded" % (8, 8, 6, len(ANCHORS))) print(" EXPECT bytes, and the table in Runtime.mod") if problems: print("FAIL: %d problem(s)" % len(problems)) for p in problems: print(" - %s" % p) return 1 print("PASS: mod=11 register identities match the table in Runtime.mod") return 0 if __name__ == "__main__": sys.exit(main(sys.argv))