Refactoring the mayundef OP to be more general...

5 files changed, 191 insertions, 201 deletions

diff --git a/riscV/NeedOp.v b/riscV/NeedOp.v
index 4ed9868c..cfadea37 100644
--- a/riscV/NeedOp.v
+++ b/riscV/NeedOp.v
@@ -117,8 +117,6 @@ Definition needs_of_operation (op: operation) (nv: nval): list nval :=
   | OEoril _ => op1 (default nv)
   | OEloadli _ => op1 (default nv)
   | OEmayundef _ => op2 (default nv)
-  | OEshrxundef _ => op2 (default nv)
-  | OEshrxlundef _ => op2 (default nv)
   | OEfeqd => op2 (default nv)
   | OEfltd => op2 (default nv)
   | OEfled => op2 (default nv)
diff --git a/riscV/Op.v b/riscV/Op.v
index 0569676a..b8835c61 100644
--- a/riscV/Op.v
+++ b/riscV/Op.v
@@ -69,6 +69,13 @@ Inductive condition : Type :=
   | CEbgel (optR0: option bool)                      (**r branch-if-greater-or-equal signed *)
   | CEbgeul (optR0: option bool).                    (**r branch-if-greater-or-equal unsigned *)
 
+(* This type will define the eval function of a OEmayundef operation. *)
+Inductive mayundef: Type :=
+  | MUint: mayundef
+  | MUlong: mayundef
+  | MUshrx: int -> mayundef
+  | MUshrxl: int -> mayundef.
+
 (** Arithmetic and logical operations.  In the descriptions, [rd] is the
   result of the operation and [r1], [r2], etc, are the arguments. *)
 
@@ -201,9 +208,7 @@ Inductive operation : Type :=
   | OExoril (n: int64)                           (**r xor immediate *)
   | OEluil (n: int64)                            (**r load upper-immediate *)
   | OEloadli (n: int64)                          (**r load an immediate int64 *)
-  | OEmayundef (is_long: bool)
-  | OEshrxundef (n: int)
-  | OEshrxlundef (n: int)
+  | OEmayundef (mu: mayundef)
   | OEfeqd                                       (**r compare equal *)
   | OEfltd                                       (**r compare less-than *)
   | OEfled                                       (**r compare less-than/equal *)
@@ -242,9 +247,9 @@ Defined.
 
 Definition eq_operation: forall (x y: operation), {x=y} + {x<>y}.
 Proof.
-  generalize Int.eq_dec Int64.eq_dec Ptrofs.eq_dec Float.eq_dec Float32.eq_dec ident_eq eq_condition bool_dec; intros.
+  generalize Int.eq_dec Int64.eq_dec Ptrofs.eq_dec Float.eq_dec Float32.eq_dec ident_eq eq_condition bool_dec Val.eq; intros.
   decide equality.
