branches expansions support

1 files changed, 158 insertions, 2 deletions

diff --git a/riscV/ExpansionOracle.ml b/riscV/ExpansionOracle.ml
index 2a21b7a4..7295ae0d 100644
--- a/riscV/ExpansionOracle.ml
+++ b/riscV/ExpansionOracle.ml
@@ -339,6 +339,46 @@ let is_inv_cmp = function Cle | Cgt -> true | _ -> false
 let make_optR is_x0 is_inv =
   if is_x0 then if is_inv then Some X0_L else Some X0_R else None
 
+let cbranch_int32s is_x0 cmp a1 a2 iinfo succ1 succ2 k =
+  let optR = make_optR is_x0 (is_inv_cmp cmp) in
+  match cmp with
+  | Ceq -> Scond (CEbeqw optR, [ a1; a2 ], succ1, succ2, iinfo) :: k
+  | Cne -> Scond (CEbnew optR, [ a1; a2 ], succ1, succ2, iinfo) :: k
+  | Clt -> Scond (CEbltw optR, [ a1; a2 ], succ1, succ2, iinfo) :: k
+  | Cle -> Scond (CEbgew optR, [ a2; a1 ], succ1, succ2, iinfo) :: k
+  | Cgt -> Scond (CEbltw optR, [ a2; a1 ], succ1, succ2, iinfo) :: k
+  | Cge -> Scond (CEbgew optR, [ a1; a2 ], succ1, succ2, iinfo) :: k
+
+let cbranch_int32u is_x0 cmp a1 a2 iinfo succ1 succ2 k =
+  let optR = make_optR is_x0 (is_inv_cmp cmp) in
+  match cmp with
+  | Ceq -> Scond (CEbequw optR, [ a1; a2 ], succ1, succ2, iinfo) :: k
+  | Cne -> Scond (CEbneuw optR, [ a1; a2 ], succ1, succ2, iinfo) :: k
+  | Clt -> Scond (CEbltuw optR, [ a1; a2 ], succ1, succ2, iinfo) :: k
+  | Cle -> Scond (CEbgeuw optR, [ a2; a1 ], succ1, succ2, iinfo) :: k
+  | Cgt -> Scond (CEbltuw optR, [ a2; a1 ], succ1, succ2, iinfo) :: k
+  | Cge -> Scond (CEbgeuw optR, [ a1; a2 ], succ1, succ2, iinfo) :: k
+
+let cbranch_int64s is_x0 cmp a1 a2 iinfo succ1 succ2 k =
+  let optR = make_optR is_x0 (is_inv_cmp cmp) in
+  match cmp with
+  | Ceq -> Scond (CEbeql optR, [ a1; a2 ], succ1, succ2, iinfo) :: k
+  | Cne -> Scond (CEbnel optR, [ a1; a2 ], succ1, succ2, iinfo) :: k
+  | Clt -> Scond (CEbltl optR, [ a1; a2 ], succ1, succ2, iinfo) :: k
+  | Cle -> Scond (CEbgel optR, [ a2; a1 ], succ1, succ2, iinfo) :: k
+  | Cgt -> Scond (CEbltl optR, [ a2; a1 ], succ1, succ2, iinfo) :: k
+  | Cge -> Scond (CEbgel optR, [ a1; a2 ], succ1, succ2, iinfo) :: k
+
+let cbranch_int64u is_x0 cmp a1 a2 iinfo succ1 succ2 k =
+  let optR = make_optR is_x0 (is_inv_cmp cmp) in
+  match cmp with
+  | Ceq -> Scond (CEbequl optR, [ a1; a2 ], succ1, succ2, iinfo) :: k
+  | Cne -> Scond (CEbneul optR, [ a1; a2 ], succ1, succ2, iinfo) :: k
+  | Clt -> Scond (CEbltul optR, [ a1; a2 ], succ1, succ2, iinfo) :: k
+  | Cle -> Scond (CEbgeul optR, [ a2; a1 ], succ1, succ2, iinfo) :: k
+  | Cgt -> Scond (CEbltul optR, [ a2; a1 ], succ1, succ2, iinfo) :: k
+  | Cge -> Scond (CEbgeul optR, [ a1; a2 ], succ1, succ2, iinfo) :: k
+
 let cond_int32s vn is_x0 cmp a1 a2 dest =
   let optR = make_optR is_x0 (is_inv_cmp cmp) in
   match cmp with
