diff options
Diffstat (limited to 'cfrontend/Ctyping.v')
| -rw-r--r-- | cfrontend/Ctyping.v | 158 |
1 files changed, 113 insertions, 45 deletions
diff --git a/cfrontend/Ctyping.v b/cfrontend/Ctyping.v index ba1d34fb..00fcf8ab 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) = AST.Tvoid) + \/ (tyargs = Tcons type_bool (Tcons ty (Tcons ty Tnil)) + /\ let t := typ_of_type ty in + let sg := mksignature (AST.Tint :: t :: t :: nil) 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 -> @@ -517,11 +521,20 @@ Fixpoint bind_globdef (e: typenv) (l: list (ident * globdef fundef type)) : type | (id, Gvar v) :: l => bind_globdef (PTree.set id v.(gvar_info) e) l end. +Inductive wt_fundef (ce: composite_env) (e: typenv) : fundef -> Prop := + | wt_fundef_internal: forall f, + wt_function ce e f -> + wt_fundef ce e (Internal f) + | wt_fundef_external: forall ef targs tres cc, + (ef_sig ef).(sig_res) = rettype_of_type tres -> + wt_fundef ce e (External ef targs tres cc). + Inductive wt_program : program -> Prop := | wt_program_intro: forall p, let e := bind_globdef (PTree.empty _) p.(prog_defs) in - (forall id f, In (id, Gfun (Internal f)) p.(prog_defs) -> - wt_function p.(prog_comp_env) e f) -> + (forall id fd, + In (id, Gfun fd) p.(prog_defs) -> + wt_fundef p.(prog_comp_env) e fd) -> wt_program p. Hint Constructors wt_val wt_rvalue wt_lvalue wt_stmt wt_lblstmts: ty. @@ -741,10 +754,16 @@ Definition ebuiltin (ef: external_function) (tyargs: typelist) (args: exprlist) do x1 <- check_rvals args; do x2 <- check_arguments args tyargs; if type_eq tyres Tvoid - && opt_typ_eq (sig_res (ef_sig ef)) None + && AST.rettype_eq (sig_res (ef_sig ef)) AST.Tvoid 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). @@ -905,7 +924,8 @@ Definition retype_function (ce: composite_env) (e: typenv) (f: function) : res f Definition retype_fundef (ce: composite_env) (e: typenv) (fd: fundef) : res fundef := match fd with | Internal f => do f' <- retype_function ce e f; OK (Internal f') - | External id args res cc => OK fd + | External ef args res cc => + assertion (rettype_eq (ef_sig ef).(sig_res) (rettype_of_type res)); OK fd end. Definition typecheck_program (p: program) : res program := @@ -977,10 +997,20 @@ Proof. classify_cast (Tint i s a) t2 <> cast_case_default). { unfold classify_cast. destruct t2; try congruence. destruct f; congruence. + destruct Archi.ptr64; congruence. } 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. @@ -1221,10 +1251,21 @@ Lemma ebuiltin_sound: Proof. intros. monadInv H. destruct (type_eq tyres Tvoid); simpl in EQ2; try discriminate. - destruct (opt_typ_eq (sig_res (ef_sig ef)) None); inv EQ2. + destruct (rettype_eq (sig_res (ef_sig ef)) AST.Tvoid); inv EQ2. 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. @@ -1342,6 +1383,14 @@ Proof. intros. monadInv H. constructor; simpl. eapply retype_stmt_sound; eauto. Qed. +Lemma retype_fundef_sound: + forall ce e fd fd', retype_fundef ce e fd = OK fd' -> wt_fundef ce e fd'. +Proof. + intros. destruct fd; monadInv H. +- constructor; eapply retype_function_sound; eauto. +- constructor; auto. +Qed. + Theorem typecheck_program_sound: forall p p', typecheck_program p = OK p' -> wt_program p'. Proof. @@ -1364,11 +1413,11 @@ Proof. inv H1. simpl. auto. } rewrite ENVS. - intros id f. revert MATCH; generalize (prog_defs p) (AST.prog_defs tp). + intros id fd. revert MATCH; generalize (prog_defs p) (AST.prog_defs tp). induction 1; simpl; intros. contradiction. destruct H0; auto. subst b1; inv H. simpl in H1. inv H1. - destruct f1; monadInv H4. eapply retype_function_sound; eauto. + eapply retype_fundef_sound; eauto. Qed. (** * Subject reduction *) @@ -1632,15 +1681,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. @@ -1689,6 +1729,26 @@ Proof. inv H; auto. Qed. +Lemma has_rettype_wt_val: + forall v ty, + Val.has_rettype v (rettype_of_type ty) -> wt_val v ty. +Proof. + unfold rettype_of_type, Val.has_rettype, Val.has_type; destruct ty; intros. +- destruct v; contradiction || constructor. +- destruct i. + + destruct s; destruct v; try contradiction; constructor; red; auto. + + destruct s; destruct v; try contradiction; constructor; red; auto. + + destruct v; try contradiction; constructor; auto. + + destruct v; try contradiction; constructor; red; auto. +- destruct v; try contradiction; constructor; auto. +- destruct f; destruct v; try contradiction; constructor. +- unfold Tptr in *; destruct v; destruct Archi.ptr64 eqn:P64; try contradiction; constructor; auto. +- destruct v; contradiction || constructor. +- destruct v; contradiction || constructor. +- destruct v; contradiction || constructor. +- destruct v; contradiction || constructor. +Qed. + Lemma wt_rred: forall ge tenv a m t a' m', rred ge a m t a' m' -> wt_rvalue ge tenv a -> wt_rvalue ge tenv a'. @@ -1725,7 +1785,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) 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 +1847,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: @@ -1854,12 +1934,6 @@ Hypothesis WTPROG: wt_program prog. Let ge := globalenv prog. Let gtenv := bind_globdef (PTree.empty _) prog.(prog_defs). -Hypothesis WT_EXTERNAL: - forall id ef args res cc vargs m t vres m', - In (id, Gfun (External ef args res cc)) prog.(prog_defs) -> - external_call ef ge vargs m t vres m' -> - wt_val vres res. - Inductive wt_expr_cont: typenv -> function -> cont -> Prop := | wt_Kdo: forall te f k, wt_stmt_cont te f k -> @@ -1958,12 +2032,6 @@ Proof. induction 1; simpl; auto; econstructor; eauto. Qed. -Definition wt_fundef (fd: fundef) := - match fd with - | Internal f => wt_function ge gtenv f - | External ef targs tres cc => True - end. - Definition fundef_return (fd: fundef) : type := match fd with | Internal f => f.(fn_return) @@ -1971,10 +2039,10 @@ Definition fundef_return (fd: fundef) : type := end. Lemma wt_find_funct: - forall v fd, Genv.find_funct ge v = Some fd -> wt_fundef fd. + forall v fd, Genv.find_funct ge v = Some fd -> wt_fundef ge gtenv fd. Proof. intros. apply Genv.find_funct_prop with (p := prog) (v := v); auto. - intros. inv WTPROG. destruct f; simpl; auto. apply H1 with id; auto. + intros. inv WTPROG. apply H1 with id; auto. Qed. Inductive wt_state: state -> Prop := @@ -1990,7 +2058,7 @@ Inductive wt_state: state -> Prop := wt_state (ExprState f r k e m) | wt_call_state: forall b fd vargs k m (WTK: wt_call_cont k (fundef_return fd)) - (WTFD: wt_fundef fd) + (WTFD: wt_fundef ge gtenv fd) (FIND: Genv.find_funct ge b = Some fd), wt_state (Callstate fd vargs k m) | wt_return_state: forall v k m ty @@ -2047,7 +2115,6 @@ Qed. End WT_FIND_LABEL. - Lemma preservation_estep: forall S t S', estep ge S t S' -> wt_state S -> wt_state S'. Proof. @@ -2122,9 +2189,10 @@ Proof. - inv WTS; eauto with ty. - exploit wt_find_label. eexact WTB. eauto. eapply call_cont_wt'; eauto. intros [A B]. eauto with ty. -- simpl in WTFD; inv WTFD. econstructor; eauto. apply wt_call_cont_stmt_cont; auto. -- exploit (Genv.find_funct_inversion prog); eauto. intros (id & A). - econstructor; eauto. +- inv WTFD. inv H3. econstructor; eauto. apply wt_call_cont_stmt_cont; auto. +- inv WTFD. econstructor; eauto. + apply has_rettype_wt_val. simpl; rewrite <- H1. + eapply external_call_well_typed_gen; eauto. - inv WTK. eauto with ty. Qed. @@ -2139,7 +2207,7 @@ Theorem wt_initial_state: Proof. intros. inv H. econstructor. constructor. apply Genv.find_funct_ptr_prop with (p := prog) (b := b); auto. - intros. inv WTPROG. destruct f0; simpl; auto. apply H4 with id; auto. + intros. inv WTPROG. apply H4 with id; auto. instantiate (1 := (Vptr b Ptrofs.zero)). rewrite Genv.find_funct_find_funct_ptr. auto. Qed. |