Fix OCaml files for compilation

4 files changed, 94 insertions, 92 deletions

diff --git a/src/hls/Partition.ml b/src/hls/Partition.ml
index d9bccad..d0b5a1b 100644
--- a/src/hls/Partition.ml
+++ b/src/hls/Partition.ml
@@ -25,6 +25,7 @@ open Maps
 open AST
 open Kildall
 open Op
+open RTLBlockInstr
 open RTLBlock
 
 (* Assuming that the nodes of the CFG [code] are numbered in reverse postorder (cf. pass
@@ -64,14 +65,14 @@ let rec next_bblock_from_RTL is_start e (c : RTL.code) s i =
   match trans_inst, succ with
   | (None, Some i'), _ ->
     if List.exists (fun x -> x = s) (snd e) && not is_start then
-      Errors.OK { bb_body = []; bb_exit = Some (RBgoto s) }
+      Errors.OK { bb_body = []; bb_exit = RBgoto s }
     else
-      Errors.OK { bb_body = []; bb_exit = Some i' }
+      Errors.OK { bb_body = []; bb_exit = i' }
   | (Some i', None), (s', Some i_n)::[] ->
     if List.exists (fun x -> x = s) (fst e) then
-      Errors.OK { bb_body = [i']; bb_exit = Some (RBgoto s') }
+      Errors.OK { bb_body = [i']; bb_exit = RBgoto s' }
     else if List.exists (fun x -> x = s) (snd e) && not is_start then
-      Errors.OK { bb_body = []; bb_exit = Some (RBgoto s) }
+      Errors.OK { bb_body = []; bb_exit = RBgoto s }
     else begin
       match next_bblock_from_RTL false e c s' i_n with
       | Errors.OK bb ->
@@ -100,14 +101,12 @@ let rec translate_all edge c s res =
      | Some i ->
        match next_bblock_from_RTL true edge c s i with
        | Errors.Error msg -> Errors.Error msg
-       | Errors.OK {bb_exit = None; _} ->
-         Errors.Error (Errors.msg (coqstring_of_camlstring "Error in translate all"))
-       | Errors.OK {bb_body = bb; bb_exit = Some e} ->
+       | Errors.OK {bb_body = bb; bb_exit = e} ->
          let succ = List.filter (fun x -> P.lt x s) (successors_instr e) in
          (match traverseacc (translate_all edge c) succ (c_bb, s :: translated) with
           | Errors.Error msg -> Errors.Error msg
           | Errors.OK (c', t') ->
-            Errors.OK (PTree.set s {bb_body = bb; bb_exit = Some e} c', t')))
+            Errors.OK (PTree.set s {bb_body = bb; bb_exit = e} c', t')))
 
 (* Partition a function and transform it into RTLBlock. *)
 let function_from_RTL f =
diff --git a/src/hls/PrintRTLBlock.ml b/src/hls/PrintRTLBlock.ml
index 45bd253..caf64ff 100644
--- a/src/hls/PrintRTLBlock.ml
+++ b/src/hls/PrintRTLBlock.ml
@@ -17,8 +17,10 @@ open Camlcoq
 open Datatypes
 open Maps
 open AST
+open RTLBlockInstr
 open RTLBlock
 open PrintAST
+open PrintRTLBlockInstr
 
 (* Printing of RTL code *)
 
@@ -34,55 +36,6 @@ let ros pp = function
   | Coq_inl r -> reg pp r
   | Coq_inr s -> fprintf pp "\"%s\"" (extern_atom s)
 
-let print_bblock_body pp i =
-  fprintf pp "\t\t";
-  match i with
-  | RBnop -> fprintf pp "nop\n"
-  | RBop(op, ls, dst) ->
-     fprintf pp "%a = %a\n"
-       reg dst (PrintOp.print_operation reg) (op, ls)
-  | RBload(chunk, addr, args, dst) ->
-     fprintf pp "%a = %s[%a]\n"
-       reg dst (name_of_chunk chunk)
-       (PrintOp.print_addressing reg) (addr, args)
-  | RBstore(chunk, addr, args, src) ->
-     fprintf pp "%s[%a] = %a\n"
-       (name_of_chunk chunk)
-       (PrintOp.print_addressing reg) (addr, args)
-       reg src
-
-let print_bblock_exit pp i =
-  fprintf pp "\t\t";
-  match i with
-  | Some(RBcall(_, fn, args, res, _)) ->
-      fprintf pp "%a = %a(%a)\n"
-        reg res ros fn regs args;
-  | Some(RBtailcall(_, fn, args)) ->
-      fprintf pp "tailcall %a(%a)\n"
-        ros fn regs args
-  | Some(RBbuiltin(ef, args, res, _)) ->
-      fprintf pp "%a = %s(%a)\n"
-        (print_builtin_res reg) res
-        (name_of_external ef)
-        (print_builtin_args reg) args
-  | Some(RBcond(cond, args, s1, s2)) ->
-      fprintf pp "if (%a) goto %d else goto %d\n"
-        (PrintOp.print_condition reg) (cond, args)
-        (P.to_int s1) (P.to_int s2)
-  | Some(RBjumptable(arg, tbl)) ->
-      let tbl = Array.of_list tbl in
-      fprintf pp "jumptable (%a)\n" reg arg;
-      for i = 0 to Array.length tbl - 1 do
-        fprintf pp "\tcase %d: goto %d\n" i (P.to_int tbl.(i))
-      done
-  | Some(RBreturn None) ->
-      fprintf pp "return\n"
-  | Some(RBreturn (Some arg)) ->
-      fprintf pp "return %a\n" reg arg
-  | Some(RBgoto n) ->
-     fprintf pp "goto %d\n" (P.to_int n)
-  | None -> fprintf pp "\n"
-
 let print_bblock pp (pc, i) =
   fprintf pp "%5d:{\n" pc;
   List.iter (print_bblock_body pp) i.bb_body;
diff --git a/src/hls/PrintRTLBlockInstr.ml b/src/hls/PrintRTLBlockInstr.ml
new file mode 100644
index 0000000..3709e04
--- /dev/null
+++ b/src/hls/PrintRTLBlockInstr.ml
@@ -0,0 +1,67 @@
+open Printf
+open Camlcoq
+open Datatypes
+open Maps
+open AST
+open RTLBlockInstr
+open PrintAST
+
+let reg pp r =
+  fprintf pp "x%d" (P.to_int r)
+
+let rec regs pp = function
+  | [] -> ()
+  | [r] -> reg pp r
+  | r1::rl -> fprintf pp "%a, %a" reg r1 regs rl
+
+let ros pp = function
+  | Coq_inl r -> reg pp r
+  | Coq_inr s -> fprintf pp "\"%s\"" (extern_atom s)
+
+let print_bblock_body pp i =
+  fprintf pp "\t\t";
+  match i with
+  | RBnop -> fprintf pp "nop\n"
+  | RBop(op, ls, dst) ->
+     fprintf pp "%a = %a\n"
+       reg dst (PrintOp.print_operation reg) (op, ls)
+  | RBload(chunk, addr, args, dst) ->
+     fprintf pp "%a = %s[%a]\n"
+       reg dst (name_of_chunk chunk)
+       (PrintOp.print_addressing reg) (addr, args)
+  | RBstore(chunk, addr, args, src) ->
+     fprintf pp "%s[%a] = %a\n"
+       (name_of_chunk chunk)
+       (PrintOp.print_addressing reg) (addr, args)
+       reg src
+
+let print_bblock_exit pp i =
+  fprintf pp "\t\t";
+  match i with
+  | RBcall(_, fn, args, res, _) ->
+      fprintf pp "%a = %a(%a)\n"
+        reg res ros fn regs args;
+  | RBtailcall(_, fn, args) ->
+      fprintf pp "tailcall %a(%a)\n"
+        ros fn regs args
+  | RBbuiltin(ef, args, res, _) ->
+      fprintf pp "%a = %s(%a)\n"
+        (print_builtin_res reg) res
+        (name_of_external ef)
+        (print_builtin_args reg) args
+  | RBcond(cond, args, s1, s2) ->
+      fprintf pp "if (%a) goto %d else goto %d\n"
+        (PrintOp.print_condition reg) (cond, args)
+        (P.to_int s1) (P.to_int s2)
+  | RBjumptable(arg, tbl) ->
+      let tbl = Array.of_list tbl in
+      fprintf pp "jumptable (%a)\n" reg arg;
+      for i = 0 to Array.length tbl - 1 do
+        fprintf pp "\tcase %d: goto %d\n" i (P.to_int tbl.(i))
+      done
+  | RBreturn None ->
+      fprintf pp "return\n"
+  | RBreturn (Some arg) ->
+      fprintf pp "return %a\n" reg arg
+  | RBgoto n ->
+     fprintf pp "goto %d\n" (P.to_int n)
diff --git a/src/hls/Schedule.ml b/src/hls/Schedule.ml
index f30197a..9865690 100644
--- a/src/hls/Schedule.ml
+++ b/src/hls/Schedule.ml
@@ -25,6 +25,7 @@ open Maps
 open AST
 open Kildall
 open Op
+open RTLBlockInstr
 open RTLBlock
 open HTL
 open Verilog
@@ -38,7 +39,7 @@ module IMap = Map.Make (struct
   let compare = compare
 end)
 
-type dfg = { nodes : instruction list; edges : (int * int) list }
+type dfg = { nodes : instr list; edges : (int * int) list }
 (** The DFG type defines a list of instructions with their data dependencies as [edges], which are
    the pairs of integers that represent the index of the instruction in the [nodes].  The edges
    always point from left to right. *)
@@ -54,7 +55,7 @@ let print_tuple out_chan a =
 
 let print_dfg out_chan dfg =
   fprintf out_chan "{ nodes = %a, edges = %a }"
-    (print_list PrintRTLBlock.print_bblock_body)
+    (print_list PrintRTLBlockInstr.print_bblock_body)
     dfg.nodes (print_list print_tuple) dfg.edges
 
 let read_process command =
@@ -246,9 +247,7 @@ let gather_bb_constraints debug bb =
     List.fold_left accumulate_WAW_mem_deps (0, dfg'''') bb.bb_body
   in
   if debug then printf "DFG''''': %a\n" print_dfg dfg''''' else ();
-  match bb.bb_exit with
-  | None -> assert false
-  | Some e -> (List.length bb.bb_body, dfg''''', successors_instr e)
+  (List.length bb.bb_body, dfg''''', successors_instr bb.bb_exit)
 
 let gen_bb_name s i = sprintf "bb%d%s" (P.to_int i) s
 
@@ -368,21 +367,6 @@ let find_max = function
       in
       find_max' (snd l) ls
 
-let translate_instruction = function
-  | RBnop -> RTLPar.RPnop
-  | RBop (op, lr, r) -> RTLPar.RPop (op, lr, r)
-  | RBload (chunk, addr, args, dst) -> RTLPar.RPload (chunk, addr, args, dst)
-  | RBstore (chunk, addr, args, src) -> RTLPar.RPstore (chunk, addr, args, src)
-
-let translate_control_flow = function
-  | RBcall (s, i, lr, dst, n) -> RTLPar.RPcall (s, i, lr, dst, n)
-  | RBtailcall (s, i, lr) -> RTLPar.RPtailcall (s, i, lr)
-  | RBbuiltin (e, lr, dst, n) -> RTLPar.RPbuiltin (e, lr, dst, n)
-  | RBcond (c, lr, n1, n2) -> RTLPar.RPcond (c, lr, n1, n2)
-  | RBjumptable (r, ln) -> RTLPar.RPjumptable (r, ln)
-  | RBreturn r -> RTLPar.RPreturn r
-  | RBgoto n -> RTLPar.RPgoto n
-
 let ( >>= ) = bind
 
 let combine_bb_schedule schedule s =
@@ -393,13 +377,13 @@ let compare_tuple (a, _) (b, _) = compare a b
 
 (** Should generate the [RTLPar] code based on the input [RTLBlock] description. *)
 let transf_rtlpar c (schedule : (int * int) list IMap.t) =
-  let f i bb =
+  let f i bb : RTLPar.bblock =
     match bb with
-    | { bb_body = []; bb_exit = Some c } ->
-      { RTLPar.bb_body = [];
-        RTLPar.bb_exit = Some (translate_control_flow c)
+    | { bb_body = []; bb_exit = c } ->
+      { bb_body = [];
+        bb_exit = c
       }
-    | { bb_body = bb_body'; bb_exit = Some ctrl_flow } ->
+    | { bb_body = bb_body'; bb_exit = ctrl_flow } ->
         let i_sched =
           try IMap.find (P.to_int i) schedule
           with Not_found -> (
@@ -417,17 +401,16 @@ let transf_rtlpar c (schedule : (int * int) list IMap.t) =
         in
         printf "--------------- curr: %d, max: %d, min: %d, next: %d\n" (P.to_int i) max_state min_state (P.to_int i - max_state + min_state - 1);
         printf "HIIIII: %d orig: %d\n" (P.to_int i - max_state + min_state - 1) (P.to_int i);
-        { RTLPar.bb_body = (IMap.to_seq i_sched_tree |> List.of_seq |> List.sort compare_tuple |> List.map snd
-                           |> List.map (List.map (fun x -> List.nth bb_body' x |> translate_instruction)));
-          RTLPar.bb_exit = Some (translate_control_flow ctrl_flow)
+        { bb_body = (IMap.to_seq i_sched_tree |> List.of_seq |> List.sort compare_tuple |> List.map snd
+                           |> List.map (List.map (fun x -> List.nth bb_body' x)));
+          bb_exit = ctrl_flow
         }
-    | _ -> assert false
   in
   PTree.map f c
 
 let second = function (_, a, _) -> a
 
-let schedule entry (c : code) =
+let schedule entry (c : RTLBlock.bb RTLBlockInstr.code) =
   let debug = true in
   let c' = PTree.map1 (gather_bb_constraints false) c in
   let _ = if debug then PTree.map (fun r o -> printf "##### %d #####\n%a\n\n" (P.to_int r) print_dfg (second o)) c' else PTree.empty in
@@ -440,9 +423,9 @@ let schedule entry (c : code) =
   transf_rtlpar c schedule'
 
 let schedule_fn (f : RTLBlock.coq_function) : RTLPar.coq_function =
-  { RTLPar.fn_sig = f.fn_sig;
-    RTLPar.fn_params = f.fn_params;
-    RTLPar.fn_stacksize = f.fn_stacksize;
-    RTLPar.fn_code = schedule f.fn_entrypoint f.fn_code;
-    RTLPar.fn_entrypoint = f.fn_entrypoint
+  { fn_sig = f.fn_sig;
+    fn_params = f.fn_params;
+    fn_stacksize = f.fn_stacksize;
+    fn_code = schedule f.fn_entrypoint f.fn_code;
+    fn_entrypoint = f.fn_entrypoint
   }