From 8663f220ec0b0f10e74ae7442cdf221a83fc3943 Mon Sep 17 00:00:00 2001
From: Léo Gourdin <leo.gourdin@univ-grenoble-alpes.fr>
Date: Tue, 20 Jul 2021 22:16:11 +0200
Subject: bug fix in oracle

---
 riscV/ExpansionOracle.ml | 393 +++++++++++++++++++++++++++++++++++++++++++----
 1 file changed, 360 insertions(+), 33 deletions(-)

(limited to 'riscV')

diff --git a/riscV/ExpansionOracle.ml b/riscV/ExpansionOracle.ml
index 7950cb6a..c1cf5c9c 100644
--- a/riscV/ExpansionOracle.ml
+++ b/riscV/ExpansionOracle.ml
@@ -20,6 +20,7 @@ open BTLcommonaux
 open AST
 open Datatypes
 open Maps
+open Asmgen
 
 (** Tools *)
 
@@ -31,10 +32,7 @@ let rec iblock_to_list ib =
 
 let rec list_to_iblock lib =
   match lib with
-  | i1 :: k ->
-      if List.length lib > 1 then
-        Bseq (i1, list_to_iblock k)
-      else i1
+  | i1 :: k -> if List.length lib > 1 then Bseq (i1, list_to_iblock k) else i1
   | [] -> failwith "list_to_iblock: called on empty list"
 
 (** Mini CSE (a dynamic numbering is applied during expansion. 
@@ -205,7 +203,7 @@ let extract_final vn fl fdest =
     | _ -> fl
   else failwith "extract_final: trying to extract on an empty list"
 
-let addinst vn op args rd iinfo =
+let addinst vn op args rd =
   let v = get_nvalues vn args in
   let rh = Sop (op, v) in
   match find_rhs vn rh with
@@ -214,34 +212,308 @@ let addinst vn op args rd iinfo =
       Sr r
   | None ->
       addsop vn v op rd;
-      Sexp (rd, rh, args, iinfo)
+      Sexp (rd, rh, args, def_iinfo ())
 
 (** Expansion functions *)
 
+type immt =
+  | Addiw
+  | Addil
+  | Andiw
+  | Andil
+  | Oriw
+  | Oril
+  | Xoriw
+  | Xoril
+  | Sltiw
+  | Sltiuw
+  | Sltil
+  | Sltiul
+
+let load_hilo32 vn dest hi lo =
+  let op1 = OEluiw hi in
+  if Int.eq lo Int.zero then [ addinst vn op1 [] dest ]
+  else
+    let r = r2pi () in
+    let op2 = OEaddiw (None, lo) in
+    let i1 = addinst vn op1 [] r in
+    let r', l = extract_arg [ i1 ] in
+    let i2 = addinst vn op2 [ r' ] dest in
+    i2 :: l
+
+let load_hilo64 vn dest hi lo =
+  let op1 = OEluil hi in
+  if Int64.eq lo Int64.zero then [ addinst vn op1 [] dest ]
+  else
+    let r = r2pi () in
+    let op2 = OEaddil (None, lo) in
+    let i1 = addinst vn op1 [] r in
+    let r', l = extract_arg [ i1 ] in
+    let i2 = addinst vn op2 [ r' ] dest in
+    i2 :: l
+
+let loadimm32 vn dest n =
+  match make_immed32 n with
+  | Imm32_single imm ->
+      let op1 = OEaddiw (Some X0_R, imm) in
+      [ addinst vn op1 [] dest ]
+  | Imm32_pair (hi, lo) -> load_hilo32 vn dest hi lo
+
+let loadimm64 vn dest n =
+  match make_immed64 n with
+  | Imm64_single imm ->
+      let op1 = OEaddil (Some X0_R, imm) in
+      [ addinst vn op1 [] dest ]
+  | Imm64_pair (hi, lo) -> load_hilo64 vn dest hi lo
+  | Imm64_large imm ->
+      let op1 = OEloadli imm in
+      [ addinst vn op1 [] dest ]
+
+let get_opimm optR imm = function
+  | Addiw -> OEaddiw (optR, imm)
+  | Andiw -> OEandiw imm
+  | Oriw -> OEoriw imm
+  | Xoriw -> OExoriw imm
+  | Sltiw -> OEsltiw imm
+  | Sltiuw -> OEsltiuw imm
+  | Addil -> OEaddil (optR, imm)
+  | Andil -> OEandil imm
+  | Oril -> OEoril imm
+  | Xoril -> OExoril imm
+  | Sltil -> OEsltil imm
+  | Sltiul -> OEsltiul imm
+
+let opimm32 vn a1 dest n optR op opimm =
+  match make_immed32 n with
+  | Imm32_single imm -> [ addinst vn (get_opimm optR imm opimm) [ a1 ] dest ]
+  | Imm32_pair (hi, lo) ->
+      let r = r2pi () in
+      let l = load_hilo32 vn r hi lo in
+      let r', l' = extract_arg l in
+      let i = addinst vn op [ a1; r' ] dest in
+      i :: l'
+
+let opimm64 vn a1 dest n optR op opimm =
+  match make_immed64 n with
+  | Imm64_single imm -> [ addinst vn (get_opimm optR imm opimm) [ a1 ] dest ]
+  | Imm64_pair (hi, lo) ->
+      let r = r2pi () in
+      let l = load_hilo64 vn r hi lo in
+      let r', l' = extract_arg l in
+      let i = addinst vn op [ a1; r' ] dest in
+      i :: l'
+  | Imm64_large imm ->
+      let r = r2pi () in
+      let op1 = OEloadli imm in
+      let i1 = addinst vn op1 [] r in
+      let r', l' = extract_arg [ i1 ] in
+      let i2 = addinst vn op [ a1; r' ] dest in
+      i2 :: l'
+
+let addimm32 vn a1 dest n optR = opimm32 vn a1 dest n optR Oadd Addiw
+
+let andimm32 vn a1 dest n = opimm32 vn a1 dest n None Oand Andiw
+
+let orimm32 vn a1 dest n = opimm32 vn a1 dest n None Oor Oriw
+
+let xorimm32 vn a1 dest n = opimm32 vn a1 dest n None Oxor Xoriw
+
+let sltimm32 vn a1 dest n = opimm32 vn a1 dest n None (OEsltw None) Sltiw
+
+let sltuimm32 vn a1 dest n = opimm32 vn a1 dest n None (OEsltuw None) Sltiuw
+
+let addimm64 vn a1 dest n optR = opimm64 vn a1 dest n optR Oaddl Addil
+
+let andimm64 vn a1 dest n = opimm64 vn a1 dest n None Oandl Andil
+
+let orimm64 vn a1 dest n = opimm64 vn a1 dest n None Oorl Oril
+
+let xorimm64 vn a1 dest n = opimm64 vn a1 dest n None Oxorl Xoril
+
+let sltimm64 vn a1 dest n = opimm64 vn a1 dest n None (OEsltl None) Sltil
+
+let sltuimm64 vn a1 dest n = opimm64 vn a1 dest n None (OEsltul None) Sltiul
+
 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 cond_int32s vn is_x0 cmp a1 a2 dest iinfo =
+let cond_int32s vn is_x0 cmp a1 a2 dest =
   let optR = make_optR is_x0 (is_inv_cmp cmp) in
   match cmp with
-  | Ceq -> [ addinst vn (OEseqw optR) [ a1; a2 ] dest iinfo ]
-  | Cne -> [ addinst vn (OEsnew optR) [ a1; a2 ] dest iinfo ]
-  | Clt -> [ addinst vn (OEsltw optR) [ a1; a2 ] dest iinfo ]
+  | Ceq -> [ addinst vn (OEseqw optR) [ a1; a2 ] dest ]
+  | Cne -> [ addinst vn (OEsnew optR) [ a1; a2 ] dest ]
+  | Clt -> [ addinst vn (OEsltw optR) [ a1; a2 ] dest ]
   | Cle ->
       let r = r2pi () in
       let op = OEsltw optR in
-      let i1 = addinst vn op [ a2; a1 ] r iinfo in
+      let i1 = addinst vn op [ a2; a1 ] r in
       let r', l = extract_arg [ i1 ] in
-      addinst vn (OExoriw Int.one) [ r' ] dest iinfo :: l
-  | Cgt -> [ addinst vn (OEsltw optR) [ a2; a1 ] dest iinfo ]
+      addinst vn (OExoriw Int.one) [ r' ] dest :: l
+  | Cgt -> [ addinst vn (OEsltw optR) [ a2; a1 ] dest ]
   | Cge ->
       let r = r2pi () in
       let op = OEsltw optR in
-      let i1 = addinst vn op [ a1; a2 ] r iinfo in
+      let i1 = addinst vn op [ a1; a2 ] r in
+      let r', l = extract_arg [ i1 ] in
+      addinst vn (OExoriw Int.one) [ r' ] dest :: l
+
+let cond_int32u vn is_x0 cmp a1 a2 dest =
+  let optR = make_optR is_x0 (is_inv_cmp cmp) in
+  match cmp with
+  | Ceq -> [ addinst vn (OEsequw optR) [ a1; a2 ] dest ]
+  | Cne -> [ addinst vn (OEsneuw optR) [ a1; a2 ] dest ]
+  | Clt -> [ addinst vn (OEsltuw optR) [ a1; a2 ] dest ]
+  | Cle ->
+      let r = r2pi () in
+      let op = OEsltuw optR in
+      let i1 = addinst vn op [ a2; a1 ] r in
+      let r', l = extract_arg [ i1 ] in
+      addinst vn (OExoriw Int.one) [ r' ] dest :: l
+  | Cgt -> [ addinst vn (OEsltuw optR) [ a2; a1 ] dest ]
+  | Cge ->
+      let r = r2pi () in
+      let op = OEsltuw optR in
+      let i1 = addinst vn op [ a1; a2 ] r in
+      let r', l = extract_arg [ i1 ] in
+      addinst vn (OExoriw Int.one) [ r' ] dest :: l
+
+let cond_int64s vn is_x0 cmp a1 a2 dest =
+  let optR = make_optR is_x0 (is_inv_cmp cmp) in
+  match cmp with
+  | Ceq -> [ addinst vn (OEseql optR) [ a1; a2 ] dest ]
+  | Cne -> [ addinst vn (OEsnel optR) [ a1; a2 ] dest ]
+  | Clt -> [ addinst vn (OEsltl optR) [ a1; a2 ] dest ]
+  | Cle ->
+      let r = r2pi () in
+      let op = OEsltl optR in
+      let i1 = addinst vn op [ a2; a1 ] r in
       let r', l = extract_arg [ i1 ] in
-      addinst vn (OExoriw Int.one) [ r' ] dest iinfo :: l
+      addinst vn (OExoriw Int.one) [ r' ] dest :: l
+  | Cgt -> [ addinst vn (OEsltl optR) [ a2; a1 ] dest ]
+  | Cge ->
+      let r = r2pi () in
+      let op = OEsltl optR in
+      let i1 = addinst vn op [ a1; a2 ] r in
+      let r', l = extract_arg [ i1 ] in
+      addinst vn (OExoriw Int.one) [ r' ] dest :: l
+
+let cond_int64u vn is_x0 cmp a1 a2 dest =
+  let optR = make_optR is_x0 (is_inv_cmp cmp) in
+  match cmp with
+  | Ceq -> [ addinst vn (OEsequl optR) [ a1; a2 ] dest ]
+  | Cne -> [ addinst vn (OEsneul optR) [ a1; a2 ] dest ]
+  | Clt -> [ addinst vn (OEsltul optR) [ a1; a2 ] dest ]
+  | Cle ->
+      let r = r2pi () in
+      let op = OEsltul optR in
+      let i1 = addinst vn op [ a2; a1 ] r in
+      let r', l = extract_arg [ i1 ] in
+      addinst vn (OExoriw Int.one) [ r' ] dest :: l
+  | Cgt -> [ addinst vn (OEsltul optR) [ a2; a1 ] dest ]
+  | Cge ->
+      let r = r2pi () in
+      let op = OEsltul optR in
+      let i1 = addinst vn op [ a1; a2 ] r in
+      let r', l = extract_arg [ i1 ] in
+      addinst vn (OExoriw Int.one) [ r' ] dest :: l
+
+let is_normal_cmp = function Cne -> false | _ -> true
+
+let cond_float vn cmp f1 f2 dest =
+  match cmp with
+  | Ceq -> [ addinst vn OEfeqd [ f1; f2 ] dest ]
+  | Cne -> [ addinst vn OEfeqd [ f1; f2 ] dest ]
+  | Clt -> [ addinst vn OEfltd [ f1; f2 ] dest ]
+  | Cle -> [ addinst vn OEfled [ f1; f2 ] dest ]
+  | Cgt -> [ addinst vn OEfltd [ f2; f1 ] dest ]
+  | Cge -> [ addinst vn OEfled [ f2; f1 ] dest ]
+
+let cond_single vn cmp f1 f2 dest =
+  match cmp with
+  | Ceq -> [ addinst vn OEfeqs [ f1; f2 ] dest ]
+  | Cne -> [ addinst vn OEfeqs [ f1; f2 ] dest ]
+  | Clt -> [ addinst vn OEflts [ f1; f2 ] dest ]
+  | Cle -> [ addinst vn OEfles [ f1; f2 ] dest ]
+  | Cgt -> [ addinst vn OEflts [ f2; f1 ] dest ]
+  | Cge -> [ addinst vn OEfles [ f2; f1 ] dest ]
+
+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
+    match cmp with
+    | Ceq | Cne ->
+        let r = r2pi () in
+        let l = xorimm32 vn a1 r n in
+        let r', l' = extract_arg l in
+        cond_int32s vn true cmp r' r' dest @ l'
+    | Clt -> sltimm32 vn a1 dest n
+    | Cle ->
+        if Int.eq n (Int.repr Int.max_signed) then
+          let l = loadimm32 vn dest Int.one in
+          let r, l' = extract_arg l in
+          addinst vn (OEmayundef MUint) [ a1; r ] dest :: l'
+        else sltimm32 vn a1 dest (Int.add n Int.one)
+    | _ ->
+        let r = r2pi () in
+        let l = loadimm32 vn r n in
+        let r', l' = extract_arg l in
+        cond_int32s vn false cmp a1 r' dest @ l'
+
+let expanse_condimm_int32u vn cmp a1 n dest =
+  if Int.eq n Int.zero then cond_int32u vn true cmp a1 a1 dest
+  else
+    match cmp with
+    | Clt -> sltuimm32 vn a1 dest n
+    | _ ->
+        let r = r2pi () in
+        let l = loadimm32 vn r n in
+        let r', l' = extract_arg l in
+        cond_int32u vn false cmp a1 r' dest @ l'
+
+let expanse_condimm_int64s vn cmp a1 n dest =
+  if Int64.eq n Int64.zero then cond_int64s vn true cmp a1 a1 dest
+  else
+    match cmp with
+    | Ceq | Cne ->
+        let r = r2pi () in
+        let l = xorimm64 vn a1 r n in
+        let r', l' = extract_arg l in
+        cond_int64s vn true cmp r' r' dest @ l'
+    | Clt -> sltimm64 vn a1 dest n
+    | Cle ->
+        if Int64.eq n (Int64.repr Int64.max_signed) then
+          let l = loadimm32 vn dest Int.one in
+          let r, l' = extract_arg l in
+          addinst vn (OEmayundef MUlong) [ a1; r ] dest :: l'
+        else sltimm64 vn a1 dest (Int64.add n Int64.one)
+    | _ ->
+        let r = r2pi () in
+        let l = loadimm64 vn r n in
+        let r', l' = extract_arg l in
+        cond_int64s vn false cmp a1 r' dest @ l'
+
+let expanse_condimm_int64u vn cmp a1 n dest =
+  if Int64.eq n Int64.zero then cond_int64u vn true cmp a1 a1 dest
+  else
+    match cmp with
+    | Clt -> sltuimm64 vn a1 dest n
+    | _ ->
+        let r = r2pi () in
+        let l = loadimm64 vn r n in
+        let r', l' = extract_arg l in
+        cond_int64u vn false cmp a1 r' dest @ l'
+
+let expanse_cond_fp vn cnot fn_cond cmp f1 f2 dest =
+  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 dest in
+  if normal' then insn
+  else
+    let r', l = extract_arg insn in
+    addinst vn (OExoriw Int.one) [ r' ] dest :: l
+
 
 (** Return olds args if the CSE numbering is empty *)
 
@@ -256,8 +528,7 @@ let rec gen_btl_list vn exp =
       let args = get_arguments vn vals args in
       let inst = Bop (op, args, rd, iinfo) in
       inst :: gen_btl_list vn k
-  | [ Sexp (rd, Smove, args, iinfo) ] ->
-      [ Bop (Omove, args, rd, iinfo) ]
+  | [ Sexp (rd, Smove, args, iinfo) ] -> [ Bop (Omove, args, rd, iinfo) ]
   | [ Scond (cond, args, succ1, succ2, iinfo) ] ->
       [ Bcond (cond, args, succ1, succ2, iinfo) ]
   | [] -> []
@@ -277,7 +548,62 @@ let expanse_list li =
          match i with
          | Bop (Ocmp (Ccomp c), a1 :: a2 :: nil, dest, iinfo) ->
              debug "Bop/Ccomp\n";
-             exp := cond_int32s vn false c a1 a2 dest iinfo;
+             exp := cond_int32s vn false c a1 a2 dest;
+             exp := extract_final vn !exp dest;
+             was_exp := true
+         | Bop (Ocmp (Ccompu c), a1 :: a2 :: nil, dest, iinfo) ->
+             debug "Bop/Ccompu\n";
+             exp := cond_int32u vn false c a1 a2 dest;
+             exp := extract_final vn !exp dest;
+             was_exp := true
+         | Bop (Ocmp (Ccompimm (c, imm)), a1 :: nil, dest, iinfo) ->
+             debug "Bop/Ccompimm\n";
+             exp := expanse_condimm_int32s vn c a1 imm dest;
+             exp := extract_final vn !exp dest;
+             was_exp := true
+         | Bop (Ocmp (Ccompuimm (c, imm)), a1 :: nil, dest, iinfo) ->
+             debug "Bop/Ccompuimm\n";
+             exp := expanse_condimm_int32u vn c a1 imm dest;
+             exp := extract_final vn !exp dest;
+             was_exp := true
+         | Bop (Ocmp (Ccompl c), a1 :: a2 :: nil, dest, iinfo) ->
+             debug "Bop/Ccompl\n";
+             exp := cond_int64s vn false c a1 a2 dest;
+             exp := extract_final vn !exp dest;
+             was_exp := true
+         | Bop (Ocmp (Ccomplu c), a1 :: a2 :: nil, dest, iinfo) ->
+             debug "Bop/Ccomplu\n";
+             exp := cond_int64u vn false c a1 a2 dest;
+             exp := extract_final vn !exp dest;
+             was_exp := true
+         | Bop (Ocmp (Ccomplimm (c, imm)), a1 :: nil, dest, iinfo) ->
+             debug "Bop/Ccomplimm\n";
+             exp := expanse_condimm_int64s vn c a1 imm dest;
+             exp := extract_final vn !exp dest;
+             was_exp := true
+         | Bop (Ocmp (Ccompluimm (c, imm)), a1 :: nil, dest, iinfo) ->
+             debug "Bop/Ccompluimm\n";
+             exp := expanse_condimm_int64u vn c a1 imm dest;
+             exp := extract_final vn !exp dest;
+             was_exp := true
+         | Bop (Ocmp (Ccompf c), f1 :: f2 :: nil, dest, iinfo) ->
+             debug "Bop/Ccompf\n";
+             exp := expanse_cond_fp vn false cond_float c f1 f2 dest;
+             exp := extract_final vn !exp dest;
+             was_exp := true
+         | Bop (Ocmp (Cnotcompf c), f1 :: f2 :: nil, dest, iinfo) ->
+             debug "Bop/Cnotcompf\n";
+             exp := expanse_cond_fp vn true cond_float c f1 f2 dest;
+             exp := extract_final vn !exp dest;
+             was_exp := true
+         | Bop (Ocmp (Ccompfs c), f1 :: f2 :: nil, dest, iinfo) ->
+             debug "Bop/Ccompfs\n";
+             exp := expanse_cond_fp vn false cond_single c f1 f2 dest;
+             exp := extract_final vn !exp dest;
+             was_exp := true
+         | Bop (Ocmp (Cnotcompfs c), f1 :: f2 :: nil, dest, iinfo) ->
+             debug "Bop/Cnotcompfs\n";
+             exp := expanse_cond_fp vn true cond_single c f1 f2 dest;
              exp := extract_final vn !exp dest;
              was_exp := true
          | _ -> ());
@@ -292,19 +618,22 @@ let expanse_list li =
               (* TODO gourdinl empty numb BF? vn := empty_numbering ()*)
           | _ -> ());
           i :: expanse_list_rec li')
-        else
-          gen_btl_list vn !exp @ expanse_list_rec li'
+        else gen_btl_list vn (List.rev !exp) @ expanse_list_rec li'
   in
   expanse_list_rec li
 
 let expanse n ibf btl =
-  debug_flag := true;
+  (*debug_flag := true;*)
   let lib = iblock_to_list ibf.entry in
   let new_lib = expanse_list lib in
-  let ibf' = { entry = list_to_iblock new_lib;
-               input_regs = ibf.input_regs;
-               binfo = ibf.binfo } in
-  debug_flag := false;
+  let ibf' =
+    {
+      entry = list_to_iblock new_lib;
+      input_regs = ibf.input_regs;
+      binfo = ibf.binfo;
+    }
+  in
+  (*debug_flag := false;*)
   PTree.set n ibf' btl
 
 (** Form a list containing both sources and destination regs of a block *)
@@ -315,16 +644,14 @@ let rec get_regs_ib = function
   | Bop (_, args, dest, _) -> dest :: args
   | Bload (_, _, _, args, dest, _) -> dest :: args
   | Bstore (_, _, args, src, _) -> src :: args
-  | Bcond (_, args, ib1, ib2, _) -> 
-      get_regs_ib ib1 @ get_regs_ib ib2 @ args
-  | Bseq (ib1, ib2) ->
-      get_regs_ib ib1 @ get_regs_ib ib2
-  | BF (Breturn (Some r), _) -> [r]
+  | Bcond (_, args, ib1, ib2, _) -> get_regs_ib ib1 @ get_regs_ib ib2 @ args
+  | Bseq (ib1, ib2) -> get_regs_ib ib1 @ get_regs_ib ib2
+  | BF (Breturn (Some r), _) -> [ r ]
   | BF (Bcall (_, t, args, dest, _), _) -> dest :: (get_regindent t @ args)
-  | BF (Btailcall (_, t, args), _) -> (get_regindent t @ args)
-  | BF (Bbuiltin (_, args, dest, _), _) -> 
+  | BF (Btailcall (_, t, args), _) -> get_regindent t @ args
+  | BF (Bbuiltin (_, args, dest, _), _) ->
       AST.params_of_builtin_res dest @ AST.params_of_builtin_args args
-  | BF (Bjumptable (arg, _), _) -> [arg]
+  | BF (Bjumptable (arg, _), _) -> [ arg ]
   | _ -> []
 
 let rec find_last_reg = function
-- 
cgit