From 633e60ed36c07c4b6cb4b1dc93b9eea312882ceb Mon Sep 17 00:00:00 2001 From: Xavier Leroy Date: Thu, 4 Jul 2019 17:49:11 +0200 Subject: 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. --- cfrontend/Ctyping.v | 77 ++++++++++++++++++++++++++++++++++++++++------------- 1 file changed, 59 insertions(+), 18 deletions(-) (limited to 'cfrontend/Ctyping.v') 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: -- cgit