rm old select/selectl/selectf/selectfs

14 files changed, 47 insertions, 914 deletions

diff --git a/backend/Selection.v b/backend/Selection.v
index 37a78853..2d407094 100644
--- a/backend/Selection.v
+++ b/backend/Selection.v
@@ -277,67 +277,6 @@ Definition sel_switch_long :=
     (fun arg ofs => subl arg (longconst (Int64.repr ofs)))
     lowlong.
 
-Definition sel_builtin_default optid ef args :=
-  OK (Sbuiltin (sel_builtin_res optid) ef
-               (sel_builtin_args args
-                                 (Machregs.builtin_constraints ef))).
-
-Definition sel_builtin optid ef args :=
-  match ef with
-    | EF_builtin name sign =>
-      (if String.string_dec name "__builtin_ternary_uint"
-       || String.string_dec name "__builtin_ternary_int"
-       then
-         match optid with
-           | None => OK Sskip
-           | Some id =>
-             match args with
-               | a1::a2::a3::nil =>
-                 OK (Sassign id (select (sel_expr a3) (sel_expr a2) (sel_expr a1)))
-               | _ => Error (msg "__builtin_ternary_(u)int: arguments")
-             end
-         end
-       else
-       if String.string_dec name "__builtin_ternary_ulong"
-       || String.string_dec name "__builtin_ternary_long"  
-       then
-         match optid with
-           | None => OK Sskip
-           | Some id =>
-             match args with
-               | a1::a2::a3::nil =>
-                 OK (Sassign id (selectl (sel_expr a3) (sel_expr a2) (sel_expr a1)))
-               | _ => Error (msg "__builtin_ternary_(u)long: arguments")
-             end
-         end
-       else
-       if String.string_dec name "__builtin_ternary_double"
-       then
-         match optid with
-           | None => OK Sskip
-           | Some id =>
-             match args with
-               | a1::a2::a3::nil =>
-                 OK (Sassign id (selectf (sel_expr a3) (sel_expr a2) (sel_expr a1)))
-               | _ => Error (msg "__builtin_ternary_double: arguments")
-             end
-         end
-       else
-       if String.string_dec name "__builtin_ternary_float"
-       then
-         match optid with
-           | None => OK Sskip
-           | Some id =>
-             match args with
-               | a1::a2::a3::nil =>
-                 OK (Sassign id (selectfs (sel_expr a3) (sel_expr a2) (sel_expr a1)))
-               | _ => Error (msg "__builtin_ternary_float: arguments")
-             end
-         end
-       else
-         sel_builtin_default optid ef args)
-    | _ => sel_builtin_default optid ef args
-
 (** "If conversion": conversion of certain if-then-else statements
   into branchless conditional move instructions. *)
 
diff --git a/backend/Selectionaux.ml b/backend/Selectionaux.ml
index 52ddd799..b43b0e7f 100644
--- a/backend/Selectionaux.ml
+++ b/backend/Selectionaux.ml
@@ -75,9 +75,9 @@ let fast_cmove ty =
   | "powerpc", _ -> false
   | "riscV", _ -> false
   | "x86", _ -> 
-      (match ty with Tint -> true | Tlong -> Archi.ptr64 | _ -> false)
-  | _, _ ->
-      assert false
+     (match ty with Tint -> true | Tlong -> Archi.ptr64 | _ -> false)
+  | "mppa_k1c", _ -> false (* TODO DM *)
+  | a, m -> failwith (Printf.sprintf "fast_cmove: unknown arch %s %s" a m)
 
 (* The if-conversion heuristic depend on the
    -fif-conversion and -ffavor-branchless flags.
diff --git a/mppa_k1c/Archi.v b/mppa_k1c/Archi.v
index bbe66c5b..113f5d51 100644
--- a/mppa_k1c/Archi.v
+++ b/mppa_k1c/Archi.v
@@ -17,8 +17,8 @@
 (** Architecture-dependent parameters for RISC-V *)
 
 Require Import ZArith.
-Require Import Fappli_IEEE.
-Require Import Fappli_IEEE_bits.
+(*From Flocq*)
+Require Import Binary Bits.
 
 Definition ptr64 := true.
 
@@ -41,23 +41,26 @@ Qed.
    We need to extend the [choose_binop_pl] functions to account for
    this case. *)
 
