diff options
Diffstat (limited to 'cfrontend')
-rw-r--r-- | cfrontend/C2C.ml | 18 | ||||
-rw-r--r-- | cfrontend/Cop.v | 4 | ||||
-rw-r--r-- | cfrontend/Csem.v | 2 | ||||
-rw-r--r-- | cfrontend/Cshmgen.v | 39 | ||||
-rw-r--r-- | cfrontend/Cshmgenproof.v | 133 | ||||
-rw-r--r-- | cfrontend/Csyntax.v | 2 | ||||
-rw-r--r-- | cfrontend/Ctypes.v | 19 | ||||
-rw-r--r-- | cfrontend/Ctyping.v | 87 | ||||
-rw-r--r-- | cfrontend/PrintCsyntax.ml | 4 |
9 files changed, 232 insertions, 76 deletions
diff --git a/cfrontend/C2C.ml b/cfrontend/C2C.ml index 24e3cacf..ec5fb4dc 100644 --- a/cfrontend/C2C.ml +++ b/cfrontend/C2C.ml @@ -33,6 +33,7 @@ type inline_status = type atom_info = { a_storage: C.storage; (* storage class *) + a_size: int64 option; (* size in bytes *) a_alignment: int option; (* alignment *) a_sections: Sections.section_name list; (* in which section to put it *) (* 1 section for data, 3 sections (code/lit/jumptbl) for functions *) @@ -72,9 +73,14 @@ let atom_sections a = with Not_found -> [] -let atom_is_small_data a ofs = +let atom_is_small_data a ofs = try - (Hashtbl.find decl_atom a).a_access = Sections.Access_near + let info = Hashtbl.find decl_atom a in + info.a_access = Sections.Access_near + && (match info.a_size with + | None -> false + | Some sz -> + let ofs = camlint64_of_ptrofs ofs in 0L <= ofs && ofs < sz) with Not_found -> false @@ -376,6 +382,7 @@ let name_for_string_literal s = Hashtbl.add decl_atom id { a_storage = C.Storage_static; a_alignment = Some 1; + a_size = Some (Int64.of_int (String.length s + 1)); a_sections = [Sections.for_stringlit()]; a_access = Sections.Access_default; a_inline = No_specifier; @@ -403,9 +410,12 @@ let name_for_wide_string_literal s = incr stringNum; let name = Printf.sprintf "__stringlit_%d" !stringNum in let id = intern_string name in + let wchar_size = Machine.((!config).sizeof_wchar) in Hashtbl.add decl_atom id { a_storage = C.Storage_static; - a_alignment = Some Machine.((!config).sizeof_wchar); + a_alignment = Some wchar_size; + a_size = Some (Int64.(mul (of_int (List.length s + 1)) + (of_int wchar_size))); a_sections = [Sections.for_stringlit()]; a_access = Sections.Access_default; a_inline = No_specifier; @@ -1247,6 +1257,7 @@ let convertFundef loc env fd = Hashtbl.add decl_atom id' { a_storage = fd.fd_storage; a_alignment = None; + a_size = None; a_sections = Sections.for_function env id' fd.fd_attrib; a_access = Sections.Access_default; a_inline = inline; @@ -1341,6 +1352,7 @@ let convertGlobvar loc env (sto, id, ty, optinit) = Hashtbl.add decl_atom id' { a_storage = sto; a_alignment = Some (Z.to_int al); + a_size = Some (Z.to_int64 sz); a_sections = [section]; a_access = access; a_inline = No_specifier; diff --git a/cfrontend/Cop.v b/cfrontend/Cop.v index aa73abb0..143e87a3 100644 --- a/cfrontend/Cop.v +++ b/cfrontend/Cop.v @@ -140,8 +140,8 @@ Definition classify_cast (tfrom tto: type) : classify_cast_cases := | Tfloat F64 _, Tfloat F32 _ => cast_case_s2f | Tfloat F32 _, Tfloat F64 _ => cast_case_f2s (* To pointer types *) - | Tpointer _ _, Tint _ _ _ => - if Archi.ptr64 then cast_case_i2l Unsigned else cast_case_pointer + | Tpointer _ _, Tint _ si _ => + if Archi.ptr64 then cast_case_i2l si else cast_case_pointer | Tpointer _ _, Tlong _ _ => if Archi.ptr64 then cast_case_pointer else cast_case_l2i I32 Unsigned | Tpointer _ _, (Tpointer _ _ | Tarray _ _ _ | Tfunction _ _ _) => cast_case_pointer diff --git a/cfrontend/Csem.v b/cfrontend/Csem.v index a76a14ba..6d2b470f 100644 --- a/cfrontend/Csem.v +++ b/cfrontend/Csem.v @@ -444,7 +444,7 @@ Lemma red_selection: Proof. intros. unfold Eselection. set (t := typ_of_type ty). - set (sg := mksignature (AST.Tint :: t :: t :: nil) (Some t) cc_default). + set (sg := mksignature (AST.Tint :: t :: t :: nil) t cc_default). 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. } diff --git a/cfrontend/Cshmgen.v b/cfrontend/Cshmgen.v index 792a73f9..5bd12d00 100644 --- a/cfrontend/Cshmgen.v +++ b/cfrontend/Cshmgen.v @@ -23,6 +23,7 @@ Require Import Coqlib Maps Errors Integers Floats. Require Import AST Linking. Require Import Ctypes Cop Clight Cminor Csharpminor. +Require Import Conventions1. Local Open Scope string_scope. Local Open Scope error_monad_scope. @@ -558,6 +559,34 @@ Fixpoint typlist_of_arglist (al: list Clight.expr) (tyl: typelist) typ_of_type (default_argument_conversion (typeof a1)) :: typlist_of_arglist a2 Tnil end. +(** Translate a function call. + Depending on the ABI, it may be necessary to normalize the value + returned by casting it to the return type of the function. + For example, in the x86 ABI, a return value of type "char" is + returned in register AL, leaving the top 24 bits of EAX + unspecified. Hence, a cast to type "char" is needed to sign- or + zero-extend the returned integer before using it. *) + +Definition make_normalization (t: type) (a: expr) := + match t with + | Tint IBool _ _ => Eunop Ocast8unsigned a + | Tint I8 Signed _ => Eunop Ocast8signed a + | Tint I8 Unsigned _ => Eunop Ocast8unsigned a + | Tint I16 Signed _ => Eunop Ocast16signed a + | Tint I16 Unsigned _ => Eunop Ocast16unsigned a + | _ => a + end. + +Definition make_funcall (x: option ident) (tres: type) (sg: signature) + (fn: expr) (args: list expr): stmt := + match x, return_value_needs_normalization sg.(sig_res) with + | Some id, true => + Sseq (Scall x sg fn args) + (Sset id (make_normalization tres (Evar id))) + | _, _ => + Scall x sg fn args + end. + (** * Translation of statements *) (** [transl_statement nbrk ncnt s] returns a Csharpminor statement @@ -601,10 +630,10 @@ Fixpoint transl_statement (ce: composite_env) (tyret: type) (nbrk ncnt: nat) | fun_case_f args res cconv => do tb <- transl_expr ce b; do tcl <- transl_arglist ce cl args; - OK(Scall x {| sig_args := typlist_of_arglist cl args; - sig_res := opttyp_of_type res; - sig_cc := cconv |} - tb tcl) + let sg := {| sig_args := typlist_of_arglist cl args; + sig_res := rettype_of_type res; + sig_cc := cconv |} in + OK (make_funcall x res sg tb tcl) | _ => Error(msg "Cshmgen.transl_stmt(call)") end | Clight.Sbuiltin x ef tyargs bl => @@ -667,7 +696,7 @@ Definition transl_var (ce: composite_env) (v: ident * type) := Definition signature_of_function (f: Clight.function) := {| sig_args := map typ_of_type (map snd (Clight.fn_params f)); - sig_res := opttyp_of_type (Clight.fn_return f); + sig_res := rettype_of_type (Clight.fn_return f); sig_cc := Clight.fn_callconv f |}. Definition transl_function (ce: composite_env) (f: Clight.function) : res function := diff --git a/cfrontend/Cshmgenproof.v b/cfrontend/Cshmgenproof.v index 09e31cb2..1ceb8e4d 100644 --- a/cfrontend/Cshmgenproof.v +++ b/cfrontend/Cshmgenproof.v @@ -15,7 +15,7 @@ Require Import Coqlib Errors Maps Integers Floats. Require Import AST Linking. Require Import Values Events Memory Globalenvs Smallstep. -Require Import Ctypes Cop Clight Cminor Csharpminor. +Require Import Ctypes Ctyping Cop Clight Cminor Csharpminor. Require Import Cshmgen. (** * Relational specification of the transformation *) @@ -996,6 +996,26 @@ Proof. eapply make_memcpy_correct with (b := b) (v := Vptr b' ofs'); eauto. Qed. +Lemma make_normalization_correct: + forall e le m a v t, + eval_expr ge e le m a v -> + wt_val v t -> + eval_expr ge e le m (make_normalization t a) v. +Proof. + intros. destruct t; simpl; auto. inv H0. +- destruct i; simpl in H3. + + destruct s; econstructor; eauto; simpl; congruence. + + destruct s; econstructor; eauto; simpl; congruence. + + auto. + + econstructor; eauto; simpl; congruence. +- auto. +- destruct i. + + destruct s; econstructor; eauto. + + destruct s; econstructor; eauto. + + auto. + + econstructor; eauto. +Qed. + End CONSTRUCTORS. (** * Basic preservation invariants *) @@ -1360,7 +1380,16 @@ Inductive match_cont: composite_env -> type -> nat -> nat -> Clight.cont -> Csha match_cont cu.(prog_comp_env) (Clight.fn_return f) nbrk' ncnt' k tk -> match_cont ce tyret nbrk ncnt (Clight.Kcall id f e le k) - (Kcall id tf te le tk). + (Kcall id tf te le tk) + | match_Kcall_normalize: forall ce tyret nbrk ncnt nbrk' ncnt' f e k id a tf te le tk cu, + linkorder cu prog -> + transl_function cu.(prog_comp_env) f = OK tf -> + match_env e te -> + match_cont cu.(prog_comp_env) (Clight.fn_return f) nbrk' ncnt' k tk -> + (forall v e le m, wt_val v tyret -> le!id = Some v -> eval_expr tge e le m a v) -> + match_cont ce tyret nbrk ncnt + (Clight.Kcall (Some id) f e le k) + (Kcall (Some id) tf te le (Kseq (Sset id a) tk)). Inductive match_states: Clight.state -> Csharpminor.state -> Prop := | match_state: @@ -1377,14 +1406,15 @@ Inductive match_states: Clight.state -> Csharpminor.state -> Prop := forall fd args k m tfd tk targs tres cconv cu ce (LINK: linkorder cu prog) (TR: match_fundef cu fd tfd) - (MK: match_cont ce Tvoid 0%nat 0%nat k tk) + (MK: match_cont ce tres 0%nat 0%nat k tk) (ISCC: Clight.is_call_cont k) (TY: type_of_fundef fd = Tfunction targs tres cconv), match_states (Clight.Callstate fd args k m) (Callstate tfd args tk m) | match_returnstate: - forall res k m tk ce - (MK: match_cont ce Tvoid 0%nat 0%nat k tk), + forall res tres k m tk ce + (MK: match_cont ce tres 0%nat 0%nat k tk) + (WT: wt_val res tres), match_states (Clight.Returnstate res k m) (Returnstate res tk m). @@ -1442,7 +1472,9 @@ Proof. - (* set *) auto. - (* call *) - simpl in TR. destruct (classify_fun (typeof e)); monadInv TR. auto. + simpl in TR. destruct (classify_fun (typeof e)); monadInv TR. + unfold make_funcall. + destruct o; auto; destruct Conventions1.return_value_needs_normalization; auto. - (* builtin *) auto. - (* seq *) @@ -1500,24 +1532,26 @@ End FIND_LABEL. (** Properties of call continuations *) Lemma match_cont_call_cont: - forall ce' tyret' nbrk' ncnt' ce tyret nbrk ncnt k tk, + forall ce' nbrk' ncnt' ce tyret nbrk ncnt k tk, match_cont ce tyret nbrk ncnt k tk -> - match_cont ce' tyret' nbrk' ncnt' (Clight.call_cont k) (call_cont tk). + match_cont ce' tyret nbrk' ncnt' (Clight.call_cont k) (call_cont tk). Proof. induction 1; simpl; auto. - constructor. - econstructor; eauto. +- apply match_Kstop. +- eapply match_Kcall; eauto. +- eapply match_Kcall_normalize; eauto. Qed. Lemma match_cont_is_call_cont: - forall ce tyret nbrk ncnt k tk ce' tyret' nbrk' ncnt', + forall ce tyret nbrk ncnt k tk ce' nbrk' ncnt', match_cont ce tyret nbrk ncnt k tk -> Clight.is_call_cont k -> - match_cont ce' tyret' nbrk' ncnt' k tk /\ is_call_cont tk. + match_cont ce' tyret nbrk' ncnt' k tk /\ is_call_cont tk. Proof. intros. inv H; simpl in H0; try contradiction; simpl. - split; auto; constructor. - split; auto; econstructor; eauto. + split; auto; apply match_Kstop. + split; auto; eapply match_Kcall; eauto. + split; auto; eapply match_Kcall_normalize; eauto. Qed. (** The simulation proof *) @@ -1549,19 +1583,44 @@ Proof. - (* call *) revert TR. simpl. case_eq (classify_fun (typeof a)); try congruence. - intros targs tres cc CF TR. monadInv TR. inv MTR. + intros targs tres cc CF TR. monadInv TR. exploit functions_translated; eauto. intros (cu' & tfd & FIND & TFD & LINK'). rewrite H in CF. simpl in CF. inv CF. - econstructor; split. - apply plus_one. econstructor; eauto. - eapply transl_expr_correct with (cunit := cu); eauto. - eapply transl_arglist_correct with (cunit := cu); eauto. - erewrite typlist_of_arglist_eq by eauto. - eapply transl_fundef_sig1; eauto. - rewrite H3. auto. - econstructor; eauto. - eapply match_Kcall with (ce := prog_comp_env cu') (cu := cu); eauto. - simpl. auto. + set (sg := {| sig_args := typlist_of_arglist al targs; + sig_res := rettype_of_type tres; + sig_cc := cc |}) in *. + assert (SIG: funsig tfd = sg). + { unfold sg; erewrite typlist_of_arglist_eq by eauto. + eapply transl_fundef_sig1; eauto. rewrite H3; auto. } + assert (EITHER: tk' = tk /\ ts' = Scall optid sg x x0 + \/ exists id, optid = Some id /\ + tk' = tk /\ ts' = Sseq (Scall optid sg x x0) + (Sset id (make_normalization tres (Evar id)))). + { unfold make_funcall in MTR. + destruct optid. destruct Conventions1.return_value_needs_normalization. + inv MTR. right; exists i; auto. + inv MTR; auto. + inv MTR; auto. } + destruct EITHER as [(EK & ES) | (id & EI & EK & ES)]; rewrite EK, ES. + + (* without normalization of return value *) + econstructor; split. + apply plus_one. eapply step_call; eauto. + eapply transl_expr_correct with (cunit := cu); eauto. + eapply transl_arglist_correct with (cunit := cu); eauto. + econstructor; eauto. + eapply match_Kcall with (ce := prog_comp_env cu') (cu := cu); eauto. + exact I. + + (* with normalization of return value *) + subst optid. + econstructor; split. + eapply plus_two. apply step_seq. eapply step_call; eauto. + eapply transl_expr_correct with (cunit := cu); eauto. + eapply transl_arglist_correct with (cunit := cu); eauto. + traceEq. + econstructor; eauto. + eapply match_Kcall_normalize with (ce := prog_comp_env cu') (cu := cu); eauto. + intros. eapply make_normalization_correct; eauto. constructor; eauto. + exact I. - (* builtin *) monadInv TR. inv MTR. @@ -1658,6 +1717,7 @@ Proof. eapply match_env_free_blocks; eauto. eapply match_returnstate with (ce := prog_comp_env cu); eauto. eapply match_cont_call_cont. eauto. + constructor. - (* return some *) monadInv TR. inv MTR. @@ -1667,6 +1727,7 @@ Proof. eapply match_env_free_blocks; eauto. eapply match_returnstate with (ce := prog_comp_env cu); eauto. eapply match_cont_call_cont. eauto. + apply wt_val_casted. eapply cast_val_is_casted; eauto. - (* skip call *) monadInv TR. inv MTR. @@ -1675,6 +1736,7 @@ Proof. apply plus_one. apply step_skip_call. auto. eapply match_env_free_blocks; eauto. eapply match_returnstate with (ce := prog_comp_env cu); eauto. + constructor. - (* switch *) monadInv TR. @@ -1738,20 +1800,33 @@ Proof. simpl. econstructor; eauto. unfold transl_function. rewrite EQ; simpl. rewrite EQ1; simpl. auto. constructor. + replace (fn_return f) with tres. eassumption. + simpl in TY. unfold type_of_function in TY. congruence. - (* external function *) inv TR. exploit match_cont_is_call_cont; eauto. intros [A B]. econstructor; split. - apply plus_one. constructor. eauto. + apply plus_one. constructor. eapply external_call_symbols_preserved; eauto. apply senv_preserved. eapply match_returnstate with (ce := ce); eauto. + apply has_rettype_wt_val. + replace (rettype_of_type tres0) with (sig_res (ef_sig ef)). + eapply external_call_well_typed_gen; eauto. + rewrite H5. simpl. simpl in TY. congruence. - (* returnstate *) inv MK. - econstructor; split. - apply plus_one. constructor. - econstructor; eauto. simpl; reflexivity. constructor. + + (* without normalization *) + econstructor; split. + apply plus_one. constructor. + econstructor; eauto. simpl; reflexivity. constructor. + + (* with normalization *) + econstructor; split. + eapply plus_three. econstructor. econstructor. constructor. + simpl. apply H13. eauto. apply PTree.gss. + traceEq. + simpl. rewrite PTree.set2. econstructor; eauto. simpl; reflexivity. constructor. Qed. Lemma transl_initial_states: diff --git a/cfrontend/Csyntax.v b/cfrontend/Csyntax.v index c34a5e13..e3e2c1e9 100644 --- a/cfrontend/Csyntax.v +++ b/cfrontend/Csyntax.v @@ -106,7 +106,7 @@ Definition Epreincr (id: incr_or_decr) (l: expr) (ty: type) := Definition Eselection (r1 r2 r3: expr) (ty: type) := let t := typ_of_type ty in - let sg := mksignature (AST.Tint :: t :: t :: nil) (Some t) cc_default in + let sg := mksignature (AST.Tint :: t :: t :: nil) t cc_default in Ebuiltin (EF_builtin "__builtin_sel"%string sg) (Tcons type_bool (Tcons ty (Tcons ty Tnil))) (Econs r1 (Econs r2 (Econs r3 Enil))) diff --git a/cfrontend/Ctypes.v b/cfrontend/Ctypes.v index bfc5daa9..664a60c5 100644 --- a/cfrontend/Ctypes.v +++ b/cfrontend/Ctypes.v @@ -732,8 +732,21 @@ Definition typ_of_type (t: type) : AST.typ := | Tpointer _ _ | Tarray _ _ _ | Tfunction _ _ _ | Tstruct _ _ | Tunion _ _ => AST.Tptr end. -Definition opttyp_of_type (t: type) : option AST.typ := - if type_eq t Tvoid then None else Some (typ_of_type t). +Definition rettype_of_type (t: type) : AST.rettype := + match t with + | Tvoid => AST.Tvoid + | Tint I32 _ _ => AST.Tint + | Tint I8 Signed _ => AST.Tint8signed + | Tint I8 Unsigned _ => AST.Tint8unsigned + | Tint I16 Signed _ => AST.Tint16signed + | Tint I16 Unsigned _ => AST.Tint16unsigned + | Tint IBool _ _ => AST.Tint8unsigned + | Tlong _ _ => AST.Tlong + | Tfloat F32 _ => AST.Tsingle + | Tfloat F64 _ => AST.Tfloat + | Tpointer _ _ => AST.Tptr + | Tarray _ _ _ | Tfunction _ _ _ | Tstruct _ _ | Tunion _ _ => AST.Tvoid + end. Fixpoint typlist_of_typelist (tl: typelist) : list AST.typ := match tl with @@ -742,7 +755,7 @@ Fixpoint typlist_of_typelist (tl: typelist) : list AST.typ := end. Definition signature_of_type (args: typelist) (res: type) (cc: calling_convention): signature := - mksignature (typlist_of_typelist args) (opttyp_of_type res) cc. + mksignature (typlist_of_typelist args) (rettype_of_type res) cc. (** * Construction of the composite environment *) diff --git a/cfrontend/Ctyping.v b/cfrontend/Ctyping.v index b92a9bac..00fcf8ab 100644 --- a/cfrontend/Ctyping.v +++ b/cfrontend/Ctyping.v @@ -397,10 +397,10 @@ Inductive wt_rvalue : expr -> Prop := wt_arguments rargs tyargs -> (* 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) + (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) (Some t) cc_default 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, @@ -521,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. @@ -745,7 +754,7 @@ 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"). @@ -915,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 := @@ -987,6 +997,7 @@ 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. @@ -1240,7 +1251,7 @@ 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. @@ -1372,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. @@ -1394,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 *) @@ -1710,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'. @@ -1749,7 +1788,7 @@ Proof. - (* 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 *. + 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. } @@ -1895,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 -> @@ -1999,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) @@ -2012,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 := @@ -2031,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 @@ -2088,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. @@ -2163,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. @@ -2180,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. diff --git a/cfrontend/PrintCsyntax.ml b/cfrontend/PrintCsyntax.ml index 1c9729c5..03dc5837 100644 --- a/cfrontend/PrintCsyntax.ml +++ b/cfrontend/PrintCsyntax.ml @@ -19,7 +19,7 @@ open Format open Camlcoq open Values open AST -open Ctypes +open! Ctypes open Cop open Csyntax @@ -85,7 +85,7 @@ let name_optid id = let rec name_cdecl id ty = match ty with - | Tvoid -> + | Ctypes.Tvoid -> "void" ^ name_optid id | Ctypes.Tint(sz, sg, a) -> name_inttype sz sg ^ attributes a ^ name_optid id |