main.pl
The nanofil command line: the impure driver that reads a C or IR file, runs it through the compiler's stages and prints the result.
Commands
| Command | Does |
|---|---|
check FILE | read and validate; prints ok |
print FILE | read, validate, print the IR (ir_text.pl) |
compile FILE | read, validate, print x86-64 assembly |
cc FILE | compile C (.c, or preprocessed .i) to Fil-C assembly |
cc-ir FILE | compile C, print the IR (unchecked; the Fil-C backend's input is pizlonated) |
checked-terms FILE | print, without its context items, the checked module cc (a C file) or compile (a Fil-C IR file) gives the backend, as a term (rocq/gate.sh) |
tokens FILE | print C token terms, without locations |
run FILE FN ARG... | interpret FN on integer arguments |
difftest FILE OUTDIR | write OUTDIR/expected.txt, OUTDIR/harness.c and OUTDIR/mode for the file's runFn, Args facts |
outcomes FILE | print the checked module of a Fil-C IR file and the interpreter's outcome of each run line, as terms (rocq/) |
asm-terms FILE TEXT | as compile for a Fil-C module, but write the assembly text to the file TEXT and print each asm.pl line as a term (rocq/backend) |
abi-terms FILE | print the checked module of a Fil-C file, then the reference ABI plan of each of its functions and its weak thunks' plans, as terms (rocq/backend) |
encode FILE OUT | read, validate and write the module as NFB, the bytecode of nfb.pl, to OUT (docs/nfb.md) |
encode-input FILE OUT | as encode, without the CONTEXT section: the input of nanofil-backend compile-nfb (docs/nfb.md) |
decode FILE | read an NFB file, validate, print the IR |
nfb-terms FILE PREFIX | write the module, and a Fil-C module's checked module, as NFB with NAMES to PREFIX.unchecked.nfb and PREFIX.checked.nfb, and print each as nfb_moduleStage, Module without its context items (rocq/backend) |
nfb-check FILE | write the module, and a Fil-C module's checked module, as NFB and read each back: the same term with NAMES, the same words without it (tests/nfb.sh) |
emit-terms FILE | print the checked module of a Fil-C file, then the reference emission's asm.pl lines, a list for each item, for each weak thunk and for the end of the file, as terms; a .i file is a Fil-C module whatever it uses, as for cc (rocq/backend) |
pizlonate-terms FILE | print the module of a file and then its pizlonation, each without its context items, as terms: the result of pizlonate.pl alone, neither validated nor passed to the check passes (rocq/backend) |
promote-terms FILE | print the module of a file, then what promote.pl makes of it, then what copy.pl makes of that, each without its context items, as terms (rocq/backend) |
compile-promoted FILE | as compile with only the passes promote and copy, stack registers, selected branches, called copies and reference checks: what the extracted compiler's compile-promoted must print (rocq/backend) |
read-terms FILE | print the module of an IR text file as a term, as read: every item, the context items included, and not validated (rocq/backend) |
read-each FILE... | for each IR text file in turn, print readModule with the module read-terms prints, or refused where reading it throws (rocq/backend) |
A FILE ending in .c or .i goes through the C frontend, one ending in .nfb is NFB, and any other FILE is IR text. A .c file is preprocessed with the predefined macros and include paths of $FILCC (default filcc).
cc runs the whole pipeline; c_pp lexes with c_lex. IR text enters at the middle end, and a module in plain mode goes to amd64.pl instead of pizlonate and filc_amd64.
-O
-O before the command runs the middle end (opt.pl) after loading. Without it the IR goes to the backend as loaded, which is the reference the optimized path is checked against. With -O, difftest also runs every run line on the unoptimized module and fails unless each optimized outcome refines the original one (translation validation), and prints how many allocs promote removed.
--registers=stack|temps|pointers independently selects reference emission or validated whole-function register homes for scalars with validated register operands and frame cells, on a frame with a home per scalar temporary (docs/perf.md items 3, 5a-loads and 3d), in the Fil-C backend. Pointers is temps with pointer address words as homes too, their lowers staying in the frame record (docs/perf.md 5b-2). The default is pointers with -O and stack without it; NANOFIL_REGISTERS supplies the same choice to build harnesses, -O --registers=temps keeps scalar homes only, and -O --registers=stack keeps the reference emission. The modes local, function, operands, cells and flow were retired in October 2026 (docs/perf.md, register modes) and are refused. The plain backend is unchanged. Options precede the command.
--operands=rewrite|regions selects, under temps or pointers, how each straight-line region's operands are chosen once the homes are in registers: rewrite, step 3b's forwarding of copies, or regions, which selects each region's registers again from the values the validated stream computes, operating on homes directly, with lea and three-address forms (docs/perf.md item 19). Both are checked by the same operand checker. The default is regions; NANOFIL_OPERANDS supplies the same choice.
--slow-calls=reference|save (NANOFIL_SLOW_CALLS) selects ordinary SysV slow calls, the default, or local r10/r11 save stubs for poll, store-barrier and ensure-aux calls. Only save mode lets register homes cross those calls in r10/r11 (docs/abi-findings.md).
--registers-limit=N (or NANOFIL_REGISTERS_LIMIT), opt-in, emits each function of more than N checked IR instructions by the reference (stack) emission when registers are temps or pointers, to save compile time on very large functions (docs/perf.md, compile time).
--branches=reference|selected independently selects the reference branch on a stored boolean, or a branch on the flags of a compare that only the branch reads, with jumps to the next block left to fall through (docs/perf.md). The default is selected with -O and reference without it; NANOFIL_BRANCHES supplies the same choice, and -O --branches=reference keeps the reference branches.
--memcpy=call|inline independently selects the reference call for every memcpy and memmove, or, for a constant 1 to 16 bytes to a function the module does not define, an inline copy in front of that call, taken only when the runtime's checks would pass and neither object has aux (docs/perf.md item 7a). The default is inline with -O and call without it; NANOFIL_MEMCPY supplies the same choice, and nanofil-cc passes call for -fno-builtin, -fno-builtin-memcpy, -fno-builtin-memmove and -ffreestanding.
--bounds=split|merged|sign|or selects the bounds check's shape: split, the default, tests ptr < lower and ptr > upper - Size with a branch each; merged tests both with one unsigned comparison of ptr - lower; sign and or test (ptr - lower) | (upper - Size - ptr) with one branch (docs/bounds.md). NANOFIL_BOUNDS supplies the same choice.
--share=none|block|null|upper shares parts of heap checks of one object under split bounds and local selection: block leaves out the null test of a check whose lower an earlier check in its block tested, null also when that check is in a dominating block, and upper also reuses the upper a check of the same object just loaded (src/check_share.pl, docs/perf.md item 17). The default is upper with -O, except with --checks=reference, and none otherwise; NANOFIL_SHARE supplies the same choice.
--lowers=own|shared selects the frame's GC roots: own, the default, gives every pointer temporary its own lowers[] entry; shared lets a flight use its lower root's entry, kept while the flight is live, and validates every frame (src/lower_roots.pl, src/lowers_check.pl, docs/lowers.md). NANOFIL_LOWERS supplies the same choice.
--inline=none|small|wide independently selects no inlining, or, with -O, inlining of small static functions before promotion (src/inline.pl, docs/perf.md item 4), or that and more: always_inline, single-call-site and non-leaf callees, callees first (item 20). The default is wide with -O; without -O nothing inlines. NANOFIL_INLINE supplies the same choice, and nanofil-cc passes none for -fno-inline and -O0. A trap inside an inlined function reports its caller's name, as filcc -O2 does without -g.
--simplify=none|full independently selects, with -O, the cheap middle end after copy propagation (src/simplify.pl, docs/perf.md item 8). The default is full; NANOFIL_SIMPLIFY supplies the same choice.
--checks=reference|reuse|renew|guard|hoist|schedule|half|forward|combined|hull|getter|extended independently selects the reference checked IR, a check before every access, check reuse after pizlonation, reuse followed by renewal of dominated checks, both followed by range guards for checks in loops, both followed by hoisted bounds, a limit taken before a loop for its full checks of a root defined before it, or both followed by scheduled checks, which check early the bytes every path ahead needs and renew what they cover; a scheduled check may trap before stores that precede the failing access, or both followed by half checks, which test only the bound an earlier check of the object does not already establish, or reuse that also serves pointer loads and covers a check by the hull of its object's live facts, then renewal, which moves no trap, or that followed by half checks (combined), combined with renewal by the hull of two checks (hull), with facts kept across repeated getters of local globals (getter), or both (extended) (src/check_reuse.pl, src/schedule.pl, src/half_check.pl, docs/m7.md, docs/bounds.md, docs/schedule.md, docs/half.md, docs/forward.md). The default is combined with -O and reference without; NANOFIL_CHECKS supplies the same choice. With any but reference, cc, compile and difftest's pizlonation comparison use that module.
GNU vector types and the SSE through AVX2 intrinsics (docs/vector-access.md) are on; --no-vectors (or --vectors=off) turns them off, refusing every vector type, and --vectors (or --vectors=on) turns them back on; the last one given wins. NANOFIL_VECTORS=0 or 1 supplies the same choice.
difftest
expected.txt holds the interpreter's result for every run line whose outcome a native run can reproduce: a known return value, or for a Fil-C module a trap, written just trap. harness.c prints the same lines from native code; for a Fil-C module it makes one call per process, chosen by argv[1], since a trap ends the process. mode holds plain or filc. Other outcomes are reported on stdout and left out of the comparison.
For a Fil-C module, difftest also runs every run line on the pizlonated module and fails unless each outcome is the same, traps and their reasons included.
Compile-only commands do not need the interpreter or its CLP(Z) solver.
The emission choices: emit(Registers, Branches, Copies).
NANOFIL_CHECKS, or unbound until -O decides.
Argv is Argv0 less its vector options, the last of which sets NANOFIL_VECTORS (c_types vector_type/4), for drivers that pass only options: --vectors and --vectors=on to 1, --no-vectors and --vectors=off to 0.
Argv is Argv0 less its --bounds= options, the last of which sets NANOFIL_BOUNDS, the bounds check's shape (filc_amd64:bounds_check//4): split, the default, merged, sign or or.
Argv is Argv0 less its --lowers= options, the last of which sets NANOFIL_LOWERS (lower_roots:lowers_mode/1).
Argv is Argv0 less its --operands= options, the last of which sets NANOFIL_OPERANDS (amd64_regs:operand_selection/1).
the last --slow-calls option selects the opt-in compiler-local r10/r11 save stubs. With no option NANOFIL_SLOW_CALLS applies; unset means reference, even under -O.
Argv is Argv0 less its --inline= options, the last of which gives Inline.
NANOFIL_INLINE, or unbound until -O decides.
as inline_options/4, for --registers-limit=N; Limit is none or a nonnegative integer.
limited(R, N) for temps or pointers registers under a limit (filc_amd64.pl's item_placed_lines/6).
as inline_options/4, for --simplify=.
NANOFIL_SIMPLIFY, or unbound until -O decides.
the middle end's selection (opt.pl). Inlining and simplification need -O, where inlining is wide and simplification full unless chosen otherwise.
Registers is the register mode for optimization level Opt (o0 or o1) when no --registers option or NANOFIL_REGISTERS chose one: stack, the reference emission, without -O, and pointers, a home per scalar temporary and per pointer address word (amd64_regs.pl), with it. branches_default/2 does the same for branch selection: reference without -O, selected with it.
-O combines forward facts and half checks (docs/forward.md, docs/half.md); without it every access keeps its full check.
Loading
Module is the valid IR module in File. A .c or .i file goes through the C frontend, a .nfb file is NFB, and anything else is IR text.
Module is the valid IR module of the C file. c_file_module/4 also gives the assembly lines of its top-level asm (c_lower c_toplevel_asm/2), which cc prints after the module, and its functions' inlining attributes (c_lower c_module/3).
Tokens are the C tokens of File. A .i file is already preprocessed; anything else goes through c_pp with the predefined macros and include paths of $FILCC (default filcc).
Commands
release_stacks: collect garbage and return unused stack memory to the system between the stages of a large compile. SWI grows its stacks between collections and keeps them grown, and its stack limit counts what is allocated, not what is live: gnulib's test-intprops.c, whose main has 87,000 blocks, never has more than about 210 MB live, yet the frontend leaves the trail at 250 MB and the middle end the global stack at 1 GB, and the next collection, which must shift them first, exceeds the default 1 GB limit. A host without these predicates skips them.
Runs the command Args, [Command|Operands], such as [cc, File]; the header comment's table lists the commands. Opt is the middle end's selection: o0 without -O, else o1, o1(Inline) or o1(Inline, full) (opt.pl). Registers is the emission choice emit(Registers, Branches, Copies), and Checks the check passes (checks_module/3). Only native emission needs Registers and only the Fil-C checked stage needs Checks (difftest runs it too). Throws nanofil_error(Msg) for a refused program.
cc a .i file, and cc compiles any module aswide inlining takes the C file's always_inline and noinline functions (c_module/3), which the IR does not carry, in its selection. Other selections are unchanged.
carry out the command line Args (without options), running the middle end when Opt is o1 (-O given) and not when o0. Fails or throws when the command does.
Module, written as NFB, reads back as itself, and its core sections alone read back as a module whose core encoding is those very words (nfb.pl). Prints the sizes; throws nanofil_error otherwise.
Code is Module without its context items.
write Module, its context items dropped, as NFB with NAMES to Prefix.Stage.nfb, and print it as nfb_module(Stage, Module) for the Gallina reader and writer (rocq/backend/tests/nfb.sh).
Prints, as Prolog terms, the checked module of the Fil-C IR File (after the middle end when Opt is o1, and the check passes Checks) and then, for each run line, outcome(Fn, Args, Fuel, Outcome), the interpreter's outcome on that module, or error(Fn, Args, Fuel, E) when the run throws E or finds no outcome. An independent model of the checked IR (rocq/, docs/formal.md) reads them.
Prints the assembly of Module by the backend for Mode, filc or plain. Fil-C prints one item at a time (filc_module_emit/3), since a large module's lines (SQLite's) need not all be held at once.
the text of the asm.pl lines Lines to Stream, and each line as a canonical term and a full stop to the current output. The extracted printer must turn the terms into the text (rocq/backend/tests/asm.sh).
Term as a canonical term and a full stop.
Checked is Module pizlonated (pizlonate_module/2), validated as checked IR (valid_module/1), and then rewritten by the check passes Checks selects (checks_module/3). Throws if the validator refuses either.
Checked is the checked module Checked0 after the check passes of Checks (--checks; docs/m7.md): reference keeps pizlonate's naive checks; reuse deletes a check an earlier live one covers; renew also replaces a dominated check by a test of only the free and read-only flags; guard also puts a span test before a loop and makes its checks renew_if; combined, the -O default, is forward facts followed by half checks; hull, getter and extended add renew_hull and facts across repeated getters (docs/forward.md). Each pass's result must pass its *_refines identity check against its input, and the validator (valid_module/1) then checks the result's evidence again on its own.
Renew (docs/m7.md, round 4) runs after reuse: what reuse keeps, a dominating check may renew. Only the result is validated: a renew keeps its check's proof and index, so reuse's output is valid if it is.
Guards (docs/m7.md, round 5) run after renewal: a check renewal left in a loop may become a guarded renewal. Only the result is validated.
Hoisted bounds (docs/bounds.md) run after renewal: a full check renewal left in a loop may test its bounds against a limit taken before the loop. Only the result is validated.
Scheduled checks (docs/schedule.md) run after renewal: a check widens over the bytes every path ahead needs from its base, and the checks it then covers are renewed at a distance. Only the result is validated.
Half checks (docs/half.md) run after renewal: a full check renewal left whose object an earlier check covers at one end tests only the other. Only the result is validated.
Forward facts (docs/forward.md): reuse that also serves heap pointer loads and covers a check by the hull of its object's live facts, then renewal at any distance (docs/schedule.md's renew from a related pointer's check). No trap moves. Only the result is validated.
Combined: forward facts, then half checks for what renewal left. Each stage keeps its own refines check. Only the result is validated.
Combined with renewal by the hull of two checks (hull), with facts kept across repeated getter calls (getter), or both (extended), opt-in (docs/forward.md). Each stage keeps its own refines check.
For a filc module, the checked Module (checked_module/3 with Checks) has the same outcome as Module on every run of Runs, traps and their reasons included, or the command throws: the explicit checks are exactly the implicit ones. A missing or too weak check shows as the outcome unchecked(Why). Both run with the same fuel, since pizlonate keeps every block. A plain module has nothing to compare.
with -O (o1), the optimized Module is valid. valid_module's clauses leave choice points that throw on retry.
with -O (o1), report_validation/4.
Prints the -O difftest report: promote's effect, then every validation failure among Verdicts, which together make the command throw.
Running and validating
Fuel (blocks run) for a command-line run and the last validation step.
validated_run(+Opt, +Original, +Optimized, +Run, -Result, -Verdict): Result is Run's r/3 on the module that difftest compares, and Verdict ok or bad(CallText, OriginalText, OptimizedText).
Translation validation: the unoptimized module's outcome on the same run must allow the optimized one's. Both runs happen in the same findall step, so an unknown result keeps its constraints. Promote keeps every block and branch, so a correct result needs exactly the blocks the original needs: both run with the same fuel, starting small and growing until the original finishes. A broken pass that loops then ends as out_of_fuel, cheaply (the interpreter's memory grows quickly with the number of blocks run, so a looping run at full fuel would exhaust it).
the optimized module's fuel. Inlining adds a join block per inlined call, at most one block run for each block the original runs.
Fuel is one of the growing fuel limits, smallest first, ending at max_fuel.
Result is the r(Fn, Args, Outcome) of the "# run:" line Run on a module and the interpreter's preparation of it, with Fuel. Throws if the line does not fit the module or the interpreter finds no outcome.
a native run in Mode (plain or filc) reproduces Result's outcome, a known return value or, for filc, a trap or a reached unreachable, both a Fil-C safety panic natively. Nothing else has a native counterpart.
Text is the atom 'Fn(A1, A2, ...)'.
difftest output files
write the characters Body2 (a DCG body) describes to File.
one "CALL = OUTCOME" line per result, a trap's outcome shown as just "trap" (the native run cannot tell why). Only Fil-C mode compares unreachable, which panics there.
a C program that calls Module's functions as Results do and prints what expected_lines//1 prints.
Fil-C: one run per process, selected by argv[1], since a trap ends the process. The call text is printed first, so a trap leaves it unfinished.
Fns is the ordset of the functions Results call.
the switch cases I, I+1, ... of the Fil-C harness, one per result.
an extern C declaration of each of Fns.
Style labelled prints "CALL = ret N" lines from one main; bare prints "ret N" inside a case.
the line of harness_calls//3 for one call of Fn, which returns Ret.
as harness_call//5, for a call with Result.
main's line for a call of Fn.
Runs
Runs are the run(Fn, Args) facts of IR File, in order.
library(format)'s format_//2 raises type_error(list, '') for an argument of '' (Trealla 12f4cbd), which a call with no arguments produces. fmt(+Format, +Args)//: the characters format/3 makes of Format and Args.