Try to save values in virtual registers during expansion

1 files changed, 100 insertions, 89 deletions

diff --git a/riscV/ExpansionOracle.ml b/riscV/ExpansionOracle.ml
index 41a2227b..95a300c5 100644
--- a/riscV/ExpansionOracle.ml
+++ b/riscV/ExpansionOracle.ml
@@ -29,6 +29,10 @@ let r2p () = Camlcoq.P.of_int !reg
 
 let n2p () = Camlcoq.P.of_int !node
 
+let r2pi () =
+  reg := !reg + 1;
+  r2p ()
+
 let n2pi () =
   node := !node + 1;
   n2p ()
@@ -36,27 +40,27 @@ 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
+  if Int.eq lo Int.zero then Iop (OEluiw (hi, is_long), [ a1 ], dest, succ) :: k
   else
-    Iop (OEluiw (hi, is_long), [a1], dest, n2pi ())
-    :: Iop (Oaddimm lo, [ dest ], dest, succ)
-    :: k
+    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
+  if Int64.eq lo Int64.zero then Iop (OEluil hi, [ a1 ], dest, succ) :: k
   else
-    Iop (OEluil hi, [a1], dest, n2pi ())
-    :: Iop (Oaddlimm lo, [ dest ], dest, succ)
-    :: k
+    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 =
   match make_immed32 n with
-  | Imm32_single imm -> Iop (OEaddiwr0 (imm, is_long), [a1], dest, succ) :: k
+  | 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
 
 let loadimm64 a1 dest n succ k =
   match make_immed64 n with
-  | Imm64_single imm -> Iop (OEaddilr0 imm, [a1], dest, succ) :: k
+  | 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
 
@@ -72,28 +76,28 @@ let opimm32 a1 dest n succ is_long k op opimm =
   match make_immed32 n with
   | Imm32_single imm -> Iop (get_opimm imm opimm, [ a1 ], dest, succ) :: k
   | Imm32_pair (hi, lo) ->
-      reg := !reg + 1;
-      load_hilo32 a1 (r2p ()) hi lo (n2pi ()) is_long
-        (Iop (op, [ a1; r2p () ], dest, succ) :: k)
+      let r = r2pi () in
+      load_hilo32 a1 r hi lo (n2pi ()) is_long
+        (Iop (op, [ a1; r ], dest, succ) :: k)
 
 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 a1 (r2p ()) hi lo (n2pi ())
-        (Iop (op, [ a1; r2p () ], dest, succ) :: k)
+      let r = r2pi () in
+      load_hilo64 a1 r hi lo (n2pi ()) (Iop (op, [ a1; r ], dest, succ) :: k)
   | Imm64_large imm ->
-      reg := !reg + 1;
-      Iop (OEloadli imm, [], r2p (), n2pi ())
-      :: Iop (op, [ a1; r2p () ], dest, succ)
-      :: k
+      let r = r2pi () in
+      Iop (OEloadli imm, [], r, n2pi ()) :: 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 is_long k =
+  opimm32 a1 dest n succ is_long k Oxor Xoriw
 
-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 is_long k =
+  opimm32 a1 dest n succ is_long k (OEsltw None) Sltiw
 
-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 is_long k =
+  opimm32 a1 dest n succ is_long k (OEsltuw None) Sltiuw
 
 let xorimm64 a1 dest n succ k = opimm64 a1 dest n succ k Oxorl Xoril
 
@@ -152,14 +156,14 @@ let cond_int32s is_x0 cmp a1 a2 dest succ k =
   | Cne -> Iop (OEsnew optR0, [ a1; a2 ], dest, succ) :: k
   | Clt -> Iop (OEsltw optR0, [ a1; a2 ], dest, succ) :: k
   | Cle ->
