Ccomp for long

1 files changed, 166 insertions, 35 deletions

diff --git a/riscV/ExpansionOracle.ml b/riscV/ExpansionOracle.ml
index 4d587b12..c3f2cb3f 100644
--- a/riscV/ExpansionOracle.ml
+++ b/riscV/ExpansionOracle.ml
@@ -18,7 +18,7 @@ open RTL
 open Op
 open Asmgen
 open DebugPrint
-open PrintRTL
+(*open PrintRTL*)
 open! Integers
 
 let reg = ref 1
@@ -28,7 +28,7 @@ let r2p () = Camlcoq.P.of_int !reg
 let n2p () = Camlcoq.P.of_int !node
 let n2pi () = node := !node + 1; n2p()
 
-type immt = Xori | Slti
+type immt = Xoriw | Xoril | Sltiw | Sltiuw | Sltil | Sltiul
 
 let load_hilo32 dest hi lo succ k =
   if Int.eq lo Int.zero then
@@ -36,15 +36,32 @@ let load_hilo32 dest hi lo succ k =
   else (
       Iop (OEluiw hi, [], dest, n2pi()) :: (Iop (Oaddimm lo, [dest], dest, succ)) :: k)
 
+let load_hilo64 dest hi lo succ k =
+  if Int64.eq lo Int64.zero then
+    Iop (OEluil hi, [], dest, succ) :: k
+  else (
+      Iop (OEluil hi, [], dest, n2pi()) :: (Iop (Oaddlimm lo, [dest], dest, succ)) :: k)
+
 let loadimm32 dest n succ k =
   match make_immed32 n with
   | Imm32_single imm ->
       Iop (OEaddiwr0 imm, [], dest, succ) :: k
   | Imm32_pair (hi, lo) -> load_hilo32 dest hi lo succ k
 
+let loadimm64 dest n succ k =
+  match make_immed64 n with
+  | Imm64_single imm ->
+      Iop (OEaddilr0 imm, [], dest, succ) :: k
+  | Imm64_pair (hi, lo) -> load_hilo64 dest hi lo succ k
+  | Imm64_large imm -> Iop (OEloadli imm, [], dest, succ) :: k
+
 let get_opimm imm = function
-  | Xori -> OExoriw imm
-  | Slti -> OEsltiw imm
+  | Xoriw -> OExoriw imm
+  | Sltiw -> OEsltiw imm
+  | Sltiuw -> OEsltiuw imm
+  | Xoril -> OExoril imm
+  | Sltil -> OEsltil imm
+  | Sltiul -> OEsltiul imm
 
 let opimm32 a1 dest n succ k op opimm =
   match make_immed32 n with
@@ -54,8 +71,23 @@ let opimm32 a1 dest n succ k op opimm =
       reg := !reg + 1;
       load_hilo32 (r2p()) hi lo (n2pi()) (Iop (op, [a1;r2p()], dest, succ) :: k)
 
-let xorimm32 a1 dest n succ k = opimm32 a1 dest n succ k Oxor Xori
-let sltimm32 a1 dest n succ k = opimm32 a1 dest n succ k (OEsltw None) Slti
+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 (r2p()) hi lo (n2pi()) (Iop (op, [a1;r2p()], dest, succ) :: k)
+  | Imm64_large imm  ->
+      reg := !reg + 1;
+      Iop (OEloadli imm, [], r2p(), n2pi()) :: Iop (op, [a1;r2p()], dest, succ) :: k
+
+let xorimm32 a1 dest n succ k = opimm32 a1 dest n succ k Oxor Xoriw
+let sltimm32 a1 dest n succ k = opimm32 a1 dest n succ k (OEsltw None) Sltiw
+let sltuimm32 a1 dest n succ k = opimm32 a1 dest n succ k (OEsltuw None) Sltiuw
+let xorimm64 a1 dest n succ k = opimm64 a1 dest n succ k Oxorl Xoril
+let sltimm64 a1 dest n succ k = opimm64 a1 dest n succ k (OEsltl None) Sltil
+let sltuimm64 a1 dest n succ k = opimm64 a1 dest n succ k (OEsltul None) Sltiul
 
 let cond_int32s_x0 cmp a1 dest succ k =
   match cmp with
@@ -75,6 +107,60 @@ let cond_int32s_reg cmp a1 a2 dest succ k =
   | Cgt -> Iop (OEsltw None, [a2;a1], dest, succ) :: k
   | Cge -> Iop (OEsltw None, [a1;a2], dest, n2pi()) :: Iop (OExoriw Int.one, [dest], dest, succ) :: k
 
