Previous  Up  Next

Module BTLtoRTLaux

module BTLtoRTLaux: sig .. end

Translation from BTL to RTL and CFG factorization

val translate_function : BTL.iblock_info Maps.PTree.t -> 'a -> RTL.instruction Maps.PTree.t
module Mapnode: Stdlib.Map.Make(Stdlib.Int)
val no_succ_inst : RTL.instruction -> RTL.instruction
module Instbl: Stdlib.Hashtbl.Make(sig
type t = RTL.instruction 
val equal : RTL.instruction -> RTL.instruction -> bool
val hash : RTL.instruction -> int
end)
val find : Mapnode.key Mapnode.t ->
       Mapnode.key -> Mapnode.key
val subst_inst : Mapnode.key Mapnode.t ->
       RTL.instruction -> RTL.instruction
val label : 'a Mapnode.t Stdlib.ref -> Mapnode.key -> 'a -> unit
val minimize_output : RTL.instruction Mapnode.t ->
       Mapnode.key Mapnode.t ->
       RTL.instruction Mapnode.t
val init_rep : Mapnode.key Mapnode.t Stdlib.ref ->
       Mapnode.key -> unit
val ord_add_rep : Mapnode.key Mapnode.t Stdlib.ref ->
       Mapnode.key -> Mapnode.key -> unit
val get_succ : RTL.instruction -> int list
val first_approx : Instbl.key Mapnode.t ->
       Mapnode.key Mapnode.t
val simplify_id : RTL.instruction Mapnode.t ->
       RTL.instruction Mapnode.t *
       Mapnode.key Mapnode.t
val preds : RTL.instruction Mapnode.t ->
       (int, Mapnode.key) Stdlib.Hashtbl.t
type eqclass = {
   rep : int;
   mutable others : int list;
} 
val eqv_of : 'a ->
       Mapnode.key Mapnode.t ->
       eqclass Mapnode.t
type state = {
   cfg : RTL.instruction Mapnode.t;
   preds : (int, int) Stdlib.Hashtbl.t;
   old_repm : int Mapnode.t;
   mutable repm : int Mapnode.t;
   mutable eqv : eqclass Mapnode.t;
   mutable queue : eqclass Mapnode.t;
} 
val init_state : Instbl.key Mapnode.t -> state
val init_eqc : state -> Mapnode.key -> eqclass
val ord_add_eqc : state -> Mapnode.key -> eqclass -> unit
val get_succ_repr : state -> Mapnode.key -> Mapnode.key list
val init_succm : state ->
       eqclass ->
       (Mapnode.key list, eqclass) Stdlib.Hashtbl.t
val get_pred : state ->
       eqclass -> eqclass Mapnode.t
val mark_to_visit : state ->
       'a ->
       eqclass Mapnode.t ->
       eqclass Mapnode.t -> unit
val next_approx : state -> eqclass -> unit
val get_rep : Camlcoq.P.t ->
       int Mapnode.t ->
       Mapnode.key Mapnode.t -> Camlcoq.P.t
val factorize_cfg : Instbl.key Maps.PTree.t ->
       Camlcoq.P.t ->
       Camlcoq.P.t Maps.PTree.tree ->
       (RTL.instruction Maps.PTree.t * Camlcoq.P.t) * Camlcoq.P.t Maps.PTree.tree
val btl2rtl : BTL.coq_function ->
       (RTL.instruction Maps.PTree.t * Camlcoq.P.t) * Camlcoq.P.t Maps.PTree.t