Merge remote-tracking branch 'origin/riscv-work' into riscv-work-fpinit-stillexp

1 files changed, 141 insertions, 68 deletions

diff --git a/riscV/ExpansionOracle.ml b/riscV/ExpansionOracle.ml
index 23e3c38e..a61e5c95 100644
--- a/riscV/ExpansionOracle.ml
+++ b/riscV/ExpansionOracle.ml
@@ -20,14 +20,21 @@ open Asmgen
 open DebugPrint
 open RTLpath
 open! Integers
+open Camlcoq
+
+type sop = Sop of operation * P.t list
+
+type sval = Si of RTL.instruction | Sr of P.t
 
 let reg = ref 1
 
 let node = ref 1
 
-let r2p () = Camlcoq.P.of_int !reg
+let p2i r = P.to_int r
 
-let n2p () = Camlcoq.P.of_int !node
+let r2p () = P.of_int !reg
+
+let n2p () = P.of_int !node
 
 let r2pi () =
   reg := !reg + 1;
@@ -39,30 +46,69 @@ let n2pi () =
 
 type immt = Xoriw | Xoril | Sltiw | Sltiuw | Sltil | Sltiul
 
-let load_hilo32 a1 dest hi lo succ is_long k =
-  if Int.eq lo Int.zero then Iop (OEluiw (hi, is_long), [ a1 ], dest, succ) :: k
+let find_or_addnmove op args rd succ map_consts =
+  let sop = Sop (op, args) in
+  match Hashtbl.find_opt map_consts sop with
+  | Some r ->
+      Sr (P.of_int r)
+  | None ->
+      Hashtbl.add map_consts sop (p2i rd);
+      Si (Iop (op, args, rd, succ))
+
+let build_head_tuple head sv =
+  match sv with Si i -> (head @ [ i ], None) | Sr r -> (head, Some r)
+
+let load_hilo32 dest hi lo succ map_consts =
+  let op1 = OEluiw hi in
+  if Int.eq lo Int.zero then
+    let sv = find_or_addnmove op1 [] dest succ map_consts in
+    build_head_tuple [] sv
   else
     let r = r2pi () in
