From ab520acd80f7d39aa14fdda6932accbb2a787ebf Mon Sep 17 00:00:00 2001 From: Léo Gourdin Date: Wed, 19 May 2021 12:47:22 +0200 Subject: Grouping common RTL functions, printer improvement --- backend/Duplicateaux.ml | 2 +- backend/LICMaux.ml | 5 +-- common/AuxTools.ml | 49 ++++++++++++++++++++++++++++ common/DebugPrint.ml | 6 ++-- scheduling/PrintBTL.ml | 16 ++++++++- scheduling/RTLpathLivegenaux.ml | 49 +++------------------------- scheduling/RTLpathScheduleraux.ml | 1 + scheduling/RTLtoBTLaux.ml | 68 ++++----------------------------------- 8 files changed, 79 insertions(+), 117 deletions(-) create mode 100644 common/AuxTools.ml diff --git a/backend/Duplicateaux.ml b/backend/Duplicateaux.ml index d55da64a..e8e60a4f 100644 --- a/backend/Duplicateaux.ml +++ b/backend/Duplicateaux.ml @@ -23,6 +23,7 @@ open RTL open Maps open Camlcoq open DebugPrint +open AuxTools let stats_oc = ref None @@ -95,7 +96,6 @@ let write_stats_oc () = end let get_loop_headers = LICMaux.get_loop_headers -let get_some = LICMaux.get_some let rtl_successors = LICMaux.rtl_successors (* Get list of nodes following a BFS of the code *) diff --git a/backend/LICMaux.ml b/backend/LICMaux.ml index b88dbc2d..df609505 100644 --- a/backend/LICMaux.ml +++ b/backend/LICMaux.ml @@ -17,16 +17,13 @@ open Kildall;; open HashedSet;; open Inject;; open DebugPrint;; +open AuxTools;; type reg = P.t;; (** get_loop_headers moved from Duplicateaux.ml to LICMaux.ml to prevent cycle dependencies *) type vstate = Unvisited | Processed | Visited -let get_some = function -| None -> failwith "Did not get some" -| Some thing -> thing - let rtl_successors = function | Itailcall _ | Ireturn _ -> [] | Icall(_,_,_,_,n) | Ibuiltin(_,_,_,n) | Inop n | Iop (_,_,_,n) diff --git a/common/AuxTools.ml b/common/AuxTools.ml new file mode 100644 index 00000000..a667044f --- /dev/null +++ b/common/AuxTools.ml @@ -0,0 +1,49 @@ +open RTL +open Maps + +let get_some = function + | None -> failwith "Got None instead of Some _" + | Some thing -> thing + +let successors_inst = function + | Inop n + | Iop (_, _, _, n) + | Iload (_, _, _, _, _, n) + | Istore (_, _, _, _, n) + | Icall (_, _, _, _, n) + | Ibuiltin (_, _, _, n) -> + [ n ] + | Icond (_, _, n1, n2, _) -> [ n1; n2 ] + | Ijumptable (_, l) -> l + | Itailcall _ | Ireturn _ -> [] + +let predicted_successor = function + | Inop n | Iop (_, _, _, n) | Iload (_, _, _, _, _, n) | Istore (_, _, _, _, n) + -> + Some n + | Icall (_, _, _, _, n) | Ibuiltin (_, _, _, n) -> None + | Icond (_, _, n1, n2, p) -> ( + match p with Some true -> Some n1 | Some false -> Some n2 | None -> None) + | Ijumptable _ | Itailcall _ | Ireturn _ -> None + +let non_predicted_successors i = function + | None -> successors_inst i + | Some ps -> List.filter (fun s -> s != ps) (successors_inst i) + +(* adapted from Linearizeaux.get_join_points *) +let get_join_points code entry = + let reached = ref (PTree.map (fun n i -> false) code) in + let reached_twice = ref (PTree.map (fun n i -> false) code) in + let rec traverse pc = + if get_some @@ PTree.get pc !reached then begin + if not (get_some @@ PTree.get pc !reached_twice) then + reached_twice := PTree.set pc true !reached_twice + end else begin + reached := PTree.set pc true !reached; + traverse_succs (successors_inst @@ get_some @@ PTree.get pc code) + end + and traverse_succs = function + | [] -> () + | [pc] -> traverse pc + | pc :: l -> traverse pc; traverse_succs l + in traverse entry; !reached_twice diff --git a/common/DebugPrint.ml b/common/DebugPrint.ml index 6f8449ee..021ea5c0 100644 --- a/common/DebugPrint.ml +++ b/common/DebugPrint.ml @@ -1,6 +1,7 @@ open Maps open Camlcoq open Registers +open AuxTools let debug_flag = ref false @@ -128,10 +129,7 @@ end let print_instructions insts code = - let get_some = function - | None -> failwith "Did not get some" - | Some thing -> thing - in if (!debug_flag) then begin + if (!debug_flag) then begin debug "[ "; List.iter ( fun n -> (PrintRTL.print_instruction stdout (P.to_int n, get_some @@ PTree.get n code)) diff --git a/scheduling/PrintBTL.ml b/scheduling/PrintBTL.ml index 781dcaf3..b461e3f1 100644 --- a/scheduling/PrintBTL.ml +++ b/scheduling/PrintBTL.ml @@ -23,38 +23,48 @@ let ros pp = function let print_succ pp s = fprintf pp "\tsucc %d\n" (P.to_int s) +let print_pref pp pref = + fprintf pp "%s" pref + let rec print_iblock pp is_rec pref ib = - fprintf pp "%s" pref; match ib with | Bnop -> + print_pref pp pref; fprintf pp "Bnop\n" | Bop(op, args, res) -> + print_pref pp pref; fprintf pp "Bop: %a = %a\n" reg res (PrintOp.print_operation reg) (op, args) | Bload(trap, chunk, addr, args, dst) -> + print_pref pp pref; fprintf pp "Bload: %a = %s[%a]%a\n" reg dst (name_of_chunk chunk) (PrintOp.print_addressing reg) (addr, args) print_trapping_mode trap | Bstore(chunk, addr, args, src) -> + print_pref pp pref; fprintf pp "Bstore: %s[%a] = %a\n" (name_of_chunk chunk) (PrintOp.print_addressing reg) (addr, args) reg src | BF (Bcall(sg, fn, args, res, s)) -> + print_pref pp pref; fprintf pp "Bcall: %a = %a(%a)\n" reg res ros fn regs args; print_succ pp s | BF (Btailcall(sg, fn, args)) -> + print_pref pp pref; fprintf pp "Btailcall: %a(%a)\n" ros fn regs args | BF (Bbuiltin(ef, args, res, s)) -> + print_pref pp pref; fprintf pp "Bbuiltin: %a = %s(%a)\n" (print_builtin_res reg) res (name_of_external ef) (print_builtin_args reg) args; print_succ pp s | Bcond(cond, args, ib1, ib2, info) -> + print_pref pp pref; fprintf pp "Bcond: (%a) (prediction: %s)\n" (PrintOp.print_condition reg) (cond, args) (match info with None -> "none" | Some true -> "branch" | Some false -> "fallthrough"); @@ -67,15 +77,19 @@ let rec print_iblock pp is_rec pref ib = fprintf pp "%s]\n" pref | BF (Bjumptable(arg, tbl)) -> let tbl = Array.of_list tbl in + print_pref pp pref; fprintf pp "Bjumptable: (%a)\n" reg arg; for i = 0 to Array.length tbl - 1 do fprintf pp "\t\tcase %d: goto %d\n" i (P.to_int tbl.(i)) done | BF (Breturn None) -> + print_pref pp pref; fprintf pp "Breturn\n" | BF (Breturn (Some arg)) -> + print_pref pp pref; fprintf pp "Breturn: %a\n" reg arg | BF (Bgoto s) -> + print_pref pp pref; fprintf pp "Bgoto: %d\n" (P.to_int s) | Bseq (ib1, ib2) -> if is_rec then ( diff --git a/scheduling/RTLpathLivegenaux.ml b/scheduling/RTLpathLivegenaux.ml index 2a20a15d..c9bb94d3 100644 --- a/scheduling/RTLpathLivegenaux.ml +++ b/scheduling/RTLpathLivegenaux.ml @@ -7,31 +7,7 @@ open Datatypes open Kildall open Lattice open DebugPrint - -let get_some = function -| None -> failwith "Got None instead of Some _" -| Some thing -> thing - -let successors_inst = function -| Inop n | Iop (_,_,_,n) | Iload (_,_,_,_,_,n) | Istore (_,_,_,_,n) | Icall (_,_,_,_,n) | Ibuiltin (_,_,_,n) -> [n] -| Icond (_,_,n1,n2,_) -> [n1; n2] -| Ijumptable (_,l) -> l -| Itailcall _ | Ireturn _ -> [] - -let predicted_successor = function -| Inop n | Iop (_,_,_,n) | Iload (_,_,_,_,_,n) | Istore (_,_,_,_,n) -> Some n -| Icall (_,_,_,_,n) | Ibuiltin (_,_,_,n) -> None -| Icond (_,_,n1,n2,p) -> ( - match p with - | Some true -> Some n1 - | Some false -> Some n2 - | None -> None ) -| Ijumptable _ | Itailcall _ | Ireturn _ -> None - -let non_predicted_successors i = - match predicted_successor i with - | None -> successors_inst i - | Some n -> List.filter (fun n' -> n != n') (successors_inst i) +open AuxTools let rec list_to_regset = function | [] -> Regset.empty @@ -59,24 +35,6 @@ let get_output_reg i = | Iop (_, _, r, _) | Iload (_, _, _, _, r, _) | Icall (_, _, _, r, _) -> Some r | Ibuiltin (_, _, brr, _) -> (match brr with AST.BR r -> Some r | _ -> None) -(* adapted from Linearizeaux.get_join_points *) -let get_join_points code entry = - let reached = ref (PTree.map (fun n i -> false) code) in - let reached_twice = ref (PTree.map (fun n i -> false) code) in - let rec traverse pc = - if get_some @@ PTree.get pc !reached then begin - if not (get_some @@ PTree.get pc !reached_twice) then - reached_twice := PTree.set pc true !reached_twice - end else begin - reached := PTree.set pc true !reached; - traverse_succs (successors_inst @@ get_some @@ PTree.get pc code) - end - and traverse_succs = function - | [] -> () - | [pc] -> traverse pc - | pc :: l -> traverse pc; traverse_succs l - in traverse entry; !reached_twice - (* Does not set the input_regs and liveouts field *) let get_path_map code entry join_points = let visited = ref (PTree.map (fun n i -> false) code) in @@ -92,12 +50,13 @@ let get_path_map code entry join_points = let inst = get_some @@ PTree.get n code in begin psize := !psize + 1; - let successor = match predicted_successor inst with + let psucc = predicted_successor inst in + let successor = match psucc with | None -> None | Some n' -> if get_some @@ PTree.get n' join_points then None else Some n' in match successor with | Some n' -> begin - path_successors := !path_successors @ non_predicted_successors inst; + path_successors := !path_successors @ non_predicted_successors inst psucc; dig_path_rec n' end | None -> Some ({ psize = (Camlcoq.Nat.of_int !psize); diff --git a/scheduling/RTLpathScheduleraux.ml b/scheduling/RTLpathScheduleraux.ml index aeed39df..70a0c507 100644 --- a/scheduling/RTLpathScheduleraux.ml +++ b/scheduling/RTLpathScheduleraux.ml @@ -7,6 +7,7 @@ open RTL open Maps open Registers open ExpansionOracle +open AuxTools let config = Machine.config diff --git a/scheduling/RTLtoBTLaux.ml b/scheduling/RTLtoBTLaux.ml index 9a61f55e..e14e0ab3 100644 --- a/scheduling/RTLtoBTLaux.ml +++ b/scheduling/RTLtoBTLaux.ml @@ -3,62 +3,9 @@ open RTL open BTL open Registers open DebugPrint -open PrintRTL open PrintBTL open Camlcoq - -(* TODO gourdinl duplicated parts from RTLpathLivegenaux.ml - This should be accessible everywhere. *) -let get_some = function - | None -> failwith "Got None instead of Some _" - | Some thing -> thing - -let successors_inst = function - | Inop n - | Iop (_, _, _, n) - | Iload (_, _, _, _, _, n) - | Istore (_, _, _, _, n) - | Icall (_, _, _, _, n) - | Ibuiltin (_, _, _, n) -> - [ n ] - | Icond (_, _, n1, n2, _) -> [ n1; n2 ] - | Ijumptable (_, l) -> l - | Itailcall _ | Ireturn _ -> [] - -let predicted_successor = function - | Inop n | Iop (_, _, _, n) | Iload (_, _, _, _, _, n) | Istore (_, _, _, _, n) - -> - Some n - | Icall (_, _, _, _, n) | Ibuiltin (_, _, _, n) -> None - | Icond (_, _, n1, n2, p) -> ( - match p with Some true -> Some n1 | Some false -> Some n2 | None -> None) - | Ijumptable _ | Itailcall _ | Ireturn _ -> None - -(* TODO gourdinl Adapted from RTLpathLivegenaux to avoid redundant computations ... *) -let non_predicted_successors i = function - | None -> successors_inst i - | Some ps -> List.filter (fun s -> s != ps) (successors_inst i) - -(* adapted from Linearizeaux.get_join_points *) -let get_join_points code entry = - let reached = ref (PTree.map (fun n i -> false) code) in - let reached_twice = ref (PTree.map (fun n i -> false) code) in - let rec traverse pc = - if get_some @@ PTree.get pc !reached then ( - if not (get_some @@ PTree.get pc !reached_twice) then - reached_twice := PTree.set pc true !reached_twice) - else ( - reached := PTree.set pc true !reached; - traverse_succs (successors_inst @@ get_some @@ PTree.get pc code)) - and traverse_succs = function - | [] -> () - | [ pc ] -> traverse pc - | pc :: l -> - traverse pc; - traverse_succs l - in - traverse entry; - !reached_twice +open AuxTools let encaps_final inst osucc = match inst with @@ -94,7 +41,7 @@ let translate_inst inst is_final = let translate_function code entry join_points = let reached = ref (PTree.map (fun n i -> false) code) in let btl_code = ref PTree.empty in - (* SEPARATE IN A BETTER WAY!! *) + (* TODO gourdinl SEPARATE IN A BETTER WAY!! *) let rec build_btl_tree e = if get_some @@ PTree.get e !reached then () else ( @@ -102,9 +49,6 @@ let translate_function code entry join_points = let next_nodes = ref [] in let rec build_btl_block n = let inst = get_some @@ PTree.get n code in - debug "Inst is : "; - print_instruction stderr (0, inst); - debug "\n"; let psucc = predicted_successor inst in let succ = match psucc with @@ -148,7 +92,7 @@ let print_dm dm = (PTree.elements dm) let rtl2btl (f : RTL.coq_function) = - (*debug_flag := true;*) + debug_flag := true; let code = f.fn_code in let entry = f.fn_entrypoint in let join_points = get_join_points code entry in @@ -157,12 +101,12 @@ let rtl2btl (f : RTL.coq_function) = debug "Entry %d\n" (P.to_int entry); debug "RTL Code: "; print_code code; + debug_flag := false; debug "BTL Code: "; print_btl_code stderr btl true; - debug "BTL Dupmap:\n"; - print_dm dm; + debug "Dupmap:\n"; + print_ptree print_pint dm; debug "Join points: "; print_true_nodes join_points; debug "\n"; - debug_flag := false; ((btl, entry), dm) -- cgit