+let cond_int32u_x0 cmp a1 dest succ k =
+  match cmp with
+  | Ceq -> Iop (OEseqw (Some false), [a1;a1], dest, succ) :: k
+  | Cne -> Iop (OEsnew (Some false), [a1;a1], dest, succ) :: k
+  | Clt -> Iop (OEsltuw (Some false), [a1;a1], dest, succ) :: k
+  | Cle -> Iop (OEsltuw (Some true), [a1;a1], dest, n2pi()) :: Iop (OExoriw Int.one, [dest], dest, succ) :: k
+  | Cgt -> Iop (OEsltuw (Some true), [a1;a1], dest, succ) :: k
+  | Cge -> Iop (OEsltuw (Some false), [a1;a1], dest, n2pi()) :: Iop (OExoriw Int.one, [dest], 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 cond_int64s_x0 cmp a1 dest succ k =
+  match cmp with
+  | Ceq -> Iop (OEseql (Some false), [a1;a1], dest, succ) :: k
+  | Cne -> Iop (OEsnel (Some false), [a1;a1], dest, succ) :: k
+  | Clt -> Iop (OEsltl (Some false), [a1;a1], dest, succ) :: k
+  | Cle -> Iop (OEsltl (Some true), [a1;a1], dest, n2pi()) :: Iop (OExoriw Int.one, [dest], dest, succ) :: k
+  | Cgt -> Iop (OEsltl (Some true), [a1;a1], dest, succ) :: k
+  | Cge -> Iop (OEsltl (Some false), [a1;a1], dest, n2pi()) :: Iop (OExoriw Int.one, [dest], dest, succ) :: k
+
+let cond_int64s_reg cmp a1 a2 dest succ k =
+  match cmp with
+  | Ceq -> Iop (OEseql None, [a1;a2], dest, succ) :: k
+  | Cne -> Iop (OEsnel None, [a1;a2], dest, succ) :: k
+  | Clt -> Iop (OEsltl None, [a1;a2], dest, succ) :: k
+  | Cle -> Iop (OEsltl None, [a2;a1], dest, n2pi()) :: Iop (OExoriw Int.one, [dest], dest, succ) :: k
+  | Cgt -> Iop (OEsltl None, [a2;a1], dest, succ) :: k
+  | Cge -> Iop (OEsltl None, [a1;a2], dest, n2pi()) :: Iop (OExoriw Int.one, [dest], dest, succ) :: k
+
+let cond_int64u_x0 cmp a1 dest succ k =
+  match cmp with
+  | Ceq -> Iop (OEseql (Some false), [a1;a1], dest, succ) :: k
+  | Cne -> Iop (OEsnel (Some false), [a1;a1], dest, succ) :: k
+  | Clt -> Iop (OEsltul (Some false), [a1;a1], dest, succ) :: k
+  | Cle -> Iop (OEsltul (Some true), [a1;a1], dest, n2pi()) :: Iop (OExoriw Int.one, [dest], dest, succ) :: k
+  | Cgt -> Iop (OEsltul (Some true), [a1;a1], dest, succ) :: k
+  | Cge -> Iop (OEsltul (Some false), [a1;a1], dest, n2pi()) :: Iop (OExoriw Int.one, [dest], dest, succ) :: k
+
+let cond_int64u_reg cmp a1 a2 dest succ k =
+  match cmp with
+  | Ceq -> Iop (OEseql None, [a1;a2], dest, succ) :: k
+  | Cne -> Iop (OEsnel None, [a1;a2], dest, succ) :: k
+  | Clt -> Iop (OEsltul None, [a1;a2], dest, succ) :: k
+  | Cle -> Iop (OEsltul None, [a2;a1], dest, n2pi()) :: Iop (OExoriw Int.one, [dest], dest, succ) :: k
+  | Cgt -> Iop (OEsltul None, [a2;a1], dest, succ) :: k
+  | Cge -> Iop (OEsltul None, [a1;a2], dest, n2pi()) :: Iop (OExoriw Int.one, [dest], dest, succ) :: k
+
 let expanse_condimm_int32s cmp a1 n dest succ k =
   if Int.eq n Int.zero then cond_int32s_x0 cmp a1 dest succ k else
   match cmp with
@@ -87,22 +173,40 @@ 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 =
+let expanse_condimm_int32u cmp a1 n dest succ k =
+  if Int.eq n Int.zero then cond_int32u_x0 cmp a1 dest succ k else
   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
+  | Clt -> sltuimm32 a1 dest n succ k
+  | _   -> reg := !reg + 1;
+           loadimm32 (r2p()) n (n2pi()) (cond_int32u_reg cmp a1 (r2p()) dest succ k)
+
+let expanse_condimm_int64s cmp a1 n dest succ k =
+  if Int.eq n Int.zero then cond_int64s_x0 cmp a1 dest succ k else
+  match cmp with
+  | Ceq | Cne ->
+      reg := !reg + 1;
+      xorimm64 a1 (r2p()) n (n2pi()) (cond_int64s_x0 cmp (r2p()) dest succ k)
+  | Clt -> sltimm64 a1 dest n succ k
+  | Cle -> if Int64.eq n (Int64.repr Int64.max_signed)
+           then loadimm32 dest Int.one succ k
+            else sltimm64 a1 dest (Int64.add n Int64.one) succ k
+  | _   -> reg := !reg + 1;
+           loadimm64 (r2p()) n (n2pi()) (cond_int64s_reg cmp a1 (r2p()) dest succ k)
+ 
+let expanse_condimm_int64u cmp a1 n dest succ k =
+  if Int64.eq n Int64.zero then cond_int64u_x0 cmp a1 dest succ k else
+  match cmp with
+  | Clt -> sltuimm64 a1 dest n succ k
+  | _   -> reg := !reg + 1;
+           loadimm64 (r2p()) n (n2pi()) (cond_int64u_reg cmp a1 (r2p()) dest succ k)
 
 let rec write_tree exp n code' =
   match exp with
   | (Iop (_,_,_,succ)) as inst :: k ->
-      print_instruction stderr (0,inst);
-      Printf.eprintf "PLACING NODE %d\n" (Camlcoq.P.to_int n);
+      (*print_instruction stderr (0,inst);*)
+      (*Printf.eprintf "PLACING NODE %d\n" (Camlcoq.P.to_int n);*)
       code' := PTree.set n inst !code';
-      Printf.eprintf "WITH SUCC %d\n" (Camlcoq.P.to_int succ);
+      (*Printf.eprintf "WITH SUCC %d\n" (Camlcoq.P.to_int succ);*)
       write_tree k (Camlcoq.P.of_int ((Camlcoq.P.to_int n) + 1)) code'
   | _ -> !code'
 
@@ -135,34 +239,61 @@ let generate_head_order n start_node new_order =
 let expanse (sb: superblock) code =
   debug_flag := true;
   let new_order = ref [] in
+  let exp = ref [] in
+  let was_exp = ref false in
   let code' = ref code in
   Array.iter (fun n ->
+    was_exp := false;
     let inst = get_some @@ PTree.get n code in
+    let start_node = Camlcoq.P.of_int (!node + 1) in (
     match inst with
+    | Iop (Ocmp (Ccomp c), a1 :: a2 :: nil, dest, succ) -> (
+      Printf.eprintf "Ccomp\n";
+      exp := cond_int32s_reg c a1 a2 dest succ [];
+      was_exp := true)
     | 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);
-      Printf.eprintf "SUCC IS %d\n" (Camlcoq.P.to_int succ);
-      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)
+      Printf.eprintf "Ccompu\n";
+      exp := cond_int32u_reg c a1 a2 dest succ [];
+      was_exp := true)
     | 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';
