Osel -> assembleur

3 files changed, 112 insertions, 104 deletions

diff --git a/mppa_k1c/Asmblockgen.v b/mppa_k1c/Asmblockgen.v
index 33fa39b5..72d7394b 100644
--- a/mppa_k1c/Asmblockgen.v
+++ b/mppa_k1c/Asmblockgen.v
@@ -334,6 +334,47 @@ Definition transl_cond_notfloat64 (cmp: comparison) (rd r1 r2: ireg) (k: bcode)
   | Reversed ft => Pfcompl ft rd r2 r1 ::i k
   end.
 
+
+(* CoMPare Unsigned Words to Zero *)
+Definition btest_for_cmpuwz (c: comparison) :=
+  match c with
+  | Cne => OK BTwnez
+  | Ceq => OK BTweqz
+  | Clt => Error (msg "btest_for_compuwz: Clt")
+  | Cge => Error (msg "btest_for_compuwz: Cge")
+  | Cle => Error (msg "btest_for_compuwz: Cle")
+  | Cgt => Error (msg "btest_for_compuwz: Cgt")
+  end.
+
+(* CoMPare Unsigned Words to Zero *)
+Definition btest_for_cmpudz (c: comparison) :=
+  match c with
+  | Cne => OK BTdnez
+  | Ceq => OK BTdeqz
+  | Clt => Error (msg "btest_for_compudz: Clt")
+  | Cge => Error (msg "btest_for_compudz: Cge")
+  | Cle => Error (msg "btest_for_compudz: Cle")
+  | Cgt => Error (msg "btest_for_compudz: Cgt")
+  end.
+
+Definition conditional_move (cond0 : condition0) (rc rd rs : ireg) :
+  res basic :=
+  if ireg_eq rd rs
+  then OK Pnop
+  else
+    (match cond0 with
+     | Ccomp0 cmp =>
+       OK (PArith (Pcmove (btest_for_cmpswz cmp) rd rc rs))
+     | Ccompu0 cmp =>
+       do bt <- btest_for_cmpuwz cmp;
+         OK (PArith (Pcmoveu bt rd rc rs))
+     | Ccompl0 cmp =>
+       OK (PArith (Pcmove (btest_for_cmpsdz cmp) rd rc rs))
+     | Ccomplu0 cmp =>
+       do bt <- btest_for_cmpudz cmp;
+         OK (PArith (Pcmoveu bt rd rc rs))
+     end).
+
 Definition transl_cond_op
            (cond: condition) (rd: ireg) (args: list mreg) (k: bcode) :=
   match cond, args with
@@ -377,28 +418,6 @@ Definition transl_cond_op
       Error(msg "Asmblockgen.transl_cond_op")
 end.
 
-(* CoMPare Unsigned Words to Zero *)
-Definition btest_for_cmpuwz (c: comparison) :=
-  match c with
-  | Cne => OK BTwnez
-  | Ceq => OK BTweqz
-  | Clt => Error (msg "btest_for_compuwz: Clt")
-  | Cge => Error (msg "btest_for_compuwz: Cge")
-  | Cle => Error (msg "btest_for_compuwz: Cle")
-  | Cgt => Error (msg "btest_for_compuwz: Cgt")
-  end.
-
-(* CoMPare Unsigned Words to Zero *)
-Definition btest_for_cmpudz (c: comparison) :=
-  match c with
-  | Cne => OK BTdnez
-  | Ceq => OK BTdeqz
-  | Clt => Error (msg "btest_for_compudz: Clt")
-  | Cge => Error (msg "btest_for_compudz: Cge")
-  | Cle => Error (msg "btest_for_compudz: Cle")
-  | Cgt => Error (msg "btest_for_compudz: Cgt")
-  end.
-
 (** Translation of the arithmetic operation [r <- op(args)].
   The corresponding instructions are prepended to [k]. *)
 
@@ -821,6 +840,14 @@ Definition transl_op
       do rd  <- ireg_of res; do rs <- ireg_of a1;
       OK (Pinsfl stop start rd rs ::i k)
 
+  | Osel cond0 ty, aT :: aF :: aC :: nil =>
+    assertion (mreg_eq aT res);
+      do rT <- ireg_of aT;
+      do rF <- ireg_of aF;
+      do rC <- ireg_of aC;
+      do op <- conditional_move (negate_condition0 cond0) rC rT rF;
+      OK (op ::i k)
+      
   | _, _ =>
       Error(msg "Asmgenblock.transl_op")
   end.
diff --git a/mppa_k1c/Asmblockgenproof1.v b/mppa_k1c/Asmblockgenproof1.v
index 8125741b..86e640c9 100644
--- a/mppa_k1c/Asmblockgenproof1.v
+++ b/mppa_k1c/Asmblockgenproof1.v
@@ -1649,6 +1649,25 @@ Proof.
   destruct (Z.eq_dec _ _); destruct (Z.eq_dec _ _); congruence.
 Qed.
 