-  all: destruct optR0, optR1; decide equality.
+  all: try destruct optR0, optR1; try decide equality.
 Defined.
 
 (* Alternate definition: 
@@ -271,42 +276,28 @@ Definition apply_bin_r0 {B} (optR0: option bool) (sem: val -> val -> B) (v1 v2 v
   | Some false => sem v1 vz
   end.
 
-Definition may_undef_int (is_long: bool) (v1 v2: val): val :=
-  if negb is_long then
-    match v1 with
-    | Vint _ => v2
-    | _ => Vundef
-    end
-  else
-    match v1 with
-    | Vlong _ => v2
-    | _ => Vundef
-    end.
-
-Definition shrx_imm_undef (v1 v2: val): val :=
-  match v1 with
-  | Vint n1 =>
-      match v2 with
-      | Vint n2 =>
-          if Int.ltu n2 (Int.repr 31)
-          then Vint n1
-          else Vundef
+Definition eval_may_undef (mu: mayundef) (v1 v2: val): val :=
+  match mu with
+  | MUint => match v1 with
+             | Vint _ => v2
+             | _ => Vundef
+             end
+  | MUlong => match v1 with
+              | Vlong _ => v2
+              | _ => Vundef
+              end
+  | MUshrx i =>
+      match v1 with
+      | Vint _ =>
+          if Int.ltu i (Int.repr 31) then v1 else Vundef
       | _ => Vundef
       end
-  | _ => Vundef
-  end.
-
-Definition shrxl_imm_undef (v1 v2: val): val :=
-  match v1 with
-  | Vlong n1 =>
-      match v2 with
-      | Vint n2 =>
-          if Int.ltu n2 (Int.repr 63)
-          then Vlong n1
-          else Vundef
+  | MUshrxl i =>
+      match v1 with
+      | Vlong _ =>
+          if Int.ltu i (Int.repr 63) then v1 else Vundef
       | _ => Vundef
       end
-  | _ => Vundef
   end.
 
 (** * Evaluation functions *)
@@ -481,9 +472,7 @@ Definition eval_operation
   | OEandil n, v1::nil => Some (Val.andl (Vlong n) v1)
   | OEoril n, v1::nil => Some (Val.orl (Vlong n) v1)
   | OEloadli n, nil => Some (Vlong n)
-  | OEmayundef is_long, v1::v2::nil => Some (may_undef_int is_long v1 v2)
-  | OEshrxundef n, v1::nil => Some (shrx_imm_undef v1 (Vint n))
-  | OEshrxlundef n, v1::nil => Some (shrxl_imm_undef v1 (Vint n))
+  | OEmayundef mu, v1 :: v2 :: nil => Some (eval_may_undef mu v1 v2)
   | OEfeqd, v1::v2::nil => Some (Val.cmpf Ceq v1 v2)
   | OEfltd, v1::v2::nil => Some (Val.cmpf Clt v1 v2)
   | OEfled, v1::v2::nil => Some (Val.cmpf Cle v1 v2)
@@ -693,8 +682,6 @@ Definition type_of_operation (op: operation) : list typ * typ :=
   | OEaddilr0 _ => (nil, Tlong)
   | OEloadli _ => (nil, Tlong)
   | OEmayundef _ => (Tany64 :: Tany64 :: nil, Tany64)
-  | OEshrxundef _ => (Tint :: nil, Tint)
-  | OEshrxlundef _ => (Tlong :: nil, Tlong)
   | OEfeqd => (Tfloat :: Tfloat :: nil, Tint)
   | OEfltd => (Tfloat :: Tfloat :: nil, Tint)
   | OEfled => (Tfloat :: Tfloat :: nil, Tint)
@@ -736,6 +723,14 @@ Proof.
   intros. unfold Val.has_type, Val.addl. destruct Archi.ptr64, v1, v2; auto.
 Qed.
 
+Remark type_mayundef:
+  forall mu v1 v2, Val.has_type (eval_may_undef mu v1 v2) Tany64.
+Proof.
+  intros. unfold eval_may_undef.
+  destruct mu eqn:EQMU, v1, v2; simpl; auto.
+  all: destruct Int.ltu; simpl; auto.
+Qed.
+
 Lemma type_of_operation_sound:
   forall op vl sp v m,
   op <> Omove ->
@@ -946,8 +941,7 @@ Proof with (try exact I; try reflexivity; auto using Val.Vptr_has_type).
   (* OExoriw *)
   - destruct v0...
   (* OEluiw *)
-  - unfold may_undef_int;
-    destruct (Int.ltu _ _); cbn; trivial.
+  - destruct (Int.ltu _ _); cbn; trivial.
   (* OEseql *)
   - destruct optR0 as [[]|]; simpl; unfold Val.cmpl;
     destruct Val.cmpl_bool... all: destruct b...
@@ -986,16 +980,7 @@ Proof with (try exact I; try reflexivity; auto using Val.Vptr_has_type).
   (* OEloadli *)
   - trivial.
   (* OEmayundef *)
-  - unfold may_undef_int;
-    destruct is_long, v0, v1; simpl; trivial.
-  (* OEshrxundef *)
-  - unfold shrx_imm_undef;
-    destruct v0; simpl; trivial.
-    destruct (Int.ltu _ _); simpl; trivial.
-  (* OEshrxlundef *)
-  - unfold shrxl_imm_undef;
-    destruct v0; simpl; trivial.
-    destruct (Int.ltu _ _); simpl; trivial.
+  - apply type_mayundef.
   (* OEfeqd *)
   - destruct v0; destruct v1; cbn; auto.
     destruct Float.cmp; cbn; auto.
@@ -1721,7 +1706,7 @@ Proof.
   (* shru, shruimm *)
   - inv H4; inv H2; simpl; auto. destruct (Int.ltu i0 Int64.iwordsize'); auto.
   - inv H4; simpl; auto. destruct (Int.ltu n Int64.iwordsize'); auto.
-    (* shrx *)
+  (* shrx *)
   - inv H4; cbn; try apply Val.val_inject_undef.
     destruct (Int.ltu n (Int.repr 63)); cbn.
     apply Val.inject_long.
@@ -1851,17 +1836,9 @@ Proof.
   (* OExoril *)
   - inv H4; simpl; auto.
   (* OEmayundef *)
-  - destruct is_long; inv H4; inv H2;
-    unfold may_undef_int; simpl; auto;
-    eapply Val.inject_ptr; eauto.
-  (* OEshrxundef *)
-  - inv H4;
-    unfold shrx_imm_undef; simpl; auto.
-    destruct (Int.ltu _ _); auto.
-  (* OEshrxlundef *)
-  - inv H4;
-    unfold shrxl_imm_undef; simpl; auto.
-    destruct (Int.ltu _ _); auto.
+  - destruct mu; inv H4; inv H2; simpl; auto;
+    try destruct (Int.ltu _ _); simpl; auto.
+    all: eapply Val.inject_ptr; eauto.
   (* OEfeqd *)
   - inv H4; inv H2; cbn; simpl; auto.
     destruct Float.cmp; unfold Vtrue, Vfalse; cbn; auto.
diff --git a/riscV/PrintOp.ml b/riscV/PrintOp.ml
index 4494080e..3a775c20 100644
--- a/riscV/PrintOp.ml
+++ b/riscV/PrintOp.ml
@@ -30,6 +30,12 @@ let comparison_name = function
   | Cgt -> ">"
   | Cge -> ">="
 
+let mu_name pp = function
+  | MUint -> fprintf pp "MUint"
+  | MUlong -> fprintf pp "MUlong"
+  | MUshrx i -> fprintf pp "MUshrx(%ld)" (camlint_of_coqint i)
+  | MUshrxl i -> fprintf pp "MUshrxl(%ld)" (camlint_of_coqint i)
+
 let get_optR0_s c reg pp r1 r2 = function
   | None -> fprintf pp "(%a %s %a)" reg r1 (comparison_name c) reg r2
   | Some true -> fprintf pp "(X0 %s %a)" (comparison_name c) reg r1
@@ -226,9 +232,7 @@ let print_operation reg pp = function
   | OEandil n, [r1] -> fprintf pp "OEandil(%a,%ld)" reg r1 (camlint_of_coqint n)
   | OEoril n, [r1] -> fprintf pp "OEoril(%a,%ld)" reg r1 (camlint_of_coqint n)
   | OEloadli n, _ -> fprintf pp "OEloadli(%ld)" (camlint_of_coqint n)
-  | OEmayundef isl, [r1;r2] -> fprintf pp "OEmayundef (%b,%a,%a)" isl reg r1 reg r2
-  | OEshrxundef n, [r1] -> fprintf pp "OEshrxundef (%ld,%a)" (camlint_of_coqint n) reg r1
-  | OEshrxlundef n, [r1] -> fprintf pp "OEshrxlundef (%ld,%a)" (camlint_of_coqint n) reg r1
+  | OEmayundef mu, [r1;r2] -> fprintf pp "OEmayundef (%a,%a,%a)" mu_name mu reg r1 reg r2
   | OEfeqd, [r1;r2] -> fprintf pp "OEfeqd(%a,%s,%a)" reg r1 (comparison_name Ceq) reg r2
   | OEfltd, [r1;r2] -> fprintf pp "OEfltd(%a,%s,%a)" reg r1 (comparison_name Clt) reg r2
   | OEfled, [r1;r2] -> fprintf pp "OEfled(%a,%s,%a)" reg r1 (comparison_name Cle) reg r2
diff --git a/riscV/RTLpathSE_simplify.v b/riscV/RTLpathSE_simplify.v
index 5804e67e..6066c7f5 100644
--- a/riscV/RTLpathSE_simplify.v
+++ b/riscV/RTLpathSE_simplify.v
@@ -165,7 +165,7 @@ Definition expanse_condimm_int32s (cmp: comparison) (hv1: hsval) (n: int) :=
         if Int.eq n (Int.repr Int.max_signed) then
           let hvs := loadimm32 Int.one in
           let hl := make_lhsv_cmp false hv1 hvs in
-          fSop (OEmayundef false) hl
+          fSop (OEmayundef MUint) hl
         else sltimm32 hv1 (Int.add n Int.one)
     | _ =>
         let optR0 := make_optR0 false is_inv in
@@ -208,7 +208,7 @@ Definition expanse_condimm_int64s (cmp: comparison) (hv1: hsval) (n: int64) :=
         if Int64.eq n (Int64.repr Int64.max_signed) then
           let hvs := loadimm32 Int.one in
           let hl := make_lhsv_cmp false hv1 hvs in
-          fSop (OEmayundef true) hl
+          fSop (OEmayundef MUlong) hl
         else sltimm64 hv1 (Int64.add n Int64.one)
     | _ =>
         let optR0 := make_optR0 false is_inv in
@@ -440,8 +440,8 @@ Definition target_op_simplify (op: operation) (lr: list reg) (hst: hsistate_loca
       let hl := make_lhsv_single hv1 in
       if Int.eq n Int.zero then
         let move_s := fSop Omove hl in
-        let move_l := make_lhsv_single move_s in
-        Some (fSop (OEshrxundef n) move_l)
+        let move_l := make_lhsv_cmp false move_s move_s in
+        Some (fSop (OEmayundef (MUshrx n)) move_l)
       else
         if Int.eq n Int.one then
           let srliw_s := fSop (Oshruimm (Int.repr 31)) hl in
@@ -449,8 +449,8 @@ Definition target_op_simplify (op: operation) (lr: list reg) (hst: hsistate_loca
           let addw_s := fSop Oadd srliw_l in
           let addw_l := make_lhsv_single addw_s in
           let sraiw_s := fSop (Oshrimm Int.one) addw_l in
-          let sraiw_l := make_lhsv_single sraiw_s in
-          Some (fSop (OEshrxundef n) sraiw_l)
+          let sraiw_l := make_lhsv_cmp false sraiw_s sraiw_s in
+          Some (fSop (OEmayundef (MUshrx n)) sraiw_l)
         else 
           let sraiw_s := fSop (Oshrimm (Int.repr 31)) hl in
           let sraiw_l := make_lhsv_single sraiw_s in
@@ -459,15 +459,15 @@ Definition target_op_simplify (op: operation) (lr: list reg) (hst: hsistate_loca
           let addw_s := fSop Oadd srliw_l in
           let addw_l := make_lhsv_single addw_s in
           let sraiw_s' := fSop (Oshrimm n) addw_l in
-          let sraiw_l' := make_lhsv_single sraiw_s' in
-          Some (fSop (OEshrxundef n) sraiw_l')
+          let sraiw_l' := make_lhsv_cmp false sraiw_s' sraiw_s' in
+          Some (fSop (OEmayundef (MUshrx n)) sraiw_l')
   | Oshrxlimm n, a1 :: nil =>
       let hv1 := fsi_sreg_get hst a1 in
       let hl := make_lhsv_single hv1 in
       if Int.eq n Int.zero then
         let move_s := fSop Omove hl in
-        let move_l := make_lhsv_single move_s in
-        Some (fSop (OEshrxlundef n) move_l)
+        let move_l := make_lhsv_cmp false move_s move_s in
+        Some (fSop (OEmayundef (MUshrxl n)) move_l)
       else
         if Int.eq n Int.one then
           let srlil_s := fSop (Oshrluimm (Int.repr 63)) hl in
@@ -475,8 +475,8 @@ Definition target_op_simplify (op: operation) (lr: list reg) (hst: hsistate_loca
           let addl_s := fSop Oaddl srlil_l in
           let addl_l := make_lhsv_single addl_s in
           let srail_s := fSop (Oshrlimm Int.one) addl_l in
-          let srail_l := make_lhsv_single srail_s in
-          Some (fSop (OEshrxlundef n) srail_l)
+          let srail_l := make_lhsv_cmp false srail_s srail_s in
+          Some (fSop (OEmayundef (MUshrxl n)) srail_l)
         else
           let srail_s := fSop (Oshrlimm (Int.repr 63)) hl in
           let srail_l := make_lhsv_single srail_s in
@@ -485,8 +485,8 @@ Definition target_op_simplify (op: operation) (lr: list reg) (hst: hsistate_loca
           let addl_s := fSop Oaddl srlil_l in
           let addl_l := make_lhsv_single addl_s in
           let srail_s' := fSop (Oshrlimm n) addl_l in
-          let srail_l' := make_lhsv_single srail_s' in
-          Some (fSop (OEshrxlundef n) srail_l')
+          let srail_l' := make_lhsv_cmp false srail_s' srail_s' in
+          Some (fSop (OEmayundef (MUshrxl n)) srail_l')
   (*| Oaddrstack n, nil =>*)
       (*let hv1 := fsi_sreg_get hst a1 in*)
       (*OK (addptrofs hv1 n)*)
@@ -964,7 +964,7 @@ Proof.
     try rewrite OKv1;
     try rewrite OK2;
     try rewrite (Int.add_commut _ Int.zero), Int.add_zero_l in H; subst;
-    unfold Val.cmp, may_undef_int, zero32, Val.add; simpl;
+    unfold Val.cmp, eval_may_undef, zero32, Val.add; simpl;
     destruct v; auto.
   all:
     try rewrite ltu_12_wordsize;
@@ -1018,7 +1018,7 @@ Proof.
     try rewrite OKv1;
     try rewrite OK2;
     rewrite HMEM;
-    unfold may_undef_int, Val.cmpu;
+    unfold eval_may_undef, Val.cmpu;
     destruct v; simpl; auto;
     try rewrite EQIMM; try destruct (Archi.ptr64) eqn:EQARCH; simpl;
     try rewrite ltu_12_wordsize; trivial;
@@ -1141,7 +1141,7 @@ Proof.
     unfold Val.cmpl, Val.addl;
     try rewrite xorl_zero_eq_cmpl; trivial;
     try rewrite optbool_mktotal; trivial;
-    unfold may_undef_int, zero32, Val.add; simpl;
+    unfold eval_may_undef, zero32, Val.add; simpl;
     destruct v; auto.
   1,2,3,4,5,6,7,8,9,10,11,12:
       try rewrite <- optbool_mktotal; trivial;
@@ -1210,7 +1210,7 @@ Proof.
   all: try apply xor_neg_ltle_cmplu; trivial.
   (* Others subcases with swap/negation *)
   all:
-    unfold Val.cmplu, may_undef_int, zero64, Val.addl;
+    unfold Val.cmplu, eval_may_undef, zero64, Val.addl;
     try apply Int64.same_if_eq in EQLO; subst;
     try rewrite Int64.add_commut, Int64.add_zero_l in *; trivial;
     try rewrite Int64.add_commut;
@@ -1681,41 +1681,57 @@ Lemma simplify_shrximm_correct ge sp rs0 m0 lr hst fsv st args m n: forall
           hsi_sreg_eval ge sp hst r rs0 m0 =
           seval_sval ge sp (si_sreg st r) rs0 m0)
   (H : match lr with
-      | nil => None
-      | a1 :: nil =>
-          if Int.eq n Int.zero
-          then
-           Some
-             (fSop (OEshrxundef n)
-                (make_lhsv_single
-                   (fSop Omove (make_lhsv_single (fsi_sreg_get hst a1)))))
-          else
-           if Int.eq n Int.one
+       | nil => None
+       | a1 :: nil =>
+           if Int.eq n Int.zero
            then
             Some
-              (fSop (OEshrxundef n)
-                 (make_lhsv_single
-                    (fSop (Oshrimm Int.one)
-                       (make_lhsv_single
-                          (fSop Oadd
-                             (make_lhsv_cmp false (fsi_sreg_get hst a1)
-                                (fSop (Oshruimm (Int.repr 31))
-                                   (make_lhsv_single (fsi_sreg_get hst a1)))))))))
+              (fSop (OEmayundef (MUshrx n))
+                 (make_lhsv_cmp false
+                    (fSop Omove (make_lhsv_single (fsi_sreg_get hst a1)))
+                    (fSop Omove (make_lhsv_single (fsi_sreg_get hst a1)))))
            else
-            Some
-              (fSop (OEshrxundef n)
-                 (make_lhsv_single
-                    (fSop (Oshrimm n)
-                       (make_lhsv_single
-                          (fSop Oadd
-                             (make_lhsv_cmp false (fsi_sreg_get hst a1)
-                                (fSop (Oshruimm (Int.sub Int.iwordsize n))
-                                   (make_lhsv_single
-                                      (fSop (Oshrimm (Int.repr 31))
-                                         (make_lhsv_single
-                                            (fsi_sreg_get hst a1)))))))))))
-      | a1 :: _ :: _ => None
-      end = Some fsv)
+            if Int.eq n Int.one
+            then
+             Some
+               (fSop (OEmayundef (MUshrx n))
+                  (make_lhsv_cmp false
+                     (fSop (Oshrimm Int.one)
+                        (make_lhsv_single
+                           (fSop Oadd
+                              (make_lhsv_cmp false (fsi_sreg_get hst a1)
+                                 (fSop (Oshruimm (Int.repr 31))
+                                    (make_lhsv_single (fsi_sreg_get hst a1)))))))
+                     (fSop (Oshrimm Int.one)
+                        (make_lhsv_single
+                           (fSop Oadd
+                              (make_lhsv_cmp false (fsi_sreg_get hst a1)
+                                 (fSop (Oshruimm (Int.repr 31))
+                                    (make_lhsv_single (fsi_sreg_get hst a1)))))))))
+            else
+             Some
+               (fSop (OEmayundef (MUshrx n))
+                  (make_lhsv_cmp false
+                     (fSop (Oshrimm n)
+                        (make_lhsv_single
+                           (fSop Oadd
+                              (make_lhsv_cmp false (fsi_sreg_get hst a1)
+                                 (fSop (Oshruimm (Int.sub Int.iwordsize n))
+                                    (make_lhsv_single
+                                       (fSop (Oshrimm (Int.repr 31))
+                                          (make_lhsv_single
+                                             (fsi_sreg_get hst a1)))))))))
+                     (fSop (Oshrimm n)
+                        (make_lhsv_single
+                           (fSop Oadd
+                              (make_lhsv_cmp false (fsi_sreg_get hst a1)
+                                 (fSop (Oshruimm (Int.sub Int.iwordsize n))
+                                    (make_lhsv_single
+                                       (fSop (Oshrimm (Int.repr 31))
+                                          (make_lhsv_single
+                                             (fsi_sreg_get hst a1)))))))))))
+       | a1 :: _ :: _ => None
+       end = Some fsv)
   (OK1 : seval_list_sval ge sp (list_sval_inj (map (si_sreg st) lr)) rs0 m0 = Some args),
   seval_sval ge sp (hsval_proj fsv) rs0 m0 =
   eval_operation ge sp (Oshrximm n) args m.
@@ -1734,7 +1750,7 @@ Proof.
     erewrite !fsi_sreg_get_correct; eauto;
     destruct (seval_sval ge sp (si_sreg st p) rs0 m0) eqn:OKv1; try congruence; inv H1;
     destruct (Val.shrx v (Vint n)) eqn:TOTAL; cbn;
-    unfold shrx_imm_undef.
+    unfold eval_may_undef.
   2,4,6:
     unfold Val.shrx in TOTAL;
     destruct v; simpl in TOTAL; simpl; try congruence;
@@ -1769,41 +1785,57 @@ Lemma simplify_shrxlimm_correct ge sp rs0 m0 lr hst fsv st args m n: forall
           hsi_sreg_eval ge sp hst r rs0 m0 =
           seval_sval ge sp (si_sreg st r) rs0 m0)
   (H : match lr with
-      | nil => None
-      | a1 :: nil =>
-          if Int.eq n Int.zero
-          then
-           Some
-             (fSop (OEshrxlundef n)
-                (make_lhsv_single
-                   (fSop Omove (make_lhsv_single (fsi_sreg_get hst a1)))))
-          else
-           if Int.eq n Int.one
+       | nil => None
+       | a1 :: nil =>
+           if Int.eq n Int.zero
            then
             Some
-              (fSop (OEshrxlundef n)
-                 (make_lhsv_single
-                    (fSop (Oshrlimm Int.one)
-                       (make_lhsv_single
-                          (fSop Oaddl
-                             (make_lhsv_cmp false (fsi_sreg_get hst a1)
-                                (fSop (Oshrluimm (Int.repr 63))
-                                   (make_lhsv_single (fsi_sreg_get hst a1)))))))))
+              (fSop (OEmayundef (MUshrxl n))
+                 (make_lhsv_cmp false
+                    (fSop Omove (make_lhsv_single (fsi_sreg_get hst a1)))
+                    (fSop Omove (make_lhsv_single (fsi_sreg_get hst a1)))))
            else
-            Some
-              (fSop (OEshrxlundef n)
-                 (make_lhsv_single
-                    (fSop (Oshrlimm n)
-                       (make_lhsv_single
-                          (fSop Oaddl
-                             (make_lhsv_cmp false (fsi_sreg_get hst a1)
-                                (fSop (Oshrluimm (Int.sub Int64.iwordsize' n))
-                                   (make_lhsv_single
-                                      (fSop (Oshrlimm (Int.repr 63))
-                                         (make_lhsv_single
-                                            (fsi_sreg_get hst a1)))))))))))
-      | a1 :: _ :: _ => None
-      end = Some fsv)
+            if Int.eq n Int.one
+            then
+             Some
+               (fSop (OEmayundef (MUshrxl n))
+                  (make_lhsv_cmp false
+                     (fSop (Oshrlimm Int.one)
+                        (make_lhsv_single
+                           (fSop Oaddl
+                              (make_lhsv_cmp false (fsi_sreg_get hst a1)
+                                 (fSop (Oshrluimm (Int.repr 63))
+                                    (make_lhsv_single (fsi_sreg_get hst a1)))))))
+                     (fSop (Oshrlimm Int.one)
+                        (make_lhsv_single
+                           (fSop Oaddl
+                              (make_lhsv_cmp false (fsi_sreg_get hst a1)
+                                 (fSop (Oshrluimm (Int.repr 63))
+                                    (make_lhsv_single (fsi_sreg_get hst a1)))))))))
+            else
+             Some
+               (fSop (OEmayundef (MUshrxl n))
+                  (make_lhsv_cmp false
+                     (fSop (Oshrlimm n)
+                        (make_lhsv_single
+                           (fSop Oaddl
+                              (make_lhsv_cmp false (fsi_sreg_get hst a1)
+                                 (fSop (Oshrluimm (Int.sub Int64.iwordsize' n))
+                                    (make_lhsv_single
+                                       (fSop (Oshrlimm (Int.repr 63))
+                                          (make_lhsv_single
+                                             (fsi_sreg_get hst a1)))))))))
+                     (fSop (Oshrlimm n)
+                        (make_lhsv_single
+                           (fSop Oaddl
+                              (make_lhsv_cmp false (fsi_sreg_get hst a1)
+                                 (fSop (Oshrluimm (Int.sub Int64.iwordsize' n))
+                                    (make_lhsv_single
+                                       (fSop (Oshrlimm (Int.repr 63))
+                                          (make_lhsv_single
+                                             (fsi_sreg_get hst a1)))))))))))
+       | a1 :: _ :: _ => None
+       end = Some fsv)
   (OK1 : seval_list_sval ge sp (list_sval_inj (map (si_sreg st) lr)) rs0 m0 = Some args),
   seval_sval ge sp (hsval_proj fsv) rs0 m0 =
   eval_operation ge sp (Oshrxlimm n) args m.
@@ -1822,7 +1854,7 @@ Proof.
     erewrite !fsi_sreg_get_correct; eauto;
     destruct (seval_sval ge sp (si_sreg st p) rs0 m0) eqn:OKv1; try congruence; inv H1;
     destruct (Val.shrxl v (Vint n)) eqn:TOTAL; cbn;
-    unfold shrxl_imm_undef.
+    unfold eval_may_undef.
   2,4,6:
     unfold Val.shrxl in TOTAL;
     destruct v; simpl in TOTAL; simpl; try congruence;
@@ -1850,7 +1882,7 @@ Proof.
     destruct Int.ltu eqn:EQN2 in TOTAL; try discriminate.
     rewrite !EQN2. rewrite EQN0.
     reflexivity.
-Qed.
+ Qed.
 
 Lemma simplify_cast32unsigned_correct ge sp rs0 m0 lr hst fsv st args m: forall
   (SREG: forall r: positive,
@@ -2001,7 +2033,7 @@ Proof.
     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 may_undef_int; 
+    unfold eval_may_undef; 
     try erewrite !fsi_sreg_get_correct; eauto;
     try rewrite OKv1; simpl; trivial;
     try destruct v; try rewrite H;
diff --git a/riscV/ValueAOp.v b/riscV/ValueAOp.v
index fe519921..82291f9c 100644
--- a/riscV/ValueAOp.v
+++ b/riscV/ValueAOp.v
@@ -27,42 +27,28 @@ Definition apply_bin_r0 {B} (optR0: option bool) (sem: aval -> aval -> B) (v1 v2
   | Some false => sem v1 vz
   end.
 
-Definition may_undef_int (is_long: bool) (v1 v2: aval): aval :=
-  if negb is_long then
-    match v1 with
-    | I _ => v2
-    | _ => Ifptr Ptop
-    end
-  else
-    match v1 with
-    | L _ => v2
-    | _ => Ifptr Ptop
-    end.
-
-Definition shrx_imm_undef (v1 v2: aval): aval :=
-  match v1 with
-  | I n1 =>
-      match v2 with
-      | I n2 =>
-          if Int.ltu n2 (Int.repr 31)
-          then I n1
-          else Ifptr Ptop
+Definition eval_may_undef (mu: mayundef) (v1 v2: aval): aval :=
+  match mu with
+  | MUint => match v1 with
+             | I _ => v2
+             | _ => Ifptr Ptop
+             end
+  | MUlong => match v1 with
+              | L _ => v2
+              | _ => Ifptr Ptop
+              end
+  | MUshrx i =>
+      match v1 with
+      | I _ =>
+          if Int.ltu i (Int.repr 31) then v1 else Ifptr Ptop
       | _ => Ifptr Ptop
       end
-  | _ => Ifptr Ptop
-  end.
-
-Definition shrxl_imm_undef (v1 v2: aval): aval :=
-  match v1 with
-  | L n1 =>
-      match v2 with
-      | I n2 =>
-          if Int.ltu n2 (Int.repr 63)
-          then L n1
-          else Ifptr Ptop
+  | MUshrxl i =>
+      match v1 with
+      | L _ =>
+          if Int.ltu i (Int.repr 63) then v1 else Ifptr Ptop
       | _ => Ifptr Ptop
       end
-  | _ => Ifptr Ptop
   end.
 
 Definition eval_static_condition (cond: condition) (vl: list aval): abool :=
@@ -263,9 +249,7 @@ Definition eval_static_operation (op: operation) (vl: list aval): aval :=
   | OEaddil n, v1::nil => addl (L n) v1
   | OEaddilr0 n, nil => addl (L n) zero64
   | OEloadli n, nil => L (n)
-  | OEmayundef is_long, v1::v2::nil => may_undef_int is_long v1 v2
-  | OEshrxundef n, v1::nil => shrx_imm_undef v1 (I n)
-  | OEshrxlundef n, v1::nil => shrxl_imm_undef v1 (I n)
+  | OEmayundef mu, v1 :: v2 :: nil => eval_may_undef mu v1 v2
   | OEfeqd, v1::v2::nil => of_optbool (cmpf_bool Ceq v1 v2)
   | OEfltd, v1::v2::nil => of_optbool (cmpf_bool Clt v1 v2)
   | OEfled, v1::v2::nil => of_optbool (cmpf_bool Cle v1 v2)
@@ -508,21 +492,16 @@ Proof.
   
   1,10: simpl; eauto with va.
   2:
-    unfold Op.may_undef_int, may_undef_int; destruct is_long;
-    simpl; inv H0; inv H1; eauto with va; inv H;
-    apply vmatch_ifptr_p; eauto with va.
+    unfold Op.eval_may_undef, eval_may_undef; destruct mu;
+    inv H1; inv H0; eauto with va;
+    try destruct (Int.ltu _ _); simpl;
+    try eapply vmatch_ifptr_p, pmatch_top'; eauto with va.
   
   3,4,6: apply eval_cmplu_sound; auto.
   1,2,3: apply eval_cmpl_sound; auto.
   { unfold Val.cmpl; apply of_optbool_maketotal_sound; eauto with va. }
   { unfold Val.cmplu; apply of_optbool_maketotal_sound; eauto with va. }
   { unfold zero64; simpl; eauto with va. }
-  { unfold Op.shrx_imm_undef, shrx_imm_undef.
-    simpl; inv H1; eauto with va;
-    destruct (Int.ltu _ _); simpl; eauto with va. }
-  { unfold Op.shrxl_imm_undef, shrxl_imm_undef.
-    simpl; inv H1; eauto with va;
-    destruct (Int.ltu _ _); simpl; eauto with va. }
   all: unfold Val.cmpf; apply of_optbool_sound; eauto with va.
 Qed.