branches expansions support

1 files changed, 229 insertions, 11 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.