Make __builtin_sel available from C source code

It is type-checked like a conditional expression then translated to
a call to the known builtin function.

1 files changed, 59 insertions, 18 deletions

diff --git a/cfrontend/Ctyping.v b/cfrontend/Ctyping.v
index ba1d34fb..b92a9bac 100644
--- a/cfrontend/Ctyping.v
+++ b/cfrontend/Ctyping.v
@@ -18,7 +18,7 @@
 Require Import String.
 Require Import Coqlib Maps Integers Floats Errors.
 Require Import AST Linking.
-Require Import Values Memory Globalenvs Events.
+Require Import Values Memory Globalenvs Builtins Events.
 Require Import Ctypes Cop Csyntax Csem.
 
 Local Open Scope error_monad_scope.
@@ -392,13 +392,17 @@ Inductive wt_rvalue : expr -> Prop :=
       classify_fun (typeof r1) = fun_case_f tyargs tyres cconv ->
       wt_arguments rargs tyargs ->
       wt_rvalue (Ecall r1 rargs tyres)
-  | wt_Ebuiltin: forall ef tyargs rargs,
+  | wt_Ebuiltin: forall ef tyargs rargs ty,
       wt_exprlist rargs ->
       wt_arguments rargs tyargs ->
-      (* This is specialized to builtins returning void, the only
-         case generated by C2C. *)
-      sig_res (ef_sig ef) = None ->
-      wt_rvalue (Ebuiltin ef tyargs rargs Tvoid)
+      (* This typing rule is specialized to the builtin invocations generated
+         by C2C, which are either __builtin_sel or builtins returning void. *)
+         (ty = Tvoid /\ sig_res (ef_sig ef) = None)
+      \/ (tyargs = Tcons type_bool (Tcons ty (Tcons ty Tnil))
+          /\ let t := typ_of_type ty in
+             let sg := mksignature (AST.Tint :: t :: t :: nil) (Some t) cc_default in
+             ef = EF_builtin "__builtin_sel"%string sg) ->
+      wt_rvalue (Ebuiltin ef tyargs rargs ty)
   | wt_Eparen: forall r tycast ty,
       wt_rvalue r ->
       wt_cast (typeof r) tycast -> subtype tycast ty ->
@@ -745,6 +749,12 @@ Definition ebuiltin (ef: external_function) (tyargs: typelist) (args: exprlist)
   then OK (Ebuiltin ef tyargs args tyres)
   else Error (msg "builtin: wrong type decoration").
 
+Definition eselection (r1 r2 r3: expr) : res expr :=
+  do x1 <- check_rval r1; do x2 <- check_rval r2; do x3 <- check_rval r3;
+  do y1 <- check_bool (typeof r1);
+  do ty <- type_conditional (typeof r2) (typeof r3);
+  OK (Eselection r1 r2 r3 ty).
+
 Definition sdo (a: expr) : res statement :=
   do x <- check_rval a; OK (Sdo a).
 
@@ -981,6 +991,15 @@ Proof.
   destruct i; auto.
 Qed.
 
+Lemma wt_bool_cast:
+  forall ty, wt_bool ty -> wt_cast ty type_bool.
+Proof.
+  unfold wt_bool, wt_cast; unfold classify_bool; intros.
+  destruct ty; simpl in *; try congruence;
+  try (destruct Archi.ptr64; congruence).
+  destruct f; congruence.
+Qed.
+
 Lemma wt_cast_int:
   forall i1 s1 a1 i2 s2 a2, wt_cast (Tint i1 s1 a1) (Tint i2 s2 a2).
 Proof.
@@ -1225,6 +1244,17 @@ Proof.
   econstructor; eauto. eapply check_arguments_sound; eauto.
 Qed.
 
+Lemma eselection_sound:
+  forall r1 r2 r3 a, eselection r1 r2 r3 = OK a ->
+  wt_expr ce e r1 -> wt_expr ce e r2 -> wt_expr ce e r3 -> wt_expr ce e a.
+Proof.
+  intros. monadInv H. apply type_conditional_cast in EQ3. destruct EQ3.
+  eapply wt_Ebuiltin.
+  repeat (constructor; eauto with ty).
+  repeat (constructor; eauto with ty). apply wt_bool_cast; eauto with ty.
+  right; auto.
+Qed.
+
 Lemma sdo_sound:
   forall a s, sdo a = OK s -> wt_expr ce e a -> wt_stmt ce e rt s.
 Proof.
@@ -1632,15 +1662,6 @@ Proof.
   destruct f; discriminate.
 Qed.
 
-Lemma wt_bool_cast:
-  forall ty, wt_bool ty -> wt_cast ty type_bool.
-Proof.
-  unfold wt_bool, wt_cast; unfold classify_bool; intros.
-  destruct ty; simpl in *; try congruence;
-  try (destruct Archi.ptr64; congruence).
-  destruct f; congruence.
-Qed.
-
 Lemma wt_cast_self:
   forall t1 t2, wt_cast t1 t2 -> wt_cast t2 t2.
 Proof.
@@ -1725,7 +1746,27 @@ Proof.
   constructor; auto.
 - (* comma *) auto.
 - (* paren *) inv H3. constructor. apply H5. eapply pres_sem_cast; eauto.
-- (* builtin *) subst. auto with ty.
+- (* builtin *) subst. destruct H7 as [(A & B) | (A & B)].
++ subst ty. auto with ty.
++ simpl in B. set (T := typ_of_type ty) in *. 
+  set (sg := mksignature (AST.Tint :: T :: T :: nil) (Some T) cc_default) in *.
+  assert (LK: lookup_builtin_function "__builtin_sel"%string sg = Some (BI_standard (BI_select T))).
+  { unfold sg, T; destruct ty as   [ | ? ? ? | ? | [] ? | ? ? | ? ? ? | ? ? ? | ? ? | ? ? ];
+    simpl; unfold Tptr; destruct Archi.ptr64; reflexivity. }
+  subst ef. red in H0. red in H0. rewrite LK in H0. inv H0. 
+  inv H. inv H8. inv H9. inv H10. simpl in H1.
+  assert (A: val_casted v1 type_bool) by (eapply cast_val_is_casted; eauto).
+  inv A. 
+  set (v' := if Int.eq n Int.zero then v4 else v2) in *.
+  constructor.
+  destruct (type_eq ty Tvoid).
+  subst. constructor.
+  inv H1.
+  assert (C: val_casted v' ty).
+  { unfold v'; destruct (Int.eq n Int.zero); eapply cast_val_is_casted; eauto. }
+  assert (EQ: Val.normalize v' T = v').
+  { apply Val.normalize_idem. apply val_casted_has_type; auto. }
+  rewrite EQ. apply wt_val_casted; auto.
 Qed.
 
 Lemma wt_lred:
@@ -1767,8 +1808,8 @@ with wt_subexprlist:
   wt_exprlist cenv tenv (C a) ->
   wt_expr_kind cenv tenv from a.
 Proof.
-  destruct 1; intros WT; auto; inv WT; eauto.
-  destruct 1; intros WT; inv WT; eauto.
+- destruct 1; intros WT; auto; inv WT; eauto.
+- destruct 1; intros WT; inv WT; eauto.
 Qed.
 
 Lemma typeof_context: