5 files changed, 25 insertions, 30 deletions
diff --git a/mppa_k1c/Asmgen.v b/mppa_k1c/Asmgen.v
index dbd7b4f5..6b6531c3 100644
--- a/mppa_k1c/Asmgen.v
+++ b/mppa_k1c/Asmgen.v
@@ -429,11 +429,11 @@ Definition transl_op
   | Ocast32signed, a1 :: nil =>
       do rd <- ireg_of res; do rs <- ireg_of a1;
       OK (cast32signed rd rs k)
-(*| Ocast32unsigned, a1 :: nil =>
+  | Ocast32unsigned, a1 :: nil =>
       do rd <- ireg_of res; do rs <- ireg_of a1;
       assertion (ireg_eq rd rs);
-      OK (Pcvtw2l rd :: Psllil rd rd (Int.repr 32) :: Psrlil rd rd (Int.repr 32) :: k)
-*)| Oaddl, a1 :: a2 :: nil =>
+      OK (Pcvtw2l rd ::i Psllil rd rd (Int.repr 32) ::i Psrlil rd rd (Int.repr 32) ::i k)
+  | Oaddl, a1 :: a2 :: nil =>
       do rd <- ireg_of res; do rs1 <- ireg_of a1; do rs2 <- ireg_of a2;
       OK (Paddl rd rs1 rs2 ::i k)
   | Oaddlimm n, a1 :: nil =>
diff --git a/mppa_k1c/Asmgenproof1.v b/mppa_k1c/Asmgenproof1.v
index ecb06802..bb39b4a5 100644
--- a/mppa_k1c/Asmgenproof1.v
+++ b/mppa_k1c/Asmgenproof1.v
@@ -1124,6 +1124,15 @@ Opaque Int.eq.
   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. auto. auto. auto.
+  split; intros; Simpl. unfold getl; 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.
 - (* Ocmp *)
   exploit transl_cond_op_correct; eauto. intros (rs' & A & B & C).
   exists rs'; split. eexact A. eauto with asmgen.
@@ -1170,13 +1179,7 @@ Opaque Int.eq.
   intros (rs' & A & B & C).
   exists rs'; split; eauto. rewrite B; auto with asmgen.
 
-- (* longofintu *)
-  econstructor; split.
-  eapply exec_straight_three. simpl; eauto. simpl; eauto. simpl; eauto. auto. auto. auto.
-  split; intros; Simpl. 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.
+
 
 - (* addlimm *)
   exploit (opimm64_correct Paddl Paddil Val.addl); auto. instantiate (1 := x0); eauto with asmgen.
diff --git a/mppa_k1c/Machregs.v b/mppa_k1c/Machregs.v
index ed582c98..bed3c040 100644
--- a/mppa_k1c/Machregs.v
+++ b/mppa_k1c/Machregs.v
@@ -208,11 +208,11 @@ Global Opaque
   integers as their 64-bit sign extension; and [Ocast32unsigned],
   because it builds on the same magic no-op. *)
 
-Definition two_address_op (op: operation) : bool := false.
-  (* match op with
-  | Ocast32signed | Ocast32unsigned => true
+Definition two_address_op (op: operation) : bool :=
+  match op with
+  | Ocast32unsigned => true
   | _ => false
-  end. *)
+  end.
 
 (** Constraints on constant propagation for builtins *)
 
diff --git a/mppa_k1c/SelectLong.v b/mppa_k1c/SelectLong.v
index 876d02fb..f2aa6be2 100644
--- a/mppa_k1c/SelectLong.v
+++ b/mppa_k1c/SelectLong.v
@@ -706,14 +706,10 @@ Definition notl (e: expr) :=
 
 (** ** Integer division and modulus *)
 
-Definition divlu_base (e1: expr) (e2: expr) :=
-  if Archi.splitlong then SplitLong.divlu_base e1 e2 else Eop Odivlu (e1:::e2:::Enil).
-Definition modlu_base (e1: expr) (e2: expr) :=
-  if Archi.splitlong then SplitLong.modlu_base e1 e2 else Eop Omodlu (e1:::e2:::Enil).
-Definition divls_base (e1: expr) (e2: expr) :=
-  if Archi.splitlong then SplitLong.divls_base e1 e2 else Eop Odivl (e1:::e2:::Enil).
-Definition modls_base (e1: expr) (e2: expr) :=
-  if Archi.splitlong then SplitLong.modls_base e1 e2 else Eop Omodl (e1:::e2:::Enil).
+Definition divlu_base (e1: expr) (e2: expr) := SplitLong.divlu_base e1 e2.
+Definition modlu_base (e1: expr) (e2: expr) := SplitLong.modlu_base e1 e2.
+Definition divls_base (e1: expr) (e2: expr) := SplitLong.divls_base e1 e2.
+Definition modls_base (e1: expr) (e2: expr) := SplitLong.modls_base e1 e2.
 
 Definition shrxlimm (e: expr) (n: int) :=
   if Archi.splitlong then SplitLong.shrxlimm e n else
diff --git a/mppa_k1c/SelectLongproof.v b/mppa_k1c/SelectLongproof.v
index 511dee92..d12fb9ae 100644
--- a/mppa_k1c/SelectLongproof.v
+++ b/mppa_k1c/SelectLongproof.v
@@ -447,30 +447,26 @@ Qed.
 
 Theorem eval_divls_base: partial_binary_constructor_sound divls_base Val.divls.
 Proof.
-  unfold divls_base; red; intros. destruct Archi.splitlong eqn:SL.
+  unfold divls_base; red; intros.
   eapply SplitLongproof.eval_divls_base; eauto.
-  TrivialExists.
 Qed.
 
 Theorem eval_modls_base: partial_binary_constructor_sound modls_base Val.modls.
 Proof.
-  unfold modls_base; red; intros. destruct Archi.splitlong eqn:SL.
+  unfold modls_base; red; intros.
   eapply SplitLongproof.eval_modls_base; eauto.
-  TrivialExists.
 Qed.
 
 Theorem eval_divlu_base: partial_binary_constructor_sound divlu_base Val.divlu.
 Proof.
-  unfold divlu_base; red; intros. destruct Archi.splitlong eqn:SL.
+  unfold divlu_base; red; intros.
   eapply SplitLongproof.eval_divlu_base; eauto.
-  TrivialExists.
 Qed.
 
 Theorem eval_modlu_base: partial_binary_constructor_sound modlu_base Val.modlu.
 Proof.
-  unfold modlu_base; red; intros. destruct Archi.splitlong eqn:SL.
+  unfold modlu_base; red; intros.
   eapply SplitLongproof.eval_modlu_base; eauto.
-  TrivialExists.
 Qed.
 
 Theorem eval_shrxlimm: