cond and branches expanded

1 files changed, 251 insertions, 181 deletions

diff --git a/riscV/ExpansionOracle.ml b/riscV/ExpansionOracle.ml
index 9e494d0a..af14811d 100644
--- a/riscV/ExpansionOracle.ml
+++ b/riscV/ExpansionOracle.ml
@@ -18,8 +18,6 @@ open RTL
 open Op
 open Asmgen
 open DebugPrint
-
-(*open PrintRTL*)
 open! Integers
 
 let reg = ref 1
@@ -102,150 +100,169 @@ 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
+let is_inv_cmp = function Cle | Cgt -> true | _ -> false
 
-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
+let make_optR0 is_x0 is_inv = if is_x0 then Some is_inv else None
 
-let cond_int32u_x0 cmp a1 dest succ k =
+let cbranch_int32s is_x0 cmp a1 a2 info succ1 succ2 k =
+  let optR0 = make_optR0 is_x0 (is_inv_cmp cmp) in
   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 =
+  | Ceq -> Icond (CEbeqw optR0, [ a1; a2 ], succ1, succ2, info) :: k
+  | Cne -> Icond (CEbnew optR0, [ a1; a2 ], succ1, succ2, info) :: k
+  | Clt -> Icond (CEbltw optR0, [ a1; a2 ], succ1, succ2, info) :: k
+  | Cle -> Icond (CEbgew optR0, [ a2; a1 ], succ1, succ2, info) :: k
+  | Cgt -> Icond (CEbltw optR0, [ a2; a1 ], succ1, succ2, info) :: k
+  | Cge -> Icond (CEbgew optR0, [ a1; a2 ], succ1, succ2, info) :: k
+
+let cbranch_int32u is_x0 cmp a1 a2 info succ1 succ2 k =
+  let optR0 = make_optR0 is_x0 (is_inv_cmp cmp) in
   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 =
+  | Ceq -> Icond (CEbeqw optR0, [ a1; a2 ], succ1, succ2, info) :: k
+  | Cne -> Icond (CEbnew optR0, [ a1; a2 ], succ1, succ2, info) :: k
+  | Clt -> Icond (CEbltuw optR0, [ a1; a2 ], succ1, succ2, info) :: k
+  | Cle -> Icond (CEbgeuw optR0, [ a2; a1 ], succ1, succ2, info) :: k
+  | Cgt -> Icond (CEbltuw optR0, [ a2; a1 ], succ1, succ2, info) :: k
+  | Cge -> Icond (CEbgeuw optR0, [ a1; a2 ], succ1, succ2, info) :: k
+
+let cbranch_int64s is_x0 cmp a1 a2 info succ1 succ2 k =
+  let optR0 = make_optR0 is_x0 (is_inv_cmp cmp) in
+  match cmp with
+  | Ceq -> Icond (CEbeql optR0, [ a1; a2 ], succ1, succ2, info) :: k
+  | Cne -> Icond (CEbnel optR0, [ a1; a2 ], succ1, succ2, info) :: k
+  | Clt -> Icond (CEbltl optR0, [ a1; a2 ], succ1, succ2, info) :: k
+  | Cle -> Icond (CEbgel optR0, [ a2; a1 ], succ1, succ2, info) :: k
+  | Cgt -> Icond (CEbltl optR0, [ a2; a1 ], succ1, succ2, info) :: k
+  | Cge -> Icond (CEbgel optR0, [ a1; a2 ], succ1, succ2, info) :: k
+
+let cbranch_int64u is_x0 cmp a1 a2 info succ1 succ2 k =
+  let optR0 = make_optR0 is_x0 (is_inv_cmp cmp) in
+  match cmp with
+  | Ceq -> Icond (CEbeql optR0, [ a1; a2 ], succ1, succ2, info) :: k
+  | Cne -> Icond (CEbnel optR0, [ a1; a2 ], succ1, succ2, info) :: k
+  | Clt -> Icond (CEbltul optR0, [ a1; a2 ], succ1, succ2, info) :: k
+  | Cle -> Icond (CEbgeul optR0, [ a2; a1 ], succ1, succ2, info) :: k
+  | Cgt -> Icond (CEbltul optR0, [ a2; a1 ], succ1, succ2, info) :: k
+  | Cge -> Icond (CEbgeul optR0, [ a1; a2 ], succ1, succ2, info) :: k
+
+let cond_int32s is_x0 cmp a1 a2 dest succ k =
+  let optR0 = make_optR0 is_x0 (is_inv_cmp cmp) in
   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
