Oselectf, Oselectfs with condition

8 files changed, 325 insertions, 131 deletions

diff --git a/backend/Selection.v b/backend/Selection.v
index 971f9948..d2067dab 100644
--- a/backend/Selection.v
+++ b/backend/Selection.v
@@ -308,10 +308,7 @@ Definition sel_builtin optid ef args :=
            | Some id =>
              match args with
                | a1::a2::a3::nil =>
-                 OK (Sassign id (Eop Oselectf
-                                     ((sel_expr a3):::
-                                                   (sel_expr a2):::
-                                                   (sel_expr a1):::Enil)))
+                 OK (Sassign id (selectf (sel_expr a3) (sel_expr a2) (sel_expr a1)))
                | _ => Error (msg "__builtin_ternary_double: arguments")
              end
          end
@@ -323,10 +320,7 @@ Definition sel_builtin optid ef args :=
            | Some id =>
              match args with
                | a1::a2::a3::nil =>
-                 OK (Sassign id (Eop Oselectfs
-                                     ((sel_expr a3):::
-                                                   (sel_expr a2):::
-                                                   (sel_expr a1):::Enil)))
+                 OK (Sassign id (selectfs (sel_expr a3) (sel_expr a2) (sel_expr a1)))
                | _ => Error (msg "__builtin_ternary_float: arguments")
              end
          end
diff --git a/mppa_k1c/Asmblockgen.v b/mppa_k1c/Asmblockgen.v
index b3478a9a..392b7953 100644
--- a/mppa_k1c/Asmblockgen.v
+++ b/mppa_k1c/Asmblockgen.v
@@ -752,7 +752,9 @@ Definition transl_op
       transl_cond_op cmp rd args k
 
   | Oselect cond, a0 :: a1 :: aS :: nil
-  | Oselectl 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;
@@ -769,14 +771,6 @@ Definition transl_op
          do bt <- btest_for_cmpudz cmp;
            OK (Pcmoveu bt r0 rS r1 ::i k)
        end)
-    
-  | Oselectf, a0 :: a1 :: aS :: nil
-  | Oselectfs, a0 :: a1 :: aS :: nil =>
-    assertion (mreg_eq a0 res);
-      do r0 <- ireg_of a0;
-      do r1 <- ireg_of a1;
-      do rS <- ireg_of aS;
-        OK (Pcmove BTwnez r0 rS r1 ::i k)
 
   | _, _ =>
       Error(msg "Asmgenblock.transl_op")
diff --git a/mppa_k1c/Asmblockgenproof1.v b/mppa_k1c/Asmblockgenproof1.v
index 874e40a8..6cf5c60c 100644
--- a/mppa_k1c/Asmblockgenproof1.v
+++ b/mppa_k1c/Asmblockgenproof1.v
@@ -1698,7 +1698,7 @@ Opaque Int.eq.
     * intros.
       rewrite Pregmap.gso; congruence.
 
-- (* Oselect *)
+- (* Oselectl *)
   destruct cond in *; simpl in *; try congruence;
     try monadInv EQ3;
     try (injection EQ3; clear EQ3; intro Hrew; rewrite <- Hrew in * ; clear Hrew);
@@ -1760,31 +1760,125 @@ Opaque Int.eq.
       rewrite Pregmap.gso; congruence.
 
 - (* Oselectf *)
-  econstructor; split.
-  + eapply exec_straight_one.
-    simpl; reflexivity.
+  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_selectf.
-      destruct (rs x1) eqn:eqX1; try constructor.
+    * unfold eval_select.
       destruct (rs x) eqn:eqX; try constructor.
       destruct (rs x0) eqn:eqX0; try constructor.
-      simpl.
-      rewrite int_eq_comm.
-      destruct (Int.eq i Int.zero); simpl; rewrite Pregmap.gss; 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 *)
-  econstructor; split.
-  + eapply exec_straight_one.
-    simpl; reflexivity.
+  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_selectfs.
-      destruct (rs x1) eqn:eqX1; try constructor.
+    * unfold eval_select.
       destruct (rs x) eqn:eqX; try constructor.
       destruct (rs x0) eqn:eqX0; try constructor.
