|
@@ -25,6 +25,7 @@ manual, not guessed.
|
|
|
| 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** |
|
|
| 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) + `Exec86`, the in-process 8086 interpreter | `v-TP3-CMDRUN` | done, **a second execution oracle: 33/33 fixtures agree with qemu byte for byte, and `R` runs one inside the shell** |
|
|
| `CmdRun` (the `R` key) + `Exec86`, the in-process 8086 interpreter | `v-TP3-CMDRUN` | done, **a second execution oracle: 33/33 fixtures agree with qemu byte for byte, and `R` runs one inside the shell** |
|
|
|
|
|
+| Image layout in one file; a check's sweep region measured, not restated | `v-TP3-IMAGELAYOUT` | done, **every reader of a linked `.COM` imports `tests/comimage.py`, and the region `check_framedisp` sweeps is two readings of the file required to agree** |
|
|
|
|
|
|
|
|
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
|
|
|
`master`; verified by diffing the rows against `git tag -l`, which is how
|
|
`master`; verified by diffing the rows against `git tag -l`, which is how
|
|
@@ -186,6 +187,7 @@ proves each one can go red.
|
|
|
| `probe/run_modrm19.py` | the mod=00/01/10 effective addresses, by **executing** 23 cases on a real 8086 under qemu and scanning for where the marker landed | mod=11 — see below |
|
|
| `probe/run_modrm19.py` | the mod=00/01/10 effective addresses, by **executing** 23 cases on a real 8086 under qemu and scanning for where the marker landed | mod=11 — see below |
|
|
|
| `probe/modrm11.py` | the mod=11 register identities, by **encoding** with GNU `as` and decoding with FCML, against hard-coded bytes | the table agreeing with itself |
|
|
| `probe/modrm11.py` | the mod=11 register identities, by **encoding** with GNU `as` and decoding with FCML, against hard-coded bytes | the table agreeing with itself |
|
|
|
| `audit_helpers.py` | every one-line emitter in **both** `Runtime.mod` and `Compiler.mod` decodes to what its *name* says — **101/101**, from an inventory scanned independently of the parser | anything longer than one instruction |
|
|
| `audit_helpers.py` | every one-line emitter in **both** `Runtime.mod` and `Compiler.mod` decodes to what its *name* says — **101/101**, from an inventory scanned independently of the parser | anything longer than one instruction |
|
|
|
|
|
+| `check_comimage.py` | a linked image's layout is described in **exactly one file**: `comimage.py` defines each part once, every reader imports it, no second `find_header` exists anywhere in `tests/` | a check that *hand-rolls* the layout from literals (`hdr = 3 + rt_size`), which defines none of those names — the readers catch that a different way: each states the layout twice, from two independent sources, and requires the two to agree |
|
|
|
| `check_runtime.py` + `runtime.golden` | the built runtime's code region (436 bytes, code ends at 405) sweeps cleanly through FCML, every entry and all branch targets land on an instruction boundary, and the whole disassembly is byte-for-byte the committed golden | whether the golden is *right* |
|
|
| `check_runtime.py` + `runtime.golden` | the built runtime's code region (436 bytes, code ends at 405) sweeps cleanly through FCML, every entry and all branch targets land on an instruction boundary, and the whole disassembly is byte-for-byte the committed golden | whether the golden is *right* |
|
|
|
| `check_framedisp.py` | `[BP+off]` uses disp8 iff `off <= 127`, for locals (negative) and far parameters (>127) | which of the two encodings was chosen, if the other also works |
|
|
| `check_framedisp.py` | `[BP+off]` uses disp8 iff `off <= 127`, for locals (negative) and far parameters (>127) | which of the two encodings was chosen, if the other also works |
|
|
|
| `run_com_exec.py` | the **emitted image executes** and prints exactly the expected bytes | semantics the fixture never exercises |
|
|
| `run_com_exec.py` | the **emitted image executes** and prints exactly the expected bytes | semantics the fixture never exercises |
|
|
@@ -247,6 +249,18 @@ entire 16-bit range as a signed value. The check also asserts the *rule* rather
|
|
|
than one encoding — always-disp16 is accepted, and `nonvacuity.sh` proves that
|
|
than one encoding — always-disp16 is accepted, and `nonvacuity.sh` proves that
|
|
|
by building it and requiring the check to stay green.
|
|
by building it and requiring the check to stay green.
|
|
|
|
|
|
|
|
|
|
+It had a **second, unrelated blind spot of its own**: the region it swept came
|
|
|
|
|
+from `RT_SZ = 391`, a runtime size that had drifted, so the sweep began inside
|
|
|
|
|
+the runtime, part way through an instruction — and the check passed anyway,
|
|
|
|
|
+because the byte patterns it searches for are in the image wherever they happen
|
|
|
|
|
+to be and a decode starting mid-instruction happened to reach the same offsets.
|
|
|
|
|
+Nothing in the check could see where its own region began, which is a wrong
|
|
|
|
|
+input that produces the right answers until the layout moves. The region is now
|
|
|
|
|
+**two independent readings of the file** — where the entry jump says execution
|
|
|
|
|
+starts, where the program header says the runtime ends — required to agree
|
|
|
|
|
+before a single byte is swept, with `tests/comimage.py` supplying both readings
|
|
|
|
|
+and `tests/check_comimage.py` asserting there is only one copy of each.
|
|
|
|
|
+
|
|
|
### Execution under qemu — `tests/run_com_exec.py`
|
|
### Execution under qemu — `tests/run_com_exec.py`
|
|
|
|
|
|
|
|
The check that cannot be written as a byte comparison, so also the one that
|
|
The check that cannot be written as a byte comparison, so also the one that
|
|
@@ -271,7 +285,8 @@ 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.
|
|
|
|
|
|
|
|
-**The `.COM` layout constants are measured, not restated.** `run_com_tests.sh`
|
|
|
|
|
|
|
+**The `.COM` layout constants are measured, not restated — and now live in one
|
|
|
|
|
+file.** `run_com_tests.sh`
|
|
|
and `comtest.py` both used to hard-code `RT_SZ = 391` against a runtime that
|
|
and `comtest.py` both used to hard-code `RT_SZ = 391` against a runtime that
|
|
|
had since grown to 432 bytes at the time, so they read the program header 41 bytes early
|
|
had since grown to 432 bytes at the time, so they read the program header 41 bytes early
|
|
|
and reported **30 false failures** — a red suite that meant nothing, which is
|
|
and reported **30 false failures** — a red suite that meant nothing, which is
|
|
@@ -286,7 +301,18 @@ measured runtime size: 436 bytes (header at image offset 439)
|
|
|
|
|
|
|
|
A restated constant that has drifted is worse than a derived one, and the two
|
|
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 were two of them and why both were wrong in the same way.
|
|
|
|
|
+
|
|
|
|
|
+So the layout itself moved into **`tests/comimage.py`**, and the third reader
|
|
|
|
|
+joined the first two. Four places now read a linked image — `comtest.py`, the
|
|
|
|
|
+independent checker inside `run_com_tests.sh`, `check_framedisp.py` and
|
|
|
|
|
+`check_8086.py` — and none of them says what a `.COM` looks like; they import
|
|
|
|
|
+it. `tests/check_comimage.py` is the assertion that this stays true: one
|
|
|
|
|
+definition of each part, imported by every reader, no second `find_header`
|
|
|
|
|
+anywhere in `tests/`. Its scope is stated in its own docstring, because it
|
|
|
|
|
+cannot see a check that re-derives the layout from inline numbers — that is what
|
|
|
|
|
+the readers do instead, each stating the layout twice from two different
|
|
|
|
|
+sources and refusing to proceed when the two disagree.
|
|
|
|
|
|
|
|
### 8086 legality — `tests/check_8086.py`
|
|
### 8086 legality — `tests/check_8086.py`
|
|
|
|
|
|
|
@@ -410,21 +436,35 @@ goes red before a single instruction has run.
|
|
|
|
|
|
|
|
### Non-vacuity — `tests/nonvacuity.sh`
|
|
### Non-vacuity — `tests/nonvacuity.sh`
|
|
|
|
|
|
|
|
-Every assertion in this file is proved able to fail: **52 deliberate
|
|
|
|
|
|
|
+Every assertion in this file is proved able to fail: **62 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** — `non-vacuity: 52 ok, 0 failed`.
|
|
|
|
|
|
|
+reason, then restored and re-asserted green** — `non-vacuity: 62 ok, 0 failed`.
|
|
|
They cover the runtime's emitter audit and its restored source, the mod=11
|
|
They cover the runtime's emitter audit and its restored source, the mod=11
|
|
|
table (including restoring the exact wrong table this project once shipped),
|
|
table (including restoring the exact wrong table this project once shipped),
|
|
|
the `[BP+off]` rule, the behavioural bugs, the emitter-name audit of
|
|
the `[BP+off]` rule, the behavioural bugs, the emitter-name audit of
|
|
|
-`Compiler.mod`, the BP contract, the `.COM` layout checker, the 8086 lowering,
|
|
|
|
|
-the interpreter itself, and the `R` key.
|
|
|
|
|
|
|
+`Compiler.mod`, the BP contract, the `.COM` layout checker, the image-layout
|
|
|
|
|
+helper and the three checks that read it, the 8086 lowering, the interpreter
|
|
|
|
|
+itself, and the `R` key.
|
|
|
|
|
|
|
|
-Eight of those 52 arrived with this milestone, and each one is the same shape:
|
|
|
|
|
-code that compiled clean and passed every byte-level check, until it was
|
|
|
|
|
-**run**. Two are behavioural (below), two come from the new interpreter, two
|
|
|
|
|
|
|
+Eight arrived with the previous milestone (`v-TP3-CMDRUN`), and each one is the
|
|
|
|
|
+same shape: code that compiled clean and passed every byte-level check, until it
|
|
|
|
|
+was **run**. Two are behavioural (below), two come from the new interpreter, two
|
|
|
pin the two new grammar rows the helper audit gained for `EmXorAl01`, and two
|
|
pin the two new grammar rows the helper audit gained for `EmXorAl01`, and two
|
|
|
are the `R` key's mutation and its restored green.
|
|
are the `R` key's mutation and its restored green.
|
|
|
|
|
|
|
|
|
|
+Ten arrived with this one, and they are a different shape: **a check whose own
|
|
|
|
|
+input had never been verified.** `check_framedisp` swept a region built from a
|
|
|
|
|
+literal that had drifted, and the region is now two independent readings of the
|
|
|
|
|
+file required to agree — so the first three cases break each reading in turn:
|
|
|
|
|
+the entry jump answered with the old literal, and the header's own equation one
|
|
|
|
|
+byte out, seen red by **two different readers** with two different sentences.
|
|
|
|
|
+The next four break the single copy itself — a `find_header` copied out of
|
|
|
|
|
+`comimage.py`, a layout constant copied out of it, the definition deleted (which
|
|
|
|
|
+must be a red report rather than a silent green one, because a rule that matches
|
|
|
|
|
+nothing looks exactly like a rule that passes), and a caller that reaches the
|
|
|
|
|
+helper through another consumer instead of through `comimage`. The last three
|
|
|
|
|
+are restored greens, one per reader.
|
|
|
|
|
+
|
|
|
That last group is the newest and the least optional. Two of its five
|
|
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
|
|
(`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
|
|
sequence, so no shape-based check can see it and only a source-derived
|
|
@@ -1531,8 +1571,9 @@ 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
|
|
the reasoning beside each row — a table measured from the image would agree with
|
|
|
any behaviour including a wrong one.
|
|
any behaviour including a wrong one.
|
|
|
|
|
|
|
|
-Five mutations are now permanent cases in `tests/nonvacuity.sh` (`52 ok, 0
|
|
|
|
|
-failed` in total across every section; these five were `44 ok` when added):
|
|
|
|
|
|
|
+Five mutations are now permanent cases in `tests/nonvacuity.sh` (its final
|
|
|
|
|
+`non-vacuity:` line reports the total across every section; these five were
|
|
|
|
|
+`44 ok` when added):
|
|
|
M1 and M2 restore each original defect, M3 swaps `>`/`>=`,
|
|
M1 and M2 restore each original defect, M3 swaps `>`/`>=`,
|
|
|
M4 inverts the branch polarity everywhere, M5 inverts it for IF and CASE only.
|
|
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
|
|
M5's first run was the one that came back green, and that is the case's whole
|
|
@@ -1665,42 +1706,34 @@ independently-scanned inventory at all.
|
|
|
|
|
|
|
|
## Next steps
|
|
## Next steps
|
|
|
|
|
|
|
|
-1. **Close the third restated `RT_SZ`.** `tests/check_framedisp.py` hard-codes
|
|
|
|
|
- `RT_SZ = 391` where the runtime now measures 436, so `img[RTSZ:]` begins 61
|
|
|
|
|
- bytes inside the runtime tail and the check passes by luck. `run_com_tests.sh`
|
|
|
|
|
- and `comtest.py` carried the same constant and were fixed by *measuring* the
|
|
|
|
|
- header from its own signature; this one needs that shared helper
|
|
|
|
|
- (`tests/comimage.py`) and, being new, its own non-vacuity case — a green
|
|
|
|
|
- nobody has ever seen red is the failure mode this project keeps
|
|
|
|
|
- rediscovering, and this is the last known instance of it.
|
|
|
|
|
-2. **The multi-argument kind-2 clobber.** `f (a > b, x)` passes a wrong first
|
|
|
|
|
|
|
+1. **The multi-argument kind-2 clobber.** `f (a > b, x)` passes a wrong first
|
|
|
value, and `f (a > b, c > d)` passes the second comparison twice.
|
|
value, and `f (a > b, c > d)` passes the second comparison twice.
|
|
|
`SaveLeft` parks a computed operand across the parse of the *other* operand
|
|
`SaveLeft` parks a computed operand across the parse of the *other* operand
|
|
|
of a binary operator; the three call parsers park nothing. Fixture first, so
|
|
of a binary operator; the three call parsers park nothing. Fixture first, so
|
|
|
the bug is red before the fix (see "Honest limitations").
|
|
the bug is red before the fix (see "Honest limitations").
|
|
|
-3. **String *variables*** — `s : string`, `s := 'hi'`, `writeln(s)`. The
|
|
|
|
|
|
|
+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. Now that `R` runs
|
|
|
|
|
|
|
+8. FreeDOS (`freedos.qcow2`, FD14-LiveCD) is still untried. Now that `R` runs
|
|
|
the image in-process, a real DOS is no longer needed for any claim above —
|
|
the image in-process, a real DOS is no longer needed for any claim above —
|
|
|
but it is still the only way to get a third opinion on the `INT 21h` shim,
|
|
but it is still the only way to get a third opinion on the `INT 21h` shim,
|
|
|
and `Exec86` deliberately implements only the three functions the runtime
|
|
and `Exec86` deliberately implements only the three functions the runtime
|