Implement a `Osel` operation for PowerPC

This operation compiles down to an `isel` instruction (conditional move).
The semantics is given by `Val.select`.

7 files changed, 106 insertions, 9 deletions

diff --git a/powerpc/Asmgen.v b/powerpc/Asmgen.v
index dba24a5a..62efc17f 100644
--- a/powerpc/Asmgen.v
+++ b/powerpc/Asmgen.v
@@ -404,6 +404,18 @@ Definition transl_cond_op
          else Pxori r' r' (Cint Int.one) :: k)
   end.
 
+(** Translation of a select operation *)
+
+Definition transl_select_op
+              (cond: condition) (args: list mreg) (r1 r2 rd: ireg) (k: code) :=
+  if ireg_eq r1 r2 then
+    OK (Pmr rd r1 :: k)
+  else
+   (let p := crbit_for_cond cond in
+    let r1' := if snd p then r1 else r2 in
+    let r2' := if snd p then r2 else r1 in
+    transl_cond cond args (Pisel rd r1' r2' (fst p) :: k)).
+
 (** Translation of the arithmetic operation [r <- op(args)].
   The corresponding instructions are prepended to [k]. *)
 
@@ -610,6 +622,10 @@ Definition transl_op
       do r1 <- ireg_of a1; do r <- ireg_of res; OK (Plhi r r1 :: k)
   | Ocmp cmp, _ =>
       transl_cond_op cmp args res k
+  | Osel cmp ty, a1 :: a2 :: args =>
+      assertion (typ_eq ty Tint || typ_eq ty Tlong);
+      do r1 <- ireg_of a1; do r2 <- ireg_of a2; do r <- ireg_of res;
+      transl_select_op cmp args r1 r2 r k
 (*c PPC64 operations *)
   | Olongconst n, nil =>
       do r <- ireg_of res; OK (loadimm64 r n k)
diff --git a/powerpc/Asmgenproof.v b/powerpc/Asmgenproof.v
index d0d82cb5..4d0b41ba 100644
--- a/powerpc/Asmgenproof.v
+++ b/powerpc/Asmgenproof.v
@@ -248,6 +248,15 @@ Proof.
   destruct (snd (crbit_for_cond c0)); TailNoLabel.
 Qed.
 
+Remark transl_select_op_label:
+  forall cond args r1 r2 rd k c,
+  transl_select_op cond args r1 r2 rd k = OK c -> tail_nolabel k c.
+Proof.
+  unfold transl_select_op; intros. destruct (ireg_eq r1 r2).
+  TailNoLabel.
+  eapply tail_nolabel_trans. eapply transl_cond_label; eauto.  TailNoLabel.
+Qed.
+
 Remark transl_op_label:
   forall op args r k c,
   transl_op op args r k = OK c -> tail_nolabel k c.
@@ -275,6 +284,7 @@ Opaque Int.eq.
   destruct Int64.eq. TailNoLabel.
   destruct ireg_eq; [apply tail_nolabel_cons; unfold nolabel;auto|]; eapply tail_nolabel_trans; TailNoLabel.
 - eapply transl_cond_op_label; eauto.
+- eapply transl_select_op_label; eauto.
 Qed.
 
 Remark transl_memory_access_label:
