srsd

2 files changed, 10 insertions, 16 deletions

diff --git a/mppa_k1c/Asmblockgen.v b/mppa_k1c/Asmblockgen.v
index 835b8a8c..49f6e4f9 100644
--- a/mppa_k1c/Asmblockgen.v
+++ b/mppa_k1c/Asmblockgen.v
@@ -641,11 +641,7 @@ Definition transl_op
       OK (Psrlil rd rs n ::i k)
   | Oshrxlimm n, a1 :: nil =>
       do rd <- ireg_of res; do rs <- ireg_of a1;
-      OK (if Int.eq n Int.zero then Pmv rd rs ::i k else
-          Psrail RTMP rs (Int.repr 63) ::i
-          Psrlil RTMP RTMP (Int.sub Int64.iwordsize' n) ::i
-          Paddl RTMP rs RTMP ::i
-          Psrail rd RTMP n ::i k)
+      OK (Psrxil rd rs n ::i k)
   | Omaddl, a1 :: a2 :: a3 :: nil =>
     assertion (mreg_eq a1 res);
       do r1 <- ireg_of a1;
diff --git a/mppa_k1c/Asmblockgenproof1.v b/mppa_k1c/Asmblockgenproof1.v
index a2f11154..40f9f08b 100644
--- a/mppa_k1c/Asmblockgenproof1.v
+++ b/mppa_k1c/Asmblockgenproof1.v
@@ -1604,18 +1604,16 @@ Opaque Int.eq.
     * intros.
       rewrite Pregmap.gso; trivial.
 - (* Oshrxlimm *)
-  clear H. exploit Val.shrxl_shrl_2; eauto. intros E; subst v; clear EV.
-  destruct (Int.eq n Int.zero).
-+ econstructor; split. apply exec_straight_one. simpl; eauto.
-  split; intros; Simpl. 
-+ change (Int.repr 64) with Int64.iwordsize'. set (n' := Int.sub Int64.iwordsize' n).
   econstructor; split.
-  eapply exec_straight_step. simpl; reflexivity.
-  eapply exec_straight_step. simpl; reflexivity.
-  eapply exec_straight_step. simpl; reflexivity.
-  apply exec_straight_one. simpl; reflexivity.
-
-  split; intros; Simpl.
+  + apply exec_straight_one. simpl. eauto.
+  + split.
+    * rewrite Pregmap.gss.
+      subst v.
+      destruct (rs x0); simpl; trivial.
+      unfold Val.maketotal.
+      destruct (Int.ltu _ _); simpl; trivial.
+    * intros.
+      rewrite Pregmap.gso; trivial.
 - (* Ocmp *)
   exploit transl_cond_op_correct; eauto. intros (rs' & A & B & C).
   exists rs'; split. eexact A. eauto with asmgen.