rocq/backend/Fuse.v
Fusion, the first step of the Fil-C backend (filc_amd64.pl's fused_blocks/5): each check of the checked IR and the raw access after it, which reads the check's proof, become one instruction at one index, the access now at the checked pointer itself. A proof is then a register value and needs no frame slot. A later access under the same proof is reused, with no check; a function check fuses with its raw call.
The first version takes the checks the compiler emits without −O: check (a check_ahead is the check of its whole range), check_local and check_function. A function with a renewed, half or limit check, which only the optimizer's passes make, is refused, as is one the Prolog compiler throws on: an access without its check, or pointer arithmetic that is not a flight.
Before fusion
As without_locs/2 and ahead_as_check/2: the instructions is without their source positions, each check_ahead now the check of its whole range, whose early bytes are tested with the access's own.
A block before fusion.
Proofs that hold in every block
As temp_defs/3, its names: every definition of a temporary, the parameters ps, then each block's phis and instructions.
The names ns counted: each maps to whether it occurs more than once.
Whether the name n is defined more than once.
As single_proofs/3: the proof q mapped to its checked pointer p for each heap check let(tmp(Q), a, check(...), [P]) where q has one definition in the function and p, if a temporary, has no more than one. Only these may be reused in another block: reloading p there gives the value that was checked.
A block's proofs
As proofs_empty/1.
As proofs_add/3: pr with the proof q of the pointer p.
As proofs_kill/3: pr once d is defined again: without d's own pair and without each pair whose pointer is tmp(D). Emission reloads the pointer from its slot, so its old proofs are of another value.
Accesses
Which protocols a fused pointer access may declare: a heap object's or a named local's.
| | | Heap | ||
| | | Local |
As proven_access/4 (heap) and proven_local_access/4 (local): the raw access i, which reads the proof q, as the access at the place p. A pointer access must declare a protocol of its storage: the heap's or the atomic helpers', or the local's. A touch uses the proof and accesses nothing, and is the heap's only.
As access_pointer/3, its offset: the access a is at its place plus this.
The proof and the offset of an access that may be reused: a non-pointer raw load or store, or a pointer load by the heap's load protocol.
As unchecked_access/1 and implicit_flight/1, for the checked IR: an instruction that must not reach emission by itself: a raw access or call not fused with its check, a call of a pointer, or pointer arithmetic outside a flight.
Whether access_check//2 can emit the check c: of the bytes from the pointer up to a positive size below 2^31, aligned to 1, 2, 4 or 8.
Fusing
As fused_inst/5: the instruction i fused with the one after it in rest, if it is a check, and whether that one was taken. Nothing if i is a check without its access, a check the first version does not emit, or an instruction that is not_emitted.
One step of fused_insts/5: the instruction i under the block's proofs pr and the function's single proofs. An access whose proof is among them is reused, at the proof's pointer, if its offset fits 32 bits; anything else is fused_inst's.
As fused_insts/5: the instructions is fused, in front of the reversed acc. Each instruction's definition first forgets the proofs it invalidates; a check then adds its own; and what the fused instruction defines, a load's destination perhaps, forgets again.
A block after fusion: its instructions are finsts.
As fused_blocks/5: the blocks bs of a function with the parameters ps, fused. fused_blocks/5 also throws unless every cycle polls, which is the validator's to check here.