From bd1fc29d17bdd5d51ec96d429dbc03f21c236d8e Mon Sep 17 00:00:00 2001 From: Yann Herklotz Date: Wed, 13 Jan 2021 17:58:09 +0000 Subject: Translate from RTLBlock to RTLPar --- src/hls/Schedule.ml | 240 +++++++++------------------------------------------- 1 file changed, 39 insertions(+), 201 deletions(-) (limited to 'src/hls/Schedule.ml') 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) -- cgit