Coalesce Reference Counting Operations

This pass coalesces multiple inc/dec operations on the same variable within a basic block. Within a basic block, it is always safe to:

• Move all increments on a variable to the first inc location (summing the counts). Because if there are later incs no intermediate operation can observe RC=1 (as the value must stay alive until the later inc) and thus doing all relevant inc in the beginning doesn't change semantics.
• Move all decrements on a variable to the last dec location (summing the counts). Because the value is guaranteed to stay alive until at least the last dec anyway so a similar argument to inc holds.

Crucially this pass must be placed after expandResetReuse as that one relies on incs still being present in their original location for optimization purposes.

def Lean.Compiler.LCNF.coalesceRC : Pass

Equations

• Lean.Compiler.LCNF.coalesceRC = Lean.Compiler.LCNF.Pass.mkPerDeclaration `coalesceRc Lean.Compiler.LCNF.Phase.impure Lean.Compiler.LCNF.Decl.coalesceRC✝