ir.pl
The nanofil IR: modules of functions and data as ground Prolog terms, the contract between the frontend, the middle end, the interpreter and the backends. This module states its grammar and checks that a module is well formed.
A function is a list of blocks; a block is phis, then instructions, then one jump. Temps are ground names; logic variables never appear in IR terms.
funcName, Linkage, Ret, Params, BlocksphitmpD, K, PairsClasses
Every value has a class, one letter:
| Class | Value |
|---|---|
w | 32-bit integer (a word) |
l | 64-bit integer (a long) |
s | 32-bit float (single) |
d | 64-bit float (double) |
x | x87 80-bit extended float (C's long double; filc mode only, never a parameter, result, call argument or phi: docs/float.md) |
p | pointer: an address with its Fil-C capability (filc mode only) |
a | proven address: a pointer or named-local access that a check has cleared (checked stage only) |
f | proven function: a p that a function check has cleared (checked stage only) |
A store's width may also be b (8 bits) or h (16 bits). A load and ext name the narrow types sb ub sh uh sw uw: signed or unsigned byte, halfword and word.
Items
| Term | Means |
|---|---|
moduleItems | Items are func/5, data/4, alias/3 and optional context/2 terms |
funcName, Linkage, Ret, Params, Blocks | a function, fields below |
dataName, Linkage, Align, Items | a data object, fields under Data |
aliasName, Linkage, Target | a second symbol Name, of linkage export or weak, for the function or data object Target the module defines (filc mode only; GNU's alias attribute) |
contextName, Records | explanatory binding, typed-origin, value, alias and site records; see provenance.pl |
| Field of func | Is |
|---|---|
| Name | an atom, the symbol |
| Linkage | export, local, or weak (filc mode only): exported, and a strong definition elsewhere replaces it |
| Ret | w, l, p, s, d, void, or tupleK1, K2 |
| Params | a list of paramK, tmpN, K one of w l p s d |
| Blocks | a list of blockLabel, Phis, Insts, Jump, the entry block first |
A tupleK1, K2 return is two words, each Ki l, p, s or d: a struct of 9 to 16 bytes, its eightbytes as SysV classes them (filc mode only).
Phis and instructions
| Term | Means |
|---|---|
phitmpD, K, Pred−Value | D is Value when control came from block Pred |
lettmpD, K, Op, Args | D, of class K, is Op of Args (Ops below) |
storeWidth, Value, Addr | store Value at Addr; Width one of b h w l p s d |
atomic_storep, Value, Addr | (filc mode) store the pointer Value at Addr single-copy atomically, sequentially consistent (Fil-C's filc_store_ptr_atomic) |
fence | a sequentially consistent fence (mfence) |
accessK, Addr, Size, Align | trap as a K (read or write) access of Size (8, 16, 32 or 64) bytes at Addr with alignment Align (1, 2, 4 or 8) would, and access nothing: a vector's full-width check before its chunks (docs/vector-access.md) |
touchtmpQ | checked stage: use the proof Q of the check just before it, and do nothing else (pizlonated access) |
asm_fixedM, Ins, Outs | the fixed-register instruction M (asm_fixed_regs/3) on w inputs R-V in the registers M reads, defining w temporaries R−tmpD from registers it writes (docs/asm-fixed.md) |
local_allocName, Size | create a zeroed, exact-sized invocation-local object, without an address value |
local_loadtmpD, K, T, Name, Off | checked load semantics at the fixed byte offset Off in Name |
local_storeWidth, Value, Name, Off | checked store semantics at the fixed byte offset Off in Name |
callRes, Callee, argK, Value | call Callee: globalF, or (filc mode) a p temp |
locFile, Line | does nothing: the instructions after it, up to the next loc, come from line Line of File |
raw_storeWidth, Off, Value, Addr | checked stage: a non-pointer store at Addr+Off that does not check (Stages, below) |
raw_store_pointerOff, Value, Addr, Effects | checked stage: a pointer store whose ordered aux/barrier effects are explicit |
raw_callRes, Callee, Args | checked stage: call the proven function Callee (class f); argument, result and exception handling are as for call |
flighttmpD, Op, Args, Lower | checked stage: construct a p from a 64-bit address calculation and an independently selected capability |
A call's Res is one of resulttmpD, K, void, or tupleresulttmpD1, K1, resulttmpD2, K2.
Named locals are Fil-C-only. Their ground names have a separate namespace from temporaries. Each is declared once in the entry block, before its uses, and lives until this invocation exits. Functions with setjmp cannot contain them. Off is a signed 64-bit integer; an access outside [0, Size) traps, including every access to a zero-sized object. Pointer contents have ordinary capabilities, but a local's own native address is never a p value or heap lower.
flight computes its address with copy, add or sub, using unsigned 64-bit arithmetic. Each argument is an l value or addressP, the address bits of a p value. Lower is none or lowerP, exactly P's capability identity, not an integer bound. The donors may differ: constructing a pair proves nothing about access. No getter, check, memory access or safepoint occurs inside flight; both components become one rooted p result. Projections occur only here and cannot read globals or proof classes.
Jumps
| Jump | Means |
|---|---|
gotoL | go to L |
branchV, L1, L2 | go to L1 if V is nonzero, else to L2 |
retV | return V |
retsV1, V2 | return a tuple |
ret | return from a void function |
unreachable | stop the program (a trap instruction) |
A jump's target may be pollL: a pollcheck on the edge, after the phis' copies, then L. A pollcheck is a safepoint: the thread may run signal handlers and answer the collector.
Ops
The Op of a lettmpD, K, Op, Args; op_kind/2 and valid_op/1 state these sets once, op_result_ok/3 and op_arg_classes/4 the classes.
| Op | Result K | Args | Means |
|---|---|---|---|
add sub | any | [K, K]; at p, a p and an l offset | |
mul div | w l s d | [K, K] | |
udiv rem urem and or xor | w l | [K, K] | |
sar shr shl | w l | [K, w] | the count is read at w |
neg | w l s d | [K] | |
copy | any | [K] | |
cmpCond, K1 | w l; w when K1 is a float | [K1, K1] | Cond for K1 w or l: eq ne sle slt sge sgt ule ult uge ugt; for s or d: eq ne le lt ge gt o uo |
extT | l for sw uw; w or l for sh uh sb ub | [w] | extend the low bytes |
exts | d | [s] | single to double |
exts | x | [s] | single to extended |
extd | x | [d] | double to extended |
truncd | s | [d] | double to single |
truncx | s d | [x] | extended to single or double |
stosi stoui / dtosi dtoui / xtosi xtoui | w l | [s] / [d] / [x] | float to signed or unsigned integer |
swtof uwtof / sltof ultof | s d | [w] / [l] | signed or unsigned integer to float |
cast | w s l d | [s] [w] [d] [l] | bitwise: w and s, l and d |
loadT | as T: l, p, s, d; w or l for a narrow T | [Addr] | T one of l sw uw sh uh sb ub p s d |
allocAlign | the address class | [l], the size | Align a power of two from 4 to 4096 |
ptoi | l | [p] | filc only |
itop | p | [l] | filc only |
va_args | p | constN | filc only: a cursor into the entry argument snapshot; N, non-negative, is the byte count of the fixed prefix |
va_arg | any | [p] | filc only: a load through a va_list address, advancing its cursor (reads and writes memory) |
setjmpKind | w | [p, w]: Buf, SaveMask | filc only, below |
checkLo, Hi, Rights, Align | a | [p] | checked stage, below |
check_aheadLo, Hi, Rights, Align, AHi | a | [p] | checked stage: checkLo, Hi, Rights, Align of which only [Lo, AHi) is its own access's requirement; the rest is anticipated (docs/schedule.md) |
renewLo, Hi, Rights, Align | a | [a, p]: Q1, P | checked stage: renew an earlier heap proof's temporal facts (docs/m7.md, round 4) |
renew_hullLo, Hi, Rights, Align | a | [a, a, p]: QL, QH, P | checked stage: a renew whose bounds the hull of two earlier heap proofs of P's object covers (docs/forward.md, multi-source renewal) |
half_checkBound, Lo, Hi, Rights, Align | a | [a, p]: Q1, P | checked stage: checkLo, Hi, Rights, Align of P, which tests only the bound Bound, upper or lower; Q1's earlier check of the same object proves the other (docs/half.md) |
span_testLo, Hi | w | [p] | checked stage: 1 if the pointer's object contains [P+Lo, P+Hi), else 0; never traps (docs/m7.md, round 5) |
renew_ifLo, Hi, Rights, Align | a | [p, w]: P, G | checked stage: checkLo, Hi, Rights, Align of P, whose bounds part a passing span test G proves (docs/m7.md, round 5) |
limitSize | l | [p] | checked stage: an opaque snapshot of the pointer's bounds for Size-byte accesses; never traps (docs/bounds.md) |
check_limitLo, Hi, Rights, Align | a | [p, l]: P, U | checked stage: checkLo, Hi, Rights, Align of P, its bounds tested against the limit U of P's lower (docs/bounds.md) |
check_localName, Off, Bytes, Rights, Align | a | [] | checked stage: prove exact bounds and alignment for the named object, preserving its identity and offset |
atomic_loadp | p | [p] | (filc mode) a single-copy atomic, sequentially consistent pointer load (Fil-C's filc_load_ptr_atomic) |
casT | as loadT | [K, K, p]: Expected, New, Addr | (filc mode) atomic compare-exchange, below; T one of l sw uw sh uh sb ub p |
raw_casT, Off | as casT | [a, K, K] | checked stage: casT at A+Off, right after the check that covers it |
raw_loadT, Off | as loadT, except p | [a] | checked stage: a non-pointer load at A+Off that does not check |
raw_load_pointerOff, Effects | p | [a] | checked stage: read aux, resolve the lower, then read the primary address |
check_function | f | [p] | checked stage: trap unless the pointer designates a function object at its exact callable address |
casT reads [Expected, New, Addr] and is one sequentially consistent atomic step: it reads the T at Addr, old; if old equals Expected, it writes New there; the result is old, extended as loadT extends it. Equality is bitwise on the low bytes of T, and for p it compares addresses only: capabilities are ignored, so a New may replace an old that has the expected address but another capability, and the result is old's pair, as Fil-C's filc_strong_cas_ptr does. An integer cas needs write rights and its address aligned to its width, even when it fails (x86 lock cmpxchg writes; a misaligned one is a split lock, and Fil-C traps); a pointer cas, the 8-byte slot's. The checked form raw_casT, Off is right after its own check, never a reused proof. A pointer cas is heap only, with the effect list [atomic_cas]: Fil-C's helper checks again, ensures aux (it may exit), barriers New, and boxes the slot; New and Addr stay rooted through it. Every cas ends every live proof. Read-modify-writes other than compare-exchange are loops of cas (c_lower.pl); there is no other atomic read-modify-write term.
setjmpKind: Kind is setjmp, '_setjmp' or sigsetjmp, and SaveMask must be const0 except for sigsetjmp. It returns twice natively; the snapshot and restore contract is in docs/setjmp.md.
checkLo, Hi, Rights, Align reads [p P]. It traps unless P's capability permits Rights (read or write) on [P+Lo, P+Hi) and P+Lo is Align-aligned (Align one of 1, 2, 4, 8, 16); otherwise its result is P, proven accessible.
check_aheadLo, Hi, Rights, Align, AHi reads [p P], with Lo < AHi < Hi, and is exactly checkLo, Hi, Rights, Align of P: its access must lie in [Lo, AHi), and the bytes [AHi, Hi) are checked early. It is valid only where every path from its access reaches an access through P's base that needs those bytes, and reaches it first: before a call or other effect (ahead_transparent/1), a poll edge, an edge back or a return; its own access must be ahead_transparent/1 too (ahead_justified/3, docs/schedule.md). So it traps where the plain check would not only on executions that trap later anyway.
renewLo, Hi, Rights, Align reads [a Q1, p P]: Q1 is the proof of an earlier heap check of P1 that dominates it, whose bounds and alignment still hold since an object's bounds change only when it is freed, and P the pointer of the check it replaces, at a constant distance D from P1 through one base (pointer_distance/4; 0 is same_pointer/3), with its capability. Q1's check covers [Lo+D, Hi+D). It traps as checkLo, Hi, Rights, Align of P would if the object has been freed since, or if Rights is write and the object is read-only; otherwise its result is P, proven accessible. Q1 and P1 have one definition each, Q1's check covers [Lo, Hi) at Align, and the function has no setjmp (stage_func/6).
renew_hullLo, Hi, Rights, Align reads [a QL, a QH, p P] and is a renew of P whose bounds and alignment two earlier heap proofs give together: QL's check proves P's object from at or below P+Lo, QH's to at or above P+Hi, each of a pointer at an exact distance from P through one base (hull_renewable/8, docs/forward.md). It traps as the renew would.
half_checkBound, Lo, Hi, Rights, Align reads [a Q1, p P] and is exactly checkLo, Hi, Rights, Align of P: it traps when the check would, with its reason, and is followed by the access it covers. Q1 is a single-definition heap proof of P1 (a renew's sources), P is at a distance D from P1 through one base (pointer_distance/4), taken signed modulo 2^64, and so has Q1's capability. Q1's check passed for [Lo1, Hi1) of P1. Bound upper needs Lo1 =< Lo + D: P's capability is not null and P+Lo is not below lower, so only the upper end is tested. Bound lower needs Hi + D =< Hi1: P+Hi is not above the upper that check saw, which changes only when the object is freed, so only the lower end and the free flag are tested. D + Lo - Lo1 and D + Hi - Hi1 lie within +-2^62 (near_offset/1) and the function has no setjmp (half_known/6, docs/half.md).
span_testLo, Hi reads [p P0], with integers Lo < Hi. It is 1 when P0's capability is an object's and lower =< P0+Lo < P0+Hi =< upper, addresses modulo 2^64 compared unsigned, and 0 otherwise (a null, function or external capability, a freed object). It never traps and reaches no safepoint.
renew_ifLo, Hi, Rights, Align reads [p P, w G] and is exactly checkLo, Hi, Rights, Align of P: it traps when the check would, with its reason, and is followed by the access it covers. G has one definition, a span test of P0; P is P0 plus an offset through single-definition add, sub and copy flights with P0's lower; the offset's interval (guard_chain/3) shifted by [Lo, Hi) lies in the span test's [Lo, Hi); every name on the way has one definition and the function has no setjmp. When G is 1 only the free flag, the read-only flag for a write, and alignment are tested natively.
limitSize reads [p P0], with 0 < Size < 2^31. Its value is a snapshot of P0's capability and of its object's bounds, in an encoding the backend chooses; it never traps, reaches no safepoint, and is read only as a check_limit's second argument (limit_reads/2). check_limit0, Size, Rights, Align reads [p P, l U] and is exactly check0, Size, Rights, Align of P, followed by the access it covers. U has one definition, a limitSize of P0 with one definition, P has P0's lower through single-definition flights (lower_chain/3), with any address, and the function has no setjmp. Natively the bounds are tested against the snapshot and the free flag (and for a write the read-only flag) at the access: an object's bounds change only when it is freed (docs/m7.md, round 4's lifetime lemma), which sets the free flag.
check_local proves [Off, Off+Bytes) within the named object's exact size and 16-aligned base. Its adjacent raw access has offset zero. Pointer load/store effects are respectively [aux_read, address_read] and [lower_write, address_write]: explicit stack aux has neither a heap header nor a lower box. Validation selects this protocol by proof provenance, not list shape.
Values
| Value | Means |
|---|---|
tmpName | a temporary, defined once (SSA) |
constInteger | a number; at s or d an unsigned IEEE bit pattern (docs/float.md) |
globalName | the address of a function or data object, by its symbol |
Data
In dataName, Linkage, Align, Items, Align is a power of two from 1 to 4096, the payload's alignment, and Linkage is export, local, roexport or rolocal, ro for read-only data (in .rodata), or tlsexport or tlslocal (filc mode only) for C's thread-local objects: each thread has its own instance, created and initialized with Items when that thread first takes the symbol's address. The interpreter runs one thread, so there it is an ordinary object. Linkage initctor, Priority or initdtor, Priority (filc mode only) is an entry of the constructor (destructor) table, which the program runs before main (at exit) through the Fil-C runtime: Items is the one itemp, symF, 0 of a function F defined in the module, and Priority an integer from 0 to 65535, lower first, or none, after those with one. It is not an object: nothing may take its address, neither globalName nor another item's symName, _, and the interpreter does not run it. Linkage weak or roweak (filc mode only) is export that a strong definition elsewhere replaces. Linkage externweak (filc mode only), with Items [], declares that Name, which the module does not define, is weak: if no object of the program defines it, globalName is a null pointer. It is not an object. Beside a definition of Name, globalName is the definition, which may not have local linkage: the declaration would make its symbols weak and global, and another object's Name could replace them. Align is 1, 2, 4, 8 or 16. Items is a list of:
| Item | Means |
|---|---|
itemW, constN | N at width W |
itemb, strChars | the bytes themselves, one character per byte (codes 0..255); a backend escapes them when it prints assembly |
iteml, symName, Off | the address of Name plus Off (plain mode) |
itemp, symName, Off | a pointer with the capability of Name (filc mode only) |
zeroN | N zero bytes |
Each item is one of these, with integer N and Off, an atom Name and W a width of width_bytes/2; a pointer item itemp, sym_, _ starts at a multiple of 8 bytes into the object. No two items of a module, functions, data other than an externweak declaration, and aliases, define the same name (unique_names/1).
Modes
A module is in one of two modes, told apart by what it uses (module_mode/2):
| Mode | Means |
|---|---|
plain | classes w, l, s and d only. Addresses are l values, and the plain backend (amd64.pl) compiles it to ordinary x86-64. |
filc | anything of class p, a tuple return, read-only data, a pointer-only op, or a call to a function the module does not define. Addresses are p values (flight pointers with a capability), alloc yields p, loads and stores take a p address, p arithmetic is add or sub of an l offset, and ptoi and itop convert. |
In filc mode calls may name functions outside the module, or go through a p value. A call may name data the module defines; it traps (not_a_function), as the function check of native code does. It may not name an alias of data, nor, like a copy, a constructor or destructor table entry. A symbol globalS is read only by lettmpD, p, copy, globalS, which yields a pointer to the data or function object; S may be defined outside the module. See docs/m3.md and docs/m4.md.
Stages
A module is in one of two stages, told apart by its vocabulary:
| Stage | Means |
|---|---|
unchecked | as the frontend and the middle end write it. In filc mode, loadT and store at a p address mean "Fil-C's access check, then the access". |
checked | after pizlonate.pl, what the Fil-C backend compiles: every check is explicit, and every cycle of the CFG has a poll edge. |
In the checked stage a check yields a temporary of class a, a proven address, which only raw accesses read: raw_loadT, Off and raw_storeW, Off, V, A. The check that covers an access is its address operand's definition. A raw access its check does not cover is a bug of the pass, which the interpreter reports as the outcome uncheckedWhy.
Pure pointer copies, add/sub and integer-to-pointer conversion use flight in checked IR; ordinary p copy remains only for getters. The middle end runs before pizlonation. Its entry point leaves a directly supplied checked module unchanged, even with -O.
A check_function similarly yields class f, consumed only as the callee of the immediately following raw_call. It proves the target's identity, not a signature match: raw_call still selects fast or generic argument/result handling. A bad raw target reports uncheckednot_a_function; traps from that handling or from the callee remain traps. Direct calls keep call and their ABI thunks.
Pointer accesses carry the complete ordered list described by pointer_memory_effects/2. The list is executed, not an annotation. Each access is one instruction for liveness and layout, not an atomic transaction: aux_ensure may exit/re-enter or fail without returning. rooted_reload reloads the original p pair, not the ephemeral proof. The stored value also remains rooted through the whole instruction.
Neither proof class crosses an intervening safepoint (a call, a pollcheck, alloc, setjmp, va_arg or getter), since a free may make it stale. Each check is followed immediately by its first use. The pointer store's internal ensure-aux/reload sequence is the existing Fil-C exception, not permission to move another effect between the pair. The atomic store's helper call (atomic_write), which may exit in its ensure-aux, is the same exception; both atomic effect lists are heap-only and end every live proof.
A heap check's proof may also be read by later scalar raw accesses that it covers, while its evidence lasts (docs/m7.md): on every path from the check only evidence_preserving/1 instructions and unpolled edges come between, and neither the proof nor the checked pointer is redefined (a phi destination counts). Local and function proofs have one use.
Variable names
In the predicates below: M a module, Fn a function name, K a class, V an IR value, L a label.
Bits is the width in bits of the numeric class K (w, l, s or d).
Op takes N arguments; it fails for anything that is not an Op of the grammar.
| 493 | additive | 2 |
| 494 | alu | 2 |
| 495 | shift | 2 |
| 496 | cmp | 2 |
| 497 | neg | 1 |
| 498 | copy | 1 |
| 499 | ptoi | 1 |
| 500 | itop | 1 |
| 501 | va_args | 1 |
| 502 | va_arg | 1 |
| 503 | setjmp | 2 |
| 504 | ext | 1 |
| 505 | load | 1 |
| 506 | atomic_load | 1 |
| 507 | cas | 3 |
| 508 | raw_cas | 3 |
| 509 | alloc | 1 |
| 510 | float_convert | 1 |
| 511 | float_to_int | 1 |
| 512 | int_to_float | 1 |
| 513 | cast | 1 |
| 514 | check | 1 |
| 515 | check_ahead | 1 |
| 516 | renew | 2 |
| 517 | renew_hull | 3 |
| 518 | half_check | 2 |
| 519 | span_test | 1 |
| 520 | renew_if | 2 |
| 521 | limit | 1 |
| 522 | check_limit | 2 |
| 523 | check_local | 0 |
| 524 | check_function | 1 |
| 525 | ld | 1 |
| 526 | ld_pointer | 1 |
Op is an instruction of the IR: one of op_kind/2's, with operands from the sets below where it has them.
Effects is the closed, ordered protocol of a pointer access of kind Access: load, store, local_load, local_store, atomic_load, atomic_store or cas. For an ordinary heap load, aux_read reads the encoded lower (or none) and lower_resolve unboxes it without taking the box's address. A store ensures aux (may exit), barriers the value's lower (may call, cannot exit), reloads its destination p pair from rooted storage, then writes the ordinary lower before the primary address. No effect list may omit or reorder these obligations; the backend executes the list, it is not an annotation.
| 582 | load | aux_read, lower_resolve, address_read |
| 583 | store | aux_ensure, lower_barrier, rooted_reload, lower_write, address_write |
Proven nonescaping memory has an explicit stack aux, never a heap header or atomic box. These protocols are selected by check_local's provenance, not merely by a shorter effect list supplied by the caller. | ||
| 588 | local_load | aux_read, address_read |
| 589 | local_store | lower_write, address_write |
An atomic access delegates its whole protocol to Fil-C's helper, after the inline check: atomic_read is filc_load_ptr_atomic (the address, then the lower or the atomic box's pair, fenced); atomic_write is filc_store_ptr_atomic (its own check, ensure-aux, which may exit, the store barrier, a box allocated or reused, the pair stored atomically, then the address). Heap storage only: stack aux has no boxes. | ||
| 596 | atomic_load | atomic_read |
| 597 | atomic_store | atomic_write |
atomic_cas is filc_strong_cas_ptr_with_manual_tracking (its own check, ensure-aux, which may exit, the barrier of New, a box, then the address), named for raw_cas(p, _), which has no list of its own. | ||
| 601 | cas | atomic_cas |
a cas may be of type T, cas_bytes(+T, -Bytes) wide.
, data_align(?Align): an alloc's alignment is a power of two from 4 to 4096, a data item's from 1 to 4096. Above 16, Fil-C allocates with filc_allocate_with_alignment and pads a data object before its header (docs/abi-findings.md).
Kind is the category of Op that its consumers dispatch on, so that each can case-split on Kind in clause heads. Deterministic in mode (+, -): one fact per op, indexed on the first argument.
additive add sub: integer, or (filc) a p plus or minus an l offset alu mul div udiv rem urem and or xor: binary, integer only shift sar shr shl: the count is read at w neg copy ptoi itop each its own kind; copy may be of class p cmp ext load alloc compounds check ld the checked stage: a check and a raw load
Func is the func/5 term that defines Name in the module M, or in the symbols(Index) that module_symbols/2 made of it.
The module M, or the one module_symbols/2 indexed, has data named Name.
variadic_named(+M, +Name) is semidet.
The function named Name in M, or in the module module_symbols/2 indexed, is variadic (variadic_func/1), found without rescanning its blocks at every call to it.
M, or the module module_symbols/2 indexed, defines Name with linkage weak (or roweak), which another object's definition may replace.
M, or the module module_symbols/2 indexed, declares Name weak (linkage externweak) without defining it.
Symbols indexes the functions and data of module M by name, for func_named/3 and data_named/2: a large module (SQLite) calls thousands of functions, and a scan of its items per call would be quadratic. As memberchk/2 does, the first item of a name wins; in a valid module each name has one item (unique_names/1).
Func takes the entry argument snapshot (va_args) of a variadic function. The snapshot's metadata is retained even if its cursor is unused.
Func calls setjmp somewhere, reachable or not. Nonlocal returns restore compiler slots, not mutable local memory, so transformations must keep this boundary even in unreachable blocks: the passes leave such a function alone and the backend gives it the reference emission (docs/setjmp.md).
Module mode
Mode is filc when anything in M has class p, uses a pointer-only op, or calls a function M does not define (which only the Fil-C ABI can reach), and plain otherwise.
The mode is inferred rather than stated: M uses a feature only filc mode has, or it does not. Every rule above is such a feature, the external call as much as class p. Stating the mode would mean a module(Mode, Items) term or a Mode argument for valid_module/1, run/5, promote and the backends, and a mode clause in each IR file, for no case the inference gets wrong: a C module is filc unless it uses none of these features (no memory, no pointers, no external calls), and then validation, promotion and the interpreter treat it alike in both modes; nanofil cc picks the Fil-C backend itself.
Item has class p somewhere, or is read-only, weak or thread-local data or a weak function, which only filc mode models. The cuts commit to the first witness.
Inst produces, stores, passes or calls through a p value, or converts one (ptoi). Several clauses may hold for one Inst.
Validation
M is a well-formed module. When it is not, throws nanofil_error(Message) describing the first problem found, so callers get a diagnostic rather than a silent failure. A few terms outside the grammar (an item, instruction or jump of no known shape) make it fail instead.
Functions are checked against a context
ctx(Symbols, Fn, Ret, LabelSet, TempClasses, PredMap, Mode)
where Symbols is the module's module_symbols/2, and whose three assocs map each label to t, each temporary to its class, and each label to its sorted predecessors.
no two items define the same name. Functions, data and aliases share one namespace; an extern(weak) declaration defines nothing. The interpreter's layout, the symbol table and the assembler would otherwise each pick a different item of the name.
Stage is checked when M uses any word of the checked stage (a check, renew, span test, raw access, flight or a poll edge), else unchecked. Like the mode, the stage is read off the vocabulary, never stated.
Item, an item of M, is well formed.
An alias names a function or a data object the module defines, its target, and no other item defines its name. Its kind is the target's: a call names it only if the target is a function.
Item is one of the header's data items.
each pointer item of Items, from Off bytes into the object, starts at a multiple of 8, as the layout of its capability requires.
C is a character that stands for one byte.
Objects are Name-Size for Func's local_alloc declarations, in instruction order. Their names are a namespace of their own, never ordinary values.
Defs are Name-Class for every definition of a temporary: parameters, then each block's phis and instructions, duplicates kept.
Defs is sorted, so two classes for one temporary are adjacent.
each label's sorted predecessors.
Block's phis cover exactly its predecessors, and its instructions and jump are well formed.
Jump can branch to the label L, with or without a pollcheck.
a temporary may have a value class or a proof class. Proofs live in no memory and are not values of C.
Only a check defines a proof temporary, and nothing passes one as a call argument. Phis, parameters and call results would carry a proof across an edge or a safepoint. (A check's own class is op_result_ok/3's.)
In every reachable block, each use of a temporary is dominated by one of its definitions: a parameter, an earlier instruction or phi of the same block, or one in a block that strictly dominates it. A phi reads its value at the end of the predecessor, if that is reachable. A temporary may be defined more than once (tests/fixtures/memory.ir); one dominating definition is enough. Unreachable blocks are not checked.
N-at(L, I) for each definition of tmp(N), at index I of block L, a phi's at -1.
Pairs N-Site, sorted by N, grouped as N-Sites.
every use in the reachable blocks of Blocks (those with a dominator-tree interval) is dominated: an instruction's at its index, the jump's at the end of the block, and a phi's operand at the end of its predecessor, if that is reachable. D is dom(Fn, Sites, Intervals, Ends), Ends the number of instructions of each block. Plain recursion, not maplist/3 over closures, which Trealla copies with D at every call.
some definition of tmp(N) dominates position I of block L.
the definition Def comes before position I of block L on every path from the entry.
Fn's blocks are well formed for the module's Stage. A checked function accesses memory only by raw accesses, each covered by a check whose evidence still holds, and polls on every cycle.
Evidence across edges (docs/m7.md): one pass in block order. A block's entry evidence is the intersection, over every incoming edge (both arms of a branch counted separately), of what the edge carries: the source's exit evidence on a plain edge from a block already processed, none on a poll edge or from a block not yet processed. A block with no incoming edge starts with none. Phi destinations then end the evidence that names them.
each label's incoming edges as From-plain or From-poll, one per jump target, duplicates kept.
Within a block evidence is ev(Facts, Names, ByQ): Facts the live/6 facts, newest first; Names holds every name a fact mentions (perhaps more); ByQ each fact by its proof. A definition only scans Facts when Names has its name, which strict SSA makes rare, so a long block's validation is not quadratic in its checks.
Each check in Insts is followed by an access it covers, its first use, so no safepoint can come between them; no other instruction accesses memory unchecked. Live are the heap proofs liveQ, P, Lo, Hi, Rights, Align whose evidence still holds (docs/m7.md): a later scalar raw access may read one that covers it. An instruction that is not evidence_preserving/1 ends them all, and redefining Q or P ends that one; LiveOut are those at the block's end. Local and function proofs are used once, right away.
stage_sources(+Symbols, +Params, +Blocks, -src(Renews, Once, Ahead, Getters)): Renews maps each proof Q1 that a renew may read to check(P1, Lo1, Hi1, Align1): Q1 has one definition, a heap check or renew_if of tmp(P1), and P1 one too, counting parameters, phis and every instruction form. Once maps each name with one definition to it (param for a parameter), for renew_if's guard (round 5) and check_limit's limit. Both are empty when the function has none of these ops, or has a setjmp, whose second return the CFG does not show. With strict SSA (definitions_dominate/3), Q1's check dominates the renew, so P1 and Q1 there hold the values the check saw (docs/m7.md, round 4); a renew_if proves the same bounds as the check it replaced. Ahead holds each check_ahead's proof that ahead_justified/3 accepts, empty with a setjmp too. Getters holds the repeated getter copies (repeated_getters/4), empty with a setjmp.
repeated_getters(+Symbols, +Blocks, +Once, -Getters) is det.
Getters maps D to G for each single-definition getter copy of global(G), G defined in this module with local linkage, that another copy of G dominates (below).
repeated_getters(+Symbols, +Blocks, +Once, -Getters): Getters maps D to G for each single-definition lettmpD, p, copy, globalG that another copy of global(G) dominates: an earlier one in its block, or one in a block that strictly dominates it (dom_intervals/3). Unreachable blocks have none. G must be defined in this module with local linkage (local_global/2), so its getter is the one nanofil emits and no other module can interpose it. Such a copy is a repeated call of that getter (docs/forward.md, Getters): a call has returned before it in this activation, so it takes the fast path (or, inside an initialization on this thread, the recursive path), and reaches no safepoint, frees nothing and stores nothing.
G is a function or data item this module defines with local linkage (not exported, weak or extern): its getter is a local symbol only this module calls.
Scheduled checks (docs/schedule.md). ahead_justified(+Blocks, +Once, -Ahead): Ahead holds Q for each single-definition lettmpQ, a, check_aheadLo, Hi, _, _, _, P such that, right after its access, P's base B (a single-definition name on guard_chain/3 at an exact offset K) has need(B) >= K + Hi, with K and K + Lo inside the signed range (near_offset/1). The check's start B + K + Lo then lies at most 2^63 below the needed bytes' end B + H, so the two do not wrap past each other modulo 2^64: where the check fails at B + K + Hi, the later access ends beyond it (tests/unit.pl, schedule_validation; docs/rocq.md, "A need past 2^64").
need(B) = H at a point means: every path from it reaches a raw heap access through a pointer at an exact offset from B (well inside the signed range, near_offset/1) whose bytes reach B + H or beyond, and reaches it first: before any instruction that is not ahead_transparent/1, any poll edge, edge to the same or an earlier block, or the function's end (each of which ends the need), and before B is redefined. Computed backward in one pass over the blocks in reverse order:
- a block's exit facts are the meet over its jump's edges, both arms of a branch counted: a plain edge to a later block carries that block's entry facts, any other edge none; a base present on every edge keeps the least H, and no edge means no facts;
- an instruction that is not
ahead_transparent/1ends every fact; one that defines N ends N's fact; a raw access (not a cas) at a single-definition proof of P, at offset Off, of Size bytes, raises need(B) to at least K + Off + Size for each exact base B-i(K, K) of P; - phi destinations end their facts at the block's entry.
Any edge into a later block was walked before, so one pass suffices. In the reference program every such access has its own check, which fails if those bytes are outside the object: so where this check fails early, the reference traps later on every path (unless something else traps first).
Q-P for each single-definition heap proof Q and the pointer P it proves.
After are the facts after the first of RevInsts (the block's last instruction), AfterNext those after the instruction that follows it.
guard_chain/3's offsets are exact only modulo 2^64 (class l wraps), so a need is counted only for offsets well inside the signed range, where the integer is the true distance: an access at B + 2^64 - 8 is at B - 8, and must not count as reaching past B.
A check of [Lo, Hi) at P, where P is P1 + D0 modulo 2^64 with P1's capability, may test only Bound when a passed check of [Lo1, Hi1) at P1 proves the other end (docs/half.md). D is D0 taken signed modulo 2^64. upper: P+Lo is E = D + Lo - Lo1 >= 0 bytes above P1+Lo1, which was at or above lower, and with E =< 2^62 that sum cannot wrap, as P1+Lo1 is a user address. lower: P+Hi is F = D + Hi - Hi1 =< 0 bytes from P1+Hi1, at or below that check's upper; with F >= -2^62, P+Lo taken signed is the true address, which the signed lower test reads (and Hi - Lo =< 2^62 keeps P+Lo above -2^63).
Inst may come between a check_ahead and the access whose need it checks early (docs/schedule.md): it is evidence_preserving/1, so it reaches no safepoint, calls nothing and cannot free, and it is not a division, whose fault would end the program otherwise than a Fil-C trap. Calls, allocation, getters, pointer stores, atomics, setjmp and va_arg are not, nor are poll edges, which may run signal handlers.
hull_renewable(+Sources, +Once, +P, +Lo, +Hi, +Align, +QL, +QH): a renew_hull of [Lo, Hi) at P may read QL and QH (docs/forward.md, multi-source renewal). Each is a single-definition heap proof in the renew-source table (a check that passed, at a point that dominates this one by strict SSA, in a function without setjmp) of a pointer at an exact distance from P through one base, so of P's object: QL's of [LoL, HiL) at PL, P = PL + DL, and QH's of [LoH, HiH) at PH, P = PH + DH, all modulo 2^64. With E = Lo + DL - LoL and F = HiH - Hi - DH both in [0, 2^62] and Hi - Lo =< 2^62:
- P+Lo is E bytes above PL+LoL, which was at or above lower, and as PL+LoL is a user address (below 2^56) the sum does not wrap;
- P+Hi is that plus Hi - Lo, and also F bytes below PH+HiH, which was at or below upper; both readings are below 2^63 + 2^62 + 2^56 and above -2^62 and equal modulo 2^64, so they are the same integer.
So [P+Lo, P+Hi) lies in the object as both checks saw it. Its bounds change only when it is freed, which the renew's flag test catches; read-only is the object's, which the flag test reads too. Alignment comes from either source, as renew's: P+Lo is (Lo + D - Lo1) bytes from a check's Al1-aligned start.
P's address is P1's plus D modulo 2^64, with P1's capability, at any point both dominate: both reach one single-definition base B through guard_chain/3 at exact offsets K and K1, and D = K - K1 (the argument of same_pointer/3, which is the case D = 0 modulo 2^64).
Once maps each temporary with exactly one definition (temp_defs/3's forms) to it: param, its phi, or its instruction.
Range guards (docs/m7.md, round 5, slice A). Chain is P-i(0, 0) followed by B-i(Lo, Hi) for each base B of P: P has B's capability and an address congruent modulo 2^64 to B's plus some X with Lo =< X =< Hi, through single-definition flights add, sub and copy whose lower donor is their address operand. Once maps each single-definition name to its definition (single_definitions/3).
offset_interval(+Once, +V, +K, +Depth, -Lo, -Hi): every value V of class K can hold, taken signed in K's width, lies in [Lo, Hi]; for l, the value is congruent modulo 2^64 to one in [Lo, Hi], which is all an address needs. A name needs one definition (Once) of the forms below, each sound for any operand values within their intervals; a w result must lie in [-2^31, 2^31), so no w arithmetic wraps.
as above, with each name's interval (or none) memoised, so an offset whose terms share names (x = x + x, repeated) is walked once per name.
At any point both P and P1 dominate, they hold the same address and capability: both reach one single-definition base B through guard_chain/3 at point offsets equal modulo 2^64 (P == P1 included). After B's last execution before that point, each definition on either chain ran again, since each dominates it and B dominates each, so both were computed from B's current value (docs/m7.md, round 4 addendum). Once maps each single-definition name to its definition.
G is a single-definition span test of a single-definition P0 whose span contains P's [Lo, Hi) for every offset P can have from P0.
U is a single-definition limit(Size) of a single-definition P0 whose lower P has (lower_chain/3), for exactly P's accesses [0, Size) (docs/bounds.md, hoisted checks).
P has B's lower: P is B, or a single-definition flight whose lower donor has B's lower, whatever its address. At any point that P's definitions dominate, P's lower is B's current one, by round 4's dominance argument (docs/m7.md), since every name on the way has one definition. Once maps each single-definition name to its definition.
A limit's value is an encoding only check_limit reads (docs/bounds.md): no phi, jump or other instruction reads a name a limit defines, and a check_limit reads one only as its second argument. Throws otherwise.
Inst, a raw access of type or width X, may read a live proof that is not its own check's: a scalar load or store, or a pointer load with the heap load effects, which read aux and box words only (docs/forward.md). A pointer store's ensure-aux may exit, and a cas is atomic; both keep their own check.
hull_covered(+Access, +Q, +P, +Lo, +Align, +Live, +Once): Access at proof Q of P, whose live fact's lower end is Lo at alignment Align, lies within the hull of the live facts of P's object (docs/forward.md). Each live fact live(Q1, P1, Lo1, Hi1, R1, _) with P1 at an exact distance D from P through one single-definition base (pointer_distance/4) shows that P+[Lo1+D, Hi1+D) is inside the object; an object is one interval, so every byte between the least such lower end and the greatest upper end is too. All the facts are live, so the object has not been freed since any of their checks; a write needs one of them with write rights (read-only is the object's). Alignment is Q's own, as covered_access/6 has it. Every offset and span end counts only well inside the signed range (near_offset/1): then each passed fact lies in an object far smaller than 2^62, and the integer hull is the true address interval.
Live are the proofs of Live0 whose evidence still holds after Inst (checked_insts/5).
Inst reaches no safepoint and cannot free an object or change its bounds or rights: pure arithmetic, comparison and conversion, pure pointer construction, a heap check, a scalar raw access (object headers lie outside every object's bounds) and a raw pointer load (aux and box reads, no helper). Calls, alloc, getters, setjmp, va_arg, pointer stores and the rest are not.
Inst is a pure pointer operation (add, sub, itop, or a copy of a temporary or constant at class p) whose address and lower sources must be made explicit as flight before validation or emission of checked IR. A copy of a symbol is not one: it calls the getter, an effect.
Inst is a raw load of type X or store of width X at tmp(Q)+Off, needing Rights.
| 2262 | let_, _, raw_loadT, Off, tmpQ | Q | T | Off | read |
| 2263 | raw_storeW, Off, _, tmpQ | Q | W | Off | write |
| 2264 | let_, _, raw_load_pointerOff, _, tmpQ | Q | p | Off | read |
| 2265 | raw_store_pointerOff, _, tmpQ, _ | Q | p | Off | write |
| 2266 | let_, _, raw_casT, Off, tmpQ_ | Q | casT | Off | write |
Access, right after the heap check, renew or renew_if that defines Q over [Lo, Hi) with Rights and Align, uses its proof: a heap raw access it covers, or a touch of Q, which accesses nothing (docs/vector-access.md).
Access is a raw access at tmp(Q) within [Q+Lo, Q+Hi), as aligned as it must be, and Rights allow it (write allows reading too).
Every cycle of the control-flow graph of Blocks, unreachable blocks included, has a poll edge: without them the graph is acyclic. A call does not count, since the callee need not poll. Depth-first search, with each label gray while on the path and done after.
no cycle of Graph is reachable from Ls; a gray successor closes one. Plain recursion, since Trealla copies a closure's arguments, Graph included, at every call.
pairs_keys_values/3, without depending on library(pairs).
Inst is well formed and reads each operand at a class its definition allows. In filc mode a symbol is an operand only of copy, which yields its pointer; the cut commits to that case before the general clause for ins/4.
Inputs are exactly class w, not an l read as w (docs/asm-fixed.md).
global(S) does not name a constructor or destructor table entry, which is not an object (the header's Data): nothing may take its address or call it.
the call site reads the result the way the callee returns it.
a call site may read at class K the result of Callee, which returns Ret.
as to_result_ok/4, for a result of class Ret. A long may be read as a word, nothing else changes class.
Jump names existing labels and returns what the function's return class requires.
the jump target T, a label or poll(Label), names a block.
V may be read at class K. Arguments are in the order maplist needs; valid_use_/3 indexes on the value.
A p temporary is used only at p and vice versa; ptoi and itop are the conversions. An integer constant at p is a pointer with no capability. Only a check makes a proof (class a or f): no constant is one.
the symbol global(G) may be read at class K in a module of Mode: in plain mode as an address of data, in filc mode never (copy, which yields its pointer, is checked apart).
Operand and result classes
Op may produce a result of class K in a module of Mode. With Op partial (cmp(_, _), ext(_), load(_)) it enumerates the operands.
as op_result_ok/3, for Op of Kind.
Classes is the list of classes at which the arguments of Op are read when its result has class K in a module of Mode. Fails for an Op outside the grammar.
as op_arg_classes/4, for Op of Kind.
throw nanofil_error with the message Fmt/Args, attributed to the function Fn.
Erase explanatory metadata at execution/code-generation boundaries. Never use erasure to relax checked-IR validation's adjacency rule.
The fixed-register instructions asm_fixed may name (docs/asm-fixed.md), with the registers each reads and writes (a, b, c, d: rax to rdx, of which only the low 32 bits are read; every write is 32 bits and zero-extends). mfence is the fence instruction.
| 2847 | cpuid | a, c | a, b, c, d |
| 2848 | xgetbv | c | a, d |
| 2849 | rdtsc | [] | a, d |
| 2850 | rdtscp | [] | a, c, d |
| 2851 | lfence | [] | [] |
| 2852 | sfence | [] | [] |
| 2853 | pause | [] | [] |
Sub lists distinct elements of Set, in Set's order.