osel imm

8 files changed, 117 insertions, 23 deletions

diff --git a/mppa_k1c/Asmblockgen.v b/mppa_k1c/Asmblockgen.v
index 04ce13e7..e5b9b35a 100644
--- a/mppa_k1c/Asmblockgen.v
+++ b/mppa_k1c/Asmblockgen.v
@@ -375,6 +375,34 @@ Definition conditional_move (cond0 : condition0) (rc rd rs : ireg) :
          OK (PArith (Pcmoveu bt rd rc rs))
      end).
 
+Definition conditional_move_imm32 (cond0 : condition0) (rc rd : ireg) (imm : int) : res basic :=
+  match cond0 with
+  | Ccomp0 cmp =>
+    OK (PArith (Pcmoveiw (btest_for_cmpswz cmp) rd rc imm))
+  | Ccompu0 cmp =>
+    do bt <- btest_for_cmpuwz cmp;
+      OK (PArith (Pcmoveuiw bt rd rc imm))
+  | Ccompl0 cmp =>
+    OK (PArith (Pcmoveiw (btest_for_cmpsdz cmp) rd rc imm))
+  | Ccomplu0 cmp =>
+    do bt <- btest_for_cmpudz cmp;
+      OK (PArith (Pcmoveuiw bt rd rc imm))
+  end.
+
+Definition conditional_move_imm64 (cond0 : condition0) (rc rd : ireg) (imm : int64) : res basic :=
+  match cond0 with
+  | Ccomp0 cmp =>
+    OK (PArith (Pcmoveil (btest_for_cmpswz cmp) rd rc imm))
+  | Ccompu0 cmp =>
+    do bt <- btest_for_cmpuwz cmp;
+      OK (PArith (Pcmoveuil bt rd rc imm))
+  | Ccompl0 cmp =>
+    OK (PArith (Pcmoveil (btest_for_cmpsdz cmp) rd rc imm))
+  | Ccomplu0 cmp =>
+    do bt <- btest_for_cmpudz cmp;
+      OK (PArith (Pcmoveuil bt rd rc imm))
+  end.
+
 Definition transl_cond_op
            (cond: condition) (rd: ireg) (args: list mreg) (k: bcode) :=
   match cond, args with
@@ -847,6 +875,21 @@ Definition transl_op
       do rC <- ireg_of aC;
       do op <- conditional_move (negate_condition0 cond0) rC rT rF;
       OK (op ::i k)
+
+  | Oselimm cond0 imm, aT :: aC :: nil =>
+    assertion (mreg_eq aT res);
+      do rT <- ireg_of aT;
+      do rC <- ireg_of aC;
+      do op <- conditional_move_imm32 (negate_condition0 cond0) rC rT imm;
+      OK (op ::i k)
+      
+
+  | Osellimm cond0 imm, aT :: aC :: nil =>
+    assertion (mreg_eq aT res);
+      do rT <- ireg_of aT;
+      do rC <- ireg_of aC;
+      do op <- conditional_move_imm64 (negate_condition0 cond0) rC rT imm;
+      OK (op ::i k)
       
   | _, _ =>
       Error(msg "Asmgenblock.transl_op")
diff --git a/mppa_k1c/Asmblockgenproof1.v b/mppa_k1c/Asmblockgenproof1.v
index 8939cc30..bc549b4a 100644
--- a/mppa_k1c/Asmblockgenproof1.v
+++ b/mppa_k1c/Asmblockgenproof1.v
@@ -1799,6 +1799,54 @@ Opaque Int.eq.
     try destruct (_ || _);
     trivial;
     try apply Val.lessdef_normalize.
