begin osel imm

1 files changed, 39 insertions, 3 deletions

diff --git a/mppa_k1c/Op.v b/mppa_k1c/Op.v
index be7ea812..1b3a839f 100644
--- a/mppa_k1c/Op.v
+++ b/mppa_k1c/Op.v
@@ -210,7 +210,9 @@ Inductive operation : Type :=
   | Oextfsl (stop : Z) (start : Z)
   | Oinsf (stop : Z) (start : Z)
   | Oinsfl (stop : Z) (start : Z)
-  | Osel (c0 : condition0) (ty : typ).
+  | Osel (c0 : condition0) (ty : typ)
+  | Oselimm (c0 : condition0) (imm: int)
+  | Osellimm (c0 : condition0) (imm: int64).
 
 (** Addressing modes.  [r1], [r2], etc, are the arguments to the
   addressing. *)
@@ -454,6 +456,8 @@ Definition eval_operation
   | (Oinsf stop start), v0::v1::nil => Some (insf stop start v0 v1)
   | (Oinsfl stop start), v0::v1::nil => Some (insfl stop start v0 v1)
   | Osel c ty, v1::v2::vc::nil => Some(Val.select (eval_condition0 c vc m) v1 v2 ty)
+  | Oselimm c imm, v1::v2::vc::nil => Some(Val.select (eval_condition0 c vc m) v1 (Vint imm) Tint)
+  | Osellimm c imm, v1::v2::vc::nil => Some(Val.select (eval_condition0 c vc m) v1 (Vlong imm) Tlong)
   | _, _ => None
   end.
 
@@ -658,6 +662,8 @@ Definition type_of_operation (op: operation) : list typ * typ :=
   | Oinsf _ _ => (Tint :: Tint :: nil, Tint)
   | Oinsfl _ _ => (Tlong :: Tlong :: nil, Tlong)
   | Osel c ty => (ty :: ty :: arg_type_of_condition0 c :: nil, ty)
+  | Oselimm c ty => (Tint :: Tint :: arg_type_of_condition0 c :: nil, Tint)
+  | Osellimm c ty => (Tlong :: Tlong :: arg_type_of_condition0 c :: nil, Tlong)
   end.
 
 (* FIXME: two Tptr ?! *)
@@ -971,6 +977,14 @@ Proof with (try exact I; try reflexivity; auto using Val.Vptr_has_type).
   - unfold Val.select. destruct (eval_condition0 _ _ m).
     + apply Val.normalize_type.
     + constructor.
+ (* Oselimm *)
+  - unfold Val.select. destruct (eval_condition0 _ _ m).
+    + apply Val.normalize_type.
+    + constructor.
+ (* Osellimm *)
+  - unfold Val.select. destruct (eval_condition0 _ _ m).
+    + apply Val.normalize_type.
+    + constructor.
 Qed.
 
 End SOUNDNESS.
@@ -1132,8 +1146,8 @@ Definition op_depends_on_memory (op: operation) : bool :=
   | Ocmp (Ccomplu _) => Archi.ptr64
   | Ocmp (Ccompluimm _ _) => Archi.ptr64
   
-  | Osel (Ccompu0 _) _ => negb Archi.ptr64
-  | Osel (Ccomplu0 _) _ => Archi.ptr64
+  | Osel (Ccompu0 _) _   | Oselimm (Ccompu0 _) _   | Osellimm (Ccompu0 _) _ => negb Archi.ptr64
+  | Osel (Ccomplu0 _) _ | Oselimm (Ccomplu0 _) _ | Osellimm (Ccomplu0 _) _ => Archi.ptr64
 
   | _ => false
   end.
@@ -1150,6 +1164,12 @@ Proof.
   - destruct c0; simpl; try congruence;
     intros SF; auto; rewrite ? negb_false_iff in SF;
       unfold Val.cmpu_bool, Val.cmplu_bool; rewrite SF; reflexivity.
+  - destruct c0; simpl; try congruence;
+    intros SF; auto; rewrite ? negb_false_iff in SF;
+      unfold Val.cmpu_bool, Val.cmplu_bool; rewrite SF; reflexivity.
+  - destruct c0; simpl; try congruence;
+    intros SF; auto; rewrite ? negb_false_iff in SF;
+      unfold Val.cmpu_bool, Val.cmplu_bool; rewrite SF; reflexivity.
 Qed.
 
 (** Global variables mentioned in an operation or addressing mode *)
@@ -1591,6 +1611,22 @@ Proof.
       symmetry.
       eapply eval_condition0_inj; eassumption.
     + left. trivial.
+
+ (* Oselimm *)
+  - apply Val.select_inject; trivial.
+    destruct (eval_condition0 c0 v2 m1) eqn:Hcond.
+    + right.
+      symmetry.
+      eapply eval_condition0_inj; eassumption.
+    + left. trivial.
+
+ (* Osellimm *)
+  - apply Val.select_inject; trivial.
+    destruct (eval_condition0 c0 v2 m1) eqn:Hcond.
+    + right.
+      symmetry.
+      eapply eval_condition0_inj; eassumption.
+    + left. trivial.
 Qed.
 
 Lemma eval_addressing_inj: