Translate from RTLBlock to RTLPar

1 files changed, 39 insertions, 201 deletions

diff --git a/src/hls/Schedule.ml b/src/hls/Schedule.ml
index 982aa0e..f30197a 100644
--- a/src/hls/Schedule.ml
+++ b/src/hls/Schedule.ml
@@ -324,7 +324,7 @@ let rec intersperse s = function
 let update_schedule v = function Some l -> Some (v :: l) | None -> Some [ v ]
 
 let parse_soln tree s =
-  let r = Str.regexp "v\([0-9]+\)b_\([0-9]+\)[ ]+\([0-9]+\)" in
+  let r = Str.regexp "v\\([0-9]+\\)b_\\([0-9]+\\)[ ]+\\([0-9]+\\)" in
   if Str.string_match r s 0 then
     IMap.update
       (Str.matched_group 1 s |> int_of_string)
@@ -368,151 +368,37 @@ let find_max = function
       in
       find_max' (snd l) ls
 
-type registers = { reg_finish : reg; reg_return : reg; reg_stk : reg }
+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 translate_control_flow r curr_st instr =
-  match instr with
-  | RBgoto n ->
-      fun state ->
-        OK
-          ( (),
-            {
-              state with
-              st_controllogic =
-                PTree.set curr_st (state_goto state.st_st n)
-                  state.st_controllogic;
-            } )
-  | RBcond (c, rs, n1, n2) ->
-      translate_condition c rs >>= fun ce state ->
-      OK
-        ( (),
-          {
-            state with
-            st_controllogic =
-              PTree.set curr_st
-                (state_cond state.st_st ce n1 n2)
-                state.st_controllogic;
-          } )
-  | RBreturn ret -> (
-      let new_state state = state.st_freshstate in
-      match ret with
-      | None ->
-          let fin =
-            Vseq
-              ( HTLgen.block r.reg_finish
-                  (Vlit (ValueInt.coq_ZToValue (Z.of_uint 1))),
-                HTLgen.block r.reg_return
-                  (Vlit (ValueInt.coq_ZToValue (Z.of_uint 0))) )
-          in
-          fun state ->
-            OK
-              ( (),
-                {
-                  state with
-                  st_datapath =
-                    PTree.set (new_state state) fin state.st_datapath;
-                  st_controllogic =
-                    PTree.set curr_st
-                      (state_goto state.st_st (new_state state))
-                      state.st_controllogic;
-                  st_freshstate = P.succ state.st_freshstate;
-                } )
-      | Some ret' ->
-          let fin =
-            Vseq
-              ( HTLgen.block r.reg_finish
-                  (Vlit (ValueInt.coq_ZToValue (Z.of_uint 1))),
-                HTLgen.block r.reg_return (Vvar ret') )
-          in
-          fun state ->
-            OK
-              ( (),
-                {
-                  state with
-                  st_datapath =
-                    PTree.set (new_state state) fin state.st_datapath;
-                  st_controllogic =
-                    PTree.set curr_st
-                      (state_goto state.st_st (new_state state))
-                      state.st_controllogic;
-                  st_freshstate = P.succ state.st_freshstate;
-                } ) )
-  | RBjumptable (r, tbl) ->
-      fun state ->
-      OK ( (),
-        {
-          state with
-          st_controllogic = PTree.set curr_st (Vcase (Vvar r, HTLgen.tbl_to_case_expr state.st_st tbl, Some Vskip)) state.st_controllogic
-        })
-  | _ ->
-      error
-        (Errors.msg
-           (coqstring_of_camlstring
-              "Control flow instructions not implemented."))
-
-let translate_instr r curr_st instr =
-  let prev_instr state =
-    match PTree.get curr_st state.st_datapath with None -> Vskip | Some v -> v
-  in
-  match instr with
-  | RBnop ->
-      fun state ->
-        OK
-          ( (),
-            {
-              state with
-              st_datapath =
-                PTree.set curr_st (prev_instr state) state.st_datapath;
-            } )
-  | RBop (op, rs, dst) ->
-      translate_instr op rs >>= fun instr ->
-      declare_reg None dst (Nat.of_int 32) >>= fun _ state ->
-      let stmnt = Vseq (prev_instr state, nonblock dst instr) in
-      OK
-        ( (),
-          { state with st_datapath = PTree.set curr_st stmnt state.st_datapath }
-        )
-  | RBload (mem, addr, rs, dst) ->
-      translate_arr_access mem addr rs r.reg_stk >>= fun src ->
-      declare_reg None dst (Nat.of_int 32) >>= fun _ state ->
-      let stmnt = Vseq (prev_instr state, nonblock dst src) in
-      OK
-        ( (),
-          { state with st_datapath = PTree.set curr_st stmnt state.st_datapath }
-        )
-  | RBstore (mem, addr, rs, src) ->
-      translate_arr_access mem addr rs r.reg_stk >>= fun dst state ->
-      OK
-        ( (),
-          {
-            state with
-            st_datapath =
-              PTree.set curr_st
-                (Vseq (prev_instr state, Vnonblock (dst, Vvar src)))
-                state.st_datapath;
-          } )
-
 let combine_bb_schedule schedule s =
   let i, st = s in
   IMap.update st (update_schedule i) schedule
 
-let add_schedules r bb_body min_sched curr ischedule =
-  let i, schedule = ischedule in
-  let curr_state = curr - i + min_sched in
-  let instrs = List.map (List.nth bb_body) schedule in
-  if curr_state = 20 then printf "HII: curr_state: %d : curr: %d\n" curr_state curr;
-  collectlist (translate_instr r (P.of_int curr_state)) instrs >>= fun _ ->
-  translate_control_flow r (P.of_int curr_state)
-    (RBgoto (curr_state - 1 |> P.of_int))
-
-(** Should generate the [HTL] code based on the input [RTLBlock] description. *)
-let transf_htl r c (schedule : (int * int) list IMap.t) =
-  let f bbs =
-    let i, bb = bbs in
+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 =
     match bb with
-    | { bb_body = []; bb_exit = Some c } -> translate_control_flow r i c
+    | { bb_body = []; bb_exit = Some c } ->
+      { RTLPar.bb_body = [];
+        RTLPar.bb_exit = Some (translate_control_flow c)
+      }
     | { bb_body = bb_body'; bb_exit = Some ctrl_flow } ->
         let i_sched =
           try IMap.find (P.to_int i) schedule
@@ -529,26 +415,19 @@ let transf_htl r c (schedule : (int * int) list IMap.t) =
         let i_sched_tree =
           List.fold_left combine_bb_schedule IMap.empty i_sched
         in
-        collectlist
-          (add_schedules r bb_body' min_state (P.to_int i))
-          (IMap.to_seq i_sched_tree |> List.of_seq)
-        >>= fun _ ->
         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);
-        (match ctrl_flow with
-         | RBgoto _ ->
-           translate_control_flow r (P.of_int (P.to_int i - max_state + min_state)) ctrl_flow
-         | _ ->
-           translate_control_flow r (P.of_int (P.to_int i - max_state + min_state - 1)) ctrl_flow)
-    | _ ->
-        coqstring_of_camlstring "Illegal state reached in scheduler"
-        |> Errors.msg |> error
+        { 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)
+        }
+    | _ -> assert false
   in
-  collectlist f c
+  PTree.map f c
 
 let second = function (_, a, _) -> a
 
-let schedule entry r (c : code) =
+let schedule entry (c : 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
@@ -558,53 +437,12 @@ let schedule entry r (c : code) =
   let schedule' = solve_constraints vars constraints types in
   IMap.iter (fun a b -> printf "##### %d #####\n%a\n\n" a (print_list print_tuple) b) schedule';
   (*printf "Schedule: %a\n" (fun a x -> IMap.iter (fun d -> fprintf a "%d: %a\n" d (print_list print_tuple)) x) schedule';*)
-  transf_htl r (PTree.elements c) schedule'
-
-let transl_module' (f : RTLBlock.coq_function) : HTL.coq_module mon =
-  create_reg (Some Voutput) (Nat.of_int 1) >>= fun fin ->
-  create_reg (Some Voutput) (Nat.of_int 32) >>= fun rtrn ->
-  create_arr None (Nat.of_int 32) (Nat.of_int (Z.to_int f.fn_stacksize / 4))
-  >>= fun stack_var ->
-  let stack, stack_len = stack_var in
-  schedule f.fn_entrypoint
-    { reg_finish = fin; reg_return = rtrn; reg_stk = stack }
-    f.fn_code
-  >>= fun _ ->
-  collectlist (fun r -> declare_reg (Some Vinput) r (Nat.of_int 32)) f.fn_params
-  >>= fun _ ->
-  create_reg (Some Vinput) (Nat.of_int 1) >>= fun start ->
-  create_reg (Some Vinput) (Nat.of_int 1) >>= fun rst ->
-  create_reg (Some Vinput) (Nat.of_int 1) >>= fun clk current_state ->
-  let m =
-    {
-      HTL.mod_params = f.fn_params;
-      HTL.mod_datapath = current_state.st_datapath;
-      HTL.mod_controllogic = current_state.st_controllogic;
-      HTL.mod_entrypoint = f.fn_entrypoint;
-      HTL.mod_st = current_state.st_st;
-      HTL.mod_stk = stack;
-      HTL.mod_stk_len = stack_len;
-      HTL.mod_finish = fin;
-      HTL.mod_return = rtrn;
-      HTL.mod_start = start;
-      HTL.mod_reset = rst;
-      HTL.mod_clk = clk;
-      HTL.mod_scldecls = current_state.st_scldecls;
-      HTL.mod_arrdecls = current_state.st_arrdecls;
-    }
-  in
-  OK (m, current_state)
-
-let max_state f =
-  let st = P.of_int 10000 in
-  {
-    (init_state st) with
-    st_st = st;
-    st_freshreg = P.succ st;
-    st_freshstate = P.of_int 10000;
-    st_scldecls =
-      AssocMap.AssocMap.set st (None, Nat.of_int 32) (init_state st).st_scldecls;
+  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
   }
-
-let transl_module (f : RTLBlock.coq_function) : HTL.coq_module Errors.res =
-  run_mon (max_state f) (transl_module' f)