Oselectf, Oselectfs with condition

1 files changed, 95 insertions, 47 deletions

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: