From 3a050b22f37f3c79a10a8ebae3d292fa77e91b76 Mon Sep 17 00:00:00 2001 From: xleroy Date: Sun, 23 May 2010 15:26:33 +0000 Subject: More faithful semantics for volatile reads and writes. git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1346 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e --- common/Events.v | 610 +++++++++++++++++++++++++++++++++----------------------- 1 file changed, 363 insertions(+), 247 deletions(-) (limited to 'common/Events.v') diff --git a/common/Events.v b/common/Events.v index a666b40..329f31c 100644 --- a/common/Events.v +++ b/common/Events.v @@ -22,6 +22,7 @@ Require Import Integers. Require Import Floats. Require Import Values. Require Import Memory. +Require Import Globalenvs. (** * Events and traces *) @@ -47,15 +48,12 @@ Require Import Memory. As mentioned above, we do not expose pointer values directly. Pointers relative to a global variable are shown with the name of the variable instead of the block identifier. - Pointers within a dynamically-allocated block are collapsed - to the [EVptr_local] constant. *) Inductive eventval: Type := | EVint: int -> eventval | EVfloat: float -> eventval - | EVptr_global: ident -> int -> eventval - | EVptr_local: eventval. + | EVptr_global: ident -> int -> eventval. Inductive event: Type := | Event_syscall: ident -> list eventval -> eventval -> event @@ -248,105 +246,155 @@ Qed. (** * Relating values and event values *) +Set Implicit Arguments. + Section EVENTVAL. -(** Parameter to translate between global variable names and their block identifiers. *) -Variable symb: ident -> option block. - -(** Translation from a value to an event value. *) - -Inductive eventval_of_val: val -> eventval -> Prop := - | evofv_int: forall i, - eventval_of_val (Vint i) (EVint i) - | evofv_float: forall f, - eventval_of_val (Vfloat f) (EVfloat f) - | evofv_ptr_global: forall id b ofs, - symb id = Some b -> - eventval_of_val (Vptr b ofs) (EVptr_global id ofs) - | evofv_ptr_local: forall b ofs, - (forall id, symb id <> Some b) -> - eventval_of_val (Vptr b ofs) EVptr_local. - -(** Translation from an event value to a value. To preserve determinism, - the translation is undefined if the event value is [EVptr_local]. *) - -Inductive val_of_eventval: eventval -> typ -> val -> Prop := - | voffv_int: forall i, - val_of_eventval (EVint i) Tint (Vint i) - | voffv_float: forall f, - val_of_eventval (EVfloat f) Tfloat (Vfloat f) - | voffv_ptr_global: forall id b ofs, - symb id = Some b -> - val_of_eventval (EVptr_global id ofs) Tint (Vptr b ofs). +(** Global environment used to translate between global variable names and their block identifiers. *) +Variables F V: Type. +Variable ge: Genv.t F V. + +(** Translation between values and event values. *) + +Inductive eventval_match: eventval -> typ -> val -> Prop := + | ev_match_int: forall i, + eventval_match (EVint i) Tint (Vint i) + | ev_match_float: forall f, + eventval_match (EVfloat f) Tfloat (Vfloat f) + | ev_match_ptr: forall id b ofs, + Genv.find_symbol ge id = Some b -> + eventval_match (EVptr_global id ofs) Tint (Vptr b ofs). + +Inductive eventval_list_match: list eventval -> list typ -> list val -> Prop := + | evl_match_nil: + eventval_list_match nil nil nil + | evl_match_cons: + forall ev1 evl ty1 tyl v1 vl, + eventval_match ev1 ty1 v1 -> + eventval_list_match evl tyl vl -> + eventval_list_match (ev1::evl) (ty1::tyl) (v1::vl). (** Some properties of these translation predicates. *) -Lemma val_of_eventval_type: +Lemma eventval_match_type: forall ev ty v, - val_of_eventval ev ty v -> Val.has_type v ty. + eventval_match ev ty v -> Val.has_type v ty. Proof. intros. inv H; constructor. Qed. -Lemma eventval_of_val_lessdef: - forall v1 v2 ev, - eventval_of_val v1 ev -> Val.lessdef v1 v2 -> eventval_of_val v2 ev. +Lemma eventval_list_match_length: + forall evl tyl vl, eventval_list_match evl tyl vl -> List.length vl = List.length tyl. +Proof. + induction 1; simpl; eauto. +Qed. + +Lemma eventval_match_lessdef: + forall ev ty v1 v2, + eventval_match ev ty v1 -> Val.lessdef v1 v2 -> eventval_match ev ty v2. Proof. intros. inv H; inv H0; constructor; auto. Qed. +Lemma eventval_list_match_lessdef: + forall evl tyl vl1, eventval_list_match evl tyl vl1 -> + forall vl2, Val.lessdef_list vl1 vl2 -> eventval_list_match evl tyl vl2. +Proof. + induction 1; intros. inv H; constructor. + inv H1. constructor. eapply eventval_match_lessdef; eauto. eauto. +Qed. + +(** Compatibility with memory injections *) + Variable f: block -> option (block * Z). Definition meminj_preserves_globals : Prop := - (forall id b, symb id = Some b -> f b = Some(b, 0)) - /\ (forall id b1 b2 delta, symb id = Some b2 -> f b1 = Some(b2, delta) -> b2 = b1). + (forall id b, Genv.find_symbol ge id = Some b -> f b = Some(b, 0)) + /\ (forall b gv, Genv.find_var_info ge b = Some gv -> f b = Some(b, 0)) + /\ (forall b1 b2 delta gv, Genv.find_var_info ge b2 = Some gv -> f b1 = Some(b2, delta) -> b2 = b1). -Lemma eventval_of_val_inject: - forall v1 v2 ev, - meminj_preserves_globals -> - eventval_of_val v1 ev -> val_inject f v1 v2 -> eventval_of_val v2 ev. +Hypothesis glob_pres: meminj_preserves_globals. + +Lemma eventval_match_inject: + forall ev ty v1 v2, + eventval_match ev ty v1 -> val_inject f v1 v2 -> eventval_match ev ty v2. Proof. - intros. destruct H. inv H0; inv H1. - constructor. constructor. - exploit H; eauto. intro EQ. rewrite H5 in EQ; inv EQ. - rewrite Int.add_zero. constructor; auto. - constructor. intros; red; intros. - exploit H2; eauto. intro EQ. elim (H3 id). congruence. + intros. inv H; inv H0. constructor. constructor. + destruct glob_pres as [A [B C]]. + exploit A; eauto. intro EQ; rewrite H3 in EQ; inv EQ. + rewrite Int.add_zero. econstructor; eauto. Qed. -Lemma val_of_eventval_inject: +Lemma eventval_match_inject_2: forall ev ty v, - meminj_preserves_globals -> - val_of_eventval ev ty v -> val_inject f v v. + eventval_match ev ty v -> val_inject f v v. Proof. - intros. destruct H. inv H0. - constructor. constructor. - apply val_inject_ptr with 0. eauto. rewrite Int.add_zero; auto. + induction 1. constructor. constructor. + destruct glob_pres as [A [B C]]. + exploit A; eauto. intro EQ. + econstructor; eauto. rewrite Int.add_zero; auto. Qed. -Definition symbols_injective: Prop := - forall id1 id2 b, symb id1 = Some b -> symb id2 = Some b -> id1 = id2. - -Remark eventval_of_val_determ: - forall v ev1 ev2, - symbols_injective -> - eventval_of_val v ev1 -> eventval_of_val v ev2 -> ev1 = ev2. +Lemma eventval_list_match_inject: + forall evl tyl vl1, eventval_list_match evl tyl vl1 -> + forall vl2, val_list_inject f vl1 vl2 -> eventval_list_match evl tyl vl2. Proof. - intros. inv H0; inv H1; auto. - exploit (H id id0); eauto. congruence. - elim (H5 _ H2). - elim (H2 _ H5). + induction 1; intros. inv H; constructor. + inv H1. constructor. eapply eventval_match_inject; eauto. eauto. Qed. -Remark val_of_eventval_determ: - forall ev ty v1 v2, - val_of_eventval ev ty v1 -> val_of_eventval ev ty v2 -> v1 = v2. +(** Determinism *) + +Lemma eventval_match_determ_1: + forall ev ty v1 v2, eventval_match ev ty v1 -> eventval_match ev ty v2 -> v1 = v2. Proof. intros. inv H; inv H0; auto. congruence. Qed. +Lemma eventval_match_determ_2: + forall ev1 ev2 ty v, eventval_match ev1 ty v -> eventval_match ev2 ty v -> ev1 = ev2. +Proof. + intros. inv H; inv H0; auto. + decEq. eapply Genv.genv_vars_inj; eauto. +Qed. + +Lemma eventval_list_match_determ_2: + forall evl1 tyl vl, eventval_list_match evl1 tyl vl -> + forall evl2, eventval_list_match evl2 tyl vl -> evl1 = evl2. +Proof. + induction 1; intros. inv H. auto. inv H1. f_equal; eauto. + eapply eventval_match_determ_2; eauto. +Qed. + End EVENTVAL. +(** Invariance under changes to the global environment *) + +Section EVENTVAL_INV. + +Variables F1 V1 F2 V2: Type. +Variable ge1: Genv.t F1 V1. +Variable ge2: Genv.t F2 V2. + +Hypothesis symbols_preserved: + forall id, Genv.find_symbol ge2 id = Genv.find_symbol ge1 id. + +Lemma eventval_match_preserved: + forall ev ty v, + eventval_match ge1 ev ty v -> eventval_match ge2 ev ty v. +Proof. + induction 1; constructor. rewrite symbols_preserved; auto. +Qed. + +Lemma eventval_list_match_preserved: + forall evl tyl vl, + eventval_list_match ge1 evl tyl vl -> eventval_list_match ge2 evl tyl vl. +Proof. + induction 1; constructor; auto. eapply eventval_match_preserved; eauto. +Qed. + +End EVENTVAL_INV. + (** * Semantics of external functions *) (** Each external function is of one of the following kinds: *) @@ -357,19 +405,14 @@ Inductive extfun_kind: signature -> Type := result that is an integer or a float, 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. Reads and returns the given memory - chunk from the address given as first argument. Since this is - a volatile access, the contents of this address may have changed - asynchronously since the last write we did at this address. - To account for this fact, we first update the given address - with a value that is provided by the outside world through - the trace of events. - Produces an [Event_load] event. *) + (** 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. Store the value given as second - argument at the address given as first argument, using the - given memory chunk. - Produces an [Event_store] event. *) + (** 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. @@ -384,7 +427,7 @@ 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 mapping from global variables to blocks +- the global environment - the values of the arguments passed to this function - the memory state before the call - the result value of the call @@ -393,7 +436,7 @@ Parameter classify_external_function: *) Definition extcall_sem : Type := - (ident -> option block) -> list val -> mem -> trace -> val -> mem -> Prop. + forall (F V: Type), Genv.t F V -> list val -> mem -> trace -> val -> mem -> Prop. (** We now specify the expected properties of this predicate. *) @@ -433,43 +476,57 @@ Fixpoint matching_traces (t1 t2: trace) {struct t1} : Prop := True end. +Definition block_is_volatile (F V: Type) (ge: Genv.t F V) (b: block) : bool := + match Genv.find_var_info ge b with + | None => false + | Some gv => gv.(gvar_volatile) + end. + Record extcall_properties (sem: extcall_sem) (sg: signature) : Prop := mk_extcall_properties { (** The return value of an external call must agree with its signature. *) ec_well_typed: - forall symb vargs m1 t vres m2, - sem symb vargs m1 t vres m2 -> + forall F V (ge: Genv.t F V) vargs m1 t vres m2, + sem F V ge vargs m1 t vres m2 -> Val.has_type vres (proj_sig_res sg); (** The number of arguments of an external call must agree with its signature. *) ec_arity: - forall symb vargs m1 t vres m2, - sem symb vargs m1 t vres m2 -> + forall F V (ge: Genv.t F V) vargs m1 t vres m2, + sem F V ge vargs m1 t vres m2 -> List.length vargs = List.length sg.(sig_args); +(** The semantics is invariant under change of global environment that preserves symbols. *) + ec_symbols_preserved: + forall F1 V1 (ge1: Genv.t F1 V1) F2 V2 (ge2: Genv.t F2 V2) vargs m1 t vres m2, + (forall id, Genv.find_symbol ge2 id = Genv.find_symbol ge1 id) -> + (forall b, block_is_volatile ge2 b = block_is_volatile ge1 b) -> + sem F1 V1 ge1 vargs m1 t vres m2 -> + sem F2 V2 ge2 vargs m1 t vres m2; + (** External calls cannot invalidate memory blocks. (Remember that freeing a block does not invalidate its block identifier.) *) ec_valid_block: - forall symb vargs m1 t vres m2 b, - sem symb vargs m1 t vres m2 -> + forall F V (ge: Genv.t F V) vargs m1 t vres m2 b, + sem F V ge vargs m1 t vres m2 -> Mem.valid_block m1 b -> Mem.valid_block m2 b; (** External calls preserve the bounds of valid blocks. *) ec_bounds: - forall symb vargs m1 t vres m2 b, - sem symb vargs m1 t vres m2 -> + forall F V (ge: Genv.t F V) vargs m1 t vres m2 b, + sem F V ge vargs m1 t vres m2 -> Mem.valid_block m1 b -> Mem.bounds m2 b = Mem.bounds m1 b; (** External calls must commute with memory extensions, in the following sense. *) ec_mem_extends: - forall symb vargs m1 t vres m2 m1' vargs', - sem symb vargs m1 t vres m2 -> + forall F V (ge: Genv.t F V) vargs m1 t vres m2 m1' vargs', + sem F V ge vargs m1 t vres m2 -> Mem.extends m1 m1' -> Val.lessdef_list vargs vargs' -> exists vres', exists m2', - sem symb vargs' m1' t vres' m2' + sem F V ge vargs' m1' t vres' m2' /\ Val.lessdef vres vres' /\ Mem.extends m2 m2' /\ mem_unchanged_on (loc_out_of_bounds m1) m1' m2'; @@ -477,13 +534,13 @@ Record extcall_properties (sem: extcall_sem) (** External calls must commute with memory injections, in the following sense. *) ec_mem_inject: - forall symb vargs m1 t vres m2 f m1' vargs', - meminj_preserves_globals symb f -> - sem symb vargs m1 t vres m2 -> + forall F V (ge: Genv.t F V) vargs m1 t vres m2 f m1' vargs', + meminj_preserves_globals ge f -> + sem F V ge vargs m1 t vres m2 -> Mem.inject f m1 m1' -> val_list_inject f vargs vargs' -> exists f', exists vres', exists m2', - sem symb vargs' m1' t vres' m2' + sem F V ge vargs' m1' t vres' m2' /\ val_inject f' vres vres' /\ Mem.inject f' m2 m2' /\ mem_unchanged_on (loc_unmapped f) m1 m2 @@ -495,24 +552,43 @@ Record extcall_properties (sem: extcall_sem) if the observable traces match, the return states must be identical. *) ec_determ: - forall symb vargs m t1 vres1 m1 t2 vres2 m2, - symbols_injective symb -> - sem symb vargs m t1 vres1 m1 -> sem symb vargs m t2 vres2 m2 -> + forall F V ge vargs m t1 vres1 m1 t2 vres2 m2, + sem F V ge vargs m t1 vres1 m1 -> sem F V ge vargs m t2 vres2 m2 -> matching_traces t1 t2 -> t1 = t2 /\ vres1 = vres2 /\ m1 = m2 }. (** ** Semantics of volatile loads *) -Inductive volatile_load_sem (chunk: memory_chunk): extcall_sem := - | volatile_load_sem_intro: forall symb b ofs m id ev v m' res, - symb id = Some b -> - val_of_eventval symb ev (type_of_chunk chunk) v -> - Mem.store chunk m b (Int.signed ofs) v = Some m' -> - Mem.load chunk m' b (Int.signed ofs) = Some res -> - volatile_load_sem chunk symb - (Vptr b ofs :: nil) m - (Event_vload chunk id ofs ev :: nil) - res m'. +Inductive volatile_load_sem (chunk: memory_chunk) (F V: Type) (ge: Genv.t F V): + list val -> mem -> trace -> val -> mem -> Prop := + | volatile_load_sem_vol: forall b ofs m id ev v, + Genv.find_symbol ge id = Some b -> block_is_volatile ge b = true -> + eventval_match ge ev (type_of_chunk chunk) v -> + volatile_load_sem chunk ge + (Vptr b ofs :: nil) m + (Event_vload chunk id ofs ev :: nil) + (Val.load_result chunk v) m + | volatile_load_sem_nonvol: forall b ofs m v, + block_is_volatile ge b = false -> + Mem.load chunk m b (Int.signed ofs) = Some v -> + volatile_load_sem chunk ge + (Vptr b ofs :: nil) m + E0 + v m. + +Remark meminj_preserves_block_is_volatile: + forall F V (ge: Genv.t F V) f b1 b2 delta, + meminj_preserves_globals ge f -> + f b1 = Some (b2, delta) -> + block_is_volatile ge b2 = block_is_volatile ge b1. +Proof. + intros. destruct H as [A [B C]]. unfold block_is_volatile. + case_eq (Genv.find_var_info ge b1); intros. + exploit B; eauto. intro EQ; rewrite H0 in EQ; inv EQ. rewrite H; auto. + case_eq (Genv.find_var_info ge b2); intros. + exploit C; eauto. intro EQ. congruence. + auto. +Qed. Lemma volatile_load_ok: forall chunk, @@ -521,81 +597,77 @@ Lemma volatile_load_ok: Proof. intros; constructor; intros. - inv H. unfold proj_sig_res. simpl. eapply Mem.load_type; eauto. + unfold proj_sig_res; simpl. destruct H. + destruct chunk; destruct v; simpl; constructor. + eapply Mem.load_type; eauto. - inv H. simpl. auto. + destruct H; simpl; auto. - inv H. eauto with mem. + destruct H1. + econstructor; eauto. rewrite H; auto. eapply eventval_match_preserved; eauto. + econstructor; eauto. - inv H. eapply Mem.bounds_store; eauto. + destruct H; auto. - inv H. inv H1. inv H7. inv H9. - exploit Mem.store_within_extends; eauto. intros [m2' [A B]]. - exploit Mem.load_extends; eauto. intros [vres' [C D]]. - exists vres'; exists m2'. - split. econstructor; eauto. - split. auto. - split. auto. - red; split; intros. - eapply Mem.perm_store_1; eauto. - rewrite <- H1. eapply Mem.load_store_other; eauto. - destruct (eq_block b0 b); auto. subst b0; right. - exploit Mem.valid_access_in_bounds. - eapply Mem.store_valid_access_3. eexact H4. - intros [P Q]. - generalize (size_chunk_pos chunk0). intro E. - generalize (size_chunk_pos chunk). intro F. - apply (Intv.range_disjoint' (ofs0, ofs0 + size_chunk chunk0) - (Int.signed ofs, Int.signed ofs + size_chunk chunk)). - red; intros. generalize (H x H6). unfold loc_out_of_bounds, Intv.In; simpl. omega. - simpl; omega. simpl; omega. + destruct H; auto. - inv H0. inv H2. inv H8. inv H10. - exploit val_of_eventval_inject; eauto. intro INJ. - exploit Mem.store_mapped_inject; eauto. intros [m2' [A B]]. - exploit Mem.load_inject; eauto. intros [vres' [C D]]. - exists f; exists vres'; exists m2'; intuition. - destruct H as [P Q]. - rewrite (P _ _ H3) in H7. inv H7. rewrite Int.add_zero. + destruct H. + inv H1. inv H8. inv H6. + exists (Val.load_result chunk v); exists m1'; intuition. + constructor; auto. + red; auto. + inv H1. inv H7. inv H5. + exploit Mem.load_extends; eauto. intros [v' [A B]]. + exists v'; exists m1'; intuition. econstructor; eauto. - replace (Int.signed ofs) with (Int.signed ofs + 0) by omega; auto. - replace (Int.signed ofs) with (Int.signed ofs + 0) by omega; auto. - split; intros. eapply Mem.perm_store_1; eauto. - rewrite <- H2. eapply Mem.load_store_other; eauto. - left. exploit (H0 ofs0). generalize (size_chunk_pos chunk0). omega. - unfold loc_unmapped. congruence. - split; intros. eapply Mem.perm_store_1; eauto. - rewrite <- H2. eapply Mem.load_store_other; eauto. - destruct (eq_block b0 b2); auto. subst b0; right. - exploit Mem.valid_access_in_bounds. - eapply Mem.store_valid_access_3. eexact H5. - intros [P Q]. - generalize (size_chunk_pos chunk0). intro E. - generalize (size_chunk_pos chunk). intro F. - apply (Intv.range_disjoint' (ofs0, ofs0 + size_chunk chunk0) - (Int.signed ofs + delta, Int.signed ofs + delta + size_chunk chunk)). - red; intros. exploit (H0 x H8). eauto. unfold Intv.In; simpl. omega. - simpl; omega. simpl; omega. + red; auto. + + destruct H0. + inv H2. inv H9. inv H7. + generalize H; intros [P [Q R]]. + exploit P; eauto. intro EQ; rewrite H6 in EQ; inv EQ. + exists f; exists (Val.load_result chunk v); exists m1'; intuition. + rewrite Int.add_zero. constructor; auto. + apply val_load_result_inject. eapply eventval_match_inject_2; eauto. + red; auto. + red; auto. + red; intros. congruence. + inv H2. inv H8. + exploit Mem.loadv_inject; eauto. simpl. eauto. intros [v1 [A B]]. + inv H6; simpl in *. + exists f; exists v1; exists m1'; intuition. + econstructor; eauto. + rewrite <- H0. eapply meminj_preserves_block_is_volatile; eauto. + red; auto. + red; auto. red; intros. congruence. - inv H0. inv H1. simpl in H2. - assert (id = id0) by (eapply H; eauto). subst id0. - assert (ev = ev0) by intuition. subst ev0. - exploit val_of_eventval_determ. eexact H4. eexact H9. intro. + inv H; inv H0; try congruence. + assert (id = id0) by (eapply Genv.genv_vars_inj; eauto). subst id0. + assert (ev = ev0) by (red in H1; tauto). subst ev0. + assert (v = v0) by (eapply eventval_match_determ_1; eauto). subst v0. + auto. intuition congruence. Qed. (** ** Semantics of volatile stores *) -Inductive volatile_store_sem (chunk: memory_chunk): extcall_sem := - | volatile_store_sem_intro: forall symb b ofs v id ev m m', - symb id = Some b -> - eventval_of_val symb v ev -> +Inductive volatile_store_sem (chunk: memory_chunk) (F V: Type) (ge: Genv.t F V): + list val -> mem -> trace -> val -> mem -> Prop := + | volatile_store_sem_vol: forall b ofs m id ev v, + Genv.find_symbol ge id = Some b -> block_is_volatile ge b = true -> + eventval_match ge ev (type_of_chunk chunk) v -> + volatile_store_sem chunk ge + (Vptr b ofs :: v :: nil) m + (Event_vstore chunk id ofs ev :: nil) + Vundef m + | volatile_store_sem_nonvol: forall b ofs m v m', + block_is_volatile ge b = false -> Mem.store chunk m b (Int.signed ofs) v = Some m' -> - volatile_store_sem chunk symb - (Vptr b ofs :: v :: nil) m - (Event_vstore chunk id ofs ev :: nil) - Vundef m'. + volatile_store_sem chunk ge + (Vptr b ofs :: v :: nil) m + E0 + Vundef m'. Lemma volatile_store_ok: forall chunk, @@ -604,71 +676,93 @@ Lemma volatile_store_ok: Proof. intros; constructor; intros. - inv H. unfold proj_sig_res. simpl. auto. + unfold proj_sig_res; simpl. inv H; constructor. + + inv H; simpl; auto. - inv H. simpl. auto. + inv H1. + constructor. rewrite H; auto. rewrite H0; auto. eapply eventval_match_preserved; eauto. + constructor; auto. rewrite H0; auto. - inv H. eauto with mem. + inv H. auto. eauto with mem. - inv H. eapply Mem.bounds_store; eauto. + inv H. auto. eapply Mem.bounds_store; eauto. - inv H. inv H1. inv H6. inv H8. inv H7. + inv H. + inv H1. inv H6. inv H8. inv H7. + exists Vundef; exists m1'; intuition. + constructor; auto. eapply eventval_match_lessdef; eauto. + red; auto. + inv H1. inv H5. inv H7. inv H6. exploit Mem.store_within_extends; eauto. intros [m' [A B]]. exists Vundef; exists m'; intuition. - constructor; auto. eapply eventval_of_val_lessdef; eauto. + constructor; auto. red; split; intros. eapply Mem.perm_store_1; eauto. rewrite <- H1. eapply Mem.load_store_other; eauto. destruct (eq_block b0 b); auto. subst b0; right. exploit Mem.valid_access_in_bounds. - eapply Mem.store_valid_access_3. eexact H4. + eapply Mem.store_valid_access_3. eexact H3. intros [C D]. generalize (size_chunk_pos chunk0). intro E. - generalize (size_chunk_pos chunk). intro F. + generalize (size_chunk_pos chunk). intro G. apply (Intv.range_disjoint' (ofs0, ofs0 + size_chunk chunk0) (Int.signed ofs, Int.signed ofs + size_chunk chunk)). - red; intros. generalize (H x H6). unfold loc_out_of_bounds, Intv.In; simpl. omega. + red; intros. generalize (H x H5). unfold loc_out_of_bounds, Intv.In; simpl. omega. simpl; omega. simpl; omega. - inv H0. inv H2. inv H7. inv H9. inv H10. - exploit Mem.store_mapped_inject; eauto. intros [m2' [A B]]. + inv H0. + inv H2. inv H7. inv H9. inv H10. + generalize H; intros [P [Q R]]. + exploit P; eauto. intro EQ; rewrite H6 in EQ; inv EQ. + exists f; exists Vundef; exists m1'; intuition. + rewrite Int.add_zero. constructor; auto. + eapply eventval_match_inject; eauto. + red; auto. + red; auto. + red; intros; congruence. + inv H2. inv H8. inv H9. inv H6. + assert (Mem.storev chunk m1 (Vptr b ofs) v = Some m2). simpl; auto. + exploit Mem.storev_mapped_inject; eauto. intros [m2' [A B]]. + inv H4. exists f; exists Vundef; exists m2'; intuition. - elim H; intros P Q. - rewrite (P _ _ H3) in H6. inv H6. rewrite Int.add_zero. econstructor; eauto. - eapply eventval_of_val_inject; eauto. - replace (Int.signed ofs) with (Int.signed ofs + 0) by omega; auto. + constructor; auto. rewrite <- H3. eapply meminj_preserves_block_is_volatile; eauto. split; intros. eapply Mem.perm_store_1; eauto. - rewrite <- H2. eapply Mem.load_store_other; eauto. - left. exploit (H0 ofs0). generalize (size_chunk_pos chunk0). omega. + rewrite <- H4. eapply Mem.load_store_other; eauto. + left. exploit (H2 ofs0). generalize (size_chunk_pos chunk0). omega. unfold loc_unmapped. congruence. split; intros. eapply Mem.perm_store_1; eauto. - rewrite <- H2. eapply Mem.load_store_other; eauto. + rewrite <- H4. eapply Mem.load_store_other; eauto. destruct (eq_block b0 b2); auto. subst b0; right. + assert (EQ: Int.signed (Int.add ofs (Int.repr delta)) = Int.signed ofs + delta). + eapply Mem.address_inject; eauto with mem. + simpl in A. rewrite EQ in A. rewrite EQ. exploit Mem.valid_access_in_bounds. - eapply Mem.store_valid_access_3. eexact H5. + eapply Mem.store_valid_access_3. eexact H0. intros [C D]. generalize (size_chunk_pos chunk0). intro E. - generalize (size_chunk_pos chunk). intro F. + generalize (size_chunk_pos chunk). intro G. apply (Intv.range_disjoint' (ofs0, ofs0 + size_chunk chunk0) (Int.signed ofs + delta, Int.signed ofs + delta + size_chunk chunk)). - red; intros. exploit (H0 x H8). eauto. unfold Intv.In; simpl. omega. + red; intros. exploit (H2 x H8). eauto. unfold Intv.In; simpl. omega. simpl; omega. simpl; omega. + red; intros; congruence. - red; intros. congruence. - - inv H0; inv H1. - assert (id = id0) by (eapply H; eauto). - exploit eventval_of_val_determ. eauto. eexact H4. eexact H14. intros. + inv H; inv H0; try congruence. + assert (id = id0) by (eapply Genv.genv_vars_inj; eauto). subst id0. + assert (ev = ev0) by (eapply eventval_match_determ_2; eauto). subst ev0. + auto. intuition congruence. Qed. (** ** Semantics of dynamic memory allocation (malloc) *) -Inductive extcall_malloc_sem: extcall_sem := - | extcall_malloc_sem_intro: forall symb n m m' b m'', +Inductive extcall_malloc_sem (F V: Type) (ge: Genv.t F V): + list val -> mem -> trace -> val -> mem -> Prop := + | extcall_malloc_sem_intro: forall n m m' b m'', Mem.alloc m (-4) (Int.signed n) = (m', b) -> Mem.store Mint32 m' b (-4) (Vint n) = Some m'' -> - extcall_malloc_sem symb (Vint n :: nil) m E0 (Vptr b Int.zero) m''. + extcall_malloc_sem ge (Vint n :: nil) m E0 (Vptr b Int.zero) m''. Lemma extcall_malloc_ok: extcall_properties extcall_malloc_sem @@ -692,6 +786,8 @@ Proof. inv H. auto. + inv H1; econstructor; eauto. + inv H. eauto with mem. inv H. transitivity (Mem.bounds m' b). @@ -714,7 +810,7 @@ Proof. intros [f' [m3' [b' [ALLOC [A [B [C D]]]]]]]. exploit Mem.store_mapped_inject. eexact A. eauto. eauto. instantiate (1 := Vint n). auto. - intros [m2' [E F]]. + intros [m2' [E G]]. exists f'; exists (Vptr b' Int.zero); exists m2'; intuition. econstructor; eauto. econstructor. eauto. auto. @@ -724,17 +820,18 @@ Proof. subst b1. rewrite C in H2. inv H2. eauto with mem. rewrite D in H2. congruence. auto. - inv H0; inv H1. intuition congruence. + inv H; inv H0. intuition congruence. Qed. (** ** Semantics of dynamic memory deallocation (free) *) -Inductive extcall_free_sem: extcall_sem := - | extcall_free_sem_intro: forall symb b lo sz m m', +Inductive extcall_free_sem (F V: Type) (ge: Genv.t F V): + list val -> mem -> trace -> val -> mem -> Prop := + | extcall_free_sem_intro: forall b lo sz m m', Mem.load Mint32 m b (Int.signed lo - 4) = Some (Vint sz) -> Int.signed sz > 0 -> Mem.free m b (Int.signed lo - 4) (Int.signed lo + Int.signed sz) = Some m' -> - extcall_free_sem symb (Vptr b lo :: nil) m E0 Vundef m'. + extcall_free_sem ge (Vptr b lo :: nil) m E0 Vundef m'. Lemma extcall_free_ok: extcall_properties extcall_free_sem @@ -761,6 +858,8 @@ Proof. inv H. auto. + inv H1; econstructor; eauto. + inv H. eauto with mem. inv H. eapply Mem.bounds_free; eauto. @@ -820,17 +919,17 @@ Proof. red; intros. congruence. - inv H0; inv H1. intuition congruence. + inv H; inv H0. intuition congruence. Qed. (** ** Semantics of system calls. *) -Inductive extcall_io_sem (name: ident) (sg: signature): extcall_sem := - | extcall_io_sem_intro: forall symb vargs m args res vres, - length vargs = length (sig_args sg) -> - list_forall2 (eventval_of_val symb) vargs args -> - val_of_eventval symb res (proj_sig_res sg) vres -> - extcall_io_sem name sg symb vargs m (Event_syscall name args res :: E0) vres m. +Inductive extcall_io_sem (name: ident) (sg: signature) (F V: Type) (ge: Genv.t F V): + list val -> mem -> trace -> val -> mem -> Prop := + | extcall_io_sem_intro: forall vargs m args res vres, + eventval_list_match ge args (sig_args sg) vargs -> + eventval_match ge res (proj_sig_res sg) vres -> + extcall_io_sem name sg ge vargs m (Event_syscall name args res :: E0) vres m. Lemma extcall_io_ok: forall name sg, @@ -838,9 +937,13 @@ Lemma extcall_io_ok: Proof. intros; constructor; intros. - inv H. eapply val_of_eventval_type; eauto. + inv H. eapply eventval_match_type; eauto. - inv H. auto. + inv H. eapply eventval_list_match_length; eauto. + + inv H1. econstructor; eauto. + eapply eventval_list_match_preserved; eauto. + eapply eventval_match_preserved; eauto. inv H; auto. @@ -849,33 +952,22 @@ Proof. inv H. exists vres; exists m1'; intuition. econstructor; eauto. - rewrite <- H2. - generalize vargs vargs' H1. induction 1; simpl; congruence. - generalize vargs vargs' H1 args H3. induction 1; intros. - inv H5. constructor. - inv H6. constructor; eauto. eapply eventval_of_val_lessdef; eauto. + eapply eventval_list_match_lessdef; eauto. red; auto. inv H0. exists f; exists vres; exists m1'; intuition. econstructor; eauto. - rewrite <- H3. - generalize vargs vargs' H2. induction 1; simpl; congruence. - generalize vargs vargs' H2 args H4. induction 1; intros. - inv H0. constructor. - inv H7. constructor; eauto. eapply eventval_of_val_inject; eauto. - eapply val_of_eventval_inject; eauto. + eapply eventval_list_match_inject; eauto. + eapply eventval_match_inject_2; eauto. red; auto. red; auto. red; intros; congruence. - inv H0; inv H1. simpl in H2. - assert (args = args0). - generalize vargs args H4 args0 H6. induction 1; intros. - inv H1; auto. - inv H9. decEq; eauto. eapply eventval_of_val_determ; eauto. - destruct H2; auto. subst. - intuition. eapply val_of_eventval_determ; eauto. + inv H; inv H0. simpl in H1. + assert (args = args0). eapply eventval_list_match_determ_2; eauto. subst args0. + assert (res = res0). tauto. subst res0. + intuition. eapply eventval_match_determ_1; eauto. Qed. (** ** Combined semantics of external calls *) @@ -912,22 +1004,46 @@ Proof. apply extcall_free_ok. Qed. -Definition external_call_well_typed ef := ec_well_typed _ _ (external_call_spec ef). -Definition external_call_arity ef := ec_arity _ _ (external_call_spec ef). -Definition external_call_valid_block ef := ec_valid_block _ _ (external_call_spec ef). -Definition external_call_bounds ef := ec_bounds _ _ (external_call_spec ef). -Definition external_call_mem_extends ef := ec_mem_extends _ _ (external_call_spec ef). -Definition external_call_mem_inject ef := ec_mem_inject _ _ (external_call_spec ef). -Definition external_call_determ ef := ec_determ _ _ (external_call_spec ef). +Definition external_call_well_typed ef := ec_well_typed (external_call_spec ef). +Definition external_call_arity ef := ec_arity (external_call_spec ef). +Definition external_call_symbols_preserved_gen ef := ec_symbols_preserved (external_call_spec ef). +Definition external_call_valid_block ef := ec_valid_block (external_call_spec ef). +Definition external_call_bounds ef := ec_bounds (external_call_spec ef). +Definition external_call_mem_extends ef := ec_mem_extends (external_call_spec ef). +Definition external_call_mem_inject ef := ec_mem_inject (external_call_spec ef). +Definition external_call_determ ef := ec_determ (external_call_spec ef). -(** The only dependency on the global environment is on the addresses of symbols. *) +(** Special cases of [external_call_symbols_preserved_gen]. *) Lemma external_call_symbols_preserved: - forall ef symb1 symb2 vargs m1 t vres m2, - external_call ef symb1 vargs m1 t vres m2 -> - (forall id, symb2 id = symb1 id) -> - external_call ef symb2 vargs m1 t vres m2. + forall ef F1 F2 V (ge1: Genv.t F1 V) (ge2: Genv.t F2 V) vargs m1 t vres m2, + external_call ef ge1 vargs m1 t vres m2 -> + (forall id, Genv.find_symbol ge2 id = Genv.find_symbol ge1 id) -> + (forall b, Genv.find_var_info ge2 b = Genv.find_var_info ge1 b) -> + external_call ef ge2 vargs m1 t vres m2. +Proof. + intros. eapply external_call_symbols_preserved_gen; eauto. + intros. unfold block_is_volatile. rewrite H1. auto. +Qed. + +Require Import Errors. + +Lemma external_call_symbols_preserved_2: + forall ef F1 V1 F2 V2 (tvar: V1 -> res V2) + (ge1: Genv.t F1 V1) (ge2: Genv.t F2 V2) vargs m1 t vres m2, + external_call ef ge1 vargs m1 t vres m2 -> + (forall id, Genv.find_symbol ge2 id = Genv.find_symbol ge1 id) -> + (forall b gv1, Genv.find_var_info ge1 b = Some gv1 -> + exists gv2, Genv.find_var_info ge2 b = Some gv2 /\ transf_globvar tvar gv1 = OK gv2) -> + (forall b gv2, Genv.find_var_info ge2 b = Some gv2 -> + exists gv1, Genv.find_var_info ge1 b = Some gv1 /\ transf_globvar tvar gv1 = OK gv2) -> + external_call ef ge2 vargs m1 t vres m2. Proof. - intros. replace symb2 with symb1; auto. - symmetry. apply extensionality. auto. + intros. eapply external_call_symbols_preserved_gen; eauto. + intros. unfold block_is_volatile. + case_eq (Genv.find_var_info ge1 b); intros. + exploit H1; eauto. intros [g2 [A B]]. rewrite A. monadInv B. destruct g; auto. + case_eq (Genv.find_var_info ge2 b); intros. + exploit H2; eauto. intros [g1 [A B]]. congruence. + auto. Qed. -- cgit v1.2.3