All Ocmp expanded in RTL

1 files changed, 315 insertions, 185 deletions

diff --git a/riscV/ExpansionOracle.ml b/riscV/ExpansionOracle.ml
index c3f2cb3f..9e494d0a 100644
--- a/riscV/ExpansionOracle.ml
+++ b/riscV/ExpansionOracle.ml
@@ -18,40 +18,46 @@ open RTL
 open Op
 open Asmgen
 open DebugPrint
+
 (*open PrintRTL*)
 open! Integers
 
 let reg = ref 1
+
 let node = ref 1
 
 let r2p () = Camlcoq.P.of_int !reg
+
 let n2p () = Camlcoq.P.of_int !node
-let n2pi () = node := !node + 1; n2p()
+
+let n2pi () =
+  node := !node + 1;
+  n2p ()
 
 type immt = Xoriw | Xoril | Sltiw | Sltiuw | Sltil | Sltiul
 
 let load_hilo32 dest hi lo succ k =
-  if Int.eq lo Int.zero then
-    Iop (OEluiw hi, [], dest, succ) :: k
-  else (
-      Iop (OEluiw hi, [], dest, n2pi()) :: (Iop (Oaddimm lo, [dest], dest, succ)) :: k)
+  if Int.eq lo Int.zero then Iop (OEluiw hi, [], dest, 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)
+  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_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_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
 
@@ -65,236 +71,359 @@ let get_opimm imm = function
 
 let opimm32 a1 dest n succ k op opimm =
   match make_immed32 n with
-  | Imm32_single imm ->
-      Iop (get_opimm imm opimm, [a1], dest, succ) :: k
+  | Imm32_single imm -> Iop (get_opimm imm opimm, [ a1 ], dest, succ) :: k
   | Imm32_pair (hi, lo) ->
       reg := !reg + 1;
