Module BTLcommonaux

module BTLcommonaux: sig .. end

Shadowfields related functions

val undef_node : int

val mk_iinfo_shadow : int -> bool option -> BTLtypes.inst_info_shadow

val new_iinfo : BTL.inst_info -> int -> bool option -> BTL.inst_info

val def_iinfo_shadow : unit -> BTLtypes.inst_info_shadow

val def_iinfo : unit -> BTL.inst_info

val mk_binfo : int ->
       Registers.Regset.t ->
       Registers.Regset.t ->
       Camlcoq.P.t list -> Camlcoq.P.t list -> BTLtypes.block_info

val def_binfo : unit -> BTLtypes.block_info

val mk_ibinfo : BTL.iblock -> BTL.block_info -> BTL.iblock_info

val mk_finfo : RTLtyping.regenv -> bool -> BTLtypes.function_info

val mk_function : BTL.function_info ->
       BTL_Invariants.gluemap ->
       AST.signature ->
       Registers.reg list ->
       BinNums.coq_Z -> BTL.code -> RTL.node -> BTL.coq_function

Auxiliary functions on BTL

val pget : BinNums.positive -> 'a Maps.PTree.tree -> 'a

val reset_visited_ibf : BTL.iblock_info Maps.PTree.t -> unit

val apply_over_function : 'a Maps.PTree.t -> (BinNums.positive -> 'a -> unit) -> unit

val tf_ibf_ib : ('a -> BTL.iblock -> 'b) -> 'a -> BTL.iblock_info -> 'b

val reset_visited_ib_rec : 'a -> BTL.iblock -> unit

val get_visited : BTL.iblock -> bool

val jump_visit : BTL.iblock -> bool

val get_inumb : bool -> BTL.iblock -> int

val get_inumb_succ : BTL.iblock_info Maps.PTree.tree -> bool -> BinNums.positive -> int

val successors_instr_btl : BTL.iblock -> BTL.exit list

val successors_block : BTL.iblock_info -> BTL.exit list

val change_final_successor_btl : BTL.exit -> BTL.exit -> BTL.iblock -> BTL.iblock

val get_regindent : ('a, 'b) Datatypes.sum -> 'a list

val get_regs_ib : BTL.iblock -> Registers.reg list

val find_last_reg_btl : ('a * BTL.iblock_info) list -> unit

val plist2IS : Camlcoq.P.t list -> BTLtypes.OrdIS.t

val flatten_iblock_aux : BTL.iblock -> (BTL.iblock -> BTL.iblock) -> BTL.iblock

val flatten_iblock : BTL.iblock -> BTL.iblock

Invariants map related functions

val mk_ir : bool -> Registers.reg -> BTL_Invariants.ireg

val empty_csasv : unit -> BTL_Invariants.csasv

val get_inv_in_gm_or_def : BinNums.positive ->
       BTL_Invariants.invariants Maps.PTree.tree -> BTL_Invariants.invariants

val add_outputs_in_gm : BinNums.positive ->
       BTL_Invariants.invariants Maps.PTree.tree ->
       Registers.Regset.t ->
       BTLtypes.inv_t -> BTL_Invariants.invariants Maps.PTree.tree

val add_aseq_in_gm : BinNums.positive ->
       BTL_Invariants.invariants Maps.PTree.tree ->
       Registers.reg ->
       BTL_Invariants.ival ->
       BTLtypes.inv_t -> BTL_Invariants.invariants Maps.PTree.tree

val build_liveness_invariants : (BinNums.positive * BTL.iblock_info) list ->
       BTL_Invariants.invariants Maps.PTree.tree ->
       BTL_Invariants.invariants Maps.PTree.tree

val instr_all_deps : BTL.iblock -> Registers.reg list * Registers.reg list

val btl_max_reg : BTL.code -> Registers.reg list -> int