From 4df03aaf5204d2f15885b49fe3f5c9cb61b4596d Mon Sep 17 00:00:00 2001 From: Léo Gourdin Date: Tue, 2 Feb 2021 18:31:46 +0100 Subject: Ccompu expansion --- riscV/ExpansionOracle.ml | 27 ++++++++++++++++++--------- 1 file changed, 18 insertions(+), 9 deletions(-) (limited to 'riscV/ExpansionOracle.ml') diff --git a/riscV/ExpansionOracle.ml b/riscV/ExpansionOracle.ml index 15a418fd..4d587b12 100644 --- a/riscV/ExpansionOracle.ml +++ b/riscV/ExpansionOracle.ml @@ -87,6 +87,15 @@ 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 = + 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 rec write_tree exp n code' = match exp with | (Iop (_,_,_,succ)) as inst :: k -> @@ -130,7 +139,7 @@ let expanse (sb: superblock) code = Array.iter (fun n -> let inst = get_some @@ PTree.get n code in match inst with - | Iop (Ocmp (Ccompimm (c, imm)), a1 :: nil, dest, succ) -> ( + | 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); @@ -138,21 +147,21 @@ let expanse (sb: superblock) code = 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) + | 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'; let first = Inop (n2pi()) in code' := PTree.set n first !code'; - generate_head_order n start_node new_order; + generate_head_order n start_node new_order) (*Printf.eprintf "entry is %d\n" (Camlcoq.P.to_int !entry);*) (*entry := n2p()*) - (*| Icond (cond,args,ifso,ifnot,info) -> (code' := - match cond, args with - | Ccompimm (c, imm), a1 :: nil -> - expanse_condimm_int32s cond a1 imm info ifso ifnot - PTree.set n (Icond (cond,args,ifso,ifnot,info)) !code' - | (_, _) -> !code'*) - (*PTree.set node*)) | _ -> new_order := !new_order @ [n] ) sb.instructions; sb.instructions <- Array.of_list !new_order; -- cgit