+  | Ceq -> Iop (OEseqw optR0, [ 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 (OEsltl (Some true), [ a1; a1 ], dest, n2pi ())
+      Iop (OEsltw optR0, [ a2; a1 ], dest, n2pi ())
       :: Iop (OExoriw Int.one, [ dest ], dest, succ)
       :: k
-  | Cgt -> Iop (OEsltl (Some true), [ a1; a1 ], dest, succ) :: k
+  | Cgt -> Iop (OEsltw optR0, [ a2; a1 ], dest, succ) :: k
   | Cge ->
-      Iop (OEsltl (Some false), [ a1; a1 ], dest, n2pi ())
+      Iop (OEsltw optR0, [ a1; a2 ], dest, n2pi ())
       :: Iop (OExoriw Int.one, [ dest ], dest, succ)
       :: k
 
-let cond_int64s_reg cmp a1 a2 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
   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
+  | Ceq -> Iop (OEseqw optR0, [ a1; a2 ], dest, succ) :: k
+  | Cne -> Iop (OEsnew optR0, [ a1; a2 ], dest, succ) :: k
+  | Clt -> Iop (OEsltuw optR0, [ a1; a2 ], dest, succ) :: k
   | Cle ->
-      Iop (OEsltl None, [ a2; a1 ], dest, n2pi ())
+      Iop (OEsltuw optR0, [ a2; a1 ], dest, n2pi ())
       :: Iop (OExoriw Int.one, [ dest ], dest, succ)
       :: k
-  | Cgt -> Iop (OEsltl None, [ a2; a1 ], dest, succ) :: k
+  | Cgt -> Iop (OEsltuw optR0, [ a2; a1 ], dest, succ) :: k
   | Cge ->
-      Iop (OEsltl None, [ a1; a2 ], dest, n2pi ())
+      Iop (OEsltuw optR0, [ a1; a2 ], dest, n2pi ())
       :: Iop (OExoriw Int.one, [ dest ], dest, succ)
       :: k
 
-let cond_int64u_x0 cmp a1 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
   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
+  | Ceq -> Iop (OEseql optR0, [ 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 (OEsltul (Some true), [ a1; a1 ], dest, n2pi ())
+      Iop (OEsltl optR0, [ a2; a1 ], dest, n2pi ())
       :: Iop (OExoriw Int.one, [ dest ], dest, succ)
       :: k
-  | Cgt -> Iop (OEsltul (Some true), [ a1; a1 ], dest, succ) :: k
+  | Cgt -> Iop (OEsltl optR0, [ a2; a1 ], dest, succ) :: k
   | Cge ->
-      Iop (OEsltul (Some false), [ a1; a1 ], dest, n2pi ())
+      Iop (OEsltl optR0, [ a1; a2 ], dest, n2pi ())
       :: Iop (OExoriw Int.one, [ dest ], dest, succ)
       :: k
 
-let cond_int64u_reg cmp a1 a2 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
   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
+  | Ceq -> Iop (OEseql optR0, [ a1; a2 ], dest, succ) :: k
+  | Cne -> Iop (OEsnel optR0, [ a1; a2 ], dest, succ) :: k
+  | Clt -> Iop (OEsltul optR0, [ a1; a2 ], dest, succ) :: k
   | Cle ->
-      Iop (OEsltul None, [ a2; a1 ], dest, n2pi ())
+      Iop (OEsltul optR0, [ a2; a1 ], dest, n2pi ())
       :: Iop (OExoriw Int.one, [ dest ], dest, succ)
       :: k
-  | Cgt -> Iop (OEsltul None, [ a2; a1 ], dest, succ) :: k
+  | Cgt -> Iop (OEsltul optR0, [ a2; a1 ], dest, succ) :: k
   | Cge ->
-      Iop (OEsltul None, [ a1; a2 ], dest, n2pi ())
+      Iop (OEsltul optR0, [ a1; a2 ], dest, n2pi ())
       :: Iop (OExoriw Int.one, [ dest ], dest, succ)
       :: k
 
+let is_normal_cmp = function Cne -> false | _ -> true
+
 let cond_float cmp f1 f2 dest succ =
   match cmp with
-  | 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)
+  | Ceq -> Iop (OEfeqd, [ f1; f2 ], dest, succ)
+  | Cne -> Iop (OEfeqd, [ f1; f2 ], dest, succ)
+  | Clt -> Iop (OEfltd, [ f1; f2 ], dest, succ)
+  | Cle -> Iop (OEfled, [ f1; f2 ], dest, succ)
+  | Cgt -> Iop (OEfltd, [ f2; f1 ], dest, succ)
+  | Cge -> Iop (OEfled, [ f2; f1 ], dest, succ)
 
 let cond_single cmp f1 f2 dest succ =
   match cmp with
-  | 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)
+  | Ceq -> Iop (OEfeqs, [ f1; f2 ], dest, succ)
+  | Cne -> Iop (OEfeqs, [ f1; f2 ], dest, succ)
+  | Clt -> Iop (OEflts, [ f1; f2 ], dest, succ)
+  | Cle -> Iop (OEfles, [ 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 =
+  if Int.eq n Int.zero then cbranch_int32s true cmp a1 a1 info succ1 succ2 k
+  else (
+    reg := !reg + 1;
+    loadimm32 (r2p ()) n (n2pi ())
+      (cbranch_int32s false cmp a1 (r2p ()) 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 (r2p ()) n (n2pi ())
+      (cbranch_int32u false cmp a1 (r2p ()) 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 (r2p ()) n (n2pi ())
+      (cbranch_int64s false cmp a1 (r2p ()) 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 (r2p ()) n (n2pi ())
+      (cbranch_int64u false cmp a1 (r2p ()) info succ1 succ2 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
+  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 ()) (cond_int32s_x0 cmp dest dest succ k)
+        xorimm32 a1 dest n (n2pi ())
+          (cond_int32s true cmp dest 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
@@ -253,26 +270,26 @@ 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)
+          (cond_int32s false 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
+  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 k
     | _ ->
         reg := !reg + 1;
         loadimm32 (r2p ()) n (n2pi ())
-          (cond_int32u_reg cmp a1 (r2p ()) dest succ k)
+          (cond_int32u false 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
+  if Int.eq n Int.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_x0 cmp (r2p ()) dest succ k)
+          (cond_int64s true cmp (r2p ()) (r2p ()) dest succ k)
     | Clt -> sltimm64 a1 dest n succ k
     | Cle ->
         if Int64.eq n (Int64.repr Int64.max_signed) then
@@ -281,47 +298,36 @@ let expanse_condimm_int64s cmp a1 n dest succ k =
     | _ ->
         reg := !reg + 1;
         loadimm64 (r2p ()) n (n2pi ())
-          (cond_int64s_reg cmp a1 (r2p ()) dest succ k)
+          (cond_int64s false 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
+  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
     | _ ->
         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)
+          (cond_int64u false cmp a1 (r2p ()) 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
+let expanse_cond_fp cnot fn_cond cmp f1 f2 dest succ k =
+  let normal = is_normal_cmp cmp in
+  let normal' = if cnot then not normal else normal in
+  let succ' = if normal' then succ else n2pi () in
+  let insn = fn_cond cmp f1 f2 dest succ' in
   insn
-  :: (if normal then Iop (OExoriw Int.one, [ dest ], dest, succ) :: k else k)
+  :: (if normal' then k else Iop (OExoriw Int.one, [ dest ], dest, succ) :: k)
 
-let expanse_cond_single cmp f1 f2 dest succ k =
-  let insn, normal = cond_single cmp f1 f2 dest succ in
+let expanse_cbranch_fp cnot fn_cond cmp f1 f2 info succ1 succ2 k =
+  reg := !reg + 1;
+  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
   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 ->
-      (*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'
-  | _ -> !code'
+  :: (if normal' then
+      Icond (CEbnew (Some false), [ r2p (); r2p () ], succ1, succ2, info)
+     else Icond (CEbeqw (Some false), [ r2p (); r2p () ], succ1, succ2, info))
+  :: k
 
 let get_regindent = function Coq_inr _ -> [] | Coq_inl r -> [ r ]
 
@@ -339,94 +345,158 @@ let get_regs_inst = function
   | 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 ]
-  done;
-  new_order := n :: !new_order
+let rec write_tree' exp current initial code' new_order =
+  if current = !node then (
+    code' := PTree.set initial (Inop (n2p ())) !code';
+    new_order := initial :: !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;
+      write_tree' k (current - 1) initial 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;
+      write_tree' k (current - 1) initial code' new_order
+  | [] -> ()
+  | _ -> failwith "ExpansionOracle.write_tree: inconsistent instruction."
 
 let expanse (sb : superblock) code =
-  debug_flag := true;
   let new_order = ref [] in
+  let liveins = ref sb.liveins in
   let exp = ref [] in
+  let was_branch = ref false in
   let was_exp = ref false in
   let code' = ref code in
   Array.iter
     (fun n ->
+      was_branch := false;
       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 [];
+          debug "Iop/Ccomp\n";
+          exp := cond_int32s false 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 [];
+          debug "Iop/Ccompu\n";
+          exp := cond_int32u false c a1 a2 dest succ [];
           was_exp := true
       | Iop (Ocmp (Ccompimm (c, imm)), a1 :: nil, dest, succ) ->
-          Printf.eprintf "Ccompimm\n";
+          debug "Iop/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";
+          debug "Iop/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 [];
+          debug "Iop/Ccompl\n";
+          exp := cond_int64s false 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 [];
+          debug "Iop/Ccomplu\n";
+          exp := cond_int64u false 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()*)
+          debug "Iop/Ccomplimm\n";
           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";
+          debug "Iop/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 [];
+          debug "Iop/Ccompf\n";
+          exp := expanse_cond_fp false 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 [];
+          debug "Iop/Cnotcompf\n";
+          exp := expanse_cond_fp true cond_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 [];
+          debug "Iop/Ccompfs\n";
+          exp := expanse_cond_fp false 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 [];
+          debug "Iop/Cnotcompfs\n";
+          exp := expanse_cond_fp true cond_single c f1 f2 dest succ [];
+          was_exp := true
+      | Icond (Ccomp c, a1 :: a2 :: nil, succ1, succ2, info) ->
+          debug "Icond/Ccomp\n";
+          exp := cbranch_int32s false c a1 a2 info succ1 succ2 [];
+          was_branch := true;
+          was_exp := true
+      | Icond (Ccompu c, a1 :: a2 :: nil, succ1, succ2, info) ->
+          debug "Icond/Ccompu\n";
+          exp := cbranch_int32u false c a1 a2 info succ1 succ2 [];
+          was_branch := true;
+          was_exp := true
+      | Icond (Ccompimm (c, imm), a1 :: nil, succ1, succ2, info) ->
+          debug "Icond/Ccompimm\n";
+          exp := expanse_cbranchimm_int32s c a1 imm info succ1 succ2 [];
+          was_branch := true;
+          was_exp := true
+      | Icond (Ccompuimm (c, imm), a1 :: nil, succ1, succ2, info) ->
+          debug "Icond/Ccompuimm\n";
+          exp := expanse_cbranchimm_int32u c a1 imm info succ1 succ2 [];
+          was_branch := true;
+          was_exp := true
+      | Icond (Ccompl c, a1 :: a2 :: nil, succ1, succ2, info) ->
+          debug "Icond/Ccompl\n";
+          exp := cbranch_int64s false c a1 a2 info succ1 succ2 [];
+          was_branch := true;
+          was_exp := true
+      | Icond (Ccomplu c, a1 :: a2 :: nil, succ1, succ2, info) ->
+          debug "Icond/Ccomplu\n";
+          exp := cbranch_int64u false c a1 a2 info succ1 succ2 [];
+          was_branch := true;
+          was_exp := true
+      | Icond (Ccomplimm (c, imm), a1 :: nil, succ1, succ2, info) ->
+          debug "Icond/Ccomplimm\n";
+          exp := expanse_cbranchimm_int64s c a1 imm info succ1 succ2 [];
+          was_branch := true;
+          was_exp := true
+      | Icond (Ccompluimm (c, imm), a1 :: nil, succ1, succ2, info) ->
+          debug "Icond/Ccompluimm\n";
+          exp := expanse_cbranchimm_int64u c a1 imm info succ1 succ2 [];
+          was_branch := true;
+          was_exp := true
+      | Icond (Ccompf c, f1 :: f2 :: nil, succ1, succ2, info) ->
+          debug "Icond/Ccompf\n";
+          exp := expanse_cbranch_fp false cond_float c f1 f2 info succ1 succ2 [];
+          was_branch := true;
+          was_exp := true
+      | Icond (Cnotcompf c, f1 :: f2 :: nil, succ1, succ2, info) ->
+          debug "Icond/Cnotcompf\n";
+          exp := expanse_cbranch_fp true cond_float c f1 f2 info succ1 succ2 [];
+          was_branch := true;
+          was_exp := true
+      | Icond (Ccompfs c, f1 :: f2 :: nil, succ1, succ2, info) ->
+          debug "Icond/Ccompfs\n";
+          exp :=
+            expanse_cbranch_fp false cond_single c f1 f2 info succ1 succ2 [];
+          was_branch := true;
+          was_exp := true
+      | Icond (Cnotcompfs c, f1 :: f2 :: nil, succ1, succ2, info) ->
+          debug "Icond/Cnotcompfs\n";
+          exp := expanse_cbranch_fp true cond_single c f1 f2 info succ1 succ2 [];
+          was_branch := true;
           was_exp := true
-      | _ -> new_order := !new_order @ [ n ]);
+      | _ -> new_order := n :: !new_order);
       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))
+        node := !node + 1;
+        (if !was_branch then
+         let lives = PTree.get n !liveins in
+         match lives with
+         | Some lives ->
+             liveins := PTree.set (n2p ()) lives !liveins;
+             liveins := PTree.remove n !liveins
+         | _ -> ());
+        write_tree' !exp !node n code' new_order))
     sb.instructions;
-  sb.instructions <- Array.of_list !new_order;
-  (*print_arrayp sb.instructions;*)
-  debug_flag := false;
+  sb.instructions <- Array.of_list (List.rev !new_order);
+  sb.liveins <- !liveins;
   !code'
 
 let rec find_last_node_reg = function