Merge remote-tracking branch 'origin/mppa-work' into mppa-refactor

Conflicts:
	mppa_k1c/Asm.v
	mppa_k1c/Asmblock.v

15 files changed, 1202 insertions, 87 deletions

diff --git a/mppa_k1c/Asm.v b/mppa_k1c/Asm.v
index 893552c4..303a624c 100644
--- a/mppa_k1c/Asm.v
+++ b/mppa_k1c/Asm.v
@@ -214,6 +214,8 @@ Inductive instruction : Type :=
   | Pandnil             (rd rs: ireg) (imm: int64)  (**r andn long *)

   | Pornil              (rd rs: ireg) (imm: int64)  (**r orn long *)

   | Pmaddil             (rd rs: ireg) (imm: int64)  (**r multiply add imm long *)

+  | Pcmove (bt: btest) (rcond rd rs : ireg) (** conditional move *) 

+  | Pcmoveu (bt: btest) (rcond rd rs : ireg) (** conditional move, unsigned semantics *) 

 .

 

 (** Correspondance between Asmblock and Asm *)

@@ -361,6 +363,8 @@ Definition basic_to_instruction (b: basic) :=
   (** ARRR *)

   | PArithARRR Asmvliw.Pmaddw rd rs1 rs2       => Pmaddw rd rs1 rs2

   | PArithARRR Asmvliw.Pmaddl rd rs1 rs2       => Pmaddl rd rs1 rs2

+  | PArithARRR (Asmvliw.Pcmove cond) rd rs1 rs2=> Pcmove cond rd rs1 rs2

+  | PArithARRR (Asmvliw.Pcmoveu cond) rd rs1 rs2=> Pcmoveu cond rd rs1 rs2

 

   (** ARRI32 *)

   | PArithARRI32 Asmvliw.Pmaddiw rd rs1 imm    => Pmaddiw rd rs1 imm

diff --git a/mppa_k1c/Asmblockdeps.v b/mppa_k1c/Asmblockdeps.v
index ee76e3e5..18aeafac 100644
--- a/mppa_k1c/Asmblockdeps.v
+++ b/mppa_k1c/Asmblockdeps.v
@@ -1445,6 +1445,8 @@ Definition string_of_name_arrr (n: arith_name_arrr): pstring :=
   match n with
   | Pmaddw  => "Pmaddw"
   | Pmaddl  => "Pmaddl"
+  | Pcmove _ => "Pcmove"
+  | Pcmoveu _ => "Pcmoveu"
   end.
 
 Definition string_of_name_arri32 (n: arith_name_arri32): pstring :=
diff --git a/mppa_k1c/Asmblockgen.v b/mppa_k1c/Asmblockgen.v
index 7cd02540..bf466c4e 100644
--- a/mppa_k1c/Asmblockgen.v
+++ b/mppa_k1c/Asmblockgen.v
@@ -367,6 +367,28 @@ Definition transl_cond_op
       Error(msg "Asmblockgen.transl_cond_op")
 end.
 
+(* CoMPare Unsigned Words to Zero *)
+Definition btest_for_cmpuwz (c: comparison) :=
+  match c with
+  | Cne => OK BTwnez
+  | Ceq => OK BTweqz
+  | Clt => Error (msg "btest_for_compuwz: Clt")
+  | Cge => Error (msg "btest_for_compuwz: Cge")
+  | Cle => Error (msg "btest_for_compuwz: Cle")
+  | Cgt => Error (msg "btest_for_compuwz: Cgt")
+  end.
+
+(* CoMPare Unsigned Words to Zero *)
+Definition btest_for_cmpudz (c: comparison) :=
+  match c with
+  | Cne => OK BTdnez
+  | Ceq => OK BTdeqz
+  | Clt => Error (msg "btest_for_compudz: Clt")
+  | Cge => Error (msg "btest_for_compudz: Cge")
+  | Cle => Error (msg "btest_for_compudz: Cle")
+  | Cgt => Error (msg "btest_for_compudz: Cgt")
+  end.
+
 (** Translation of the arithmetic operation [r <- op(args)].
   The corresponding instructions are prepended to [k]. *)
 
@@ -729,6 +751,27 @@ Definition transl_op
       do rd <- ireg_of res;
       transl_cond_op cmp rd args k
 
+  | Oselect cond, a0 :: a1 :: aS :: nil
+  | Oselectl cond, a0 :: a1 :: aS :: nil
+  | Oselectf cond, a0 :: a1 :: aS :: nil
+  | Oselectfs cond, a0 :: a1 :: aS :: nil  =>
+    assertion (mreg_eq a0 res);
+      do r0 <- ireg_of a0;
+      do r1 <- ireg_of a1;
+      do rS <- ireg_of aS;
+      (match cond with
+       | Ccomp0 cmp =>
+         OK (Pcmove (btest_for_cmpswz cmp) r0 rS r1 ::i k)
+       | Ccompu0 cmp =>
+         do bt <- btest_for_cmpuwz cmp;
+           OK (Pcmoveu bt r0 rS r1 ::i k)
+       | Ccompl0 cmp =>
+         OK (Pcmove (btest_for_cmpsdz cmp) r0 rS r1 ::i k)
+       | Ccomplu0 cmp =>
+         do bt <- btest_for_cmpudz cmp;
+           OK (Pcmoveu bt r0 rS r1 ::i k)
+       end)
+
   | _, _ =>
       Error(msg "Asmgenblock.transl_op")
   end.
diff --git a/mppa_k1c/Asmblockgenproof1.v b/mppa_k1c/Asmblockgenproof1.v
index a2b307fb..bbcffbe2 100644
--- a/mppa_k1c/Asmblockgenproof1.v
+++ b/mppa_k1c/Asmblockgenproof1.v
@@ -1527,6 +1527,26 @@ Ltac TranslOpSimpl :=
   [ apply exec_straight_one; reflexivity
   | split; [ apply Val.lessdef_same; simpl; Simpl; fail | intros; simpl; Simpl; fail ] ].
 
+Lemma int_eq_comm:
+  forall (x y: int),
+  (Int.eq x y) = (Int.eq y x).
+Proof.
+  intros.
+  unfold Int.eq.
+  unfold zeq.
+  destruct (Z.eq_dec _ _); destruct (Z.eq_dec _ _); congruence.
+Qed.
+
+Lemma int64_eq_comm:
+  forall (x y: int64),
+  (Int64.eq x y) = (Int64.eq y x).
+Proof.
+  intros.
+  unfold Int64.eq.
+  unfold zeq.
+  destruct (Z.eq_dec _ _); destruct (Z.eq_dec _ _); congruence.
+Qed.
+
 Lemma transl_op_correct:
   forall op args res k (rs: regset) m v c,
   transl_op op args res k = OK c ->
