2 files changed, 10 insertions, 29 deletions
diff --git a/mppa_k1c/Asmblockgen.v b/mppa_k1c/Asmblockgen.v
index 80210f7f..835b8a8c 100644
--- a/mppa_k1c/Asmblockgen.v
+++ b/mppa_k1c/Asmblockgen.v
@@ -519,11 +519,7 @@ Definition transl_op
       OK (Psrliw rd rs n ::i k)
   | Oshrximm 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
-          Psraiw RTMP rs (Int.repr 31) ::i
-          Psrliw RTMP RTMP (Int.sub Int.iwordsize n) ::i
-          Paddw RTMP rs RTMP ::i
-          Psraiw rd RTMP n ::i k)
+      OK (Psrxiw rd rs n ::i k)
   | Ororimm n, a1 :: nil =>
     do rd <- ireg_of res; do rs <- ireg_of a1;
       OK (Proriw rd rs n ::i k)
diff --git a/mppa_k1c/Asmblockgenproof1.v b/mppa_k1c/Asmblockgenproof1.v
index bbcffbe2..a2f11154 100644
--- a/mppa_k1c/Asmblockgenproof1.v
+++ b/mppa_k1c/Asmblockgenproof1.v
@@ -1593,31 +1593,16 @@ Opaque Int.eq.
   destruct (rs x0); auto; simpl. rewrite A; simpl. Simpl. unfold Val.shr. rewrite A. 
   apply Val.lessdef_same. f_equal. apply Int.sign_ext_shr_shl. split; reflexivity.
 - (* Oshrximm *)
-  clear H. exploit Val.shrx_shr_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 32) with Int.iwordsize. set (n' := Int.sub Int.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.
-(* - (* Ocast32signed *)
-  exploit cast32signed_correct; eauto. intros (rs' & A & B & C).
-  exists rs'; split; eauto. split. apply B.
-  intros. assert (r <> PC). { destruct r; auto; contradict H; discriminate. }
-  apply C; auto.
- *)(* - (* longofintu *)
-  econstructor; split.
-  eapply exec_straight_three. simpl; eauto. simpl; eauto. simpl; eauto.
-  split; intros; Simpl. (* unfold Pregmap.set; Simpl. *) destruct (PregEq.eq x0 x0).
-  + destruct (rs x0); auto. simpl. 
-    assert (A: Int.ltu (Int.repr 32) Int64.iwordsize' = true) by auto.
-    rewrite A; simpl. rewrite A. apply Val.lessdef_same. f_equal.
-    rewrite cast32unsigned_from_cast32signed. apply Int64.zero_ext_shru_shl. compute; auto.
-  + contradict n. auto. *)
+  + 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.
 - (* Oshrxlimm *)
   clear H. exploit Val.shrxl_shrl_2; eauto. intros E; subst v; clear EV.
   destruct (Int.eq n Int.zero).