diff options
| author | xleroy <xleroy@fca1b0fc-160b-0410-b1d3-a4f43f01ea2e> | 2013-02-24 09:01:28 +0000 |
|---|---|---|
| committer | xleroy <xleroy@fca1b0fc-160b-0410-b1d3-a4f43f01ea2e> | 2013-02-24 09:01:28 +0000 |
| commit | 202bc495442a1a8fa184b73ac0063bdbbbcdf846 (patch) | |
| tree | 46c6920201b823bf47252bc52864b0bf60f3233e /common/Events.v | |
| parent | f774d5f2d604f747e72e2d3bb56cc3f90090e2dd (diff) | |
| download | compcert-kvx-202bc495442a1a8fa184b73ac0063bdbbbcdf846.tar.gz compcert-kvx-202bc495442a1a8fa184b73ac0063bdbbbcdf846.zip | |
Constant propagation within __builtin_annot.
git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2126 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
Diffstat (limited to 'common/Events.v')
| -rw-r--r-- | common/Events.v | 21 |
1 files changed, 15 insertions, 6 deletions
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. |