diff options
Diffstat (limited to 'common')
-rw-r--r-- | common/AST.v | 18 | ||||
-rw-r--r-- | common/Events.v | 21 |
2 files changed, 30 insertions, 9 deletions
diff --git a/common/AST.v b/common/AST.v index d2065d6b..44811b2b 100644 --- a/common/AST.v +++ b/common/AST.v @@ -443,7 +443,7 @@ Inductive external_function : Type := 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) + | EF_annot (text: ident) (targs: list annot_arg) (** 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. *) @@ -451,15 +451,27 @@ Inductive external_function : Type := (** 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. *) - | EF_inline_asm (text: ident). + | EF_inline_asm (text: ident) (** Inline [asm] statements. Semantically, treated like an annotation with no parameters ([EF_annot text nil]). To be used with caution, as it can invalidate the semantic preservation theorem. Generated only if [-finline-asm] is given. *) +with annot_arg : Type := + | AA_arg (ty: typ) + | AA_int (n: int) + | AA_float (n: float). + (** The type signature of an external function. *) +Fixpoint annot_args_typ (targs: list annot_arg) : list typ := + match targs with + | nil => nil + | AA_arg ty :: targs' => ty :: annot_args_typ targs' + | _ :: targs' => annot_args_typ targs' + end. + Definition ef_sig (ef: external_function): signature := match ef with | EF_external name sg => sg @@ -471,7 +483,7 @@ Definition ef_sig (ef: external_function): signature := | 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 text targs => mksignature (annot_args_typ targs) None | EF_annot_val text targ => mksignature (targ :: nil) (Some targ) | EF_inline_asm text => mksignature nil None end. diff --git a/common/Events.v b/common/Events.v index 3f81e60e..e310bfed 100644 --- a/common/Events.v +++ b/common/Events.v @@ -1456,23 +1456,32 @@ Proof. intros EQ; inv EQ. split; auto. eapply eventval_match_determ_1; eauto. Qed. -(** ** Semantics of annotation. *) +(** ** Semantics of annotations. *) + +Fixpoint annot_eventvals (targs: list annot_arg) (vargs: list eventval) : list eventval := + match targs, vargs with + | AA_arg ty :: targs', varg :: vargs' => varg :: annot_eventvals targs' vargs' + | AA_int n :: targs', _ => EVint n :: annot_eventvals targs' vargs + | AA_float n :: targs', _ => EVfloat n :: annot_eventvals targs' vargs + | _, _ => vargs + end. -Inductive extcall_annot_sem (text: ident) (targs: list typ) (F V: Type) (ge: Genv.t F V): +Inductive extcall_annot_sem (text: ident) (targs: list annot_arg) (F V: Type) (ge: Genv.t F V): list val -> mem -> trace -> val -> mem -> Prop := | 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. + eventval_list_match ge args (annot_args_typ targs) vargs -> + extcall_annot_sem text targs ge vargs m + (Event_annot text (annot_eventvals targs args) :: E0) Vundef m. Lemma extcall_annot_ok: forall text targs, - extcall_properties (extcall_annot_sem text targs) (mksignature targs None). + extcall_properties (extcall_annot_sem text targs) (mksignature (annot_args_typ targs) None). Proof. intros; constructor; intros. (* well typed *) inv H. simpl. auto. (* arity *) - inv H. eapply eventval_list_match_length; eauto. + inv H. simpl. eapply eventval_list_match_length; eauto. (* symbols *) inv H1. econstructor; eauto. eapply eventval_list_match_preserved; eauto. |