-Program Definition default_pl_64 : bool * nan_pl 53 :=
-  (false, iter_nat 51 _ xO xH).
+Definition default_nan_64 : { x : binary64 | is_nan _ _ x = true } :=
+  exist _ (B754_nan 53 1024 true (iter_nat 51 _ xO xH) (eq_refl true)) (eq_refl true).
 
-Definition choose_binop_pl_64 (s1: bool) (pl1: nan_pl 53) (s2: bool) (pl2: nan_pl 53) :=
+Definition choose_binop_pl_64 (pl1 pl2 : positive) :=
   false.                        (**r always choose first NaN *)
 
-Program Definition default_pl_32 : bool * nan_pl 24 :=
-  (false, iter_nat 22 _ xO xH).
+Definition default_nan_32 : { x : binary32 | is_nan _ _ x = true } :=
+  exist _ (B754_nan 24 128 true (iter_nat 22 _ xO xH) (eq_refl true)) (eq_refl true).
 
-Definition choose_binop_pl_32 (s1: bool) (pl1: nan_pl 24) (s2: bool) (pl2: nan_pl 24) :=
+Definition choose_binop_pl_32 (pl1 pl2 : positive) :=
   false.                        (**r always choose first NaN *)
 
+(* TODO check *)
+Definition fpu_returns_default_qNaN := false.
+
 Definition float_of_single_preserves_sNaN := false.
 
 Global Opaque ptr64 big_endian splitlong
-              default_pl_64 choose_binop_pl_64
-              default_pl_32 choose_binop_pl_32
+              default_nan_64 choose_binop_pl_64
+              default_nan_32 choose_binop_pl_32
               float_of_single_preserves_sNaN.
 
 (** Whether to generate position-independent code or not *)
diff --git a/mppa_k1c/Asmblockgen.v b/mppa_k1c/Asmblockgen.v
index 941796cd..33fa39b5 100644
--- a/mppa_k1c/Asmblockgen.v
+++ b/mppa_k1c/Asmblockgen.v
@@ -784,31 +784,10 @@ Definition transl_op
   | Olonguofsingle , _ => Error (msg "Asmblockgen.transl_op: Olonguofsingle")
 
 
-
   | Ocmp cmp, _ =>
       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)
 
   | Oextfz stop start, a1 :: nil =>
     assertion (ExtValues.is_bitfield stop start);
diff --git a/mppa_k1c/Asmblockgenproof1.v b/mppa_k1c/Asmblockgenproof1.v
index 3c1162bd..8125741b 100644
--- a/mppa_k1c/Asmblockgenproof1.v
+++ b/mppa_k1c/Asmblockgenproof1.v
@@ -1719,250 +1719,6 @@ Opaque Int.eq.
 - (* Ocmp *)
   exploit transl_cond_op_correct; eauto. intros (rs' & A & B & C).
   exists rs'; split. eexact A. eauto 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/ExtValues.v b/mppa_k1c/ExtValues.v
index 155afa83..8e6aa028 100644
--- a/mppa_k1c/ExtValues.v
+++ b/mppa_k1c/ExtValues.v
@@ -287,10 +287,10 @@ Proof.
   intros.
   apply Int.eqm_samerepr.
   unfold Int.eqm.
-  unfold Int.eqmod.
+  unfold Zbits.eqmod.
   pose proof (Int64.eqm_unsigned_repr x) as H64.
   unfold Int64.eqm in H64.
-  unfold Int64.eqmod in H64.
+  unfold Zbits.eqmod in H64.
   destruct H64 as [k64 H64].
   change Int64.modulus with 18446744073709551616 in *.
   change Int.modulus with 4294967296.
@@ -367,7 +367,7 @@ Proof.
         apply Int.eqm_samerepr.
         unfold Int.eqm.
         change (Int64.unsigned (Int64.repr (-2147483648))) with 18446744071562067968.
-        unfold Int.eqmod.
+        unfold Zbits.eqmod.
         change Int.modulus with 4294967296.
         exists (-4294967296).
         compute.
diff --git a/mppa_k1c/Machregs.v b/mppa_k1c/Machregs.v
index db3dfe64..4e8eedda 100644
--- a/mppa_k1c/Machregs.v
+++ b/mppa_k1c/Machregs.v
@@ -216,7 +216,6 @@ Definition two_address_op (op: operation) : bool :=
   | Omadd | Omaddimm _
   | Omaddl | Omaddlimm _
   | Omsub | Omsubl
-  | Oselect _ | Oselectl _ | Oselectf _ | Oselectfs _
   | Oinsf _ _ | Oinsfl _ _ => true
   | _ => false
   end.
diff --git a/mppa_k1c/NeedOp.v b/mppa_k1c/NeedOp.v
index 5ba9851f..746b21a6 100644
--- a/mppa_k1c/NeedOp.v
+++ b/mppa_k1c/NeedOp.v
@@ -129,7 +129,6 @@ 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)
   | Oextfz _ _ | Oextfs _ _  | Oextfzl _ _ | Oextfsl _ _ => op1 (default nv)
   | Oinsf _ _ | Oinsfl _ _ => op2 (default nv)
   end.