diff --git a/powerpc/Asmgenproof1.v b/powerpc/Asmgenproof1.v
index b891e42f..8c9fd2bd 100644
--- a/powerpc/Asmgenproof1.v
+++ b/powerpc/Asmgenproof1.v
@@ -1258,6 +1258,35 @@ Proof.
   intuition Simpl.
   rewrite RES1. destruct (eval_condition c rs ## (preg_of ## rl) m). destruct b; auto. auto.
 Qed.
+  
+Lemma transl_select_op_correct:
+  forall cond args ty r1 r2 rd k rs m c,
+  transl_select_op cond args r1 r2 rd k = OK c ->
+  important_preg r1 = true -> important_preg r2 = true ->
+  exists rs',
+  exec_straight ge fn c rs m k rs' m
+  /\ Val.lessdef (Val.select (eval_condition cond (map rs (map preg_of args)) m) rs#r1 rs#r2 ty) rs'#rd
+  /\ forall r, important_preg r = true  -> r <> rd -> rs'#r = rs#r.
+Proof.
+  intros until c.  intros TR IMP1 IMP2.
+  unfold transl_select_op in TR.
+  destruct (ireg_eq r1 r2).
+  - inv TR. econstructor; split; [|split].
+    + apply exec_straight_one. simpl; eauto. auto.
+    + Simpl. destruct (eval_condition cond rs ## (preg_of ## args) m) as [[]|]; simpl; auto using Val.lessdef_normalize.
+    + intros; Simpl.
+  - destruct (transl_cond_correct_1 cond args _ rs m _ TR) as (rs1 & A & B & C).
+    set (bit := fst (crbit_for_cond cond)) in *.
+    set (dir := snd (crbit_for_cond cond)) in *.
+    set (ob := eval_condition cond rs##(preg_of##args) m) in *.
+    econstructor; split; [|split].
+    + eapply exec_straight_trans. eexact A. apply exec_straight_one. simpl; eauto.
+      reflexivity.
+    + Simpl.
+      rewrite <- (C r1), <- (C r2) by auto.
+      rewrite B. destruct dir; destruct ob as [[]|]; simpl; auto using Val.lessdef_normalize.
+    + intros. Simpl.
+Qed.
 
 (** Translation of arithmetic operations. *)
 
@@ -1455,6 +1484,12 @@ Opaque Val.add.
   (* Ocmp *)
 - destruct (transl_cond_op_correct c0 args res k rs m c) as [rs' [A [B C]]]; auto.
   exists rs'; auto with asmgen.
+  (* Osel *)
+- assert (X: forall mr r, ireg_of mr = OK r -> important_preg r = true).
+  { intros. apply ireg_of_eq in H. apply important_data_preg_1. rewrite <- H.
+    auto with asmgen. }
+  destruct (transl_select_op_correct _ _ t _ _ _ _ rs m _ EQ3) as (rs' & A & B & C);
+  eauto.
 Qed.
 
 Lemma transl_op_correct:
diff --git a/powerpc/NeedOp.v b/powerpc/NeedOp.v
index 9a579cc5..5ea09bd8 100644
--- a/powerpc/NeedOp.v
+++ b/powerpc/NeedOp.v
@@ -65,6 +65,7 @@ Definition needs_of_operation (op: operation) (nv: nval): list nval :=
   | Ofloatofwords | Omakelong => op2 (default nv)
   | Olowlong | Ohighlong => op1 (default nv)
   | Ocmp c => needs_of_condition c
+  | Osel c ty => nv :: nv :: needs_of_condition c
   end.
 
 Definition operation_is_redundant (op: operation) (nv: nval): bool :=
@@ -147,6 +148,10 @@ Proof.
   erewrite needs_of_condition_sound by eauto.
   subst v; simpl. auto with na.
   subst v; auto with na.
+- destruct (eval_condition c args m) as [b|] eqn:EC.
+  erewrite needs_of_condition_sound by eauto.
+  apply select_sound; auto.
+  simpl; auto with na.
 Qed.
 
 Lemma operation_is_redundant_sound:
diff --git a/powerpc/Op.v b/powerpc/Op.v
index e6f942c1..0f082c1f 100644
--- a/powerpc/Op.v
+++ b/powerpc/Op.v
@@ -150,8 +150,9 @@ Inductive operation : Type :=
   | Olowlong: operation                 (**r [rd = low-word(r1)] *)
   | Ohighlong: operation                (**r [rd = high-word(r1)] *)
 (*c Boolean tests: *)
-  | Ocmp: condition -> operation.       (**r [rd = 1] if condition holds, [rd = 0] otherwise. *)
-
+  | Ocmp: condition -> operation        (**r [rd = 1] if condition holds, [rd = 0] otherwise. *)
+  | Osel: condition -> typ -> operation.
+                                        (**r [rd = rs1] if condition holds, [rd = rs2] otherwise. *)
 
 (** Addressing modes.  [r1], [r2], etc, are the arguments to the
   addressing. *)
@@ -173,7 +174,7 @@ Proof.
 Defined.
 
 Definition beq_operation: forall (x y: operation), bool.
-  generalize Int.eq_dec Int64.eq_dec Ptrofs.eq_dec ident_eq Float.eq_dec Float32.eq_dec  eq_condition; boolean_equality.
+  generalize Int.eq_dec Int64.eq_dec Ptrofs.eq_dec ident_eq Float.eq_dec Float32.eq_dec typ_eq eq_condition; boolean_equality.
 Defined.
 
 Definition eq_operation (x y: operation): {x=y} + {x<>y}.
@@ -306,6 +307,7 @@ Definition eval_operation
   | Olowlong, v1::nil => Some(Val.loword v1)
   | Ohighlong, v1::nil => Some(Val.hiword v1)
   | Ocmp c, _ => Some(Val.of_optbool (eval_condition c vl m))
+  | Osel c ty, v1::v2::vl => Some(Val.select (eval_condition c vl m) v1 v2 ty)
   | _, _ => None
   end.
 
@@ -455,6 +457,7 @@ Definition type_of_operation (op: operation) : list typ * typ :=
   | Olowlong => (Tlong :: nil, Tint)
   | Ohighlong => (Tlong :: nil, Tint)
   | Ocmp c => (type_of_condition c, Tint)
+  | Osel c ty => (ty :: ty :: type_of_condition c, ty)
   end.
 
 Definition type_of_addressing (addr: addressing) : list typ :=
@@ -575,6 +578,7 @@ Proof with (try exact I; try reflexivity).
   destruct v0...
   destruct v0...
   destruct (eval_condition c vl m); simpl... destruct b...
+  unfold Val.select. destruct (eval_condition c vl m). apply Val.normalize_type. exact I.
 Qed.
 
 End SOUNDNESS.
@@ -727,22 +731,40 @@ Definition is_trivial_op (op: operation) : bool :=
 
 (** Operations that depend on the memory state. *)
 
+Definition condition_depends_on_memory (c: condition) : bool :=
+  match c with
+  | Ccompu _ => true
+  | Ccompuimm _ _ => true
+  | Ccomplu _ => Archi.ppc64
+  | Ccompluimm _ _ => Archi.ppc64
+  | _ => false
+  end.
+
 Definition op_depends_on_memory (op: operation) : bool :=
   match op with
-  | Ocmp (Ccompu _) => true
-  | Ocmp (Ccompuimm _ _) => true
-  | Ocmp (Ccomplu _) => Archi.ppc64
-  | Ocmp (Ccompluimm _ _) => Archi.ppc64
+  | Ocmp c => condition_depends_on_memory c
+  | Osel c ty => condition_depends_on_memory c
   | _ => false
   end.
 
+Lemma condition_depends_on_memory_correct:
+  forall c args m1 m2,
+  condition_depends_on_memory c = false ->
+  eval_condition c args m1 = eval_condition c args m2.
+Proof.
+  intros. destruct c; simpl; auto; discriminate.
+Qed.
+
 Lemma op_depends_on_memory_correct:
   forall (F V: Type) (ge: Genv.t F V) sp op args m1 m2,
   op_depends_on_memory op = false ->
   eval_operation ge sp op args m1 = eval_operation ge sp op args m2.
 Proof.
-  intros until m2. destruct op; simpl; try congruence. unfold eval_condition.
-  destruct c; simpl; auto; try discriminate.
+  intros until m2. destruct op; simpl; try congruence; intros C.
+- f_equal; f_equal; apply condition_depends_on_memory_correct; auto.
+- destruct args; auto. destruct args; auto.
+  rewrite (condition_depends_on_memory_correct c args m1 m2 C).
+  auto.
 Qed.
 
 (** Global variables mentioned in an operation or addressing mode *)
@@ -989,6 +1011,9 @@ Proof.
   exploit eval_condition_inj; eauto. intros EQ; rewrite EQ.
   destruct b; simpl; constructor.
   simpl; constructor.
+  apply Val.select_inject; auto.  
+  destruct (eval_condition c vl1 m1) eqn:?; auto.
+  right; symmetry; eapply eval_condition_inj; eauto.
 Qed.
 
 Lemma eval_addressing_inj:
diff --git a/powerpc/PrintOp.ml b/powerpc/PrintOp.ml
index cffaafdb..8d7f17ab 100644
--- a/powerpc/PrintOp.ml
+++ b/powerpc/PrintOp.ml
@@ -110,6 +110,10 @@ let print_operation reg pp = function
   | Olowlong, [r1] -> fprintf pp "lowlong(%a)" reg r1
   | Ohighlong, [r1] -> fprintf pp "highlong(%a)" reg r1
   | Ocmp c, args -> print_condition reg pp (c, args)
+  | Osel (c, ty), r1::r2::args ->
+      fprintf pp "%a ?%s %a : %a"
+         (print_condition reg) (c, args)
+         (PrintAST.name_of_type ty) reg r1 reg r2
   | Olongconst n, [] -> fprintf pp "%LdL" (camlint64_of_coqint n)
   | Ocast32signed, [r1] -> fprintf pp "int32signed(%a)" reg r1
   | Ocast32unsigned, [r1] -> fprintf pp "int32unsigned(%a)" reg r1
diff --git a/powerpc/ValueAOp.v b/powerpc/ValueAOp.v
index f7f65e9e..a270d857 100644
--- a/powerpc/ValueAOp.v
+++ b/powerpc/ValueAOp.v
@@ -141,6 +141,7 @@ Definition eval_static_operation (op: operation) (vl: list aval): aval :=
   | Olowlong, v1::nil => loword v1
   | Ohighlong, v1::nil => hiword v1
   | Ocmp c, _ => of_optbool (eval_static_condition c vl)
+  | Osel c ty, v1::v2::vl => select (eval_static_condition c vl) v1 v2
   | _, _ => Vbot
   end.
 
@@ -211,6 +212,7 @@ Proof.
   apply rolml_sound; auto.
   apply floatofwords_sound; auto.
   apply of_optbool_sound. eapply eval_static_condition_sound; eauto.
+  apply select_sound; auto. eapply eval_static_condition_sound; eauto.
 Qed.
 
 End SOUNDNESS.