Implement a `Osel` operation for ARM

The operation comples down to conditional moves.
Both integer and floating-point conditional moves are supported.

12 files changed, 115 insertions, 7 deletions

diff --git a/arm/Asm.v b/arm/Asm.v
index e6d1b4fc..194074ac 100644
--- a/arm/Asm.v
+++ b/arm/Asm.v
@@ -220,6 +220,7 @@ Inductive instruction : Type :=
   | Plabel: label -> instruction                    (**r define a code label *)
   | Ploadsymbol: ireg -> ident -> ptrofs -> instruction (**r load the address of a symbol *)
   | Pmovite: testcond -> ireg -> shift_op -> shift_op -> instruction (**r integer conditional move *)
+  | Pfmovite: testcond -> freg -> freg -> freg -> instruction (**r FP conditional move *)
   | Pbtbl: ireg -> list label -> instruction       (**r N-way branch through a jump table *)
   | Pbuiltin: external_function -> list (builtin_arg preg) -> builtin_res preg -> instruction (**r built-in function (pseudo) *)
   | Padc: ireg -> ireg -> shift_op -> instruction     (**r add with carry *)
@@ -783,6 +784,14 @@ Definition exec_instr (f: function) (i: instruction) (rs: regset) (m: mem) : out
         | None => Vundef
         end in
       Next (nextinstr (rs#r1 <- v)) m
+  | Pfmovite cond r1 ifso ifnot =>
+      let v :=
+        match eval_testcond cond rs with
+        | Some true => rs#ifso
+        | Some false => rs#ifnot
+        | None => Vundef
+        end in
+      Next (nextinstr (rs#r1 <- v)) m
   | Pbtbl r tbl =>
       match rs#r with
       | Vint n =>
diff --git a/arm/AsmToJSON.ml b/arm/AsmToJSON.ml
index 3874e141..dfad6972 100644
--- a/arm/AsmToJSON.ml
+++ b/arm/AsmToJSON.ml
@@ -259,7 +259,8 @@ let pp_instructions pp ic =
     | Pmla(r1, r2, r3, r4) -> instruction pp "Pmla" [Ireg r1; Ireg r2; Ireg r3; Ireg r4]
     | Pmov(r1, so) -> instruction pp "Pmov" [Ireg r1; Shift so]
     | Pmovite(cond, r1, so1, so2) -> instruction pp "Pmovite" [Ireg r1; Condition (TargetPrinter.condition_name cond); Shift so1; Condition (TargetPrinter.neg_condition_name cond); Shift so2]
-    | Pmovt(r1, n) -> instruction pp "Pmovt" [Ireg r1; Long n]
+    | Pfmovite(cond, r1, r2, r3) -> instruction pp "Pfmovite" [DFreg r1; Condition (TargetPrinter.condition_name cond); DFreg r2; Condition (TargetPrinter.neg_condition_name cond); DFreg r3] 
+   | Pmovt(r1, n) -> instruction pp "Pmovt" [Ireg r1; Long n]
     | Pmovw(r1, n) -> instruction pp "Pmovw" [Ireg r1; Long n]
     | Pmul(r1, r2, r3) -> instruction pp "Pmul" [Ireg r1; Ireg r2; Ireg r3]
     | Pmvn(r1, so) -> instruction pp "Pmvn" [Ireg r1; Shift so]
diff --git a/arm/Asmgen.v b/arm/Asmgen.v
index f12ea870..1a1e7f2f 100644
--- a/arm/Asmgen.v
+++ b/arm/Asmgen.v
@@ -555,6 +555,19 @@ Definition transl_op
       do r <- ireg_of res;
       transl_cond cmp args
         (Pmovite (cond_for_cond cmp) r (SOimm Int.one) (SOimm Int.zero) :: k)
+  | Osel cmp ty, a1 :: a2 :: args =>
+      match preg_of res with
+      | IR r => 
+          do r1 <- ireg_of a1; do r2 <- ireg_of a2;
+          transl_cond cmp args
+            (Pmovite (cond_for_cond cmp) r (SOreg r1) (SOreg r2) :: k)
+      | FR r =>
+          do r1 <- freg_of a1; do r2 <- freg_of a2;
+          transl_cond cmp args
+            (Pfmovite (cond_for_cond cmp) r r1 r2 :: k)
+      | _ =>
+          Error(msg "Asmgen.Osel")
+      end
   | _, _ =>
       Error(msg "Asmgen.transl_op")
   end.
diff --git a/arm/Asmgenproof.v b/arm/Asmgenproof.v
index 2c001f45..25f91d23 100644
--- a/arm/Asmgenproof.v
+++ b/arm/Asmgenproof.v
@@ -270,6 +270,7 @@ Opaque Int.eq.
   destruct Archi.thumb2_support; TailNoLabel.
   eapply tail_nolabel_trans; TailNoLabel.
   eapply tail_nolabel_trans. eapply transl_cond_label; eauto. TailNoLabel.
+  destruct (preg_of r); monadInv H; (eapply tail_nolabel_trans; [eapply transl_cond_label; eauto|TailNoLabel]).
 Qed.
 
 Remark transl_memory_access_label:
diff --git a/arm/Asmgenproof1.v b/arm/Asmgenproof1.v
index edf35bb8..807e069d 100644
--- a/arm/Asmgenproof1.v
+++ b/arm/Asmgenproof1.v
@@ -1189,7 +1189,7 @@ Lemma transl_op_correct_same:
   forall op args res k c (rs: regset) m v,
   transl_op op args res k = OK c ->
   eval_operation ge rs#IR13 op (map rs (map preg_of args)) m = Some v ->
-  match op with Ocmp _ => False | Oaddrstack _ => False | _ => True end ->
+  match op with Ocmp _ => False | Osel _ _ => False | Oaddrstack _ => False | _ => True end ->
   exists rs',
      exec_straight ge fn c rs m k rs' m
   /\ rs'#(preg_of res) = v
@@ -1333,6 +1333,8 @@ Transparent destroyed_by_op.
   intuition Simpl.
   (* Ocmp *)
   contradiction.
+  (* Osel *)
+  contradiction.
 Qed.
 
 Lemma transl_op_correct:
@@ -1369,6 +1371,27 @@ Proof.
   split; intros; Simpl.
   destruct (eval_condition c0 rs ## (preg_of ## args) m) as [b|]; simpl; auto.
   destruct B as [B1 B2]; rewrite B1. destruct b; auto.
+- (* Osel *)
+  clear SAME. simpl in H.  ArgsInv. simpl in H0; inv H0.
+  assert (D1: data_preg (preg_of m0) = true) by auto with asmgen.
+  assert (D2: data_preg (preg_of m1) = true) by auto with asmgen.
+  destruct (preg_of res) eqn:RES; monadInv H.
++ inv EQ2. rewrite (ireg_of_eq _ _ EQ), (ireg_of_eq _ _ EQ1) in *.
+  exploit transl_cond_correct; eauto. instantiate (1 := rs). instantiate (1 := m). intros [rs1 [A [B C]]].
+  econstructor; split.
+  eapply exec_straight_trans. eexact A. apply exec_straight_one. simpl; eauto. auto.
+  split; intros; Simpl.
+  rewrite ! C by auto.
+  destruct (eval_condition c0 rs ## (preg_of ## args) m) as [b|]; simpl; auto.
+  destruct B as [B1 B2]; rewrite B1. destruct b; apply Val.lessdef_normalize.
++ inv EQ2. rewrite (freg_of_eq _ _ EQ), (freg_of_eq _ _ EQ1) in *.
+  exploit transl_cond_correct; eauto. instantiate (1 := rs). instantiate (1 := m). intros [rs1 [A [B C]]].
+  econstructor; split.
+  eapply exec_straight_trans. eexact A. apply exec_straight_one. simpl; eauto. auto.
+  split; intros; Simpl.
+  rewrite ! C by auto.
+  destruct (eval_condition c0 rs ## (preg_of ## args) m) as [b|]; simpl; auto.
+  destruct B as [B1 B2]; rewrite B1. destruct b; apply Val.lessdef_normalize.
 Qed.
 
 (** Translation of loads and stores. *)
diff --git a/arm/NeedOp.v b/arm/NeedOp.v
index dee7cae1..c70c7e40 100644
--- a/arm/NeedOp.v
+++ b/arm/NeedOp.v
@@ -83,6 +83,7 @@ Definition needs_of_operation (op: operation) (nv: nval): list nval :=
   | 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 :=
@@ -183,6 +184,10 @@ Proof.
 - apply notint_sound; auto.
 - apply notint_sound. apply needs_of_shift_sound; auto.
 - apply needs_of_shift_sound; auto.
+- 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/arm/Op.v b/arm/Op.v
index 8e1cd367..cc90e043 100644
--- a/arm/Op.v
+++ b/arm/Op.v
@@ -140,7 +140,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. *)
@@ -174,7 +176,7 @@ Defined.
 
 Definition eq_operation (x y: operation): {x=y} + {x<>y}.
 Proof.
-  generalize Int.eq_dec Ptrofs.eq_dec ident_eq; intros.
+  generalize Int.eq_dec Ptrofs.eq_dec ident_eq typ_eq; intros.
   generalize Float.eq_dec Float32.eq_dec; intros.
   generalize eq_shift; intro.
   generalize eq_condition; intro.
@@ -294,6 +296,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.
 
@@ -419,6 +422,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 :=
@@ -511,6 +515,7 @@ Proof with (try exact I; try reflexivity).
   destruct v0...
   destruct v0...
   destruct (eval_condition c vl m)... destruct b...
+  unfold Val.select. destruct (eval_condition c vl m). apply Val.normalize_type. exact I.
 Qed.
 
 End SOUNDNESS.
@@ -682,19 +687,37 @@ 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 _ | Ccompushift _ _| Ccompuimm _ _ => true
+  | _ => false
+  end.
+
 Definition op_depends_on_memory (op: operation) : bool :=
   match op with
-  | Ocmp (Ccompu _ | Ccompushift _ _| Ccompuimm _ _) => true
+  | 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.
-  intros. destruct c; simpl; auto; congruence.
+  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 *)
@@ -929,6 +952,10 @@ 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/arm/PrintOp.ml b/arm/PrintOp.ml
index 642fff80..d74acf3f 100644
--- a/arm/PrintOp.ml
+++ b/arm/PrintOp.ml
@@ -129,6 +129,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
   | _ -> fprintf pp "<bad operator>"
 
 let print_addressing reg pp = function
diff --git a/arm/SelectOp.vp b/arm/SelectOp.vp
index c361df65..61ea6283 100644
--- a/arm/SelectOp.vp
+++ b/arm/SelectOp.vp
@@ -382,6 +382,9 @@ Definition compf (c: comparison) (e1: expr) (e2: expr) :=
 Definition compfs (c: comparison) (e1: expr) (e2: expr) :=
   Eop (Ocmp (Ccompfs c)) (e1 ::: e2 ::: Enil).
 
+Definition select (ty: typ) (cond: condition) (args: exprlist) (e1 e2: expr) :=
+  Some (Eop (Osel cond ty) (e1 ::: e2 ::: args)).
+
 (** ** Integer conversions *)
 
 Definition cast8unsigned (e: expr) := andimm (Int.repr 255) e.
diff --git a/arm/SelectOpproof.v b/arm/SelectOpproof.v
index d4aac9b6..f281f7ce 100644
--- a/arm/SelectOpproof.v
+++ b/arm/SelectOpproof.v
@@ -735,6 +735,20 @@ Proof.
   intros; red; intros. unfold compfs. TrivialExists.
 Qed.
 
+Theorem eval_select:
+  forall le ty cond al vl a1 v1 a2 v2 a b,
+  select ty cond al a1 a2 = Some a ->
+  eval_exprlist ge sp e m le al vl ->
+  eval_expr ge sp e m le a1 v1 ->
+  eval_expr ge sp e m le a2 v2 ->
+  eval_condition cond vl m = Some b ->
+  exists v, 
+     eval_expr ge sp e m le a v
+  /\ Val.lessdef (Val.select (Some b) v1 v2 ty) v.
+Proof.
+  unfold select; intros; inv H. rewrite <- H3; TrivialExists. 
+Qed.
+
 Theorem eval_cast8signed: unary_constructor_sound cast8signed (Val.sign_ext 8).
 Proof.
   red; intros until x. unfold cast8signed; case (cast8signed_match a); intros.
diff --git a/arm/TargetPrinter.ml b/arm/TargetPrinter.ml
index 20989615..64448648 100644
--- a/arm/TargetPrinter.ml
+++ b/arm/TargetPrinter.ml
@@ -443,6 +443,12 @@ struct
         (condition_name cond) ireg r1 shift_op ifso;
       fprintf oc "	mov%s	%a, %a\n"
         (neg_condition_name cond) ireg r1 shift_op ifnot
+    | Pfmovite(cond, r1, ifso, ifnot) ->
+      fprintf oc "	ite	%s\n" (condition_name cond);
+      fprintf oc "	vmov%s	%a, %a\n"
+        (condition_name cond) freg r1 freg ifso;
+      fprintf oc "	vmov%s	%a, %a\n"
+        (neg_condition_name cond) freg r1 freg ifnot
     | Pbtbl(r, tbl) ->
       if !Clflags.option_mthumb then begin
         fprintf oc "	lsl	r14, %a, #2\n" ireg r;
diff --git a/arm/ValueAOp.v b/arm/ValueAOp.v
index e19ddd6d..a3fd9d7d 100644
--- a/arm/ValueAOp.v
+++ b/arm/ValueAOp.v
@@ -127,6 +127,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.
 
@@ -205,6 +206,7 @@ Proof.
   rewrite Ptrofs.add_zero_l; eauto with va.
   fold (Val.sub (Vint i) a1). auto with va.
   apply of_optbool_sound. eapply eval_static_condition_sound; eauto.
+  apply select_sound; auto. eapply eval_static_condition_sound; eauto.
 Qed.
 
 End SOUNDNESS.