-    Iop (OEluiw (hi, is_long), [ a1 ], r, n2pi ())
-    :: Iop (Oaddimm lo, [ r ], dest, succ) :: k
-
-let load_hilo64 a1 dest hi lo succ k =
-  if Int64.eq lo Int64.zero then Iop (OEluil hi, [ a1 ], dest, succ) :: k
+    let op2 = Oaddimm lo in
+    match find_or_addnmove op1 [] r (n2pi ()) map_consts with
+    | Si i ->
+        let sv = find_or_addnmove op2 [ r ] dest succ map_consts in
+        build_head_tuple [ i ] sv
+    | Sr r' ->
+        let sv = find_or_addnmove op2 [ r' ] dest succ map_consts in
+        build_head_tuple [] sv
+
+let load_hilo64 dest hi lo succ map_consts =
+  let op1 = OEluil hi in
+  if Int64.eq lo Int64.zero then
+    let sv = find_or_addnmove op1 [] dest succ map_consts in
+    build_head_tuple [] sv
   else
     let r = r2pi () in
-    Iop (OEluil hi, [ a1 ], r, n2pi ())
-    :: Iop (Oaddlimm lo, [ r ], dest, succ) :: k
-
-let loadimm32 a1 dest n succ is_long k =
+    let op2 = Oaddlimm lo in
+    match find_or_addnmove op1 [] r (n2pi ()) map_consts with
+    | Si i ->
+        let sv = find_or_addnmove op2 [ r ] dest succ map_consts in
+        build_head_tuple [ i ] sv
+    | Sr r' ->
+        let sv = find_or_addnmove op2 [ r' ] dest succ map_consts in
+        build_head_tuple [] sv
+
+let loadimm32 dest n succ map_consts =
   match make_immed32 n with
-  | Imm32_single imm -> Iop (OEaddiwr0 (imm, is_long), [ a1 ], dest, succ) :: k
-  | Imm32_pair (hi, lo) -> load_hilo32 a1 dest hi lo succ is_long k
+  | Imm32_single imm ->
+      let op1 = OEaddiwr0 imm in
+      let sv = find_or_addnmove op1 [] dest succ map_consts in
+      build_head_tuple [] sv
+  | Imm32_pair (hi, lo) -> load_hilo32 dest hi lo succ map_consts
 
-let loadimm64 a1 dest n succ k =
+let loadimm64 dest n succ map_consts =
   match make_immed64 n with
-  | Imm64_single imm -> Iop (OEaddilr0 imm, [ a1 ], dest, succ) :: k
-  | Imm64_pair (hi, lo) -> load_hilo64 a1 dest hi lo succ k
-  | Imm64_large imm -> Iop (OEloadli imm, [], dest, succ) :: k
+  | Imm64_single imm ->
+      let op1 = OEaddilr0 imm in
+      let sv = find_or_addnmove op1 [] dest succ map_consts in
+      build_head_tuple [] sv
+  | Imm64_pair (hi, lo) -> load_hilo64 dest hi lo succ map_consts
+  | Imm64_large imm ->
+      let op1 = OEloadli imm in
+      let sv = find_or_addnmove op1 [] dest succ map_consts in
+      build_head_tuple [] sv
 
 let get_opimm imm = function
   | Xoriw -> OExoriw imm
@@ -72,32 +118,42 @@ let get_opimm imm = function
   | Sltil -> OEsltil imm
   | Sltiul -> OEsltiul imm
 
-let opimm32 a1 dest n succ is_long k op opimm =
+let unzip_head_tuple ht r = match ht with l, Some r' -> r' | l, None -> r
+
+let opimm32 a1 dest n succ k op opimm map_consts =
   match make_immed32 n with
   | Imm32_single imm -> Iop (get_opimm imm opimm, [ a1 ], dest, succ) :: k
   | Imm32_pair (hi, lo) ->
       let r = r2pi () in
-      load_hilo32 a1 r hi lo (n2pi ()) is_long
-        (Iop (op, [ a1; r ], dest, succ) :: k)
+      let ht = load_hilo32 r hi lo (n2pi ()) map_consts in
+      let r' = unzip_head_tuple ht r in
+      fst ht @ Iop (op, [ a1; r' ], dest, succ) :: k
 
-let opimm64 a1 dest n succ k op opimm =
+let opimm64 a1 dest n succ k op opimm map_consts =
   match make_immed64 n with
   | Imm64_single imm -> Iop (get_opimm imm opimm, [ a1 ], dest, succ) :: k
   | Imm64_pair (hi, lo) ->
       let r = r2pi () in
-      load_hilo64 a1 r hi lo (n2pi ()) (Iop (op, [ a1; r ], dest, succ) :: k)
+      let ht = load_hilo64 r hi lo (n2pi ()) map_consts in
+      let r' = unzip_head_tuple ht r in
+      fst ht @ Iop (op, [ a1; r' ], dest, succ) :: k
   | Imm64_large imm ->
       let r = r2pi () in
-      Iop (OEloadli imm, [], r, n2pi ()) :: Iop (op, [ a1; r ], dest, succ) :: k
+      let op1 = OEloadli imm in
+      let inode = n2pi () in
+      let sv = find_or_addnmove op1 [] r inode map_consts in
+      let ht = build_head_tuple [] sv in
+      let r' = unzip_head_tuple ht r in
+      fst ht @ Iop (op, [ a1; r' ], dest, succ) :: k
 
-let xorimm32 a1 dest n succ is_long k =
-  opimm32 a1 dest n succ is_long k Oxor Xoriw
+let xorimm32 a1 dest n succ k map_consts =
+  opimm32 a1 dest n succ k Oxor Xoriw map_consts
 
-let sltimm32 a1 dest n succ is_long k =
-  opimm32 a1 dest n succ is_long k (OEsltw None) Sltiw
+let sltimm32 a1 dest n succ k map_consts =
+  opimm32 a1 dest n succ k (OEsltw None) Sltiw map_consts
 
-let sltuimm32 a1 dest n succ is_long k =
-  opimm32 a1 dest n succ is_long k (OEsltuw None) Sltiuw
+let sltuimm32 a1 dest n succ k map_consts =
+  opimm32 a1 dest n succ k (OEsltuw None) Sltiuw map_consts
 
 let xorimm64 a1 dest n succ k = opimm64 a1 dest n succ k Oxorl Xoril
 
@@ -233,85 +289,101 @@ let cond_single cmp f1 f2 dest succ =
   | Cgt -> Iop (OEflts, [ f2; f1 ], dest, succ)
   | Cge -> Iop (OEfles, [ f2; f1 ], dest, succ)
 
-let expanse_cbranchimm_int32s cmp a1 n info succ1 succ2 k =
+let expanse_cbranchimm_int32s cmp a1 n info succ1 succ2 k map_consts =
   if Int.eq n Int.zero then cbranch_int32s true cmp a1 a1 info succ1 succ2 k
   else
     let r = r2pi () in
-    loadimm32 a1 r n (n2pi ()) false
-      (cbranch_int32s false cmp a1 r info succ1 succ2 k)
+    let ht = loadimm32 r n (n2pi ()) map_consts in
+    let r' = unzip_head_tuple ht r in
+    fst ht @ cbranch_int32s false cmp a1 r' info succ1 succ2 k
 
-let expanse_cbranchimm_int32u cmp a1 n info succ1 succ2 k =
+let expanse_cbranchimm_int32u cmp a1 n info succ1 succ2 k map_consts =
   if Int.eq n Int.zero then cbranch_int32u true cmp a1 a1 info succ1 succ2 k
   else
     let r = r2pi () in
-    loadimm32 a1 r n (n2pi ()) false
-      (cbranch_int32u false cmp a1 r info succ1 succ2 k)
+    let ht = loadimm32 r n (n2pi ()) map_consts in
+    let r' = unzip_head_tuple ht r in
+    fst ht @ cbranch_int32u false cmp a1 r' info succ1 succ2 k
 
-let expanse_cbranchimm_int64s cmp a1 n info succ1 succ2 k =
+let expanse_cbranchimm_int64s cmp a1 n info succ1 succ2 k map_consts =
   if Int64.eq n Int64.zero then cbranch_int64s true cmp a1 a1 info succ1 succ2 k
   else
     let r = r2pi () in
-    loadimm64 a1 r n (n2pi ())
-      (cbranch_int64s false cmp a1 r info succ1 succ2 k)
+    let ht = loadimm64 r n (n2pi ()) map_consts in
+    let r' = unzip_head_tuple ht r in
+    fst ht @ cbranch_int64s false cmp a1 r' info succ1 succ2 k
 
-let expanse_cbranchimm_int64u cmp a1 n info succ1 succ2 k =
+let expanse_cbranchimm_int64u cmp a1 n info succ1 succ2 k map_consts =
   if Int64.eq n Int64.zero then cbranch_int64u true cmp a1 a1 info succ1 succ2 k
   else
     let r = r2pi () in
-    loadimm64 a1 r n (n2pi ())
-      (cbranch_int64u false cmp a1 r info succ1 succ2 k)
+    let ht = loadimm64 r n (n2pi ()) map_consts in
+    let r' = unzip_head_tuple ht r in
+    fst ht @ cbranch_int64u false cmp a1 r' info succ1 succ2 k
 
-let expanse_condimm_int32s cmp a1 n dest succ k =
+let expanse_condimm_int32s cmp a1 n dest succ k map_consts =
   if Int.eq n Int.zero then cond_int32s true cmp a1 a1 dest succ k
   else
     match cmp with
     | Ceq | Cne ->
         let r = r2pi () in
-        xorimm32 a1 r n (n2pi ()) false (cond_int32s true cmp r r dest succ k)
-    | Clt -> sltimm32 a1 dest n succ false k
+        xorimm32 a1 r n (n2pi ())
+          (cond_int32s true cmp r r dest succ k)
+          map_consts
+    | Clt -> sltimm32 a1 dest n succ k map_consts
     | Cle ->
         if Int.eq n (Int.repr Int.max_signed) then
-          loadimm32 a1 dest Int.one succ false k
-        else sltimm32 a1 dest (Int.add n Int.one) succ false k
+          let ht = loadimm32 dest Int.one succ map_consts in
+          fst ht @ k
+        else sltimm32 a1 dest (Int.add n Int.one) succ k map_consts
     | _ ->
         let r = r2pi () in
-        loadimm32 a1 r n (n2pi ()) false
-          (cond_int32s false cmp a1 r dest succ k)
+        let ht = loadimm32 r n (n2pi ()) map_consts in
+        let r' = unzip_head_tuple ht r in
+        fst ht @ cond_int32s false cmp a1 r' dest succ k
 
-let expanse_condimm_int32u cmp a1 n dest succ k =
+let expanse_condimm_int32u cmp a1 n dest succ k map_consts =
   if Int.eq n Int.zero then cond_int32u true cmp a1 a1 dest succ k
   else
     match cmp with
-    | Clt -> sltuimm32 a1 dest n succ false k
+    | Clt -> sltuimm32 a1 dest n succ k map_consts
     | _ ->
         let r = r2pi () in
-        loadimm32 a1 r n (n2pi ()) false
-          (cond_int32u false cmp a1 r dest succ k)
+        let ht = loadimm32 r n (n2pi ()) map_consts in
+        let r' = unzip_head_tuple ht r in
+        fst ht @ cond_int32u false cmp a1 r' dest succ k
 
-let expanse_condimm_int64s cmp a1 n dest succ k =
+let expanse_condimm_int64s cmp a1 n dest succ k map_consts =
   if Int64.eq n Int64.zero then cond_int64s true cmp a1 a1 dest succ k
   else
     match cmp with
     | Ceq | Cne ->
         let r = r2pi () in
-        xorimm64 a1 r n (n2pi ()) (cond_int64s true cmp r r dest succ k)
-    | Clt -> sltimm64 a1 dest n succ k
+        xorimm64 a1 r n (n2pi ())
+          (cond_int64s true cmp r r dest succ k)
+          map_consts
+    | Clt -> sltimm64 a1 dest n succ k map_consts
     | Cle ->
         if Int64.eq n (Int64.repr Int64.max_signed) then
-          loadimm32 a1 dest Int.one succ true k
-        else sltimm64 a1 dest (Int64.add n Int64.one) succ k
+          let ht = loadimm32 dest Int.one succ map_consts in
+          fst ht @ k
+        else sltimm64 a1 dest (Int64.add n Int64.one) succ k map_consts
     | _ ->
         let r = r2pi () in
-        loadimm64 a1 r n (n2pi ()) (cond_int64s false cmp a1 r dest succ k)
+        let ht = loadimm64 r n (n2pi ()) map_consts in
+        let r' = unzip_head_tuple ht r in
+        fst ht @ cond_int64s false cmp a1 r' dest succ k
 
-let expanse_condimm_int64u cmp a1 n dest succ k =
+let expanse_condimm_int64u cmp a1 n dest succ k map_consts =
   if Int64.eq n Int64.zero then cond_int64u true cmp a1 a1 dest succ k
   else
     match cmp with
-    | Clt -> sltuimm64 a1 dest n succ k
+    | Clt -> sltuimm64 a1 dest n succ k map_consts
     | _ ->
         let r = r2pi () in
-        loadimm64 a1 r n (n2pi ()) (cond_int64u false cmp a1 r dest succ k)
+        let ht = loadimm64 r n (n2pi ()) map_consts in
+        let r' = unzip_head_tuple ht r in
+        fst ht @ cond_int64u false cmp a1 r' dest succ k
 
 let expanse_cond_fp cnot fn_cond cmp f1 f2 dest succ k =
   let normal = is_normal_cmp cmp in
@@ -368,12 +440,12 @@ let write_pathmap initial esize pm' =
 let rec write_tree exp current code' new_order =
   match exp with
   | (Iop (_, _, _, succ) as inst) :: k ->
-      code' := PTree.set (Camlcoq.P.of_int current) inst !code';
-      new_order := Camlcoq.P.of_int current :: !new_order;
+      code' := PTree.set (P.of_int current) inst !code';
+      new_order := P.of_int current :: !new_order;
       write_tree k (current - 1) code' new_order
   | (Icond (_, _, succ1, succ2, _) as inst) :: k ->
-      code' := PTree.set (Camlcoq.P.of_int current) inst !code';
-      new_order := Camlcoq.P.of_int current :: !new_order;
+      code' := PTree.set (P.of_int current) inst !code';
+      new_order := P.of_int current :: !new_order;
       write_tree k (current - 1) code' new_order
   | [] -> ()
   | _ -> failwith "ExpansionOracle.write_tree: inconsistent instruction."
@@ -387,6 +459,7 @@ let expanse (sb : superblock) code pm =
   let was_exp = ref false in
   let code' = ref code in
   let pm' = ref pm in
+  let map_consts = Hashtbl.create 100 in
   Array.iter
     (fun n ->
       begin (
@@ -558,7 +631,7 @@ let rec find_last_node_reg = function
       let rec traverse_list var = function
         | [] -> ()
         | e :: t ->
-            let e' = Camlcoq.P.to_int e in
+            let e' = p2i e in
             if e' > !var then var := e';
             traverse_list var t
       in