-      load_hilo32 (r2p()) hi lo (n2pi()) (Iop (op, [a1;r2p()], dest, succ) :: k)
+      load_hilo32 (r2p ()) hi lo (n2pi ())
+        (Iop (op, [ a1; r2p () ], 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_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  ->
+      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
+      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
-  | Ceq -> Iop (OEseqw (Some false), [a1;a1], dest, succ) :: k
-  | Cne -> Iop (OEsnew (Some false), [a1;a1], dest, succ) :: k
-  | Clt -> Iop (OEsltw (Some false), [a1;a1], dest, succ) :: k
-  | Cle -> Iop (OEsltw (Some true), [a1;a1], dest, n2pi()) :: Iop (OExoriw Int.one, [dest], dest, succ) :: k
-  | Cgt -> Iop (OEsltw (Some true), [a1;a1], dest, succ) :: k
-  | Cge -> Iop (OEsltw (Some false), [a1;a1], dest, n2pi()) :: Iop (OExoriw Int.one, [dest], dest, succ) :: k
+  | Ceq -> Iop (OEseqw (Some false), [ a1; a1 ], dest, succ) :: k
+  | Cne -> Iop (OEsnew (Some false), [ a1; a1 ], dest, succ) :: k
+  | Clt -> Iop (OEsltw (Some false), [ a1; a1 ], dest, succ) :: k
+  | Cle ->
+      Iop (OEsltw (Some true), [ a1; a1 ], dest, n2pi ())
+      :: Iop (OExoriw Int.one, [ dest ], dest, succ)
+      :: k
+  | Cgt -> Iop (OEsltw (Some true), [ a1; a1 ], dest, succ) :: k
+  | Cge ->
+      Iop (OEsltw (Some false), [ a1; a1 ], dest, n2pi ())
+      :: Iop (OExoriw Int.one, [ dest ], dest, succ)
+      :: k
 
 let cond_int32s_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 (OEsltw None, [a1;a2], dest, succ) :: k
-  | Cle -> Iop (OEsltw None, [a2;a1], dest, n2pi()) :: Iop (OExoriw Int.one, [dest], 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
+  | Ceq -> Iop (OEseqw None, [ a1; a2 ], dest, succ) :: k
+  | Cne -> Iop (OEsnew None, [ a1; a2 ], dest, succ) :: k
+  | Clt -> Iop (OEsltw None, [ a1; a2 ], dest, succ) :: k
+  | Cle ->
+      Iop (OEsltw None, [ a2; a1 ], dest, n2pi ())
+      :: Iop (OExoriw Int.one, [ dest ], 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
+  | 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
+  | 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
+  | 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
+  | 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
+  | 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
+  | 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
+let cond_float cmp f1 f2 dest succ =
   match cmp with
-  | Ceq | Cne ->
-      xorimm32 a1 dest n (n2pi()) (cond_int32s_x0 cmp dest dest succ k)
-  | Clt -> sltimm32 a1 dest n succ k
-  | Cle -> if Int.eq n (Int.repr Int.max_signed)
-           then loadimm32 dest Int.one succ k
-            else sltimm32 a1 dest (Int.add n Int.one) succ k
-  | _   -> reg := !reg + 1;
-           loadimm32 (r2p()) n (n2pi()) (cond_int32s_reg cmp a1 (r2p()) dest succ k)
+  | Ceq -> (Iop (OEfeqd, [ f1; f2 ], dest, succ), true)
+  | Cne -> (Iop (OEfeqd, [ f1; f2 ], dest, succ), false)
+  | Clt -> (Iop (OEfltd, [ f1; f2 ], dest, succ), true)
+  | Cle -> (Iop (OEfled, [ f1; f2 ], dest, succ), true)
+  | Cgt -> (Iop (OEfltd, [ f2; f1 ], dest, succ), true)
+  | Cge -> (Iop (OEfled, [ f2; f1 ], dest, succ), true)
 
-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
+let cond_single cmp f1 f2 dest succ =
   match cmp with
-  | Clt -> sltuimm32 a1 dest n succ k
-  | _   -> reg := !reg + 1;
-           loadimm32 (r2p()) n (n2pi()) (cond_int32u_reg cmp a1 (r2p()) dest succ k)
+  | Ceq -> (Iop (OEfeqs, [ f1; f2 ], dest, succ), true)
+  | Cne -> (Iop (OEfeqs, [ f1; f2 ], dest, succ), false)
+  | Clt -> (Iop (OEflts, [ f1; f2 ], dest, succ), true)
+  | Cle -> (Iop (OEfles, [ f1; f2 ], dest, succ), true)
+  | Cgt -> (Iop (OEflts, [ f2; f1 ], dest, succ), true)
+  | Cge -> (Iop (OEfles, [ f2; f1 ], dest, succ), true)
+
+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
+    | Ceq | Cne ->
+        xorimm32 a1 dest n (n2pi ()) (cond_int32s_x0 cmp dest dest succ k)
+    | Clt -> sltimm32 a1 dest n succ k
+    | Cle ->
+        if Int.eq n (Int.repr Int.max_signed) then loadimm32 dest Int.one succ k
+        else sltimm32 a1 dest (Int.add n Int.one) succ k
+    | _ ->
+        reg := !reg + 1;
+        loadimm32 (r2p ()) n (n2pi ())
+          (cond_int32s_reg cmp a1 (r2p ()) 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
+    | 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)
- 
+  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)
+  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 expanse_cond_float cmp f1 f2 dest succ k =
+  let insn, normal = cond_float cmp f1 f2 dest succ in
+  insn
+  :: (if normal then k else Iop (OExoriw Int.one, [ dest ], dest, succ) :: k)
+
+let expanse_cond_not_float cmp f1 f2 dest succ k =
+  let insn, normal = cond_float cmp f1 f2 dest succ in
+  insn
+  :: (if normal then Iop (OExoriw Int.one, [ dest ], dest, succ) :: k else k)
+
+let expanse_cond_single cmp f1 f2 dest succ k =
+  let insn, normal = cond_single cmp f1 f2 dest succ in
+  insn
+  :: (if normal then k else Iop (OExoriw Int.one, [ dest ], dest, succ) :: k)
+
+let expanse_cond_not_single cmp f1 f2 dest succ k =
+  let insn, normal = cond_single cmp f1 f2 dest succ in
+  insn
+  :: (if normal then Iop (OExoriw Int.one, [ dest ], dest, succ) :: k else k)
 
 let rec write_tree exp n code' =
   match exp with
-  | (Iop (_,_,_,succ)) as inst :: k ->
+  | (Iop (_, _, _, succ) as inst) :: k ->
       (*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);*)
-      write_tree k (Camlcoq.P.of_int ((Camlcoq.P.to_int n) + 1)) code'
+      write_tree k (Camlcoq.P.of_int (Camlcoq.P.to_int n + 1)) code'
   | _ -> !code'
 
-let get_regindent = function
-  | Coq_inr _ -> []
-  | Coq_inl r -> [r]
-  
+let get_regindent = function Coq_inr _ -> [] | Coq_inl r -> [ r ]
+
 let get_regs_inst = function
-  | Inop (_) -> []
-  | Iop (_,args,dest,_) -> dest :: args
-  | Iload (_,_,_,args,dest,_) -> dest :: args
-  | Istore (_,_,args,src,_) -> src :: args
-  | Icall (_,t,args,dest,_) -> dest :: ((get_regindent t) @ args)
-  | Itailcall (_,t,args) -> (get_regindent t) @ args
-  | Ibuiltin (_,args,dest,_) ->
-      (AST.params_of_builtin_res dest) @
-      AST.params_of_builtin_args args
-  | Icond (_,args,_,_,_) -> args
-  | Ijumptable (arg,_) -> [arg]
-  | Ireturn (Some r) -> [r]
+  | Inop _ -> []
+  | Iop (_, args, dest, _) -> dest :: args
+  | Iload (_, _, _, args, dest, _) -> dest :: args
+  | Istore (_, _, args, src, _) -> src :: args
+  | Icall (_, t, args, dest, _) -> dest :: (get_regindent t @ args)
+  | Itailcall (_, t, args) -> get_regindent t @ args
+  | Ibuiltin (_, args, dest, _) ->
+      AST.params_of_builtin_res dest @ AST.params_of_builtin_args args
+  | Icond (_, args, _, _, _) -> args
+  | Ijumptable (arg, _) -> [ arg ]
+  | Ireturn (Some r) -> [ r ]
   | _ -> []
 
 let generate_head_order n start_node new_order =
-  Printf.eprintf "GEN n %d start %d node %d\n" (Camlcoq.P.to_int n) (Camlcoq.P.to_int start_node) !node;
-  for i = !node downto (Camlcoq.P.to_int start_node) do
-    new_order := !new_order @ [Camlcoq.P.of_int i];
+  Printf.eprintf "GEN n %d start %d node %d\n" (Camlcoq.P.to_int n)
+    (Camlcoq.P.to_int start_node)
+    !node;
+  for i = !node downto Camlcoq.P.to_int start_node do
+    new_order := !new_order @ [ Camlcoq.P.of_int i ]
   done;
   new_order := n :: !new_order
 
-let expanse (sb: superblock) code =
+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 "Ccompu\n";
-      exp := cond_int32u_reg c a1 a2 dest succ [];
-      was_exp := true)
-    | Iop (Ocmp (Ccompimm (c, imm)), a1 :: nil, dest, succ) -> (
-      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)
-  ) sb.instructions;
+  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 "Ccompu\n";
+          exp := cond_int32u_reg c a1 a2 dest succ [];
+          was_exp := true
+      | Iop (Ocmp (Ccompimm (c, imm)), a1 :: nil, dest, succ) ->
+          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
+      | Iop (Ocmp (Ccompf c), f1 :: f2 :: nil, dest, succ) ->
+          Printf.eprintf "Ccompf\n";
+          exp := expanse_cond_float c f1 f2 dest succ [];
+          was_exp := true
+      | Iop (Ocmp (Cnotcompf c), f1 :: f2 :: nil, dest, succ) ->
+          Printf.eprintf "Cnotcompf\n";
+          exp := expanse_cond_not_float c f1 f2 dest succ [];
+          was_exp := true
+      | Iop (Ocmp (Ccompfs c), f1 :: f2 :: nil, dest, succ) ->
+          Printf.eprintf "Ccompfs\n";
+          exp := expanse_cond_single c f1 f2 dest succ [];
+          was_exp := true
+      | Iop (Ocmp (Cnotcompfs c), f1 :: f2 :: nil, dest, succ) ->
+          Printf.eprintf "Cnotcompfs\n";
+          exp := expanse_cond_not_single c f1 f2 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))
+    sb.instructions;
   sb.instructions <- Array.of_list !new_order;
   (*print_arrayp sb.instructions;*)
   debug_flag := false;
@@ -303,12 +432,13 @@ let expanse (sb: superblock) code =
 let rec find_last_node_reg = function
   | [] -> ()
   | (pc, i) :: k ->
-    let rec traverse_list var = function
-    | [] -> ()
-    | e :: t ->
-        (let e' = Camlcoq.P.to_int e in
-        if e' > !var then var := e';
-        traverse_list var t) in
-    traverse_list node [pc];
-    traverse_list reg (get_regs_inst i);
-    find_last_node_reg k
+      let rec traverse_list var = function
+        | [] -> ()
+        | e :: t ->
+            let e' = Camlcoq.P.to_int e in
+            if e' > !var then var := e';
+            traverse_list var t
+      in
+      traverse_list node [ pc ];
+      traverse_list reg (get_regs_inst i);
+      find_last_node_reg k