pizlonate.pl
Pizlonation: from the unchecked IR to the checked IR (ir.pl), the form the Fil-C backend compiles, named after Fil-C's LLVM pass.
The checks Fil-C requires are implicit in the unchecked stage, where a load or store at a p address means "check, then access". This pass states them: each such access becomes a check, whose class a result is the proven address, and the raw access that reads it.
| Unchecked | Checked |
|---|---|
lettmpD, K, loadT, A | lettmpQ, a, check0, S, read, Al, A, then lettmpD, K, raw_loadT, 0, tmpQ |
storeW, V, A | lettmpQ, a, check0, S, write, Al, A, then raw_storeW, 0, V, tmpQ |
accessK, A, S, Al | lettmpQ, a, check0, S, K, Al, A, then touchtmpQ |
| pointer load/store | the same check, then raw_load_pointer or raw_store_pointer with its explicit pointer_memory_effects/2 sequence |
atomic_loadp, atomic_storep, V, A | the same check, then the raw pointer access with the atomic effect list ([atomic_read], [atomic_write]) |
letD, K, casT, E, N, A | a write check of T's width at that alignment, then letD, K, raw_casT, 0, tmpQ, E, N |
callRes, tmpP, Args | lettmpQ, f, check_function, tmpP, then raw_callRes, tmpQ, Args |
letD, p, add, P, X (also sub) | flightD, add, addressP, X, lowerP |
letD, p, copy, P (not a symbol) | flightD, copy, addressP, lowerP |
letD, p, itop, X | flightD, copy, X, none |
S and Al are the access's size and alignment (ir:access_size_align/3), and Q is a fresh name.
Every edge that does not go forward in block order, to a block at or before its source, gets a pollcheck, pollL, so every cycle polls. In a plain module, whose addresses are not Fil-C pointers, only the polls are added.
pizlonate itself stays naive: one check right before each access (a vector's access/4 becomes a full-width check and a touch before its chunks), and every backward edge polls. Under --checks (renew is the -O default), check_reuse.pl's reuse, renew and guard run after it (docs/m7.md); each result must pass its *_refines identity check, and the validator (ir.pl, checked_insts/5) then checks the evidence independently.
The jmp_buf store of setjmp and the cursor of va_arg stay opaque: the backend checks them inside the instruction, as the runtime helpers they call do.
M is the unchecked module M0 with every check explicit and a poll on every edge to a block at or before its source in block order. In a plain module, whose addresses are not Fil-C pointers, only the polls are added.
Each item has one pizlonation; committing to it frees the choicepoints that would otherwise keep every function's intermediate terms alive.
Each proof temp and polled label is generated once, so the bases pizlonate(Q) and poll(L) are distinct and Ids need not grow.
Names is the assoc of every temp name the function defines, so a fresh name avoids them. A valid function reads only temps it defines.
Blocks are Blocks0, the first at index I in block order, checked: each block's instructions by checked_insts/11 and its jump by polled_jump/4. P is p(Mode, Names, Index), Index each label's position in block order, and N counts fresh names. Map is the old-to-new site map for provenance's remap_sites/3, and Generated the proof(Q, Site) and poll(L) facts the context gains. Plain recursion: Trealla copies a closure's arguments at every call.
Insts are Insts0 of block L with Fil-C's checks explicit (filc mode only): each access becomes its check and raw access (checked_access/4), each pure pointer operation a flight (flight_inst/2), and everything else stays. Fresh proof names chkN count from N0 to N, avoiding Names. Old and New number the instructions before and after, for the site Map; Generated records each proof made.
Inst is the flight of the pure pointer operation Inst0: add or sub of an offset, a copy of a temporary or constant, or itop, which has no lower. The address calculation and lower are chosen independently; no new temporary or safepoint separates them. A symbol copy still calls its getter; it is not a pure projection, and stays.
| 168 | letD, p, add, P, X | flightD, add, addressP, X, lowerP |
| 169 | letD, p, sub, P, X | flightD, sub, addressP, X, lowerP |
| 170 | letD, p, copy, tmpN | flightD, copy, addresstmpN, lowertmpN |
| 171 | letD, p, copy, constN | flightD, copy, addressconstN, lowerconstN |
| 172 | letD, p, itop, X | flightD, copy, X, none |
Insts less Insts1 are Access's check, defining tmp(Q), and its raw access: the table in this module's header, one clause per row. Fails for an instruction that is not an access.
An atomic pointer access has the same inline check; Fil-C's helper does the rest (ir.pl, pointer_memory_effects/2).
A cas, integer or pointer, checks write rights at its width's alignment (ir.pl); for p Fil-C's helper does the rest.
A vector's full-width check (docs/vector-access.md): the check, then touch, which uses its proof and accesses nothing.
Q is chkI for the least I >= N0 not among Names, and N is I + 1.
Jump is Jump0, ending the block at index From, with poll(L) for each target L at or before it in block order (Index), so every cycle of the CFG polls.