TP3/shell/tests/probe/modrm11.py

#!/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))