rocq/backend/Escape.v
# Escape classification of allocs
As escape.pl, on terms: which temporaries of a function hold the address of an alloc at a known offset (address_temps), and, for each alloc, whether its address is only used for loads and stores at such offsets (alloc_classes). Promote.v turns the slots of such an alloc into temporaries.
The analysis rests on one fact: a local alloc can only be reached through its own address, so no other pointer or integer can name it. Offsets are exact integers.
escape.pl also says why an alloc escapes; no pass reads that, so it is left out.
String equality, written as Prolog's ==.
Widths
As ir.pl's width_bytes(W, Bytes): the bytes of the width w.
As slot_load_width(T, W): the width a load of the type t reads. None for a type whose load is no slot access, as x.
Instructions
The destination, class, op and arguments when the term i is let(D, K, Op, Args).
Whether the op o is an alloc(Align).
The integer n when the value v is const(N).
As offset_of(Inst, X, N): the instruction i gives its destination the value of the temporary x plus the constant n.
Address temporaries
For each temporary that holds an address of an alloc: the alloc's temporary, the root, and the offset from it.
The root and the offset when the value v is an address temporary.
The edges from the temporary x: the position, the destination and the constant of each instruction that adds a constant to x.
Of the pairs ps, sorted by key, the first with each key.
As layers_addrs/4: the addresses addrs and those derived from the temporaries of layer, layer by layer. A temporary that two instructions of a layer define takes the first one's source. Every layer but the last adds a temporary that an instruction defines, so a fuel of their number, and one, is enough.
As address_temps(F, Addrs): the address temporaries of the blocks bs. The temporary of each alloc is its own root, at offset 0; a temporary defined as an address plus or minus a constant, or as its copy, is an address too. None when two allocs define one temporary, where list_to_assoc/2 throws.
Classes
An access acc(Off, W): the bytes of the width w at the offset off of an alloc.
The standard order of two accesses, as terms acc(Off, W).
Whether a and b are the same access.
The accesses the map m has for the alloc a, none if it has no entry.
What an instruction does to an alloc, the root: an access, or, with None, a use that lets its address escape.
An escape for each address among the values vs.
Whether the op o is of a kind whose address arguments escape (kind_event/4): the arithmetic, a copy, the conversions between pointers and integers, va_args and va_arg, setjmp, a comparison, the extension of a narrow integer and an alloc.
As inst_event(Inst, Addrs, Event): the events of the instruction i.
- A load from an address is an access of the type's width, or an escape for a type with none.
- A store to an address is an access; a store of an address lets it escape.
- An address that an atomic access, a compare-and-swap, an
access, anasm_fixedor a call reads escapes. - So does an address argument of an op of
escaping_op, but in an instruction that derives an address from an address (offset_of). - A
va_argof an address is, besides, an access of a pointer.
As jump_value(Jump, V): the values the jump j reads.
Every definition of a temporary in a function: by a param, a phi, a let, a call or an asm_fixed. A temporary defined twice is there twice.
As alloc_classes(F, Addrs, DefCounts, Classes): for each let(tmp(A), _, alloc(_), [Size]) of the blocks bs, in their order, the temporary a, the size and the class: None when the address escapes, or else the ordset of the alloc's accesses, local(Size, Accs). Besides the instructions' events, an address escapes as a phi argument, as a jump's value, and when its temporary has two definitions.