Add selection to CompCert C as a derived form

`Eselection r1 r2 r3 ty` is like `Econdition r1 r2 r3 ty`, except
that both `r2` and `r3` are always evaluated, thus the expression
can be compiled down to a conditional move.

Internally, `Eselection` is expressed as a call to the built-in
`EF_select`.  We prove admissible evaluation rules, showing that
the encoding gives the expected semantics.

3 files changed, 81 insertions, 0 deletions

diff --git a/cfrontend/Cop.v b/cfrontend/Cop.v
index c395a2cb..782fb32a 100644
--- a/cfrontend/Cop.v
+++ b/cfrontend/Cop.v
@@ -1580,6 +1580,27 @@ Proof.
   intros. apply cast_val_casted. eapply cast_val_is_casted; eauto.
 Qed.
 
+(** Moreover, casted values belong to the machine type corresponding to the
+    C type. *)
+
+Lemma val_casted_has_type:
+  forall v ty, val_casted v ty -> ty <> Tvoid -> Val.has_type v (typ_of_type ty).
+Proof.
+  intros. inv H; simpl typ_of_type.
+- exact I.
+- exact I.
+- exact I.
+- exact I.
+- apply Val.Vptr_has_type.
+- red; unfold Tptr; rewrite H1; auto.
+- red; unfold Tptr; rewrite H1; auto.
+- red; unfold Tptr; rewrite H1; auto.
+- red; unfold Tptr; rewrite H1; auto.
+- apply Val.Vptr_has_type.
+- apply Val.Vptr_has_type.
+- congruence.
+Qed.
+
 (** Relation with the arithmetic conversions of ISO C99, section 6.3.1 *)
 
 Module ArithConv.
diff --git a/cfrontend/Csem.v b/cfrontend/Csem.v
index 0c3e00de..45ec6d41 100644
--- a/cfrontend/Csem.v
+++ b/cfrontend/Csem.v
@@ -437,6 +437,56 @@ Definition not_stuck (e: expr) (m: mem) : Prop :=
   forall k C e' ,
   context k RV C -> e = C e' -> imm_safe k e' m.
 
+(** ** Derived forms. *)
+
+(** The following are admissible reduction rules for some derived forms
+  of the CompCert C language.  They help showing that the derived forms
+  make sense. *)
+
+Lemma red_selection:
+  forall v1 ty1 v2 ty2 v3 ty3 ty m b v2' v3',
+  ty <> Tvoid ->
+  bool_val v1 ty1 m = Some b ->
+  sem_cast v2 ty2 ty m = Some v2' ->
+  sem_cast v3 ty3 ty m = Some v3' ->
+  rred (Eselection (Eval v1 ty1) (Eval v2 ty2) (Eval v3 ty3) ty) m
+    E0 (Eval (if b then v2' else v3') ty) m.
+Proof.
+  intros. unfold Eselection.
+  set (v' := if b then v2' else v3').
+  assert (C: val_casted v' ty).
+  { unfold v'; destruct b; eapply cast_val_is_casted; eauto. }
+  assert (EQ: Val.normalize v' (typ_of_type ty) = v').
+  { apply Val.normalize_idem. apply val_casted_has_type; auto. }
+  econstructor.
+- constructor. rewrite cast_bool_bool_val, H0. eauto.
+  constructor. eauto.
+  constructor. eauto.
+  constructor.
+- rewrite <- EQ. constructor.
+  destruct b; simpl.
+  apply (Val.bool_of_val_int Int.one).
+  apply (Val.bool_of_val_int Int.zero).
+Qed.
+
+Lemma ctx_selection_1:
+  forall k C r2 r3 ty, context k RV C -> context k RV (fun x => Eselection (C x) r2 r3 ty).
+Proof.
+  intros. apply ctx_builtin. constructor; auto.
+Qed.
+
+Lemma ctx_selection_2:
+  forall k r1 C r3 ty, context k RV C -> context k RV (fun x => Eselection r1 (C x) r3 ty).
+Proof.
+  intros. apply ctx_builtin. constructor; constructor; auto.
+Qed.
+
+Lemma ctx_selection_3:
+  forall k r1 r2 C ty, context k RV C -> context k RV (fun x => Eselection r1 r2 (C x) ty).
+Proof.
+  intros. apply ctx_builtin. constructor; constructor; constructor; auto.
+Qed.
+
 End EXPR.
 
 (** ** Transition semantics. *)
diff --git a/cfrontend/Csyntax.v b/cfrontend/Csyntax.v
index 00565309..42f3451c 100644
--- a/cfrontend/Csyntax.v
+++ b/cfrontend/Csyntax.v
@@ -100,6 +100,16 @@ Definition Epreincr (id: incr_or_decr) (l: expr) (ty: type) :=
   Eassignop (match id with Incr => Oadd | Decr => Osub end)
             l (Eval (Vint Int.one) type_int32s) (typeconv ty) ty.
 
+(** Selection is a conditional expression that always evaluates both arms
+  and can be implemented by "conditional move" instructions.
+  It is expressed as an invocation of a builtin function. *)
+
+Definition Eselection (r1 r2 r3: expr) (ty: type) :=
+  Ebuiltin (EF_select (typ_of_type ty))
+           (Tcons type_bool (Tcons ty (Tcons ty Tnil)))
+           (Econs r1 (Econs r2 (Econs r3 Enil)))
+           ty.
+
 (** Extract the type part of a type-annotated expression. *)
 
 Definition typeof (a: expr) : type :=