rocq/backend/FrameSlots.v

Stack slots for temporaries (frame_slots.pl's temp_slots/7, with shared pools): each temporary gets a slot of its pool, and two whose live intervals are strictly disjoint may share one.

A temporary's interval is closed. It covers every write, even of a dead result, every use by an instruction, and every block boundary where the temporary is live in or out. One instruction is one point, with all its helper calls, so a result never overwrites its operands. The slots are found first-fit over the intervals in the standard order of range(Start, End, Pool, N), which makes the layout the Prolog compiler's, slot for slot.

From Stdlib Require Import String ZArith List Bool

From Nanofil Require Import Term Syntax Validate Maps Cfg

From Backend Require Import Order Plan Fuse Liveness

Import ListNotations

Open Scope Z_scope

Touches

A group of temporaries touched at one point: an instruction's uses or definitions, a block's phis, or the temporaries live into or out of a block.

24Inductive touch: Type ≔

\|	TouchPlain	ns : listname
\|	TouchLiveIn	ns : names	`live(in, Ns)`
\|	TouchLiveOut	ns : names	`live(out, Ns)`

As inst_ranges/5: the touches of the instructions is from the point p, each instruction's uses and definitions at its own point, in front of acc, the last first. With them, the point after the last instruction.

33Definition inst_touchesis : listfinst p : Z acc : listtouch × Z : Z × listtouch × Z ≔

fold_left

λ st i ⇒

let q ≔ fstst in

q + 1, TouchPlainmapfst finst_defsi, q :: TouchPlainfinst_usesi, q :: sndst

p, acc

As block_ranges/8: the touches of the blocks bs from the point p, in front of acc, the last first, and the point after the last block. A block's live-in set and phis are at its own point, the jump's uses and the live-out set at its exit. The live sets keep only what can move a bound: the live-in set less prev_out, the live-out set of the block before, and the live-out set less the next block's live-in set.

48Fixpoint block_touchesbs : listfblock live_in live_outs : nmapnames prev_out : names p : Z acc : listtouch × Z : Z × listtouch × Z ≔

match bs with

[ ]

⇒

p, acc

b :: bs′

⇒

let new_in ≔ nsubtractnames_atlive_in fb_labelb prev_out in

let phi_names ≔

map

λ ph ⇒

match ph with

Phid _ _

⇒

fb_phisb

let r ≔ inst_touchesfb_instsb p + 1 TouchPlainphi_names, p :: TouchLiveInnew_in, p :: acc in

let exit ≔ fstr in

let out ≔ names_atlive_outs fb_labelb in

let next_in ≔

match bs′ with

next :: _

⇒

names_atlive_in fb_labelnext

[ ]

⇒

[ ]

block_touchesbs′ live_in live_outs out exit + 1 TouchLiveOutnsubtractout next_in, exit :: TouchPlainjump_usesfb_jumpb, exit :: sndr

As first_touches/3: each temporary mapped to the point of its first touch in ts. The live-in groups are left out if skip_in, else the live-out ones: a live-out set never moves a first touch, nor a live-in set a last one.

72Definition first_touchesskip_in : bool ts : listtouch × Z : nmapZ ≔

fold_left

λ m t ⇒

let touched ≔

λ ns ⇒

fold_left

λ m n ⇒

nm_memn m

→

else

nm_addn sndt m

match fstt with

TouchPlainns

⇒

touchedns

TouchLiveInns

⇒

skip_in

→

else

touchedns

TouchLiveOutns

⇒

skip_in

→

touchedns

else

nm_empty

Ranges

As range(Start, End, Pool, N): the temporary n, of the pool, is live from the point start to the point stop, both included.

88Record range: Type ≔ mkRange

rg_start	: Z
rg_stop	: Z
rg_pool	: pool
rg_name	: name

As class_pool/3 with shared pools: the pool a temporary of the class k is kept in. A proof has none.

97Definition class_poolk : class : optionpool ≔

match k with

⇒

SomePoolPointer

W | L | Single | Double

⇒

SomePoolScalar

Extended

⇒

SomePoolWide

A | F

⇒

None

The place of a pool's atom in the standard order: pointer, scalar, wide.

107Definition pool_rankp : pool : Z ≔

match p with

PoolPointer

⇒

PoolScalar

⇒

PoolWide

⇒

The standard order of two range(Start, End, Pool, N) terms.

111Definition range_comparer r′ : range : Datatypes.comparison ≔

match Z.comparerg_startr rg_startr′ with

Datatypes.Eq

⇒

match Z.comparerg_stopr rg_stopr′ with

Datatypes.Eq

⇒

match Z.comparepool_rankrg_poolr pool_rankrg_poolr′ with

Datatypes.Eq

⇒

term_comparerg_namer rg_namer′

⇒

The name of a variadic function's hidden parameter, the promoted argument packet: hidden(va_snapshot).

125Definition va_snapshot: name ≔

TApp"hidden" TAtom"va_snapshot"

As temp_ranges/7: the live range of each of temps, the temporaries of a function with the parameters ps and the blocks bs, in the standard order. The parameters are touched at point 0 and the blocks start at 1. The hidden va_snapshot parameter is read by every va_args, so it is kept to the end.

132Definition temp_rangesps : listclass × name bs : listfblock temps : listname × class : optionlistrange ≔

let* live ≔ temp_livenessbs in

let r ≔ block_touchesbs fstlive sndlive [ ] 1 TouchPlainmapsnd ps, 0 in

let backwards ≔

existsbλp ⇒ class_eqbfstp P && name_eqbsndp va_snapshot ps

→

TouchPlainva_snapshot, fstr :: sndr

else

sndr

let lo ≔ first_touchesfalse rev'backwards in

let hi ≔ first_touchestrue backwards in

let* ranges ≔

all_some

λ t ⇒

let* start ≔ nm_findfstt lo in

let* stop ≔ nm_findfstt hi in

let* pool ≔ class_poolsndt in

SomemkRangestart stop pool fstt

temps

Somesortrange_compare ranges

Slots

As reuse_slot/7: the slot for a range from s to e among slots, each a slot's index and the end of the last range in it, of which there are n0. It is the first whose last range ends before s, or a new one. The result is the slots now, their number, and the index taken.

155Fixpoint reuse_slotslots : listZ × Z s e n₀ : Z : listZ × Z × Z × Z ≔

match slots with

[ ]

⇒

n₀, e, n₀ + 1, n₀

i₀, e₀ :: slots′

⇒

e₀ <? s

→

i₀, e :: slots′, n₀, i₀

else

match reuse_slotslots′ s e n₀ with

tail, n, i

⇒

i₀, e₀ :: tail, n, i

The slots of a function's temporaries: the slot of each, by name, in the order of the names, and the number of slots of each pool.

168Record slots: Type ≔ mkSlots

sl_aliases	: listname × pool × Z
sl_scalars	: Z
sl_pointers	: Z
sl_wides	: Z

A pool while its ranges are allocated: its slots and their number.

177Definition pool_state: Type ≔

listZ × Z × Z%type

As allocate/6 and wide_slot/3: the ranges rs, in order, each given a slot of its pool.

181Definition allocaters : listrange : slots ≔

let step ≔

λ st : pool_state × pool_state × pool_state × listname × pool × Z r : range ⇒

match st with

sc, pt, wd, acc

⇒

let take ≔ λps : pool_state ⇒ reuse_slotfstps rg_startr rg_stopr sndps in

match rg_poolr with

PoolScalar

⇒

match takesc with

ss, n, i

⇒

ss, n, pt, wd, rg_namer, PoolScalar, i :: acc

PoolPointer

⇒

match takept with

ss, n, i

⇒

sc, ss, n, wd, rg_namer, PoolPointer, i :: acc

PoolWide

⇒

match takewd with

ss, n, i

⇒

sc, pt, ss, n, rg_namer, PoolWide, i :: acc

match fold_leftstep rs [ ], 0, [ ], 0, [ ], 0, [ ] with

sc, pt, wd, acc

⇒

mkSlotssortλa b ⇒ term_comparefsta fstb acc sndsc sndpt sndwd

As temp_slots/7: the slots of temps, the temporaries of a function with the parameters ps and the fused blocks bs.

206Definition temp_slotsps : listclass × name bs : listfblock temps : listname × class : optionslots ≔

let* rs ≔ temp_rangesps bs temps in

Someallocaters