@@ -277,179 +276,6 @@ Proof.
     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.
@@ -514,14 +340,6 @@ 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:
diff --git a/mppa_k1c/Op.v b/mppa_k1c/Op.v
index 4df157b0..24572e13 100644
--- a/mppa_k1c/Op.v
+++ b/mppa_k1c/Op.v
@@ -204,10 +204,6 @@ Inductive operation : Type :=
   | Osingleoflongu           (**r [rd = float32_of_unsigned_int(r1)] *)
 (*c Boolean tests: *)
   | 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] *)
   | Oextfz (stop : Z) (start : Z)
   | Oextfs (stop : Z) (start : Z)
   | Oextfzl (stop : Z) (start : Z)
@@ -304,24 +300,24 @@ Definition eval_condition0 (cond: condition0) (v1: val) (m: mem): option bool :=
   | 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 :=
+Definition eval_selecti (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 :=
+Definition eval_selecti2 (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).
+Lemma eval_selecti_to2: forall cond v0 v1 vselect m,
+    (eval_selecti cond v0 v1 vselect m) =
+    (eval_selecti2 cond v0 v1 vselect m).
 Proof.
   intros.
-  unfold eval_select2.
+  unfold eval_selecti2.
   destruct v0; destruct v1; simpl; destruct (eval_condition0 cond vselect m); simpl; reflexivity.
 Qed.
 
@@ -526,10 +522,6 @@ 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)
   | (Oextfz stop start), v0::nil => Some (extfz stop start v0)
   | (Oextfs stop start), v0::nil => Some (extfs stop start v0)
   | (Oextfzl stop start), v0::nil => Some (extfzl stop start v0)
@@ -734,12 +726,7 @@ Definition type_of_operation (op: operation) : list typ * typ :=
   | Olonguofsingle => (Tsingle :: nil, Tlong)
   | 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)
+  | Ocmp c => (type_of_condition c, Tint)                
   | Oextfz _ _ | Oextfs _ _ => (Tint :: nil, Tint)
   | Oextfzl _ _ | Oextfsl _ _ => (Tlong :: nil, Tlong)
   | Oinsf _ _ => (Tint :: Tint :: nil, Tint)
@@ -1021,43 +1008,6 @@ 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.
  (* extfz *)
   - unfold extfz.
     destruct (is_bitfield _ _).
@@ -1250,19 +1200,6 @@ 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.
 
@@ -1274,7 +1211,7 @@ Proof.
   intros until m2. destruct op; simpl; try congruence;
                      
   destruct cond; simpl; intros SF; auto; rewrite ? negb_false_iff in SF;
-  unfold eval_select, eval_selectl, eval_selectf, eval_selectfs, eval_condition0, Val.cmpu_bool, Val.cmplu_bool; rewrite SF; reflexivity.
+  unfold eval_selecti, 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 *)
@@ -1668,62 +1605,6 @@ 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.
 
  (* extfz *)
   - unfold extfz.
diff --git a/mppa_k1c/SelectLong.vp b/mppa_k1c/SelectLong.vp
index 4e369e11..981c796c 100644
--- a/mppa_k1c/SelectLong.vp
+++ b/mppa_k1c/SelectLong.vp
@@ -306,14 +306,6 @@ Nondetfunction andl (e1: expr) (e2: expr) :=
   | 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
@@ -332,17 +324,6 @@ Nondetfunction orl (e1: expr) (e2: expr) :=
   | 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)
-  |  (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 (Oandlimm nmask) (prev:::Enil)),
     (Eop (Oandlimm mask)
       ((Eop (Oshllimm start) (fld:::Enil)):::Enil)) =>
