diff options
| -rw-r--r-- | scheduling/BTL.v | 82 | ||||
| -rw-r--r-- | scheduling/PrintBTL.ml | 107 | ||||
| -rw-r--r-- | scheduling/RTLtoBTLaux.ml | 161 |
3 files changed, 253 insertions, 97 deletions
diff --git a/scheduling/BTL.v b/scheduling/BTL.v index 9fdf39be..3daa40c4 100644 --- a/scheduling/BTL.v +++ b/scheduling/BTL.v @@ -529,13 +529,13 @@ Fixpoint verify_block (dupmap: PTree.t node) cfg isfst pc ib : res (option node) do u <- verify_is_copy dupmap pc1 pc; if negb isfst then OK None - else Error (msg "verify_block: isfst is true Bgoto") + else Error (msg "BTL.verify_block: isfst is true Bgoto") | Breturn or => match cfg!pc with | Some (Ireturn or') => if option_eq Pos.eq_dec or or' then OK None - else Error (msg "verify_block: different opt reg in Breturn") - | _ => Error (msg "verify_block: incorrect cfg Breturn") + else Error (msg "BTL.verify_block: different opt reg in Breturn") + | _ => Error (msg "BTL.verify_block: incorrect cfg Breturn") end | Bcall s ri lr r pc1 => match cfg!pc with @@ -545,11 +545,11 @@ Fixpoint verify_block (dupmap: PTree.t node) cfg isfst pc ib : res (option node) if (product_eq Pos.eq_dec ident_eq ri ri') then if (list_eq_dec Pos.eq_dec lr lr') then if (Pos.eq_dec r r') then OK None - else Error (msg "verify_block: different r r' in Bcall") - else Error (msg "verify_block: different lr in Bcall") - else Error (msg "verify_block: different ri in Bcall") - else Error (msg "verify_block: different signatures in Bcall") - | _ => Error (msg "verify_block: incorrect cfg Bcall") + else Error (msg "BTL.verify_block: different r r' in Bcall") + else Error (msg "BTL.verify_block: different lr in Bcall") + else Error (msg "BTL.verify_block: different ri in Bcall") + else Error (msg "BTL.verify_block: different signatures in Bcall") + | _ => Error (msg "BTL.verify_block: incorrect cfg Bcall") end | Btailcall s ri lr => match cfg!pc with @@ -557,10 +557,10 @@ Fixpoint verify_block (dupmap: PTree.t node) cfg isfst pc ib : res (option node) if (signature_eq s s') then if (product_eq Pos.eq_dec ident_eq ri ri') then if (list_eq_dec Pos.eq_dec lr lr') then OK None - else Error (msg "verify_block: different lr in Btailcall") - else Error (msg "verify_block: different ri in Btailcall") - else Error (msg "verify_block: different signatures in Btailcall") - | _ => Error (msg "verify_block: incorrect cfg Btailcall") + else Error (msg "BTL.verify_block: different lr in Btailcall") + else Error (msg "BTL.verify_block: different ri in Btailcall") + else Error (msg "BTL.verify_block: different signatures in Btailcall") + | _ => Error (msg "BTL.verify_block: incorrect cfg Btailcall") end | Bbuiltin ef la br pc1 => match cfg!pc with @@ -569,24 +569,24 @@ Fixpoint verify_block (dupmap: PTree.t node) cfg isfst pc ib : res (option node) if (external_function_eq ef ef') then if (list_eq_dec builtin_arg_eq_pos la la') then if (builtin_res_eq_pos br br') then OK None - else Error (msg "verify_block: different brr in Bbuiltin") - else Error (msg "verify_block: different lbar in Bbuiltin") - else Error (msg "verify_block: different ef in Bbuiltin") - | _ => Error (msg "verify_block: incorrect cfg Bbuiltin") + else Error (msg "BTL.verify_block: different brr in Bbuiltin") + else Error (msg "BTL.verify_block: different lbar in Bbuiltin") + else Error (msg "BTL.verify_block: different ef in Bbuiltin") + | _ => Error (msg "BTL.verify_block: incorrect cfg Bbuiltin") end | Bjumptable r ln => match cfg!pc with | Some (Ijumptable r' ln') => do u <- verify_is_copy_list dupmap ln ln'; if (Pos.eq_dec r r') then OK None - else Error (msg "verify_block: different r in Bjumptable") - | _ => Error (msg "verify_block: incorrect cfg Bjumptable") + else Error (msg "BTL.verify_block: different r in Bjumptable") + | _ => Error (msg "BTL.verify_block: incorrect cfg Bjumptable") end end | Bnop => match cfg!pc with | Some (Inop pc') => OK (Some pc') - | _ => Error (msg "verify_block: incorrect cfg Bnop") + | _ => Error (msg "BTL.verify_block: incorrect cfg Bnop") end | Bop op lr r => match cfg!pc with @@ -595,10 +595,10 @@ Fixpoint verify_block (dupmap: PTree.t node) cfg isfst pc ib : res (option node) if (list_eq_dec Pos.eq_dec lr lr') then if (Pos.eq_dec r r') then OK (Some pc') - else Error (msg "verify_block: different r in Bop") - else Error (msg "verify_block: different lr in Bop") - else Error (msg "verify_block: different operations in Bop") - | _ => Error (msg "verify_block: incorrect cfg Bop") + else Error (msg "BTL.verify_block: different r in Bop") + else Error (msg "BTL.verify_block: different lr in Bop") + else Error (msg "BTL.verify_block: different operations in Bop") + | _ => Error (msg "BTL.verify_block: incorrect cfg Bop") end | Bload tm m a lr r => match cfg!pc with @@ -609,12 +609,12 @@ Fixpoint verify_block (dupmap: PTree.t node) cfg isfst pc ib : res (option node) if (list_eq_dec Pos.eq_dec lr lr') then if (Pos.eq_dec r r') then OK (Some pc') - else Error (msg "verify_block: different r in Bload") - else Error (msg "verify_block: different lr in Bload") - else Error (msg "verify_block: different addressing in Bload") - else Error (msg "verify_block: different mchunk in Bload") - else Error (msg "verify_block: NOTRAP trapping_mode unsupported in Bload") - | _ => Error (msg "verify_block: incorrect cfg Bload") + else Error (msg "BTL.verify_block: different r in Bload") + else Error (msg "BTL.verify_block: different lr in Bload") + else Error (msg "BTL.verify_block: different addressing in Bload") + else Error (msg "BTL.verify_block: different mchunk in Bload") + else Error (msg "BTL.verify_block: NOTRAP trapping_mode unsupported in Bload") + | _ => Error (msg "BTL.verify_block: incorrect cfg Bload") end | Bstore m a lr r => match cfg!pc with @@ -623,18 +623,18 @@ Fixpoint verify_block (dupmap: PTree.t node) cfg isfst pc ib : res (option node) if (eq_addressing a a') then if (list_eq_dec Pos.eq_dec lr lr') then if (Pos.eq_dec r r') then OK (Some pc') - else Error (msg "verify_block: different r in Bstore") - else Error (msg "verify_block: different lr in Bstore") - else Error (msg "verify_block: different addressing in Bstore") - else Error (msg "verify_block: different mchunk in Bstore") - | _ => Error (msg "verify_block: incorrect cfg Bstore") + else Error (msg "BTL.verify_block: different r in Bstore") + else Error (msg "BTL.verify_block: different lr in Bstore") + else Error (msg "BTL.verify_block: different addressing in Bstore") + else Error (msg "BTL.verify_block: different mchunk in Bstore") + | _ => Error (msg "BTL.verify_block: incorrect cfg Bstore") end | Bseq b1 b2 => do opc <- verify_block dupmap cfg isfst pc b1; match opc with | Some pc' => verify_block dupmap cfg false pc' b2 - | None => Error (msg "verify_block: None next pc in Bseq (deadcode)") + | None => Error (msg "BTL.verify_block: None next pc in Bseq (deadcode)") end | Bcond c lr bso bnot i => match cfg!pc with @@ -648,11 +648,11 @@ Fixpoint verify_block (dupmap: PTree.t node) cfg isfst pc ib : res (option node) | o, None => OK o | Some x, Some x' => if Pos.eq_dec x x' then OK (Some x) - else Error (msg "verify_block: is_join_opt incorrect for Bcond") + else Error (msg "BTL.verify_block: is_join_opt incorrect for Bcond") end - else Error (msg "verify_block: incompatible conditions in Bcond") - else Error (msg "verify_block: different lr in Bcond") - | _ => Error (msg "verify_block: incorrect cfg Bcond") + else Error (msg "BTL.verify_block: incompatible conditions in Bcond") + else Error (msg "BTL.verify_block: different lr in Bcond") + | _ => Error (msg "BTL.verify_block: incorrect cfg Bcond") end end. @@ -753,9 +753,9 @@ Fixpoint verify_blocks dupmap (cfg: code) (cfg':RTL.code) l: res unit := | Some ib => do o <- verify_block dupmap cfg' true pc' ib.(entry); match o with | None => verify_blocks dupmap cfg cfg' l - | _ => Error(msg "verify_blocks.end") + | _ => Error(msg "BTL.verify_blocks.end") end - | _ => Error(msg "verify_blocks.entry") + | _ => Error(msg "BTL.verify_blocks.entry") end end. diff --git a/scheduling/PrintBTL.ml b/scheduling/PrintBTL.ml new file mode 100644 index 00000000..8f61380e --- /dev/null +++ b/scheduling/PrintBTL.ml @@ -0,0 +1,107 @@ +open Printf +open Camlcoq +open Datatypes +open Maps +open AST +open BTL +open PrintAST + +(* Printing of BTL code *) + +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_succ pp s = + fprintf pp "\tsucc %d\n" (P.to_int s) + +let rec print_iblock pp is_rec pref ib = + fprintf pp "%s" pref; + match ib with + | Bnop -> + fprintf pp "Bnop\n" + | Bop(op, args, res) -> + fprintf pp "Bop: %a = %a\n" + reg res (PrintOp.print_operation reg) (op, args) + | Bload(trap, chunk, addr, args, dst) -> + 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) -> + 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)) -> + fprintf pp "Bcall: %a = %a(%a)\n" + reg res ros fn regs args; + print_succ pp s + | BF (Btailcall(sg, fn, args)) -> + fprintf pp "Btailcall: %a(%a)\n" + ros fn regs args + | BF (Bbuiltin(ef, args, res, s)) -> + 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) -> + fprintf pp "Bcond: (%a) (prediction: %s)\n" + (PrintOp.print_condition reg) (cond, args) + (match info with None -> "none" | Some true -> "branch" | Some false -> "fallthrough"); + let pref' = pref ^ " " in + fprintf pp "%sifso = [\n" pref; + if is_rec then print_iblock pp is_rec pref' ib1 else fprintf pp "...\n"; + fprintf pp "%s]\n" pref; + fprintf pp "%sifnot = [\n" pref; + if is_rec then print_iblock pp is_rec pref' ib2 else fprintf pp "...\n"; + fprintf pp "%s]\n" pref + | BF (Bjumptable(arg, tbl)) -> + let tbl = Array.of_list tbl in + 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) -> + fprintf pp "Breturn\n" + | BF (Breturn (Some arg)) -> + fprintf pp "Breturn: %a\n" reg arg + | BF (Bgoto s) -> + fprintf pp "Bgoto: %d\n" (P.to_int s) + | Bseq (ib1, ib2) -> + if is_rec then ( + print_iblock pp is_rec pref ib1; + print_iblock pp is_rec pref ib2) + else fprintf pp "Bseq...\n" + +let print_btl_code pp btl is_rec = + fprintf pp "\n"; + List.iter (fun (n,ibf) -> + fprintf pp "[BTL block %d]\n" (P.to_int n); + print_iblock pp is_rec " " ibf.entry; + fprintf pp "\n") + (PTree.elements btl); + fprintf pp "\n" + +let print_function pp id f = + fprintf pp "%s(%a) {\n" (extern_atom id) regs f.fn_params; + let instrs = List.map (fun (n,i) -> i.entry) (PTree.elements f.fn_code) in + List.iter (print_iblock pp true "") instrs; + fprintf pp "}\n\n" + +let print_globdef pp (id, gd) = + match gd with + | Gfun(Internal f) -> print_function pp id f + | _ -> () + +let print_program pp (prog: BTL.program) = + List.iter (print_globdef pp) prog.prog_defs diff --git a/scheduling/RTLtoBTLaux.ml b/scheduling/RTLtoBTLaux.ml index 20aa01aa..3c9b7644 100644 --- a/scheduling/RTLtoBTLaux.ml +++ b/scheduling/RTLtoBTLaux.ml @@ -3,28 +3,35 @@ open RTL open BTL open Registers open DebugPrint +open PrintRTL +open PrintBTL (* 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 + | 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 _ -> [] + | 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 + | 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 @@ -36,83 +43,125 @@ 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 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 - end else begin + 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) - end + 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 + | [ pc ] -> traverse pc + | pc :: l -> + traverse pc; + traverse_succs l + in + traverse entry; + !reached_twice + +let encaps_final inst osucc = + match inst with + | BF _ | Bcond _ -> inst + | _ -> Bseq (inst, BF (Bgoto (get_some @@ osucc))) -let translate_inst = function - | Inop (_) -> Bnop - | Iop (op,lr,rd,_) -> Bop (op,lr,rd) - | Iload (trap,chk,addr,lr,rd,_) -> Bload (trap,chk,addr,lr,rd) - | Istore (chk,addr,lr,rd,_) -> Bstore (chk,addr,lr,rd) - | Icall (sign,fn,lr,rd,s) -> BF (Bcall (sign,fn,lr,rd,s)) - | Itailcall (sign,fn,lr) -> BF (Btailcall (sign,fn,lr)) - | Ibuiltin (ef,lr,rd,s) -> BF (Bbuiltin (ef,lr,rd,s)) - | Icond (cond,lr,ifso,ifnot,info) -> ( +let translate_inst inst is_final = + let osucc = ref None in + let btli = + match inst with + | Inop s -> + osucc := Some s; + Bnop + | Iop (op, lr, rd, s) -> + osucc := Some s; + Bop (op, lr, rd) + | Iload (trap, chk, addr, lr, rd, s) -> + osucc := Some s; + Bload (trap, chk, addr, lr, rd) + | Istore (chk, addr, lr, rd, s) -> + osucc := Some s; + Bstore (chk, addr, lr, rd) + | Icall (sign, fn, lr, rd, s) -> BF (Bcall (sign, fn, lr, rd, s)) + | Itailcall (sign, fn, lr) -> BF (Btailcall (sign, fn, lr)) + | Ibuiltin (ef, lr, rd, s) -> BF (Bbuiltin (ef, lr, rd, s)) + | Icond (cond, lr, ifso, ifnot, info) -> (* TODO gourdinl remove this *) assert (info = None); - Bcond (cond,lr,BF (Bgoto(ifso)),BF (Bgoto(ifnot)),info)) - | Ijumptable (arg, tbl) -> BF (Bjumptable (arg,tbl)) - | Ireturn (oreg) -> BF (Breturn (oreg)) + Bcond (cond, lr, BF (Bgoto ifso), BF (Bgoto ifnot), info) + | Ijumptable (arg, tbl) -> BF (Bjumptable (arg, tbl)) + | Ireturn oreg -> BF (Breturn oreg) + in + if is_final then encaps_final btli !osucc else btli 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!! *) let rec build_btl_tree e = - if (get_some @@ PTree.get e !reached) then () + if get_some @@ PTree.get e !reached then () else ( reached := PTree.set e true !reached; 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 - | Some ps -> if get_some @@ PTree.get ps join_points then None else Some ps - | None -> None - in match succ with + match psucc with + | Some ps -> + if get_some @@ PTree.get ps join_points then ( + debug "IS JOIN PT\n"; + None) + else Some ps + | None -> None + in + match succ with | Some s -> ( - match inst with - | Icond (cond,lr,ifso,ifnot,info) -> ( - (* TODO gourdinl remove this *) - assert (s = ifso || s = ifnot); - next_nodes := !next_nodes @ non_predicted_successors inst psucc; - if s = ifso then - Bcond (cond,lr,build_btl_block s,BF (Bgoto (ifnot)),info) - else - Bcond (cond,lr,BF (Bgoto (ifso)),build_btl_block s,info)) - | _ -> Bseq (translate_inst inst, build_btl_block s)) - | None -> ( + debug "BLOCK CONTINUE\n"; + match inst with + | Icond (cond, lr, ifso, ifnot, info) -> + (* TODO gourdinl remove this *) + assert (s = ifnot); + next_nodes := !next_nodes @ non_predicted_successors inst psucc; + Bcond (cond, lr, BF (Bgoto ifso), build_btl_block s, info) + | _ -> Bseq (translate_inst inst false, build_btl_block s)) + | None -> + debug "BLOCK END.\n"; next_nodes := !next_nodes @ successors_inst inst; - translate_inst inst) + translate_inst inst true in let ib = build_btl_block e in let succs = !next_nodes in let ibf = { entry = ib; input_regs = Regset.empty } in btl_code := PTree.set e ibf !btl_code; List.iter build_btl_tree succs) - in build_btl_tree entry; !btl_code + in + build_btl_tree entry; + !btl_code + +(*let print_dm dm =*) + (*List.iter (fun (n,ib) ->*) + (*debug "%d:" (P.to_int n);*) + (*print_iblock stderr false ib.entry)*) + (*(PTree.elements dm)*) + -let rtl2btl (f: RTL.coq_function) = + +let rtl2btl (f : RTL.coq_function) = + debug_flag := true; let code = f.fn_code in let entry = f.fn_entrypoint in let join_points = get_join_points code entry in let btl = translate_function code entry join_points in - debug_flag := true; - debug"Code: "; + let dm = PTree.map (fun n i -> n) btl in + debug "RTL Code: "; print_code code; + debug "BTL Code: "; + print_btl_code stderr btl true; debug "Join points: "; print_true_nodes join_points; debug "\n"; + (*print_dm dm;*) debug_flag := false; - ((btl, entry), PTree.empty) + ((btl, entry), dm) |