M1: IR, relational interpreter, QBE subset
Archived: a record of finished work, kept as written. nanofil's archive lists the others.
M1 built the IR as a QBE subset, with a QBE text parser and printer and differential tests against real qbe. Since October 2026 the IR is nanofil's own: src/ir.pl's terms, their meaning in src/interp.pl, and Prolog-clause text read and printed by src/ir_text.pl. The QBE parser, printer and qbe difftest are gone. The table and commands below are current; the rest records M1 as it was.
What exists
| File | Role |
|---|---|
| src/ir.pl | IR terms (documented at the top) and a validator that reports the first problem with a function name |
| src/ir_text.pl | IR files as Prolog clauses, read with read_term/3 and
printed in a stable layout |
| src/interp.pl | run(Module, Fn, Args, Fuel, Outcome), the semantics in
CLP(Z) |
| src/main.pl | Driver: check, print, run,
difftest |
At M1 the subset was QBE's integer IL: classes w and
l, all integer arithmetic, comparisons, extensions, loads,
stores, alloc, jmp/jnz/
ret/unreachable, phis, direct calls between
functions in the module, and data definitions with integer, string,
symbol and zero items. Floats, aggregate types, variadics, external
calls and blit are rejected.
cd nanofil/src
../bin/nanofil run ../tests/fixtures/memory.ir fibs 15 # ret 610
../bin/nanofil --script ../tests/unit.pl
../tests/difftest.sh ../tests/fixtures/*.ir
nix build .#checks.x86_64-linux.nanofilSemantics decisions
- Values are integers in
0..2^bits-1. Reading anlvalue atwtakes its low 32 bits, as the IL's subtyping says.jnzreads its argument atw. - Shift counts are taken modulo the width, matching x86 and qbe.
- Division by zero and
INT_MIN / -1are outcomes,ub(...), not failures. So are accesses outside every live allocation, including use of a callee'sallocafter it returns (addresses are never reused). - Unwritten bytes are fresh variables in
0..255. A load of them is an unknown value, never a made-up one. - Memory is an assoc from byte address to byte, plus the list of live regions. Addresses and allocation sizes must be known when an access runs; otherwise an instantiation error is raised. That is incomplete but never wrong, and it was the M1 open question about modelling memory. Symbolic addresses can wait until a pass needs them.
Because arithmetic and branches are constraints, run/5
runs backwards. The unit tests ask which input makes
3x + 1 = 7 (x = 2), which input reaches
unreachable, and for an input where signed division by 2
and sar 1 differ (−1).
Testing
- Differential.
difftestwrites the interpreter's result for every# run:line with a known return value, and a C harness calling the same functions.difftest.shcompiles both the original file and nanofil's printed version of it with realqbe, runs them and diffs the results. This tests the interpreter, the parser and the printer at once. - Random.
tests/gen.py, since replaced by its Prolog port tests/gen.pl, generates functions mixing both classes, edge-value constants, diamonds with phis, counted loops and overlapping stack stores and loads. Seeds 1 to 8 (1,600 functions) gave 8,098 compared runs with no mismatch once the qbe bugs below were avoided. About 17% of runs end inuband are not compared. - Unit. tests/unit.pl
covers what native runs cannot:
ub,unreachable, fuel, unknown bytes, backwards queries, diagnostics and the printer round trip. The expected values are derived by hand. - Mutation check (manual). Six deliberate interpreter
bugs were each caught by the fixtures and the random corpus: truncating
sar, sequential phis,jnzreading 64 bits, unsignedextsb, flooredremand big-endian loads.
qbe bugs found
The interpreter disagreed with qbe four ways. The first three
reproduce with nixpkgs qbe 1.2 and upstream c081897 (May
2026). Each is a fixture in tests/backend/,
and the unit tests pin the answer the IL document gives for the first
three.
- storew-l.ir.
Load forwarding after a sub-word store of a value with bits beyond the
store width (an
ltemp, or a constant such as −661) does not mask those bits, so an overlapping narrower load sees them. - jnz-shift-flags.ir.
jnzreuses the flags of the shift that defines its argument, but an x86 shift by zero leaves flags unchanged. - jnz-long-flags.ir.
After a 64-bit op,
jnztests all 64 bits instead of the low 32 the IL specifies. With a plainlparameter, qbe tests 32 bits. - jnz-long-const.ir.
The same when the
largument folds to a constant (c081897only), found once the generator stopped avoiding bug 3.
qbe also emits an unmasked constant shift count as an immediate that
GNU as rejects outside 8 bits. The check uses qbe
c081897 built by nix/qbe.nix
with fixes for all five, kept as patches/qbe-*.patch in the
filnix tree, so the generator no longer avoids these patterns.
Trealla bug found
A clause whose body has a CLP(Z) goal over a ground integer constant
of at least 2^63, such as Z #= X mod 18446744073709551616,
crashed Trealla 12f4cbd and upstream head
ba473a6. Natively it segfaulted; the Fil-C build reported
cannot write pointer to free object in
set_var. Goal expansion pasted the expanded goal's cells
into the clause and then destroyed the sub-parser, freeing the bigint.
filnix now carries patches/trealla-goal-expansion-share-cells.patch
in both the Fil-C port and nanofil's native Trealla; it has not been
sent upstream yet.
The unit tests also pass under the Fil-C Trealla
(pkgsFilc.trealla), in about 5 s against 0.6 s
natively.