branches expansions support

4 files changed, 404 insertions, 29 deletions

diff --git a/riscV/BTL_SEsimplify.v b/riscV/BTL_SEsimplify.v
index 0cdea5fe..baa4edeb 100644
--- a/riscV/BTL_SEsimplify.v
+++ b/riscV/BTL_SEsimplify.v
@@ -258,6 +258,55 @@ Definition expanse_cond_fp (cnot: bool) fn_cond cmp (lsv: list_sval) :=
   let lfsv := make_lfsv_single fsv in
   if normal' then fsv else fSop (OExoriw Int.one) lfsv.
 
+(** ** Branches instructions *)
+
+Definition transl_cbranch_int32s (cmp: comparison) (optR: option oreg) :=
+  match cmp with
+  | Ceq => CEbeqw optR
+  | Cne => CEbnew optR
+  | Clt => CEbltw optR
+  | Cle => CEbgew optR
+  | Cgt => CEbltw optR
+  | Cge => CEbgew optR
+  end.
+
+Definition transl_cbranch_int32u (cmp: comparison) (optR: option oreg) :=
+  match cmp with
+  | Ceq => CEbequw optR
+  | Cne => CEbneuw optR
+  | Clt => CEbltuw optR
+  | Cle => CEbgeuw optR
+  | Cgt => CEbltuw optR
+  | Cge => CEbgeuw optR
+  end.
+
+Definition transl_cbranch_int64s (cmp: comparison) (optR: option oreg) :=
+  match cmp with
+  | Ceq => CEbeql optR
+  | Cne => CEbnel optR
+  | Clt => CEbltl optR
+  | Cle => CEbgel optR
+  | Cgt => CEbltl optR
+  | Cge => CEbgel optR
+  end.
+
+Definition transl_cbranch_int64u (cmp: comparison) (optR: option oreg) :=
+  match cmp with
+  | Ceq => CEbequl optR
+  | Cne => CEbneul optR
+  | Clt => CEbltul optR
+  | Cle => CEbgeul optR
+  | Cgt => CEbltul optR
+  | Cge => CEbgeul optR
+  end.
+
+Definition expanse_cbranch_fp (cnot: bool) fn_cond cmp (lfsv: list_sval) : (condition * list_sval) :=
+  let normal := is_normal_cmp cmp in
+  let normal' := if cnot then negb normal else normal in
+  let fsv := fn_cond cmp lfsv in
+  let lfsv' := make_lfsv_cmp false fsv fsv in
+  if normal' then ((CEbnew (Some X0_R)), lfsv') else ((CEbeqw (Some X0_R)), lfsv').
+
 (** Target op simplifications using "fake" values *)
 
 Definition target_op_simplify (op: operation) (lr: list reg) (hrs: ristate): option sval :=
@@ -437,7 +486,109 @@ Definition target_op_simplify (op: operation) (lr: list reg) (hrs: ristate): opt
   end.
 
 Definition target_cbranch_expanse (prev: ristate) (cond: condition) (args: list reg) : option (condition * list_sval) :=
-  None.
+  match cond, args with
+  | (Ccomp c), (a1 :: a2 :: nil) =>
+      let is_inv := is_inv_cmp_int c in
+      let cond := transl_cbranch_int32s c (make_optR false is_inv) in
+      let fsv1 := ris_sreg_get prev a1 in
+      let fsv2 := ris_sreg_get prev a2 in
+      let lfsv := make_lfsv_cmp is_inv fsv1 fsv2 in
+      Some (cond, lfsv)
+  | (Ccompu c), (a1 :: a2 :: nil) =>
+      let is_inv := is_inv_cmp_int c in
+      let cond := transl_cbranch_int32u c (make_optR false is_inv) in
+      let fsv1 := ris_sreg_get prev a1 in
+      let fsv2 := ris_sreg_get prev a2 in
+      let lfsv := make_lfsv_cmp is_inv fsv1 fsv2 in
+      Some (cond, lfsv)
+  | (Ccompimm c n), (a1 :: nil) =>
+      let is_inv := is_inv_cmp_int c in
+      let fsv1 := ris_sreg_get prev a1 in
+      (if Int.eq n Int.zero then
+        let lfsv := make_lfsv_cmp is_inv fsv1 fsv1 in
+        let cond := transl_cbranch_int32s c (make_optR true is_inv) in
+        Some (cond, lfsv)
+      else
+        let fsv := loadimm32 n in
+        let lfsv := make_lfsv_cmp is_inv fsv1 fsv in
+        let cond := transl_cbranch_int32s c (make_optR false is_inv) in
+        Some (cond, lfsv))
+  | (Ccompuimm c n), (a1 :: nil) =>
+      let is_inv := is_inv_cmp_int c in
+      let fsv1 := ris_sreg_get prev a1 in
+      (if Int.eq n Int.zero then
+        let lfsv := make_lfsv_cmp is_inv fsv1 fsv1 in
+        let cond := transl_cbranch_int32u c (make_optR true is_inv) in
+        Some (cond, lfsv)
+      else
+        let fsv := loadimm32 n in
+        let lfsv := make_lfsv_cmp is_inv fsv1 fsv in
+        let cond := transl_cbranch_int32u c (make_optR false is_inv) in
+         Some (cond, lfsv))
+  | (Ccompl c), (a1 :: a2 :: nil) =>
+      let is_inv := is_inv_cmp_int c in
+      let cond := transl_cbranch_int64s c (make_optR false is_inv) in
+      let fsv1 := ris_sreg_get prev a1 in
+      let fsv2 := ris_sreg_get prev a2 in
+      let lfsv := make_lfsv_cmp is_inv fsv1 fsv2 in
+      Some (cond, lfsv)
+  | (Ccomplu c), (a1 :: a2 :: nil) =>
+      let is_inv := is_inv_cmp_int c in
+      let cond := transl_cbranch_int64u c (make_optR false is_inv) in
+      let fsv1 := ris_sreg_get prev a1 in
+      let fsv2 := ris_sreg_get prev a2 in
+      let lfsv := make_lfsv_cmp is_inv fsv1 fsv2 in
+      Some (cond, lfsv)
+  | (Ccomplimm c n), (a1 :: nil) =>
+      let is_inv := is_inv_cmp_int c in
+      let fsv1 := ris_sreg_get prev a1 in
+      (if Int64.eq n Int64.zero then
+        let lfsv := make_lfsv_cmp is_inv fsv1 fsv1 in
+        let cond := transl_cbranch_int64s c (make_optR true is_inv) in
+        Some (cond, lfsv)
+      else
+        let fsv := loadimm64 n in
+        let lfsv := make_lfsv_cmp is_inv fsv1 fsv in
+        let cond := transl_cbranch_int64s c (make_optR false is_inv) in
+        Some (cond, lfsv))
+  | (Ccompluimm c n), (a1 :: nil) =>
+      let is_inv := is_inv_cmp_int c in
+      let fsv1 := ris_sreg_get prev a1 in
+      (if Int64.eq n Int64.zero then
+        let lfsv := make_lfsv_cmp is_inv fsv1 fsv1 in
+        let cond := transl_cbranch_int64u c (make_optR true is_inv) in
+        Some (cond, lfsv)
+      else
+        let fsv := loadimm64 n in
+        let lfsv := make_lfsv_cmp is_inv fsv1 fsv in
+        let cond := transl_cbranch_int64u c (make_optR false is_inv) in
+        Some (cond, lfsv))
+  | (Ccompf c), (f1 :: f2 :: nil) =>
+      let fsv1 := ris_sreg_get prev f1 in
+      let fsv2 := ris_sreg_get prev f2 in
+      let is_inv := is_inv_cmp_float c in
+      let lfsv := make_lfsv_cmp is_inv fsv1 fsv2 in
+      Some (expanse_cbranch_fp false cond_float c lfsv)
+  | (Cnotcompf c), (f1 :: f2 :: nil) =>
+      let fsv1 := ris_sreg_get prev f1 in
+      let fsv2 := ris_sreg_get prev f2 in
+      let is_inv := is_inv_cmp_float c in
+      let lfsv := make_lfsv_cmp is_inv fsv1 fsv2 in
+      Some (expanse_cbranch_fp true cond_float c lfsv)
+  | (Ccompfs c), (f1 :: f2 :: nil) =>
+      let fsv1 := ris_sreg_get prev f1 in
+      let fsv2 := ris_sreg_get prev f2 in
+      let is_inv := is_inv_cmp_float c in
+      let lfsv := make_lfsv_cmp is_inv fsv1 fsv2 in
+      Some (expanse_cbranch_fp false cond_single c lfsv)
+  | (Cnotcompfs c), (f1 :: f2 :: nil) =>
+      let fsv1 := ris_sreg_get prev f1 in
+      let fsv2 := ris_sreg_get prev f2 in
+      let is_inv := is_inv_cmp_float c in
+      let lfsv := make_lfsv_cmp is_inv fsv1 fsv2 in
+      Some (expanse_cbranch_fp true cond_single c lfsv)
+  | _, _ => None
+   end.
 
 (** * Auxiliary lemmas on comparisons *)
 
@@ -1706,17 +1857,84 @@ Proof.
   - eapply simplify_cnotcompfs_correct; eauto.
 Qed.
 
-(*
-Lemma target_cbranch_expanse_correct hrs c l ge sp rs0 m0 st c' l': forall
+Lemma target_cbranch_expanse_correct hrs c l ctx st c' l': forall
   (TARGET: target_cbranch_expanse hrs c l = Some (c', l'))
-  (LREF : hsilocal_refines ge sp rs0 m0 hrs st)
-  (OK: hsok_local ge sp rs0 m0 hrs),
-  seval_condition ge sp c' (hsval_list_proj l') (si_smem st) rs0 m0 =
-  seval_condition ge sp c (list_sval_inj (map (si_sreg st) l)) (si_smem st) rs0 m0.
+  (REF: ris_refines ctx hrs st)
+  (OK: ris_ok ctx hrs),
+  eval_scondition ctx c' l' =
+  eval_scondition ctx c (list_sval_inj (map (si_sreg st) l)).
 Proof.
-  unfold target_cbranch_expanse, seval_condition; simpl.
-  intros H (LREF & SREF & SREG & SMEM) ?.
-  congruence.
+  unfold target_cbranch_expanse, eval_scondition; simpl.
+  intros H ? ?. inversion REF.
+  destruct c; try congruence;
+  repeat (destruct l; simpl in H; try congruence).
+  1,2,5,6:
+    destruct c; inv H; simpl;
+    rewrite !REG_EQ;
+    try (destruct (eval_smem ctx (si_smem st)) eqn:OKmem; try congruence);
+    try (destruct (eval_sval ctx (si_sreg st r)) eqn:OKv1; try congruence);
+    try (destruct (eval_sval ctx (si_sreg st r0)) eqn:OKv2; try congruence);
+    try replace (Cle) with (swap_comparison Cge) by auto;
+    try replace (Clt) with (swap_comparison Cgt) by auto;
+    try rewrite Val.swap_cmp_bool; trivial;
+    try rewrite Val.swap_cmpu_bool; trivial;
+    try rewrite Val.swap_cmpl_bool; trivial;
+    try rewrite Val.swap_cmplu_bool; trivial.
+  1,2,3,4:
+    try destruct (Int.eq n Int.zero) eqn: EQIMM;
+    try apply Int.same_if_eq in EQIMM;
+    try destruct (Int64.eq n Int64.zero) eqn: EQIMM;
+    try apply Int64.same_if_eq in EQIMM;
+    destruct c; inv H; simpl;
+    rewrite !REG_EQ;
+    try (destruct (eval_smem ctx (si_smem st)) eqn:OKmem; try congruence);
+    try (destruct (eval_sval ctx (si_sreg st r)) eqn:OKv1; try congruence);
+    try (destruct (eval_sval ctx (si_sreg st r0)) eqn:OKv2; try congruence);
+    unfold loadimm32, load_hilo32, Val.cmp, Val.cmpu, zero32;
+    unfold loadimm64, load_hilo64, Val.cmpl, Val.cmplu, zero64;
+    intros; try (specialize make_immed32_sound with (n);
+    destruct (make_immed32 n) eqn:EQMKI); intros; simpl;
+    intros; try (specialize make_immed64_sound with (n);
+    destruct (make_immed64 n) eqn:EQMKI); intros; simpl;
+    try rewrite EQLO; simpl;
+    try destruct (Int.eq lo Int.zero) eqn:EQLO;
+    try destruct (Int64.eq lo Int64.zero) eqn:EQLO;
+    try apply Int.same_if_eq in EQLO; simpl; trivial;
+    try apply Int64.same_if_eq in EQLO; simpl; trivial;
+    unfold eval_may_undef; 
+    try erewrite !fsi_sreg_get_correct; eauto;
+    try rewrite OKv1; simpl; trivial;
+    try destruct v; try rewrite H;
+    try rewrite ltu_12_wordsize; try rewrite EQLO;
+    try rewrite Int.add_commut, Int.add_zero_l;
+    try rewrite Int64.add_commut, Int64.add_zero_l;
+    try rewrite Int64.add_commut;
+    try rewrite Int.add_zero_l; try rewrite Int64.add_zero_l;
+    auto; simpl;
+    try rewrite H in EQIMM;
+    try rewrite EQLO in EQIMM;
+    try rewrite Int.add_commut, Int.add_zero_l in EQIMM;
+    try rewrite Int64.add_commut, Int64.add_zero_l in EQIMM;
+    try rewrite EQIMM; simpl;
+    try destruct (Archi.ptr64); trivial.
+
+    1,2,3,4:
+    destruct c; inv H; simpl;
+    rewrite !REG_EQ;
+    try (destruct (eval_smem ctx (si_smem st)) eqn:OKmem; try congruence);
+    try (destruct (eval_sval ctx (si_sreg st r)) eqn:OKv1; try congruence);
+    try (destruct (eval_sval ctx (si_sreg st r0)) eqn:OKv2; try congruence);
+    unfold zero32, zero64, Val.cmpf, Val.cmpfs;
+    destruct v, v0; simpl; trivial;
+    try rewrite Float.cmp_ne_eq;
+    try rewrite Float32.cmp_ne_eq;
+    try rewrite <- Float.cmp_swap; simpl;
+    try rewrite <- Float32.cmp_swap; simpl;
+    try destruct (Float.cmp _ _); simpl;
+    try destruct (Float32.cmp _ _); simpl;
+    try rewrite Int.eq_true; simpl;
+    try rewrite Int.eq_false; try apply Int.one_not_zero;
+    simpl; trivial.
 Qed.
 Global Opaque target_op_simplify.
-   Global Opaque target_cbranch_expanse.*)
+Global Opaque target_cbranch_expanse.
diff --git a/riscV/ExpansionOracle.ml b/riscV/ExpansionOracle.ml
index 2a21b7a4..7295ae0d 100644
--- a/riscV/ExpansionOracle.ml
+++ b/riscV/ExpansionOracle.ml
@@ -339,6 +339,46 @@ let is_inv_cmp = function Cle | Cgt -> true | _ -> false
 let make_optR is_x0 is_inv =
   if is_x0 then if is_inv then Some X0_L else Some X0_R else None
 
