Simplify tunneling factorisation

The recursive module definitions required unnecessarily long expicit
signatures for little added legibility.

1 files changed, 24 insertions, 41 deletions

diff --git a/backend/RTLTunnelingaux.ml b/backend/RTLTunnelingaux.ml
index 5fe327d4..9333e357 100644
--- a/backend/RTLTunnelingaux.ml
+++ b/backend/RTLTunnelingaux.ml
@@ -26,8 +26,6 @@ open Maps
 open Camlcoq
 open Tunnelinglibs
 
-let nopcounter = ref 0
-
 module LANG = struct
   type code_unit = RTL.instruction
   type funct = RTL.coq_function
@@ -40,60 +38,44 @@ module OPT = struct
   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
+module Partial = Tunnelinglibs.Tunneling(LANG)(OPT)
 
-  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
+module FUNS = 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;
+       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 = T.get_node c s1 in
-       let ns2 = T.get_node c s2 in
-       let npc = T.get_node c pc in
+       let ns1 = get_node c s1 in
+       let ns2 = get_node c s2 in
+       let npc = 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
+    | Inop s -> (if println then Partial.debug "\n");
+        Partial.debug "%d:Inop %d %s\n" pc (P.to_int s) (string_of_labeli c.nodes pc);
+        false
+    | Icond (_, _, s1, s2, _) -> (if println then Partial.debug "\n");
+        Partial.debug "%d:Icond (%d,%d) %s\n" pc (P.to_int s1) (P.to_int s2) (string_of_labeli c.nodes pc);
+        false
+    | _ -> Partial.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 ->
@@ -105,8 +87,8 @@ end = struct
             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))
+                 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
@@ -115,15 +97,16 @@ end = struct
                  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))
+                           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 (T.BugOnPC (P.to_int pc)) end
+            raise (BugOnPC (P.to_int pc)) end
     | None -> ()
 
 end
 
+module T = Partial.T(FUNS)
 let branch_target = T.branch_target