Remove first nop when doing expansion

1 files changed, 212 insertions, 188 deletions

diff --git a/riscV/ExpansionOracle.ml b/riscV/ExpansionOracle.ml
index b3c19802..81c369f7 100644
--- a/riscV/ExpansionOracle.ml
+++ b/riscV/ExpansionOracle.ml
@@ -21,6 +21,7 @@ open DebugPrint
 open RTLpath
 open! Integers
 open Camlcoq
+open Option
 
 type sop = Sop of operation * P.t list
 
@@ -49,8 +50,7 @@ type immt = Xoriw | Xoril | Sltiw | Sltiuw | Sltil | Sltiul
 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)
+  | Some r -> Sr (P.of_int r)
   | None ->
       Hashtbl.add map_consts sop (p2i rd);
       Si (Iop (op, args, rd, succ))
@@ -205,7 +205,7 @@ let cbranch_int64u is_x0 cmp a1 a2 info succ1 succ2 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 cond_int32s is_x0 cmp a1 a2 dest tmp_reg succ k =
   let optR0 = make_optR0 is_x0 (is_inv_cmp cmp) in
   match cmp with
   | Ceq -> Iop (OEseqw optR0, [ a1; a2 ], dest, succ) :: k
@@ -213,15 +213,15 @@ let cond_int32s is_x0 cmp a1 a2 dest succ k =
   | Clt -> Iop (OEsltw optR0, [ a1; a2 ], dest, succ) :: k
   | Cle ->
       let r = r2pi () in
-      Iop (OEsltw optR0, [ a2; a1 ], r, n2pi ())
+      Iop (OEsltw optR0, [ a2; a1 ], r, get tmp_reg)
       :: Iop (OExoriw Int.one, [ r ], dest, succ) :: k
   | Cgt -> Iop (OEsltw optR0, [ a2; a1 ], dest, succ) :: k
   | Cge ->
       let r = r2pi () in
-      Iop (OEsltw optR0, [ a1; a2 ], r, n2pi ())
+      Iop (OEsltw optR0, [ a1; a2 ], r, get tmp_reg)
       :: Iop (OExoriw Int.one, [ r ], dest, succ) :: k
 
-let cond_int32u is_x0 cmp a1 a2 dest succ k =
+let cond_int32u is_x0 cmp a1 a2 dest tmp_reg succ k =
   let optR0 = make_optR0 is_x0 (is_inv_cmp cmp) in
   match cmp with
   | Ceq -> Iop (OEsequw optR0, [ a1; a2 ], dest, succ) :: k
@@ -229,15 +229,15 @@ let cond_int32u is_x0 cmp a1 a2 dest succ k =
   | Clt -> Iop (OEsltuw optR0, [ a1; a2 ], dest, succ) :: k
   | Cle ->
       let r = r2pi () in
-      Iop (OEsltuw optR0, [ a2; a1 ], r, n2pi ())
+      Iop (OEsltuw optR0, [ a2; a1 ], r, get tmp_reg)
       :: Iop (OExoriw Int.one, [ r ], dest, succ) :: k
   | Cgt -> Iop (OEsltuw optR0, [ a2; a1 ], dest, succ) :: k
   | Cge ->
       let r = r2pi () in
-      Iop (OEsltuw optR0, [ a1; a2 ], r, n2pi ())
+      Iop (OEsltuw optR0, [ a1; a2 ], r, get tmp_reg)
       :: Iop (OExoriw Int.one, [ r ], dest, succ) :: k
 
-let cond_int64s is_x0 cmp a1 a2 dest succ k =
+let cond_int64s is_x0 cmp a1 a2 dest tmp_reg succ k =
   let optR0 = make_optR0 is_x0 (is_inv_cmp cmp) in
   match cmp with
   | Ceq -> Iop (OEseql optR0, [ a1; a2 ], dest, succ) :: k
@@ -245,15 +245,15 @@ let cond_int64s is_x0 cmp a1 a2 dest succ k =
   | Clt -> Iop (OEsltl optR0, [ a1; a2 ], dest, succ) :: k
   | Cle ->
       let r = r2pi () in
-      Iop (OEsltl optR0, [ a2; a1 ], r, n2pi ())
+      Iop (OEsltl optR0, [ a2; a1 ], r, get tmp_reg)
       :: Iop (OExoriw Int.one, [ r ], dest, succ) :: k
   | Cgt -> Iop (OEsltl optR0, [ a2; a1 ], dest, succ) :: k
   | Cge ->
       let r = r2pi () in