+let cbranch_int32s is_x0 cmp a1 a2 iinfo succ1 succ2 k =
+  let optR = make_optR is_x0 (is_inv_cmp cmp) in
+  match cmp with
+  | Ceq -> Scond (CEbeqw optR, [ a1; a2 ], succ1, succ2, iinfo) :: k
+  | Cne -> Scond (CEbnew optR, [ a1; a2 ], succ1, succ2, iinfo) :: k
+  | Clt -> Scond (CEbltw optR, [ a1; a2 ], succ1, succ2, iinfo) :: k
+  | Cle -> Scond (CEbgew optR, [ a2; a1 ], succ1, succ2, iinfo) :: k
+  | Cgt -> Scond (CEbltw optR, [ a2; a1 ], succ1, succ2, iinfo) :: k
+  | Cge -> Scond (CEbgew optR, [ a1; a2 ], succ1, succ2, iinfo) :: k
+
+let cbranch_int32u is_x0 cmp a1 a2 iinfo succ1 succ2 k =
+  let optR = make_optR is_x0 (is_inv_cmp cmp) in
+  match cmp with
+  | Ceq -> Scond (CEbequw optR, [ a1; a2 ], succ1, succ2, iinfo) :: k
+  | Cne -> Scond (CEbneuw optR, [ a1; a2 ], succ1, succ2, iinfo) :: k
+  | Clt -> Scond (CEbltuw optR, [ a1; a2 ], succ1, succ2, iinfo) :: k
+  | Cle -> Scond (CEbgeuw optR, [ a2; a1 ], succ1, succ2, iinfo) :: k
+  | Cgt -> Scond (CEbltuw optR, [ a2; a1 ], succ1, succ2, iinfo) :: k
+  | Cge -> Scond (CEbgeuw optR, [ a1; a2 ], succ1, succ2, iinfo) :: k
+
+let cbranch_int64s is_x0 cmp a1 a2 iinfo succ1 succ2 k =
+  let optR = make_optR is_x0 (is_inv_cmp cmp) in
+  match cmp with
+  | Ceq -> Scond (CEbeql optR, [ a1; a2 ], succ1, succ2, iinfo) :: k
+  | Cne -> Scond (CEbnel optR, [ a1; a2 ], succ1, succ2, iinfo) :: k
+  | Clt -> Scond (CEbltl optR, [ a1; a2 ], succ1, succ2, iinfo) :: k
+  | Cle -> Scond (CEbgel optR, [ a2; a1 ], succ1, succ2, iinfo) :: k
+  | Cgt -> Scond (CEbltl optR, [ a2; a1 ], succ1, succ2, iinfo) :: k
+  | Cge -> Scond (CEbgel optR, [ a1; a2 ], succ1, succ2, iinfo) :: k
+
+let cbranch_int64u is_x0 cmp a1 a2 iinfo succ1 succ2 k =
+  let optR = make_optR is_x0 (is_inv_cmp cmp) in
+  match cmp with
+  | Ceq -> Scond (CEbequl optR, [ a1; a2 ], succ1, succ2, iinfo) :: k
+  | Cne -> Scond (CEbneul optR, [ a1; a2 ], succ1, succ2, iinfo) :: k
+  | Clt -> Scond (CEbltul optR, [ a1; a2 ], succ1, succ2, iinfo) :: k
+  | Cle -> Scond (CEbgeul optR, [ a2; a1 ], succ1, succ2, iinfo) :: k
+  | Cgt -> Scond (CEbltul optR, [ a2; a1 ], succ1, succ2, iinfo) :: k
+  | Cge -> Scond (CEbgeul optR, [ a1; a2 ], succ1, succ2, iinfo) :: k
+
 let cond_int32s vn is_x0 cmp a1 a2 dest =
   let optR = make_optR is_x0 (is_inv_cmp cmp) in
   match cmp with
