Files
LithosAnanke/v4/tools/mkpost.py
T
Claude be456d44e9 fix(v4): #190 POST regenerates the same; #16 sanitizers and hosted-check nightly
Captain Bob, 2026-11-13: "Create the issues then fix them before the long
acceptance test runs"; #16: "Nightly".

#190 -- make -C v4 post79 did not reproduce POST:
- mkpost.py runs v3 with address randomisation off (setarch -R): its
  printed addresses (>IN, FIND) are the same each run, so POST79.md is.
- v4/Makefile post79 builds hosted v3 from this tree's source first and
  uses it, not the lfs/ copy, which can be older.
- post_cases.c and POST79.md regenerated: 539 cases -- LOAD.rest_of_line,
  which v3 gets through since it changed after 2026-10-07. Two runs the
  same. POST_FLOOR 538 -> 539 (#173).
- test_host_unit.c takes the table's count, not 538 typed in the test.

#16 -- scripts/nightly.sh v4-checks: make -C v4 sanitize hosted-check,
logged under logs/<TS>/v4-checks/, refused without qemu-user; nightly.yml
runs it after publishing, before the proofs, installing qemu-user if the
image lacks it.

Evidence (logs/20261113-014927/post79, -024314): before, regenerated with
nothing changed: 539 cases and addresses differing run to run; after: the
same twice, hosted POST 539/539; test, test-32 99 programs 0 failures;
v4-checks 79 programs under the sanitizers 0 failures, the hosted builds
alike. The first verification failed at test_host_unit.c:442 (kept); a
stray v4-checks run stopped at once is kept, labelled (-014453).

Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_017RzZgrf7V7Zk2iczBXDRbm
2026-11-13 03:19:24 +00:00

520 lines
23 KiB
Python
Executable File

#!/usr/bin/env python3
# SPDX-License-Identifier: LicenseRef-Starship-1.0
# Copyright (c) 2023-2026 Robert A. James
"""mkpost.py -- write v4/system/post_cases.c from v3's POST cases.
v4/tools/mkpost.py [--v3 PATH] [--report FILE]
A development tool, run when the cases change; its output is committed and
reviewed like any source. docs/v4.0.0/NUCLEUS.md section 6.
What it does:
1. Reads v3's case tables, v3/src/test_runner/modules/*.c, in the order
v3's own POST runs them. A case is a word, a name, a line of FORTH and
whether an error is expected.
2. Keeps the cases for words of the FORTH-79 Required Word Set.
3. Runs every kept case, in order, in one session of the hosted v3 binary,
and records what v3 did: an error or not, the data stack, and what was
printed. v3 is the reference.
4. Writes the cases as a table in C, which the kernel holds and feeds to
the node (v4/system/post.c): for each its name, its lines, and what it
must do -- end in an error, or leave v3's stack and print v3's output.
A case is left out, and listed in the report, when: its word reads the
keyboard; it forgets a word of the system or damages it on purpose; v3 could
not finish it in one session; or one of its lines cannot be cut to fit a
64-character line. (The cases were a capsule of 64-character block lines
until MESH.md step 6b; the cutting is kept so that they are the same cases
and the same lines.)
"""
import argparse
import os
import platform
import re
import shutil
import subprocess
import sys
sys.path.insert(0, os.path.dirname(os.path.abspath(__file__)))
import post79_rules as rules # noqa: E402
ROOT = os.path.abspath(os.path.join(os.path.dirname(__file__), "..", ".."))
MODULE_DIR = os.path.join(ROOT, "v3", "src", "test_runner", "modules")
OUTPUT = os.path.join(ROOT, "v4", "system", "post_cases.c")
LINE_MAX = 64
# v3's POST order (v3/src/test_runner/test_runner.c, test_modules[]), the
# modules that test FORTH-79 words.
MODULES = [
"stack_words_test.c", "return_stack_words_test.c", "memory_words_test.c",
"arithmetic_words_test.c", "logical_words_test.c",
"mixed_arithmetic_words_test.c", "double_words_test.c",
"format_words_test.c", "string_words_test.c", "io_words_test.c",
"block_words_test.c", "dictionary_words_test.c",
"dictionary_manipulation_words_test.c", "vocabulary_words_test.c",
"system_words_test.c", "defining_words_tests.c", "control_words_test.c",
]
# The FORTH-79 Standard's Required Word Set, by the standard's own groups.
# Written from the standard's word list; check it against the document
# before relying on it for a claim of compliance.
REQUIRED = """
DUP DROP SWAP OVER ROT PICK ROLL ?DUP DEPTH >R R> R@
< = > 0< 0= 0> D< U< NOT
+ - * / MOD /MOD */ */MOD 1+ 1- 2+ 2- MAX MIN ABS NEGATE D+ DNEGATE
U* U/MOD AND OR XOR
@ ! C@ C! ? +! MOVE CMOVE FILL
DO LOOP +LOOP I J LEAVE IF ELSE THEN BEGIN UNTIL WHILE REPEAT EXIT EXECUTE
CR EMIT SPACE SPACES TYPE COUNT -TRAILING KEY EXPECT QUERY WORD
BASE DECIMAL . U. CONVERT <# # #S HOLD SIGN #>
LIST LOAD SCR BLOCK UPDATE BUFFER SAVE-BUFFERS EMPTY-BUFFERS
: ; VARIABLE CONSTANT VOCABULARY CREATE DOES>
CONTEXT CURRENT FORTH DEFINITIONS ' FIND FORGET
, ALLOT ." IMMEDIATE LITERAL STATE [ ] COMPILE [COMPILE]
( >IN ABORT QUIT HERE PAD BLK 79-STANDARD
""".split()
# Words whose cases wait for the keyboard, which a boot cannot type at.
KEYBOARD = {"KEY", "EXPECT", "QUERY"}
# ---- reading v3's case tables ----------------------------------------------
TOKEN = re.compile(r'''
\s+ | /\*.*?\*/ | //[^\n]* |
(?P<str>"(?:\\.|[^"\\])*") |
(?P<punct>[{}(),;=\[\]&*]) |
(?P<word>[A-Za-z0-9_.+\-]+)
''', re.S | re.X)
ESCAPES = {"n": "\n", "t": "\t", "\\": "\\", '"': '"', "r": "\r", "0": "\0"}
def unescape(lit):
out, i, body = [], 0, lit[1:-1]
while i < len(body):
if body[i] == "\\" and i + 1 < len(body):
out.append(ESCAPES.get(body[i + 1], body[i + 1]))
i += 2
else:
out.append(body[i])
i += 1
return "".join(out)
def tokens(text):
pos, out = 0, []
while pos < len(text):
m = TOKEN.match(text, pos)
if not m:
pos += 1
continue
pos = m.end()
if m.group("str"):
value = unescape(m.group("str"))
if out and out[-1][0] == "str": # adjacent literals join
out[-1] = ("str", out[-1][1] + value)
else:
out.append(("str", value))
elif m.group("punct"):
out.append(("punct", m.group("punct")))
elif m.group("word"):
out.append(("word", m.group("word")))
return out
def parse_braces(toks, i):
"""toks[i] is '{'; returns (nested list, index after the matching '}')."""
items = []
i += 1
while toks[i] != ("punct", "}"):
if toks[i] == ("punct", "{"):
sub, i = parse_braces(toks, i)
items.append(sub)
elif toks[i] == ("punct", ","):
i += 1
else:
items.append(toks[i][1] if toks[i][0] != "str" else ("s", toks[i][1]))
i += 1
return items, i + 1
def read_module(path):
"""Yields (word, case name, input, should_error) for every implemented case."""
toks = tokens(open(path, encoding="utf-8", errors="replace").read())
for i, t in enumerate(toks):
if t != ("word", "WordTestSuite"):
continue
j = i
while j < len(toks) and toks[j] != ("punct", "=") and toks[j] != ("punct", ";") and toks[j] != ("punct", "("):
j += 1
if j >= len(toks) or toks[j] != ("punct", "="):
continue
suites, _ = parse_braces(toks, j + 1)
for suite in suites:
if not isinstance(suite, list) or not suite or not isinstance(suite[0], tuple):
continue
word = suite[0][1]
for case in suite[1]:
if not isinstance(case, list) or len(case) < 6 or not isinstance(case[0], tuple):
continue
name, text = case[0][1], case[1][1]
should_error, implemented = case[4] != "0", case[5] != "0"
if implemented:
yield word, name, text, should_error
# ---- cutting a case's line to block lines ------------------------------------
STRING_OPENERS = {'."', 'S"', 'ABORT"', '.('}
def atoms(text):
"""The line as pieces that must each stay on one line: a word, or a word
that takes text together with its text. None if the line has a new-line
inside such a text."""
out, i, n = [], 0, len(text)
while i < n:
if text[i].isspace():
i += 1
continue
j = i
while j < n and not text[j].isspace():
j += 1
word = text[i:j]
upper = word.upper()
if upper in STRING_OPENERS or upper == "(":
close = ")" if upper in ("(", ".(") else '"'
k = text.find(close, j + 1 if j < n else j)
if k < 0:
k = n - 1
piece = text[i:k + 1]
if "\n" in piece:
return None
out.append(piece)
i = k + 1
elif word == "\\":
break # the rest of the line is a comment
else:
out.append(word)
i = j
return out
def pack(prefix, pieces, width=LINE_MAX):
"""Pieces into lines no longer than `width`, each begun with `prefix`
(which may be empty). None if a piece cannot fit on a line."""
head = [prefix] if prefix else []
lines, current = [], []
for piece in pieces:
if len(" ".join(head + [piece])) > width:
return None
if current and len(" ".join(head + current + [piece])) > width:
lines.append(current)
current = []
current.append(piece)
if current:
lines.append(current)
return [" ".join(head + line) for line in lines]
# A store to the search order, which v3's C test runner survives and a
# running FORTH system does not.
DAMAGES = re.compile(r"\b(CONTEXT|CURRENT)\s+!")
def forgets_system_word(text):
"""True if the line FORGETs a word it did not itself define. In a plain
v3 session that takes the rest of the system with it, and v4 refuses."""
words = text.split()
for i, word in enumerate(words[:-1]):
if word.upper() == "FORGET":
target = words[i + 1]
made = any(words[k] == target and k > 0 and words[k - 1].upper() in
(":", "CREATE", "VARIABLE", "CONSTANT", "VOCABULARY") for k in range(i))
if not made:
return True
return False
# ---- what v3 does --------------------------------------------------------------
ANSI = re.compile(r"\x1b\[[0-9;]*m")
def run_v3(v3, cases):
"""Runs the cases in one session. Returns a list, one entry per case:
None if v3 did not get through it, else (error, stack, output)."""
# The lines are run as the kernel sends them to the node: without the
# "T| " each began with when they were lines of a capsule. A case that
# looks at where it is in its line (>IN) depends on it.
script = [": TCLR BEGIN DEPTH WHILE DROP REPEAT ;"]
for n, case in enumerate(cases):
script.append('TCLR DECIMAL FORTH DEFINITIONS ." [[B%d]]"' % n)
assert all(line.startswith("T| ") for line in case["lines"]), case
script.extend(line[3:] for line in case["lines"])
script.append('." [[E%d]]" BASE @ DECIMAL .S BASE ! ." [[S%d]]"' % (n, n))
script.append("BYE")
# With the address space randomised, what v3 prints for an address (>IN, FIND) is different on
# every run, so the report (POST79.md) could never be written twice the same (#190): v3 is run
# with randomisation off (setarch -R), and its addresses are the same each time.
cmd = [v3, "--log-none"]
if shutil.which("setarch"):
cmd = ["setarch", platform.machine(), "-R"] + cmd
done = subprocess.run(cmd, input=("\n".join(script) + "\n").encode("latin-1"),
capture_output=True, timeout=600)
text = ANSI.sub("", done.stdout.decode("latin-1")) # a byte is a character
results = []
for n, case in enumerate(cases):
begin, mid, end = "[[B%d]] ok\nok> " % n, "ok> [[E%d]]" % n, "[[S%d]]" % n
b = text.find(begin)
e = text.find(mid, b) if b >= 0 else -1
s = text.find(end, e) if e >= 0 else -1
if b < 0 or e < 0 or s < 0:
results.append(None)
continue
body = text[b + len(begin):e]
# one "ok> " and one " ok" or " ERROR" for every line of the case
chunks = body.split("ok> ")
output, error, ok = "", False, True
for chunk in chunks:
if chunk.endswith(" ERROR\n"):
output += chunk[:-len(" ERROR\n")]
error = True
elif chunk.endswith(" ok\n"):
output += chunk[:-len(" ok\n")]
else:
ok = False
m = re.match(r"<(\d+)>((?: -?\d+)*) \n", text[e + len(mid):s])
if not ok or not m:
results.append(None)
continue
stack = [int(v) for v in m.group(2).split()]
results.append((error, stack[:-1], output)) # the last value is BASE
return results
def checksum(output):
total = 0
for ch in output.encode("latin-1", errors="replace"):
total = (total * 31 + ch) & 0xFFFFFF
return total
# ---- writing the capsule -------------------------------------------------------
def main():
ap = argparse.ArgumentParser()
ap.add_argument("--v3", default=os.path.join(ROOT, "lfs", "amd64", "starforth"))
ap.add_argument("--report", default=None)
ap.add_argument("--dump", default=None, help="write what v3 did with every case")
args = ap.parse_args()
required, left_out, cases, seen = set(REQUIRED), [], [], {}
for module in MODULES:
for word, name, text, should_error in read_module(os.path.join(MODULE_DIR, module)):
if word not in required:
continue
label = ("%s.%s" % (word, name))[:31]
seen[label] = seen.get(label, 0) + 1
if seen[label] > 1:
label = (label[:28] + "~%d" % seen[label])[:31]
if word in KEYBOARD:
left_out.append((label, "reads the keyboard"))
continue
if forgets_system_word(text):
left_out.append((label, "forgets a word of the system"))
continue
if DAMAGES.search(text.upper()):
left_out.append((label, "damages the system on purpose"))
continue
pieces = atoms(text)
lines = pack("T|", pieces) if pieces is not None else None
if not lines:
left_out.append((label, "a line cannot be cut to fit a block line"))
continue
cases.append({"label": label, "word": word, "text": text, "lines": lines, "should_error": should_error})
# v3 is run until every case left is one it gets through
while True:
results = run_v3(args.v3, cases)
bad = [i for i, r in enumerate(results) if r is None]
if not bad:
break
first = bad[0]
left_out.append((cases[first]["label"], "v3 did not get through it in one session"))
del cases[first]
table = []
disagreements, applied = [], {"address": 0, "standard": 0, "extra": 0}
def expectation(error, stack, output, mode="full"):
"""What a case must do."""
if error:
return {"expect": "V4_POST_ERROR", "stack": [], "depth": 0, "out": ""}
if mode == "depth":
return {"expect": "V4_POST_DEPTH", "stack": [], "depth": len(stack), "out": ""}
if mode == "depth+output":
return {"expect": "V4_POST_DEPTH_OUTPUT", "stack": [], "depth": len(stack), "out": output}
return {"expect": "V4_POST_STACK", "stack": list(stack), "depth": len(stack), "out": output}
def emit(label, lines, ending):
# the lines were cut for a block, each begun "T| ": the same lines, without it
assert all(line.startswith("T| ") for line in lines), lines
table.append((label, [line[3:] for line in lines], ending))
dump = []
for case, (error, stack, output) in zip(cases, results):
label = case["label"]
dump.append("%s\n input: %s\n v3: %s stack=%s out=%r\n"
% (label, " ".join(case["text"].split()), "ERROR" if error else "ok", stack, output))
if error != case["should_error"]:
disagreements.append((label, "v3's table says %s, v3 %s"
% ("error" if case["should_error"] else "no error",
"raised one" if error else "raised none")))
if label in rules.STANDARD:
rule = rules.STANDARD[label]
if rule is None: # the case is dropped
applied["standard"] += 1
left_out.append((label, rules.DROPPED[label]))
continue
lines = pack("T|", atoms(rule.get("text", case["text"])))
assert lines, label
if "depth" in rule:
emit(label, lines, {"expect": "V4_POST_DEPTH", "stack": [], "depth": rule["depth"], "out": ""})
else:
emit(label, lines, expectation(rule.get("error", False), rule.get("stack", []), rule.get("out", "")))
applied["standard"] += 1
elif label in rules.ADDRESS:
emit(label, case["lines"], expectation(error, stack, output, rules.ADDRESS[label]))
applied["address"] += 1
else:
emit(label, case["lines"], expectation(error, stack, output))
for rule in rules.EXTRA:
lines = pack("T|", atoms(rule["text"]))
assert lines, rule
emit(rule["label"], lines, expectation(rule.get("error", False), rule.get("stack", []), rule.get("out", "")))
applied["extra"] += 1
unknown = [k for k in list(rules.STANDARD) + list(rules.ADDRESS) if k not in {c["label"] for c in cases}]
assert not unknown, "rules for cases that do not exist: %s" % unknown
if args.dump:
open(args.dump, "w").write("\n".join(dump))
write_table(table)
tested = sorted({c["word"] for c in cases} | {r["label"].rsplit(".", 1)[0] for r in rules.EXTRA})
untested = [w for w in REQUIRED if w not in set(tested)]
dropped = sum(1 for v in rules.STANDARD.values() if v is None)
total = len(cases) - dropped + len(rules.EXTRA)
assert total == len(table), (total, len(table))
report = ["POST cases: %d, in %s" % (total, os.path.relpath(OUTPUT, ROOT)),
" from v3 unchanged: %d" % (len(cases) - applied["address"] - applied["standard"]),
" from v3, address-dependent (post79_rules.ADDRESS): %d" % applied["address"],
" rewritten or dropped for FORTH-79 (post79_rules.STANDARD): %d, of which dropped %d" % (applied["standard"], dropped),
" written by hand (post79_rules.EXTRA): %d" % applied["extra"],
"Required words with at least one case: %d of %d" % (len(tested), len(REQUIRED)),
"Required words with no case: " + " ".join(untested), "",
"Left out (%d):" % len(left_out)]
report += [" %-32s %s" % item for item in left_out]
report += ["", "v3 did not do what its own table expects (%d):" % len(disagreements)]
report += [" %-32s %s" % item for item in disagreements]
text = "\n".join(report) + "\n"
write_doc(cases, results, left_out, disagreements, untested, total, applied, dropped)
if args.report:
open(args.report, "w").write(text)
sys.stdout.write(text)
def c_string(text):
"""`text` as a C string literal: everything that is not plain is octal."""
out = []
for ch in text.encode("latin-1", errors="replace"):
if 32 <= ch < 127 and ch not in (34, 92, 63): # not " \ or ? (no trigraphs)
out.append(chr(ch))
else:
out.append("\\%03o" % ch)
return '"' + "".join(out) + '"'
def write_table(table):
with open(OUTPUT, "w", encoding="ascii") as out:
out.write("/* post_cases.c -- POST's cases for the FORTH-79 Required Word Set on v4.\n"
" * Generated by v4/tools/mkpost.py from v3's POST cases: do not edit.\n"
" * docs/v4.0.0/NUCLEUS.md section 6; docs/v4.0.0/POST79.md lists every case\n"
" * that is not v3's own with v3's result.\n */\n"
'#include "v4/post.h"\n\n')
for k, (label, lines, want) in enumerate(table):
out.write("static const char *const l%d[] = { %s };\n" % (k, ", ".join(c_string(line) for line in lines)))
if want["stack"]:
out.write("static const long long s%d[] = { %s };\n" % (k, ", ".join("%dLL" % v if v != -9223372036854775808 else "(-9223372036854775807LL - 1)" for v in want["stack"])))
out.write("\nconst v4_post_case v4_post_cases[] = {\n")
for k, (label, lines, want) in enumerate(table):
out.write(" { %s, l%d, %du, %s, %s, %du, %s, %du },\n"
% (c_string(label), k, len(lines), want["expect"], ("s%d" % k) if want["stack"] else "0", want["depth"],
c_string(want["out"]), len(want["out"].encode("latin-1", errors="replace"))))
out.write("};\n\nconst unsigned v4_post_case_count = %du;\n" % len(table))
DOC = os.path.join(ROOT, "docs", "v4.0.0", "POST79.md")
def code(text):
return "`" + " ".join(text.split()).replace("|", "\\|") + "`"
def expects(rule):
if rule.get("error"):
return "an error"
if "depth" in rule:
return "%d value(s) left; output not compared" % rule["depth"]
return "stack `%s`, prints %s" % (" ".join(str(v) for v in rule.get("stack", [])) or "empty",
"`%s`" % rule["out"].replace("\n", "\\n") if rule.get("out") else "nothing")
def write_doc(cases, results, left_out, disagreements, untested, total, applied, dropped):
by_label = {c["label"]: (c, r) for c, r in zip(cases, results)}
out = ["# POST for the FORTH-79 Required Word Set: where it departs from v3", "",
"Written by `v4/tools/mkpost.py` from `v4/tools/post79_rules.py`; do not edit.",
"Design: `NUCLEUS.md` section 6. The cases are `v4/system/post_cases.c`.", "",
"POST runs %d cases. %d are v3's, with what the hosted v3 binary did as the" % (total, len(cases) - applied["address"] - applied["standard"]),
"expected result. This file lists every other case, and why.", "",
"## 1. Rewritten for FORTH-79 (%d)" % (applied["standard"] - dropped), "",
"v3 departs from the standard, or the case is written for v3's machine. v4",
"follows the standard (standing ruling), so the expected result is the",
"standard's and not v3's.", "",
"| Case | v3's line | What v3 did | As POST runs it | Must do | Why |", "|---|---|---|---|---|---|"]
for label, rule in rules.STANDARD.items():
if rule is None:
continue
case, (error, stack, output) = by_label[label]
did = "error" if error else "stack `%s`, printed `%s`" % (" ".join(map(str, stack)) or "empty", output.replace("\n", "\\n")[:40])
ran = code(rule["text"]) if "text" in rule else "unchanged"
out.append("| `%s` | %s | %s | %s | %s | %s |" % (label, code(case["text"]), did, ran, expects(rule), rule["why"]))
out += ["", "## 2. Address-dependent (%d)" % applied["address"], "",
"The case leaves or prints a memory address, which is a different number on",
"the two machines. The number of values left is checked, and what is",
"printed unless an address is printed; the values are not.", "",
"| Case | Line | Checked |", "|---|---|---|"]
for label, mode in rules.ADDRESS.items():
out.append("| `%s` | %s | %s |" % (label, code(by_label[label][0]["text"]),
"values left, and output" if mode == "depth+output" else "values left only"))
out += ["", "## 3. Written by hand (%d)" % len(rules.EXTRA), "",
"For required words v3 has no case for. The expected results are the",
"standard's; no v3 run stands behind them.", "",
"| Case | Line | Must do |", "|---|---|---|"]
for rule in rules.EXTRA:
out.append("| `%s` | %s | %s |" % (rule["label"], code(rule["text"]), expects(rule)))
out += ["", "## 4. v3 cases left out (%d)" % len(left_out), "", "| Case | Why |", "|---|---|"]
out += ["| `%s` | %s |" % item for item in left_out]
out += ["", "## 5. Required words POST does not test", "",
" ".join("`%s`" % w for w in untested) + ".", "",
"`KEY`, `EXPECT` and `QUERY` wait for the keyboard, which a boot cannot type",
"at. `QUIT` returns to the terminal without `ok`.", "",
"## 6. Where v3 did not do what its own table expects (%d)" % len(disagreements), "",
"POST expects what v3 did, unless section 1 says otherwise.", "", "| Case | |", "|---|---|"]
out += ["| `%s` | %s |" % item for item in disagreements]
open(DOC, "w").write("\n".join(out) + "\n")
if __name__ == "__main__":
main()