+
+- (* Oselimm *)
+  unfold conditional_move_imm32 in *.
+  destruct c0; simpl in *.
+
+  all:
+    destruct c; simpl in *; inv EQ0;
+    econstructor; split; try (apply exec_straight_one; constructor);
+    split; try (simpl; intros; rewrite Pregmap.gso; trivial; assumption);
+    unfold Val.select; simpl;
+    unfold cmove, cmoveu;   
+    rewrite Pregmap.gss;
+    destruct (rs x0); simpl; trivial;
+    try rewrite int_ltu_to_neq;
+    try rewrite int64_ltu_to_neq;
+    try change (Int64.eq Int64.zero Int64.zero) with true;
+    try destruct Archi.ptr64;
+    repeat rewrite if_neg;
+    simpl;
+    trivial;
+    try destruct (_ || _);
+    trivial;
+    try apply Val.lessdef_normalize.
+
+
+- (* Osellimm *)
+  unfold conditional_move_imm64 in *.
+  destruct c0; simpl in *.
+
+  all:
+    destruct c; simpl in *; inv EQ0;
+    econstructor; split; try (apply exec_straight_one; constructor);
+    split; try (simpl; intros; rewrite Pregmap.gso; trivial; assumption);
+    unfold Val.select; simpl;
+    unfold cmove, cmoveu;   
+    rewrite Pregmap.gss;
+    destruct (rs x0); simpl; trivial;
+    try rewrite int_ltu_to_neq;
+    try rewrite int64_ltu_to_neq;
+    try change (Int64.eq Int64.zero Int64.zero) with true;
+    try destruct Archi.ptr64;
+    repeat rewrite if_neg;
+    simpl;
+    trivial;
+    try destruct (_ || _);
+    trivial;
+    try apply Val.lessdef_normalize.
+
 Qed.
 
 (** Memory accesses *)
diff --git a/mppa_k1c/Machregs.v b/mppa_k1c/Machregs.v
index ee3a63c7..5a7d42b4 100644
--- a/mppa_k1c/Machregs.v
+++ b/mppa_k1c/Machregs.v
@@ -216,7 +216,7 @@ Definition two_address_op (op: operation) : bool :=
   | Omadd | Omaddimm _
   | Omaddl | Omaddlimm _
   | Omsub | Omsubl
-  | Osel _ _
+  | Osel _ _ | Oselimm _ _ | Osellimm _ _
   | Oinsf _ _ | Oinsfl _ _ => true
   | _ => false
   end.
diff --git a/mppa_k1c/Op.v b/mppa_k1c/Op.v
index 1b3a839f..35fbb596 100644
--- a/mppa_k1c/Op.v
+++ b/mppa_k1c/Op.v
@@ -456,8 +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)
+  | Oselimm c imm, v1::vc::nil => Some(Val.select (eval_condition0 c vc m) v1 (Vint imm) Tint)
+  | Osellimm c imm, v1::vc::nil => Some(Val.select (eval_condition0 c vc m) v1 (Vlong imm) Tlong)
   | _, _ => None
   end.
 
@@ -662,8 +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)
+  | Oselimm c ty => (Tint :: arg_type_of_condition0 c :: nil, Tint)
+  | Osellimm c ty => (Tlong :: arg_type_of_condition0 c :: nil, Tlong)
   end.
 
 (* FIXME: two Tptr ?! *)
@@ -1614,7 +1614,7 @@ Proof.
 
  (* Oselimm *)
   - apply Val.select_inject; trivial.
-    destruct (eval_condition0 c0 v2 m1) eqn:Hcond.
+    destruct (eval_condition0 _ _ _) eqn:Hcond.
     + right.
       symmetry.
       eapply eval_condition0_inj; eassumption.
@@ -1622,7 +1622,7 @@ Proof.
 
  (* Osellimm *)
   - apply Val.select_inject; trivial.
-    destruct (eval_condition0 c0 v2 m1) eqn:Hcond.
+    destruct (eval_condition0 _ _ _) eqn:Hcond.
     + right.
       symmetry.
       eapply eval_condition0_inj; eassumption.
diff --git a/mppa_k1c/PostpassSchedulingOracle.ml b/mppa_k1c/PostpassSchedulingOracle.ml
index 78af896a..6ccc4e97 100644
--- a/mppa_k1c/PostpassSchedulingOracle.ml
+++ b/mppa_k1c/PostpassSchedulingOracle.ml
@@ -551,7 +551,7 @@ let ab_inst_to_real = function
   | "Pfixedudrzz" -> Fixedudz
   | "Pfixeddrzz_i32" -> Fixeddz
   | "Pfixedudrzz_i32" -> Fixedudz
