Use Tunnelinglibs in RTLTunnelingaux

1 files changed, 25 insertions, 12 deletions

diff --git a/backend/Tunnelinglibs.ml b/backend/Tunnelinglibs.ml
index ce384dac..e1e61d68 100644
--- a/backend/Tunnelinglibs.ml
+++ b/backend/Tunnelinglibs.ml
@@ -20,7 +20,6 @@ See [Tunneling.v] and [RTLTunneling.v]
 
 *)
 
-open Coqlib
 open Maps
 open Camlcoq
 
@@ -42,7 +41,8 @@ and node = {
 
 type cfg_node = (int, node) Hashtbl.t
 
-type lnode = P.t
+type positive = P.t
+type integer = Z.t
 
 (* type of the (simplified) CFG *)
 type cfg = {
@@ -64,19 +64,15 @@ module Tunneling = functor
     val final_dump: bool (* set to true to have a more verbose debugging *)
   end)
   (FUNS: sig
-    type lang
-    type code_type
-
     (* build [c.nodes] and accumulate in [acc] conditions at beginning of LTL basic-blocks *)
-    val build_simplified_cfg: cfg -> cfg_node list -> lnode ->
-      LANG.code_unit -> cfg_node list
+    val build_simplified_cfg: cfg -> node list -> positive -> LANG.code_unit -> node list
 
-    val print_code_unit: cfg -> bool -> (int * LANG.code_unit) -> bool
+    val print_code_unit: cfg -> bool -> int * LANG.code_unit -> bool
 
     val fn_code: LANG.funct -> LANG.code_unit PTree.t
-    val fn_entrypoint: LANG.funct -> lnode
+    val fn_entrypoint: LANG.funct -> positive
 
-    val check_code_unit: LANG.code_unit PTree.t -> lnode -> LANG.code_unit -> unit
+    val check_code_unit: (positive * integer) PTree.t -> positive -> LANG.code_unit -> unit
   end)
 -> struct
 
@@ -151,8 +147,7 @@ let try_change_cond c acc pc =
 (* repeat [try_change_cond] until no condition is changed into a branch *)
 let rec repeat_change_cond c =
   c.iter_num <- c.iter_num + 1;
-  debug "++ %sTunneling.branch_target %d: remaining number of conds to consider
-  = %d\n" OPT.langname (c.iter_num) (c.num_rems);
+  debug "++ %sTunneling.branch_target %d: remaining number of conds to consider = %d\n" OPT.langname (c.iter_num) (c.num_rems);
   let old =  c.num_rems in
   c.rems <- List.fold_left (try_change_cond c) [] c.rems;
   let curr = c.num_rems in
@@ -234,4 +229,22 @@ let check_code td c =
 
 (*** END: copy-paste & debugging functions *******)
 
+let branch_target f =
+  debug "* %sTunneling.branch_target: starting on a new function\n" OPT.langname;
+  if OPT.limit_tunneling <> None then debug "* WARNING: limit_tunneling <> None\n";
+  let c = { nodes = Hashtbl.create 100; rems = []; num_rems = 0; iter_num = 0 } in
+  c.rems <- PTree.fold (FUNS.build_simplified_cfg c) (FUNS.fn_code f) [];
+  repeat_change_cond c;
+  let res = final_export f c in
+  if !OPT.debug_flag then (
+    try
+      check_code res (FUNS.fn_code f);
+      if OPT.final_dump then print_cfg f c;
+    with e -> (
+      print_cfg f c;
+      check_code res (FUNS.fn_code f)
+    )
+  );
+  res
+
 end