diff options
Diffstat (limited to 'common')
-rw-r--r-- | common/AST.v | 73 | ||||
-rw-r--r-- | common/Events.v | 175 | ||||
-rw-r--r-- | common/PrintAST.ml | 23 |
3 files changed, 242 insertions, 29 deletions
diff --git a/common/AST.v b/common/AST.v index 9c29a374..d2926178 100644 --- a/common/AST.v +++ b/common/AST.v @@ -576,7 +576,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 annot_arg) + | 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. *) @@ -584,27 +584,15 @@ 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 @@ -616,7 +604,7 @@ Definition ef_sig (ef: external_function): signature := | EF_malloc => mksignature (Tint :: nil) (Some Tint) cc_default | EF_free => mksignature (Tint :: nil) None cc_default | EF_memcpy sz al => mksignature (Tint :: Tint :: nil) None cc_default - | EF_annot text targs => mksignature (annot_args_typ targs) None cc_default + | EF_annot text targs => mksignature targs None cc_default | EF_annot_val text targ => mksignature (targ :: nil) (Some targ) cc_default | EF_inline_asm text => mksignature nil None cc_default end. @@ -653,7 +641,7 @@ Definition external_function_eq: forall (ef1 ef2: external_function), {ef1=ef2} Proof. generalize ident_eq signature_eq chunk_eq typ_eq zeq Int.eq_dec; intros. decide equality. - apply list_eq_dec. decide equality. apply Float.eq_dec. + apply list_eq_dec. auto. Defined. Global Opaque external_function_eq. @@ -699,3 +687,56 @@ Definition transf_partial_fundef (fd: fundef A): res (fundef B) := end. End TRANSF_PARTIAL_FUNDEF. + +(** * Arguments to annotations *) + +Set Contextual Implicit. + +Inductive annot_arg (A: Type) : Type := + | AA_base (x: A) + | AA_int (n: int) + | AA_long (n: int64) + | AA_float (f: float) + | AA_single (f: float32) + | AA_loadstack (chunk: memory_chunk) (ofs: int) + | AA_addrstack (ofs: int) + | AA_loadglobal (chunk: memory_chunk) (id: ident) (ofs: int) + | AA_addrglobal (id: ident) (ofs: int) + | AA_longofwords (hi lo: annot_arg A). + +Fixpoint globals_of_annot_arg (A: Type) (a: annot_arg A) : list ident := + match a with + | AA_loadglobal chunk id ofs => id :: nil + | AA_addrglobal id ofs => id :: nil + | AA_longofwords hi lo => globals_of_annot_arg hi ++ globals_of_annot_arg lo + | _ => nil + end. + +Definition globals_of_annot_args (A: Type) (al: list (annot_arg A)) : list ident := + List.fold_right (fun a l => globals_of_annot_arg a ++ l) nil al. + +Fixpoint params_of_annot_arg (A: Type) (a: annot_arg A) : list A := + match a with + | AA_base x => x :: nil + | AA_longofwords hi lo => params_of_annot_arg hi ++ params_of_annot_arg lo + | _ => nil + end. + +Definition params_of_annot_args (A: Type) (al: list (annot_arg A)) : list A := + List.fold_right (fun a l => params_of_annot_arg a ++ l) nil al. + +Fixpoint map_annot_arg (A B: Type) (f: A -> B) (a: annot_arg A) : annot_arg B := + match a with + | AA_base x => AA_base (f x) + | AA_int n => AA_int n + | AA_long n => AA_long n + | AA_float n => AA_float n + | AA_single n => AA_single n + | AA_loadstack chunk ofs => AA_loadstack chunk ofs + | AA_addrstack ofs => AA_addrstack ofs + | AA_loadglobal chunk id ofs => AA_loadglobal chunk id ofs + | AA_addrglobal id ofs => AA_addrglobal id ofs + | AA_longofwords hi lo => + AA_longofwords (map_annot_arg f hi) (map_annot_arg f lo) + end. + diff --git a/common/Events.v b/common/Events.v index 3fb58806..ad59ece9 100644 --- a/common/Events.v +++ b/common/Events.v @@ -1344,25 +1344,16 @@ Qed. (** ** 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 annot_arg) (ge: Senv.t): +Inductive extcall_annot_sem (text: ident) (targs: list typ) (ge: Senv.t): list val -> mem -> trace -> val -> mem -> Prop := | extcall_annot_sem_intro: forall vargs m args, - 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. + 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 targs, extcall_properties (extcall_annot_sem text targs) - (mksignature (annot_args_typ targs) None cc_default) + (mksignature targs None cc_default) nil. Proof. intros; constructor; intros. @@ -1794,9 +1785,167 @@ Proof. split; congruence. Qed. +(** * Evaluation of annotation arguments *) + +Section EVAL_ANNOT_ARG. + +Variable A: Type. +Variable ge: Senv.t. +Variable e: A -> val. +Variable sp: val. +Variable m: mem. + +Inductive eval_annot_arg: annot_arg A -> val -> Prop := + | eval_AA_base: forall x, + eval_annot_arg (AA_base x) (e x) + | eval_AA_int: forall n, + eval_annot_arg (AA_int n) (Vint n) + | eval_AA_long: forall n, + eval_annot_arg (AA_long n) (Vlong n) + | eval_AA_float: forall n, + eval_annot_arg (AA_float n) (Vfloat n) + | eval_AA_single: forall n, + eval_annot_arg (AA_single n) (Vsingle n) + | eval_AA_loadstack: forall chunk ofs v, + Mem.loadv chunk m (Val.add sp (Vint ofs)) = Some v -> + eval_annot_arg (AA_loadstack chunk ofs) v + | eval_AA_addrstack: forall ofs, + eval_annot_arg (AA_addrstack ofs) (Val.add sp (Vint ofs)) + | eval_AA_loadglobal: forall chunk id ofs v, + Mem.loadv chunk m (Senv.symbol_address ge id ofs) = Some v -> + eval_annot_arg (AA_loadglobal chunk id ofs) v + | eval_AA_addrglobal: forall id ofs, + eval_annot_arg (AA_addrglobal id ofs) (Senv.symbol_address ge id ofs) + | eval_AA_longofwords: forall hi lo vhi vlo, + eval_annot_arg hi vhi -> eval_annot_arg lo vlo -> + eval_annot_arg (AA_longofwords hi lo) (Val.longofwords vhi vlo). + +Definition eval_annot_args (al: list (annot_arg A)) (vl: list val) : Prop := + list_forall2 eval_annot_arg al vl. + +Lemma eval_annot_arg_determ: + forall a v, eval_annot_arg a v -> forall v', eval_annot_arg a v' -> v' = v. +Proof. + induction 1; intros v' EV; inv EV; try congruence. + f_equal; eauto. +Qed. + +Lemma eval_annot_args_determ: + forall al vl, eval_annot_args al vl -> forall vl', eval_annot_args al vl' -> vl' = vl. +Proof. + induction 1; intros v' EV; inv EV; f_equal; eauto using eval_annot_arg_determ. +Qed. + +End EVAL_ANNOT_ARG. + +Hint Constructors eval_annot_arg: aarg. + +(** Invariance by change of global environment. *) + +Section EVAL_ANNOT_ARG_PRESERVED. + +Variables A F1 V1 F2 V2: Type. +Variable ge1: Genv.t F1 V1. +Variable ge2: Genv.t F2 V2. +Variable e: A -> val. +Variable sp: val. +Variable m: mem. + +Hypothesis symbols_preserved: + forall id, Genv.find_symbol ge2 id = Genv.find_symbol ge1 id. + +Lemma eval_annot_arg_preserved: + forall a v, eval_annot_arg ge1 e sp m a v -> eval_annot_arg ge2 e sp m a v. +Proof. + assert (EQ: forall id ofs, Senv.symbol_address ge2 id ofs = Senv.symbol_address ge1 id ofs). + { unfold Senv.symbol_address; simpl; intros. rewrite symbols_preserved; auto. } + induction 1; eauto with aarg. rewrite <- EQ in H; eauto with aarg. rewrite <- EQ; eauto with aarg. +Qed. + +Lemma eval_annot_args_preserved: + forall al vl, eval_annot_args ge1 e sp m al vl -> eval_annot_args ge2 e sp m al vl. +Proof. + induction 1; constructor; auto; eapply eval_annot_arg_preserved; eauto. +Qed. + +End EVAL_ANNOT_ARG_PRESERVED. + +(** Compatibility with the "is less defined than" relation. *) + +Section EVAL_ANNOT_ARG_LESSDEF. + +Variable A: Type. +Variable ge: Senv.t. +Variables e1 e2: A -> val. +Variable sp: val. +Variables m1 m2: mem. +Hypothesis env_lessdef: forall x, Val.lessdef (e1 x) (e2 x). +Hypothesis mem_extends: Mem.extends m1 m2. +Lemma eval_annot_arg_lessdef: + forall a v1, eval_annot_arg ge e1 sp m1 a v1 -> + exists v2, eval_annot_arg ge e2 sp m2 a v2 /\ Val.lessdef v1 v2. +Proof. + induction 1. +- exists (e2 x); auto with aarg. +- econstructor; eauto with aarg. +- econstructor; eauto with aarg. +- econstructor; eauto with aarg. +- econstructor; eauto with aarg. +- exploit Mem.loadv_extends; eauto. intros (v' & P & Q). exists v'; eauto with aarg. +- econstructor; eauto with aarg. +- exploit Mem.loadv_extends; eauto. intros (v' & P & Q). exists v'; eauto with aarg. +- econstructor; eauto with aarg. +- destruct IHeval_annot_arg1 as (vhi' & P & Q). + destruct IHeval_annot_arg2 as (vlo' & R & S). + econstructor; split; eauto with aarg. apply Val.longofwords_lessdef; auto. +Qed. + +Lemma eval_annot_args_lessdef: + forall al vl1, eval_annot_args ge e1 sp m1 al vl1 -> + exists vl2, eval_annot_args ge e2 sp m2 al vl2 /\ Val.lessdef_list vl1 vl2. +Proof. + induction 1. +- econstructor; split. constructor. auto. +- exploit eval_annot_arg_lessdef; eauto. intros (v1' & P & Q). + destruct IHlist_forall2 as (vl' & U & V). + exists (v1'::vl'); split; constructor; auto. +Qed. + +End EVAL_ANNOT_ARG_LESSDEF. + +(** Extensionality *) + +Section EVAL_ANNOT_ARG_EXTEN. + +Variable A: Type. +Variable ge: Senv.t. +Variables e1 e2: A -> val. +Variable sp: val. +Variable m: mem. + +Lemma eval_annot_arg_exten: + forall a v, eval_annot_arg ge e1 sp m a v -> + (forall x, In x (params_of_annot_arg a) -> e2 x = e1 x) -> + eval_annot_arg ge e2 sp m a v. +Proof. + induction 1; simpl; intros EXT; try (now constructor). +- rewrite <- EXT by auto. constructor. +- constructor; eauto using in_or_app. +Qed. + +Lemma eval_annot_args_exten: + forall a v, eval_annot_args ge e1 sp m a v -> + (forall x, In x (params_of_annot_args a) -> e2 x = e1 x) -> + eval_annot_args ge e2 sp m a v. +Proof. + induction 1; simpl; intros EXT; constructor. + eapply eval_annot_arg_exten; eauto using in_or_app. + eapply IHlist_forall2; eauto using in_or_app. +Qed. +End EVAL_ANNOT_ARG_EXTEN. diff --git a/common/PrintAST.ml b/common/PrintAST.ml index c0eab04f..e4d79c3e 100644 --- a/common/PrintAST.ml +++ b/common/PrintAST.ml @@ -54,3 +54,26 @@ let name_of_external = function | EF_annot(text, targs) -> sprintf "annot %S" (extern_atom text) | EF_annot_val(text, targ) -> sprintf "annot_val %S" (extern_atom text) | EF_inline_asm text -> sprintf "inline_asm %S" (extern_atom text) + +let print_annot_arg px oc = function + | AA_base x -> px oc x + | AA_int n -> fprintf oc "int %ld" (camlint_of_coqint n) + | AA_long n -> fprintf oc "long %Ld" (camlint64_of_coqint n) + | AA_float n -> fprintf oc "float %F" (camlfloat_of_coqfloat n) + | AA_single n -> fprintf oc "single %F" (camlfloat_of_coqfloat32 n) + | AA_loadstack(chunk, ofs) -> + fprintf oc "%s[sp + %ld]" (name_of_chunk chunk) (camlint_of_coqint ofs) + | AA_addrstack(ofs) -> + fprintf oc "sp + %ld" (camlint_of_coqint ofs) + | AA_loadglobal(chunk, id, ofs) -> + fprintf oc "%s[&%s + %ld]" + (name_of_chunk chunk) (extern_atom id) (camlint_of_coqint ofs) + | AA_addrglobal(id, ofs) -> + fprintf oc "&%s + %ld" (extern_atom id) (camlint_of_coqint ofs) + | AA_longofwords(hi, lo) -> fprintf oc "longofwords %a %a" px hi px lo + +let rec print_annot_args px oc = function + | [] -> () + | [a] -> print_annot_arg px oc a + | a1 :: al -> + fprintf oc "%a, %a" (print_annot_arg px) a1 (print_annot_args px) al |