|
@@ -23,6 +23,7 @@ manual, not guessed.
|
|
|
| Execution: a boot sector, qemu, and a claim about behaviour | `v-TP3-EXECUTION` | done, **21/21 fixtures run, exact output** |
|
|
| Execution: a boot sector, qemu, and a claim about behaviour | `v-TP3-EXECUTION` | done, **21/21 fixtures run, exact output** |
|
|
|
| Execute the nine fixtures that only compiled | `v-TP3-DEAD-FIXTURES` | done, **30/30 run; four operator/scoping bugs found** |
|
|
| Execute the nine fixtures that only compiled | `v-TP3-DEAD-FIXTURES` | done, **30/30 run; four operator/scoping bugs found** |
|
|
|
| Runtime entries under qemu, and the register contract stated | `v-TP3-BP-CONTRACT` | done, **36/36 entry checks; `wrchar`/`wrbool` no longer destroy BP** |
|
|
| Runtime entries under qemu, and the register contract stated | `v-TP3-BP-CONTRACT` | done, **36/36 entry checks; `wrchar`/`wrbool` no longer destroy BP** |
|
|
|
|
|
+| 8086-legal conditional branches and `SETcc` | `v-TP3-8086-LOWERING` | done, **the emitted code no longer contains an opcode the 8086 lacks** |
|
|
|
| `CmdRun` (the `R` key), in-process 8086 interpreter | — | **not started** |
|
|
| `CmdRun` (the `R` key), in-process 8086 interpreter | — | **not started** |
|
|
|
|
|
|
|
|
Every row that names a tag has one, and every tag points at a commit on
|
|
Every row that names a tag has one, and every tag points at a commit on
|
|
@@ -219,14 +220,19 @@ by building it and requiring the check to stay green.
|
|
|
### Execution under qemu — `tests/run_com_exec.py`
|
|
### Execution under qemu — `tests/run_com_exec.py`
|
|
|
|
|
|
|
|
The sixth check is the one that cannot be written as a byte comparison, so it
|
|
The sixth check is the one that cannot be written as a byte comparison, so it
|
|
|
-is also the one that finds the most: 30 fixtures are compiled to `.COM`, put on
|
|
|
|
|
|
|
+is also the one that finds the most: 31 fixtures are compiled to `.COM`, put on
|
|
|
a floppy, booted, and their serial output compared to a committed `.out` file
|
|
a floppy, booted, and their serial output compared to a committed `.out` file
|
|
|
**exactly** — CRLF included — plus the exit code passed to `INT 21h AH=4Ch`.
|
|
**exactly** — CRLF included — plus the exit code passed to `INT 21h AH=4Ch`.
|
|
|
|
|
|
|
|
```
|
|
```
|
|
|
-execution: 30 passed, 0 failed (of 30)
|
|
|
|
|
|
|
+execution: 31 passed, 0 failed (of 31)
|
|
|
```
|
|
```
|
|
|
|
|
|
|
|
|
|
+It also found bug 33 — the branch polarity inverted in *every* conditional in
|
|
|
|
|
+*every* program — while the compile matrix and the `.COM` layout check were both
|
|
|
|
|
+perfectly happy. That is the third time in a row that a fault passed every
|
|
|
|
|
+byte-level check in this file and was caught only here.
|
|
|
|
|
+
|
|
|
The two fixtures it found nothing in are the interesting ones: `t31_procparam`
|
|
The two fixtures it found nothing in are the interesting ones: `t31_procparam`
|
|
|
and `t32_forexit` were the two most expensive bugs in the project, and neither
|
|
and `t32_forexit` were the two most expensive bugs in the project, and neither
|
|
|
was visible as a wrong byte count. See `overProc` below.
|
|
was visible as a wrong byte count. See `overProc` below.
|
|
@@ -248,18 +254,83 @@ A restated constant that has drifted is worse than a derived one, and the two
|
|
|
checkers had drifted from each other as well as from the runtime — which is why
|
|
checkers had drifted from each other as well as from the runtime — which is why
|
|
|
there are two of them and why both were wrong in the same way.
|
|
there are two of them and why both were wrong in the same way.
|
|
|
|
|
|
|
|
|
|
+### 8086 legality — `tests/check_8086.py`
|
|
|
|
|
+
|
|
|
|
|
+The twelfth and newest check, and the only one that asks a question about the
|
|
|
|
|
+*target* rather than about the compiler: **does the 8086 have this instruction
|
|
|
|
|
+at all?**
|
|
|
|
|
+
|
|
|
|
|
+```
|
|
|
|
|
+8086 check: 26 comparison sites, 22 lowered to a Boolean value, 13 lowered to a branch
|
|
|
|
|
+ value conditions : = x2 <> x2 < x5 >= x3 <= x2 > x8
|
|
|
|
|
+ branch conditions : IF / REPEAT x9 CASE x2 FOR downto x1 FOR to x3
|
|
|
|
|
+ runtime: 436 bytes, 219 swept, 0 0F-prefixed
|
|
|
|
|
+ program code: 28 of 31 fixtures swept end to end, 2257 bytes
|
|
|
|
|
+ t33_cmpops: 13 comparisons matched against their source operators, in order
|
|
|
|
|
+ clause H: 8 of 8 fixtures matched the branch conditions read off their source
|
|
|
|
|
+```
|
|
|
|
|
+
|
|
|
|
|
+It exists because bugs 32 and 33 got past everything else, and because **no
|
|
|
|
|
+execution oracle can exist for this**: qemu 10.0.11's lowest CPU model is 486,
|
|
|
|
|
+so `0F 84` is an ordinary `JZ` there and always was. Nor could the
|
|
|
|
|
+disassembler help — FCML's `-m16` mode is a 386, so the project's independent
|
|
|
|
|
+checker was guaranteed to agree with the bug.
|
|
|
|
|
+
|
|
|
|
|
+The design is mostly a list of things that do **not** work:
|
|
|
|
|
+
|
|
|
|
|
+- **A linear sweep of the code region is not a sound oracle.** Inline string
|
|
|
|
|
+ literals are emitted into the code stream, so the sweep desynchronises and
|
|
|
|
|
+ then aborts on text — `t09_if` decodes 16 real instructions and dies on
|
|
|
|
|
+ `FE E9 0D 00`, which is ASCII.
|
|
|
|
|
+- **A bare `3D` anchor is unsound.** It matches displacement and immediate bytes
|
|
|
|
|
+ as readily as opcodes, and using one produced **two false alarms**: a `3D`
|
|
|
|
|
+ inside a `CALL` displacement in `t11_for`, and one inside a string in
|
|
|
|
|
+ `t21_mixed`. The anchor is the three-byte `3D 00 00` or nothing.
|
|
|
|
|
+
|
|
|
|
|
+So it **anchors on comparison sites instead of instruction boundaries**: `3B C1`
|
|
|
|
|
+(`EmCmpAxCx`) and `3D 00 00` (`EmCmpAxi (0)`) are the only sequences that can
|
|
|
|
|
+precede a lowering, and all seven `EmJcc` sites and the `EmSetcc` site sit
|
|
|
|
|
+immediately after one — which was verified by reading each site, not inferred.
|
|
|
|
|
+Branches are *additionally* found by shape (`7x 03 E9`, searching for the
|
|
|
|
|
+`E9`), which is what covers the CASE arm whose `EmCmpAxi` carries a label rather
|
|
|
|
|
+than 0. Where a region sweeps clean the sweep also asserts no `0F`, and the
|
|
|
|
|
+fraction it reached (28 of 31) is **printed rather than implied**.
|
|
|
|
|
+
|
|
|
|
|
+"Is this an 8086 shape" is a much weaker question than it looks — a `SETG` where
|
|
|
|
|
+a `SETGE` belongs is still a fine shape — so two further clauses compare against
|
|
|
|
|
+**source**. **G** matches `t33_cmpops`'s 13 comparisons against the operators in
|
|
|
|
|
+source order, which catches a `>`/`>=` swap. That fixture exists partly for this:
|
|
|
|
|
+`=`, `<>` and `<=` had never been used as a comparison anywhere in the suite, and
|
|
|
|
|
+`>`/`>=` had already been swapped once, so the coverage hole and the bug it let
|
|
|
|
|
+through were the same hole. **H** pins, per fixture, the conditions its branch
|
|
|
|
|
+sites declare, read off the `.pas` sources; its need was *measured* (mutation M5
|
|
|
|
|
+came back green before H existed) rather than anticipated.
|
|
|
|
|
+
|
|
|
|
|
+**What it does not do.** It cannot assert on the CASE arm's label immediate, and
|
|
|
|
|
+it never executes anything: it proves the opcodes are 8086 and that conditions
|
|
|
|
|
+are attached to the right constructs, but the control flow those bytes produce
|
|
|
|
|
+is still only checked by qemu on a 486. An in-process 8086 interpreter is the
|
|
|
|
|
+only thing that would close that, which is why `CmdRun` is next.
|
|
|
|
|
+
|
|
|
### Non-vacuity — `tests/nonvacuity.sh`
|
|
### Non-vacuity — `tests/nonvacuity.sh`
|
|
|
|
|
|
|
|
-Every assertion in this file is proved able to fail: **28 deliberate
|
|
|
|
|
|
|
+Every assertion in this file is proved able to fail: **44 deliberate
|
|
|
breakages, each asserted to turn exactly one named check red for the stated
|
|
breakages, each asserted to turn exactly one named check red for the stated
|
|
|
reason, then restored and re-asserted green.** Six break the runtime, five
|
|
reason, then restored and re-asserted green.** Six break the runtime, five
|
|
|
attack the mod=11 table (including restoring the exact wrong table this
|
|
attack the mod=11 table (including restoring the exact wrong table this
|
|
|
project once shipped), three target `EmBpDisp` — the truncation, the
|
|
project once shipped), three target `EmBpDisp` — the truncation, the
|
|
|
always-disp16 over-encoding that must *stay* green, and the restored source —
|
|
always-disp16 over-encoding that must *stay* green, and the restored source —
|
|
|
-six attack the helper audit, and five attack the `.COM` layout checker.
|
|
|
|
|
|
|
+six attack the helper audit, five attack the `.COM` layout checker, and five
|
|
|
|
|
+attack the 8086 lowering.
|
|
|
|
|
+
|
|
|
|
|
+That last group is the newest and the least optional. Two of its five
|
|
|
|
|
+(`M4`, `M5`) invert the branch polarity, which is a *legal* 8086 opcode
|
|
|
|
|
+sequence, so no shape-based check can see it and only a source-derived
|
|
|
|
|
+expectation can. **`M5` came back green on its first run**, which is why
|
|
|
|
|
+clause H of `check_8086.py` exists at all; see bug 33 above.
|
|
|
|
|
|
|
|
-Two properties of the harness itself are enforced, because both had already
|
|
|
|
|
-gone wrong silently:
|
|
|
|
|
|
|
+Four properties of the harness itself are enforced, because all four had
|
|
|
|
|
+already gone wrong silently:
|
|
|
|
|
|
|
|
- **A baseline assertion runs first**, so a case that is *already* red is
|
|
- **A baseline assertion runs first**, so a case that is *already* red is
|
|
|
reported as `NOT NON-VACUOUS` and distinguished from one that *went* red.
|
|
reported as `NOT NON-VACUOUS` and distinguished from one that *went* red.
|
|
@@ -271,6 +342,23 @@ gone wrong silently:
|
|
|
been reformatted, and a checker that correctly stayed green because the
|
|
been reformatted, and a checker that correctly stayed green because the
|
|
|
breakage it looked for was no longer the breakage the checker hunts. Two
|
|
breakage it looked for was no longer the breakage the checker hunts. Two
|
|
|
of the four (`MovAlDh`, `StBxDl`) were repaired rather than deleted.
|
|
of the four (`MovAlDh`, `StBxDl`) were repaired rather than deleted.
|
|
|
|
|
+- **The python mutation helpers fail LOUDLY.** A non-zero exit from a helper
|
|
|
|
|
+ makes `if mutate_foo; then` false, so the case is silently **skipped** — and
|
|
|
|
|
+ a skipped case and a passing case are indistinguishable in the total. This
|
|
|
|
|
+ is not hypothetical: the `SETcc` case lost its first run to an apostrophe in
|
|
|
|
|
+ an `assert` message that closed a Python string, python died, the compiler
|
|
|
|
|
+ was never broken, and the suite still reported 0 failed. Each helper now
|
|
|
|
|
+ echoes a `BROKEN CASE` line and increments `fail`.
|
|
|
|
|
+- **Each helper counts its targets before replacing.** `assert s != before`
|
|
|
|
|
+ only proves the file changed; with two edits it passes if either landed, and
|
|
|
|
|
+ with two identical `HideLocals` call sites it would delete the wrong one —
|
|
|
|
|
+ still a changed file, still a working compiler, still green for the wrong
|
|
|
|
|
+ reason. So `assert s.count(X) == 1` everywhere.
|
|
|
|
|
+- **A failed rebuild is a FAILURE, not a skip.** The 8086 group's first draft
|
|
|
|
|
+ rebuilt with `make` but ran `check_8086.py`, which links against the `comtest`
|
|
|
|
|
+ binary that `make` does not build — so the *stale* compiler was measured and
|
|
|
|
|
+ the first mutation was reported as VACUOUS. The helper now checks the build
|
|
|
|
|
+ and says so.
|
|
|
|
|
|
|
|
The one that produced the most information was restoring the original shifted
|
|
The one that produced the most information was restoring the original shifted
|
|
|
mod=11 table: it turns **three** cells red rather than one, because the error
|
|
mod=11 table: it turns **three** cells red rather than one, because the error
|
|
@@ -803,16 +891,24 @@ Details that are deliberate, not incidental:
|
|
|
a global `x` is rejected. Pascal allows the shadow and the inner one wins.
|
|
a global `x` is rejected. Pascal allows the shadow and the inner one wins.
|
|
|
`HideLocals` fixed siblings colliding with each other; this is the
|
|
`HideLocals` fixed siblings colliding with each other; this is the
|
|
|
parent-vs-child direction of the same question and is untouched.
|
|
parent-vs-child direction of the same question and is untouched.
|
|
|
-- **The branch and compare lowering is 386 code on an 8086 target.** `EmJcc`
|
|
|
|
|
- emits `0F 8x rel16` and `EmSetcc` emits `0F 9x` (SETcc). Neither exists on
|
|
|
|
|
- an 8086. TP3 uses `JZ rel8` over a 3-byte `EJMP`, with `excond` materialising
|
|
|
|
|
- the *negated* boolean (`TPSRC8` ~244-300). Every relational operator and every
|
|
|
|
|
- conditional branch in the compiler is affected, so this is not one call site
|
|
|
|
|
- but the whole idiom. **No test can see it**: qemu-i386 defaults to a
|
|
|
|
|
- post-386 CPU, so every image in `run_com_exec.py` runs correctly on hardware
|
|
|
|
|
- that did not exist when TP3 shipped. Catching it needs `-cpu 8086` (untried) or
|
|
|
|
|
- a rewrite to the `excond` idiom plus a short/near branch policy — a milestone
|
|
|
|
|
- with a wide golden blast radius, deliberately not folded into this one.
|
|
|
|
|
|
|
+- **`qemu-system-i386` cannot execute 8086 code, so the 8086 checks are
|
|
|
|
|
+ static and stay static.** The lowest CPU model qemu 10.0.11 offers is 486
|
|
|
|
|
+ (`-cpu help` confirms it; there is no 8086 model to ask for). Every image in
|
|
|
|
|
+ `run_com_exec.py` therefore runs on hardware that did not exist when TP3
|
|
|
|
|
+ shipped, and no amount of fixture work changes that. This is why
|
|
|
|
|
+ `tests/check_8086.py` exists and why it had to be written as a byte-level
|
|
|
|
|
+ question rather than a behavioural one — and why its clauses G and H compare
|
|
|
|
|
+ against *source* rather than against another run of the machine. It remains a
|
|
|
|
|
+ weaker instrument than execution: it proves the opcodes are 8086 and that the
|
|
|
|
|
+ conditions are attached to the right constructs, but the control flow those
|
|
|
|
|
+ bytes produce is still only checked by qemu on a 486.
|
|
|
|
|
+- **The 8086 check cannot assert on the CASE arm's comparison.** `CASE`
|
|
|
|
|
+ compares against a *label*, so its `EmCmpAxi` is `3D lo hi` with a non-zero
|
|
|
|
|
+ immediate, and no sound anchor can find it — a bare `3D` also matches
|
|
|
|
|
+ displacement and immediate bytes, which produced two false alarms before the
|
|
|
|
|
+ 3-byte `3D 00 00` form replaced it. The arm is covered by *shape*
|
|
|
|
|
+ (`7x 03 E9`, searching for the `E9`) and by `t22_case`'s execution, but the
|
|
|
|
|
+ label immediate itself is unchecked.
|
|
|
- **The runtime's entries are now each called directly, and two of its
|
|
- **The runtime's entries are now each called directly, and two of its
|
|
|
invariants are stated rather than implied.** 436 bytes, 14 entries, 100
|
|
invariants are stated rather than implied.** 436 bytes, 14 entries, 100
|
|
|
emitter helpers decoded against their own names across both modules, the
|
|
emitter helpers decoded against their own names across both modules, the
|
|
@@ -1160,15 +1256,115 @@ emitter audit.
|
|
|
`symtab[old].resvar` holds an index and a function's result variable is one
|
|
`symtab[old].resvar` holds an index and a function's result variable is one
|
|
|
of the entries being hidden.
|
|
of the entries being hidden.
|
|
|
|
|
|
|
|
-The theme is worth stating because it is the same theme as bug 27: **a name that
|
|
|
|
|
-does not distinguish two things makes the next mistake invisible.** `*` and `+`
|
|
|
|
|
-were both `1`; `>` and `>=` were two hex bytes; two procedures' `a` was one
|
|
|
|
|
-symbol. In each case the fix is to make the distinction part of the name or the
|
|
|
|
|
-surrounding text, not to fix the value and leave the ambiguity in place.
|
|
|
|
|
|
|
+### Then the emitted code stopped being 8086 code, and two more appeared
|
|
|
|
|
+
|
|
|
|
|
+Thirty-two bugs. Bug 32 had been present since the code generator was written
|
|
|
|
|
+and every check in the project was blind to it, which is a more interesting
|
|
|
|
|
+fault than the previous thirty-one and is worth setting out at length.
|
|
|
|
|
+
|
|
|
|
|
+32. **Every conditional branch and every comparison in every compiled program
|
|
|
|
|
+ was an illegal instruction on the target CPU.** `EmJcc` emitted
|
|
|
|
|
+ `0F 8x rel16` (`Jcc` near) and `EmSetcc` emitted `0F 9x rel8` (`SETcc`).
|
|
|
|
|
+ `0F` is a 386-and-later opcode-escape prefix. The 8086 — the machine TP3
|
|
|
|
|
+ targets, and the machine this compiler exists to emit for — has no such
|
|
|
|
|
+ prefix. So the code was not wrong, it was not *code*.
|
|
|
|
|
+
|
|
|
|
|
+ What makes this worth a section rather than a bullet is that **everything
|
|
|
|
|
+ was green while it was true.** The compile matrix passed. The `.COM` layout
|
|
|
|
|
+ checker passed. The runtime golden passed. The emitter audit passed. Thirty
|
|
|
|
|
+ fixtures booted in qemu and printed exactly their hand-derived expected
|
|
|
|
|
+ bytes. Two reasons, and the second is the one to remember:
|
|
|
|
|
+
|
|
|
|
|
+ - **qemu-system-i386 has no 8086 model.** Its lowest is 486, where
|
|
|
|
|
+ `0F 84` is an ordinary `JZ`. So the execution oracle cannot see this class
|
|
|
|
|
+ of fault, ever — not with a better fixture, not with a longer run. The
|
|
|
|
|
+ suite that had found bugs 28–31 could not find this one by construction.
|
|
|
|
|
+ - **FCML is this project's *independent* disassembler, and FCML's 16-bit
|
|
|
|
|
+ mode is a 386.** The one tool whose entire job is to say "this is not a
|
|
|
|
|
+ real instruction" was architecturally guaranteed to agree with the bug.
|
|
|
|
|
+ An independent checker that shares the subject's blind spot is worse than
|
|
|
|
|
+ no checker, because it converts an unknown into a false assurance.
|
|
|
|
|
+
|
|
|
|
|
+ The fix is TP3's own idiom, read off the disassembly of the original rather
|
|
|
|
|
+ than invented. `TPSRC8` ~246-295 lays IF/WHILE/REPEAT out as `MOV AL,brnchop
|
|
|
|
|
+ ; MOV AH,#$03 ; CALL eword ; PUSH pc ; CALL ejump` — a **short** `Jcc` of
|
|
|
|
|
+ displacement 3, stepping over a 3-byte `EJMP`. And `TPSRC9` ~412-424
|
|
|
|
|
+ (`flgbool`) lays a comparison-to-Boolean out as `MOV AX,#0001 ; <Jcc> +1 ;
|
|
|
|
|
+ DEC AX`. Both are 8086 code, both are shorter than what they replace, and
|
|
|
|
|
+ the condition is carried in the opcode's **low nibble**, which is why
|
|
|
|
|
+ `70H + cc` reproduces the identical condition and all seven `EmJcc` sites
|
|
|
|
|
+ and all six `EmSetcc` arms go on passing the byte they always passed. The
|
|
|
|
|
+ flags survive, which the FOR test needs: it emits `CMP` then `Jcc` with
|
|
|
|
|
+ nothing in between.
|
|
|
|
|
+
|
|
|
|
|
+33. **The first attempt at that port inverted every conditional in every
|
|
|
|
|
+ program.** `EmJcc` *jumps to* its target, but the 8086 shape *steps over*
|
|
|
|
|
+ the `EJMP` — so writing `7x 03` and falling into the destination runs the
|
|
|
|
|
+ two the wrong way round. TP3's `brnchop` is the branch taken when the
|
|
|
|
|
+ condition is TRUE; the nibbles these call sites pass are the branch taken
|
|
|
|
|
+ when the condition is **FALSE** (IF's `EmJcc (84H)` is `JZ` patched to the
|
|
|
|
|
+ `ELSE`, so it must fire when the test failed). The two spellings are
|
|
|
|
|
+ opposite, and the naive port took the wrong one. `t09_if` printed
|
|
|
|
|
+ `pos / nonpos / lt` for a program whose hand-derived output is
|
|
|
|
|
+ `nonpos / pos / ge`, and `t12_repeat` looped forever.
|
|
|
|
|
+
|
|
|
|
|
+ Only the **execution** suite noticed. The compile matrix and the `.COM`
|
|
|
|
|
+ layout check were both perfectly happy with every conditional inverted —
|
|
|
|
|
+ third instance in a row of a byte-level-clean, behaviour-wrong fault.
|
|
|
|
|
+ `JccShortInv` now does the negation (`n XOR 1`, spelled `n + 1 - 2*(n MOD 2)`
|
|
|
|
|
+ because gm2 under `-fiso` has no XOR on integers at all), and it is one named
|
|
|
|
|
+ function rather than open-coded at two call sites.
|
|
|
|
|
+
|
|
|
|
|
+Fixing them needed a check that asks a question nothing else was asking:
|
|
|
|
|
+**does the target CPU have this opcode at all?** `tests/check_8086.py`.
|
|
|
|
|
+
|
|
|
|
|
+Its design is mostly about what *cannot* be done. A linear sweep of the code
|
|
|
|
|
+region is not a sound oracle here: inline string literals are emitted into the
|
|
|
|
|
+code stream, so the sweep desynchronises and then aborts on text — `t09_if`
|
|
|
|
|
+decodes 16 real instructions and dies on `FE E9 0D 00`, which is ASCII. So the
|
|
|
|
|
+check **anchors on comparison sites instead of boundaries**: `3B C1`
|
|
|
|
|
+(`EmCmpAxCx`) and the three-byte `3D 00 00` (`EmCmpAxi (0)`) are the only
|
|
|
|
|
+sequences that can precede a lowering, and every one of the seven `EmJcc` sites
|
|
|
|
|
+and the one `EmSetcc` site sits immediately after one. A **bare `3D` anchor is
|
|
|
|
|
+unsound** — it matches displacement and immediate bytes, and using one produced
|
|
|
|
|
+two false alarms (a `3D` inside a `CALL` displacement in `t11_for`, one inside a
|
|
|
|
|
+string in `t21_mixed`) before it was replaced by the 3-byte form. Where a
|
|
|
|
|
+fixture's region *does* sweep clean, the sweep additionally asserts no `0F`, and
|
|
|
|
|
+the fraction it reached is printed (28 of 31) rather than implied. The CASE arm,
|
|
|
|
|
+whose `EmCmpAxi` carries a label rather than 0, is found by *shape* (`7x 03 E9`,
|
|
|
|
|
+searching for the `E9`) — but the check cannot assert on the label immediate
|
|
|
|
|
+itself, and `t22_case`'s execution is what covers that.
|
|
|
|
|
+
|
|
|
|
|
+The check also carries two clauses about **which condition** each site means,
|
|
|
|
|
+because "is this an 8086 shape" is a much weaker question than it looks. A
|
|
|
|
|
+`SETG` where a `SETGE` belongs is still a perfectly good shape. Clause G matches
|
|
|
|
|
+the 13 comparisons of `t33_cmpops` against the operators **in source order**,
|
|
|
|
|
+which is what catches a `>`/`>=` swap (mutation M3, red with the swap visible in
|
|
|
|
|
+the message: `… Dh Dh Fh Fh Dh` where the source asks `… Fh Fh Dh Dh Fh`). That
|
|
|
|
|
+fixture exists partly for this: `=`, `<>` and `<=` had **never been used as a
|
|
|
|
|
+comparison anywhere in the suite**, and `>`/`>=` had already been swapped once,
|
|
|
|
|
+so the coverage hole and the bug it let through were the same hole.
|
|
|
|
|
+
|
|
|
|
|
+Clause H exists because clause H's need was **measured, not anticipated**. As
|
|
|
|
|
+first written the check was blind to M5 — the polarity inversion of bug 33
|
|
|
|
|
+applied to the IF and CASE sites only. IF declares nibble 4, CASE declares 5,
|
|
|
|
|
+they negate into each other, and both are declared, so nothing complained while
|
|
|
|
|
+every conditional took the wrong path. The whole-suite version (M4) was caught
|
|
|
|
|
+only by luck: FOR declares `C` and `F`, whose negations `D` and `E` are declared
|
|
|
|
|
+for nothing at all. So clause H pins, per fixture, the multiset of conditions
|
|
|
|
|
+its branch sites declare, **read off the `.pas` sources** and written out with
|
|
|
|
|
+the reasoning beside each row — a table measured from the image would agree with
|
|
|
|
|
+any behaviour including a wrong one.
|
|
|
|
|
+
|
|
|
|
|
+Five mutations are now permanent cases in `tests/nonvacuity.sh` (44 ok, 0
|
|
|
|
|
+failed, up from 39): M1 and M2 restore each original defect, M3 swaps `>`/`>=`,
|
|
|
|
|
+M4 inverts the branch polarity everywhere, M5 inverts it for IF and CASE only.
|
|
|
|
|
+M5's first run was the one that came back green, and that is the case's whole
|
|
|
|
|
+reason for existing.
|
|
|
|
|
|
|
|
## The bug family, stated once
|
|
## The bug family, stated once
|
|
|
|
|
|
|
|
-Nine of the thirty-one are the *same* bug in different clothes: **loading the
|
|
|
|
|
|
|
+Nine of the thirty-two are the *same* bug in different clothes: **loading the
|
|
|
address where the value was wanted, or picking the register one byte or one
|
|
address where the value was wanted, or picking the register one byte or one
|
|
|
letter away from the right one.** `EmPushVarAddr` had the right bytes for the
|
|
letter away from the right one.** `EmPushVarAddr` had the right bytes for the
|
|
|
wrong register. `LdAlBx` and `MovAlBl` are one letter apart. `MovAh0` and
|
|
wrong register. `LdAlBx` and `MovAlBl` are one letter apart. `MovAh0` and
|
|
@@ -1245,43 +1441,34 @@ independently-scanned inventory at all.
|
|
|
|
|
|
|
|
## Next steps
|
|
## Next steps
|
|
|
|
|
|
|
|
-1. **8086 branch and compare lowering.** `EmJcc` emits `0F 8x rel16` and
|
|
|
|
|
- `EmSetcc` emits `0F 9x`; neither instruction exists on an 8086. Every
|
|
|
|
|
- relational operator and every conditional branch depends on them. TP3's
|
|
|
|
|
- idiom is `excond` materialising the negated boolean plus `JZ rel8` over a
|
|
|
|
|
- 3-byte `EJMP` (`TPSRC8` ~244-300), so this needs a boolean-materialisation
|
|
|
|
|
- strategy and a short/near branch policy, not two opcode substitutions — and
|
|
|
|
|
- it will move nearly every byte in the golden. **First, try
|
|
|
|
|
- `qemu-system-i386 -cpu 8086`** on the existing 30 images: if that turns this
|
|
|
|
|
- class red, it is a one-line addition to `rt_exec.py` and it makes every
|
|
|
|
|
- later fix provable instead of argued.
|
|
|
|
|
-2. **`CmdRun`** as an in-process 8086 interpreter — the `R` menu key, and a
|
|
|
|
|
|
|
+1. **`CmdRun`** as an in-process 8086 interpreter — the `R` menu key, and a
|
|
|
fallback executor for environments with no DOS. Validate it against qemu on
|
|
fallback executor for environments with no DOS. Validate it against qemu on
|
|
|
the *same images*, so the two oracles check each other. Cross-validation is
|
|
the *same images*, so the two oracles check each other. Cross-validation is
|
|
|
- the point: an interpreter that agrees with qemu on 30 fixtures is far more
|
|
|
|
|
- evidence than either alone.
|
|
|
|
|
-3. **String *variables*** — `s : string`, `s := 'hi'`, `writeln(s)`. The
|
|
|
|
|
|
|
+ the point: an interpreter that agrees with qemu on 31 fixtures is far more
|
|
|
|
|
+ evidence than either alone. It is also the only candidate for an **8086**
|
|
|
|
|
+ execution oracle, since qemu cannot be one.
|
|
|
|
|
+2. **String *variables*** — `s : string`, `s := 'hi'`, `writeln(s)`. The
|
|
|
encoding blocker is gone (`EmBpDisp`); what is left is a length word, an
|
|
encoding blocker is gone (`EmBpDisp`); what is left is a length word, an
|
|
|
assignment path, and a `WrStr` entry (TPSRC4 `xwrtstr`). `IoCall` currently
|
|
assignment path, and a `WrStr` entry (TPSRC4 `xwrtstr`). `IoCall` currently
|
|
|
refuses with `ENoLib`.
|
|
refuses with `ENoLib`.
|
|
|
-4. Nested procedures / recursion, `var` parameters (the `SEG:OFF` push from
|
|
|
|
|
|
|
+3. Nested procedures / recursion, `var` parameters (the `SEG:OFF` push from
|
|
|
RESUME-TP3.md §3.11), range/index checks (`TU_RANGE_CHECK`,
|
|
RESUME-TP3.md §3.11), range/index checks (`TU_RANGE_CHECK`,
|
|
|
`TU_INDEX_CHECK`), typed constants (RESUME-TP3.md §3.14), `array` at its
|
|
`TU_INDEX_CHECK`), typed constants (RESUME-TP3.md §3.14), `array` at its
|
|
|
point of use (`t14`), `case` with subrange labels.
|
|
point of use (`t14`), `case` with subrange labels.
|
|
|
-5. **`readln` of a `BYTE`** calls `rdint`, which stores 2 bytes and overflows
|
|
|
|
|
|
|
+4. **`readln` of a `BYTE`** calls `rdint`, which stores 2 bytes and overflows
|
|
|
into the next variable. TP3 has a separate `xrdbyte`; a `TU_RdByte` entry is
|
|
into the next variable. TP3 has a separate `xrdbyte`; a `TU_RdByte` entry is
|
|
|
the fix. No fixture exists yet, which is why it has not been done — write
|
|
the fix. No fixture exists yet, which is why it has not been done — write
|
|
|
the fixture first, so the bug is red before the fix.
|
|
the fixture first, so the bug is red before the fix.
|
|
|
-6. Make the 4 KiB code window an enforced limit rather than a documented one:
|
|
|
|
|
|
|
+5. Make the 4 KiB code window an enforced limit rather than a documented one:
|
|
|
report an error when `pc` reaches `dc`, instead of writing over the data.
|
|
report an error when `pc` reaches `dc`, instead of writing over the data.
|
|
|
-7. Both spellings of a multi-name declaration. `var i, c : integer;` is
|
|
|
|
|
|
|
+6. Both spellings of a multi-name declaration. `var i, c : integer;` is
|
|
|
error 1 at the comma and needs two `var` lines; `procedure f (a : integer;
|
|
error 1 at the comma and needs two `var` lines; `procedure f (a : integer;
|
|
|
b : integer)` is error 1 at the semicolon and needs a comma. Neither is
|
|
b : integer)` is error 1 at the semicolon and needs a comma. Neither is
|
|
|
wrong Pascal, so a program that compiles under one compiler may not under
|
|
wrong Pascal, so a program that compiles under one compiler may not under
|
|
|
another. A parameter may also not shadow a global (`DupTest` rejects any
|
|
another. A parameter may also not shadow a global (`DupTest` rejects any
|
|
|
name `Search` finds at any level), which Pascal allows.
|
|
name `Search` finds at any level), which Pascal allows.
|
|
|
-8. Harden the program-header parameter loop against non-advancing input
|
|
|
|
|
|
|
+7. Harden the program-header parameter loop against non-advancing input
|
|
|
(`program p(1;)`) with a `BOOLEAN` flag — **not** `EXIT`, which ICEs gm2.
|
|
(`program p(1;)`) with a `BOOLEAN` flag — **not** `EXIT`, which ICEs gm2.
|
|
|
-9. FreeDOS (`freedos.qcow2`, FD14-LiveCD) is still untried. Not needed for any
|
|
|
|
|
|
|
+8. FreeDOS (`freedos.qcow2`, FD14-LiveCD) is still untried. Not needed for any
|
|
|
claim above, but it is the only way to get a *real* DOS as a third opinion
|
|
claim above, but it is the only way to get a *real* DOS as a third opinion
|
|
|
on the `INT 21h` shim.
|
|
on the `INT 21h` shim.
|