rocq/backend/Copy.v
# Copy propagation
As copy.pl's copy_module/2, on terms: in each function in strict SSA form, a copy let(tmp(D), K, copy, [Src]) of a value of the same class goes, and every use of D reads what Src stands for; then each phi whose arguments, apart from itself, are one value goes the same way, which can make another phi trivial. A function that is not in strict SSA form, or that calls setjmp, is left as it is.
What copy.pl does besides is left out, as in Pizlonate.v: the context records and their sites. copy_module gives None where copy_module/2 fails or throws: an item, an instruction, a value or a jump of no known shape, or a jump to a label no block has. The gate (tests/promote.sh) holds the result to the term nanofilpromote − terms prints.
String equality, written as Prolog's ==.
Classes
The temporaries the instruction i defines, each with the class of its definition; an output of an asm_fixed is a w.
As temp_classes(Params, Blocks, Classes): the class of each temporary's definition.
As copy_value(Src, K, Classes, V): what a copy at the class k of the value src can be replaced by: a temporary of that class, or a constant at w or l, reduced to the class's width.
Chains
As copy_chain/6: following the copies, and the values already in reps, from the value v ends at a value that is not copied; the path has the temporaries on the way that reps lacks. A chain has at most as many links as there are copies, the fuel.
As foldl(copy_reps(Copies), Pairs, Empty, Reps): the value that replaces each temporary of pairs, the end of its chain.
Substitution
As value_reps(V0, Reps, V): what replaces the value v, or v itself.
As inst_reps(Inst0, Reps, Inst).
As jump_reps(Jump0, Reps, Jump).
Whether the term t defines, as a phi or as a copy, a temporary that reps replaces.
As reps_block(Reps, Block0, Block, _): the block b without the phis and the copies whose temporary reps replaces, and with every use of such a temporary replaced by its value.
Trivial phis
As phi_worklist_reps/5: the value of each trivial phi, found by a worklist over the phi temporaries pending, an ordset. phis has the operand values of each phi not yet simplified, and users the ordset of the phis that read each temporary. A phi is trivial when its operands other than itself are one value; the phis that read it then read that value, and are looked at again. The result is in the order the phis were simplified, the last first; the caller puts it in the order of the temporaries, an assoc's. Each step takes a temporary off pending or simplifies a phi, and only simplifying adds any, at most all the phis: the fuel.
As trivial_phis/6: the blocks bs without their trivial phis. Only a phi of a reachable block whose every argument a copy could stand for (copy_value) is looked at.
Functions and modules
As copy_context/4, without the records: the blocks bs of a function with the given params, its copies and trivial phis gone.
As copy_module/2, without the context items.
A copy goes, and its use reads the source.