+Lemma select_same_lessdef:
+  forall ty c v,
+    Val.lessdef (Val.select c v v ty) v.
+Proof.
+  intros.
+  unfold Val.select.
+  destruct c; try econstructor.
+  replace (if b then v else v) with v by (destruct b ; trivial).
+  destruct v; destruct ty; simpl; econstructor.
+Qed.
+
+Lemma if_neg : forall X,
+    forall a,
+    forall b c : X,
+    (if (negb a) then b else c) = (if a then c else b).
+Proof.
+  destruct a; reflexivity.
+Qed.
+
 Lemma transl_op_correct:
   forall op args res k (rs: regset) m v c,
   transl_op op args res k = OK c ->
@@ -1719,6 +1738,44 @@ Opaque Int.eq.
 - (* Ocmp *)
   exploit transl_cond_op_correct; eauto. intros (rs' & A & B & C).
   exists rs'; split. eexact A. eauto with asmgen.
+- (* Osel *)
+  unfold conditional_move in *.
+  destruct (ireg_eq _ _).
+  {
+    subst x. inv EQ2.
+    econstructor; split.
+    {
+      apply exec_straight_one.
+      simpl. reflexivity.
+    }
+    split.
+    { apply select_same_lessdef. } 
+    intros; trivial.
+  }
+
+  destruct c0; simpl in *.
+  1, 2, 3:
+    destruct c; simpl in *; inv EQ2;
+    econstructor; split; try (apply exec_straight_one; constructor);
+    split; try (simpl; intros; rewrite Pregmap.gso; trivial; assumption);
+    unfold Val.select; simpl;
+    rewrite Pregmap.gss;
+    destruct (rs x1); simpl; trivial;
+    rewrite if_neg;
+    apply Val.lessdef_normalize.
+  
+    destruct c; simpl in *; inv EQ2;
+    econstructor; split; try (apply exec_straight_one; constructor);
+    split; try (simpl; intros; rewrite Pregmap.gso; trivial; assumption);
+    unfold Val.select; simpl;
+    rewrite Pregmap.gss;
+    destruct (rs x1); simpl; trivial;
+    rewrite if_neg;
+    try apply Val.lessdef_normalize;
+    
+    destruct Archi.ptr64; simpl; replace (Int64.eq Int64.zero Int64.zero) with true by reflexivity; simpl; trivial;
+    destruct (_ || _); trivial;
+    apply Val.lessdef_normalize.
 Qed.
 
 (** Memory accesses *)
diff --git a/mppa_k1c/Op.v b/mppa_k1c/Op.v
index c7c04d83..be7ea812 100644
--- a/mppa_k1c/Op.v
+++ b/mppa_k1c/Op.v
@@ -301,90 +301,14 @@ Definition eval_condition0 (cond: condition0) (v1: val) (m: mem): option bool :=
   | Ccomplu0 c => Val.cmplu_bool (Mem.valid_pointer m) c v1 (Vlong Int64.zero)
   end.
 
-Definition eval_selecti (cond : condition0) (v0 : val) (v1 : val) (vselect : val) (m: mem) : val :=
-  match v0, v1, (eval_condition0 cond vselect m) with
-    | Vint i0, Vint i1, Some bval => Vint (if bval then i1 else i0)
-    | _,_,_ => Vundef
+Definition negate_condition0 (cond0 : condition0) : condition0 :=
+  match cond0 with
+  | Ccomp0 c => Ccomp0 (negate_comparison c)
+  | Ccompu0 c => Ccompu0 (negate_comparison c)
+  | Ccompl0 c => Ccompl0 (negate_comparison c)
+  | Ccomplu0 c => Ccomplu0 (negate_comparison c)
   end.
 
-Definition eval_selecti2 (cond : condition0) (v0 : val) (v1 : val) (vselect : val) (m: mem) : val :=
-  match (eval_condition0 cond vselect m), v0, v1 with
-    | Some bval, Vint i0, Vint i1 => Vint (if bval then i1 else i0)
-    | _,_,_ => Vundef
-  end.
-
-Lemma eval_selecti_to2: forall cond v0 v1 vselect m,
-    (eval_selecti cond v0 v1 vselect m) =
-    (eval_selecti2 cond v0 v1 vselect m).
-Proof.
-  intros.
-  unfold eval_selecti2.
-  destruct v0; destruct v1; simpl; destruct (eval_condition0 cond vselect m); simpl; reflexivity.
-Qed.
-
-Definition eval_selectl (cond: condition0) (v0 : val) (v1 : val) (vselect : val) (m: mem) : val :=
-  match v0, v1, (eval_condition0 cond vselect m) with
-    | Vlong i0, Vlong i1, Some bval => Vlong (if bval then i1 else i0)
-    | _,_,_ => Vundef
-  end.
-
-Definition eval_selectl2 (cond : condition0) (v0 : val) (v1 : val) (vselect : val) (m: mem) : val :=
-  match (eval_condition0 cond vselect m), v0, v1 with
-    | Some bval, Vlong i0, Vlong i1 => Vlong (if bval then i1 else i0)
-    | _,_,_ => Vundef
-  end.
-
-Lemma eval_selectl_to2: forall cond v0 v1 vselect m,
-    (eval_selectl cond v0 v1 vselect m) =
-    (eval_selectl2 cond v0 v1 vselect m).
-Proof.
-  intros.
-  unfold eval_selectl2.
-  destruct v0; destruct v1; simpl; destruct (eval_condition0 cond vselect m); simpl; reflexivity.
-Qed.
-
-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_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 :=