+      Printf.eprintf "Ccompimm\n";
+      exp := expanse_condimm_int32s c a1 imm dest succ [];
+      was_exp := true)
+    | Iop (Ocmp (Ccompuimm (c, imm)), a1 :: nil, dest, succ) -> (
+      Printf.eprintf "Ccompuimm\n";
+      exp := expanse_condimm_int32u c a1 imm dest succ [];
+      was_exp := true)
+    | Iop (Ocmp (Ccompl c), a1 :: a2 :: nil, dest, succ) -> (
+      Printf.eprintf "Ccompl\n";
+      exp := cond_int64s_reg c a1 a2 dest succ [];
+      was_exp := true)
+    | Iop (Ocmp (Ccomplu c), a1 :: a2 :: nil, dest, succ) -> (
+      Printf.eprintf "Ccomplu\n";
+      exp := cond_int64u_reg c a1 a2 dest succ [];
+      was_exp := true)
+    | Iop (Ocmp (Ccomplimm (c, imm)), a1 :: nil, dest, succ) -> (
+      (*Printf.eprintf "Ccomplimm\n";*)
+      (*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);*)
+      (*Printf.eprintf "SUCC IS %d\n" (Camlcoq.P.to_int succ);*)
+      (*debug "[EXPANSION] Replace this:\n";*)
+      (*print_instruction stderr (0,inst);*)
+      (*debug "[EXPANSION] With:\n";*)
+      (*Printf.eprintf "entry is %d\n" (Camlcoq.P.to_int !entry);*)
+      (*entry := n2p()*)
+      exp := expanse_condimm_int64s c a1 imm dest succ [];
+      was_exp := true)
+    | Iop (Ocmp (Ccompluimm (c, imm)), a1 :: nil, dest, succ) -> (
+      Printf.eprintf "Ccompluimm\n";
+      exp := expanse_condimm_int64u c a1 imm dest succ [];
+      was_exp := true)
+    | _ -> new_order := !new_order @ [n]);
+    if !was_exp then (
+      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)
-      (*Printf.eprintf "entry is %d\n" (Camlcoq.P.to_int !entry);*)
-      (*entry := n2p()*)
-    | _ -> new_order := !new_order @ [n]
   ) sb.instructions;
   sb.instructions <- Array.of_list !new_order;
   (*print_arrayp sb.instructions;*)