-      Iop (OEsltl optR0, [ a1; a2 ], r, n2pi ())
+      Iop (OEsltl optR0, [ a1; a2 ], r, get tmp_reg)
       :: Iop (OExoriw Int.one, [ r ], dest, succ) :: k
 
-let cond_int64u is_x0 cmp a1 a2 dest succ k =
+let cond_int64u is_x0 cmp a1 a2 dest tmp_reg succ k =
   let optR0 = make_optR0 is_x0 (is_inv_cmp cmp) in
   match cmp with
   | Ceq -> Iop (OEsequl optR0, [ a1; a2 ], dest, succ) :: k
@@ -261,12 +261,12 @@ let cond_int64u is_x0 cmp a1 a2 dest succ k =
   | Clt -> Iop (OEsltul optR0, [ a1; a2 ], dest, succ) :: k
   | Cle ->
       let r = r2pi () in
-      Iop (OEsltul optR0, [ a2; a1 ], r, n2pi ())
+      Iop (OEsltul optR0, [ a2; a1 ], r, get tmp_reg)
       :: Iop (OExoriw Int.one, [ r ], dest, succ) :: k
   | Cgt -> Iop (OEsltul optR0, [ a2; a1 ], dest, succ) :: k
   | Cge ->
       let r = r2pi () in
-      Iop (OEsltul optR0, [ a1; a2 ], r, n2pi ())
+      Iop (OEsltul optR0, [ a1; a2 ], r, get tmp_reg)
       :: Iop (OExoriw Int.one, [ r ], dest, succ) :: k
 
 let is_normal_cmp = function Cne -> false | _ -> true
@@ -321,14 +321,18 @@ let expanse_cbranchimm_int64u cmp a1 n info succ1 succ2 k map_consts =
     let r' = unzip_head_tuple ht r in
     fst ht @ cbranch_int64u false cmp a1 r' info succ1 succ2 k
 
+let get_tmp_reg = function Cle | Cge -> Some (n2pi ()) | _ -> None
+
 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
+  if Int.eq n Int.zero then
+    let tmp_reg = get_tmp_reg cmp in
+    cond_int32s true cmp a1 a1 dest tmp_reg succ k
   else
     match cmp with
     | Ceq | Cne ->
         let r = r2pi () in
         xorimm32 a1 r n (n2pi ())
-          (cond_int32s true cmp r r dest succ k)
+          (cond_int32s true cmp r r dest None succ k)
           map_consts
     | Clt -> sltimm32 a1 dest n succ k map_consts
     | Cle ->
@@ -338,12 +342,14 @@ let expanse_condimm_int32s cmp a1 n dest succ k map_consts =
         else sltimm32 a1 dest (Int.add n Int.one) succ k map_consts
     | _ ->
         let r = r2pi () in
+        let tmp_reg = get_tmp_reg cmp in
         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
+        fst ht @ cond_int32s false cmp a1 r' dest tmp_reg 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
+  let tmp_reg = get_tmp_reg cmp in
+  if Int.eq n Int.zero then cond_int32u true cmp a1 a1 dest tmp_reg succ k
   else
     match cmp with
     | Clt -> sltuimm32 a1 dest n succ k map_consts
@@ -351,16 +357,18 @@ let expanse_condimm_int32u cmp a1 n dest succ k map_consts =
         let r = r2pi () in
         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
+        fst ht @ cond_int32u false cmp a1 r' dest tmp_reg 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
+  if Int64.eq n Int64.zero then
+    let tmp_reg = get_tmp_reg cmp in
+    cond_int64s true cmp a1 a1 dest tmp_reg 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)
+          (cond_int64s true cmp r r dest None succ k)
           map_consts
     | Clt -> sltimm64 a1 dest n succ k map_consts
     | Cle ->
@@ -370,12 +378,14 @@ let expanse_condimm_int64s cmp a1 n dest succ k map_consts =
         else sltimm64 a1 dest (Int64.add n Int64.one) succ k map_consts
     | _ ->
         let r = r2pi () in
+        let tmp_reg = get_tmp_reg cmp in
         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
+        fst ht @ cond_int64s false cmp a1 r' dest tmp_reg 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
+  let tmp_reg = get_tmp_reg cmp in
+  if Int64.eq n Int64.zero then cond_int64u true cmp a1 a1 dest tmp_reg succ k
   else
     match cmp with
     | Clt -> sltuimm64 a1 dest n succ k map_consts
@@ -383,7 +393,7 @@ let expanse_condimm_int64u cmp a1 n dest succ k map_consts =
         let r = r2pi () in
         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