diff --git a/mppa_k1c/SelectLongproof.v b/mppa_k1c/SelectLongproof.v
index 78a2bb31..ada02585 100644
--- a/mppa_k1c/SelectLongproof.v
+++ b/mppa_k1c/SelectLongproof.v
@@ -660,81 +660,6 @@ 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.
 
   - (*insfl first case*)
     destruct (is_bitfieldl _ _) eqn:Risbitfield.
diff --git a/mppa_k1c/SelectOp.vp b/mppa_k1c/SelectOp.vp
index 23d234aa..219a462b 100644
--- a/mppa_k1c/SelectOp.vp
+++ b/mppa_k1c/SelectOp.vp
@@ -66,33 +66,8 @@ 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.
+Definition select (ty : typ) (cond : condition) (args : exprlist) (e1 e2: expr)  : option expr := None.
+
 				      
 (** ** Constants **)
 
@@ -349,24 +324,6 @@ Nondetfunction or (e1: expr) (e2: expr) :=
       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)
-  |  (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 (Oandimm nmask) (prev:::Enil)),
     (Eop (Oandimm mask)
       ((Eop (Oshlimm start) (fld:::Enil)):::Enil)) =>
diff --git a/mppa_k1c/SelectOpproof.v b/mppa_k1c/SelectOpproof.v
index a5154611..26f1bb89 100644
--- a/mppa_k1c/SelectOpproof.v
+++ b/mppa_k1c/SelectOpproof.v
@@ -609,7 +609,7 @@ Proof.
   change (Int.ltu (Int.repr 32) Int64.iwordsize') with true; simpl.
   apply Val.lessdef_same. f_equal. 
   transitivity (Int.repr (Z.shiftr (Int.signed i * Int.signed i0) 32)).
-  unfold Int.mulhs; f_equal. rewrite Int.Zshiftr_div_two_p by omega. reflexivity.
+  unfold Int.mulhs; f_equal. rewrite Zbits.Zshiftr_div_two_p by omega. reflexivity.
   apply Int.same_bits_eq; intros n N.
   change Int.zwordsize with 32 in *.
   assert (N1: 0 <= n < 64) by omega.
@@ -637,7 +637,7 @@ Proof.
   change (Int.ltu (Int.repr 32) Int64.iwordsize') with true; simpl.
   apply Val.lessdef_same. f_equal. 
   transitivity (Int.repr (Z.shiftr (Int.unsigned i * Int.unsigned i0) 32)).
-  unfold Int.mulhu; f_equal. rewrite Int.Zshiftr_div_two_p by omega. reflexivity.
+  unfold Int.mulhu; f_equal. rewrite Zbits.Zshiftr_div_two_p by omega. reflexivity.
   apply Int.same_bits_eq; intros n N.
   change Int.zwordsize with 32 in *.
   assert (N1: 0 <= n < 64) by omega.
@@ -756,83 +756,6 @@ 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.
   - set (zstop := (int_highest_bit mask)).
     set (zstart := (Int.unsigned start)).
     destruct (is_bitfield _ _) eqn:Risbitfield.
@@ -1488,6 +1411,22 @@ Proof.
 - constructor; auto.
 Qed.
 
+(* ternary *)
+
+Theorem eval_select: 
+  forall le ty cond al vl a1 v1 a2 v2 a b,
+  select ty cond al a1 a2 = Some a ->
+  eval_exprlist ge sp e m le al vl ->
+  eval_expr ge sp e m le a1 v1 ->
+  eval_expr ge sp e m le a2 v2 ->
+  eval_condition cond vl m = Some b ->
+  exists v, 
+     eval_expr ge sp e m le a v
+  /\ Val.lessdef (Val.select (Some b) v1 v2 ty) v.
+Proof.
+  discriminate.
+Qed.
+
 (* floating-point division *)
 Theorem eval_divf_base:
   forall le a b x y,
diff --git a/mppa_k1c/ValueAOp.v b/mppa_k1c/ValueAOp.v
index f41dae63..f0cdf24e 100644
--- a/mppa_k1c/ValueAOp.v
+++ b/mppa_k1c/ValueAOp.v
@@ -282,10 +282,6 @@ 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
   | (Oextfz stop start), v0::nil => eval_static_extfz stop start v0
   | (Oextfs stop start), v0::nil => eval_static_extfs stop start v0
   | (Oextfzl stop start), v0::nil => eval_static_extfzl stop start v0
@@ -411,46 +407,6 @@ Proof.
     + eauto with va.
     + destruct a1; destruct shift; reflexivity.
   - 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.
 
   (* extfz *)
   - unfold extfz, eval_static_extfz.