@@ -439,6 +479,40 @@ let cond_single vn cmp f1 f2 dest =
   | Cgt -> [ addinst vn OEflts [ f2; f1 ] dest ]
   | Cge -> [ addinst vn OEfles [ f2; f1 ] dest ]
 
+let expanse_cbranchimm_int32s vn cmp a1 n iinfo succ1 succ2 =
+  if Int.eq n Int.zero then cbranch_int32s true cmp a1 a1 iinfo succ1 succ2 []
+  else
+    let r = r2pi () in
+    let l = loadimm32 vn r n in
+    let r', l' = extract_arg l in
+    cbranch_int32s false cmp a1 r' iinfo succ1 succ2 l'
+
+let expanse_cbranchimm_int32u vn cmp a1 n iinfo succ1 succ2 =
+  if Int.eq n Int.zero then cbranch_int32u true cmp a1 a1 iinfo succ1 succ2 []
+  else
+    let r = r2pi () in
+    let l = loadimm32 vn r n in
+    let r', l' = extract_arg l in
+    cbranch_int32u false cmp a1 r' iinfo succ1 succ2 l'
+
+let expanse_cbranchimm_int64s vn cmp a1 n iinfo succ1 succ2 =
+  if Int64.eq n Int64.zero then
+    cbranch_int64s true cmp a1 a1 iinfo succ1 succ2 []
+  else
+    let r = r2pi () in
+    let l = loadimm64 vn r n in
+    let r', l' = extract_arg l in
+    cbranch_int64s false cmp a1 r' iinfo succ1 succ2 l'
+
+let expanse_cbranchimm_int64u vn cmp a1 n iinfo succ1 succ2 =
+  if Int64.eq n Int64.zero then
+    cbranch_int64u true cmp a1 a1 iinfo succ1 succ2 []
+  else
+    let r = r2pi () in
+    let l = loadimm64 vn r n in
+    let r', l' = extract_arg l in
+    cbranch_int64u false cmp a1 r' iinfo succ1 succ2 l'
+
 let expanse_condimm_int32s vn cmp a1 n dest =
   if Int.eq n Int.zero then cond_int32s vn true cmp a1 a1 dest
   else
