From 97c9a374620a1a74116aefe09f175ae964419e6a Mon Sep 17 00:00:00 2001 From: Léo Gourdin Date: Tue, 18 May 2021 19:42:31 +0200 Subject: debug prints uniformized --- riscV/ExpansionOracle.ml | 135 +++++++++++++++++++++++------------------------ 1 file changed, 66 insertions(+), 69 deletions(-) (limited to 'riscV') diff --git a/riscV/ExpansionOracle.ml b/riscV/ExpansionOracle.ml index 4f67b9af..5d739375 100644 --- a/riscV/ExpansionOracle.ml +++ b/riscV/ExpansionOracle.ml @@ -22,13 +22,11 @@ open! Integers open Camlcoq open Option open AST -open Printf +open DebugPrint (** Mini CSE (a dynamic numbering is applied during expansion. The CSE algorithm is inspired by the "static" one used in backend/CSE.v *) -let exp_debug = false - (** Managing virtual registers and node index *) let reg = ref 1 @@ -80,9 +78,9 @@ type numb = { } let print_list_pos l = - if exp_debug then eprintf "["; - List.iter (fun i -> if exp_debug then eprintf "%d;" (p2i i)) l; - if exp_debug then eprintf "]\n" + debug "["; + List.iter (fun i -> debug "%d;" (p2i i)) l; + debug "]\n" let empty_numbering () = { nnext = 1; seqs = []; nreg = Hashtbl.create 100; nval = Hashtbl.create 100 } @@ -93,11 +91,11 @@ let rec get_nvalues vn = function let v = match Hashtbl.find_opt !vn.nreg r with | Some v -> - if exp_debug then eprintf "getnval r=%d |-> v=%d\n" (p2i r) v; + debug "getnval r=%d |-> v=%d\n" (p2i r) v; v | None -> let n = !vn.nnext in - if exp_debug then eprintf "getnval r=%d |-> v=%d\n" (p2i r) n; + debug "getnval r=%d |-> v=%d\n" (p2i r) n; !vn.nnext <- !vn.nnext + 1; Hashtbl.replace !vn.nreg r n; Hashtbl.replace !vn.nval n [ r ]; @@ -112,17 +110,17 @@ let get_nval_ornil vn v = let forget_reg vn rd = match Hashtbl.find_opt !vn.nreg rd with | Some v -> - if exp_debug then eprintf "forget_reg: r=%d |-> v=%d\n" (p2i rd) v; + debug "forget_reg: r=%d |-> v=%d\n" (p2i rd) v; let old_regs = get_nval_ornil vn v in - if exp_debug then eprintf "forget_reg: old_regs are:\n"; + debug "forget_reg: old_regs are:\n"; print_list_pos old_regs; Hashtbl.replace !vn.nval v (List.filter (fun n -> not (P.eq n rd)) old_regs) | None -> - if exp_debug then eprintf "forget_reg: no mapping for r=%d\n" (p2i rd) + debug "forget_reg: no mapping for r=%d\n" (p2i rd) let update_reg vn rd v = - if exp_debug then eprintf "update_reg: update v=%d with r=%d\n" v (p2i rd); + debug "update_reg: update v=%d with r=%d\n" v (p2i rd); forget_reg vn rd; let old_regs = get_nval_ornil vn v in Hashtbl.replace !vn.nval v (rd :: old_regs) @@ -132,7 +130,7 @@ let rec find_valnum_rhs rh = function | Seq (v, rh') :: tl -> if rh = rh' then Some v else find_valnum_rhs rh tl let set_unknown vn rd = - if exp_debug then eprintf "set_unknown: rd=%d\n" (p2i rd); + debug "set_unknown: rd=%d\n" (p2i rd); forget_reg vn rd; Hashtbl.remove !vn.nreg rd @@ -141,19 +139,19 @@ let set_res_unknown vn res = match res with BR r -> set_unknown vn r | _ -> () let addrhs vn rd rh = match find_valnum_rhs rh !vn.seqs with | Some vres -> - if exp_debug then eprintf "addrhs: Some v=%d\n" vres; + debug "addrhs: Some v=%d\n" vres; Hashtbl.replace !vn.nreg rd vres; update_reg vn rd vres | None -> let n = !vn.nnext in - if exp_debug then eprintf "addrhs: None v=%d\n" n; + debug "addrhs: None v=%d\n" n; !vn.nnext <- !vn.nnext + 1; !vn.seqs <- Seq (n, rh) :: !vn.seqs; update_reg vn rd n; Hashtbl.replace !vn.nreg rd n let addsop vn v op rd = - if exp_debug then eprintf "addsop\n"; + debug "addsop\n"; if op = Omove then ( update_reg vn rd (List.hd v); Hashtbl.replace !vn.nreg rd (List.hd v)) @@ -167,11 +165,11 @@ let rec kill_mem_operations = function | eq :: tl -> eq :: kill_mem_operations tl let reg_valnum vn v = - if exp_debug then eprintf "reg_valnum: trying to find a mapping for v=%d\n" v; + debug "reg_valnum: trying to find a mapping for v=%d\n" v; match Hashtbl.find !vn.nval v with | [] -> None | r :: rs -> - if exp_debug then eprintf "reg_valnum: found a mapping r=%d\n" (p2i r); + debug "reg_valnum: found a mapping r=%d\n" (p2i r); Some r let rec reg_valnums vn = function @@ -216,7 +214,7 @@ let addinst vn op args rd = let rh = Sop (op, v) in match find_rhs vn rh with | Some r -> - if exp_debug then eprintf "addinst: rhs found with r=%d\n" (p2i r); + debug "addinst: rhs found with r=%d\n" (p2i r); Sr r | None -> addsop vn v op rd; @@ -627,8 +625,7 @@ let get_regs_inst = function (** Modify pathmap according to the size of the expansion list *) let write_pathmap initial esize pm' = - if exp_debug then - eprintf "write_pathmap: initial=%d, esize=%d\n" (p2i initial) esize; + debug "write_pathmap: initial=%d, esize=%d\n" (p2i initial) esize; let path = get_some @@ PTree.get initial !pm' in let npsize = Camlcoq.Nat.of_int (esize + Camlcoq.Nat.to_int path.psize) in let path' = @@ -655,7 +652,7 @@ let get_arguments vn vals args = (** Update the code tree with the expansion list *) let rec write_tree vn exp initial current code' new_order fturn = - if exp_debug then eprintf "wt: node is %d\n" !node; + debug "wt: node is %d\n" !node; let target_node, next_node = if fturn then (P.to_int initial, current) else (current, current - 1) in @@ -685,7 +682,7 @@ let rec write_tree vn exp initial current code' new_order fturn = (** Main expansion function - TODO gourdinl to split? *) let expanse (sb : superblock) code pm = - if exp_debug then eprintf "#### New superblock for expansion oracle\n"; + debug "#### New superblock for expansion oracle\n"; let new_order = ref [] in let liveins = ref sb.liveins in let exp = ref [] in @@ -699,129 +696,129 @@ let expanse (sb : superblock) code pm = was_branch := false; was_exp := false; let inst = get_some @@ PTree.get n code in - if exp_debug then eprintf "We are checking node %d\n" (p2i n); + debug "We are checking node %d\n" (p2i n); (match inst with (* Expansion of conditions - Ocmp *) | Iop (Ocmp (Ccomp c), a1 :: a2 :: nil, dest, succ) -> - if exp_debug then eprintf "Iop/Ccomp\n"; + debug "Iop/Ccomp\n"; exp := cond_int32s vn false c a1 a2 dest; exp := extract_final vn !exp dest succ; was_exp := true | Iop (Ocmp (Ccompu c), a1 :: a2 :: nil, dest, succ) -> - if exp_debug then eprintf "Iop/Ccompu\n"; + debug "Iop/Ccompu\n"; exp := cond_int32u vn false c a1 a2 dest; exp := extract_final vn !exp dest succ; was_exp := true | Iop (Ocmp (Ccompimm (c, imm)), a1 :: nil, dest, succ) -> - if exp_debug then eprintf "Iop/Ccompimm\n"; + debug "Iop/Ccompimm\n"; exp := expanse_condimm_int32s vn c a1 imm dest; exp := extract_final vn !exp dest succ; was_exp := true | Iop (Ocmp (Ccompuimm (c, imm)), a1 :: nil, dest, succ) -> - if exp_debug then eprintf "Iop/Ccompuimm\n"; + debug "Iop/Ccompuimm\n"; exp := expanse_condimm_int32u vn c a1 imm dest; exp := extract_final vn !exp dest succ; was_exp := true | Iop (Ocmp (Ccompl c), a1 :: a2 :: nil, dest, succ) -> - if exp_debug then eprintf "Iop/Ccompl\n"; + debug "Iop/Ccompl\n"; exp := cond_int64s vn false c a1 a2 dest; exp := extract_final vn !exp dest succ; was_exp := true | Iop (Ocmp (Ccomplu c), a1 :: a2 :: nil, dest, succ) -> - if exp_debug then eprintf "Iop/Ccomplu\n"; + debug "Iop/Ccomplu\n"; exp := cond_int64u vn false c a1 a2 dest; exp := extract_final vn !exp dest succ; was_exp := true | Iop (Ocmp (Ccomplimm (c, imm)), a1 :: nil, dest, succ) -> - if exp_debug then eprintf "Iop/Ccomplimm\n"; + debug "Iop/Ccomplimm\n"; exp := expanse_condimm_int64s vn c a1 imm dest; exp := extract_final vn !exp dest succ; was_exp := true | Iop (Ocmp (Ccompluimm (c, imm)), a1 :: nil, dest, succ) -> - if exp_debug then eprintf "Iop/Ccompluimm\n"; + debug "Iop/Ccompluimm\n"; exp := expanse_condimm_int64u vn c a1 imm dest; exp := extract_final vn !exp dest succ; was_exp := true | Iop (Ocmp (Ccompf c), f1 :: f2 :: nil, dest, succ) -> - if exp_debug then eprintf "Iop/Ccompf\n"; + debug "Iop/Ccompf\n"; exp := expanse_cond_fp vn false cond_float c f1 f2 dest; exp := extract_final vn !exp dest succ; was_exp := true | Iop (Ocmp (Cnotcompf c), f1 :: f2 :: nil, dest, succ) -> - if exp_debug then eprintf "Iop/Cnotcompf\n"; + debug "Iop/Cnotcompf\n"; exp := expanse_cond_fp vn true cond_float c f1 f2 dest; exp := extract_final vn !exp dest succ; was_exp := true | Iop (Ocmp (Ccompfs c), f1 :: f2 :: nil, dest, succ) -> - if exp_debug then eprintf "Iop/Ccompfs\n"; + debug "Iop/Ccompfs\n"; exp := expanse_cond_fp vn false cond_single c f1 f2 dest; exp := extract_final vn !exp dest succ; was_exp := true | Iop (Ocmp (Cnotcompfs c), f1 :: f2 :: nil, dest, succ) -> - if exp_debug then eprintf "Iop/Cnotcompfs\n"; + debug "Iop/Cnotcompfs\n"; exp := expanse_cond_fp vn true cond_single c f1 f2 dest; exp := extract_final vn !exp dest succ; was_exp := true (* Expansion of branches - Ccomp *) | Icond (Ccomp c, a1 :: a2 :: nil, succ1, succ2, info) -> - if exp_debug then eprintf "Icond/Ccomp\n"; + debug "Icond/Ccomp\n"; exp := cbranch_int32s false c a1 a2 info succ1 succ2 []; was_branch := true; was_exp := true | Icond (Ccompu c, a1 :: a2 :: nil, succ1, succ2, info) -> - if exp_debug then eprintf "Icond/Ccompu\n"; + debug "Icond/Ccompu\n"; exp := cbranch_int32u false c a1 a2 info succ1 succ2 []; was_branch := true; was_exp := true | Icond (Ccompimm (c, imm), a1 :: nil, succ1, succ2, info) -> - if exp_debug then eprintf "Icond/Ccompimm\n"; + debug "Icond/Ccompimm\n"; exp := expanse_cbranchimm_int32s vn c a1 imm info succ1 succ2; was_branch := true; was_exp := true | Icond (Ccompuimm (c, imm), a1 :: nil, succ1, succ2, info) -> - if exp_debug then eprintf "Icond/Ccompuimm\n"; + debug "Icond/Ccompuimm\n"; exp := expanse_cbranchimm_int32u vn c a1 imm info succ1 succ2; was_branch := true; was_exp := true | Icond (Ccompl c, a1 :: a2 :: nil, succ1, succ2, info) -> - if exp_debug then eprintf "Icond/Ccompl\n"; + debug "Icond/Ccompl\n"; exp := cbranch_int64s false c a1 a2 info succ1 succ2 []; was_branch := true; was_exp := true | Icond (Ccomplu c, a1 :: a2 :: nil, succ1, succ2, info) -> - if exp_debug then eprintf "Icond/Ccomplu\n"; + debug "Icond/Ccomplu\n"; exp := cbranch_int64u false c a1 a2 info succ1 succ2 []; was_branch := true; was_exp := true | Icond (Ccomplimm (c, imm), a1 :: nil, succ1, succ2, info) -> - if exp_debug then eprintf "Icond/Ccomplimm\n"; + debug "Icond/Ccomplimm\n"; exp := expanse_cbranchimm_int64s vn c a1 imm info succ1 succ2; was_branch := true; was_exp := true | Icond (Ccompluimm (c, imm), a1 :: nil, succ1, succ2, info) -> - if exp_debug then eprintf "Icond/Ccompluimm\n"; + debug "Icond/Ccompluimm\n"; exp := expanse_cbranchimm_int64u vn c a1 imm info succ1 succ2; was_branch := true; was_exp := true | Icond (Ccompf c, f1 :: f2 :: nil, succ1, succ2, info) -> - if exp_debug then eprintf "Icond/Ccompf\n"; + debug "Icond/Ccompf\n"; exp := expanse_cbranch_fp vn false cond_float c f1 f2 info succ1 succ2; was_branch := true; was_exp := true | Icond (Cnotcompf c, f1 :: f2 :: nil, succ1, succ2, info) -> - if exp_debug then eprintf "Icond/Cnotcompf\n"; + debug "Icond/Cnotcompf\n"; exp := expanse_cbranch_fp vn true cond_float c f1 f2 info succ1 succ2; was_branch := true; was_exp := true | Icond (Ccompfs c, f1 :: f2 :: nil, succ1, succ2, info) -> - if exp_debug then eprintf "Icond/Ccompfs\n"; + debug "Icond/Ccompfs\n"; exp := expanse_cbranch_fp vn false cond_single c f1 f2 info succ1 succ2; was_branch := true; was_exp := true | Icond (Cnotcompfs c, f1 :: f2 :: nil, succ1, succ2, info) -> - if exp_debug then eprintf "Icond/Cnotcompfs\n"; + debug "Icond/Cnotcompfs\n"; exp := expanse_cbranch_fp vn true cond_single c f1 f2 info succ1 succ2; was_branch := true; @@ -830,7 +827,7 @@ let expanse (sb : superblock) code pm = (if not !was_exp then match inst with | Iop (Ofloatconst f, nil, dest, succ) -> - if exp_debug then eprintf "Iop/Ofloatconst\n"; + debug "Iop/Ofloatconst\n"; let r = r2pi () in let l = loadimm64 vn r (Floats.Float.to_bits f) in let r', l' = extract_arg l in @@ -838,7 +835,7 @@ let expanse (sb : superblock) code pm = exp := extract_final vn !exp dest succ; was_exp := true | Iop (Osingleconst f, nil, dest, succ) -> - if exp_debug then eprintf "Iop/Osingleconst\n"; + debug "Iop/Osingleconst\n"; let r = r2pi () in let l = loadimm32 vn r (Floats.Float32.to_bits f) in let r', l' = extract_arg l in @@ -846,57 +843,57 @@ let expanse (sb : superblock) code pm = exp := extract_final vn !exp dest succ; was_exp := true | Iop (Ointconst n, nil, dest, succ) -> - if exp_debug then eprintf "Iop/Ointconst\n"; + debug "Iop/Ointconst\n"; exp := loadimm32 vn dest n; exp := extract_final vn !exp dest succ; was_exp := true | Iop (Olongconst n, nil, dest, succ) -> - if exp_debug then eprintf "Iop/Olongconst\n"; + debug "Iop/Olongconst\n"; exp := loadimm64 vn dest n; exp := extract_final vn !exp dest succ; was_exp := true | Iop (Oaddimm n, a1 :: nil, dest, succ) -> - if exp_debug then eprintf "Iop/Oaddimm\n"; + debug "Iop/Oaddimm\n"; exp := addimm32 vn a1 dest n None; exp := extract_final vn !exp dest succ; was_exp := true | Iop (Oaddlimm n, a1 :: nil, dest, succ) -> - if exp_debug then eprintf "Iop/Oaddlimm\n"; + debug "Iop/Oaddlimm\n"; exp := addimm64 vn a1 dest n None; exp := extract_final vn !exp dest succ; was_exp := true | Iop (Oandimm n, a1 :: nil, dest, succ) -> - if exp_debug then eprintf "Iop/Oandimm\n"; + debug "Iop/Oandimm\n"; exp := andimm32 vn a1 dest n; exp := extract_final vn !exp dest succ; was_exp := true | Iop (Oandlimm n, a1 :: nil, dest, succ) -> - if exp_debug then eprintf "Iop/Oandlimm\n"; + debug "Iop/Oandlimm\n"; exp := andimm64 vn a1 dest n; exp := extract_final vn !exp dest succ; was_exp := true | Iop (Oorimm n, a1 :: nil, dest, succ) -> - if exp_debug then eprintf "Iop/Oorimm\n"; + debug "Iop/Oorimm\n"; exp := orimm32 vn a1 dest n; exp := extract_final vn !exp dest succ; was_exp := true | Iop (Oorlimm n, a1 :: nil, dest, succ) -> - if exp_debug then eprintf "Iop/Oorlimm\n"; + debug "Iop/Oorlimm\n"; exp := orimm64 vn a1 dest n; exp := extract_final vn !exp dest succ; was_exp := true | Iop (Oxorimm n, a1 :: nil, dest, succ) -> - if exp_debug then eprintf "Iop/Oxorimm\n"; + debug "Iop/Oxorimm\n"; exp := xorimm32 vn a1 dest n; exp := extract_final vn !exp dest succ; was_exp := true | Iop (Oxorlimm n, a1 :: nil, dest, succ) -> - if exp_debug then eprintf "Iop/Oxorlimm\n"; + debug "Iop/Oxorlimm\n"; exp := xorimm64 vn a1 dest n; exp := extract_final vn !exp dest succ; was_exp := true | Iop (Ocast8signed, a1 :: nil, dest, succ) -> - if exp_debug then eprintf "Iop/cast8signed\n"; + debug "Iop/cast8signed\n"; let op = Oshlimm (Int.repr (Z.of_sint 24)) in let r = r2pi () in let i1 = addinst vn op [ a1 ] r in @@ -906,7 +903,7 @@ let expanse (sb : superblock) code pm = exp := extract_final vn !exp dest succ; was_exp := true | Iop (Ocast16signed, a1 :: nil, dest, succ) -> - if exp_debug then eprintf "Iop/cast16signed\n"; + debug "Iop/cast16signed\n"; let op = Oshlimm (Int.repr (Z.of_sint 16)) in let r = r2pi () in let i1 = addinst vn op [ a1 ] r in @@ -916,7 +913,7 @@ let expanse (sb : superblock) code pm = exp := extract_final vn !exp dest succ; was_exp := true | Iop (Ocast32unsigned, a1 :: nil, dest, succ) -> - if exp_debug then eprintf "Iop/Ocast32unsigned\n"; + debug "Iop/Ocast32unsigned\n"; let r1 = r2pi () in let r2 = r2pi () in let op1 = Ocast32signed in @@ -933,10 +930,10 @@ let expanse (sb : superblock) code pm = was_exp := true | Iop (Oshrximm n, a1 :: nil, dest, succ) -> if Int.eq n Int.zero then ( - if exp_debug then eprintf "Iop/Oshrximm1\n"; + debug "Iop/Oshrximm1\n"; exp := [ addinst vn (OEmayundef (MUshrx n)) [ a1; a1 ] dest ]) else if Int.eq n Int.one then ( - if exp_debug then eprintf "Iop/Oshrximm2\n"; + debug "Iop/Oshrximm2\n"; let r1 = r2pi () in let r2 = r2pi () in let op1 = Oshruimm (Int.repr (Z.of_sint 31)) in @@ -952,7 +949,7 @@ let expanse (sb : superblock) code pm = let r3, l3 = extract_arg (i3 :: l2) in exp := addinst vn (OEmayundef (MUshrx n)) [ r3; r3 ] dest :: l3) else ( - if exp_debug then eprintf "Iop/Oshrximm3\n"; + debug "Iop/Oshrximm3\n"; let r1 = r2pi () in let r2 = r2pi () in let r3 = r2pi () in @@ -976,10 +973,10 @@ let expanse (sb : superblock) code pm = was_exp := true | Iop (Oshrxlimm n, a1 :: nil, dest, succ) -> if Int.eq n Int.zero then ( - if exp_debug then eprintf "Iop/Oshrxlimm1\n"; + debug "Iop/Oshrxlimm1\n"; exp := [ addinst vn (OEmayundef (MUshrxl n)) [ a1; a1 ] dest ]) else if Int.eq n Int.one then ( - if exp_debug then eprintf "Iop/Oshrxlimm2\n"; + debug "Iop/Oshrxlimm2\n"; let r1 = r2pi () in let r2 = r2pi () in let op1 = Oshrluimm (Int.repr (Z.of_sint 63)) in @@ -995,7 +992,7 @@ let expanse (sb : superblock) code pm = let r3, l3 = extract_arg (i3 :: l2) in exp := addinst vn (OEmayundef (MUshrxl n)) [ r3; r3 ] dest :: l3) else ( - if exp_debug then eprintf "Iop/Oshrxlimm3\n"; + debug "Iop/Oshrxlimm3\n"; let r1 = r2pi () in let r2 = r2pi () in let r3 = r2pi () in -- cgit