-  | "Pcmove" | "Pcmoveu" -> Cmoved
+  | "Pcmove" | "Pcmoveu"   | "Pcmoveiw" | "Pcmoveuiw" | "Pcmoveil" | "Pcmoveuil" -> Cmoved
   
   | "Plb" -> Lbs
   | "Plbu" -> Lbz
diff --git a/mppa_k1c/SelectOp.vp b/mppa_k1c/SelectOp.vp
index 01985060..2618983b 100644
--- a/mppa_k1c/SelectOp.vp
+++ b/mppa_k1c/SelectOp.vp
@@ -91,8 +91,14 @@ Nondetfunction cond_to_condition0 (cond : condition) (args : exprlist) :=
   end.
   
 (** Ternary operator *)
-Definition select0 (ty : typ) (cond0 : condition0) (e1 e2 eC: expr) :=
-  (Eop (Osel cond0 ty) (e1 ::: e2 ::: eC ::: Enil)).
+Nondetfunction select0 (ty : typ) (cond0 : condition0) (e1 e2 e3: expr) :=
+  match ty, cond0, e1, e2, e3 with
+  | Tint, cond0, e1, (Eop (Ointconst imm) Enil), e3 =>
+    (Eop (Oselimm cond0 imm) (e1 ::: e3 ::: Enil))
+  | Tlong, cond0, e1, (Eop (Olongconst imm) Enil), e3 =>
+    (Eop (Osellimm cond0 imm) (e1 ::: e3 ::: Enil))
+  | _, _, _ => (Eop (Osel cond0 ty) (e1 ::: e2 ::: e3 ::: Enil))
+  end.
 
 Definition select (ty : typ) (cond : condition) (args : exprlist) (e1 e2: expr)  : option expr :=
   Some(
diff --git a/mppa_k1c/SelectOpproof.v b/mppa_k1c/SelectOpproof.v
index 4047048c..39ad763e 100644
--- a/mppa_k1c/SelectOpproof.v
+++ b/mppa_k1c/SelectOpproof.v
@@ -1451,12 +1451,10 @@ Lemma eval_select0:
   /\ Val.lessdef (Val.select (eval_condition0 cond0 vc m) v1 v2 ty) v.
 Proof.
   intros.
-  econstructor; split.
-  {
-    unfold select0.
-    repeat (try econstructor; try eassumption).
-  }
-  constructor.
+  unfold select0.
+  destruct (select0_match ty cond0 a1 a2 ac).
+  all: InvEval; econstructor; split;
+        repeat (try econstructor; try eassumption).
 Qed.
 
 Lemma bool_cond0_ne:
@@ -1578,12 +1576,11 @@ Proof.
     erewrite <- (bool_cond0_ne (Val.cmplu_bool (Mem.valid_pointer m) c v0 (Vlong x))).
     eapply eval_select0; repeat (try econstructor; try eassumption).
   }
-  TrivialExists.
-  repeat (try econstructor; try eassumption).
+  erewrite <- (bool_cond0_ne (Some b)).
+  eapply eval_select0; repeat (try econstructor; try eassumption).
+  rewrite <- HeC.
   simpl.
-  f_equal.
-  rewrite HeC.
-  destruct b; simpl; reflexivity.
+  reflexivity.
 Qed.
 
 (* floating-point division *)
diff --git a/mppa_k1c/ValueAOp.v b/mppa_k1c/ValueAOp.v
index daceab8b..439138da 100644
--- a/mppa_k1c/ValueAOp.v
+++ b/mppa_k1c/ValueAOp.v
@@ -265,8 +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)
+  | Oselimm c imm, v1::vc::nil => select (eval_static_condition0 c vc) v1 (I imm)
+  | Osellimm c imm, v1::vc::nil => select (eval_static_condition0 c vc) v1 (L imm)
   | _, _ => Vbot
   end.