@@ -514,6 +588,16 @@ let expanse_cond_fp vn cnot fn_cond cmp f1 f2 dest =
     let r', l = extract_arg insn in
     addinst vn (OExoriw Int.one) [ r' ] dest :: l
 
+let expanse_cbranch_fp vn cnot fn_cond cmp f1 f2 iinfo succ1 succ2 =
+  let r = r2pi () in
+  let normal = is_normal_cmp cmp in
+  let normal' = if cnot then not normal else normal in
+  let insn = fn_cond vn cmp f1 f2 r in
+  let r', l = extract_arg insn in
+  if normal' then
+    Scond (CEbnew (Some X0_R), [ r'; r' ], succ1, succ2, iinfo) :: l
+  else Scond (CEbeqw (Some X0_R), [ r'; r' ], succ1, succ2, iinfo) :: l
+
 (** Return olds args if the CSE numbering is empty *)
 
 let get_arguments vn vals args =
@@ -529,22 +613,26 @@ let rec gen_btl_list vn exp =
       inst :: gen_btl_list vn k
   | [ Sexp (rd, Smove, args, iinfo) ] -> [ Bop (Omove, args, rd, iinfo) ]
   | [ Scond (cond, args, succ1, succ2, iinfo) ] ->
-      [ Bcond (cond, args, succ1, succ2, iinfo) ]
+      let ib = Bcond (cond, args, succ1, succ2, iinfo) in
+      [ ib ]
   | [] -> []
   | _ -> failwith "write_tree: invalid list"
 
 let expanse_list li =
   debug "#### New block for expansion oracle\n";
   let exp = ref [] in
+  let was_branch = ref false in
   let was_exp = ref false in
   let vn = ref (empty_numbering ()) in
   let rec expanse_list_rec li =
     match li with
     | [] -> li
     | i :: li' ->
+        was_branch := false;
         was_exp := false;
         (if !Clflags.option_fexpanse_rtlcond then
          match i with
+         (* Expansion of conditions - Ocmp *)
          | Bop (Ocmp (Ccomp c), a1 :: a2 :: nil, dest, iinfo) ->
              debug "Bop/Ccomp\n";
              exp := cond_int32s vn false c a1 a2 dest;
@@ -605,9 +693,75 @@ let expanse_list li =
              exp := expanse_cond_fp vn true cond_single c f1 f2 dest;
              exp := extract_final vn !exp dest;
              was_exp := true
+         (* Expansion of branches - Ccomp *)
+         | Bcond (Ccomp c, a1 :: a2 :: nil, succ1, succ2, iinfo) ->
+             debug "Bcond/Ccomp\n";
+             exp := cbranch_int32s false c a1 a2 iinfo succ1 succ2 [];
+             was_branch := true;
+             was_exp := true
+         | Bcond (Ccompu c, a1 :: a2 :: nil, succ1, succ2, iinfo) ->
+             debug "Bcond/Ccompu\n";
+             exp := cbranch_int32u false c a1 a2 iinfo succ1 succ2 [];
+             was_branch := true;
+             was_exp := true
+         | Bcond (Ccompimm (c, imm), a1 :: nil, succ1, succ2, iinfo) ->
+             debug "Bcond/Ccompimm\n";
+             exp := expanse_cbranchimm_int32s vn c a1 imm iinfo succ1 succ2;
+             was_branch := true;
+             was_exp := true
+         | Bcond (Ccompuimm (c, imm), a1 :: nil, succ1, succ2, iinfo) ->
+             debug "Bcond/Ccompuimm\n";
+             exp := expanse_cbranchimm_int32u vn c a1 imm iinfo succ1 succ2;
+             was_branch := true;
+             was_exp := true
+         | Bcond (Ccompl c, a1 :: a2 :: nil, succ1, succ2, iinfo) ->
+             debug "Bcond/Ccompl\n";
+             exp := cbranch_int64s false c a1 a2 iinfo succ1 succ2 [];
+             was_branch := true;
+             was_exp := true
+         | Bcond (Ccomplu c, a1 :: a2 :: nil, succ1, succ2, iinfo) ->
+             debug "Bcond/Ccomplu\n";
+             exp := cbranch_int64u false c a1 a2 iinfo succ1 succ2 [];
+             was_branch := true;
+             was_exp := true
+         | Bcond (Ccomplimm (c, imm), a1 :: nil, succ1, succ2, iinfo) ->
+             debug "Bcond/Ccomplimm\n";
+             exp := expanse_cbranchimm_int64s vn c a1 imm iinfo succ1 succ2;
+             was_branch := true;
+             was_exp := true
+         | Bcond (Ccompluimm (c, imm), a1 :: nil, succ1, succ2, iinfo) ->
+             debug "Bcond/Ccompluimm\n";
+             exp := expanse_cbranchimm_int64u vn c a1 imm iinfo succ1 succ2;
+             was_branch := true;
+             was_exp := true
+         | Bcond (Ccompf c, f1 :: f2 :: nil, succ1, succ2, iinfo) ->
+             debug "Bcond/Ccompf\n";
+             exp :=
+               expanse_cbranch_fp vn false cond_float c f1 f2 iinfo succ1 succ2;
+             was_branch := true;
+             was_exp := true
+         | Bcond (Cnotcompf c, f1 :: f2 :: nil, succ1, succ2, iinfo) ->
+             debug "Bcond/Cnotcompf\n";
+             exp :=
+               expanse_cbranch_fp vn true cond_float c f1 f2 iinfo succ1 succ2;
+             was_branch := true;
+             was_exp := true
+         | Bcond (Ccompfs c, f1 :: f2 :: nil, succ1, succ2, iinfo) ->
+             debug "Bcond/Ccompfs\n";
+             exp :=
+               expanse_cbranch_fp vn false cond_single c f1 f2 iinfo succ1 succ2;
+             was_branch := true;
+             was_exp := true
+         | Bcond (Cnotcompfs c, f1 :: f2 :: nil, succ1, succ2, iinfo) ->
+             debug "Bcond/Cnotcompfs\n";
+             exp :=
+               expanse_cbranch_fp vn true cond_single c f1 f2 iinfo succ1 succ2;
+             was_branch := true;
+             was_exp := true
          | _ -> ());
         (if !Clflags.option_fexpanse_others && not !was_exp then
          match i with
+         (* Others expansions *)
          | Bop (Ofloatconst f, nil, dest, iinfo) -> (
              match make_immed64 (Floats.Float.to_bits f) with
              | Imm64_single _ | Imm64_large _ -> ()
@@ -814,7 +968,9 @@ let expanse_list li =
               (* TODO gourdinl empty numb BF? vn := empty_numbering ()*)
           | _ -> ());
           i :: expanse_list_rec li')
-        else gen_btl_list vn (List.rev !exp) @ expanse_list_rec li'
+        else
+          let hd = gen_btl_list vn (List.rev !exp) in
+          hd @ expanse_list_rec li'
   in
   expanse_list_rec li