From c27d87ffe33242840964dd9bd67090409eea79a5 Mon Sep 17 00:00:00 2001 From: Léo Gourdin Date: Tue, 18 May 2021 16:55:56 +0200 Subject: oracle simplification, BTL printer, and error msg spec --- scheduling/RTLtoBTLaux.ml | 161 ++++++++++++++++++++++++++++++---------------- 1 file changed, 105 insertions(+), 56 deletions(-) (limited to 'scheduling/RTLtoBTLaux.ml') 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) -- cgit