begin osel imm

3 files changed, 57 insertions, 3 deletions

diff --git a/mppa_k1c/NeedOp.v b/mppa_k1c/NeedOp.v
index 047c180a..4748f38b 100644
--- a/mppa_k1c/NeedOp.v
+++ b/mppa_k1c/NeedOp.v
@@ -133,6 +133,8 @@ Definition needs_of_operation (op: operation) (nv: nval): list nval :=
   | Oextfz _ _ | Oextfs _ _  | Oextfzl _ _ | Oextfsl _ _ => op1 (default nv)
   | Oinsf _ _ | Oinsfl _ _ => op2 (default nv)
   | Osel c ty => nv :: nv :: needs_of_condition0 c
+  | Oselimm c imm
+  | Osellimm c imm => nv :: needs_of_condition0 c
   end.
 
 Definition operation_is_redundant (op: operation) (nv: nval): bool :=
@@ -347,6 +349,16 @@ Proof.
   erewrite needs_of_condition0_sound by eauto.
   apply select_sound; auto.
   simpl; auto with na.
+  (* select imm *)
+- destruct (eval_condition0 _ _ _) as [b|] eqn:EC.
+  { erewrite needs_of_condition0_sound by eauto.
+  apply select_sound; auto with na. }
+  simpl; auto with na.
+  (* select long imm *)
+- destruct (eval_condition0 _ _ _) as [b|] eqn:EC.
+  { erewrite needs_of_condition0_sound by eauto.
+  apply select_sound; auto with na. }
+  simpl; auto with na.
 Qed.
 
 Lemma operation_is_redundant_sound:
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:
diff --git a/mppa_k1c/ValueAOp.v b/mppa_k1c/ValueAOp.v
index d24cebcc..daceab8b 100644
--- a/mppa_k1c/ValueAOp.v
+++ b/mppa_k1c/ValueAOp.v
@@ -265,6 +265,8 @@ Definition eval_static_operation (op: operation) (vl: list aval): aval :=
   | (Oinsf stop start), v0::v1::nil => eval_static_insf stop start v0 v1
   | (Oinsfl stop start), v0::v1::nil => eval_static_insfl stop start v0 v1
   | Osel c ty, v1::v2::vc::nil => select (eval_static_condition0 c vc) v1 v2
+  | Oselimm c imm, v1::v2::vc::nil => select (eval_static_condition0 c vc) v1 (I imm)
+  | Osellimm c imm, v1::v2::vc::nil => select (eval_static_condition0 c vc) v1 (L imm)
   | _, _ => Vbot
   end.
 
@@ -421,6 +423,10 @@ Proof.
     + constructor.
     (* select *)
   - apply select_sound; auto. eapply eval_static_condition0_sound; eauto.
+    (* select imm *)
+  - apply select_sound; auto with va. eapply eval_static_condition0_sound; eauto.
+    (* select long imm *)
+  - apply select_sound; auto with va. eapply eval_static_condition0_sound; eauto.
 Qed.
 
 End SOUNDNESS.