for floats and doubles, asmgen support

3 files changed, 92 insertions, 15 deletions

diff --git a/mppa_k1c/Asmblockgen.v b/mppa_k1c/Asmblockgen.v
index a7e3c8ef..ad01ff89 100644
--- a/mppa_k1c/Asmblockgen.v
+++ b/mppa_k1c/Asmblockgen.v
@@ -729,14 +729,10 @@ Definition transl_op
       do rd <- ireg_of res;
       transl_cond_op cmp rd args k
 
-  | Oselect, 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)
-
-  | Oselectl, a0 :: a1 :: aS :: nil =>
+  | Oselect, a0 :: a1 :: aS :: nil
+  | Oselectl, a0 :: a1 :: aS :: nil
+  | 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;
diff --git a/mppa_k1c/Op.v b/mppa_k1c/Op.v
index 74788387..5afd0cb9 100644
--- a/mppa_k1c/Op.v
+++ b/mppa_k1c/Op.v
@@ -183,7 +183,9 @@ Inductive operation : Type :=
 (*c Boolean tests: *)
   | Ocmp (cond: condition)   (**r [rd = 1] if condition holds, [rd = 0] otherwise. *)
   | Oselect                  (**r [rd = if r3 then r2 else r1] *)
-  | Oselectl.                (**r [rd = if r3 then r2 else r1] *)
+  | Oselectl                 (**r [rd = if r3 then r2 else r1] *)
+  | Oselectf                 (**r [rd = if r3 then r2 else r1] *)
+  | Oselectfs.               (**r [rd = if r3 then r2 else r1] *)
 
 (** Addressing modes.  [r1], [r2], etc, are the arguments to the
   addressing. *)
@@ -287,6 +289,40 @@ Definition selectl (v0 : val) (v1 : val) (vselect : val) : val :=
   | _ => Vundef
   end.
 
+Definition 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
+  end.
+
+Definition 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
+  end.
+
 Definition eval_operation
     (F V: Type) (genv: Genv.t F V) (sp: val)
     (op: operation) (vl: list val) (m: mem): option val :=
@@ -417,6 +453,8 @@ Definition eval_operation
   | Ocmp c, _ => Some (Val.of_optbool (eval_condition c vl m))
   | Oselect, v0::v1::vselect::nil => Some (select v0 v1 vselect)
   | Oselectl, v0::v1::vselect::nil => Some (selectl v0 v1 vselect)
+  | Oselectf, v0::v1::vselect::nil => Some (selectf v0 v1 vselect)
+  | Oselectfs, v0::v1::vselect::nil => Some (selectfs v0 v1 vselect)
   | _, _ => None
   end.
 
@@ -608,6 +646,8 @@ Definition type_of_operation (op: operation) : list typ * typ :=
                 
   | Oselect  => (Tint :: Tint :: Tint :: nil, Tint)
   | Oselectl => (Tlong :: Tlong :: Tint :: nil, Tlong)
+  | Oselectf  => (Tfloat :: Tfloat :: Tint :: nil, Tfloat)
+  | Oselectfs => (Tsingle :: Tsingle :: Tint :: nil, Tsingle)
   end.
 
 Definition type_of_addressing (addr: addressing) : list typ :=
@@ -847,6 +887,10 @@ Proof with (try exact I; try reflexivity; auto using Val.Vptr_has_type).
   - destruct v0; destruct v1; destruct v2; simpl in *; try discriminate; trivial.
   (* selectl *)
   - destruct v0; destruct v1; destruct v2; simpl in *; try discriminate; trivial.
+  (* selectf *)
+  - destruct v0; destruct v1; destruct v2; simpl in *; try discriminate; trivial.
+  (* selectfs *)
+  - destruct v0; destruct v1; destruct v2; simpl in *; try discriminate; trivial.
 Qed.
 
 End SOUNDNESS.
@@ -1381,6 +1425,14 @@ Proof.
   - inv H3; simpl; try constructor.
     inv H4; simpl; try constructor.
     inv H2; simpl; constructor.
+  (* selectf *)
+  - inv H3; simpl; try constructor.
+    inv H4; simpl; try constructor.
+    inv H2; simpl; constructor.
+  (* selectfs *)
+  - inv H3; simpl; try constructor.
+    inv H4; simpl; try constructor.
+    inv H2; simpl; constructor.
 Qed.
 
 Lemma eval_addressing_inj:
diff --git a/mppa_k1c/ValueAOp.v b/mppa_k1c/ValueAOp.v
index da108ada..122249a4 100644
--- a/mppa_k1c/ValueAOp.v
+++ b/mppa_k1c/ValueAOp.v
@@ -59,6 +59,24 @@ Definition selectl (v0 v1 vselect : aval) : aval :=
     else binop_long (fun x0 x1 => x1) v0 v1
   | _ => Vtop
   end.
+
+Definition 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
+  | _ => Vtop
+  end.
+
+Definition 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
+  | _ => Vtop
+  end.
   
 Definition eval_static_operation (op: operation) (vl: list aval): aval :=
   match op, vl with
@@ -186,6 +204,8 @@ Definition eval_static_operation (op: operation) (vl: list aval): aval :=
   | Ocmp c, _ => of_optbool (eval_static_condition c vl)
   | Oselect, v0::v1::vselect::nil => select v0 v1 vselect
   | Oselectl, v0::v1::vselect::nil => selectl v0 v1 vselect               
+  | Oselectf, v0::v1::vselect::nil => selectf v0 v1 vselect
+  | Oselectfs, v0::v1::vselect::nil => selectfs v0 v1 vselect               
   | _, _ => Vbot
   end.
 
@@ -265,18 +285,27 @@ Proof.
   (* select *)
   - inv H2; simpl; try constructor.
     + destruct (Int.eq _ _); apply binop_int_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.
+    + 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.
   (* selectl *)
   - inv H2; simpl; try constructor.
     + destruct (Int.eq _ _); apply binop_long_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.
+  (* 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.
+  (* 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.
 Qed.
 
 End SOUNDNESS.