Use Tunnelinglibs in RTLTunnelingaux

2 files changed, 123 insertions, 265 deletions

diff --git a/backend/RTLTunnelingaux.ml b/backend/RTLTunnelingaux.ml
index a30b43cf..5fe327d4 100644
--- a/backend/RTLTunnelingaux.ml
+++ b/backend/RTLTunnelingaux.ml
@@ -24,261 +24,106 @@ open Coqlib
 open RTL
 open Maps
 open Camlcoq
-
-let limit_tunneling = None (* for debugging: [Some x] limit the number of iterations *)
-let debug_flag = ref true
-let final_dump = false   (* set to true to have a more verbose debugging *)
-
-let debug fmt =
-  if !debug_flag then Printf.eprintf fmt
-  else Printf.ifprintf stderr fmt
-
-exception BugOnPC of int
+open Tunnelinglibs
 
 let nopcounter = ref 0
 
-(* type of labels in the cfg *)
-type label = int * P.t
-
-(* instructions under analyzis *)
-type simple_inst = (* a simplified view of RTL instructions *)
-  INOP of node
-| ICOND of node * node
-| OTHER
-and node = {
-    lab : label;
-    mutable inst: simple_inst;
-    mutable link: node; (* link in the union-find: itself for non "nop"-nodes, target of the "nop" otherwise *)
-    mutable dist: int;
-    mutable tag: int
-  }
-
-(* type of the (simplified) CFG *)
-type cfg = {
-    nodes: (int, node) Hashtbl.t;
-    mutable rems: node list; (* remaining conditions that may become lbranch or not *)
-    mutable num_rems: int;
-    mutable iter_num: int (* number of iterations in elimination of conditions *)
-  }
-
-let lab_i (n: node): int = fst n.lab
-let lab_p (n: node): P.t = snd n.lab
-
-let rec target c n = (* inspired from the "find" of union-find algorithm *)
-  match n.inst with
-  | ICOND(s1,s2) ->
-     if n.link != n
-     then update c n
-     else if n.tag < c.iter_num then (
-       (* we try to change the condition ... *)
-       n.tag <- c.iter_num; (* ... but at most once by iteration *)
-       let ts1 = target c s1 in
-       let ts2 = target c s2 in
-       if ts1 == ts2 then (n.link <- ts1; ts1) else n
-     ) else n
-  | _ ->
-     if n.link != n
-     then update c n
-     else n
-and update c n =
-  let t = target c n.link in
-  n.link <- t; t
-
-let get_node c p =
-  let li = P.to_int p in
-  try
-    Hashtbl.find c.nodes li
-  with
-    Not_found ->
-      let rec n = { lab = (li, p); inst = OTHER; link = n ; dist = 0; tag = 0 }  in
-      Hashtbl.add c.nodes li n;
-      n
-
-let set_branch c p s =
-  let li = P.to_int p in
-  try
-    let n = Hashtbl.find c.nodes li in
-    n.inst <- INOP s;
-    n.link <- target c s
-  with
-    Not_found ->
-      let n = { lab = (li,p); inst = INOP s; link = target c s; dist = 0; tag = 0 } in
-      Hashtbl.add c.nodes li n
-
-
-(* build [c.nodes] and accumulate conditions in [acc] *)
-let build_simplified_cfg c acc pc i =
-  match i with
-  | Inop s ->
-     let ns = get_node c s in
-     set_branch c pc ns;
-     incr nopcounter;
-     acc
-  | Icond (_, _, s1, s2, _) ->
-     c.num_rems <- c.num_rems + 1;
-     let ns1 = get_node c s1 in
-     let ns2 = get_node c s2 in
-     let npc = get_node c pc in
-     npc.inst <- ICOND(ns1, ns2);
-     npc::acc
-  | _ -> acc
-
-(* try to change a condition into a branch
-[acc] is the current accumulator of conditions to consider in the next iteration of repeat_change_cond
-*)
-let try_change_cond c acc pc =
-  match pc.inst with
-  | ICOND(s1,s2) ->
-     let ts1 = target c s1 in
-     let ts2 = target c s2 in
-     if ts1 == ts2 then (
-       pc.link <- ts1;
-       c.num_rems <- c.num_rems - 1;
+module LANG = struct
+  type code_unit = RTL.instruction
+  type funct = RTL.coq_function
+end
+
+module OPT = struct
+  let langname = "RTL"
+  let limit_tunneling = None
+  let debug_flag = ref false
+  let final_dump = false
+end
+
+module rec T: sig
+  val get_node: cfg -> positive -> node
+  val set_branch: cfg -> positive -> node -> unit
+  val debug: ('a, out_channel, unit) format -> 'a
+  val string_of_labeli: ('a, node) Hashtbl.t -> 'a -> string
+  exception BugOnPC of int
+  val branch_target: RTL.coq_function -> (positive * Z.t) PTree.t
+
+end = Tunnelinglibs.Tunneling(LANG)(OPT)(FUNS)
+
+and FUNS: sig
+  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 fn_code: LANG.funct -> LANG.code_unit PTree.t
+  val fn_entrypoint: LANG.funct -> positive
+
+  val check_code_unit: (positive * integer) PTree.t -> positive -> LANG.code_unit -> unit
+end = struct
+  let build_simplified_cfg c acc pc i =
+    match i with
+    | Inop s ->
+       let ns = T.get_node c s in
+       T.set_branch c pc ns;
+       incr nopcounter;
        acc
-     ) else
-       pc::acc
-  | _  -> raise (BugOnPC (lab_i pc)) (* ICOND expected *)
-
-(* 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 "++ RTLTunneling.branch_target %d: remaining number of conds to consider = %d\n" (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
-  let continue =
-    match limit_tunneling with
-    | Some n -> curr < old && c.iter_num < n
-    | None -> curr < old
-  in
-  if continue
-  then repeat_change_cond c
-
-
-(* compute the final distance of each nop nodes to its target *)
-let undef_dist = -1
-let self_dist = undef_dist-1
-let rec dist n =
-  if n.dist = undef_dist
-  then (
-    n.dist <- self_dist; (* protection against an unexpected loop in the data-structure *)
-    n.dist <-
-      (match n.inst with
-       | OTHER -> 0
-       | INOP p -> 1 + dist p
-       | ICOND (p1,p2) -> 1 + (max (dist p1) (dist p2)));
-    n.dist
-  ) else if n.dist=self_dist then raise (BugOnPC (lab_i n))
-    else n.dist
-
-let final_export f c =
-  let count = ref 0 in
-  let filter_nops_init_dist _ n acc =
-    let tn = target c n in
-    if tn == n
-    then (
-      n.dist <- 0; (* force [n] to be a base case in the recursion of [dist] *)
-      acc
-    ) else (
-      n.dist <- undef_dist; (* force [dist] to compute the actual [n.dist] *)
-      count := !count+1;
-      n::acc
-    )
-  in
-  let nops = Hashtbl.fold filter_nops_init_dist c.nodes [] in
-  let res = List.fold_left (fun acc n -> PTree.set (lab_p n) (lab_p n.link, Z.of_uint (dist n)) acc) PTree.empty nops in
-  debug "* RTLTunneling.branch_target: [stats] initial number of nops = %d\n" !nopcounter;
-  debug "* RTLTunneling.branch_target: [stats] final number of eliminated nops = %d\n" !count;
-  res
-
-(*********************************************)
-(*** START: printing and debugging functions *)
-
-let string_of_labeli nodes ipc =
-  try
-    let pc = Hashtbl.find nodes ipc in
-    if pc.link == pc
-    then Printf.sprintf "(Target@%d)" (dist pc)
-    else Printf.sprintf "(Nop %d @%d)" (lab_i pc.link) (dist pc)
-  with
-    Not_found -> ""
-
-let print_instr c println (pc, i) =
-  match i with
-  | Inop s -> (if println then debug "\n"); debug "%d:Inop %d %s\n" pc (P.to_int s) (string_of_labeli c.nodes pc); false
-  | Icond (_, _, s1, s2, _) -> (if println then debug "\n"); debug "%d:Icond (%d,%d) %s\n" pc (P.to_int s1) (P.to_int s2) (string_of_labeli c.nodes pc); false
-  | _ -> debug "%d " pc; true
-
-
-let print_cfg f c  =
-  let a = Array.of_list (PTree.fold (fun acc pc i -> (P.to_int pc,i)::acc) f.fn_code []) in
-  Array.fast_sort (fun (i1,_) (i2,_) -> i2 - i1) a;
-  let ep = P.to_int f.fn_entrypoint in
-  debug "entrypoint: %d %s\n" ep (string_of_labeli c.nodes ep);
-  let println = Array.fold_left (print_instr c) false a in
-  (if println then debug "\n");debug "remaining cond:";
-  List.iter (fun n -> debug "%d " (lab_i n)) c.rems;
-  debug "\n"
-
-(*************************************************************)
-(* Copy-paste of the extracted code of the verifier          *)
-(* with [raise (BugOnPC (P.to_int pc))] instead of [Error.*] *)
-
-let get td pc =
-  match PTree.get pc td with
-  | Some p -> let (t0, d) = p in (t0, d)
-  | None -> (pc, Z.of_uint 0)
-
-let check_instr td pc i =
-  match PTree.get pc td with
-  | Some p ->
-      let (tpc, dpc) = p in
-      let dpc0 = dpc in begin
-        match i with
-        | Inop s ->
-          let (ts, ds) = get td s in
-          if peq tpc ts
-          then if zlt ds dpc0
-               then ()
-               else raise (BugOnPC (P.to_int pc))
-          else raise (BugOnPC (P.to_int pc))
-        | Icond (_, _, s1, s2, _) ->
-          let (ts1, ds1) = get td s1 in
-          let (ts2, ds2) = get td s2 in
-          if peq tpc ts1
-          then if peq tpc ts2
-               then if zlt ds1 dpc0
-                    then if zlt ds2 dpc0
-                         then ()
-                         else raise (BugOnPC (P.to_int pc))
-                    else raise (BugOnPC (P.to_int pc))
-               else raise (BugOnPC (P.to_int pc))
-          else raise (BugOnPC (P.to_int pc))
-        | _ ->
-          raise (BugOnPC (P.to_int pc)) end
-  | None -> ()
-
-(** val check_code : coq_UF -> code -> unit res **)
-
-let check_code td c =
-  PTree.fold (fun _ pc i -> check_instr td pc i) c (())
-
-(*** END: copy-paste & debugging functions *******)
+    | Icond (_, _, s1, s2, _) ->
+       c.num_rems <- c.num_rems + 1;
+       let ns1 = T.get_node c s1 in
+       let ns2 = T.get_node c s2 in
+       let npc = T.get_node c pc in
+       npc.inst <- COND(ns1, ns2);
+       npc::acc
+    | _ -> acc
+
+  let print_code_unit c println (pc, i) =
+    match i with
+    | Inop s -> (if println then T.debug "\n"); T.debug "%d:Inop %d %s\n" pc (P.to_int s) (T.string_of_labeli c.nodes pc); false
+    | Icond (_, _, s1, s2, _) -> (if println then T.debug "\n"); T.debug "%d:Icond (%d,%d) %s\n" pc (P.to_int s1) (P.to_int s2) (T.string_of_labeli c.nodes pc); false
+    | _ -> T.debug "%d " pc; true
+
+  let fn_code f = f.fn_code
+  let fn_entrypoint f = f.fn_entrypoint
+
+  (*************************************************************)
+  (* Copy-paste of the extracted code of the verifier          *)
+  (* with [raise (BugOnPC (P.to_int pc))] instead of [Error.*] *)
+
+  let get td pc =
+    match PTree.get pc td with
+    | Some p -> let (t0, d) = p in (t0, d)
+    | None -> (pc, Z.of_uint 0)
+
+  let check_code_unit td pc i =
+    match PTree.get pc td with
+    | Some p ->
+        let (tpc, dpc) = p in
+        let dpc0 = dpc in begin
+          match i with
+          | Inop s ->
+            let (ts, ds) = get td s in
+            if peq tpc ts
+            then if zlt ds dpc0
+                 then ()
+                 else raise (T.BugOnPC (P.to_int pc))
+            else raise (T.BugOnPC (P.to_int pc))
+          | Icond (_, _, s1, s2, _) ->
+            let (ts1, ds1) = get td s1 in
+            let (ts2, ds2) = get td s2 in
+            if peq tpc ts1
+            then if peq tpc ts2
+                 then if zlt ds1 dpc0
+                      then if zlt ds2 dpc0
+                           then ()
+                           else raise (T.BugOnPC (P.to_int pc))
+                      else raise (T.BugOnPC (P.to_int pc))
+                 else raise (T.BugOnPC (P.to_int pc))
+            else raise (T.BugOnPC (P.to_int pc))
+          | _ ->
+            raise (T.BugOnPC (P.to_int pc)) end
+    | None -> ()
+
+end
+
+let branch_target = T.branch_target
 
-let branch_target f =
-  debug "* RTLTunneling.branch_target: starting on a new function\n";
-  if 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 (build_simplified_cfg c) f.fn_code [];
-  repeat_change_cond c;
-  let res = final_export f c in
-  if !debug_flag then (
-    try
-      check_code res f.fn_code;
-      if final_dump then print_cfg f c;
-    with e -> (
-      print_cfg f c;
-      check_code res f.fn_code
-    )
-  );
-  res
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