new expansions

2 files changed, 935 insertions, 15 deletions

diff --git a/riscV/BTL_SEsimplify.v b/riscV/BTL_SEsimplify.v
index a4a2785a..30468544 100644
--- a/riscV/BTL_SEsimplify.v
+++ b/riscV/BTL_SEsimplify.v
@@ -38,16 +38,16 @@ Definition load_hilo32 (hi lo: int) :=
     fSop (OEluiw hi) fSnil
   else
     let fsv := fSop (OEluiw hi) fSnil in
-    let hl := make_lfsv_single fsv in
-    fSop (OEaddiw None lo) hl.
+    let lfsv := make_lfsv_single fsv in
+    fSop (OEaddiw None lo) lfsv.
 
 Definition load_hilo64 (hi lo: int64) :=
   if Int64.eq lo Int64.zero then
     fSop (OEluil hi) fSnil
   else
     let fsv := fSop (OEluil hi) fSnil in
-    let hl := make_lfsv_single fsv in
-    fSop (OEaddil None lo) hl.
+    let lfsv := make_lfsv_single fsv in
+    fSop (OEaddil None lo) lfsv.
 
 Definition loadimm32 (n: int) :=
   match make_immed32 n with
@@ -67,27 +67,27 @@ Definition loadimm64 (n: int64) :=
 Definition opimm32 (hv1: sval) (n: int) (op: operation) (opimm: int -> operation) :=
   match make_immed32 n with
   | Imm32_single imm =>
-      let hl := make_lfsv_single hv1 in
-      fSop (opimm imm) hl
+      let lfsv := make_lfsv_single hv1 in
+      fSop (opimm imm) lfsv
   | Imm32_pair hi lo =>
       let fsv := load_hilo32 hi lo in
-      let hl := make_lfsv_cmp false hv1 fsv in
-      fSop op hl
+      let lfsv := make_lfsv_cmp false hv1 fsv in
+      fSop op lfsv
   end.
 
 Definition opimm64 (hv1: sval) (n: int64) (op: operation) (opimm: int64 -> operation) :=
   match make_immed64 n with
   | Imm64_single imm =>
-      let hl := make_lfsv_single hv1 in
-      fSop (opimm imm) hl
+      let lfsv := make_lfsv_single hv1 in
+      fSop (opimm imm) lfsv
   | Imm64_pair hi lo =>
       let fsv := load_hilo64 hi lo in
-      let hl := make_lfsv_cmp false hv1 fsv in
-      fSop op hl
+      let lfsv := make_lfsv_cmp false hv1 fsv in
+      fSop op lfsv
   | Imm64_large imm =>
       let fsv := fSop (OEloadli imm) fSnil in
-      let hl := make_lfsv_cmp false hv1 fsv in
-      fSop op hl
+      let lfsv := make_lfsv_cmp false hv1 fsv in
+      fSop op lfsv
   end.
 
 Definition addimm32 (hv1: sval) (n: int) (or: option oreg) := opimm32 hv1 n Oadd (OEaddiw or).
@@ -326,6 +326,113 @@ Definition target_op_simplify (op: operation) (lr: list reg) (hrs: ristate): opt
       let is_inv := is_inv_cmp_float c in
       let lfsv := make_lfsv_cmp is_inv fsv1 fsv2 in
       Some (expanse_cond_fp true cond_single c lfsv)