-      Iop (OEsltw optR0, [ a2; a1 ], dest, n2pi ())
-      :: Iop (OExoriw Int.one, [ dest ], dest, succ)
-      :: k
+      let r = r2pi () in
+      Iop (OEsltw optR0, [ a2; a1 ], r, n2pi ())
+      :: Iop (OExoriw Int.one, [ r ], dest, succ) :: k
   | Cgt -> Iop (OEsltw optR0, [ a2; a1 ], dest, succ) :: k
   | Cge ->
-      Iop (OEsltw optR0, [ a1; a2 ], dest, n2pi ())
-      :: Iop (OExoriw Int.one, [ dest ], dest, succ)
-      :: k
+      let r = r2pi () in
+      Iop (OEsltw optR0, [ a1; a2 ], r, n2pi ())
+      :: Iop (OExoriw Int.one, [ r ], dest, succ) :: k
 
 let cond_int32u is_x0 cmp a1 a2 dest succ k =
   let optR0 = make_optR0 is_x0 (is_inv_cmp cmp) in
@@ -168,14 +172,14 @@ let cond_int32u is_x0 cmp a1 a2 dest succ k =
   | Cne -> Iop (OEsneuw optR0, [ a1; a2 ], dest, succ) :: k
   | Clt -> Iop (OEsltuw optR0, [ a1; a2 ], dest, succ) :: k
   | Cle ->
-      Iop (OEsltuw optR0, [ a2; a1 ], dest, n2pi ())
-      :: Iop (OExoriw Int.one, [ dest ], dest, succ)
-      :: k
+      let r = r2pi () in
+      Iop (OEsltuw optR0, [ a2; a1 ], r, n2pi ())
+      :: Iop (OExoriw Int.one, [ r ], dest, succ) :: k
   | Cgt -> Iop (OEsltuw optR0, [ a2; a1 ], dest, succ) :: k
   | Cge ->
-      Iop (OEsltuw optR0, [ a1; a2 ], dest, n2pi ())
-      :: Iop (OExoriw Int.one, [ dest ], dest, succ)
-      :: k
+      let r = r2pi () in
+      Iop (OEsltuw optR0, [ a1; a2 ], r, n2pi ())
+      :: Iop (OExoriw Int.one, [ r ], dest, succ) :: k
 
 let cond_int64s is_x0 cmp a1 a2 dest succ k =
   let optR0 = make_optR0 is_x0 (is_inv_cmp cmp) in
@@ -184,14 +188,14 @@ let cond_int64s is_x0 cmp a1 a2 dest succ k =
   | Cne -> Iop (OEsnel optR0, [ a1; a2 ], dest, succ) :: k
   | Clt -> Iop (OEsltl optR0, [ a1; a2 ], dest, succ) :: k
   | Cle ->
-      Iop (OEsltl optR0, [ a2; a1 ], dest, n2pi ())
-      :: Iop (OExoriw Int.one, [ dest ], dest, succ)
-      :: k
+      let r = r2pi () in
+      Iop (OEsltl optR0, [ a2; a1 ], r, n2pi ())
+      :: Iop (OExoriw Int.one, [ r ], dest, succ) :: k
   | Cgt -> Iop (OEsltl optR0, [ a2; a1 ], dest, succ) :: k
   | Cge ->
-      Iop (OEsltl optR0, [ a1; a2 ], dest, n2pi ())
-      :: Iop (OExoriw Int.one, [ dest ], dest, succ)
-      :: k
+      let r = r2pi () in
+      Iop (OEsltl optR0, [ a1; a2 ], r, n2pi ())
+      :: Iop (OExoriw Int.one, [ r ], dest, succ) :: k
 
 let cond_int64u is_x0 cmp a1 a2 dest succ k =
   let optR0 = make_optR0 is_x0 (is_inv_cmp cmp) in
@@ -200,14 +204,14 @@ let cond_int64u is_x0 cmp a1 a2 dest succ k =
   | Cne -> Iop (OEsneul optR0, [ a1; a2 ], dest, succ) :: k
   | Clt -> Iop (OEsltul optR0, [ a1; a2 ], dest, succ) :: k
   | Cle ->