+        fst ht @ cond_int64u false cmp a1 r' dest tmp_reg succ k
 
 let expanse_cond_fp cnot fn_cond cmp f1 f2 dest succ k =
   let normal = is_normal_cmp cmp in
@@ -437,16 +447,22 @@ let write_pathmap initial esize pm' =
   in
   pm' := PTree.set initial path' !pm'
 
-let rec write_tree exp current code' new_order =
+let rec write_tree exp initial current code' new_order =
+  let target_node, next_node =
+    if current = !node then (
+      node := !node + 1;
+      (P.to_int initial, current))
+    else (current, current - 1)
+  in
   match exp with
   | (Iop (_, _, _, succ) as inst) :: k ->
-      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
+      code' := PTree.set (P.of_int target_node) inst !code';
+      new_order := P.of_int target_node :: !new_order;
+      write_tree k initial next_node code' new_order
   | (Icond (_, _, succ1, succ2, _) as inst) :: k ->
-      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
+      code' := PTree.set (P.of_int target_node) inst !code';
+      new_order := P.of_int target_node :: !new_order;
+      write_tree k initial next_node code' new_order
   | [] -> ()
   | _ -> failwith "ExpansionOracle.write_tree: inconsistent instruction."
 
@@ -462,163 +478,171 @@ let expanse (sb : superblock) code pm =
   let map_consts = Hashtbl.create 100 in
   Array.iter
     (fun n ->
-      begin (
-        was_branch := false;
-        was_exp := false;
-        let inst = get_some @@ PTree.get n code in
-        if !Clflags.option_fexpanse_rtlcond then (
-        match inst with
-        (* Expansion of conditions - Ocmp *)
-        | Iop (Ocmp (Ccomp c), a1 :: a2 :: nil, 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) ->
-            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) ->
-            debug "Iop/Ccompimm\n";
-            exp := expanse_condimm_int32s c a1 imm dest succ [] map_consts;
-            was_exp := true
-        | Iop (Ocmp (Ccompuimm (c, imm)), a1 :: nil, dest, succ) ->
-            debug "Iop/Ccompuimm\n";
-            exp := expanse_condimm_int32u c a1 imm dest succ [] map_consts;
-            was_exp := true
-        | Iop (Ocmp (Ccompl c), a1 :: a2 :: nil, 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) ->
-            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) ->
-            debug "Iop/Ccomplimm\n";
-            exp := expanse_condimm_int64s c a1 imm dest succ [] map_consts;
-            was_exp := true
-        | Iop (Ocmp (Ccompluimm (c, imm)), a1 :: nil, dest, succ) ->
-            debug "Iop/Ccompluimm\n";
-            exp := expanse_condimm_int64u c a1 imm dest succ [] map_consts;
-            was_exp := true
-        | Iop (Ocmp (Ccompf c), f1 :: f2 :: nil, 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) ->
-            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) ->
-            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) ->
-            debug "Iop/Cnotcompfs\n";
-            exp := expanse_cond_fp true cond_single c f1 f2 dest succ [];
-            was_exp := true
-        (* Expansion of branches - Ccomp *)
-        | 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 [] map_consts;
-            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 [] map_consts;
-            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 [] map_consts;
-            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 [] map_consts;
-            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
-        | _ -> ());
-        if (!Clflags.option_fexpanse_fpconst && not !was_exp) then (
-        match inst with
-        (* Expansion of fp constants *)
-        | Iop (Ofloatconst f, nil, dest, succ) ->
-            debug "Iop/Ofloatconst\n";
-            let r = r2pi () in
-            exp :=
-              [
-                Iop (Olongconst (Floats.Float.to_bits f), [], r, n2pi ());
-                Iop (Ofloat_of_bits, [ r ], dest, succ);
-              ];
-            was_exp := true
-        | Iop (Osingleconst f, nil, dest, succ) ->
-            debug "Iop/Osingleconst\n";
-            let r = r2pi () in
-            exp :=
-              [
-                Iop (Ointconst (Floats.Float32.to_bits f), [], r, n2pi ());
-                Iop (Osingle_of_bits, [ r ], dest, succ);
-              ];
-            was_exp := true
-        | _ -> ());
-        if !was_exp then (
-          node := !node + 1;
-          (if !was_branch then
-           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
-               liveins := PTree.set new_branch_pc lives !liveins;
-               liveins := PTree.remove n !liveins
-           | _ -> ());
-          write_pathmap sb.instructions.(0) (List.length !exp) pm';
-          write_initial_node n code' new_order;
-          write_tree !exp !node code' new_order)
-          else new_order := n :: !new_order)
-      end)
+      was_branch := false;
+      was_exp := false;
+      let inst = get_some @@ PTree.get n code in
+      (if !Clflags.option_fexpanse_rtlcond then
+       match inst with
+       (* Expansion of conditions - Ocmp *)
+       | Iop (Ocmp (Ccomp c), a1 :: a2 :: nil, dest, succ) ->
+           debug "Iop/Ccomp\n";
+           let tmp_reg = get_tmp_reg c in
+           exp := cond_int32s false c a1 a2 dest tmp_reg succ [];
+           was_exp := true
+       | Iop (Ocmp (Ccompu c), a1 :: a2 :: nil, dest, succ) ->
+           debug "Iop/Ccompu\n";
+           let tmp_reg = get_tmp_reg c in
+           exp := cond_int32u false c a1 a2 dest tmp_reg succ [];
+           was_exp := true
+       | Iop (Ocmp (Ccompimm (c, imm)), a1 :: nil, dest, succ) ->
+           debug "Iop/Ccompimm\n";
+           exp := expanse_condimm_int32s c a1 imm dest succ [] map_consts;
+           was_exp := true
+       | Iop (Ocmp (Ccompuimm (c, imm)), a1 :: nil, dest, succ) ->
+           debug "Iop/Ccompuimm\n";
+           exp := expanse_condimm_int32u c a1 imm dest succ [] map_consts;
+           was_exp := true
+       | Iop (Ocmp (Ccompl c), a1 :: a2 :: nil, dest, succ) ->
+           debug "Iop/Ccompl\n";
+           let tmp_reg = get_tmp_reg c in
+           exp := cond_int64s false c a1 a2 dest tmp_reg succ [];
+           was_exp := true
+       | Iop (Ocmp (Ccomplu c), a1 :: a2 :: nil, dest, succ) ->
+           debug "Iop/Ccomplu\n";
+           let tmp_reg = get_tmp_reg c in
+           exp := cond_int64u false c a1 a2 dest tmp_reg succ [];
+           was_exp := true
+       | Iop (Ocmp (Ccomplimm (c, imm)), a1 :: nil, dest, succ) ->
+           debug "Iop/Ccomplimm\n";
+           exp := expanse_condimm_int64s c a1 imm dest succ [] map_consts;
+           was_exp := true
+       | Iop (Ocmp (Ccompluimm (c, imm)), a1 :: nil, dest, succ) ->
+           debug "Iop/Ccompluimm\n";
+           exp := expanse_condimm_int64u c a1 imm dest succ [] map_consts;
+           was_exp := true
+       | Iop (Ocmp (Ccompf c), f1 :: f2 :: nil, 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) ->
+           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) ->
+           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) ->
+           debug "Iop/Cnotcompfs\n";
+           exp := expanse_cond_fp true cond_single c f1 f2 dest succ [];
+           was_exp := true
+       (* Expansion of branches - Ccomp *)
+       | 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 [] map_consts;
+           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 [] map_consts;
+           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 [] map_consts;
+           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 [] map_consts;
+           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
+       | _ -> ());
+      (if !Clflags.option_fexpanse_fpconst && not !was_exp then
+       match inst with
+       (* Expansion of fp constants *)
+       | Iop (Ofloatconst f, nil, dest, succ) ->
+           debug "Iop/Ofloatconst\n";
+           let r = r2pi () in
+           exp :=
+             [
+               Iop (Olongconst (Floats.Float.to_bits f), [], r, n2pi ());
+               Iop (Ofloat_of_bits, [ r ], dest, succ);
+             ];
+           was_exp := true
+       | Iop (Osingleconst f, nil, dest, succ) ->
+           debug "Iop/Osingleconst\n";
+           let r = r2pi () in
+           exp :=
+             [
+               Iop (Ointconst (Floats.Float32.to_bits f), [], r, n2pi ());
+               Iop (Osingle_of_bits, [ r ], dest, succ);
+             ];
+           was_exp := true
+       | _ -> ());
+      if !was_exp then (
+        (*node := !node + 1;*)
+        (*(if !was_branch then
+          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
+              liveins := PTree.set new_branch_pc lives !liveins;
+              liveins := PTree.remove n !liveins
+          | _ -> ());*)
+        write_pathmap sb.instructions.(0) (List.length !exp - 1) pm';
+        (*write_initial_node n code' new_order;*)
+        write_tree !exp n !node code' new_order)
+      else new_order := n :: !new_order)
     sb.instructions;
   sb.instructions <- Array.of_list (List.rev !new_order);
   sb.liveins <- !liveins;