From 54f97d1988f623ba7422e13a504caeb5701ba93c Mon Sep 17 00:00:00 2001 From: Xavier Leroy Date: Fri, 21 Aug 2015 11:05:36 +0200 Subject: Refactoring of builtins and annotations in the back-end. Before, the back-end languages had distinct instructions - Iannot for annotations, taking structured expressions (annot_arg) as arguments, and producing no results' - Ibuiltin for other builtins, using simple pseudoregs/locations/registers as arguments and results. This branch enriches Ibuiltin instructions so that they take structured expressions (builtin_arg and builtin_res) as arguments and results. This way, - Annotations fit the general pattern of builtin functions, so Iannot instructions are removed. - EF_vload_global and EF_vstore_global become useless, as the same optimization can be achieved by EF_vload/vstore taking a structured argument of the "address of global" kind. - Better code can be generated for builtin_memcpy between stack locations, or volatile accesses to stack locations. Finally, this commit also introduces a new kind of external function, EF_debug, which is like EF_annot but produces no observable events. It will be used later to transport debug info through the back-end, without preventing optimizations. --- common/Events.v | 464 +++++++++++++++++++++++--------------------------------- 1 file changed, 186 insertions(+), 278 deletions(-) (limited to 'common/Events.v') diff --git a/common/Events.v b/common/Events.v index 78162fff..ab418ba5 100644 --- a/common/Events.v +++ b/common/Events.v @@ -606,8 +606,7 @@ Definition inject_separated (f f': meminj) (m1 m2: mem): Prop := f b1 = None -> f' b1 = Some(b2, delta) -> ~Mem.valid_block m1 b1 /\ ~Mem.valid_block m2 b2. -Record extcall_properties (sem: extcall_sem) - (sg: signature) (free_globals: list ident) : Prop := +Record extcall_properties (sem: extcall_sem) (sg: signature) : Prop := mk_extcall_properties { (** The return value of an external call must agree with its signature. *) @@ -664,9 +663,6 @@ Record extcall_properties (sem: extcall_sem) ec_mem_inject: forall ge1 ge2 vargs m1 t vres m2 f m1' vargs', symbols_inject f ge1 ge2 -> - (forall id b1, - In id free_globals -> Senv.find_symbol ge1 id = Some b1 -> - exists b2, f b1 = Some(b2, 0) /\ Senv.find_symbol ge2 id = Some b2) -> sem ge1 vargs m1 t vres m2 -> Mem.inject f m1 m1' -> Val.inject_list f vargs vargs' -> @@ -769,37 +765,36 @@ Qed. Lemma volatile_load_ok: forall chunk, extcall_properties (volatile_load_sem chunk) - (mksignature (Tint :: nil) (Some (type_of_chunk chunk)) cc_default) - nil. + (mksignature (Tint :: nil) (Some (type_of_chunk chunk)) cc_default). Proof. intros; constructor; intros. (* well typed *) - unfold proj_sig_res; simpl. inv H. inv H0. apply Val.load_result_type. +- unfold proj_sig_res; simpl. inv H. inv H0. apply Val.load_result_type. eapply Mem.load_type; eauto. (* symbols *) - inv H2. constructor. eapply volatile_load_preserved; eauto. +- inv H2. constructor. eapply volatile_load_preserved; eauto. (* valid blocks *) - inv H; auto. +- inv H; auto. (* max perms *) - inv H; auto. +- inv H; auto. (* readonly *) - inv H. apply Mem.unchanged_on_refl. +- inv H. apply Mem.unchanged_on_refl. (* mem extends *) - inv H. inv H1. inv H6. inv H4. +- inv H. inv H1. inv H6. inv H4. exploit volatile_load_extends; eauto. intros [v' [A B]]. exists v'; exists m1'; intuition. constructor; auto. (* mem injects *) - inv H1. inv H3. inv H8. inversion H6; subst. +- inv H0. inv H2. inv H7. inversion H5; subst. exploit volatile_load_inject; eauto. intros [v' [A B]]. exists f; exists v'; exists m1'; intuition. constructor; auto. red; intros. congruence. (* trace length *) - inv H; inv H0; simpl; omega. +- inv H; inv H0; simpl; omega. (* receptive *) - inv H. exploit volatile_load_receptive; eauto. intros [v2 A]. +- inv H. exploit volatile_load_receptive; eauto. intros [v2 A]. exists v2; exists m1; constructor; auto. (* determ *) - inv H; inv H0. inv H1; inv H7; try congruence. +- inv H; inv H0. inv H1; inv H7; try congruence. assert (id = id0) by (eapply Senv.find_symbol_injective; eauto). subst id0. split. constructor. eapply eventval_match_valid; eauto. @@ -811,64 +806,6 @@ Proof. split. constructor. intuition congruence. Qed. -Inductive volatile_load_global_sem (chunk: memory_chunk) (id: ident) (ofs: int) (ge: Senv.t): - list val -> mem -> trace -> val -> mem -> Prop := - | volatile_load_global_sem_intro: forall b t v m, - Senv.find_symbol ge id = Some b -> - volatile_load ge chunk m b ofs t v -> - volatile_load_global_sem chunk id ofs ge nil m t v m. - -Remark volatile_load_global_charact: - forall chunk id ofs ge vargs m t vres m', - volatile_load_global_sem chunk id ofs ge vargs m t vres m' <-> - exists b, Senv.find_symbol ge id = Some b /\ volatile_load_sem chunk ge (Vptr b ofs :: vargs) m t vres m'. -Proof. - intros; split. - intros. inv H. exists b; split; auto. constructor; auto. - intros [b [P Q]]. inv Q. econstructor; eauto. -Qed. - -Lemma volatile_load_global_ok: - forall chunk id ofs, - extcall_properties (volatile_load_global_sem chunk id ofs) - (mksignature nil (Some (type_of_chunk chunk)) cc_default) - (id :: nil). -Proof. - intros; constructor; intros. -(* well typed *) - unfold proj_sig_res; simpl. inv H. inv H1. apply Val.load_result_type. - eapply Mem.load_type; eauto. -(* symbols *) - inv H2. econstructor. rewrite H; eauto. eapply volatile_load_preserved; eauto. -(* valid blocks *) - inv H; auto. -(* max perm *) - inv H; auto. -(* readonly *) - inv H. apply Mem.unchanged_on_refl. -(* extends *) - inv H. inv H1. exploit volatile_load_extends; eauto. intros [v' [A B]]. - exists v'; exists m1'; intuition. econstructor; eauto. -(* inject *) - inv H1. inv H3. - exploit H0; eauto with coqlib. intros (b2 & INJ & FS2). - assert (Val.inject f (Vptr b ofs) (Vptr b2 ofs)). - econstructor; eauto. rewrite Int.add_zero; auto. - exploit volatile_load_inject; eauto. intros [v' [A B]]. - exists f; exists v'; exists m1'; intuition. econstructor; eauto. - red; intros; congruence. -(* trace length *) - inv H; inv H1; simpl; omega. -(* receptive *) - inv H. exploit volatile_load_receptive; eauto. intros [v2 A]. - exists v2; exists m1; econstructor; eauto. -(* determ *) - rewrite volatile_load_global_charact in *. - destruct H as [b1 [A1 B1]]. destruct H0 as [b2 [A2 B2]]. - rewrite A1 in A2; inv A2. - eapply ec_determ. eapply volatile_load_ok. eauto. eauto. -Qed. - (** ** Semantics of volatile stores *) Inductive volatile_store_sem (chunk: memory_chunk) (ge: Senv.t): @@ -981,99 +918,40 @@ Qed. Lemma volatile_store_ok: forall chunk, extcall_properties (volatile_store_sem chunk) - (mksignature (Tint :: type_of_chunk chunk :: nil) None cc_default) - nil. + (mksignature (Tint :: type_of_chunk chunk :: nil) None cc_default). Proof. intros; constructor; intros. (* well typed *) - unfold proj_sig_res; simpl. inv H; constructor. +- unfold proj_sig_res; simpl. inv H; constructor. (* symbols preserved *) - inv H2. constructor. eapply volatile_store_preserved; eauto. +- inv H2. constructor. eapply volatile_store_preserved; eauto. (* valid block *) - inv H. inv H1. auto. eauto with mem. +- inv H. inv H1. auto. eauto with mem. (* perms *) - inv H. inv H2. auto. eauto with mem. +- inv H. inv H2. auto. eauto with mem. (* readonly *) - inv H. eapply volatile_store_readonly; eauto. +- inv H. eapply volatile_store_readonly; eauto. (* mem extends*) - inv H. inv H1. inv H6. inv H7. inv H4. +- inv H. inv H1. inv H6. inv H7. inv H4. exploit volatile_store_extends; eauto. intros [m2' [A [B C]]]. exists Vundef; exists m2'; intuition. constructor; auto. (* mem inject *) - inv H1. inv H3. inv H8. inv H9. inversion H6; subst. +- inv H0. inv H2. inv H7. inv H8. inversion H5; subst. exploit volatile_store_inject; eauto. intros [m2' [A [B [C D]]]]. exists f; exists Vundef; exists m2'; intuition. constructor; auto. red; intros; congruence. (* trace length *) - inv H; inv H0; simpl; omega. +- inv H; inv H0; simpl; omega. (* receptive *) - assert (t1 = t2). inv H. eapply volatile_store_receptive; eauto. +- assert (t1 = t2). inv H. eapply volatile_store_receptive; eauto. subst t2; exists vres1; exists m1; auto. (* determ *) - inv H; inv H0. inv H1; inv H8; try congruence. +- inv H; inv H0. inv H1; inv H8; try congruence. assert (id = id0) by (eapply Senv.find_symbol_injective; eauto). subst id0. assert (ev = ev0) by (eapply eventval_match_determ_2; eauto). subst ev0. split. constructor. auto. split. constructor. intuition congruence. Qed. -Inductive volatile_store_global_sem (chunk: memory_chunk) (id: ident) (ofs: int) (ge: Senv.t): - list val -> mem -> trace -> val -> mem -> Prop := - | volatile_store_global_sem_intro: forall b m1 v t m2, - Senv.find_symbol ge id = Some b -> - volatile_store ge chunk m1 b ofs v t m2 -> - volatile_store_global_sem chunk id ofs ge (v :: nil) m1 t Vundef m2. - -Remark volatile_store_global_charact: - forall chunk id ofs ge vargs m t vres m', - volatile_store_global_sem chunk id ofs ge vargs m t vres m' <-> - exists b, Senv.find_symbol ge id = Some b /\ volatile_store_sem chunk ge (Vptr b ofs :: vargs) m t vres m'. -Proof. - intros; split. - intros. inv H; exists b; split; auto; econstructor; eauto. - intros [b [P Q]]. inv Q. econstructor; eauto. -Qed. - -Lemma volatile_store_global_ok: - forall chunk id ofs, - extcall_properties (volatile_store_global_sem chunk id ofs) - (mksignature (type_of_chunk chunk :: nil) None cc_default) - (id :: nil). -Proof. - intros; constructor; intros. -(* well typed *) - unfold proj_sig_res; simpl. inv H; constructor. -(* symbols preserved *) - inv H2. econstructor. rewrite H; eauto. eapply volatile_store_preserved; eauto. -(* valid block *) - inv H. inv H2. auto. eauto with mem. -(* perms *) - inv H. inv H3. auto. eauto with mem. -(* readonly *) - inv H. eapply volatile_store_readonly; eauto. -(* mem extends*) - rewrite volatile_store_global_charact in H. destruct H as [b [P Q]]. - exploit ec_mem_extends. eapply volatile_store_ok. eexact Q. eauto. eauto. - intros [vres' [m2' [A [B [C D]]]]]. - exists vres'; exists m2'; intuition. rewrite volatile_store_global_charact. exists b; auto. -(* mem inject *) - rewrite volatile_store_global_charact in H1. destruct H1 as [b [P Q]]. - exploit H0; eauto with coqlib. intros (b2 & INJ & FS2). - assert (Val.inject f (Vptr b ofs) (Vptr b2 ofs)). econstructor; eauto. rewrite Int.add_zero; auto. - exploit ec_mem_inject. eapply volatile_store_ok. eauto. intuition. eexact Q. eauto. constructor. eauto. eauto. - intros [f' [vres' [m2' [A [B [C [D [E G]]]]]]]]. - exists f'; exists vres'; exists m2'; intuition. - rewrite volatile_store_global_charact. exists b2; auto. -(* trace length *) - inv H. inv H1; simpl; omega. -(* receptive *) - assert (t1 = t2). inv H. eapply volatile_store_receptive; eauto. subst t2. - exists vres1; exists m1; congruence. -(* determ *) - rewrite volatile_store_global_charact in *. - destruct H as [b1 [A1 B1]]. destruct H0 as [b2 [A2 B2]]. rewrite A1 in A2; inv A2. - eapply ec_determ. eapply volatile_store_ok. eauto. eauto. -Qed. - (** ** Semantics of dynamic memory allocation (malloc) *) Inductive extcall_malloc_sem (ge: Senv.t): @@ -1085,8 +963,7 @@ Inductive extcall_malloc_sem (ge: Senv.t): Lemma extcall_malloc_ok: extcall_properties extcall_malloc_sem - (mksignature (Tint :: nil) (Some Tint) cc_default) - nil. + (mksignature (Tint :: nil) (Some Tint) cc_default). Proof. assert (UNCHANGED: forall (P: block -> Z -> Prop) m n m' b m'', @@ -1104,19 +981,19 @@ Proof. constructor; intros. (* well typed *) - inv H. unfold proj_sig_res; simpl. auto. +- inv H. unfold proj_sig_res; simpl. auto. (* symbols preserved *) - inv H2; econstructor; eauto. +- inv H2; econstructor; eauto. (* valid block *) - inv H. eauto with mem. +- inv H. eauto with mem. (* perms *) - inv H. exploit Mem.perm_alloc_inv. eauto. eapply Mem.perm_store_2; eauto. +- inv H. exploit Mem.perm_alloc_inv. eauto. eapply Mem.perm_store_2; eauto. rewrite dec_eq_false. auto. apply Mem.valid_not_valid_diff with m1; eauto with mem. (* readonly *) - inv H. eapply UNCHANGED; eauto. +- inv H. eapply UNCHANGED; eauto. (* mem extends *) - inv H. inv H1. inv H5. inv H7. +- inv H. inv H1. inv H5. inv H7. exploit Mem.alloc_extends; eauto. apply Zle_refl. apply Zle_refl. intros [m3' [A B]]. exploit Mem.store_within_extends. eexact B. eauto. @@ -1126,7 +1003,7 @@ Proof. econstructor; eauto. eapply UNCHANGED; eauto. (* mem injects *) - inv H1. inv H3. inv H7. inv H9. +- inv H0. inv H2. inv H6. inv H8. exploit Mem.alloc_parallel_inject; eauto. apply Zle_refl. apply Zle_refl. intros [f' [m3' [b' [ALLOC [A [B [C D]]]]]]]. exploit Mem.store_mapped_inject. eexact A. eauto. eauto. @@ -1138,15 +1015,15 @@ Proof. eapply UNCHANGED; eauto. eapply UNCHANGED; eauto. red; intros. destruct (eq_block b1 b). - subst b1. rewrite C in H3. inv H3. eauto with mem. - rewrite D in H3 by auto. congruence. + subst b1. rewrite C in H2. inv H2. eauto with mem. + rewrite D in H2 by auto. congruence. (* trace length *) - inv H; simpl; omega. +- inv H; simpl; omega. (* receptive *) - assert (t1 = t2). inv H; inv H0; auto. subst t2. +- assert (t1 = t2). inv H; inv H0; auto. subst t2. exists vres1; exists m1; auto. (* determ *) - inv H; inv H0. split. constructor. intuition congruence. +- inv H; inv H0. split. constructor. intuition congruence. Qed. (** ** Semantics of dynamic memory deallocation (free) *) @@ -1161,25 +1038,24 @@ Inductive extcall_free_sem (ge: Senv.t): Lemma extcall_free_ok: extcall_properties extcall_free_sem - (mksignature (Tint :: nil) None cc_default) - nil. + (mksignature (Tint :: nil) None cc_default). Proof. constructor; intros. (* well typed *) - inv H. unfold proj_sig_res. simpl. auto. +- inv H. unfold proj_sig_res. simpl. auto. (* symbols preserved *) - inv H2; econstructor; eauto. +- inv H2; econstructor; eauto. (* valid block *) - inv H. eauto with mem. +- inv H. eauto with mem. (* perms *) - inv H. eapply Mem.perm_free_3; eauto. +- inv H. eapply Mem.perm_free_3; eauto. (* readonly *) - inv H. eapply Mem.free_unchanged_on; eauto. +- inv H. eapply Mem.free_unchanged_on; eauto. intros. red; intros. elim H3. apply Mem.perm_cur_max. apply Mem.perm_implies with Freeable; auto with mem. eapply Mem.free_range_perm; eauto. (* mem extends *) - inv H. inv H1. inv H8. inv H6. +- inv H. inv H1. inv H8. inv H6. exploit Mem.load_extends; eauto. intros [vsz [A B]]. inv B. exploit Mem.free_parallel_extends; eauto. intros [m2' [C D]]. exists Vundef; exists m2'; intuition. @@ -1191,13 +1067,13 @@ Proof. eapply Mem.free_range_perm. eexact H4. eauto. } tauto. (* mem inject *) - inv H1. inv H3. inv H8. inv H10. +- inv H0. inv H2. inv H7. inv H9. exploit Mem.load_inject; eauto. intros [vsz [A B]]. inv B. assert (Mem.range_perm m1 b (Int.unsigned lo - 4) (Int.unsigned lo + Int.unsigned sz) Cur Freeable). eapply Mem.free_range_perm; eauto. exploit Mem.address_inject; eauto. apply Mem.perm_implies with Freeable; auto with mem. - apply H1. instantiate (1 := lo). omega. + apply H0. instantiate (1 := lo). omega. intro EQ. exploit Mem.free_parallel_inject; eauto. intros (m2' & C & D). exists f, Vundef, m2'; split. @@ -1209,18 +1085,18 @@ Proof. split. auto. split. eapply Mem.free_unchanged_on; eauto. unfold loc_unmapped. intros; congruence. split. eapply Mem.free_unchanged_on; eauto. unfold loc_out_of_reach. - intros. red; intros. eelim H8; eauto. + intros. red; intros. eelim H7; eauto. apply Mem.perm_cur_max. apply Mem.perm_implies with Freeable; auto with mem. - apply H1. omega. + apply H0. omega. split. auto. red; intros. congruence. (* trace length *) - inv H; simpl; omega. +- inv H; simpl; omega. (* receptive *) - assert (t1 = t2). inv H; inv H0; auto. subst t2. +- assert (t1 = t2). inv H; inv H0; auto. subst t2. exists vres1; exists m1; auto. (* determ *) - inv H; inv H0. split. constructor. intuition congruence. +- inv H; inv H0. split. constructor. intuition congruence. Qed. (** ** Semantics of [memcpy] operations. *) @@ -1241,8 +1117,7 @@ Inductive extcall_memcpy_sem (sz al: Z) (ge: Senv.t): Lemma extcall_memcpy_ok: forall sz al, extcall_properties (extcall_memcpy_sem sz al) - (mksignature (Tint :: Tint :: nil) None cc_default) - nil. + (mksignature (Tint :: Tint :: nil) None cc_default). Proof. intros. constructor. - (* return type *) @@ -1274,7 +1149,7 @@ Proof. erewrite list_forall2_length; eauto. tauto. - (* injections *) - intros. inv H1. inv H3. inv H15. inv H16. inv H12. inv H13. + intros. inv H0. inv H2. inv H14. inv H15. inv H11. inv H12. destruct (zeq sz 0). + (* special case sz = 0 *) assert (bytes = nil). @@ -1325,7 +1200,7 @@ Proof. split. eapply Mem.storebytes_unchanged_on; eauto. unfold loc_unmapped; intros. congruence. split. eapply Mem.storebytes_unchanged_on; eauto. unfold loc_out_of_reach; intros. red; intros. - eelim H3; eauto. + eelim H2; eauto. apply Mem.perm_cur_max. apply Mem.perm_implies with Writable; auto with mem. eapply Mem.storebytes_range_perm; eauto. erewrite list_forall2_length; eauto. @@ -1353,39 +1228,38 @@ Inductive extcall_annot_sem (text: ident) (targs: list typ) (ge: Senv.t): Lemma extcall_annot_ok: forall text targs, extcall_properties (extcall_annot_sem text targs) - (mksignature targs None cc_default) - nil. + (mksignature targs None cc_default). Proof. intros; constructor; intros. (* well typed *) - inv H. simpl. auto. +- inv H. simpl. auto. (* symbols *) - inv H2. econstructor; eauto. +- inv H2. econstructor; eauto. eapply eventval_list_match_preserved; eauto. (* valid blocks *) - inv H; auto. +- inv H; auto. (* perms *) - inv H; auto. +- inv H; auto. (* readonly *) - inv H. apply Mem.unchanged_on_refl. +- inv H. apply Mem.unchanged_on_refl. (* mem extends *) - inv H. +- inv H. exists Vundef; exists m1'; intuition. econstructor; eauto. eapply eventval_list_match_lessdef; eauto. (* mem injects *) - inv H1. +- inv H0. exists f; exists Vundef; exists m1'; intuition. econstructor; eauto. eapply eventval_list_match_inject; eauto. red; intros; congruence. (* trace length *) - inv H; simpl; omega. +- inv H; simpl; omega. (* receptive *) - assert (t1 = t2). inv H; inv H0; auto. +- assert (t1 = t2). inv H; inv H0; auto. exists vres1; exists m1; congruence. (* determ *) - inv H; inv H0. +- inv H; inv H0. assert (args = args0). eapply eventval_list_match_determ_2; eauto. subst args0. split. constructor. auto. Qed. @@ -1399,43 +1273,81 @@ Inductive extcall_annot_val_sem (text: ident) (targ: typ) (ge: Senv.t): Lemma extcall_annot_val_ok: forall text targ, extcall_properties (extcall_annot_val_sem text targ) - (mksignature (targ :: nil) (Some targ) cc_default) - nil. + (mksignature (targ :: nil) (Some targ) cc_default). Proof. intros; constructor; intros. (* well typed *) - inv H. unfold proj_sig_res; simpl. eapply eventval_match_type; eauto. +- inv H. unfold proj_sig_res; simpl. eapply eventval_match_type; eauto. (* symbols *) - inv H2. econstructor; eauto. +- inv H2. econstructor; eauto. eapply eventval_match_preserved; eauto. (* valid blocks *) - inv H; auto. +- inv H; auto. (* perms *) - inv H; auto. +- inv H; auto. (* readonly *) - inv H. apply Mem.unchanged_on_refl. +- inv H. apply Mem.unchanged_on_refl. (* mem extends *) - inv H. inv H1. inv H6. +- inv H. inv H1. inv H6. exists v2; exists m1'; intuition. econstructor; eauto. eapply eventval_match_lessdef; eauto. (* mem inject *) - inv H1. inv H3. inv H8. +- inv H0. inv H2. inv H7. exists f; exists v'; exists m1'; intuition. econstructor; eauto. eapply eventval_match_inject; eauto. red; intros; congruence. (* trace length *) - inv H; simpl; omega. +- inv H; simpl; omega. (* receptive *) - assert (t1 = t2). inv H; inv H0; auto. subst t2. +- assert (t1 = t2). inv H; inv H0; auto. subst t2. exists vres1; exists m1; auto. (* determ *) - inv H; inv H0. +- inv H; inv H0. assert (arg = arg0). eapply eventval_match_determ_2; eauto. subst arg0. split. constructor. auto. Qed. +Inductive extcall_debug_sem (ge: Senv.t): + list val -> mem -> trace -> val -> mem -> Prop := + | extcall_debug_sem_intro: forall vargs m, + extcall_debug_sem ge vargs m E0 Vundef m. + +Lemma extcall_debug_ok: + forall targs, + extcall_properties extcall_debug_sem + (mksignature targs None cc_default). +Proof. + intros; constructor; intros. +(* well typed *) +- inv H. simpl. auto. +(* symbols *) +- inv H2. econstructor; eauto. +(* valid blocks *) +- inv H; auto. +(* perms *) +- inv H; auto. +(* readonly *) +- inv H. apply Mem.unchanged_on_refl. +(* mem extends *) +- inv H. + exists Vundef; exists m1'; intuition. + econstructor; eauto. +(* mem injects *) +- inv H0. + exists f; exists Vundef; exists m1'; intuition. + econstructor; eauto. + red; intros; congruence. +(* trace length *) +- inv H; simpl; omega. +(* receptive *) +- inv H; inv H0. exists Vundef, m1; constructor. +(* determ *) +- inv H; inv H0. + split. constructor. auto. +Qed. + (** ** Semantics of external functions. *) (** For functions defined outside the program ([EF_external] and [EF_builtin]), @@ -1445,14 +1357,14 @@ Qed. Parameter external_functions_sem: ident -> signature -> extcall_sem. Axiom external_functions_properties: - forall id sg, extcall_properties (external_functions_sem id sg) sg nil. + forall id sg, extcall_properties (external_functions_sem id sg) sg. (** We treat inline assembly similarly. *) Parameter inline_assembly_sem: ident -> signature -> extcall_sem. Axiom inline_assembly_properties: - forall id sg, extcall_properties (inline_assembly_sem id sg) sg nil. + forall id sg, extcall_properties (inline_assembly_sem id sg) sg. (** ** Combined semantics of external calls *) @@ -1473,33 +1385,31 @@ Definition external_call (ef: external_function): extcall_sem := | EF_builtin name sg => external_functions_sem name sg | EF_vload chunk => volatile_load_sem chunk | EF_vstore chunk => volatile_store_sem chunk - | EF_vload_global chunk id ofs => volatile_load_global_sem chunk id ofs - | EF_vstore_global chunk id ofs => volatile_store_global_sem chunk id ofs | EF_malloc => extcall_malloc_sem | EF_free => extcall_free_sem | 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 | EF_inline_asm txt sg clb => inline_assembly_sem txt sg + | EF_debug kind txt targs => extcall_debug_sem end. Theorem external_call_spec: forall ef, - extcall_properties (external_call ef) (ef_sig ef) (globals_external ef). + extcall_properties (external_call ef) (ef_sig ef). Proof. - intros. unfold external_call, ef_sig, globals_external; destruct ef. + intros. unfold external_call, ef_sig; destruct ef. apply external_functions_properties. apply external_functions_properties. apply volatile_load_ok. apply volatile_store_ok. - apply volatile_load_global_ok. - apply volatile_store_global_ok. apply extcall_malloc_ok. apply extcall_free_ok. apply extcall_memcpy_ok. apply extcall_annot_ok. apply extcall_annot_val_ok. apply inline_assembly_properties. + apply extcall_debug_ok. Qed. Definition external_call_well_typed ef := ec_well_typed (external_call_spec ef). @@ -1563,7 +1473,7 @@ Lemma external_call_mem_inject: /\ inject_separated f f' m1 m1'. Proof. intros. destruct H as (A & B & C). eapply external_call_mem_inject_gen with (ge1 := ge); eauto. -- repeat split; intros. + repeat split; intros. + simpl in H3. exploit A; eauto. intros EQ; rewrite EQ in H; inv H. auto. + simpl in H3. exploit A; eauto. intros EQ; rewrite EQ in H; inv H. auto. + simpl in H3. exists b1; split; eauto. @@ -1572,7 +1482,6 @@ Proof. * exploit B; eauto. intros EQ; rewrite EQ in H; inv H. rewrite V1; auto. * destruct (Genv.find_var_info ge b2) as [gv2|] eqn:V2; auto. exploit C; eauto. intros EQ; subst b2. congruence. -- intros. exists b1; split; auto. apply A with id; auto. Qed. (** Corollaries of [external_call_determ]. *) @@ -1648,8 +1557,7 @@ Lemma decode_longs_inject: Proof. induction tyl; simpl; intros. auto. - destruct a; inv H; auto. inv H1; auto. constructor; auto. apply Val.longofwords_inject; auto. -Qed. + destruct a; inv H; auto. inv H1; auto. constructor; auto. apply Val.longofwords_inject; auto. Qed. Lemma encode_long_lessdef: forall oty v1 v2, Val.lessdef v1 v2 -> Val.lessdef_list (encode_long oty v1) (encode_long oty v2). @@ -1785,9 +1693,9 @@ Proof. split; congruence. Qed. -(** * Evaluation of annotation arguments *) +(** * Evaluation of builtin arguments *) -Section EVAL_ANNOT_ARG. +Section EVAL_BUILTIN_ARG. Variable A: Type. Variable ge: Senv.t. @@ -1795,54 +1703,54 @@ 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, +Inductive eval_builtin_arg: builtin_arg A -> val -> Prop := + | eval_BA: forall x, + eval_builtin_arg (BA x) (e x) + | eval_BA_int: forall n, + eval_builtin_arg (BA_int n) (Vint n) + | eval_BA_long: forall n, + eval_builtin_arg (BA_long n) (Vlong n) + | eval_BA_float: forall n, + eval_builtin_arg (BA_float n) (Vfloat n) + | eval_BA_single: forall n, + eval_builtin_arg (BA_single n) (Vsingle n) + | eval_BA_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, + eval_builtin_arg (BA_loadstack chunk ofs) v + | eval_BA_addrstack: forall ofs, + eval_builtin_arg (BA_addrstack ofs) (Val.add sp (Vint ofs)) + | eval_BA_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). + eval_builtin_arg (BA_loadglobal chunk id ofs) v + | eval_BA_addrglobal: forall id ofs, + eval_builtin_arg (BA_addrglobal id ofs) (Senv.symbol_address ge id ofs) + | eval_BA_longofwords: forall hi lo vhi vlo, + eval_builtin_arg hi vhi -> eval_builtin_arg lo vlo -> + eval_builtin_arg (BA_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. +Definition eval_builtin_args (al: list (builtin_arg A)) (vl: list val) : Prop := + list_forall2 eval_builtin_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. +Lemma eval_builtin_arg_determ: + forall a v, eval_builtin_arg a v -> forall v', eval_builtin_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. +Lemma eval_builtin_args_determ: + forall al vl, eval_builtin_args al vl -> forall vl', eval_builtin_args al vl' -> vl' = vl. Proof. - induction 1; intros v' EV; inv EV; f_equal; eauto using eval_annot_arg_determ. + induction 1; intros v' EV; inv EV; f_equal; eauto using eval_builtin_arg_determ. Qed. -End EVAL_ANNOT_ARG. +End EVAL_BUILTIN_ARG. -Hint Constructors eval_annot_arg: aarg. +Hint Constructors eval_builtin_arg: barg. (** Invariance by change of global environment. *) -Section EVAL_ANNOT_ARG_PRESERVED. +Section EVAL_BUILTIN_ARG_PRESERVED. Variables A F1 V1 F2 V2: Type. Variable ge1: Genv.t F1 V1. @@ -1854,25 +1762,25 @@ 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. +Lemma eval_builtin_arg_preserved: + forall a v, eval_builtin_arg ge1 e sp m a v -> eval_builtin_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. + induction 1; eauto with barg. rewrite <- EQ in H; eauto with barg. rewrite <- EQ; eauto with barg. 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. +Lemma eval_builtin_args_preserved: + forall al vl, eval_builtin_args ge1 e sp m al vl -> eval_builtin_args ge2 e sp m al vl. Proof. - induction 1; constructor; auto; eapply eval_annot_arg_preserved; eauto. + induction 1; constructor; auto; eapply eval_builtin_arg_preserved; eauto. Qed. -End EVAL_ANNOT_ARG_PRESERVED. +End EVAL_BUILTIN_ARG_PRESERVED. (** Compatibility with the "is less defined than" relation. *) -Section EVAL_ANNOT_ARG_LESSDEF. +Section EVAL_BUILTIN_ARG_LESSDEF. Variable A: Type. Variable ge: Senv.t. @@ -1883,35 +1791,35 @@ 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. +Lemma eval_builtin_arg_lessdef: + forall a v1, eval_builtin_arg ge e1 sp m1 a v1 -> + exists v2, eval_builtin_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. +- exists (e2 x); auto with barg. +- econstructor; eauto with barg. +- econstructor; eauto with barg. +- econstructor; eauto with barg. +- econstructor; eauto with barg. +- exploit Mem.loadv_extends; eauto. intros (v' & P & Q). exists v'; eauto with barg. +- econstructor; eauto with barg. +- exploit Mem.loadv_extends; eauto. intros (v' & P & Q). exists v'; eauto with barg. +- econstructor; eauto with barg. +- destruct IHeval_builtin_arg1 as (vhi' & P & Q). + destruct IHeval_builtin_arg2 as (vlo' & R & S). + econstructor; split; eauto with barg. apply Val.longofwords_lessdef; auto. +Qed. + +Lemma eval_builtin_args_lessdef: + forall al vl1, eval_builtin_args ge e1 sp m1 al vl1 -> + exists vl2, eval_builtin_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). +- exploit eval_builtin_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. +End EVAL_BUILTIN_ARG_LESSDEF. -- cgit