@@ -439,6 +479,40 @@ let cond_single vn cmp f1 f2 dest =
   | Cgt -> [ addinst vn OEflts [ f2; f1 ] dest ]
   | Cge -> [ addinst vn OEfles [ f2; f1 ] dest ]
 
+let expanse_cbranchimm_int32s vn cmp a1 n iinfo succ1 succ2 =
+  if Int.eq n Int.zero then cbranch_int32s true cmp a1 a1 iinfo succ1 succ2 []
+  else
+    let r = r2pi () in
+    let l = loadimm32 vn r n in
+    let r', l' = extract_arg l in
+    cbranch_int32s false cmp a1 r' iinfo succ1 succ2 l'
+
+let expanse_cbranchimm_int32u vn cmp a1 n iinfo succ1 succ2 =
+  if Int.eq n Int.zero then cbranch_int32u true cmp a1 a1 iinfo succ1 succ2 []
+  else
+    let r = r2pi () in
+    let l = loadimm32 vn r n in
+    let r', l' = extract_arg l in
+    cbranch_int32u false cmp a1 r' iinfo succ1 succ2 l'
+
+let expanse_cbranchimm_int64s vn cmp a1 n iinfo succ1 succ2 =
+  if Int64.eq n Int64.zero then
+    cbranch_int64s true cmp a1 a1 iinfo succ1 succ2 []
+  else
+    let r = r2pi () in
+    let l = loadimm64 vn r n in
+    let r', l' = extract_arg l in
+    cbranch_int64s false cmp a1 r' iinfo succ1 succ2 l'
+
+let expanse_cbranchimm_int64u vn cmp a1 n iinfo succ1 succ2 =
+  if Int64.eq n Int64.zero then
+    cbranch_int64u true cmp a1 a1 iinfo succ1 succ2 []
+  else
+    let r = r2pi () in
+    let l = loadimm64 vn r n in
+    let r', l' = extract_arg l in
+    cbranch_int64u false cmp a1 r' iinfo succ1 succ2 l'
+
 let expanse_condimm_int32s vn cmp a1 n dest =
   if Int.eq n Int.zero then cond_int32s vn true cmp a1 a1 dest
   else
