This pass inserts explicit reference counting instructions. It assumes the input does not yet
contain inc, dec instructions or any lower level operations related to them. Like the other RC
related passes, it is based on the "Immutable Beans Counting" paper with a few extensions.
The pass traverses the program and performs a liveness analysis, inserting decrements at the first position where values need not be alive anymore. Furthermore, it inserts increments whenever values are used in an "owned" fashion (e.g. passed as an owned parameter) and continue being used later on. Finally, it has support for borrowed parameters, i.e. parameters where we know ahead of time that we are not allowed to free them. For these kinds of parameters it avoids performing the majority of reference counting. In addition the pass has supported for "derived borrows", i.e. it treats values that are projected from borrowed values as borrowed themselves. We can do this as we know the borrowed value is not going to be mutated and will thus keep its projectee alive.
The following section contains the derived value analysis. It figures out a dependency tree of
values that were derived from other values through projections or Array accesses. This information
is later used in the derived borrow analysis to reduce reference counting pressure.
Equations
- Lean.Compiler.LCNF.runExplicitRc decls = Array.mapM (fun (x : Lean.Compiler.LCNF.Decl Lean.Compiler.LCNF.Purity.impure) => Lean.Compiler.LCNF.Decl.explicitRc✝ x) decls