@@ -1614,69 +1634,250 @@ Opaque Int.eq.
 - (* Ocmp *)
   exploit transl_cond_op_correct; eauto. intros (rs' & A & B & C).
   exists rs'; split. eexact A. eauto with asmgen.
-(*
-- (* intconst *)
-  exploit loadimm32_correct; eauto. intros (rs' & A & B & C).
-  exists rs'; split; eauto. rewrite B; auto with asmgen.
-- (* longconst *)
-  exploit loadimm64_correct; eauto. intros (rs' & A & B & C).
-  exists rs'; split; eauto. rewrite B; auto with asmgen.
-- (* floatconst *)
-  destruct (Float.eq_dec n Float.zero).
-+ subst n. econstructor; split. 
-  apply exec_straight_one. simpl; eauto. auto.
-  split; intros; Simpl. 
-+ econstructor; split. 
-  apply exec_straight_one. simpl; eauto. auto.
-  split; intros; Simpl. 
-- (* singleconst *)
-  destruct (Float32.eq_dec n Float32.zero).
-+ subst n. econstructor; split. 
-  apply exec_straight_one. simpl; eauto. auto.
-  split; intros; Simpl. 
-+ econstructor; split. 
-  apply exec_straight_one. simpl; eauto. auto.
-  split; intros; Simpl. 
-- (* stackoffset *)
-  exploit addptrofs_correct. instantiate (1 := X2); auto with asmgen. intros (rs' & A & B & C).
-  exists rs'; split; eauto. auto with asmgen.
-- (* addimm *)
-  exploit (opimm32_correct Paddw Paddiw Val.add); auto. instantiate (1 := x0); eauto with asmgen.
-  intros (rs' & A & B & C).
-  exists rs'; split; eauto. rewrite B; auto with asmgen. 
-- (* andimm *)
-  exploit (opimm32_correct Pandw Pandiw Val.and); auto. instantiate (1 := x0); eauto with asmgen.
-  intros (rs' & A & B & C).
-  exists rs'; split; eauto. rewrite B; auto with asmgen.
-- (* orimm *)
-  exploit (opimm32_correct Porw Poriw Val.or); auto. instantiate (1 := x0); eauto with asmgen.
-  intros (rs' & A & B & C).
-  exists rs'; split; eauto. rewrite B; auto with asmgen.
-- (* xorimm *)
-  exploit (opimm32_correct Pxorw Pxoriw Val.xor); auto. instantiate (1 := x0); eauto with asmgen.
-  intros (rs' & A & B & C).
-  exists rs'; split; eauto. rewrite B; auto with asmgen.
-
-
-
-- (* addlimm *)
-  exploit (opimm64_correct Paddl Paddil Val.addl); auto. instantiate (1 := x0); eauto with asmgen.
-  intros (rs' & A & B & C).
-  exists rs'; split; eauto. rewrite B; auto with asmgen.
-
-- (* andimm *)
-  exploit (opimm64_correct Pandl Pandil Val.andl); auto. instantiate (1 := x0); eauto with asmgen.
-  intros (rs' & A & B & C).
-  exists rs'; split; eauto. rewrite B; auto with asmgen.
-- (* orimm *)
-  exploit (opimm64_correct Porl Poril Val.orl); auto. instantiate (1 := x0); eauto with asmgen.
-  intros (rs' & A & B & C).
-  exists rs'; split; eauto. rewrite B; auto with asmgen.
-- (* xorimm *)
-  exploit (opimm64_correct Pxorl Pxoril Val.xorl); auto. instantiate (1 := x0); eauto with asmgen.
-  intros (rs' & A & B & C).
-  exists rs'; split; eauto. rewrite B; auto with asmgen.
-*)
+- (* Oselect *)
+  destruct cond in *; simpl in *; try congruence;
+    try monadInv EQ3;
+    try (injection EQ3; clear EQ3; intro Hrew; rewrite <- Hrew in * ; clear Hrew);
+  econstructor; split;
+  try ( eapply exec_straight_one; simpl; reflexivity ).
+  (* Cmp *)
+  + split.
+    * unfold eval_select.
+      destruct (rs x) eqn:eqX; try constructor.
+      destruct (rs x0) eqn:eqX0; try constructor.
+      destruct c0 in *; simpl;
+      destruct (Val.cmp_bool _ _); simpl; try constructor;
+        destruct b; simpl; rewrite Pregmap.gss; constructor.
+    * intros.
+      rewrite Pregmap.gso; congruence.
+  (* Cmpu *)
+  + split.
+    * unfold eval_select.
+      destruct (rs x) eqn:eqX; try constructor.
+      destruct (rs x0) eqn:eqX0; try constructor.
+      destruct c0 in *; simpl in *; inv EQ2; simpl.
+      ** assert (Hcmpuabs := (Val_cmpu_bool_correct m Ceq (rs x1) (Vint Int.zero))).
+         destruct (Val.cmpu_bool _ _); simpl; try constructor.
+         destruct b in *; simpl in *; [ rewrite (Hcmpuabs true) | rewrite (Hcmpuabs false)]; trivial;
+         rewrite Pregmap.gss; constructor.
+      ** assert (Hcmpuabs := (Val_cmpu_bool_correct m Cne (rs x1) (Vint Int.zero))).
+         destruct (Val.cmpu_bool _ _); simpl; try constructor.
+         destruct b in *; simpl in *; [ rewrite (Hcmpuabs true) | rewrite (Hcmpuabs false)]; trivial;
+         rewrite Pregmap.gss; constructor.
+    * intros.
+      rewrite Pregmap.gso; congruence.
+
+  (* Cmpl *)
+  + split.
+    * unfold eval_select.
+      destruct (rs x) eqn:eqX; try constructor.
+      destruct (rs x0) eqn:eqX0; try constructor.
+      destruct c0 in *; simpl;
+      destruct (Val.cmpl_bool _ _); simpl; try constructor;
+        destruct b; simpl; rewrite Pregmap.gss; constructor.
+    * intros.
+      rewrite Pregmap.gso; congruence.
+      
+  (* Cmplu *)
+  + split.
+    * unfold eval_select.
+      destruct (rs x) eqn:eqX; try constructor.
+      destruct (rs x0) eqn:eqX0; try constructor.
+      destruct c0 in *; simpl in *; inv EQ2; simpl.
+      ** assert (Hcmpluabs := (Val_cmplu_bool_correct m Ceq (rs x1) (Vlong Int64.zero))).
+         destruct (Val.cmplu_bool _ _); simpl; try constructor.
+         destruct b in *; simpl in *; [ rewrite (Hcmpluabs true) | rewrite (Hcmpluabs false)]; trivial;
+         rewrite Pregmap.gss; constructor.
+      ** assert (Hcmpluabs := (Val_cmplu_bool_correct m Cne (rs x1) (Vlong Int64.zero))).
+         destruct (Val.cmplu_bool _ _); simpl; try constructor.
+         destruct b in *; simpl in *; [ rewrite (Hcmpluabs true) | rewrite (Hcmpluabs false)]; trivial;
+         rewrite Pregmap.gss; constructor.
+    * intros.
+      rewrite Pregmap.gso; congruence.
+
+- (* Oselectl *)
+  destruct cond in *; simpl in *; try congruence;
+    try monadInv EQ3;
+    try (injection EQ3; clear EQ3; intro Hrew; rewrite <- Hrew in * ; clear Hrew);
+  econstructor; split;
+  try ( eapply exec_straight_one; simpl; reflexivity ).
+  (* Cmp *)
+  + split.
+    * unfold eval_select.
+      destruct (rs x) eqn:eqX; try constructor.
+      destruct (rs x0) eqn:eqX0; try constructor.
+      destruct c0 in *; simpl;
+      destruct (Val.cmp_bool _ _); simpl; try constructor;
+        destruct b; simpl; rewrite Pregmap.gss; constructor.
+    * intros.
+      rewrite Pregmap.gso; congruence.
+  (* Cmpu *)
+  + split.
+    * unfold eval_select.
+      destruct (rs x) eqn:eqX; try constructor.
+      destruct (rs x0) eqn:eqX0; try constructor.
+      destruct c0 in *; simpl in *; inv EQ2; simpl.
+      ** assert (Hcmpuabs := (Val_cmpu_bool_correct m Ceq (rs x1) (Vint Int.zero))).
+         destruct (Val.cmpu_bool _ _); simpl; try constructor.
+         destruct b in *; simpl in *; [ rewrite (Hcmpuabs true) | rewrite (Hcmpuabs false)]; trivial;
+         rewrite Pregmap.gss; constructor.
+      ** assert (Hcmpuabs := (Val_cmpu_bool_correct m Cne (rs x1) (Vint Int.zero))).
+         destruct (Val.cmpu_bool _ _); simpl; try constructor.
+         destruct b in *; simpl in *; [ rewrite (Hcmpuabs true) | rewrite (Hcmpuabs false)]; trivial;
+         rewrite Pregmap.gss; constructor.
+    * intros.
+      rewrite Pregmap.gso; congruence.
+
+  (* Cmpl *)
+  + split.
+    * unfold eval_select.
+      destruct (rs x) eqn:eqX; try constructor.
+      destruct (rs x0) eqn:eqX0; try constructor.
+      destruct c0 in *; simpl;
+      destruct (Val.cmpl_bool _ _); simpl; try constructor;
+        destruct b; simpl; rewrite Pregmap.gss; constructor.
+    * intros.
+      rewrite Pregmap.gso; congruence.
+      
+  (* Cmplu *)
+  + split.
+    * unfold eval_select.
+      destruct (rs x) eqn:eqX; try constructor.
+      destruct (rs x0) eqn:eqX0; try constructor.
+      destruct c0 in *; simpl in *; inv EQ2; simpl.
+      ** assert (Hcmpluabs := (Val_cmplu_bool_correct m Ceq (rs x1) (Vlong Int64.zero))).
+         destruct (Val.cmplu_bool _ _); simpl; try constructor.
+         destruct b in *; simpl in *; [ rewrite (Hcmpluabs true) | rewrite (Hcmpluabs false)]; trivial;
+         rewrite Pregmap.gss; constructor.
+      ** assert (Hcmpluabs := (Val_cmplu_bool_correct m Cne (rs x1) (Vlong Int64.zero))).
+         destruct (Val.cmplu_bool _ _); simpl; try constructor.
+         destruct b in *; simpl in *; [ rewrite (Hcmpluabs true) | rewrite (Hcmpluabs false)]; trivial;
+         rewrite Pregmap.gss; constructor.
+    * intros.
+      rewrite Pregmap.gso; congruence.
+
+- (* Oselectf *)
+  destruct cond in *; simpl in *; try congruence;
+    try monadInv EQ3;
+    try (injection EQ3; clear EQ3; intro Hrew; rewrite <- Hrew in * ; clear Hrew);
+  econstructor; split;
+  try ( eapply exec_straight_one; simpl; reflexivity ).
+  (* Cmp *)
+  + split.
+    * unfold eval_select.
+      destruct (rs x) eqn:eqX; try constructor.
+      destruct (rs x0) eqn:eqX0; try constructor.
+      destruct c0 in *; simpl;
+      destruct (Val.cmp_bool _ _); simpl; try constructor;
+        destruct b; simpl; rewrite Pregmap.gss; constructor.
+    * intros.
+      rewrite Pregmap.gso; congruence.
+  (* Cmpu *)
+  + split.
+    * unfold eval_select.
+      destruct (rs x) eqn:eqX; try constructor.
+      destruct (rs x0) eqn:eqX0; try constructor.
+      destruct c0 in *; simpl in *; inv EQ2; simpl.
+      ** assert (Hcmpuabs := (Val_cmpu_bool_correct m Ceq (rs x1) (Vint Int.zero))).
+         destruct (Val.cmpu_bool _ _); simpl; try constructor.
+         destruct b in *; simpl in *; [ rewrite (Hcmpuabs true) | rewrite (Hcmpuabs false)]; trivial;
+         rewrite Pregmap.gss; constructor.
+      ** assert (Hcmpuabs := (Val_cmpu_bool_correct m Cne (rs x1) (Vint Int.zero))).
+         destruct (Val.cmpu_bool _ _); simpl; try constructor.
+         destruct b in *; simpl in *; [ rewrite (Hcmpuabs true) | rewrite (Hcmpuabs false)]; trivial;
+         rewrite Pregmap.gss; constructor.
+    * intros.
+      rewrite Pregmap.gso; congruence.
+
+  (* Cmpl *)
+  + split.
+    * unfold eval_select.
+      destruct (rs x) eqn:eqX; try constructor.
+      destruct (rs x0) eqn:eqX0; try constructor.
+      destruct c0 in *; simpl;
+      destruct (Val.cmpl_bool _ _); simpl; try constructor;
+        destruct b; simpl; rewrite Pregmap.gss; constructor.
+    * intros.
+      rewrite Pregmap.gso; congruence.
+      
+  (* Cmplu *)
+  + split.
+    * unfold eval_select.
+      destruct (rs x) eqn:eqX; try constructor.
+      destruct (rs x0) eqn:eqX0; try constructor.
+      destruct c0 in *; simpl in *; inv EQ2; simpl.
+      ** assert (Hcmpluabs := (Val_cmplu_bool_correct m Ceq (rs x1) (Vlong Int64.zero))).
+         destruct (Val.cmplu_bool _ _); simpl; try constructor.
+         destruct b in *; simpl in *; [ rewrite (Hcmpluabs true) | rewrite (Hcmpluabs false)]; trivial;
+         rewrite Pregmap.gss; constructor.
+      ** assert (Hcmpluabs := (Val_cmplu_bool_correct m Cne (rs x1) (Vlong Int64.zero))).
+         destruct (Val.cmplu_bool _ _); simpl; try constructor.
+         destruct b in *; simpl in *; [ rewrite (Hcmpluabs true) | rewrite (Hcmpluabs false)]; trivial;
+         rewrite Pregmap.gss; constructor.
+    * intros.
+      rewrite Pregmap.gso; congruence.
+
+
+- (* Oselectfs *)
+  destruct cond in *; simpl in *; try congruence;
+    try monadInv EQ3;
+    try (injection EQ3; clear EQ3; intro Hrew; rewrite <- Hrew in * ; clear Hrew);
+  econstructor; split;
+  try ( eapply exec_straight_one; simpl; reflexivity ).
+  (* Cmp *)
+  + split.
+    * unfold eval_select.
+      destruct (rs x) eqn:eqX; try constructor.
+      destruct (rs x0) eqn:eqX0; try constructor.
+      destruct c0 in *; simpl;
+      destruct (Val.cmp_bool _ _); simpl; try constructor;
+        destruct b; simpl; rewrite Pregmap.gss; constructor.
+    * intros.
+      rewrite Pregmap.gso; congruence.
+  (* Cmpu *)
+  + split.
+    * unfold eval_select.
+      destruct (rs x) eqn:eqX; try constructor.
+      destruct (rs x0) eqn:eqX0; try constructor.
+      destruct c0 in *; simpl in *; inv EQ2; simpl.
+      ** assert (Hcmpuabs := (Val_cmpu_bool_correct m Ceq (rs x1) (Vint Int.zero))).
+         destruct (Val.cmpu_bool _ _); simpl; try constructor.
+         destruct b in *; simpl in *; [ rewrite (Hcmpuabs true) | rewrite (Hcmpuabs false)]; trivial;
+         rewrite Pregmap.gss; constructor.
+      ** assert (Hcmpuabs := (Val_cmpu_bool_correct m Cne (rs x1) (Vint Int.zero))).
+         destruct (Val.cmpu_bool _ _); simpl; try constructor.
+         destruct b in *; simpl in *; [ rewrite (Hcmpuabs true) | rewrite (Hcmpuabs false)]; trivial;
+         rewrite Pregmap.gss; constructor.
+    * intros.
+      rewrite Pregmap.gso; congruence.
+
+  (* Cmpl *)
+  + split.
+    * unfold eval_select.
+      destruct (rs x) eqn:eqX; try constructor.
+      destruct (rs x0) eqn:eqX0; try constructor.
+      destruct c0 in *; simpl;
+      destruct (Val.cmpl_bool _ _); simpl; try constructor;
+        destruct b; simpl; rewrite Pregmap.gss; constructor.
+    * intros.
+      rewrite Pregmap.gso; congruence.
+      
+  (* Cmplu *)
+  + split.
+    * unfold eval_select.
+      destruct (rs x) eqn:eqX; try constructor.
+      destruct (rs x0) eqn:eqX0; try constructor.
+      destruct c0 in *; simpl in *; inv EQ2; simpl.
+      ** assert (Hcmpluabs := (Val_cmplu_bool_correct m Ceq (rs x1) (Vlong Int64.zero))).
+         destruct (Val.cmplu_bool _ _); simpl; try constructor.
+         destruct b in *; simpl in *; [ rewrite (Hcmpluabs true) | rewrite (Hcmpluabs false)]; trivial;
+         rewrite Pregmap.gss; constructor.
+      ** assert (Hcmpluabs := (Val_cmplu_bool_correct m Cne (rs x1) (Vlong Int64.zero))).
+         destruct (Val.cmplu_bool _ _); simpl; try constructor.
+         destruct b in *; simpl in *; [ rewrite (Hcmpluabs true) | rewrite (Hcmpluabs false)]; trivial;
+         rewrite Pregmap.gss; constructor.
+    * intros.
+      rewrite Pregmap.gso; congruence.
 Qed.
 
 (** Memory accesses *)
diff --git a/mppa_k1c/Asmvliw.v b/mppa_k1c/Asmvliw.v
index 6c18ac32..8620326f 100644
--- a/mppa_k1c/Asmvliw.v
+++ b/mppa_k1c/Asmvliw.v
@@ -426,6 +426,8 @@ Inductive arith_name_rri64 : Type :=
 Inductive arith_name_arrr : Type :=
   | Pmaddw                                           (**r multiply add word *)
   | Pmaddl                                           (**r multiply add long *)
+  | Pcmove (bt: btest)                               (**r conditional move *)
+  | Pcmoveu (bt: btest)                              (**r conditional move, test on unsigned semantics *)
 .
 
 Inductive arith_name_arri32 : Type :=
@@ -990,6 +992,38 @@ Definition arith_eval_arrr n v1 v2 v3 :=
   match n with
   | Pmaddw => Val.add v1 (Val.mul v2 v3)
   | Pmaddl => Val.addl v1 (Val.mull v2 v3)
+  | Pcmove bt =>
+    match cmp_for_btest bt with
+    | (Some c, Int)  =>
+      match Val.cmp_bool c v2 (Vint Int.zero) with
+      | None => Vundef
+      | Some true => v3
+      | Some false => v1
+      end
+    | (Some c, Long) =>
+      match Val.cmpl_bool c v2 (Vlong Int64.zero) with
+      | None => Vundef
+      | Some true => v3
+      | Some false => v1
+      end
+    | (None, _) => Vundef
+    end
+  | Pcmoveu bt =>
+    match cmpu_for_btest bt with
+    | (Some c, Int)  =>
+      match Val_cmpu_bool c v2 (Vint Int.zero) with
+      | None => Vundef
+      | Some true => v3
+      | Some false => v1
+      end
+    | (Some c, Long) =>
+      match Val_cmplu_bool c v2 (Vlong Int64.zero) with
+      | None => Vundef
+      | Some true => v3
+      | Some false => v1
+      end
+    | (None, _) => Vundef
+    end
   end.
 
 Definition arith_eval_arri32 n v1 v2 v3 :=
@@ -1528,4 +1562,4 @@ Ltac Det_WIO X :=
   inv H; rewrite H0 in *; eelim NOTNULL; eauto.
 - (* final states *)
   intros s r1 r2 H H0; inv H; inv H0. congruence.
-Qed.
\ No newline at end of file
+Qed.
diff --git a/mppa_k1c/Machregs.v b/mppa_k1c/Machregs.v
index 60142797..823b13e9 100644
--- a/mppa_k1c/Machregs.v
+++ b/mppa_k1c/Machregs.v
@@ -209,7 +209,7 @@ Global Opaque
 
 Definition two_address_op (op: operation) : bool :=
   match op with
-  | Ocast32unsigned | Omadd | Omaddimm _ | Omaddl | Omaddlimm _ => true
+  | Omadd | Omaddimm _ | Omaddl | Omaddlimm _ | Oselect _ | Oselectl _ | Oselectf _ | Oselectfs _ => true
   | _ => false
   end.
 
diff --git a/mppa_k1c/NeedOp.v b/mppa_k1c/NeedOp.v
index 2577370c..ba051c90 100644
--- a/mppa_k1c/NeedOp.v
+++ b/mppa_k1c/NeedOp.v
@@ -117,6 +117,7 @@ Definition needs_of_operation (op: operation) (nv: nval): list nval :=
   | Ointofsingle | Ointuofsingle | Osingleofint | Osingleofintu => op1 (default nv)
   | Olongofsingle | Olonguofsingle | Osingleoflong | Osingleoflongu => op1 (default nv)
   | Ocmp c => needs_of_condition c
+  | Oselect _ | Oselectl _ | Oselectf _ | Oselectfs _ => op3 (default nv)
   end.
 
 Definition operation_is_redundant (op: operation) (nv: nval): bool :=
@@ -145,19 +146,75 @@ Section SOUNDNESS.
 
 Variable ge: genv.
 Variable sp: block.
-Variables m m': mem.
-Hypothesis PERM: forall b ofs k p, Mem.perm m b ofs k p -> Mem.perm m' b ofs k p.
+Variables m1 m2: mem.
+Hypothesis PERM: forall b ofs k p, Mem.perm m1 b ofs k p -> Mem.perm m2 b ofs k p.
 
 Lemma needs_of_condition_sound:
   forall cond args b args',
-  eval_condition cond args m = Some b ->
+  eval_condition cond args m1 = Some b ->
   vagree_list args args' (needs_of_condition cond) ->
-  eval_condition cond args' m' = Some b.
+  eval_condition cond args' m2 = Some b.
 Proof.
   intros. unfold needs_of_condition in H0.
   eapply default_needs_of_condition_sound; eauto.
 Qed.
 
+Let valid_pointer_inj:
+  forall b1 ofs b2 delta,
+  inject_id b1 = Some(b2, delta) ->
+  Mem.valid_pointer m1 b1 (Ptrofs.unsigned ofs) = true ->
+  Mem.valid_pointer m2 b2 (Ptrofs.unsigned (Ptrofs.add ofs (Ptrofs.repr delta))) = true.
+Proof.
+  unfold inject_id; intros. inv H. rewrite Ptrofs.add_zero.
+  rewrite Mem.valid_pointer_nonempty_perm in *. eauto.
+Qed.
+
+Let weak_valid_pointer_inj:
+  forall b1 ofs b2 delta,
+  inject_id b1 = Some(b2, delta) ->
+  Mem.weak_valid_pointer m1 b1 (Ptrofs.unsigned ofs) = true ->
+  Mem.weak_valid_pointer m2 b2 (Ptrofs.unsigned (Ptrofs.add ofs (Ptrofs.repr delta))) = true.
+Proof.
+  unfold inject_id; intros. inv H. rewrite Ptrofs.add_zero.
+  rewrite Mem.weak_valid_pointer_spec in *.
+  rewrite ! Mem.valid_pointer_nonempty_perm in *.
+  destruct H0; [left|right]; eauto.
+Qed.
+
+Let weak_valid_pointer_no_overflow:
+  forall b1 ofs b2 delta,
+  inject_id b1 = Some(b2, delta) ->
+  Mem.weak_valid_pointer m1 b1 (Ptrofs.unsigned ofs) = true ->
+  0 <= Ptrofs.unsigned ofs + Ptrofs.unsigned (Ptrofs.repr delta) <= Ptrofs.max_unsigned.
+Proof.
+  unfold inject_id; intros. inv H. rewrite Z.add_0_r. apply Ptrofs.unsigned_range_2.
+Qed.
+
+Let valid_different_pointers_inj:
+  forall b1 ofs1 b2 ofs2 b1' delta1 b2' delta2,
+  b1 <> b2 ->
+  Mem.valid_pointer m1 b1 (Ptrofs.unsigned ofs1) = true ->
+  Mem.valid_pointer m1 b2 (Ptrofs.unsigned ofs2) = true ->
+  inject_id b1 = Some (b1', delta1) ->
+  inject_id b2 = Some (b2', delta2) ->
+  b1' <> b2' \/
+  Ptrofs.unsigned (Ptrofs.add ofs1 (Ptrofs.repr delta1)) <> Ptrofs.unsigned (Ptrofs.add ofs2 (Ptrofs.repr delta2)).
+Proof.
+  unfold inject_id; intros. left; congruence.
+Qed.
+
+Lemma needs_of_condition0_sound:
+  forall cond arg1 b arg2,
+  eval_condition0 cond arg1 m1 = Some b ->
+  vagree arg1 arg2 All ->
+  eval_condition0 cond arg2 m2 = Some b.
+Proof.
+  intros until arg2.
+  intros Hcond Hagree.
+  apply eval_condition0_inj with (f := inject_id) (m1 := m1) (v1 := arg1); simpl; auto.
+  apply val_inject_lessdef. apply lessdef_vagree. assumption.
+Qed.
+
 Lemma addl_sound:
   forall v1 w1 v2 w2 x,
   vagree v1 w1 (default x) -> vagree v2 w2 (default x) ->
@@ -185,6 +242,180 @@ Proof.
     inv H. inv H0.
     trivial.
 Qed.
+  
+Lemma select_sound:
+  forall cond v0 w0 v1 w1 v2 w2 x,
+    vagree v0 w0 (default x) ->
+    vagree v1 w1 (default x) ->
+    vagree v2 w2 (default x) ->
+    vagree (eval_select cond v0 v1 v2 m1) (eval_select cond w0 w1 w2 m2) x.
+Proof.
+  intros.
+  destruct x; simpl in *; trivial.
+  - rewrite eval_select_to2.
+    rewrite eval_select_to2.
+    unfold eval_select2.
+    assert (Hneedstrue := (needs_of_condition0_sound cond v2 true w2)).
+    assert (Hneedsfalse := (needs_of_condition0_sound cond v2 false w2)).
+    destruct (eval_condition0 cond v2 m1) in *; simpl in *; trivial.
+    destruct b.
+    + rewrite Hneedstrue; trivial.
+      inv H; trivial.
+      destruct w0; trivial.
+      inv H0; trivial.
+      destruct w1; trivial.
+      apply iagree_refl.
+    + rewrite Hneedsfalse; trivial.
+      inv H; trivial.
+      destruct w0; trivial.
+      inv H0; trivial.
+      destruct w1; trivial.
+      apply iagree_refl.
+  - rewrite eval_select_to2.
+    rewrite eval_select_to2.
+    unfold eval_select2.
+    assert (Hneedstrue := (needs_of_condition0_sound cond v2 true w2)).
+    assert (Hneedsfalse := (needs_of_condition0_sound cond v2 false w2)).
+    destruct (eval_condition0 cond v2 m1) in *; simpl in *; trivial.
+    destruct b.
+    + rewrite Hneedstrue; trivial.
+      inv H; trivial.
+      destruct w0; trivial.
+      inv H0; trivial.
+    + rewrite Hneedsfalse; trivial.
+      inv H; trivial.
+      destruct w0; trivial.
+      inv H0; trivial.
+Qed.
+
+Lemma selectl_sound:
+  forall cond v0 w0 v1 w1 v2 w2 x,
+    vagree v0 w0 (default x) ->
+    vagree v1 w1 (default x) ->
+    vagree v2 w2 (default x) ->
+    vagree (eval_selectl cond v0 v1 v2 m1) (eval_selectl cond w0 w1 w2 m2) x.
+Proof.
+  intros.
+  destruct x; simpl in *; trivial.
+  - rewrite eval_selectl_to2.
+    rewrite eval_selectl_to2.
+    unfold eval_selectl2.
+    assert (Hneedstrue := (needs_of_condition0_sound cond v2 true w2)).
+    assert (Hneedsfalse := (needs_of_condition0_sound cond v2 false w2)).
+    destruct (eval_condition0 cond v2 m1) in *; simpl in *; trivial.
+    destruct b.
+    + rewrite Hneedstrue; trivial.
+      inv H; trivial.
+      destruct w0; trivial.
+      inv H0; trivial.
+      destruct w1; trivial.
+    + rewrite Hneedsfalse; trivial.
+      inv H; trivial.
+      destruct w0; trivial.
+      inv H0; trivial.
+      destruct w1; trivial.
+  - rewrite eval_selectl_to2.
+    rewrite eval_selectl_to2.
+    unfold eval_selectl2.
+    assert (Hneedstrue := (needs_of_condition0_sound cond v2 true w2)).
+    assert (Hneedsfalse := (needs_of_condition0_sound cond v2 false w2)).
+    destruct (eval_condition0 cond v2 m1) in *; simpl in *; trivial.
+    destruct b.
+    + rewrite Hneedstrue; trivial.
+      inv H; trivial.
+      destruct w0; trivial.
+      inv H0; trivial.
+    + rewrite Hneedsfalse; trivial.
+      inv H; trivial.
+      destruct w0; trivial.
+      inv H0; trivial.
+Qed.
+
+Lemma selectf_sound:
+  forall cond v0 w0 v1 w1 v2 w2 x,
+    vagree v0 w0 (default x) ->
+    vagree v1 w1 (default x) ->
+    vagree v2 w2 (default x) ->
+    vagree (eval_selectf cond v0 v1 v2 m1) (eval_selectf cond w0 w1 w2 m2) x.
+Proof.
+  intros.
+  destruct x; simpl in *; trivial.
+  - rewrite eval_selectf_to2.
+    rewrite eval_selectf_to2.
+    unfold eval_selectf2.
+    assert (Hneedstrue := (needs_of_condition0_sound cond v2 true w2)).
+    assert (Hneedsfalse := (needs_of_condition0_sound cond v2 false w2)).
+    destruct (eval_condition0 cond v2 m1) in *; simpl in *; trivial.
+    destruct b.
+    + rewrite Hneedstrue; trivial.
+      inv H; trivial.
+      destruct w0; trivial.
+      inv H0; trivial.
+      destruct w1; trivial.
+    + rewrite Hneedsfalse; trivial.
+      inv H; trivial.
+      destruct w0; trivial.
+      inv H0; trivial.
+      destruct w1; trivial.
+  - rewrite eval_selectf_to2.
+    rewrite eval_selectf_to2.
+    unfold eval_selectf2.
+    assert (Hneedstrue := (needs_of_condition0_sound cond v2 true w2)).
+    assert (Hneedsfalse := (needs_of_condition0_sound cond v2 false w2)).
+    destruct (eval_condition0 cond v2 m1) in *; simpl in *; trivial.
+    destruct b.
+    + rewrite Hneedstrue; trivial.
+      inv H; trivial.
+      destruct w0; trivial.
+      inv H0; trivial.
+    + rewrite Hneedsfalse; trivial.
+      inv H; trivial.
+      destruct w0; trivial.
+      inv H0; trivial.
+Qed.
+
+Lemma selectfs_sound:
+  forall cond v0 w0 v1 w1 v2 w2 x,
+    vagree v0 w0 (default x) ->
+    vagree v1 w1 (default x) ->
+    vagree v2 w2 (default x) ->
+    vagree (eval_selectfs cond v0 v1 v2 m1) (eval_selectfs cond w0 w1 w2 m2) x.
+Proof.
+  intros.
+  destruct x; simpl in *; trivial.
+  - rewrite eval_selectfs_to2.
+    rewrite eval_selectfs_to2.
+    unfold eval_selectfs2.
+    assert (Hneedstrue := (needs_of_condition0_sound cond v2 true w2)).
+    assert (Hneedsfalse := (needs_of_condition0_sound cond v2 false w2)).
+    destruct (eval_condition0 cond v2 m1) in *; simpl in *; trivial.
+    destruct b.
+    + rewrite Hneedstrue; trivial.
+      inv H; trivial.
+      destruct w0; trivial.
+      inv H0; trivial.
+      destruct w1; trivial.
+    + rewrite Hneedsfalse; trivial.
+      inv H; trivial.
+      destruct w0; trivial.
+      inv H0; trivial.
+      destruct w1; trivial.
+  - rewrite eval_selectfs_to2.
+    rewrite eval_selectfs_to2.
+    unfold eval_selectfs2.
+    assert (Hneedstrue := (needs_of_condition0_sound cond v2 true w2)).
+    assert (Hneedsfalse := (needs_of_condition0_sound cond v2 false w2)).
+    destruct (eval_condition0 cond v2 m1) in *; simpl in *; trivial.
+    destruct b.
+    + rewrite Hneedstrue; trivial.
+      inv H; trivial.
+      destruct w0; trivial.
+      inv H0; trivial.
+    + rewrite Hneedsfalse; trivial.
+      inv H; trivial.
+      destruct w0; trivial.
+      inv H0; trivial.
+Qed.
 
 Remark default_idem: forall nv, default (default nv) = default nv.
 Proof.
@@ -193,11 +424,11 @@ Qed.
 
 Lemma needs_of_operation_sound:
   forall op args v nv args',
-  eval_operation ge (Vptr sp Ptrofs.zero) op args m = Some v ->
+  eval_operation ge (Vptr sp Ptrofs.zero) op args m1 = Some v ->
   vagree_list args args' (needs_of_operation op nv) ->
   nv <> Nothing ->
   exists v',
-     eval_operation ge (Vptr sp Ptrofs.zero) op args' m' = Some v'
+     eval_operation ge (Vptr sp Ptrofs.zero) op args' m2 = Some v'
   /\ vagree v v' nv.
 Proof.
   unfold needs_of_operation; intros; destruct op; try (eapply default_needs_of_operation_sound; eauto; fail);
@@ -238,12 +469,20 @@ Proof.
   apply mull_sound; trivial.
   rewrite default_idem; trivial.
   rewrite default_idem; trivial.
+  (* select *)
+- apply select_sound; trivial.
+  (* selectl *)
+- apply selectl_sound; trivial.
+  (* selectf *)
+- apply selectf_sound; trivial.
+  (* selectfs *)
+- apply selectfs_sound; trivial.
 Qed.
 
 Lemma operation_is_redundant_sound:
   forall op nv arg1 args v arg1' args',
   operation_is_redundant op nv = true ->
-  eval_operation ge (Vptr sp Ptrofs.zero) op (arg1 :: args) m = Some v ->
+  eval_operation ge (Vptr sp Ptrofs.zero) op (arg1 :: args) m1 = Some v ->
   vagree_list (arg1 :: args) (arg1' :: args') (needs_of_operation op nv) ->
   vagree v arg1' nv.
 Proof.
diff --git a/mppa_k1c/Op.v b/mppa_k1c/Op.v
index d533a504..14758bee 100644
--- a/mppa_k1c/Op.v
+++ b/mppa_k1c/Op.v
@@ -51,6 +51,18 @@ Inductive condition : Type :=
   | Ccompfs (c: comparison)     (**r 32-bit floating-point comparison *)
   | Cnotcompfs (c: comparison). (**r negation of a floating-point comparison *)
 
+Inductive condition0 : Type :=
+  | Ccomp0 (c: comparison) (**r signed integer comparison with 0 *)
+  | Ccompu0 (c: comparison) (**r unsigned integer comparison with 0 *)
+  | Ccompl0 (c: comparison) (**r signed 64-bit integer comparison with 0 *)
+  | Ccomplu0 (c: comparison). (**r unsigned 64-bit integer comparison with 0 *)
+
+Definition arg_type_of_condition0 (cond: condition0) :=
+  match cond with
+  | Ccomp0 _ | Ccompu0 _ => Tint
+  | Ccompl0 _ | Ccomplu0 _ => Tlong
+  end.
+
 (** Arithmetic and logical operations.  In the descriptions, [rd] is the
   result of the operation and [r1], [r2], etc, are the arguments. *)
 
@@ -181,7 +193,11 @@ Inductive operation : Type :=
   | Osingleoflong            (**r [rd = float32_of_signed_long(r1)] *)
   | Osingleoflongu           (**r [rd = float32_of_unsigned_int(r1)] *)
 (*c Boolean tests: *)
-  | Ocmp (cond: condition).  (**r [rd = 1] if condition holds, [rd = 0] otherwise. *)
+  | Ocmp (cond: condition)   (**r [rd = 1] if condition holds, [rd = 0] otherwise. *)
+  | Oselect (cond: condition0)    (**r [rd = if cond r3 then r2 else r1] *)
+  | Oselectl (cond: condition0)   (**r [rd = if cond r3 then r2 else r1] *)
+  | Oselectf (cond: condition0)   (**r [rd = if cond r3 then r2 else r1] *)
+  | Oselectfs (cond: condition0). (**r [rd = if cond r3 then r2 else r1] *)
 
 (** Addressing modes.  [r1], [r2], etc, are the arguments to the
   addressing. *)
@@ -201,6 +217,13 @@ Proof.
   decide equality.
 Defined.
 
+Definition eq_condition0 (x y: condition0) : {x=y} + {x<>y}.
+Proof.
+  generalize Int.eq_dec Int64.eq_dec; intro.
+  assert (forall (x y: comparison), {x=y}+{x<>y}). decide equality.
+  decide equality.
+Defined.
+
 Definition eq_addressing (x y: addressing) : {x=y} + {x<>y}.
 Proof.
   generalize ident_eq Ptrofs.eq_dec; intros.
@@ -209,7 +232,7 @@ 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; intros.
+  generalize Int.eq_dec Int64.eq_dec Ptrofs.eq_dec Float.eq_dec Float32.eq_dec ident_eq eq_condition eq_condition0; intros.
   decide equality.
 Defined.
 
@@ -233,7 +256,7 @@ Global Opaque eq_condition eq_addressing eq_operation.
   to lists of values.  Return [None] when the computation can trigger an
   error, e.g. integer division by zero.  [eval_condition] returns a boolean,
   [eval_operation] and [eval_addressing] return a value. *)
-
+ 
 Definition eval_condition (cond: condition) (vl: list val) (m: mem): option bool :=
   match cond, vl with
   | Ccomp c, v1 :: v2 :: nil => Val.cmp_bool c v1 v2
@@ -250,6 +273,98 @@ Definition eval_condition (cond: condition) (vl: list val) (m: mem): option bool
   | Cnotcompfs c, v1 :: v2 :: nil => option_map negb (Val.cmpfs_bool c v1 v2)
   | _, _ => None
   end.
+ 
+Definition eval_condition0 (cond: condition0) (v1: val) (m: mem): option bool :=
+  match cond with
+  | Ccomp0 c => Val.cmp_bool c v1 (Vint Int.zero)
+  | Ccompu0 c => Val.cmpu_bool (Mem.valid_pointer m) c v1 (Vint Int.zero)
+  | Ccompl0 c => Val.cmpl_bool c v1 (Vlong Int64.zero)
+  | Ccomplu0 c => Val.cmplu_bool (Mem.valid_pointer m) c v1 (Vlong Int64.zero)
+  end.
+
+Definition eval_select (cond : condition0) (v0 : val) (v1 : val) (vselect : val) (m: mem) : val :=
+  match v0, v1, (eval_condition0 cond vselect m) with
+    | Vint i0, Vint i1, Some bval => Vint (if bval then i1 else i0)
+    | _,_,_ => Vundef
+  end.
+
+Definition eval_select2 (cond : condition0) (v0 : val) (v1 : val) (vselect : val) (m: mem) : val :=
+  match (eval_condition0 cond vselect m), v0, v1 with
+    | Some bval, Vint i0, Vint i1 => Vint (if bval then i1 else i0)
+    | _,_,_ => Vundef
+  end.
+
+Lemma eval_select_to2: forall cond v0 v1 vselect m,
+    (eval_select cond v0 v1 vselect m) =
+    (eval_select2 cond v0 v1 vselect m).
+Proof.
+  intros.
+  unfold eval_select2.
+  destruct v0; destruct v1; simpl; destruct (eval_condition0 cond vselect m); simpl; reflexivity.
+Qed.
+
+Definition eval_selectl (cond: condition0) (v0 : val) (v1 : val) (vselect : val) (m: mem) : val :=
+  match v0, v1, (eval_condition0 cond vselect m) with
+    | Vlong i0, Vlong i1, Some bval => Vlong (if bval then i1 else i0)
+    | _,_,_ => Vundef
+  end.
+
+Definition eval_selectl2 (cond : condition0) (v0 : val) (v1 : val) (vselect : val) (m: mem) : val :=
+  match (eval_condition0 cond vselect m), v0, v1 with
+    | Some bval, Vlong i0, Vlong i1 => Vlong (if bval then i1 else i0)
+    | _,_,_ => Vundef
+  end.
+
+Lemma eval_selectl_to2: forall cond v0 v1 vselect m,
+    (eval_selectl cond v0 v1 vselect m) =
+    (eval_selectl2 cond v0 v1 vselect m).
+Proof.
+  intros.
+  unfold eval_selectl2.
+  destruct v0; destruct v1; simpl; destruct (eval_condition0 cond vselect m); simpl; reflexivity.
+Qed.
+
+Definition eval_selectf (cond: condition0) (v0 : val) (v1 : val) (vselect : val) (m: mem) : val :=
+  match v0, v1, (eval_condition0 cond vselect m) with
+    | Vfloat i0, Vfloat i1, Some bval => Vfloat (if bval then i1 else i0)
+    | _,_,_ => Vundef
+  end.
+
+Definition eval_selectf2 (cond : condition0) (v0 : val) (v1 : val) (vselect : val) (m: mem) : val :=
+  match (eval_condition0 cond vselect m), v0, v1 with
+    | Some bval, Vfloat i0, Vfloat i1 => Vfloat (if bval then i1 else i0)
+    | _,_,_ => Vundef
+  end.
+
+Lemma eval_selectf_to2: forall cond v0 v1 vselect m,
+    (eval_selectf cond v0 v1 vselect m) =
+    (eval_selectf2 cond v0 v1 vselect m).
+Proof.
+  intros.
+  unfold eval_selectf2.
+  destruct v0; destruct v1; simpl; destruct (eval_condition0 cond vselect m); simpl; reflexivity.
+Qed.
+
+Definition eval_selectfs (cond: condition0) (v0 : val) (v1 : val) (vselect : val) (m: mem) : val :=
+  match v0, v1, (eval_condition0 cond vselect m) with
+    | Vsingle i0, Vsingle i1, Some bval => Vsingle (if bval then i1 else i0)
+    | _,_,_ => Vundef
+  end.
+
+Definition eval_selectfs2 (cond : condition0) (v0 : val) (v1 : val) (vselect : val) (m: mem) : val :=
+  match (eval_condition0 cond vselect m), v0, v1 with
+    | Some bval, Vsingle i0, Vsingle i1 => Vsingle (if bval then i1 else i0)
+    | _,_,_ => Vundef
+  end.
+
+Lemma eval_selectfs_to2: forall cond v0 v1 vselect m,
+    (eval_selectfs cond v0 v1 vselect m) =
+    (eval_selectfs2 cond v0 v1 vselect m).
+Proof.
+  intros.
+  unfold eval_selectfs2.
+  destruct v0; destruct v1; simpl; destruct (eval_condition0 cond vselect m); simpl; reflexivity.
+Qed.
 
 Definition eval_operation
     (F V: Type) (genv: Genv.t F V) (sp: val)
@@ -379,6 +494,10 @@ Definition eval_operation
   | Osingleoflong, v1::nil => Val.singleoflong v1
   | Osingleoflongu, v1::nil => Val.singleoflongu v1
   | Ocmp c, _ => Some (Val.of_optbool (eval_condition c vl m))
+  | (Oselect cond), v0::v1::vselect::nil => Some (eval_select cond v0 v1 vselect m)
+  | (Oselectl cond), v0::v1::vselect::nil => Some (eval_selectl cond v0 v1 vselect m)
+  | (Oselectf cond), v0::v1::vselect::nil => Some (eval_selectf cond v0 v1 vselect m)
+  | (Oselectfs cond), v0::v1::vselect::nil => Some (eval_selectfs cond v0 v1 vselect m)
   | _, _ => None
   end.
 
@@ -567,6 +686,11 @@ Definition type_of_operation (op: operation) : list typ * typ :=
   | Osingleoflong => (Tlong :: nil, Tsingle)
   | Osingleoflongu => (Tlong :: nil, Tsingle)
   | Ocmp c => (type_of_condition c, Tint)
+                
+  | Oselect cond => (Tint :: Tint :: (arg_type_of_condition0 cond) :: nil, Tint)
+  | Oselectl cond => (Tlong :: Tlong :: (arg_type_of_condition0 cond) :: nil, Tlong)
+  | Oselectf cond => (Tfloat :: Tfloat :: (arg_type_of_condition0 cond) :: nil, Tfloat)
+  | Oselectfs cond => (Tsingle :: Tsingle ::  (arg_type_of_condition0 cond) :: nil, Tsingle)
   end.
 
 Definition type_of_addressing (addr: addressing) : list typ :=
@@ -802,6 +926,43 @@ Proof with (try exact I; try reflexivity; auto using Val.Vptr_has_type).
   - destruct v0; simpl in H0; inv H0...
   (* cmp *)
   - destruct (eval_condition cond vl m)... destruct b...
+  (* select *)
+  - destruct v0; destruct v1; simpl in *; try discriminate; trivial.
+    destruct cond; destruct v2; simpl in *; trivial.
+    + destruct Archi.ptr64; simpl; trivial.
+      destruct (_ && _); simpl; trivial.
+      destruct (Val.cmp_different_blocks _); simpl; trivial.
+    + destruct Archi.ptr64; simpl; trivial.
+      destruct (_ && _); simpl; trivial.
+      destruct (Val.cmp_different_blocks _); simpl; trivial.
+  (* selectl *)
+  - destruct v0; destruct v1; simpl in *; try discriminate; trivial.
+    destruct cond; destruct v2; simpl in *; trivial.
+    + destruct Archi.ptr64; simpl; trivial.
+      destruct (_ && _); simpl; trivial.
+      destruct (Val.cmp_different_blocks _); simpl; trivial.
+    + destruct Archi.ptr64; simpl; trivial.
+      destruct (_ && _); simpl; trivial.
+      destruct (Val.cmp_different_blocks _); simpl; trivial.
+
+  (* selectf *)
+  - destruct v0; destruct v1; simpl in *; try discriminate; trivial.
+    destruct cond; destruct v2; simpl in *; trivial.
+    + destruct Archi.ptr64; simpl; trivial.
+      destruct (_ && _); simpl; trivial.
+      destruct (Val.cmp_different_blocks _); simpl; trivial.
+    + destruct Archi.ptr64; simpl; trivial.
+      destruct (_ && _); simpl; trivial.
+      destruct (Val.cmp_different_blocks _); simpl; trivial.
+  (* selectfs *)
+  - destruct v0; destruct v1; simpl in *; try discriminate; trivial.
+    destruct cond; destruct v2; simpl in *; trivial.
+    + destruct Archi.ptr64; simpl; trivial.
+      destruct (_ && _); simpl; trivial.
+      destruct (Val.cmp_different_blocks _); simpl; trivial.
+    + destruct Archi.ptr64; simpl; trivial.
+      destruct (_ && _); simpl; trivial.
+      destruct (Val.cmp_different_blocks _); simpl; trivial.
 Qed.
 
 End SOUNDNESS.
@@ -962,6 +1123,19 @@ Definition op_depends_on_memory (op: operation) : bool :=
   | Ocmp (Ccompuimm _ _) => negb Archi.ptr64
   | Ocmp (Ccomplu _) => Archi.ptr64
   | Ocmp (Ccompluimm _ _) => Archi.ptr64
+
+  | Oselect (Ccompu0 _) => negb Archi.ptr64
+  | Oselect (Ccomplu0 _) => Archi.ptr64
+
+  | Oselectl (Ccompu0 _) => negb Archi.ptr64
+  | Oselectl (Ccomplu0 _) => Archi.ptr64
+
+  | Oselectf (Ccompu0 _) => negb Archi.ptr64
+  | Oselectf (Ccomplu0 _) => Archi.ptr64
+
+  | Oselectfs (Ccompu0 _) => negb Archi.ptr64
+  | Oselectfs (Ccomplu0 _) => Archi.ptr64
+                                
   | _ => false
   end.
 
@@ -970,9 +1144,10 @@ Lemma op_depends_on_memory_correct:
   op_depends_on_memory op = false ->
   eval_operation ge sp op args m1 = eval_operation ge sp op args m2.
 Proof.
-  intros until m2. destruct op; simpl; try congruence.
+  intros until m2. destruct op; simpl; try congruence;
+                     
   destruct cond; simpl; intros SF; auto; rewrite ? negb_false_iff in SF;
-  unfold Val.cmpu_bool, Val.cmplu_bool; rewrite SF; reflexivity.
+  unfold eval_select, eval_selectl, eval_selectf, eval_selectfs, eval_condition0, Val.cmpu_bool, Val.cmplu_bool; rewrite SF; reflexivity.
 Qed.
 
 (** Global variables mentioned in an operation or addressing mode *)
@@ -1100,6 +1275,19 @@ Proof.
 - inv H3; inv H2; simpl in H0; inv H0; auto.
 Qed.
 
+Lemma eval_condition0_inj:
+  forall cond v1 v2 b,
+  Val.inject f v1 v2 ->
+  eval_condition0 cond v1 m1 = Some b ->
+  eval_condition0 cond v2 m2 = Some b.
+Proof.
+  intros. destruct cond; simpl in H0; FuncInv; InvInject; simpl; auto.
+  - inv H; simpl in *; congruence.
+  - eauto 3 using Val.cmpu_bool_inject, Mem.valid_pointer_implies.
+  - inv H; simpl in *; congruence.
+  - eauto 3 using Val.cmplu_bool_inject, Mem.valid_pointer_implies.
+Qed.
+
 Ltac TrivialExists :=
   match goal with
   | [ |- exists v2, Some ?v1 = Some v2 /\ Val.inject _ _ v2 ] =>
@@ -1328,6 +1516,62 @@ Proof.
     exploit eval_condition_inj; eauto. intros EQ; rewrite EQ.
     destruct b; simpl; constructor.
     simpl; constructor.
+  (* select *)
+  - unfold eval_select.
+    inv H4; trivial.
+    inv H2; trivial.
+    inv H3; trivial;
+      try (destruct cond; simpl; trivial; fail).
+    destruct (eval_condition0 cond (Vptr _ _) m1) eqn:Hcond; trivial.
+    eassert (Hcond' : ((eval_condition0 cond (Vptr b2 (Ptrofs.add ofs1 (Ptrofs.repr delta)))) m2) = Some b).
+    * eapply eval_condition0_inj.
+      eapply Val.inject_ptr.
+      eassumption.
+      reflexivity.
+      assumption.
+    * rewrite Hcond'. constructor.
+  (* selectl *)
+  - unfold eval_selectl.
+    inv H4; trivial.
+    inv H2; trivial.
+    inv H3; trivial;
+      try (destruct cond; simpl; trivial; fail).
+    destruct (eval_condition0 cond (Vptr _ _) m1) eqn:Hcond; trivial.
+    eassert (Hcond' : ((eval_condition0 cond (Vptr b2 (Ptrofs.add ofs1 (Ptrofs.repr delta)))) m2) = Some b).
+    * eapply eval_condition0_inj.
+      eapply Val.inject_ptr.
+      eassumption.
+      reflexivity.
+      assumption.
+    * rewrite Hcond'. constructor.
+  (* selectf *)
+  - unfold eval_selectf.
+    inv H4; trivial.
+    inv H2; trivial.
+    inv H3; trivial;
+      try (destruct cond; simpl; trivial; fail).
+    destruct (eval_condition0 cond (Vptr _ _) m1) eqn:Hcond; trivial.
+    eassert (Hcond' : ((eval_condition0 cond (Vptr b2 (Ptrofs.add ofs1 (Ptrofs.repr delta)))) m2) = Some b).
+    * eapply eval_condition0_inj.
+      eapply Val.inject_ptr.
+      eassumption.
+      reflexivity.
+      assumption.
+    * rewrite Hcond'. constructor.
+  (* selectfs *)
+  - unfold eval_selectfs.
+    inv H4; trivial.
+    inv H2; trivial.
+    inv H3; trivial;
+      try (destruct cond; simpl; trivial; fail).
+    destruct (eval_condition0 cond (Vptr _ _) m1) eqn:Hcond; trivial.
+    eassert (Hcond' : ((eval_condition0 cond (Vptr b2 (Ptrofs.add ofs1 (Ptrofs.repr delta)))) m2) = Some b).
+    * eapply eval_condition0_inj.
+      eapply Val.inject_ptr.
+      eassumption.
+      reflexivity.
+      assumption.
+    * rewrite Hcond'. constructor.
 Qed.
 
 Lemma eval_addressing_inj:
diff --git a/mppa_k1c/PostpassSchedulingOracle.ml b/mppa_k1c/PostpassSchedulingOracle.ml
index 8c68deea..9a26425a 100644
--- a/mppa_k1c/PostpassSchedulingOracle.ml
+++ b/mppa_k1c/PostpassSchedulingOracle.ml
@@ -129,6 +129,8 @@ let arith_rri64_str = function
 let arith_arrr_str = function
   | Pmaddw -> "Pmaddw"
   | Pmaddl -> "Pmaddl"
+  | Pcmove _ -> "Pcmove"
+  | Pcmoveu _ -> "Pcmoveu"
             
 let arith_ri32_str = "Pmake"
 
@@ -421,7 +423,7 @@ type real_instruction =
   | Addw | Andw | Compw | Mulw | Orw | Sbfw | Sraw | Srlw | Sllw | Rorw | Xorw
   | Addd | Andd | Compd | Muld | Ord | Sbfd | Srad | Srld | Slld | Xord
   | Nandw | Norw | Nxorw | Nandd | Nord | Nxord | Andnw | Ornw | Andnd | Ornd
-  | Maddw | Maddd
+  | Maddw | Maddd | Cmoved
   | Make | Nop  | Sxwd  | Zxwd
   (* LSU *)
   | Lbs | Lbz | Lhs | Lhz | Lws | Ld
@@ -488,7 +490,8 @@ let ab_inst_to_real = function
   | "Pfixedudrzz" -> Fixedudz
   | "Pfixeddrzz_i32" -> Fixeddz
   | "Pfixedudrzz_i32" -> Fixedudz
-
+  | "Pcmove" | "Pcmoveu" -> Cmoved
+  
   | "Plb" -> Lbs
   | "Plbu" -> Lbz
   | "Plh" -> Lhs
@@ -537,7 +540,7 @@ let rec_to_usage r =
                           | Some U27L5 | Some U27L10 -> alu_tiny_x
                           | _ -> raise InvalidEncoding)
   | Addd | Andd | Nandd | Ord | Nord | Sbfd | Xord
-  | Nxord | Andnd | Ornd -> 
+  | Nxord | Andnd | Ornd | Cmoved -> 
       (match encoding with None | Some U6 | Some S10 -> alu_tiny 
                           | Some U27L5 | Some U27L10 -> alu_tiny_x
                           | Some E27U27L10 -> alu_tiny_y)
@@ -590,7 +593,7 @@ let real_inst_to_latency = function
   | Rorw | Nandw | Norw | Nxorw | Ornw | Andnw
   | Nandd | Nord | Nxord | Ornd | Andnd
   | Addd | Andd | Compd | Ord | Sbfd | Srad | Srld | Slld | Xord | Make
-  | Sxwd | Zxwd | Fcompw | Fcompd
+  | Sxwd | Zxwd | Fcompw | Fcompd | Cmoved
         -> 1
   | Floatwz | Floatuwz | Fixeduwz | Fixedwz | Floatdz | Floatudz | Fixeddz | Fixedudz -> 4
   | Mulw | Muld | Maddw | Maddd -> 2 (* FIXME - WORST CASE. If it's S10 then it's only 1 *)
diff --git a/mppa_k1c/SelectLong.vp b/mppa_k1c/SelectLong.vp
index 31112dca..f7cb3c82 100644
--- a/mppa_k1c/SelectLong.vp
+++ b/mppa_k1c/SelectLong.vp
@@ -258,9 +258,17 @@ Nondetfunction andl (e1: expr) (e2: expr) :=
   | Eop (Olongconst n1) Enil, t2 => andlimm n1 t2
   | t1, Eop (Olongconst n2) Enil => andlimm n2 t1
   | (Eop Onotl (t1:::Enil)), t2 => Eop Oandnl (t1:::t2:::Enil) 
-  | t1, (Eop Onotl (t2:::Enil)) => Eop Oandnl (t2:::t1:::Enil) 
+  | t1, (Eop Onotl (t2:::Enil)) => Eop Oandnl (t2:::t1:::Enil)
   | _, _ => Eop Oandl (e1:::e2:::Enil)
   end.
+(*
+  | (Eop Ocast32signed
+         ((Eop Oneg ((Eop (Ocmp (Ccomplimm Cne zero1))
+        (y1:::Enil)):::Enil)):::Enil)), v1 =>
+     	if Int64.eq zero1 Int64.zero                 
+	then Eop Oselectl ((Eop (Olongconst Int64.zero) Enil):::v1:::y1:::Enil)
+	else Eop Oandl (e1:::e2:::Enil)
+*)
 
 Nondetfunction orlimm (n1: int64) (e2: expr) :=
   if Int64.eq n1 Int64.zero then e2 else
@@ -277,7 +285,18 @@ Nondetfunction orl (e1: expr) (e2: expr) :=
   | Eop (Olongconst n1) Enil, t2 => orlimm n1 t2
   | t1, Eop (Olongconst n2) Enil => orlimm n2 t1
   | (Eop Onotl (t1:::Enil)), t2 => Eop Oornl (t1:::t2:::Enil) 
-  | t1, (Eop Onotl (t2:::Enil))  => Eop Oornl (t2:::t1:::Enil) 
+  | t1, (Eop Onotl (t2:::Enil))  => Eop Oornl (t2:::t1:::Enil)
+  |  (Eop Oandl ((Eop Ocast32signed
+         ((Eop Oneg ((Eop (Ocmp (Ccomplimm Ceq zero0))
+        (y0:::Enil)):::Enil)):::Enil)):::v0:::Enil)),
+     (Eop Oandl ((Eop Ocast32signed
+         ((Eop Oneg ((Eop (Ocmp (Ccomplimm Cne zero1))
+        (y1:::Enil)):::Enil)):::Enil)):::v1:::Enil)) =>
+     if same_expr_pure y0 y1
+     && Int64.eq zero0 Int64.zero
+     && Int64.eq zero1 Int64.zero                 
+     then Eop (Oselectl (Ccompl0 Cne)) (v0:::v1:::y0:::Enil)
+     else Eop Oorl (e1:::e2:::Enil)
   | _, _ => Eop Oorl (e1:::e2:::Enil)
   end.
 
diff --git a/mppa_k1c/SelectLongproof.v b/mppa_k1c/SelectLongproof.v
index 51b989d6..3fab35b3 100644
--- a/mppa_k1c/SelectLongproof.v
+++ b/mppa_k1c/SelectLongproof.v
@@ -390,6 +390,15 @@ Proof.
 - TrivialExists.
 Qed.
 
+Lemma int64_eq_commut: forall x y : int64,
+    (Int64.eq x y) = (Int64.eq y x).
+Proof.
+  intros.
+  predSpec Int64.eq Int64.eq_spec x y;
+    predSpec Int64.eq Int64.eq_spec y x;
+    congruence.
+Qed.
+
 Theorem eval_andl: binary_constructor_sound andl Val.andl.
 Proof.
   unfold andl; destruct Archi.splitlong. apply SplitLongproof.eval_andl.
@@ -398,6 +407,25 @@ Proof.
 - InvEval. apply eval_andlimm; auto.
 - (*andn*) InvEval. TrivialExists. simpl. congruence.
 - (*andn reverse*) InvEval. rewrite Val.andl_commut. TrivialExists; simpl. congruence.
+  (*
+- (* selectl *)
+  InvEval.
+  predSpec Int64.eq Int64.eq_spec zero1 Int64.zero; simpl; TrivialExists.
+  + constructor. econstructor; constructor.
+  constructor; try constructor; try constructor; try eassumption.
+  + simpl in *. f_equal. inv H6.
+    unfold selectl.
+    simpl.
+    destruct v3; simpl; trivial.
+    rewrite int64_eq_commut.
+    destruct (Int64.eq i Int64.zero); simpl.
+    * replace (Int64.repr (Int.signed (Int.neg Int.zero))) with Int64.zero by Int64.bit_solve.
+      destruct y; simpl; trivial.
+    * replace (Int64.repr (Int.signed (Int.neg Int.one))) with Int64.mone by Int64.bit_solve.
+      destruct y; simpl; trivial.
+      rewrite Int64.and_commut. rewrite Int64.and_mone. reflexivity.
+  + constructor. econstructor. constructor. econstructor. constructor. econstructor. constructor. eassumption. constructor. simpl. f_equal. constructor. simpl. f_equal. constructor. simpl. f_equal. constructor. eassumption. constructor.
+  + simpl in *. congruence. *)
 - TrivialExists.
 Qed.
 
@@ -414,6 +442,7 @@ Proof.
 - TrivialExists.
 Qed.
 
+
 Theorem eval_orl: binary_constructor_sound orl Val.orl.
 Proof.
   unfold orl; destruct Archi.splitlong. apply SplitLongproof.eval_orl.
@@ -423,6 +452,81 @@ Proof.
 - InvEval. apply eval_orlimm; auto.
 - (*orn*) InvEval. TrivialExists; simpl; congruence.
 - (*orn reversed*) InvEval. rewrite Val.orl_commut. TrivialExists; simpl; congruence.
+  - (* selectl *)
+    destruct (same_expr_pure y0 y1) eqn:PURE; simpl; try TrivialExists.
+    predSpec Int64.eq Int64.eq_spec zero0 Int64.zero; simpl; try TrivialExists.
+    predSpec Int64.eq Int64.eq_spec zero1 Int64.zero; simpl; [ | TrivialExists].
+    inv H.
+    inv H0.
+    inv H6.
+    inv H3.
+    inv H2.
+    inv H7.
+    inv H4.
+    inv H3.
+    inv H6.
+    inv H4.
+    inv H3.
+    inv H14.
+    inv H13.
+    inv H6.
+    inv H4.
+    inv H13.
+    inv H14.
+    inv H9.
+    inv H11.
+    inv H13.
+    inv H3.
+    inv H6.
+    inv H7.
+    inv H3.
+    inv H14.
+    inv H17.
+    simpl in *.
+    inv H8.
+    inv H5.
+    inv H10.
+    inv H12.
+    inv H15.
+    inv H16.
+    inv H11.
+    inv H13.
+    unfold same_expr_pure in PURE.
+    destruct y0; try congruence.
+    destruct y1; try congruence.
+    destruct (ident_eq i i0); try congruence; clear PURE.
+    rewrite <- e0 in *; clear e0.
+    inv H6.
+    inv H7.
+    rename v10 into vtest.
+    replace v11 with vtest in * by congruence.
+    TrivialExists.
+    simpl.
+    f_equal.
+    rewrite eval_selectl_to2.
+    unfold eval_selectl2.
+    destruct vtest; simpl; trivial.
+    rewrite Val.andl_commut.
+    destruct v4; simpl; trivial.
+    rewrite Val.andl_commut.
+    rewrite Val.orl_commut.
+    destruct v9; simpl; trivial.
+    rewrite int64_eq_commut.
+    destruct (Int64.eq Int64.zero i1); simpl.
+    
+    + replace (Int64.repr (Int.signed (Int.neg Int.one))) with Int64.mone by Int64.bit_solve.
+      replace (Int64.repr (Int.signed (Int.neg Int.zero))) with Int64.zero by Int64.bit_solve.
+      rewrite Int64.and_mone.
+      rewrite Int64.and_zero.
+      rewrite Int64.or_commut.
+      rewrite Int64.or_zero.
+      reflexivity.
+   + replace (Int64.repr (Int.signed (Int.neg Int.one))) with Int64.mone by Int64.bit_solve.
+      replace (Int64.repr (Int.signed (Int.neg Int.zero))) with Int64.zero by Int64.bit_solve.
+      rewrite Int64.and_mone.
+      rewrite Int64.and_zero.
+      rewrite Int64.or_zero.
+      reflexivity.
 - TrivialExists.
 Qed.
 
diff --git a/mppa_k1c/SelectOp.vp b/mppa_k1c/SelectOp.vp
index d82fe238..71e0eff3 100644
--- a/mppa_k1c/SelectOp.vp
+++ b/mppa_k1c/SelectOp.vp
@@ -61,6 +61,35 @@ Section SELECT.
 
 Context {hf: helper_functions}.
 
+(** Ternary operator *)
+Definition select_base o0 o1 oselect :=
+ Eop (Oselect (Ccomp0 Cne))
+              (o0:::o1:::oselect:::Enil).
+				      
+Definition select o0 o1 oselect :=
+  select_base o0 o1 oselect.
+				      
+Definition selectl_base o0 o1 oselect :=
+ Eop (Oselectl (Ccomp0 Cne))
+              (o0:::o1:::oselect:::Enil).
+				      
+Definition selectl o0 o1 oselect :=
+  selectl_base o0 o1 oselect.
+				      
+Definition selectf_base o0 o1 oselect :=
+ Eop (Oselectf (Ccomp0 Cne))
+              (o0:::o1:::oselect:::Enil).
+				      
+Definition selectf o0 o1 oselect :=
+  selectf_base o0 o1 oselect.
+				      
+Definition selectfs_base o0 o1 oselect :=
+ Eop (Oselectfs (Ccomp0 Cne))
+              (o0:::o1:::oselect:::Enil).
+				      
+Definition selectfs o0 o1 oselect :=
+  selectfs_base o0 o1 oselect.
+				      
 (** ** Constants **)
 
 Definition addrsymbol (id: ident) (ofs: ptrofs) :=
@@ -275,7 +304,25 @@ Nondetfunction or (e1: expr) (e2: expr) :=
       then Eop (Ororimm n2) (t1:::Enil)
       else Eop Oor (e1:::e2:::Enil)
   | (Eop Onot (t1:::Enil)), t2 => Eop Oorn (t1:::t2:::Enil) 
-  | t1, (Eop Onot (t2:::Enil))  => Eop Oorn (t2:::t1:::Enil) 
+  | t1, (Eop Onot (t2:::Enil))  => Eop Oorn (t2:::t1:::Enil)
+  |  (Eop Oand ((Eop Oneg ((Eop (Ocmp (Ccompimm Ceq zero0))
+        (y0:::Enil)):::Enil)):::v0:::Enil)),
+     (Eop Oand ((Eop Oneg ((Eop (Ocmp (Ccompimm Cne zero1))
+        (y1:::Enil)):::Enil)):::v1:::Enil)) =>
+     if same_expr_pure y0 y1
+     && Int.eq zero0 Int.zero
+     && Int.eq zero1 Int.zero                 
+     then select_base v0 v1 y0
+     else Eop Oor (e1:::e2:::Enil)
+  |  (Eop Oand ((Eop Oneg ((Eop (Ocmp (Ccompuimm Ceq zero0))
+        (y0:::Enil)):::Enil)):::v0:::Enil)),
+     (Eop Oand ((Eop Oneg ((Eop (Ocmp (Ccompuimm Cne zero1))
+        (y1:::Enil)):::Enil)):::v1:::Enil)) =>
+     if same_expr_pure y0 y1
+     && Int.eq zero0 Int.zero
+     && Int.eq zero1 Int.zero                 
+     then select_base v0 v1 y0
+     else Eop Oor (e1:::e2:::Enil)
   | _, _ => Eop Oor (e1:::e2:::Enil)
   end.
 
diff --git a/mppa_k1c/SelectOpproof.v b/mppa_k1c/SelectOpproof.v
index d426e4f1..4af5ccfa 100644
--- a/mppa_k1c/SelectOpproof.v
+++ b/mppa_k1c/SelectOpproof.v
@@ -92,7 +92,7 @@ Let ge := Genv.globalenv prog.
 Variable sp: val.
 Variable e: env.
 Variable m: mem.
-
+  
 (* Helper lemmas - from SplitLongproof.v *)
 
 Ltac UseHelper := decompose [Logic.and] arith_helpers_correct; eauto.
@@ -162,7 +162,7 @@ Definition binary_constructor_sound (cstr: expr -> expr -> expr) (sem: val -> va
   eval_expr ge sp e m le a x ->
   eval_expr ge sp e m le b y ->
   exists v, eval_expr ge sp e m le (cstr a b) v /\ Val.lessdef (sem x y) v.
-
+       
 Theorem eval_addrsymbol:
   forall le id ofs,
   exists v, eval_expr ge sp e m le (addrsymbol id ofs) v /\ Val.lessdef (Genv.symbol_address ge id ofs) v.
@@ -526,6 +526,15 @@ Proof.
   discriminate.
 Qed.
 
+Lemma int_eq_commut: forall x y : int,
+    (Int.eq x y) = (Int.eq y x).
+Proof.
+  intros.
+  predSpec Int.eq Int.eq_spec x y;
+    predSpec Int.eq Int.eq_spec y x;
+    congruence.
+Qed.
+
 Theorem eval_or: binary_constructor_sound or Val.or.
 Proof.
   unfold or; red; intros.
@@ -553,6 +562,83 @@ Proof.
     exists (Val.ror v1 (Vint n2)); split. EvalOp. rewrite Val.or_commut. apply ROR; auto.
   - (*orn*) TrivialExists; simpl; congruence.
   - (*orn reversed*) rewrite Val.or_commut. TrivialExists; simpl; congruence.
+  - (* select *)
+    destruct (same_expr_pure y0 y1) eqn:PURE; simpl; try exact DEFAULT.
+    predSpec Int.eq Int.eq_spec zero0 Int.zero; simpl; try exact DEFAULT.
+    predSpec Int.eq Int.eq_spec zero1 Int.zero; simpl; try exact DEFAULT.
+    TrivialExists.
+    simpl in *.
+    unfold eval_select.
+    f_equal.
+    inv H6.
+    inv H7.
+    inv H9.
+    inv H11.
+    unfold same_expr_pure in PURE.
+    destruct y0; try congruence.
+    destruct y1; try congruence.
+    destruct (ident_eq i i0); try congruence.
+    rewrite <- e0 in *. clear e0. clear PURE.
+    inv H2. inv H5.
+    replace v8 with v4 in * by congruence.
+    rename v4 into vselect.
+    destruct vselect; simpl; trivial;
+    destruct v5; simpl; trivial; destruct v9; simpl; trivial;
+    destruct (Int.eq i1 Int.zero); simpl; trivial.
+    + rewrite Int.neg_zero.
+      rewrite Int.and_commut.
+      rewrite Int.and_mone.
+      rewrite Int.and_commut.
+      rewrite Int.and_zero.
+      rewrite Int.or_zero.
+      reflexivity.
+    + rewrite Int.neg_zero.
+      rewrite Int.and_commut.
+      rewrite Int.and_zero.
+      rewrite Int.and_commut.
+      rewrite Int.and_mone.
+      rewrite Int.or_commut.
+      rewrite Int.or_zero.
+      reflexivity.
+  - (* select unsigned *)
+    destruct (same_expr_pure y0 y1) eqn:PURE; simpl; try exact DEFAULT.
+    predSpec Int.eq Int.eq_spec zero0 Int.zero; simpl; try exact DEFAULT.
+    predSpec Int.eq Int.eq_spec zero1 Int.zero; simpl; try exact DEFAULT.
+    TrivialExists.
+    simpl in *.
+    unfold eval_select.
+    f_equal.
+    inv H6.
+    inv H7.
+    inv H9.
+    inv H11.
+    unfold same_expr_pure in PURE.
+    destruct y0; try congruence.
+    destruct y1; try congruence.
+    destruct (ident_eq i i0); try congruence.
+    rewrite <- e0 in *. clear e0. clear PURE.
+    inv H2. inv H5.
+    replace v8 with v4 in * by congruence.
+    rename v4 into vselect.
+    destruct vselect; simpl; trivial;
+    destruct v5; simpl; trivial;
+    destruct v9; simpl; trivial;
+    destruct (Int.eq i1 Int.zero); simpl; trivial.
+    + rewrite Int.neg_zero.
+      rewrite Int.and_commut.
+      rewrite Int.and_mone.
+      rewrite Int.and_commut.
+      rewrite Int.and_zero.
+      rewrite Int.or_zero.
+      reflexivity.
+    + rewrite Int.neg_zero.
+      rewrite Int.and_commut.
+      rewrite Int.and_zero.
+      rewrite Int.and_commut.
+      rewrite Int.and_mone.
+      rewrite Int.or_commut.
+      rewrite Int.or_zero.
+      reflexivity.
   - apply DEFAULT.
 Qed.
 
diff --git a/mppa_k1c/TargetPrinter.ml b/mppa_k1c/TargetPrinter.ml
index 90ef6a4d..3aa6b319 100644
--- a/mppa_k1c/TargetPrinter.ml
+++ b/mppa_k1c/TargetPrinter.ml
@@ -529,6 +529,10 @@ module Target (*: TARGET*) =
       | Pmaddil (rd, rs, imm) ->
          fprintf oc "	maddd	%a = %a, %a\n" ireg rd ireg rs coqint64 imm
 
+      | Pcmove (bt, rd, rcond, rs) | Pcmoveu (bt, rd, rcond, rs) ->
+         fprintf oc "	cmoved.%a %a? %a = %a\n"
+           bcond bt ireg rcond ireg rd ireg rs
+        
     let get_section_names name =
       let (text, lit) =
         match C2C.atom_sections name with
diff --git a/mppa_k1c/ValueAOp.v b/mppa_k1c/ValueAOp.v
index a54dbd8f..f17bd765 100644
--- a/mppa_k1c/ValueAOp.v
+++ b/mppa_k1c/ValueAOp.v
@@ -42,6 +42,38 @@ Definition eval_static_addressing (addr: addressing) (vl: list aval): aval :=
   | _, _ => Vbot
   end.
 
+Definition eval_static_condition0 (cond : condition0) (v : aval) : abool :=
+  match cond with
+  | Ccomp0 c => cmp_bool c v (I Int.zero)
+  | Ccompu0 c => cmpu_bool c v (I Int.zero)
+  | Ccompl0  c => cmpl_bool c v (L Int64.zero)
+  | Ccomplu0 c => cmplu_bool c v (L Int64.zero)
+  end.
+  
+Definition eval_static_select (cond : condition0) (v0 v1 vselect : aval) : aval :=
+  match eval_static_condition0 cond vselect with
+  | Just b => binop_int (fun x0 x1 => if b then x1 else x0) v0 v1
+  | _ => Vtop
+  end.
+
+Definition eval_static_selectl (cond : condition0) (v0 v1 vselect : aval) : aval :=
+  match eval_static_condition0 cond vselect with
+  | Just b => binop_long (fun x0 x1 => if b then x1 else x0) v0 v1
+  | _ => Vtop
+  end.
+
+Definition eval_static_selectf (cond : condition0) (v0 v1 vselect : aval) : aval :=
+  match eval_static_condition0 cond vselect with
+  | Just b => binop_float (fun x0 x1 => if b then x1 else x0) v0 v1
+  | _ => Vtop
+  end.
+
+Definition eval_static_selectfs (cond : condition0) (v0 v1 vselect : aval) : aval :=
+  match eval_static_condition0 cond vselect with
+  | Just b => binop_single (fun x0 x1 => if b then x1 else x0) v0 v1
+  | _ => Vtop
+  end.
+  
 Definition eval_static_operation (op: operation) (vl: list aval): aval :=
   match op, vl with
   | Omove, v1::nil => v1
@@ -166,6 +198,10 @@ Definition eval_static_operation (op: operation) (vl: list aval): aval :=
   | Osingleoflong, v1::nil => singleoflong v1
   | Osingleoflongu, v1::nil => singleoflongu v1
   | Ocmp c, _ => of_optbool (eval_static_condition c vl)
+  | (Oselect cond), v0::v1::vselect::nil => eval_static_select cond v0 v1 vselect
+  | (Oselectl cond), v0::v1::vselect::nil => eval_static_selectl cond v0 v1 vselect               
+  | (Oselectf cond), v0::v1::vselect::nil => eval_static_selectf cond v0 v1 vselect
+  | (Oselectfs cond), v0::v1::vselect::nil => eval_static_selectfs cond v0 v1 vselect               
   | _, _ => Vbot
   end.
 
@@ -191,6 +227,15 @@ Proof.
   destruct cond; auto with va.
 Qed.
 
+Theorem eval_static_condition0_sound:
+  forall cond varg m aarg,
+  vmatch bc varg aarg ->
+  cmatch (eval_condition0 cond varg m) (eval_static_condition0 cond aarg).
+Proof.
+  intros until aarg; intro VM.
+  destruct cond; simpl; eauto with va.
+Qed.
+
 Lemma symbol_address_sound:
   forall id ofs,
   vmatch bc (Genv.symbol_address ge id ofs) (Ptr (Gl id ofs)).
@@ -236,12 +281,52 @@ Theorem eval_static_operation_sound:
   list_forall2 (vmatch bc) vargs aargs ->
   vmatch bc vres (eval_static_operation op aargs).
 Proof.
-  unfold eval_operation, eval_static_operation; intros;
+  unfold eval_operation, eval_static_operation, eval_static_select, eval_static_selectl, eval_static_selectf, eval_static_selectfs; intros;
   destruct op; InvHyps; eauto with va.
   destruct (propagate_float_constants tt); constructor.
   destruct (propagate_float_constants tt); constructor.
   rewrite Ptrofs.add_zero_l; eauto with va.
   apply of_optbool_sound. eapply eval_static_condition_sound; eauto.
+  (* select *)
+  - assert (Hcond : (cmatch (eval_condition0 cond a2 m) (eval_static_condition0 cond b2))) by (apply eval_static_condition0_sound; assumption).
+    rewrite eval_select_to2.
+    unfold eval_select2.
+    inv Hcond; trivial; try constructor.
+    + apply binop_int_sound; assumption.
+    + destruct a1; destruct a0; try apply vmatch_ifptr_undef.
+      apply vmatch_ifptr_i.
+    + destruct (eval_condition0 cond a2 m); destruct a1; destruct a0; try apply vmatch_ifptr_undef.
+      apply vmatch_ifptr_i.
+  (* selectl *)
+  - assert (Hcond : (cmatch (eval_condition0 cond a2 m) (eval_static_condition0 cond b2))) by (apply eval_static_condition0_sound; assumption).
+    rewrite eval_selectl_to2.
+    unfold eval_selectl2.
+    inv Hcond; trivial; try constructor.
+    + apply binop_long_sound; assumption.
+    + destruct a1; destruct a0; try apply vmatch_ifptr_undef.
+      apply vmatch_ifptr_l.
+    + destruct (eval_condition0 cond a2 m); destruct a1; destruct a0; try apply vmatch_ifptr_undef.
+      apply vmatch_ifptr_l.
+  (* selectf *)
+  - assert (Hcond : (cmatch (eval_condition0 cond a2 m) (eval_static_condition0 cond b2))) by (apply eval_static_condition0_sound; assumption).
+    rewrite eval_selectf_to2.
+    unfold eval_selectf2.
+    inv Hcond; trivial; try constructor.
+    + apply binop_float_sound; assumption.
+    + destruct a1; destruct a0; try apply vmatch_ifptr_undef.
+      constructor.
+    + destruct (eval_condition0 cond a2 m); destruct a1; destruct a0; try apply vmatch_ifptr_undef.
+      constructor.
+  (* selectfs *)
+  - assert (Hcond : (cmatch (eval_condition0 cond a2 m) (eval_static_condition0 cond b2))) by (apply eval_static_condition0_sound; assumption).
+    rewrite eval_selectfs_to2.
+    unfold eval_selectfs2.
+    inv Hcond; trivial; try constructor.
+    + apply binop_single_sound; assumption.
+    + destruct a1; destruct a0; try apply vmatch_ifptr_undef.
+      constructor.
+    + destruct (eval_condition0 cond a2 m); destruct a1; destruct a0; try apply vmatch_ifptr_undef.
+      constructor.
 Qed.
 
 End SOUNDNESS.