@@ -514,6 +588,16 @@ let expanse_cond_fp vn cnot fn_cond cmp f1 f2 dest =
     let r', l = extract_arg insn in
     addinst vn (OExoriw Int.one) [ r' ] dest :: l
 
+let expanse_cbranch_fp vn cnot fn_cond cmp f1 f2 iinfo succ1 succ2 =
+  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 vn cmp f1 f2 r in
+  let r', l = extract_arg insn in
+  if normal' then
+    Scond (CEbnew (Some X0_R), [ r'; r' ], succ1, succ2, iinfo) :: l
+  else Scond (CEbeqw (Some X0_R), [ r'; r' ], succ1, succ2, iinfo) :: l
+
 (** Return olds args if the CSE numbering is empty *)
 
 let get_arguments vn vals args =
@@ -529,22 +613,26 @@ let rec gen_btl_list vn exp =
       inst :: gen_btl_list vn k
   | [ Sexp (rd, Smove, args, iinfo) ] -> [ Bop (Omove, args, rd, iinfo) ]
   | [ Scond (cond, args, succ1, succ2, iinfo) ] ->
-      [ Bcond (cond, args, succ1, succ2, iinfo) ]
+      let ib = Bcond (cond, args, succ1, succ2, iinfo) in
+      [ ib ]
   | [] -> []
   | _ -> failwith "write_tree: invalid list"
 
 let expanse_list li =
   debug "#### New block for expansion oracle\n";
   let exp = ref [] in
+  let was_branch = ref false in
   let was_exp = ref false in
   let vn = ref (empty_numbering ()) in
   let rec expanse_list_rec li =
     match li with
     | [] -> li
     | i :: li' ->
+        was_branch := false;
         was_exp := false;
         (if !Clflags.option_fexpanse_rtlcond then
          match i with
+         (* Expansion of conditions - Ocmp *)
          | Bop (Ocmp (Ccomp c), a1 :: a2 :: nil, dest, iinfo) ->
              debug "Bop/Ccomp\n";
              exp := cond_int32s vn false c a1 a2 dest;
@@ -605,9 +693,75 @@ let expanse_list li =
              exp := expanse_cond_fp vn true cond_single c f1 f2 dest;
              exp := extract_final vn !exp dest;
              was_exp := true
+         (* Expansion of branches - Ccomp *)
+         | Bcond (Ccomp c, a1 :: a2 :: nil, succ1, succ2, iinfo) ->
+             debug "Bcond/Ccomp\n";
+             exp := cbranch_int32s false c a1 a2 iinfo succ1 succ2 [];
+             was_branch := true;
+             was_exp := true
+         | Bcond (Ccompu c, a1 :: a2 :: nil, succ1, succ2, iinfo) ->
+             debug "Bcond/Ccompu\n";
+             exp := cbranch_int32u false c a1 a2 iinfo succ1 succ2 [];
+             was_branch := true;
+             was_exp := true
+         | Bcond (Ccompimm (c, imm), a1 :: nil, succ1, succ2, iinfo) ->
+             debug "Bcond/Ccompimm\n";
+             exp := expanse_cbranchimm_int32s vn c a1 imm iinfo succ1 succ2;
+             was_branch := true;
+             was_exp := true
+         | Bcond (Ccompuimm (c, imm), a1 :: nil, succ1, succ2, iinfo) ->
+             debug "Bcond/Ccompuimm\n";
+             exp := expanse_cbranchimm_int32u vn c a1 imm iinfo succ1 succ2;
+             was_branch := true;
+             was_exp := true
+         | Bcond (Ccompl c, a1 :: a2 :: nil, succ1, succ2, iinfo) ->
+             debug "Bcond/Ccompl\n";
+             exp := cbranch_int64s false c a1 a2 iinfo succ1 succ2 [];
+             was_branch := true;
+             was_exp := true
+         | Bcond (Ccomplu c, a1 :: a2 :: nil, succ1, succ2, iinfo) ->
+             debug "Bcond/Ccomplu\n";
+             exp := cbranch_int64u false c a1 a2 iinfo succ1 succ2 [];
+             was_branch := true;
+             was_exp := true
+         | Bcond (Ccomplimm (c, imm), a1 :: nil, succ1, succ2, iinfo) ->
+             debug "Bcond/Ccomplimm\n";
+             exp := expanse_cbranchimm_int64s vn c a1 imm iinfo succ1 succ2;
+             was_branch := true;
+             was_exp := true
+         | Bcond (Ccompluimm (c, imm), a1 :: nil, succ1, succ2, iinfo) ->
+             debug "Bcond/Ccompluimm\n";
+             exp := expanse_cbranchimm_int64u vn c a1 imm iinfo succ1 succ2;
+             was_branch := true;
+             was_exp := true
+         | Bcond (Ccompf c, f1 :: f2 :: nil, succ1, succ2, iinfo) ->
+             debug "Bcond/Ccompf\n";
+             exp :=
+               expanse_cbranch_fp vn false cond_float c f1 f2 iinfo succ1 succ2;
+             was_branch := true;
+             was_exp := true
+         | Bcond (Cnotcompf c, f1 :: f2 :: nil, succ1, succ2, iinfo) ->
+             debug "Bcond/Cnotcompf\n";
+             exp :=
+               expanse_cbranch_fp vn true cond_float c f1 f2 iinfo succ1 succ2;
+             was_branch := true;
+             was_exp := true
+         | Bcond (Ccompfs c, f1 :: f2 :: nil, succ1, succ2, iinfo) ->
+             debug "Bcond/Ccompfs\n";
+             exp :=
+               expanse_cbranch_fp vn false cond_single c f1 f2 iinfo succ1 succ2;
+             was_branch := true;
+             was_exp := true
+         | Bcond (Cnotcompfs c, f1 :: f2 :: nil, succ1, succ2, iinfo) ->
+             debug "Bcond/Cnotcompfs\n";
+             exp :=
+               expanse_cbranch_fp vn true cond_single c f1 f2 iinfo succ1 succ2;
+             was_branch := true;
+             was_exp := true
          | _ -> ());
         (if !Clflags.option_fexpanse_others && not !was_exp then
          match i with
+         (* Others expansions *)
          | Bop (Ofloatconst f, nil, dest, iinfo) -> (
              match make_immed64 (Floats.Float.to_bits f) with
              | Imm64_single _ | Imm64_large _ -> ()
@@ -814,7 +968,9 @@ let expanse_list li =
               (* TODO gourdinl empty numb BF? vn := empty_numbering ()*)
           | _ -> ());
           i :: expanse_list_rec li')
-        else gen_btl_list vn (List.rev !exp) @ expanse_list_rec li'
+        else
+          let hd = gen_btl_list vn (List.rev !exp) in
+          hd @ expanse_list_rec li'
   in
   expanse_list_rec li
 
diff --git a/scheduling/BTL_SEimpl.v b/scheduling/BTL_SEimpl.v
index 7711c72d..305c3cfa 100644
--- a/scheduling/BTL_SEimpl.v
+++ b/scheduling/BTL_SEimpl.v
@@ -682,12 +682,13 @@ Lemma cbranch_expanse_correct hrs c l:
   (REF : ris_refines ctx hrs sis)
   (OK: ris_ok ctx hrs),
   eval_scondition ctx (fst r) (snd r) =
-  eval_scondition ctx c (list_sval_inj (map (si_sreg sis) l))
-  /\ (fst r) = c.
+  eval_scondition ctx c (list_sval_inj (map (si_sreg sis) l)).
 Proof.
   unfold cbranch_expanse.
-  wlp_simplify; inv REF.
-  unfold eval_scondition; erewrite <- H; eauto.
+  destruct (target_cbranch_expanse _ _ _) eqn: TARGET; wlp_simplify;
+  unfold eval_scondition; try erewrite <- H; inversion REF; eauto.
+  destruct p as [c' l']; simpl.
+  exploit target_cbranch_expanse_correct; eauto.
 Qed.
 Local Hint Resolve cbranch_expanse_correct: wlp.
 Global Opaque cbranch_expanse.
@@ -1133,9 +1134,9 @@ Proof.
       erewrite <- OK_EQUIV. 2: eauto.
       eapply sexec_rec_okpreserv with (ib:=(Bcond cond args ib1 ib2 iinfo)); simpl; eauto.
     }
-    exploit (Refcond ctx cond (snd exta) (list_sval_inj (map sis args)) exta0 exta1
+    exploit (Refcond ctx (fst exta) cond (snd exta) (list_sval_inj (map sis args)) exta0 exta1
               (sexec_rec (cf ctx) ib1 sis k) (sexec_rec (cf ctx) ib2 sis k));
-    exploit H; eauto; intros (SEVAL & EQC); subst; auto.
+    exploit H; eauto; intros SEVAL; auto.
     all:
       simpl in SOUT; generalize SOUT; clear SOUT;
       inversion_SOME b0; try_simplify_someHyps.
@@ -1217,9 +1218,9 @@ Proof.
     assert (rOK: ris_ok ctx hrs). {
       simpl in H2; generalize H2; inversion_SOME b0; destruct b0; try_simplify_someHyps.
     }
-    exploit (Refcond ctx cond (snd exta) (list_sval_inj (map sis args)) exta0 exta1
+    exploit (Refcond ctx (fst exta) cond (snd exta) (list_sval_inj (map sis args)) exta0 exta1
               (sexec_rec (cf ctx) ib1 sis k) (sexec_rec (cf ctx) ib2 sis k));
-    exploit H; eauto; intros (SEVAL & EQC); subst; auto.
+    exploit H; eauto; intros SEVAL; auto.
     all:
       simpl in H2; generalize H2; clear H2;
       inversion_SOME b0; try_simplify_someHyps.
@@ -1444,11 +1445,11 @@ Fixpoint rst_simu_check (rst1 rst2: rstate) {struct rst1} :=
       hrs_simu_check hrs1 hrs2;;
       sfval_simu_check sfv1 sfv2
   | Rcond cond1 lsv1 rsL1 rsR1, Rcond cond2 lsv2 rsL2 rsR2 =>
-      struct_check cond1 cond2 "hsstate_simu_check: conditions do not match";;
-      phys_check lsv1 lsv2 "hsstate_simu_check: args do not match";;
+      struct_check cond1 cond2 "rst_simu_check: conditions do not match";;
+      phys_check lsv1 lsv2 "rst_simu_check: args do not match";;
       rst_simu_check rsL1 rsL2;;
       rst_simu_check rsR1 rsR2
-  | _, _ => FAILWITH "hsstate_simu_check: simu_check failed"
+  | _, _ => FAILWITH "rst_simu_check: simu_check failed"
   end.
 
 Lemma rst_simu_check_correct rst1: forall rst2,
diff --git a/scheduling/BTL_SEsimuref.v b/scheduling/BTL_SEsimuref.v
index c812c607..7af1af62 100644
--- a/scheduling/BTL_SEsimuref.v
+++ b/scheduling/BTL_SEsimuref.v
@@ -260,11 +260,11 @@ Inductive rst_refines ctx: rstate -> sstate -> Prop :=
       (RIS: ris_refines ctx ris sis)
       (RFV: ris_ok ctx ris -> rfv_refines ctx rfv sfv)
       : rst_refines ctx (Rfinal ris rfv) (Sfinal sis sfv)
-  | Refcond cond rargs args rifso rifnot ifso ifnot
-      (RCOND: eval_scondition ctx cond rargs = eval_scondition ctx cond args)
-      (REFso: eval_scondition ctx cond rargs = Some true -> rst_refines ctx rifso ifso)
-      (REFnot: eval_scondition ctx cond rargs = Some false -> rst_refines ctx rifnot ifnot)
-      : rst_refines ctx (Rcond cond rargs rifso rifnot) (Scond cond args ifso ifnot)
+  | Refcond rcond cond rargs args rifso rifnot ifso ifnot
+      (RCOND: eval_scondition ctx rcond rargs = eval_scondition ctx cond args)
+      (REFso: eval_scondition ctx rcond rargs = Some true -> rst_refines ctx rifso ifso)
+      (REFnot: eval_scondition ctx rcond rargs = Some false -> rst_refines ctx rifnot ifnot)
+      : rst_refines ctx (Rcond rcond rargs rifso rifnot) (Scond cond args ifso ifnot)
   | Refabort
       : rst_refines ctx Rabort Sabort
   .