-      simpl.
-      rewrite int_eq_comm.
-      destruct (Int.eq i Int.zero); simpl; rewrite Pregmap.gss; 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.
diff --git a/mppa_k1c/Machregs.v b/mppa_k1c/Machregs.v
index ddf730a9..f36962f3 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 _ | Oselect _ | Oselectl _ | Oselectf | Oselectfs => true
+  | Ocast32unsigned | Omadd | Omaddimm _ | Omaddl | Omaddlimm _ | Oselect _ | Oselectl _ | Oselectf _ | Oselectfs _ => true
   | _ => false
   end.
 
diff --git a/mppa_k1c/NeedOp.v b/mppa_k1c/NeedOp.v
index a276cda1..ba051c90 100644
--- a/mppa_k1c/NeedOp.v
+++ b/mppa_k1c/NeedOp.v
@@ -117,7 +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)
+  | Oselect _ | Oselectl _ | Oselectf _ | Oselectfs _ => op3 (default nv)
   end.
 
 Definition operation_is_redundant (op: operation) (nv: nval): bool :=
@@ -332,41 +332,89 @@ Proof.
 Qed.
 
 Lemma selectf_sound:
-  forall v0 w0 v1 w1 v2 w2 x,
+  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 v0 v1 v2) (eval_selectf w0 w1 w2) x.
+    vagree (eval_selectf cond v0 v1 v2 m1) (eval_selectf cond w0 w1 w2 m2) x.
 Proof.
-  unfold default; intros.
-  destruct x; trivial.
-  - destruct v2; simpl; trivial.
-    destruct v0; simpl; trivial.
-    destruct v1; simpl; trivial.
-  - destruct v2; simpl; trivial.
-    destruct v0; simpl; trivial.
-    destruct v1; simpl; trivial.
-    inv H. inv H0. inv H1. simpl.
-    constructor.
+  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 v0 w0 v1 w1 v2 w2 x,
+  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 v0 v1 v2) (eval_selectfs w0 w1 w2) x.
+    vagree (eval_selectfs cond v0 v1 v2 m1) (eval_selectfs cond w0 w1 w2 m2) x.
 Proof.
-  unfold default; intros.
-  destruct x; trivial.
-  - destruct v2; simpl; trivial.
-    destruct v0; simpl; trivial.
-    destruct v1; simpl; trivial.
-  - destruct v2; simpl; trivial.
-    destruct v0; simpl; trivial.
-    destruct v1; simpl; trivial.
-    inv H. inv H0. inv H1. simpl.
-    constructor.
+  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.
diff --git a/mppa_k1c/Op.v b/mppa_k1c/Op.v
index 045946fd..14758bee 100644
--- a/mppa_k1c/Op.v
+++ b/mppa_k1c/Op.v
@@ -194,10 +194,10 @@ 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                 (**r [rd = if r3 then r2 else r1] *)
-  | Oselectfs.               (**r [rd = if r3 then r2 else r1] *)
+  | 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. *)
@@ -324,40 +324,48 @@ Proof.
   destruct v0; destruct v1; simpl; destruct (eval_condition0 cond vselect m); simpl; reflexivity.
 Qed.
 
-Definition eval_selectf (v0 : val) (v1 : val) (vselect : val) : val :=
-  match vselect with
-  | Vint iselect =>
-    match v0 with
-    | Vfloat i0 =>
-      match v1 with
-      | Vfloat i1 =>
-        Vfloat (if Int.cmp Ceq Int.zero iselect
-                then i0
-                else i1)
-      | _ => Vundef
-      end
-    | _ => Vundef
-    end
-  | _ => Vundef
+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_selectfs (v0 : val) (v1 : val) (vselect : val) : val :=
-  match vselect with
-  | Vint iselect =>
-    match v0 with
-    | Vsingle i0 =>
-      match v1 with
-      | Vsingle i1 =>
-        Vsingle (if Int.cmp Ceq Int.zero iselect
-                 then i0
-                 else i1)
-      | _ => Vundef
-      end
-    | _ => Vundef
-    end
-  | _ => Vundef
+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)
     (op: operation) (vl: list val) (m: mem): option val :=
@@ -488,8 +496,8 @@ Definition eval_operation
   | 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, v0::v1::vselect::nil => Some (eval_selectf v0 v1 vselect)
