From 7f8ccba038ce9bf7665341c05b89bb5d9b9b536b Mon Sep 17 00:00:00 2001 From: Léo Gourdin Date: Wed, 3 Feb 2021 12:29:11 +0100 Subject: Ccomp for long --- riscV/ExpansionOracle.ml | 201 ++++++++++++++++++++++++++++++++++++++--------- 1 file changed, 166 insertions(+), 35 deletions(-) (limited to 'riscV/ExpansionOracle.ml') diff --git a/riscV/ExpansionOracle.ml b/riscV/ExpansionOracle.ml index 4d587b12..c3f2cb3f 100644 --- a/riscV/ExpansionOracle.ml +++ b/riscV/ExpansionOracle.ml @@ -18,7 +18,7 @@ open RTL open Op open Asmgen open DebugPrint -open PrintRTL +(*open PrintRTL*) open! Integers let reg = ref 1 @@ -28,7 +28,7 @@ let r2p () = Camlcoq.P.of_int !reg let n2p () = Camlcoq.P.of_int !node let n2pi () = node := !node + 1; n2p() -type immt = Xori | Slti +type immt = Xoriw | Xoril | Sltiw | Sltiuw | Sltil | Sltiul let load_hilo32 dest hi lo succ k = if Int.eq lo Int.zero then @@ -36,15 +36,32 @@ let load_hilo32 dest hi lo succ k = else ( Iop (OEluiw hi, [], dest, n2pi()) :: (Iop (Oaddimm lo, [dest], dest, succ)) :: k) +let load_hilo64 dest hi lo succ k = + if Int64.eq lo Int64.zero then + Iop (OEluil hi, [], dest, succ) :: k + else ( + Iop (OEluil hi, [], dest, n2pi()) :: (Iop (Oaddlimm lo, [dest], dest, succ)) :: k) + let loadimm32 dest n succ k = match make_immed32 n with | Imm32_single imm -> Iop (OEaddiwr0 imm, [], dest, succ) :: k | Imm32_pair (hi, lo) -> load_hilo32 dest hi lo succ k +let loadimm64 dest n succ k = + match make_immed64 n with + | Imm64_single imm -> + Iop (OEaddilr0 imm, [], dest, succ) :: k + | Imm64_pair (hi, lo) -> load_hilo64 dest hi lo succ k + | Imm64_large imm -> Iop (OEloadli imm, [], dest, succ) :: k + let get_opimm imm = function - | Xori -> OExoriw imm - | Slti -> OEsltiw imm + | Xoriw -> OExoriw imm + | Sltiw -> OEsltiw imm + | Sltiuw -> OEsltiuw imm + | Xoril -> OExoril imm + | Sltil -> OEsltil imm + | Sltiul -> OEsltiul imm let opimm32 a1 dest n succ k op opimm = match make_immed32 n with @@ -54,8 +71,23 @@ let opimm32 a1 dest n succ k op opimm = reg := !reg + 1; load_hilo32 (r2p()) hi lo (n2pi()) (Iop (op, [a1;r2p()], dest, succ) :: k) -let xorimm32 a1 dest n succ k = opimm32 a1 dest n succ k Oxor Xori -let sltimm32 a1 dest n succ k = opimm32 a1 dest n succ k (OEsltw None) Slti +let opimm64 a1 dest n succ k op opimm = + match make_immed64 n with + | Imm64_single imm -> + Iop (get_opimm imm opimm, [a1], dest, succ) :: k + | Imm64_pair (hi, lo) -> + reg := !reg + 1; + load_hilo64 (r2p()) hi lo (n2pi()) (Iop (op, [a1;r2p()], dest, succ) :: k) + | Imm64_large imm -> + reg := !reg + 1; + Iop (OEloadli imm, [], r2p(), n2pi()) :: Iop (op, [a1;r2p()], dest, succ) :: k + +let xorimm32 a1 dest n succ k = opimm32 a1 dest n succ k Oxor Xoriw +let sltimm32 a1 dest n succ k = opimm32 a1 dest n succ k (OEsltw None) Sltiw +let sltuimm32 a1 dest n succ k = opimm32 a1 dest n succ k (OEsltuw None) Sltiuw +let xorimm64 a1 dest n succ k = opimm64 a1 dest n succ k Oxorl Xoril +let sltimm64 a1 dest n succ k = opimm64 a1 dest n succ k (OEsltl None) Sltil +let sltuimm64 a1 dest n succ k = opimm64 a1 dest n succ k (OEsltul None) Sltiul let cond_int32s_x0 cmp a1 dest succ k = match cmp with @@ -75,6 +107,60 @@ let cond_int32s_reg cmp a1 a2 dest succ k = | Cgt -> Iop (OEsltw None, [a2;a1], dest, succ) :: k | Cge -> Iop (OEsltw None, [a1;a2], dest, n2pi()) :: Iop (OExoriw Int.one, [dest], dest, succ) :: k +let cond_int32u_x0 cmp a1 dest succ k = + match cmp with + | Ceq -> Iop (OEseqw (Some false), [a1;a1], dest, succ) :: k + | Cne -> Iop (OEsnew (Some false), [a1;a1], dest, succ) :: k + | Clt -> Iop (OEsltuw (Some false), [a1;a1], dest, succ) :: k + | Cle -> Iop (OEsltuw (Some true), [a1;a1], dest, n2pi()) :: Iop (OExoriw Int.one, [dest], dest, succ) :: k + | Cgt -> Iop (OEsltuw (Some true), [a1;a1], dest, succ) :: k + | Cge -> Iop (OEsltuw (Some false), [a1;a1], dest, n2pi()) :: Iop (OExoriw Int.one, [dest], dest, succ) :: k + +let cond_int32u_reg cmp a1 a2 dest succ k = + match cmp with + | Ceq -> Iop (OEseqw None, [a1;a2], dest, succ) :: k + | Cne -> Iop (OEsnew None, [a1;a2], dest, succ) :: k + | Clt -> Iop (OEsltuw None, [a1;a2], dest, succ) :: k + | Cle -> Iop (OEsltuw None, [a2;a1], dest, n2pi()) :: Iop (OExoriw Int.one, [dest], dest, succ) :: k + | Cgt -> Iop (OEsltuw None, [a2;a1], dest, succ) :: k + | Cge -> Iop (OEsltuw None, [a1;a2], dest, n2pi()) :: Iop (OExoriw Int.one, [dest], dest, succ) :: k + +let cond_int64s_x0 cmp a1 dest succ k = + match cmp with + | Ceq -> Iop (OEseql (Some false), [a1;a1], dest, succ) :: k + | Cne -> Iop (OEsnel (Some false), [a1;a1], dest, succ) :: k + | Clt -> Iop (OEsltl (Some false), [a1;a1], dest, succ) :: k + | Cle -> Iop (OEsltl (Some true), [a1;a1], dest, n2pi()) :: Iop (OExoriw Int.one, [dest], dest, succ) :: k + | Cgt -> Iop (OEsltl (Some true), [a1;a1], dest, succ) :: k + | Cge -> Iop (OEsltl (Some false), [a1;a1], dest, n2pi()) :: Iop (OExoriw Int.one, [dest], dest, succ) :: k + +let cond_int64s_reg cmp a1 a2 dest succ k = + match cmp with + | Ceq -> Iop (OEseql None, [a1;a2], dest, succ) :: k + | Cne -> Iop (OEsnel None, [a1;a2], dest, succ) :: k + | Clt -> Iop (OEsltl None, [a1;a2], dest, succ) :: k + | Cle -> Iop (OEsltl None, [a2;a1], dest, n2pi()) :: Iop (OExoriw Int.one, [dest], dest, succ) :: k + | Cgt -> Iop (OEsltl None, [a2;a1], dest, succ) :: k + | Cge -> Iop (OEsltl None, [a1;a2], dest, n2pi()) :: Iop (OExoriw Int.one, [dest], dest, succ) :: k + +let cond_int64u_x0 cmp a1 dest succ k = + match cmp with + | Ceq -> Iop (OEseql (Some false), [a1;a1], dest, succ) :: k + | Cne -> Iop (OEsnel (Some false), [a1;a1], dest, succ) :: k + | Clt -> Iop (OEsltul (Some false), [a1;a1], dest, succ) :: k + | Cle -> Iop (OEsltul (Some true), [a1;a1], dest, n2pi()) :: Iop (OExoriw Int.one, [dest], dest, succ) :: k + | Cgt -> Iop (OEsltul (Some true), [a1;a1], dest, succ) :: k + | Cge -> Iop (OEsltul (Some false), [a1;a1], dest, n2pi()) :: Iop (OExoriw Int.one, [dest], dest, succ) :: k + +let cond_int64u_reg cmp a1 a2 dest succ k = + match cmp with + | Ceq -> Iop (OEseql None, [a1;a2], dest, succ) :: k + | Cne -> Iop (OEsnel None, [a1;a2], dest, succ) :: k + | Clt -> Iop (OEsltul None, [a1;a2], dest, succ) :: k + | Cle -> Iop (OEsltul None, [a2;a1], dest, n2pi()) :: Iop (OExoriw Int.one, [dest], dest, succ) :: k + | Cgt -> Iop (OEsltul None, [a2;a1], dest, succ) :: k + | Cge -> Iop (OEsltul None, [a1;a2], dest, n2pi()) :: Iop (OExoriw Int.one, [dest], dest, succ) :: k + let expanse_condimm_int32s cmp a1 n dest succ k = if Int.eq n Int.zero then cond_int32s_x0 cmp a1 dest succ k else match cmp with @@ -87,22 +173,40 @@ let expanse_condimm_int32s cmp a1 n dest succ k = | _ -> reg := !reg + 1; loadimm32 (r2p()) n (n2pi()) (cond_int32s_reg cmp a1 (r2p()) dest succ k) -let cond_int32u_reg cmp a1 a2 dest succ k = +let expanse_condimm_int32u cmp a1 n dest succ k = + if Int.eq n Int.zero then cond_int32u_x0 cmp a1 dest succ k else match cmp with - | Ceq -> Iop (OEseqw None, [a1;a2], dest, succ) :: k - | Cne -> Iop (OEsnew None, [a1;a2], dest, succ) :: k - | Clt -> Iop (OEsltuw None, [a1;a2], dest, succ) :: k - | Cle -> Iop (OEsltuw None, [a2;a1], dest, n2pi()) :: Iop (OExoriw Int.one, [dest], dest, succ) :: k - | Cgt -> Iop (OEsltuw None, [a2;a1], dest, succ) :: k - | Cge -> Iop (OEsltuw None, [a1;a2], dest, n2pi()) :: Iop (OExoriw Int.one, [dest], dest, succ) :: k + | Clt -> sltuimm32 a1 dest n succ k + | _ -> reg := !reg + 1; + loadimm32 (r2p()) n (n2pi()) (cond_int32u_reg cmp a1 (r2p()) dest succ k) + +let expanse_condimm_int64s cmp a1 n dest succ k = + if Int.eq n Int.zero then cond_int64s_x0 cmp a1 dest succ k else + match cmp with + | Ceq | Cne -> + reg := !reg + 1; + xorimm64 a1 (r2p()) n (n2pi()) (cond_int64s_x0 cmp (r2p()) dest succ k) + | Clt -> sltimm64 a1 dest n succ k + | Cle -> if Int64.eq n (Int64.repr Int64.max_signed) + then loadimm32 dest Int.one succ k + else sltimm64 a1 dest (Int64.add n Int64.one) succ k + | _ -> reg := !reg + 1; + loadimm64 (r2p()) n (n2pi()) (cond_int64s_reg cmp a1 (r2p()) dest succ k) + +let expanse_condimm_int64u cmp a1 n dest succ k = + if Int64.eq n Int64.zero then cond_int64u_x0 cmp a1 dest succ k else + match cmp with + | Clt -> sltuimm64 a1 dest n succ k + | _ -> reg := !reg + 1; + loadimm64 (r2p()) n (n2pi()) (cond_int64u_reg cmp a1 (r2p()) dest succ k) let rec write_tree exp n code' = match exp with | (Iop (_,_,_,succ)) as inst :: k -> - print_instruction stderr (0,inst); - Printf.eprintf "PLACING NODE %d\n" (Camlcoq.P.to_int n); + (*print_instruction stderr (0,inst);*) + (*Printf.eprintf "PLACING NODE %d\n" (Camlcoq.P.to_int n);*) code' := PTree.set n inst !code'; - Printf.eprintf "WITH SUCC %d\n" (Camlcoq.P.to_int succ); + (*Printf.eprintf "WITH SUCC %d\n" (Camlcoq.P.to_int succ);*) write_tree k (Camlcoq.P.of_int ((Camlcoq.P.to_int n) + 1)) code' | _ -> !code' @@ -135,34 +239,61 @@ let generate_head_order n start_node new_order = let expanse (sb: superblock) code = debug_flag := true; let new_order = ref [] in + let exp = ref [] in + let was_exp = ref false in let code' = ref code in Array.iter (fun n -> + was_exp := false; let inst = get_some @@ PTree.get n code in + let start_node = Camlcoq.P.of_int (!node + 1) in ( match inst with + | Iop (Ocmp (Ccomp c), a1 :: a2 :: nil, dest, succ) -> ( + Printf.eprintf "Ccomp\n"; + exp := cond_int32s_reg c a1 a2 dest succ []; + was_exp := true) | Iop (Ocmp (Ccompu c), a1 :: a2 :: nil, dest, succ) -> ( - Printf.eprintf "[EXPANSION] Last node is: %d\n" !node; - Printf.eprintf "[EXPANSION] Last reg is: %d\n" !reg; - Printf.eprintf "CUR IS %d\n" (Camlcoq.P.to_int n); - Printf.eprintf "SUCC IS %d\n" (Camlcoq.P.to_int succ); - debug "[EXPANSION] Replace this:\n"; - print_instruction stderr (0,inst); - debug "[EXPANSION] With:\n"; - let start_node = Camlcoq.P.of_int (!node + 1) in - let exp = cond_int32u_reg c a1 a2 dest succ [] in - code' := write_tree (List.rev exp) start_node code'; - let first = Inop (n2pi()) in - code' := PTree.set n first !code'; - generate_head_order n start_node new_order) + Printf.eprintf "Ccompu\n"; + exp := cond_int32u_reg c a1 a2 dest succ []; + was_exp := true) | Iop (Ocmp (Ccompimm (c, imm)), a1 :: nil, dest, succ) -> ( - let start_node = Camlcoq.P.of_int (!node + 1) in - let exp = expanse_condimm_int32s c a1 imm dest succ [] in - code' := write_tree (List.rev exp) start_node code'; + Printf.eprintf "Ccompimm\n"; + exp := expanse_condimm_int32s c a1 imm dest succ []; + was_exp := true) + | Iop (Ocmp (Ccompuimm (c, imm)), a1 :: nil, dest, succ) -> ( + Printf.eprintf "Ccompuimm\n"; + exp := expanse_condimm_int32u c a1 imm dest succ []; + was_exp := true) + | Iop (Ocmp (Ccompl c), a1 :: a2 :: nil, dest, succ) -> ( + Printf.eprintf "Ccompl\n"; + exp := cond_int64s_reg c a1 a2 dest succ []; + was_exp := true) + | Iop (Ocmp (Ccomplu c), a1 :: a2 :: nil, dest, succ) -> ( + Printf.eprintf "Ccomplu\n"; + exp := cond_int64u_reg c a1 a2 dest succ []; + was_exp := true) + | Iop (Ocmp (Ccomplimm (c, imm)), a1 :: nil, dest, succ) -> ( + (*Printf.eprintf "Ccomplimm\n";*) + (*Printf.eprintf "[EXPANSION] Last node is: %d\n" !node;*) + (*Printf.eprintf "[EXPANSION] Last reg is: %d\n" !reg;*) + (*Printf.eprintf "CUR IS %d\n" (Camlcoq.P.to_int n);*) + (*Printf.eprintf "SUCC IS %d\n" (Camlcoq.P.to_int succ);*) + (*debug "[EXPANSION] Replace this:\n";*) + (*print_instruction stderr (0,inst);*) + (*debug "[EXPANSION] With:\n";*) + (*Printf.eprintf "entry is %d\n" (Camlcoq.P.to_int !entry);*) + (*entry := n2p()*) + exp := expanse_condimm_int64s c a1 imm dest succ []; + was_exp := true) + | Iop (Ocmp (Ccompluimm (c, imm)), a1 :: nil, dest, succ) -> ( + Printf.eprintf "Ccompluimm\n"; + exp := expanse_condimm_int64u c a1 imm dest succ []; + was_exp := true) + | _ -> new_order := !new_order @ [n]); + if !was_exp then ( + code' := write_tree (List.rev !exp) start_node code'; let first = Inop (n2pi()) in code' := PTree.set n first !code'; generate_head_order n start_node new_order) - (*Printf.eprintf "entry is %d\n" (Camlcoq.P.to_int !entry);*) - (*entry := n2p()*) - | _ -> new_order := !new_order @ [n] ) sb.instructions; sb.instructions <- Array.of_list !new_order; (*print_arrayp sb.instructions;*) -- cgit