Module RTLtoBTLaux

module RTLtoBTLaux: sig .. end

Translation from RTL to BTL and block selection

val get_join_points : RTL.instruction Maps.PTree.t -> Camlcoq.P.t -> Bitv.t

val make_synth_node : BTL.iblock_info Maps.PTree.tree Stdlib.ref ->
       bool -> Bitv.t -> Camlcoq.P.t -> Camlcoq.P.t

val encaps_final : BTL.iblock_info Maps.PTree.tree Stdlib.ref ->
       BTL.iblock -> Camlcoq.P.t option -> bool -> Bitv.t -> BTL.iblock

val translate_inst : BTL.iblock_info Maps.PTree.tree Stdlib.ref ->
       BTL.inst_info_shadow ->
       RTL.instruction -> bool -> bool -> Bitv.t -> BTL.iblock

val no_join_point_successor : Bitv.t -> Camlcoq.P.t option -> Camlcoq.P.t option

val translate_function : RTL.instruction Maps.PTree.t ->
       Camlcoq.P.t ->
       Bitv.t ->
       bool ->
       bool -> BTL.iblock_info Maps.PTree.t * Camlcoq.P.t * Camlcoq.P.t Maps.PTree.t

val rtl2btl : RTL.coq_function ->
       bool ->
       bool ->
       ((BTL.iblock_info Maps.PTree.t * Camlcoq.P.t) * BTLtypes.function_info) *
       Camlcoq.P.t Maps.PTree.t

Main translation function, that can either build basic-blocks or superblocks, and that can optionnaly insert synthetic nodes

val rtl2btl_BB : RTL.coq_function ->
       ((BTL.iblock_info Maps.PTree.t * Camlcoq.P.t) * BTLtypes.function_info) *
       Camlcoq.P.t Maps.PTree.t

Translate from RTL to BTL with basic-blocks

val rtl2btl_BBSN : RTL.coq_function ->
       ((BTL.iblock_info Maps.PTree.t * Camlcoq.P.t) * BTLtypes.function_info) *
       Camlcoq.P.t Maps.PTree.t

Translate from RTL to BTL with basic-blocks and synthetic nodes

val rtl2btl_SB : RTL.coq_function ->
       ((BTL.iblock_info Maps.PTree.t * Camlcoq.P.t) * BTLtypes.function_info) *
       Camlcoq.P.t Maps.PTree.t

Translate from RTL to BTL with superblocks