+  | Ofloatconst f, nil =>
+      let fsv := loadimm64 (Float.to_bits f) in
+      let lfsv := make_lfsv_single fsv in
+      Some (fSop (Ofloat_of_bits) lfsv)
+  | Osingleconst f, nil =>
+      let fsv := loadimm32 (Float32.to_bits f) in
+      let lfsv := make_lfsv_single fsv in
+      Some (fSop (Osingle_of_bits) lfsv)
+  | Ointconst n, nil =>
+      Some (loadimm32 n)
+  | Olongconst n, nil =>
+      Some (loadimm64 n)
+  | Oaddimm n, a1 :: nil =>
+      let hv1 := ris_sreg_get hrs a1 in
+      Some (addimm32 hv1 n None)
+  | Oaddlimm n, a1 :: nil =>
+      let hv1 := ris_sreg_get hrs a1 in
+      Some (addimm64 hv1 n None)
+  | Oandimm n, a1 :: nil =>
+      let hv1 := ris_sreg_get hrs a1 in
+      Some (andimm32 hv1 n)
+  | Oandlimm n, a1 :: nil =>
+      let hv1 := ris_sreg_get hrs a1 in
+      Some (andimm64 hv1 n)
+  | Oorimm n, a1 :: nil =>
+      let hv1 := ris_sreg_get hrs a1 in
+      Some (orimm32 hv1 n)
+  | Oorlimm n, a1 :: nil =>
+      let hv1 := ris_sreg_get hrs a1 in
+      Some (orimm64 hv1 n)
+  | Oxorimm n, a1 :: nil =>
+      let hv1 := ris_sreg_get hrs a1 in
+      Some (xorimm32 hv1 n)
+  | Oxorlimm n, a1 :: nil =>
+      let hv1 := ris_sreg_get hrs a1 in
+      Some (xorimm64 hv1 n)
+  | Ocast8signed, a1 :: nil =>
+      let hv1 := ris_sreg_get hrs a1 in
+      let lfsv := make_lfsv_single hv1 in
+      let fsv := fSop (Oshlimm (Int.repr 24)) lfsv in
+      let hl' := make_lfsv_single fsv in
+      Some (fSop (Oshrimm (Int.repr 24)) hl')
+  | Ocast16signed, a1 :: nil =>
+      let hv1 := ris_sreg_get hrs a1 in
+      let lfsv := make_lfsv_single hv1 in
+      let fsv := fSop (Oshlimm (Int.repr 16)) lfsv in
+      let hl' := make_lfsv_single fsv in
+      Some (fSop (Oshrimm (Int.repr 16)) hl')
+  | Ocast32unsigned, a1 :: nil =>
+      let hv1 := ris_sreg_get hrs a1 in
+      let lfsv := make_lfsv_single hv1 in
+      let cast32s_s := fSop Ocast32signed lfsv in
+      let cast32s_l := make_lfsv_single cast32s_s in
+      let sllil_s := fSop (Oshllimm (Int.repr 32)) cast32s_l in
+      let sllil_l := make_lfsv_single sllil_s in
+      Some (fSop (Oshrluimm (Int.repr 32)) sllil_l)
+  | Oshrximm n, a1 :: nil =>
+      let hv1 := ris_sreg_get hrs a1 in
+      let lfsv := make_lfsv_single hv1 in
+      if Int.eq n Int.zero then
+        let lhl := make_lfsv_cmp false hv1 hv1 in
+        Some (fSop (OEmayundef (MUshrx n)) lhl)
+      else
+        if Int.eq n Int.one then
+          let srliw_s := fSop (Oshruimm (Int.repr 31)) lfsv in
+          let srliw_l := make_lfsv_cmp false hv1 srliw_s in
+          let addw_s := fSop Oadd srliw_l in
+          let addw_l := make_lfsv_single addw_s in
+          let sraiw_s := fSop (Oshrimm Int.one) addw_l in
+          let sraiw_l := make_lfsv_cmp false sraiw_s sraiw_s in
+          Some (fSop (OEmayundef (MUshrx n)) sraiw_l)
+        else 
+          let sraiw_s := fSop (Oshrimm (Int.repr 31)) lfsv in
+          let sraiw_l := make_lfsv_single sraiw_s in
+          let srliw_s := fSop (Oshruimm (Int.sub Int.iwordsize n)) sraiw_l in
+          let srliw_l := make_lfsv_cmp false hv1 srliw_s in
+          let addw_s := fSop Oadd srliw_l in
+          let addw_l := make_lfsv_single addw_s in
+          let sraiw_s' := fSop (Oshrimm n) addw_l in
+          let sraiw_l' := make_lfsv_cmp false sraiw_s' sraiw_s' in
+          Some (fSop (OEmayundef (MUshrx n)) sraiw_l')
+  | Oshrxlimm n, a1 :: nil =>
+      let hv1 := ris_sreg_get hrs a1 in
+      let lfsv := make_lfsv_single hv1 in
+      if Int.eq n Int.zero then
+        let lhl := make_lfsv_cmp false hv1 hv1 in
+        Some (fSop (OEmayundef (MUshrxl n)) lhl)
+      else
+        if Int.eq n Int.one then
+          let srlil_s := fSop (Oshrluimm (Int.repr 63)) lfsv in
+          let srlil_l := make_lfsv_cmp false hv1 srlil_s in
+          let addl_s := fSop Oaddl srlil_l in
+          let addl_l := make_lfsv_single addl_s in
+          let srail_s := fSop (Oshrlimm Int.one) addl_l in
+          let srail_l := make_lfsv_cmp false srail_s srail_s in
+          Some (fSop (OEmayundef (MUshrxl n)) srail_l)
+        else
+          let srail_s := fSop (Oshrlimm (Int.repr 63)) lfsv in
+          let srail_l := make_lfsv_single srail_s in
+          let srlil_s := fSop (Oshrluimm (Int.sub Int64.iwordsize' n)) srail_l in
+          let srlil_l := make_lfsv_cmp false hv1 srlil_s in
+          let addl_s := fSop Oaddl srlil_l in
+          let addl_l := make_lfsv_single addl_s in
+          let srail_s' := fSop (Oshrlimm n) addl_l in
+          let srail_l' := make_lfsv_cmp false srail_s' srail_s' in
+          Some (fSop (OEmayundef (MUshrxl n)) srail_l')
+
   | _, _ => None
   end.
 
@@ -950,6 +1057,606 @@ Proof.
   all: destruct (Float32.cmp _ _ _); trivial.
 Qed.
 
+Lemma simplify_intconst_correct (ctx: iblock_exec_context) (hrs: ristate) (st: sistate)
+  args fsv lr n: forall
+  (H : match lr with
+       | nil => Some (loadimm32 n)
+       | _ :: _ => None
+       end = Some fsv)
+  (OK1 : eval_list_sval ctx (list_sval_inj (map st lr)) = Some args),
+  eval_sval ctx fsv =
+  eval_operation (cge ctx) (csp ctx) (Ointconst n) args (cm0 ctx).
+Proof.
+  intros.
+  repeat (destruct lr; simpl; try congruence);
+  simpl in OK1; inv OK1; inv H; simpl;
+  unfold loadimm32, load_hilo32, make_lfsv_single; simpl;
+  specialize make_immed32_sound with (n);
+  destruct (make_immed32 (n)) eqn:EQMKI; intros; simpl;
+  try destruct (Int.eq lo Int.zero) eqn:EQLO; simpl;
+  try apply Int.same_if_eq in EQLO; subst;
+  try rewrite Int.add_commut, Int.add_zero_l;
+  try rewrite ltu_12_wordsize; try rewrite H; trivial.
+Qed.
+
+Lemma simplify_longconst_correct (ctx: iblock_exec_context) (hrs: ristate) (st: sistate)
+  args fsv lr n: forall
+  (H : match lr with
+       | nil => Some (loadimm64 n)
+       | _ :: _ => None
+       end = Some fsv)
+  (OK1 : eval_list_sval ctx (list_sval_inj (map st lr)) = Some args),
+  eval_sval ctx fsv =
+  eval_operation (cge ctx) (csp ctx) (Olongconst n) args (cm0 ctx).
+Proof.
+  intros.
+  repeat (destruct lr; simpl; try congruence);
+  simpl in OK1; inv OK1; inv H; simpl;
+  unfold loadimm64, load_hilo64, make_lfsv_single; simpl;
+  specialize make_immed64_sound with (n);
+  destruct (make_immed64 (n)) eqn:EQMKI; intros; simpl;
+  try destruct (Int64.eq lo Int64.zero) eqn:EQLO; simpl;
+  try apply Int64.same_if_eq in EQLO; subst;
+  try rewrite Int64.add_commut, Int64.add_zero_l;
+  try rewrite Int64.add_commut;
+  try rewrite ltu_12_wordsize; try rewrite H; trivial.
+Qed.
+
+Lemma simplify_floatconst_correct (ctx: iblock_exec_context) (hrs: ristate) (st: sistate)
+  args fsv lr n: forall
+  (H : match lr with
+       | nil =>
+           Some
+             (fSop Ofloat_of_bits
+                (make_lfsv_single (loadimm64 (Float.to_bits n))))
+       | _ :: _ => None
+       end = Some fsv)
+  (OK1 : eval_list_sval ctx (list_sval_inj (map st lr)) = Some args),
+  eval_sval ctx fsv =
+  eval_operation (cge ctx) (csp ctx) (Ofloatconst n) args (cm0 ctx).
+Proof.
+  intros.
+  repeat (destruct lr; simpl; try congruence);
+  simpl in OK1; inv OK1; inv H; simpl;
+  unfold loadimm64, load_hilo64; simpl;
+  specialize make_immed64_sound with (Float.to_bits n);
+  destruct (make_immed64 (Float.to_bits n)) eqn:EQMKI; intros;
+  try destruct (Int64.eq lo Int64.zero) eqn:EQLO;
+  simpl.
+  - try rewrite Int64.add_commut, Int64.add_zero_l; inv H;
+    try rewrite Float.of_to_bits; trivial.
+  - apply Int64.same_if_eq in EQLO; subst.
+    try rewrite Int64.add_commut, Int64.add_zero_l in H.
+    rewrite <- H; try rewrite Float.of_to_bits; trivial.
+  - rewrite <- H; try rewrite Float.of_to_bits; trivial.
+  - rewrite <- H; try rewrite Float.of_to_bits; trivial.
+Qed.
+
+Lemma simplify_singleconst_correct (ctx: iblock_exec_context) (hrs: ristate) (st: sistate)
+  args fsv lr n: forall
+  (H : match lr with
+       | nil =>
+           Some
+             (fSop Osingle_of_bits
+                (make_lfsv_single (loadimm32 (Float32.to_bits n))))
+       | _ :: _ => None
+       end = Some fsv)
+  (OK1 : eval_list_sval ctx (list_sval_inj (map st lr)) = Some args),
+  eval_sval ctx fsv =
+  eval_operation (cge ctx) (csp ctx) (Osingleconst n) args (cm0 ctx).
+Proof.
+  intros.
+  repeat (destruct lr; simpl; try congruence);
+  simpl in OK1; inv OK1; inv H; simpl;
+  unfold loadimm32, load_hilo32; simpl;
+  specialize make_immed32_sound with (Float32.to_bits n);
+  destruct (make_immed32 (Float32.to_bits n)) eqn:EQMKI; intros;
+  try destruct (Int.eq lo Int.zero) eqn:EQLO;
+  simpl.
+  { try rewrite Int.add_commut, Int.add_zero_l; inv H;
+    try rewrite Float32.of_to_bits; trivial. }
+  all:
+    try apply Int.same_if_eq in EQLO; subst;
+    try rewrite Int.add_commut, Int.add_zero_l in H; simpl;
+    rewrite ltu_12_wordsize; simpl; try rewrite <- H;
+    try rewrite Float32.of_to_bits; trivial.
+Qed.
+
+Lemma simplify_cast8signed_correct (ctx: iblock_exec_context) (hrs: ristate) (st: sistate)
+  args fsv lr: forall
+  (REG_EQ : forall r : positive, eval_sval ctx (hrs r) = eval_sval ctx (st r))
+  (H : match lr with
+       | nil => None
+       | a1 :: nil =>
+           Some
+             (fSop (Oshrimm (Int.repr 24))
+                (make_lfsv_single
+                   (fSop (Oshlimm (Int.repr 24)) (make_lfsv_single (hrs a1)))))
+       | a1 :: _ :: _ => None
+       end = Some fsv)
+  (OK1 : eval_list_sval ctx (list_sval_inj (map st lr)) = Some args),
+  eval_sval ctx fsv =
+  eval_operation (cge ctx) (csp ctx) Ocast8signed args (cm0 ctx).
+Proof.
+  intros.
+  repeat (destruct lr; simpl; try congruence);
+  simpl in OK1; inv H; simpl;
+  rewrite !REG_EQ.
+  destruct (eval_sval ctx (st p)) eqn:OKv1; try congruence; inv OK1.
+  unfold Val.shr, Val.shl, Val.sign_ext;
+  destruct v; simpl; auto.
+  assert (A: Int.ltu (Int.repr 24) Int.iwordsize = true) by auto.
+  rewrite A. rewrite Int.sign_ext_shr_shl; simpl; trivial. cbn; lia.
+Qed.
+
+Lemma simplify_cast16signed_correct (ctx: iblock_exec_context) (hrs: ristate) (st: sistate)
+  args fsv lr: forall
+  (REG_EQ : forall r : positive, eval_sval ctx (hrs r) = eval_sval ctx (st r))
+  (H : match lr with
+       | nil => None
+       | a1 :: nil =>
+           Some
+             (fSop (Oshrimm (Int.repr 16))
+                (make_lfsv_single
+                   (fSop (Oshlimm (Int.repr 16)) (make_lfsv_single (hrs a1)))))
+       | a1 :: _ :: _ => None
+       end = Some fsv)
+  (OK1 : eval_list_sval ctx (list_sval_inj (map st lr)) = Some args),
+  eval_sval ctx fsv =
+  eval_operation (cge ctx) (csp ctx) Ocast16signed args (cm0 ctx).
+Proof.
+  intros.
+  repeat (destruct lr; simpl; try congruence);
+  simpl in OK1; inv H; simpl;
+  rewrite !REG_EQ.
+  destruct (eval_sval ctx (st p)) eqn:OKv1; try congruence; inv OK1.
+  unfold Val.shr, Val.shl, Val.sign_ext;
+  destruct v; simpl; auto.
+  assert (A: Int.ltu (Int.repr 16) Int.iwordsize = true) by auto.
+  rewrite A. rewrite Int.sign_ext_shr_shl; simpl; trivial. cbn; lia.
+Qed.
+
+Lemma simplify_addimm_correct (ctx: iblock_exec_context) (hrs: ristate) (st: sistate)
+  args fsv lr n: forall
+  (REG_EQ : forall r : positive, eval_sval ctx (hrs r) = eval_sval ctx (st r))
+  (H : match lr with
+       | nil => None
+       | a1 :: nil => Some (addimm32 (hrs a1) n None)
+       | a1 :: _ :: _ => None
+       end = Some fsv)
+  (OK1 : eval_list_sval ctx (list_sval_inj (map st lr)) = Some args),
+  eval_sval ctx fsv =
+  eval_operation (cge ctx) (csp ctx) (Oaddimm n) args (cm0 ctx).
+Proof.
+  intros.
+  repeat (destruct lr; simpl; try congruence);
+  simpl in OK1; inv H; simpl.
+  unfold addimm32, opimm32, load_hilo32, make_lfsv_cmp; simpl;
+  specialize make_immed32_sound with (n);
+  destruct (make_immed32 (n)) eqn:EQMKI; intros; simpl;
+  try destruct (Int.eq lo Int.zero) eqn:EQLO; simpl;
+  rewrite !REG_EQ;
+  destruct (eval_sval ctx (st p)) eqn:OKv1; try congruence; inv OK1; trivial.
+  apply Int.same_if_eq in EQLO; subst;
+  rewrite Int.add_commut, Int.add_zero_l;
+  rewrite ltu_12_wordsize; trivial.
+Qed.
+
+Lemma simplify_andimm_correct (ctx: iblock_exec_context) (hrs: ristate) (st: sistate)
+  args fsv lr n: forall
+  (REG_EQ : forall r : positive, eval_sval ctx (hrs r) = eval_sval ctx (st r))
+  (H : match lr with
+       | nil => None
+       | a1 :: nil => Some (andimm32 (hrs a1) n)
+       | a1 :: _ :: _ => None
+       end = Some fsv)
+  (OK1 : eval_list_sval ctx (list_sval_inj (map st lr)) = Some args),
+  eval_sval ctx fsv =
+  eval_operation (cge ctx) (csp ctx) (Oandimm n) args (cm0 ctx).
+Proof.
+  intros.
+  repeat (destruct lr; simpl; try congruence);
+  simpl in OK1; inv H; simpl.
+  unfold andimm32, opimm32, load_hilo32, make_lfsv_cmp; simpl;
+  specialize make_immed32_sound with (n);
+  destruct (make_immed32 (n)) eqn:EQMKI; intros; simpl;
+  try destruct (Int.eq lo Int.zero) eqn:EQLO; simpl;
+  rewrite !REG_EQ;
+  destruct (eval_sval ctx (st p)) eqn:OKv1; try congruence; inv OK1; trivial.
+  fold (Val.and (Vint imm) v); rewrite Val.and_commut; trivial.
+  apply Int.same_if_eq in EQLO; subst;
+  rewrite Int.add_commut, Int.add_zero_l;
+  rewrite ltu_12_wordsize; trivial.
+Qed.
+
+Lemma simplify_orimm_correct (ctx: iblock_exec_context) (hrs: ristate) (st: sistate)
+  args fsv lr n: forall
+  (REG_EQ : forall r : positive, eval_sval ctx (hrs r) = eval_sval ctx (st r))
+  (H : match lr with
+       | nil => None
+       | a1 :: nil => Some (orimm32 (hrs a1) n)
+       | a1 :: _ :: _ => None
+       end = Some fsv)
+  (OK1 : eval_list_sval ctx (list_sval_inj (map st lr)) = Some args),
+  eval_sval ctx fsv =
+  eval_operation (cge ctx) (csp ctx) (Oorimm n) args (cm0 ctx).
+Proof.
+  intros.
+  repeat (destruct lr; simpl; try congruence);
+  simpl in OK1; inv H; simpl.
+  unfold orimm32, opimm32, load_hilo32, make_lfsv_cmp; simpl;
+  specialize make_immed32_sound with (n);
+  destruct (make_immed32 (n)) eqn:EQMKI; intros; simpl;
+  try destruct (Int.eq lo Int.zero) eqn:EQLO; simpl;
+  rewrite !REG_EQ;
+  destruct (eval_sval ctx (st p)) eqn:OKv1; try congruence; inv OK1; trivial.
+  fold (Val.or (Vint imm) v); rewrite Val.or_commut; trivial.
+  apply Int.same_if_eq in EQLO; subst;
+  rewrite Int.add_commut, Int.add_zero_l;
+  rewrite ltu_12_wordsize; trivial.
+Qed.
+
+Lemma simplify_xorimm_correct (ctx: iblock_exec_context) (hrs: ristate) (st: sistate)
+  args fsv lr n: forall
+  (REG_EQ : forall r : positive, eval_sval ctx (hrs r) = eval_sval ctx (st r))
+  (H : match lr with
+       | nil => None
+       | a1 :: nil => Some (xorimm32 (hrs a1) n)
+       | a1 :: _ :: _ => None
+       end = Some fsv)
+  (OK1 : eval_list_sval ctx (list_sval_inj (map st lr)) = Some args),
+  eval_sval ctx fsv =
+  eval_operation (cge ctx) (csp ctx) (Oxorimm n) args (cm0 ctx).
+Proof.
+  intros.
+  repeat (destruct lr; simpl; try congruence);
+  simpl in OK1; inv H; simpl.
+  unfold xorimm32, opimm32, load_hilo32, make_lfsv_cmp; simpl;
+  specialize make_immed32_sound with (n);
+  destruct (make_immed32 (n)) eqn:EQMKI; intros; simpl;
+  try destruct (Int.eq lo Int.zero) eqn:EQLO; simpl;
+  rewrite !REG_EQ;
+  destruct (eval_sval ctx (st p)) eqn:OKv1; try congruence; inv OK1; trivial.
+  apply Int.same_if_eq in EQLO; subst;
+  rewrite Int.add_commut, Int.add_zero_l;
+  rewrite ltu_12_wordsize; trivial.
+Qed.
+
+Lemma simplify_shrximm_correct (ctx: iblock_exec_context) (hrs: ristate) (st: sistate)
+  args fsv lr n: forall
+  (REG_EQ : forall r : positive, eval_sval ctx (hrs r) = eval_sval ctx (st r))
+  (H : match lr with
+       | nil => None
+       | a1 :: nil =>
+           if Int.eq n Int.zero
+           then
+            Some
+              (fSop (OEmayundef (MUshrx n))
+                 (make_lfsv_cmp false (hrs a1) (hrs a1)))
+           else
+            if Int.eq n Int.one
+            then
+             Some
+               (fSop (OEmayundef (MUshrx n))
+                  (make_lfsv_cmp false
+                     (fSop (Oshrimm Int.one)
+                        (make_lfsv_single
+                           (fSop Oadd
+                              (make_lfsv_cmp false (hrs a1)
+                                 (fSop (Oshruimm (Int.repr 31))
+                                    (make_lfsv_single (hrs a1)))))))
+                     (fSop (Oshrimm Int.one)
+                        (make_lfsv_single
+                           (fSop Oadd
+                              (make_lfsv_cmp false (hrs a1)
+                                 (fSop (Oshruimm (Int.repr 31))
+                                    (make_lfsv_single (hrs a1)))))))))
+            else
+             Some
+               (fSop (OEmayundef (MUshrx n))
+                  (make_lfsv_cmp false
+                     (fSop (Oshrimm n)
+                        (make_lfsv_single
+                           (fSop Oadd
+                              (make_lfsv_cmp false (hrs a1)
+                                 (fSop (Oshruimm (Int.sub Int.iwordsize n))
+                                    (make_lfsv_single
+                                       (fSop (Oshrimm (Int.repr 31))
+                                          (make_lfsv_single (hrs a1)))))))))
+                     (fSop (Oshrimm n)
+                        (make_lfsv_single
+                           (fSop Oadd
+                              (make_lfsv_cmp false (hrs a1)
+                                 (fSop (Oshruimm (Int.sub Int.iwordsize n))
+                                    (make_lfsv_single
+                                       (fSop (Oshrimm (Int.repr 31))
+                                          (make_lfsv_single (hrs a1)))))))))))
+       | a1 :: _ :: _ => None
+       end = Some fsv)
+  (OK1 : eval_list_sval ctx (list_sval_inj (map st lr)) = Some args),
+  eval_sval ctx fsv =
+  eval_operation (cge ctx) (csp ctx) (Oshrximm n) args (cm0 ctx).
+Proof.
+  intros.
+  repeat (destruct lr; simpl; try congruence).
+  assert (A: Int.ltu Int.zero (Int.repr 31) = true) by auto.
+  assert (B: Int.ltu (Int.repr 31) Int.iwordsize = true) by auto.
+  assert (C: Int.ltu Int.one Int.iwordsize = true) by auto.
+  destruct (Int.eq n Int.zero) eqn:EQ0;
+  destruct (Int.eq n Int.one) eqn:EQ1.
+  { apply Int.same_if_eq in EQ0.
+    apply Int.same_if_eq in EQ1; subst. discriminate. }
+  all:
+    simpl in OK1; inv H; simpl;
+    rewrite !REG_EQ;
+    destruct (eval_sval ctx (st p)) eqn:OKv1; try congruence; inv OK1;
+    destruct (Val.shrx v (Vint n)) eqn:TOTAL; cbn;
+    unfold eval_may_undef.
+  2,4,6:
+    unfold Val.shrx in TOTAL;
+    destruct v; simpl in TOTAL; simpl; try congruence;
+    try rewrite B; simpl; try rewrite C; simpl;
+    try destruct (Val.shr _ _);
+    destruct (Int.ltu n (Int.repr 31)); try congruence.
+  - destruct v; simpl in TOTAL; try congruence;
+    apply Int.same_if_eq in EQ0; subst;
+    rewrite A, Int.shrx_zero in TOTAL;
+    [auto | cbn; lia].
+  - apply Int.same_if_eq in EQ1; subst;
+    unfold Val.shr, Val.shru, Val.shrx, Val.add; simpl;
+    destruct v; simpl in *; try discriminate; trivial.
+    rewrite B, C.
+    rewrite Int.shrx1_shr in TOTAL; auto.
+  - exploit Val.shrx_shr_2; eauto. rewrite EQ0.
+    intros; subst.
+    destruct v; simpl in *; try discriminate; trivial.
+    rewrite B in *.
+    destruct Int.ltu eqn:EQN0 in TOTAL; try discriminate.
+    simpl in *.
+    destruct Int.ltu eqn:EQN1 in TOTAL; try discriminate.
+    replace Int.iwordsize with (Int.repr 32) in * by auto.
+    rewrite !EQN1. simpl in *.
+    destruct Int.ltu eqn:EQN2 in TOTAL; try discriminate.
+    rewrite !EQN2. rewrite EQN0.
+    reflexivity.
+Qed.
+
+Lemma simplify_cast32unsigned_correct (ctx: iblock_exec_context) (hrs: ristate) (st: sistate)
+  args fsv lr: forall
+  (REG_EQ : forall r : positive, eval_sval ctx (hrs r) = eval_sval ctx (st r))
+  (H : match lr with
+       | nil => None
+       | a1 :: nil =>
+           Some
+             (fSop (Oshrluimm (Int.repr 32))
+                (make_lfsv_single
+                   (fSop (Oshllimm (Int.repr 32))
+                      (make_lfsv_single
+                         (fSop Ocast32signed (make_lfsv_single (hrs a1)))))))
+       | a1 :: _ :: _ => None
+       end = Some fsv)
+  (OK1 : eval_list_sval ctx (list_sval_inj (map st lr)) = Some args),
+  eval_sval ctx fsv =
+  eval_operation (cge ctx) (csp ctx) Ocast32unsigned args (cm0 ctx).
+Proof.
+  intros.
+  repeat (destruct lr; simpl; try congruence);
+  simpl in OK1; inv H; simpl.
+  rewrite !REG_EQ;
+  destruct (eval_sval ctx (st p)) eqn:OKv1; try congruence; inv OK1.
+  unfold Val.shrlu, Val.shll, Val.longofint, Val.longofintu.
+  destruct v; simpl; auto.
+  assert (A: Int.ltu (Int.repr 32) Int64.iwordsize' = true) by auto.
+  rewrite A. rewrite Int64.shru'_shl'; auto.
+  replace (Int.ltu (Int.repr 32) (Int.repr 32)) with (false) by auto.
+  rewrite cast32unsigned_from_cast32signed.
+  replace Int64.zwordsize with 64 by auto.
+  rewrite Int.unsigned_repr; cbn; try lia.
+  replace (Int.sub (Int.repr 32) (Int.repr 32)) with (Int.zero) by auto.
+  rewrite Int64.shru'_zero. reflexivity.
+Qed.
+
+Lemma simplify_addlimm_correct (ctx: iblock_exec_context) (hrs: ristate) (st: sistate)
+  args fsv lr n: forall
+  (REG_EQ : forall r : positive, eval_sval ctx (hrs r) = eval_sval ctx (st r))
+  (H : match lr with
+       | nil => None
+       | a1 :: nil => Some (addimm64 (hrs a1) n None)
+       | a1 :: _ :: _ => None
+       end = Some fsv)
+  (OK1 : eval_list_sval ctx (list_sval_inj (map st lr)) = Some args),
+  eval_sval ctx fsv =
+  eval_operation (cge ctx) (csp ctx) (Oaddlimm n) args (cm0 ctx).
+Proof.
+  intros.
+  repeat (destruct lr; simpl; try congruence);
+  simpl in OK1; inv H; simpl;
+  unfold addimm64, opimm64, load_hilo64, make_lfsv_cmp; simpl;
+  specialize make_immed64_sound with (n);
+  destruct (make_immed64 (n)) eqn:EQMKI; intros; simpl;
+  try destruct (Int64.eq lo Int64.zero) eqn:EQLO; simpl;
+  rewrite !REG_EQ;
+  destruct (eval_sval ctx (st p)) eqn:OKv1; try congruence; inv OK1; trivial.
+  apply Int64.same_if_eq in EQLO; subst.
+  rewrite Int64.add_commut, Int64.add_zero_l; trivial.
+Qed.
+
+Lemma simplify_andlimm_correct (ctx: iblock_exec_context) (hrs: ristate) (st: sistate)
+  args fsv lr n: forall
+  (REG_EQ : forall r : positive, eval_sval ctx (hrs r) = eval_sval ctx (st r))
+  (H : match lr with
+       | nil => None
+       | a1 :: nil => Some (andimm64 (hrs a1) n)
+       | a1 :: _ :: _ => None
+       end = Some fsv)
+  (OK1 : eval_list_sval ctx (list_sval_inj (map st lr)) = Some args),
+  eval_sval ctx fsv =
+  eval_operation (cge ctx) (csp ctx) (Oandlimm n) args (cm0 ctx).
+Proof.
+  intros.
+  repeat (destruct lr; simpl; try congruence);
+  simpl in OK1; inv H; simpl;
+  unfold andimm64, opimm64, load_hilo64, make_lfsv_cmp; simpl;
+  specialize make_immed64_sound with (n);
+  destruct (make_immed64 (n)) eqn:EQMKI; intros; simpl;
+  try destruct (Int64.eq lo Int64.zero) eqn:EQLO; simpl;
+  rewrite !REG_EQ;
+  destruct (eval_sval ctx (st p)) eqn:OKv1; try congruence; inv OK1; trivial.
+  fold (Val.andl (Vlong imm) v); rewrite Val.andl_commut; trivial.
+  apply Int64.same_if_eq in EQLO; subst;
+  rewrite Int64.add_commut, Int64.add_zero_l; trivial.
+Qed.
+
+Lemma simplify_orlimm_correct (ctx: iblock_exec_context) (hrs: ristate) (st: sistate)
+  args fsv lr n: forall
+  (REG_EQ : forall r : positive, eval_sval ctx (hrs r) = eval_sval ctx (st r))
+  (H : match lr with
+       | nil => None
+       | a1 :: nil => Some (orimm64 (hrs a1) n)
+       | a1 :: _ :: _ => None
+       end = Some fsv)
+  (OK1 : eval_list_sval ctx (list_sval_inj (map st lr)) = Some args),
+  eval_sval ctx fsv =
+  eval_operation (cge ctx) (csp ctx) (Oorlimm n) args (cm0 ctx).
+Proof.
+  intros.
+  repeat (destruct lr; simpl; try congruence);
+  simpl in OK1; inv H; simpl;
+  unfold orimm64, opimm64, load_hilo64, make_lfsv_cmp; simpl;
+  specialize make_immed64_sound with (n);
+  destruct (make_immed64 (n)) eqn:EQMKI; intros; simpl;
+  try destruct (Int64.eq lo Int64.zero) eqn:EQLO; simpl;
+  rewrite !REG_EQ;
+  destruct (eval_sval ctx (st p)) eqn:OKv1; try congruence; inv OK1; trivial.
+  fold (Val.orl (Vlong imm) v); rewrite Val.orl_commut; trivial.
+  apply Int64.same_if_eq in EQLO; subst;
+  rewrite Int64.add_commut, Int64.add_zero_l; trivial.
+Qed.
+
+Lemma simplify_xorlimm_correct (ctx: iblock_exec_context) (hrs: ristate) (st: sistate)
+  args fsv lr n: forall
+  (REG_EQ : forall r : positive, eval_sval ctx (hrs r) = eval_sval ctx (st r))
+  (H : match lr with
+       | nil => None
+       | a1 :: nil => Some (xorimm64 (hrs a1) n)
+       | a1 :: _ :: _ => None
+       end = Some fsv)
+  (OK1 : eval_list_sval ctx (list_sval_inj (map st lr)) = Some args),
+  eval_sval ctx fsv =
+  eval_operation (cge ctx) (csp ctx) (Oxorlimm n) args (cm0 ctx).
+Proof.
+  intros.
+  repeat (destruct lr; simpl; try congruence);
+  simpl in OK1; inv H; simpl;
+  unfold xorimm64, opimm64, load_hilo64, make_lfsv_cmp; simpl;
+  specialize make_immed64_sound with (n);
+  destruct (make_immed64 (n)) eqn:EQMKI; intros; simpl;
+  try destruct (Int64.eq lo Int64.zero) eqn:EQLO; simpl;
+  rewrite !REG_EQ;
+  destruct (eval_sval ctx (st p)) eqn:OKv1; try congruence; inv OK1; trivial.
+  apply Int64.same_if_eq in EQLO; subst;
+  rewrite Int64.add_commut, Int64.add_zero_l; trivial.
+Qed.
+
+Lemma simplify_shrxlimm_correct (ctx: iblock_exec_context) (hrs: ristate) (st: sistate)
+  args fsv lr n: forall
+  (REG_EQ : forall r : positive, eval_sval ctx (hrs r) = eval_sval ctx (st r))
+  (H : match lr with
+       | nil => None
+       | a1 :: nil =>
+           if Int.eq n Int.zero
+           then
+            Some
+              (fSop (OEmayundef (MUshrxl n))
+                 (make_lfsv_cmp false (hrs a1) (hrs a1)))
+           else
+            if Int.eq n Int.one
+            then
+             Some
+               (fSop (OEmayundef (MUshrxl n))
+                  (make_lfsv_cmp false
+                     (fSop (Oshrlimm Int.one)
+                        (make_lfsv_single
+                           (fSop Oaddl
+                              (make_lfsv_cmp false (hrs a1)
+                                 (fSop (Oshrluimm (Int.repr 63))
+                                    (make_lfsv_single (hrs a1)))))))
+                     (fSop (Oshrlimm Int.one)
+                        (make_lfsv_single
+                           (fSop Oaddl
+                              (make_lfsv_cmp false (hrs a1)
+                                 (fSop (Oshrluimm (Int.repr 63))
+                                    (make_lfsv_single (hrs a1)))))))))
+            else
+             Some
+               (fSop (OEmayundef (MUshrxl n))
+                  (make_lfsv_cmp false
+                     (fSop (Oshrlimm n)
+                        (make_lfsv_single
+                           (fSop Oaddl
+                              (make_lfsv_cmp false (hrs a1)
+                                 (fSop (Oshrluimm (Int.sub Int64.iwordsize' n))
+                                    (make_lfsv_single
+                                       (fSop (Oshrlimm (Int.repr 63))
+                                          (make_lfsv_single (hrs a1)))))))))
+                     (fSop (Oshrlimm n)
+                        (make_lfsv_single
+                           (fSop Oaddl
+                              (make_lfsv_cmp false (hrs a1)
+                                 (fSop (Oshrluimm (Int.sub Int64.iwordsize' n))
+                                    (make_lfsv_single
+                                       (fSop (Oshrlimm (Int.repr 63))
+                                          (make_lfsv_single (hrs a1)))))))))))
+       | a1 :: _ :: _ => None
+       end = Some fsv)
+  (OK1 : eval_list_sval ctx (list_sval_inj (map st lr)) = Some args),
+  eval_sval ctx fsv =
+  eval_operation (cge ctx) (csp ctx) (Oshrxlimm n) args (cm0 ctx).
+Proof.
+  intros.
+  repeat (destruct lr; simpl; try congruence).
+  assert (A: Int.ltu Int.zero (Int.repr 63) = true) by auto.
+  assert (B: Int.ltu (Int.repr 63) Int64.iwordsize' = true) by auto.
+  assert (C: Int.ltu Int.one Int64.iwordsize' = true) by auto.
+  destruct (Int.eq n Int.zero) eqn:EQ0;
+  destruct (Int.eq n Int.one) eqn:EQ1.
+  { apply Int.same_if_eq in EQ0.
+    apply Int.same_if_eq in EQ1; subst. discriminate. }
+  all:
+    simpl in OK1; inv H; simpl;
+    rewrite !REG_EQ;
+    destruct (eval_sval ctx (st p)) eqn:OKv1; try congruence; inv OK1;
+    destruct (Val.shrxl v (Vint n)) eqn:TOTAL; cbn;
+    unfold eval_may_undef.
+  2,4,6:
+    unfold Val.shrxl in TOTAL;
+    destruct v; simpl in TOTAL; simpl; try congruence;
+    try rewrite B; simpl; try rewrite C; simpl;
+    try destruct (Val.shrl _ _);
+    destruct (Int.ltu n (Int.repr 63)); try congruence.
+  - destruct v; simpl in TOTAL; try congruence;
+    apply Int.same_if_eq in EQ0; subst;
+    rewrite A, Int64.shrx'_zero in *.
+    assumption.
+  - apply Int.same_if_eq in EQ1; subst;
+    unfold Val.shrl, Val.shrlu, Val.shrxl, Val.addl; simpl;
+    destruct v; simpl in *; try discriminate; trivial.
+    rewrite B, C.
+    rewrite Int64.shrx'1_shr' in TOTAL; auto.
+  - exploit Val.shrxl_shrl_2; eauto. rewrite EQ0.
+    intros; subst.
+    destruct v; simpl in *; try discriminate; trivial.
+    rewrite B in *.
+    destruct Int.ltu eqn:EQN0 in TOTAL; try discriminate.
+    simpl in *.
+    destruct Int.ltu eqn:EQN1 in TOTAL; try discriminate.
+    replace Int64.iwordsize' with (Int.repr 64) in * by auto.
+    rewrite !EQN1. simpl in *.
+    destruct Int.ltu eqn:EQN2 in TOTAL; try discriminate.
+    rewrite !EQN2. rewrite EQN0.
+    reflexivity.
+Qed.
+
 (* Main proof of simplification *)
 
 Lemma target_op_simplify_correct ctx op lr hrs fsv st args: forall
@@ -962,6 +1669,23 @@ Proof.
   unfold target_op_simplify; simpl.
   intros H ? ? ?; inv REF.
   destruct op; try congruence.
+  eapply simplify_intconst_correct; eauto.
+  eapply simplify_longconst_correct; eauto.
+  eapply simplify_floatconst_correct; eauto. 
+  eapply simplify_singleconst_correct; eauto. 
+  eapply simplify_cast8signed_correct; eauto.
+  eapply simplify_cast16signed_correct; eauto.
+  eapply simplify_addimm_correct; eauto.
+  eapply simplify_andimm_correct; eauto.
+  eapply simplify_orimm_correct; eauto.
+  eapply simplify_xorimm_correct; eauto.
+  eapply simplify_shrximm_correct; eauto.
+  eapply simplify_cast32unsigned_correct; eauto.
+  eapply simplify_addlimm_correct; eauto.
+  eapply simplify_andlimm_correct; eauto.
+  eapply simplify_orlimm_correct; eauto.
+  eapply simplify_xorlimm_correct; eauto.
+  eapply simplify_shrxlimm_correct; eauto.
   (* Ocmp expansions *)
   destruct cond; repeat (destruct lr; simpl; try congruence);
   simpl in OK1;
diff --git a/riscV/ExpansionOracle.ml b/riscV/ExpansionOracle.ml
index c1cf5c9c..2a21b7a4 100644
--- a/riscV/ExpansionOracle.ml
+++ b/riscV/ExpansionOracle.ml
@@ -514,7 +514,6 @@ 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
 
-
 (** Return olds args if the CSE numbering is empty *)
 
 let get_arguments vn vals args =
@@ -607,6 +606,203 @@ let expanse_list li =
              exp := extract_final vn !exp dest;
              was_exp := true
          | _ -> ());
+        (if !Clflags.option_fexpanse_others && not !was_exp then
+         match i with
+         | Bop (Ofloatconst f, nil, dest, iinfo) -> (
+             match make_immed64 (Floats.Float.to_bits f) with
+             | Imm64_single _ | Imm64_large _ -> ()
+             | Imm64_pair (hi, lo) ->
+                 debug "Bop/Ofloatconst\n";
+                 let r = r2pi () in
+                 let l = load_hilo64 vn r hi lo in
+                 let r', l' = extract_arg l in
+                 exp := addinst vn Ofloat_of_bits [ r' ] dest :: l';
+                 exp := extract_final vn !exp dest;
+                 was_exp := true)
+         | Bop (Osingleconst f, nil, dest, iinfo) -> (
+             match make_immed32 (Floats.Float32.to_bits f) with
+             | Imm32_single imm -> ()
+             | Imm32_pair (hi, lo) ->
+                 debug "Bop/Osingleconst\n";
+                 let r = r2pi () in
+                 let l = load_hilo32 vn r hi lo in
+                 let r', l' = extract_arg l in
+                 exp := addinst vn Osingle_of_bits [ r' ] dest :: l';
+                 exp := extract_final vn !exp dest;
+                 was_exp := true)
+         | Bop (Ointconst n, nil, dest, iinfo) ->
+             debug "Bop/Ointconst\n";
+             exp := loadimm32 vn dest n;
+             exp := extract_final vn !exp dest;
+             was_exp := true
+         | Bop (Olongconst n, nil, dest, iinfo) ->
+             debug "Bop/Olongconst\n";
+             exp := loadimm64 vn dest n;
+             exp := extract_final vn !exp dest;
+             was_exp := true
+         | Bop (Oaddimm n, a1 :: nil, dest, iinfo) ->
+             debug "Bop/Oaddimm\n";
+             exp := addimm32 vn a1 dest n None;
+             exp := extract_final vn !exp dest;
+             was_exp := true
+         | Bop (Oaddlimm n, a1 :: nil, dest, iinfo) ->
+             debug "Bop/Oaddlimm\n";
+             exp := addimm64 vn a1 dest n None;
+             exp := extract_final vn !exp dest;
+             was_exp := true
+         | Bop (Oandimm n, a1 :: nil, dest, iinfo) ->
+             debug "Bop/Oandimm\n";
+             exp := andimm32 vn a1 dest n;
+             exp := extract_final vn !exp dest;
+             was_exp := true
+         | Bop (Oandlimm n, a1 :: nil, dest, iinfo) ->
+             debug "Bop/Oandlimm\n";
+             exp := andimm64 vn a1 dest n;
+             exp := extract_final vn !exp dest;
+             was_exp := true
+         | Bop (Oorimm n, a1 :: nil, dest, iinfo) ->
+             debug "Bop/Oorimm\n";
+             exp := orimm32 vn a1 dest n;
+             exp := extract_final vn !exp dest;
+             was_exp := true
+         | Bop (Oorlimm n, a1 :: nil, dest, iinfo) ->
+             debug "Bop/Oorlimm\n";
+             exp := orimm64 vn a1 dest n;
+             exp := extract_final vn !exp dest;
+             was_exp := true
+         | Bop (Oxorimm n, a1 :: nil, dest, iinfo) ->
+             debug "Bop/Oxorimm\n";
+             exp := xorimm32 vn a1 dest n;
+             exp := extract_final vn !exp dest;
+             was_exp := true
+         | Bop (Oxorlimm n, a1 :: nil, dest, iinfo) ->
+             debug "Bop/Oxorlimm\n";
+             exp := xorimm64 vn a1 dest n;
+             exp := extract_final vn !exp dest;
+             was_exp := true
+         | Bop (Ocast8signed, a1 :: nil, dest, iinfo) ->
+             debug "Bop/cast8signed\n";
+             let op = Oshlimm (Int.repr (Z.of_sint 24)) in
+             let r = r2pi () in
+             let i1 = addinst vn op [ a1 ] r in
+             let r', l = extract_arg [ i1 ] in
+             exp :=
+               addinst vn (Oshrimm (Int.repr (Z.of_sint 24))) [ r' ] dest :: l;
+             exp := extract_final vn !exp dest;
+             was_exp := true
+         | Bop (Ocast16signed, a1 :: nil, dest, iinfo) ->
+             debug "Bop/cast16signed\n";
+             let op = Oshlimm (Int.repr (Z.of_sint 16)) in
+             let r = r2pi () in
+             let i1 = addinst vn op [ a1 ] r in
+             let r', l = extract_arg [ i1 ] in
+             exp :=
+               addinst vn (Oshrimm (Int.repr (Z.of_sint 16))) [ r' ] dest :: l;
+             exp := extract_final vn !exp dest;
+             was_exp := true
+         | Bop (Ocast32unsigned, a1 :: nil, dest, iinfo) ->
+             debug "Bop/Ocast32unsigned\n";
+             let r1 = r2pi () in
+             let r2 = r2pi () in
+             let op1 = Ocast32signed in
+             let i1 = addinst vn op1 [ a1 ] r1 in
+             let r1', l1 = extract_arg [ i1 ] in
+
+             let op2 = Oshllimm (Int.repr (Z.of_sint 32)) in
+             let i2 = addinst vn op2 [ r1' ] r2 in
+             let r2', l2 = extract_arg (i2 :: l1) in
+
+             let op3 = Oshrluimm (Int.repr (Z.of_sint 32)) in
+             exp := addinst vn op3 [ r2' ] dest :: l2;
+             exp := extract_final vn !exp dest;
+             was_exp := true
+         | Bop (Oshrximm n, a1 :: nil, dest, iinfo) ->
+             if Int.eq n Int.zero then (
+               debug "Bop/Oshrximm1\n";
+               exp := [ addinst vn (OEmayundef (MUshrx n)) [ a1; a1 ] dest ])
+             else if Int.eq n Int.one then (
+               debug "Bop/Oshrximm2\n";
+               let r1 = r2pi () in
+               let r2 = r2pi () in
+               let op1 = Oshruimm (Int.repr (Z.of_sint 31)) in
+               let i1 = addinst vn op1 [ a1 ] r1 in
+               let r1', l1 = extract_arg [ i1 ] in
+
+               let op2 = Oadd in
+               let i2 = addinst vn op2 [ a1; r1' ] r2 in
+               let r2', l2 = extract_arg (i2 :: l1) in
+
+               let op3 = Oshrimm Int.one in
+               let i3 = addinst vn op3 [ r2' ] dest in
+               let r3, l3 = extract_arg (i3 :: l2) in
+               exp := addinst vn (OEmayundef (MUshrx n)) [ r3; r3 ] dest :: l3)
+             else (
+               debug "Bop/Oshrximm3\n";
+               let r1 = r2pi () in
+               let r2 = r2pi () in
+               let r3 = r2pi () in
+               let op1 = Oshrimm (Int.repr (Z.of_sint 31)) in
+               let i1 = addinst vn op1 [ a1 ] r1 in
+               let r1', l1 = extract_arg [ i1 ] in
+
+               let op2 = Oshruimm (Int.sub Int.iwordsize n) in
+               let i2 = addinst vn op2 [ r1' ] r2 in
+               let r2', l2 = extract_arg (i2 :: l1) in
+
+               let op3 = Oadd in
+               let i3 = addinst vn op3 [ a1; r2' ] r3 in
+               let r3', l3 = extract_arg (i3 :: l2) in
+
+               let op4 = Oshrimm n in
+               let i4 = addinst vn op4 [ r3' ] dest in
+               let r4, l4 = extract_arg (i4 :: l3) in
+               exp := addinst vn (OEmayundef (MUshrx n)) [ r4; r4 ] dest :: l4);
+             exp := extract_final vn !exp dest;
+             was_exp := true
+         | Bop (Oshrxlimm n, a1 :: nil, dest, iinfo) ->
+             if Int.eq n Int.zero then (
+               debug "Bop/Oshrxlimm1\n";
+               exp := [ addinst vn (OEmayundef (MUshrxl n)) [ a1; a1 ] dest ])
+             else if Int.eq n Int.one then (
+               debug "Bop/Oshrxlimm2\n";
+               let r1 = r2pi () in
+               let r2 = r2pi () in
+               let op1 = Oshrluimm (Int.repr (Z.of_sint 63)) in
+               let i1 = addinst vn op1 [ a1 ] r1 in
+               let r1', l1 = extract_arg [ i1 ] in
+
+               let op2 = Oaddl in
+               let i2 = addinst vn op2 [ a1; r1' ] r2 in
+               let r2', l2 = extract_arg (i2 :: l1) in
+
+               let op3 = Oshrlimm Int.one in
+               let i3 = addinst vn op3 [ r2' ] dest in
+               let r3, l3 = extract_arg (i3 :: l2) in
+               exp := addinst vn (OEmayundef (MUshrxl n)) [ r3; r3 ] dest :: l3)
+             else (
+               debug "Bop/Oshrxlimm3\n";
+               let r1 = r2pi () in
+               let r2 = r2pi () in
+               let r3 = r2pi () in
+               let op1 = Oshrlimm (Int.repr (Z.of_sint 63)) in
+               let i1 = addinst vn op1 [ a1 ] r1 in
+               let r1', l1 = extract_arg [ i1 ] in
+
+               let op2 = Oshrluimm (Int.sub Int64.iwordsize' n) in
+               let i2 = addinst vn op2 [ r1' ] r2 in
+               let r2', l2 = extract_arg (i2 :: l1) in
+
+               let op3 = Oaddl in
+               let i3 = addinst vn op3 [ a1; r2' ] r3 in
+               let r3', l3 = extract_arg (i3 :: l2) in
+
+               let op4 = Oshrlimm n in
+               let i4 = addinst vn op4 [ r3' ] dest in
+               let r4, l4 = extract_arg (i4 :: l3) in
+               exp := addinst vn (OEmayundef (MUshrxl n)) [ r4; r4 ] dest :: l4);
+             exp := extract_final vn !exp dest;
+             was_exp := true
+         | _ -> ());
         if not !was_exp then (
           (match i with
           | Bop (op, args, dest, iinfo) ->