From a5ffc59246b09a389e5f8cbc2f217e323e76990f Mon Sep 17 00:00:00 2001 From: xleroy Date: Mon, 13 Jun 2011 18:11:19 +0000 Subject: Revised handling of annotation statements, and more generally built-in functions, and more generally external functions git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1672 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e --- common/AST.v | 87 ++++++++++++++++++++++++++++++++++---- common/Events.v | 129 ++++++++++++++++++++++++++++++++------------------------ 2 files changed, 153 insertions(+), 63 deletions(-) (limited to 'common') diff --git a/common/AST.v b/common/AST.v index bca0535..4f113c7 100644 --- a/common/AST.v +++ b/common/AST.v @@ -397,15 +397,84 @@ Qed. (** * External functions *) (** For most languages, the functions composing the program are either - internal functions, defined within the language, or external functions - (a.k.a. system calls) that emit an event when applied. We define - a type for such functions and some generic transformation functions. *) - -Record external_function : Type := mkextfun { - ef_id: ident; - ef_sig: signature; - ef_inline: bool -}. + internal functions, defined within the language, or external functions, + defined outside. External functions include system calls but also + compiler built-in functions. We define a type for external functions + and associated operations. *) + +Inductive external_function : Type := + | EF_external (name: ident) (sg: signature) + (** A system call or library function. Produces an event + in the trace. *) + | EF_builtin (name: ident) (sg: signature) + (** A compiler built-in function. Behaves like an external, but + can be inlined by the compiler. *) + | EF_vload (chunk: memory_chunk) + (** A volatile read operation. If the adress given as first argument + points within a volatile global variable, generate an + event and return the value found in this event. Otherwise, + produce no event and behave like a regular memory load. *) + | EF_vstore (chunk: memory_chunk) + (** A volatile store operation. If the adress given as first argument + points within a volatile global variable, generate an event. + Otherwise, produce no event and behave like a regular memory store. *) + | EF_malloc + (** Dynamic memory allocation. Takes the requested size in bytes + as argument; returns a pointer to a fresh block of the given size. + Produces no observable event. *) + | EF_free + (** Dynamic memory deallocation. Takes a pointer to a block + allocated by an [EF_malloc] external call and frees the + corresponding block. + Produces no observable event. *) + | EF_memcpy (sz: Z) (al: Z) + (** Block copy, of [sz] bytes, between addresses that are [al]-aligned. *) + | EF_annot (text: ident) (targs: list typ) + (** A programmer-supplied annotation. Takes zero, one or several arguments, + produces an event carrying the text and the values of these arguments, + and returns no value. *) + | EF_annot_val (text:ident) (targ: typ). + (** Another form of annotation that takes one argument, produces + an event carrying the text and the value of this argument, + and returns the value of the argument. *) + +(** The type signature of an external function. *) + +Definition ef_sig (ef: external_function): signature := + match ef with + | EF_external name sg => sg + | EF_builtin name sg => sg + | EF_vload chunk => mksignature (Tint :: nil) (Some (type_of_chunk chunk)) + | EF_vstore chunk => mksignature (Tint :: type_of_chunk chunk :: nil) None + | EF_malloc => mksignature (Tint :: nil) (Some Tint) + | EF_free => mksignature (Tint :: nil) None + | EF_memcpy sz al => mksignature (Tint :: Tint :: nil) None + | EF_annot text targs => mksignature targs None + | EF_annot_val text targ => mksignature (targ :: nil) (Some targ) + end. + +(** Whether an external function should be inlined by the compiler. *) + +Definition ef_inline (ef: external_function) : bool := + match ef with + | EF_external name sg => false + | EF_builtin name sg => true + | EF_vload chunk => true + | EF_vstore chunk => true + | EF_malloc => false + | EF_free => false + | EF_memcpy sz al => true + | EF_annot text targs => true + | EF_annot_val text targ => true + end. + +(** Whether an external function must reload its arguments. *) + +Definition ef_reloads (ef: external_function) : bool := + match ef with + | EF_annot text targs => false + | _ => true + end. (** Function definitions are the union of internal and external functions. *) diff --git a/common/Events.v b/common/Events.v index b369d46..ac6c1a0 100644 --- a/common/Events.v +++ b/common/Events.v @@ -401,41 +401,6 @@ End EVENTVAL_INV. (** * Semantics of external functions *) -(** Each external function is of one of the following kinds: *) - -Inductive extfun_kind: signature -> Type := - | EF_syscall (name: ident) (sg: signature): extfun_kind sg - (** A system call. Takes representable arguments (integers, floats, - pointers to globals), produces a representable result, - does not modify the memory, and produces an [Event_syscall] event - in the trace. *) - | EF_vload (chunk: memory_chunk): extfun_kind (mksignature (Tint :: nil) (Some (type_of_chunk chunk))) - (** A volatile read operation. If the adress given as first argument - points within a volatile global variable, generate an [Event_vload] - event and return the value found in this event. Otherwise, - produce no event and behave like a regular memory load. *) - | EF_vstore (chunk: memory_chunk): extfun_kind (mksignature (Tint :: type_of_chunk chunk :: nil) None) - (** A volatile store operation. If the adress given as first argument - points within a volatile global variable, generate an [Event_vstore] - event. Otherwise, produce no event and behave like a regular memory store. *) - | EF_malloc: extfun_kind (mksignature (Tint :: nil) (Some Tint)) - (** Dynamic memory allocation. Takes the requested size in bytes - as argument; returns a pointer to a fresh block of the given size. - Produces no observable event. *) - | EF_free: extfun_kind (mksignature (Tint :: nil) None) - (** Dynamic memory deallocation. Takes a pointer to a block - allocated by an [EF_malloc] external call and frees the - corresponding block. - Produces no observable event. *) - | EF_annotation (text: ident) (sg: signature): extfun_kind sg. - (** A programmer-supplied annotation. Takes representable arguments, - returns its first argument as result (or [Vundef] if no arguments), - does not modify the memory, and produces an [Event_annot] - event in the trace. *) - -Parameter classify_external_function: - forall (ef: external_function), extfun_kind (ef.(ef_sig)). - (** For each external function, its behavior is defined by a predicate relating: - the global environment - the values of the arguments passed to this function @@ -934,6 +899,20 @@ Proof. inv H; inv H0. intuition congruence. Qed. +(** ** Semantics of [memcpy] operations. *) + +(** To be done once [storebytes] is added to the [Memtype] interface. *) + +Definition extcall_memcpy_sem (sz al: Z) (F V: Type) (ge: Genv.t F V): list val -> mem -> trace -> val -> mem -> Prop := + fun vargs m1 t vres m2 => False. + +Lemma extcall_memcpy_ok: + forall sz al, + extcall_properties (extcall_memcpy_sem sz al) (mksignature (Tint :: Tint :: nil) None). +Proof. + intros. unfold extcall_memcpy_sem; constructor; contradiction. +Qed. + (** ** Semantics of system calls. *) Inductive extcall_io_sem (name: ident) (sg: signature) (F V: Type) (ge: Genv.t F V): @@ -984,23 +963,19 @@ Qed. (** ** Semantics of annotation. *) -Inductive extcall_annot_sem (text: ident) (sg: signature) (F V: Type) (ge: Genv.t F V): +Inductive extcall_annot_sem (text: ident) (targs: list typ) (F V: Type) (ge: Genv.t F V): list val -> mem -> trace -> val -> mem -> Prop := - | extcall_annot_sem_intro: forall vargs m args vres, - eventval_list_match ge args (sig_args sg) vargs -> - sig_res sg = match sig_args sg with nil => None | t1 :: _ => Some t1 end -> - vres = match vargs with nil => Vundef | v1 :: _ => v1 end -> - extcall_annot_sem text sg ge vargs m (Event_annot text args :: E0) vres m. + | extcall_annot_sem_intro: forall vargs m args, + eventval_list_match ge args targs vargs -> + extcall_annot_sem text targs ge vargs m (Event_annot text args :: E0) Vundef m. Lemma extcall_annot_ok: - forall text sg, - extcall_properties (extcall_annot_sem text sg) sg. + forall text targs, + extcall_properties (extcall_annot_sem text targs) (mksignature targs None). Proof. intros; constructor; intros. - inv H. unfold proj_sig_res. rewrite H1. inv H0. - constructor. - eapply eventval_match_type; eauto. + inv H. simpl. auto. inv H. eapply eventval_list_match_length; eauto. @@ -1012,17 +987,15 @@ Proof. inv H; auto. inv H. - exists (match vargs' with nil => Vundef | v1 :: _ => v1 end); exists m1'; intuition. + exists Vundef; exists m1'; intuition. econstructor; eauto. eapply eventval_list_match_lessdef; eauto. - inv H1; auto. red; auto. inv H0. - exists f; exists (match vargs' with nil => Vundef | v1 :: _ => v1 end); exists m1'; intuition. + exists f; exists Vundef; exists m1'; intuition. econstructor; eauto. eapply eventval_list_match_inject; eauto. - inv H2; auto. red; auto. red; auto. red; intros; congruence. @@ -1032,6 +1005,48 @@ Proof. intuition. Qed. +Inductive extcall_annot_val_sem (text: ident) (targ: typ) (F V: Type) (ge: Genv.t F V): + list val -> mem -> trace -> val -> mem -> Prop := + | extcall_annot_val_sem_intro: forall varg m arg, + eventval_match ge arg targ varg -> + extcall_annot_val_sem text targ ge (varg :: nil) m (Event_annot text (arg :: nil) :: E0) varg m. + +Lemma extcall_annot_val_ok: + forall text targ, + extcall_properties (extcall_annot_val_sem text targ) (mksignature (targ :: nil) (Some targ)). +Proof. + intros; constructor; intros. + + inv H. unfold proj_sig_res; simpl. eapply eventval_match_type; eauto. + + inv H. auto. + + inv H1. econstructor; eauto. + eapply eventval_match_preserved; eauto. + + inv H; auto. + + inv H; auto. + + inv H. inv H1. inv H6. + exists v2; exists m1'; intuition. + econstructor; eauto. + eapply eventval_match_lessdef; eauto. + red; auto. + + inv H0. inv H2. inv H7. + exists f; exists v'; exists m1'; intuition. + econstructor; eauto. + eapply eventval_match_inject; eauto. + red; auto. + red; auto. + red; intros; congruence. + + inv H; inv H0. simpl in H1. + assert (arg = arg0). eapply eventval_match_determ_2; eauto. subst arg0. + intuition. +Qed. + (** ** Combined semantics of external calls *) (** Combining the semantics given above for the various kinds of external calls, @@ -1046,26 +1061,32 @@ Qed. This predicate is used in the semantics of all CompCert languages. *) Definition external_call (ef: external_function): extcall_sem := - match classify_external_function ef with - | EF_syscall name sg => extcall_io_sem name sg + match ef with + | EF_external name sg => extcall_io_sem name sg + | EF_builtin name sg => extcall_io_sem name sg | EF_vload chunk => volatile_load_sem chunk | EF_vstore chunk => volatile_store_sem chunk | EF_malloc => extcall_malloc_sem | EF_free => extcall_free_sem - | EF_annotation txt sg => extcall_annot_sem txt sg + | EF_memcpy sz al => extcall_memcpy_sem sz al + | EF_annot txt targs => extcall_annot_sem txt targs + | EF_annot_val txt targ=> extcall_annot_val_sem txt targ end. Theorem external_call_spec: forall ef, extcall_properties (external_call ef) (ef_sig ef). Proof. - intros. unfold external_call. destruct (classify_external_function ef). + intros. unfold external_call, ef_sig. destruct ef. + apply extcall_io_ok. apply extcall_io_ok. apply volatile_load_ok. apply volatile_store_ok. apply extcall_malloc_ok. apply extcall_free_ok. + apply extcall_memcpy_ok. apply extcall_annot_ok. + apply extcall_annot_val_ok. Qed. Definition external_call_well_typed ef := ec_well_typed (external_call_spec ef). -- cgit v1.2.3