Module BTL_RegisterRenaming

module BTL_RegisterRenaming: sig .. end

BTL register renaming oracle, to be used with if-lifting


module IM: Stdlib.Map.Make(Stdlib.Int)
module RM: Stdlib.Map.Make(Camlcoq.P)
val ssa_renaming_map : BinNums.positive ->
BTL.iblock_info Maps.PTree.t ->
(RM.key * RM.key)
IM.t
val apply_renaming_map : BinNums.positive ->
BTL.iblock_info Maps.PTree.tree ->
(RM.key * RM.key)
IM.t -> BTL.iblock_info Maps.PTree.tree
val restore_blocks : BinNums.positive ->
BTL.iblock_info Maps.PTree.tree ->
(RM.key * RM.key)
IM.t -> BTL.iblock_info Maps.PTree.tree
val get_freg : BinNums.positive ->
BTL.iblock_info Maps.PTree.t ->
BTL.iblock_info Maps.PTree.t *
(RM.key * RM.key)
IM.t