From 3b77ad9c0f3c52ba1cc02f954ee5bc2b63f51366 Mon Sep 17 00:00:00 2001 From: Yann Herklotz Date: Sun, 31 Jan 2021 15:43:50 +0000 Subject: Fix OCaml files for compilation --- src/hls/Partition.ml | 15 +++++----- src/hls/PrintRTLBlock.ml | 51 ++------------------------------ src/hls/PrintRTLBlockInstr.ml | 67 +++++++++++++++++++++++++++++++++++++++++++ src/hls/Schedule.ml | 53 ++++++++++++---------------------- 4 files changed, 94 insertions(+), 92 deletions(-) create mode 100644 src/hls/PrintRTLBlockInstr.ml (limited to 'src') 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 } -- cgit