-      Iop (OEsltul optR0, [ a2; a1 ], dest, n2pi ())
-      :: Iop (OExoriw Int.one, [ dest ], dest, succ)
-      :: k
+      let r = r2pi () in
+      Iop (OEsltul optR0, [ a2; a1 ], r, n2pi ())
+      :: Iop (OExoriw Int.one, [ r ], dest, succ) :: k
   | Cgt -> Iop (OEsltul optR0, [ a2; a1 ], dest, succ) :: k
   | Cge ->
-      Iop (OEsltul optR0, [ a1; a2 ], dest, n2pi ())
-      :: Iop (OExoriw Int.one, [ dest ], dest, succ)
-      :: k
+      let r = r2pi () in
+      Iop (OEsltul optR0, [ a1; a2 ], r, n2pi ())
+      :: Iop (OExoriw Int.one, [ r ], dest, succ) :: k
 
 let is_normal_cmp = function Cne -> false | _ -> true
 
@@ -231,47 +235,48 @@ let cond_single cmp f1 f2 dest succ =
 
 let expanse_cbranchimm_int32s cmp a1 n info succ1 succ2 k =
   if Int.eq n Int.zero then cbranch_int32s true cmp a1 a1 info succ1 succ2 k
-  else (
-    reg := !reg + 1;
-    loadimm32 a1 (r2p ()) n (n2pi ()) false
-      (cbranch_int32s false cmp a1 (r2p ()) 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 expanse_cbranchimm_int32u cmp a1 n info succ1 succ2 k =
   if Int.eq n Int.zero then cbranch_int32u true cmp a1 a1 info succ1 succ2 k
-  else (
-    reg := !reg + 1;
-    loadimm32 a1 (r2p ()) n (n2pi ()) false
-      (cbranch_int32u false cmp a1 (r2p ()) 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 expanse_cbranchimm_int64s cmp a1 n info succ1 succ2 k =
   if Int64.eq n Int64.zero then cbranch_int64s true cmp a1 a1 info succ1 succ2 k
-  else (
-    reg := !reg + 1;
-    loadimm64 a1 (r2p ()) n (n2pi ())
-      (cbranch_int64s false cmp a1 (r2p ()) 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 expanse_cbranchimm_int64u cmp a1 n info succ1 succ2 k =
   if Int64.eq n Int64.zero then cbranch_int64u true cmp a1 a1 info succ1 succ2 k
-  else (
-    reg := !reg + 1;
-    loadimm64 a1 (r2p ()) n (n2pi ())
-      (cbranch_int64u false cmp a1 (r2p ()) 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 expanse_condimm_int32s cmp a1 n dest succ k =
   if Int.eq n Int.zero then cond_int32s true cmp a1 a1 dest succ k
   else
     match cmp with
     | Ceq | Cne ->
-        xorimm32 a1 dest n (n2pi ()) false
-          (cond_int32s true cmp dest dest dest succ k)
+        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
     | Cle ->
-        if Int.eq n (Int.repr Int.max_signed) then loadimm32 a1 dest Int.one succ false k
+        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
     | _ ->
-        reg := !reg + 1;
-        loadimm32 a1 (r2p ()) n (n2pi ()) false
-          (cond_int32s false cmp a1 (r2p ()) dest succ k)
+        let r = r2pi () in
+        loadimm32 a1 r n (n2pi ()) false
+          (cond_int32s false cmp a1 r dest succ k)
 
 let expanse_condimm_int32u cmp a1 n dest succ k =
   if Int.eq n Int.zero then cond_int32u true cmp a1 a1 dest succ k
@@ -279,27 +284,25 @@ let expanse_condimm_int32u cmp a1 n dest succ k =
     match cmp with
     | Clt -> sltuimm32 a1 dest n succ false k
     | _ ->
-        reg := !reg + 1;
-        loadimm32 a1 (r2p ()) n (n2pi ()) false
-          (cond_int32u false cmp a1 (r2p ()) dest succ k)
+        let r = r2pi () in
+        loadimm32 a1 r n (n2pi ()) false
+          (cond_int32u false cmp a1 r dest succ k)
 
 let expanse_condimm_int64s cmp a1 n dest succ k =
   if Int64.eq n Int64.zero then cond_int64s true cmp a1 a1 dest succ k
   else
     match cmp with
     | Ceq | Cne ->
-        reg := !reg + 1;
-        xorimm64 a1 (r2p ()) n (n2pi ())
-          (cond_int64s true cmp (r2p ()) (r2p ()) dest succ k)
+        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
     | 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
     | _ ->
-        reg := !reg + 1;
-        loadimm64 a1 (r2p ()) n (n2pi ())
-          (cond_int64s false cmp a1 (r2p ()) dest succ k)
+        let r = r2pi () in
+        loadimm64 a1 r n (n2pi ()) (cond_int64s false cmp a1 r dest succ k)
 
 let expanse_condimm_int64u cmp a1 n dest succ k =
   if Int64.eq n Int64.zero then cond_int64u true cmp a1 a1 dest succ k
@@ -307,9 +310,8 @@ let expanse_condimm_int64u cmp a1 n dest succ k =
     match cmp with
     | Clt -> sltuimm64 a1 dest n succ k
     | _ ->
-        reg := !reg + 1;
-        loadimm64 a1 (r2p ()) n (n2pi ())
-          (cond_int64u false cmp a1 (r2p ()) dest succ k)
+        let r = r2pi () in
+        loadimm64 a1 r n (n2pi ()) (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
@@ -320,14 +322,14 @@ let expanse_cond_fp cnot fn_cond cmp f1 f2 dest succ k =
   :: (if normal' then k else Iop (OExoriw Int.one, [ dest ], dest, succ) :: k)
 
 let expanse_cbranch_fp cnot fn_cond cmp f1 f2 info succ1 succ2 k =
-  reg := !reg + 1;
+  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 cmp f1 f2 (r2p ()) (n2pi ()) in
+  let insn = fn_cond cmp f1 f2 r (n2pi ()) in
   insn
-  :: (if normal' then
-      Icond (CEbnew (Some false), [ r2p (); r2p () ], succ1, succ2, info)
-     else Icond (CEbeqw (Some false), [ r2p (); r2p () ], succ1, succ2, info))
+  ::
+  (if normal' then Icond (CEbnew (Some false), [ r; r ], succ1, succ2, info)
+  else Icond (CEbeqw (Some false), [ r; r ], succ1, succ2, info))
   :: k
 
 let get_regindent = function Coq_inr _ -> [] | Coq_inl r -> [ r ]
@@ -352,8 +354,15 @@ let write_initial_node initial code' new_order =
 
 let write_pathmap initial esize pm' =
   let path = get_some @@ PTree.get initial !pm' in
-  let npsize = Camlcoq.Nat.of_int (esize + (Camlcoq.Nat.to_int path.psize)) in
-  let path' = { psize = npsize; input_regs = path.input_regs; pre_output_regs = path.pre_output_regs; output_regs = path.output_regs } in
+  let npsize = Camlcoq.Nat.of_int (esize + Camlcoq.Nat.to_int path.psize) in
+  let path' =
+    {
+      psize = npsize;
+      input_regs = path.input_regs;
+      pre_output_regs = path.pre_output_regs;
+      output_regs = path.output_regs;
+    }
+  in
   pm' := PTree.set initial path' !pm'
 
 let rec write_tree exp current code' new_order =
@@ -500,7 +509,9 @@ let expanse (sb : superblock) code pm =
          let lives = PTree.get n !liveins in
          match lives with
          | Some lives ->
-             let new_branch_pc = Camlcoq.P.of_int (!node - ((List.length !exp) - 1)) in
+             let new_branch_pc =
+               Camlcoq.P.of_int (!node - (List.length !exp - 1))
+             in
              liveins := PTree.set new_branch_pc lives !liveins;
              liveins := PTree.remove n !liveins
          | _ -> ());