-  | Oselectfs, v0::v1::vselect::nil => Some (eval_selectfs v0 v1 vselect)
+  | (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.
 
@@ -681,8 +689,8 @@ Definition type_of_operation (op: operation) : list typ * typ :=
                 
   | Oselect cond => (Tint :: Tint :: (arg_type_of_condition0 cond) :: nil, Tint)
   | Oselectl cond => (Tlong :: Tlong :: (arg_type_of_condition0 cond) :: nil, Tlong)
-  | Oselectf  => (Tfloat :: Tfloat :: Tint :: nil, Tfloat)
-  | Oselectfs => (Tsingle :: Tsingle :: Tint :: nil, Tsingle)
+  | 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 :=
@@ -938,9 +946,23 @@ Proof with (try exact I; try reflexivity; auto using Val.Vptr_has_type).
       destruct (Val.cmp_different_blocks _); simpl; trivial.
 
   (* selectf *)
-  - destruct v0; destruct v1; destruct v2; simpl in *; try discriminate; trivial.
+  - 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; destruct v2; simpl in *; try discriminate; trivial.
+  - 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.
@@ -1107,6 +1129,12 @@ Definition op_depends_on_memory (op: operation) : bool :=
 
   | 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.
@@ -1119,7 +1147,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_condition0, 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 *)
@@ -1517,13 +1545,33 @@ Proof.
       assumption.
     * rewrite Hcond'. constructor.
   (* selectf *)
-  - inv H3; simpl; try constructor.
-    inv H4; simpl; try constructor.
-    inv H2; simpl; constructor.
+  - 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 *)
-  - inv H3; simpl; try constructor.
-    inv H4; simpl; try constructor.
-    inv H2; simpl; constructor.
+  - 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/SelectOp.vp b/mppa_k1c/SelectOp.vp
index eeb3ffae..71e0eff3 100644
--- a/mppa_k1c/SelectOp.vp
+++ b/mppa_k1c/SelectOp.vp
@@ -76,6 +76,20 @@ Definition selectl_base o0 o1 oselect :=
 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) :=
diff --git a/mppa_k1c/ValueAOp.v b/mppa_k1c/ValueAOp.v
index 62cfa85e..f17bd765 100644
--- a/mppa_k1c/ValueAOp.v
+++ b/mppa_k1c/ValueAOp.v
@@ -62,21 +62,15 @@ Definition eval_static_selectl (cond : condition0) (v0 v1 vselect : aval) : aval
   | _ => Vtop
   end.
 
-Definition eval_static_selectf (v0 v1 vselect : aval) : aval :=
-  match vselect with
-  | I iselect =>
-    if Int.eq Int.zero iselect
-    then binop_float (fun x0 x1 => x0) v0 v1
-    else binop_float (fun x0 x1 => x1) v0 v1
+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 (v0 v1 vselect : aval) : aval :=
-  match vselect with
-  | I iselect =>
-    if Int.eq Int.zero iselect
-    then binop_single (fun x0 x1 => x0) v0 v1
-    else binop_single (fun x0 x1 => x1) v0 v1
+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.
   
@@ -206,8 +200,8 @@ Definition eval_static_operation (op: operation) (vl: list aval): aval :=
   | 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, v0::v1::vselect::nil => eval_static_selectf v0 v1 vselect
-  | Oselectfs, v0::v1::vselect::nil => eval_static_selectfs 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.
 
@@ -314,17 +308,25 @@ Proof.
     + destruct (eval_condition0 cond a2 m); destruct a1; destruct a0; try apply vmatch_ifptr_undef.
       apply vmatch_ifptr_l.
   (* selectf *)
-  - inv H2; simpl; try constructor.
-    + destruct (Int.eq _ _); apply binop_float_sound; trivial.
-    + destruct (Int.eq _ _); destruct a1; destruct a0; eauto; constructor.
-    + destruct (Int.eq _ _); destruct a1; destruct a0; eauto; constructor.
-    + destruct (Int.eq _ _); destruct a1; destruct a0; eauto; constructor.
+  - 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 *)
-  - inv H2; simpl; try constructor.
-    + destruct (Int.eq _ _); apply binop_single_sound; trivial.
-    + destruct (Int.eq _ _); destruct a1; destruct a0; eauto; constructor.
-    + destruct (Int.eq _ _); destruct a1; destruct a0; eauto; constructor.
-    + destruct (Int.eq _ _); destruct a1; destruct a0; eauto; constructor.
+  - 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.