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/AST.v | 69 +++--- common/Events.v | 610 +++++++++++++++++++++++++++++++--------------------- common/Globalenvs.v | 193 ++++++++++------- common/Values.v | 8 + 4 files changed, 522 insertions(+), 358 deletions(-) (limited to 'common') diff --git a/common/AST.v b/common/AST.v index 2d20276..861795c 100644 --- a/common/AST.v +++ b/common/AST.v @@ -93,11 +93,19 @@ Inductive init_data: Type := | Init_space: Z -> init_data | Init_addrof: ident -> int -> init_data. (**r address of symbol + offset *) +(** Information attached to global variables. *) + +Record globvar (V: Type) : Type := mkglobvar { + gvar_info: V; (**r language-dependent info, e.g. a type *) + gvar_init: list init_data; (**r initialization data *) + gvar_readonly: bool; (**r read-only variable? (const) *) + gvar_volatile: bool (**r volatile variable? *) +}. + (** Whole programs consist of: - a collection of function definitions (name and description); - the name of the ``main'' function that serves as entry point in the program; -- a collection of global variable declarations, consisting of - a name, initialization data, and additional information. +- a collection of global variable declarations (name and information). The type of function descriptions and that of additional information for variables vary among the various intermediate languages and are @@ -107,14 +115,14 @@ programs are common to all languages. *) Record program (F V: Type) : Type := mkprogram { prog_funct: list (ident * F); prog_main: ident; - prog_vars: list (ident * list init_data * V) + prog_vars: list (ident * globvar V) }. Definition prog_funct_names (F V: Type) (p: program F V) : list ident := map (@fst ident F) p.(prog_funct). Definition prog_var_names (F V: Type) (p: program F V) : list ident := - map (fun x: ident * list init_data * V => fst(fst x)) p.(prog_vars). + map (@fst ident (globvar V)) p.(prog_vars). (** * Generic transformations over programs *) @@ -230,11 +238,11 @@ Section TRANSF_PARTIAL_PROGRAM. Variable A B V: Type. Variable transf_partial: A -> res B. -Definition prefix_funct_name (id: ident) : errmsg := +Definition prefix_name (id: ident) : errmsg := MSG "In function " :: CTX id :: MSG ": " :: nil. Definition transform_partial_program (p: program A V) : res (program B V) := - do fl <- map_partial prefix_funct_name transf_partial p.(prog_funct); + do fl <- map_partial prefix_name transf_partial p.(prog_funct); OK (mkprogram fl p.(prog_main) p.(prog_vars)). Lemma transform_partial_program_function: @@ -275,12 +283,13 @@ Variable A B V W: Type. Variable transf_partial_function: A -> res B. Variable transf_partial_variable: V -> res W. -Definition prefix_var_name (id_init: ident * list init_data) : errmsg := - MSG "In global variable " :: CTX (fst id_init) :: MSG ": " :: nil. +Definition transf_globvar (g: globvar V) : res (globvar W) := + do info' <- transf_partial_variable g.(gvar_info); + OK (mkglobvar info' g.(gvar_init) g.(gvar_readonly) g.(gvar_volatile)). Definition transform_partial_program2 (p: program A V) : res (program B W) := - do fl <- map_partial prefix_funct_name transf_partial_function p.(prog_funct); - do vl <- map_partial prefix_var_name transf_partial_variable p.(prog_vars); + do fl <- map_partial prefix_name transf_partial_function p.(prog_funct); + do vl <- map_partial prefix_name transf_globvar p.(prog_vars); OK (mkprogram fl p.(prog_main) vl). Lemma transform_partial_program2_function: @@ -294,14 +303,16 @@ Proof. Qed. Lemma transform_partial_program2_variable: - forall p tp i tv, + forall p tp i tg, transform_partial_program2 p = OK tp -> - In (i, tv) tp.(prog_vars) -> - exists v, In (i, v) p.(prog_vars) /\ transf_partial_variable v = OK tv. + In (i, tg) tp.(prog_vars) -> + exists v, + In (i, mkglobvar v tg.(gvar_init) tg.(gvar_readonly) tg.(gvar_volatile)) p.(prog_vars) + /\ transf_partial_variable v = OK tg.(gvar_info). Proof. - intros. monadInv H. - eapply In_map_partial; eauto. -Qed. + intros. monadInv H. exploit In_map_partial; eauto. intros [g [P Q]]. + monadInv Q. simpl in *. exists (gvar_info g); split. destruct g; auto. auto. + Qed. Lemma transform_partial_program2_main: forall p tp, @@ -326,15 +337,16 @@ Variable A B V W: Type. Variable match_fundef: A -> B -> Prop. Variable match_varinfo: V -> W -> Prop. -Definition match_funct_entry (x1: ident * A) (x2: ident * B) := - match x1, x2 with - | (id1, fn1), (id2, fn2) => id1 = id2 /\ match_fundef fn1 fn2 - end. +Inductive match_funct_entry: ident * A -> ident * B -> Prop := + | match_funct_entry_intro: forall id fn1 fn2, + match_fundef fn1 fn2 -> + match_funct_entry (id, fn1) (id, fn2). -Definition match_var_entry (x1: ident * list init_data * V) (x2: ident * list init_data * W) := - match x1, x2 with - | (id1, init1, info1), (id2, init2, info2) => id1 = id2 /\ init1 = init2 /\ match_varinfo info1 info2 - end. +Inductive match_var_entry: ident * globvar V -> ident * globvar W -> Prop := + | match_var_entry_intro: forall id info1 info2 init ro vo, + match_varinfo info1 info2 -> + match_var_entry (id, mkglobvar info1 init ro vo) + (id, mkglobvar info2 init ro vo). Definition match_program (p1: program A V) (p2: program B W) : Prop := list_forall2 match_funct_entry p1.(prog_funct) p2.(prog_funct) @@ -359,13 +371,14 @@ Proof. (fun (ab: ident * A) (ac: ident * B) => fst ab = fst ac /\ transf_partial_function (snd ab) = OK (snd ac)). eapply map_partial_forall2. eauto. - intros. destruct v1; destruct v2; simpl in *. auto. + intros. destruct v1; destruct v2; simpl in *. destruct H1; subst. constructor. auto. split. auto. apply list_forall2_imply with - (fun (ab: ident * list init_data * V) (ac: ident * list init_data * W) => - fst ab = fst ac /\ transf_partial_variable (snd ab) = OK (snd ac)). + (fun (ab: ident * globvar V) (ac: ident * globvar W) => + fst ab = fst ac /\ transf_globvar transf_partial_variable (snd ab) = OK (snd ac)). eapply map_partial_forall2. eauto. - intros. destruct v1; destruct v2; simpl in *. destruct p0; destruct p1. intuition congruence. + intros. destruct v1; destruct v2; simpl in *. destruct H1; subst. + monadInv H2. destruct g; simpl in *. constructor. auto. Qed. (** * External functions *) 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. diff --git a/common/Globalenvs.v b/common/Globalenvs.v index 65ae06c..b540ad1 100644 --- a/common/Globalenvs.v +++ b/common/Globalenvs.v @@ -64,7 +64,7 @@ Variable V: Type. (**r The type of information attached to variables *) Record t: Type := mkgenv { genv_symb: PTree.t block; (**r mapping symbol -> block *) genv_funs: ZMap.t (option F); (**r mapping function pointer -> definition *) - genv_vars: ZMap.t (option V); (**r mapping variable pointer -> info *) + genv_vars: ZMap.t (option (globvar V)); (**r mapping variable pointer -> info *) genv_nextfun: block; (**r next function pointer *) genv_nextvar: block; (**r next variable pointer *) genv_nextfun_neg: genv_nextfun < 0; @@ -101,7 +101,7 @@ Definition find_funct (ge: t) (v: val) : option F := (** [find_var_info ge b] returns the information attached to the variable at address [b]. *) -Definition find_var_info (ge: t) (b: block) : option V := +Definition find_var_info (ge: t) (b: block) : option (globvar V) := ZMap.get b ge.(genv_vars). (** ** Constructing the global environment *) @@ -143,9 +143,9 @@ Next Obligation. eauto. Qed. -Program Definition add_variable (ge: t) (idv: ident * list init_data * V) : t := +Program Definition add_variable (ge: t) (idv: ident * globvar V) : t := @mkgenv - (PTree.set idv#1#1 ge.(genv_nextvar) ge.(genv_symb)) + (PTree.set idv#1 ge.(genv_nextvar) ge.(genv_symb)) ge.(genv_funs) (ZMap.set ge.(genv_nextvar) (Some idv#2) ge.(genv_vars)) ge.(genv_nextfun) @@ -204,7 +204,7 @@ Qed. Definition add_functions (ge: t) (fl: list (ident * F)) : t := List.fold_left add_function fl ge. -Definition add_variables (ge: t) (vl: list (ident * list init_data * V)) : t := +Definition add_variables (ge: t) (vl: list (ident * globvar V)) : t := List.fold_left add_variable vl ge. Definition globalenv (p: program F V) := @@ -230,19 +230,19 @@ Proof. Qed. Theorem find_symbol_exists: - forall p id init v, - In (id, init, v) (prog_vars p) -> + forall p id gv, + In (id, gv) (prog_vars p) -> exists b, find_symbol (globalenv p) id = Some b. Proof. - intros until v. + intros until gv. assert (forall vl ge, (exists b, find_symbol ge id = Some b) -> exists b, find_symbol (add_variables ge vl) id = Some b). unfold find_symbol; induction vl; simpl; intros. auto. apply IHvl. - simpl. rewrite PTree.gsspec. fold ident. destruct (peq id a#1#1). + simpl. rewrite PTree.gsspec. fold ident. destruct (peq id a#1). exists (genv_nextvar ge); auto. auto. - assert (forall vl ge, In (id, init, v) vl -> + assert (forall vl ge, In (id, gv) vl -> exists b, find_symbol (add_variables ge vl) id = Some b). unfold find_symbol; induction vl; simpl; intros. contradiction. destruct H0. apply H. subst; unfold find_symbol; simpl. @@ -274,7 +274,7 @@ Qed. Remark add_variables_same_symb: forall id vl ge, - ~In id (map (fun idv => idv#1#1) vl) -> + ~In id (map (@fst ident (globvar V)) vl) -> find_symbol (add_variables ge vl) id = find_symbol ge id. Proof. induction vl; simpl; intros. auto. @@ -415,7 +415,7 @@ Remark add_variables_symb_neg: Proof. induction vl; simpl; intros. auto. exploit IHvl; eauto. unfold find_symbol; simpl. rewrite PTree.gsspec. - fold ident. destruct (peq id (a#1#1)); auto. intros. inv H1. + fold ident. destruct (peq id (a#1)); auto. intros. inv H1. generalize (genv_nextvar_pos ge). intros. omegaContradiction. Qed. @@ -522,11 +522,12 @@ Fixpoint init_data_list_size (il: list init_data) {struct il} : Z := | i :: il' => init_data_size i + init_data_list_size il' end. -Definition alloc_variable (m: mem) (idv: ident * list init_data * V) : option mem := - let (m', b) := Mem.alloc m 0 (init_data_list_size idv#1#2) in - store_init_data_list m' b 0 idv#1#2. +Definition alloc_variable (m: mem) (idv: ident * globvar V) : option mem := + let init := idv#2.(gvar_init) in + let (m', b) := Mem.alloc m 0 (init_data_list_size init) in + store_init_data_list m' b 0 init. -Fixpoint alloc_variables (m: mem) (vl: list (ident * list init_data * V)) +Fixpoint alloc_variables (m: mem) (vl: list (ident * globvar V)) {struct vl} : option mem := match vl with | nil => Some m @@ -560,8 +561,9 @@ Proof. simpl; intros. inv H; unfold block; omega. simpl length; rewrite inj_S; simpl. intros m m'. unfold alloc_variable. - caseEq (Mem.alloc m 0 (init_data_list_size (a#1)#2)). intros m1 b ALLOC. - caseEq (store_init_data_list m1 b 0 a#1#2); try congruence. intros m2 STORE REC. + set (init := gvar_init a#2). + caseEq (Mem.alloc m 0 (init_data_list_size init)). intros m1 b ALLOC. + caseEq (store_init_data_list m1 b 0 init); try congruence. intros m2 STORE REC. rewrite (IHvl _ _ REC). rewrite (store_init_data_list_nextblock _ _ _ _ STORE). rewrite (Mem.nextblock_alloc _ _ _ _ _ ALLOC). @@ -590,8 +592,9 @@ Proof. induction vl. simpl; intros. congruence. intros until m'. simpl. unfold alloc_variable. - caseEq (Mem.alloc m 0 (init_data_list_size (a#1)#2)). intros m1 b ALLOC. - caseEq (store_init_data_list m1 b 0 a#1#2); try congruence. intros m2 STORE REC PERM. + set (init := gvar_init a#2). + caseEq (Mem.alloc m 0 (init_data_list_size init)). intros m1 b ALLOC. + caseEq (store_init_data_list m1 b 0 init); try congruence. intros m2 STORE REC PERM. eapply IHvl; eauto. eapply store_init_data_list_perm; eauto. eauto with mem. @@ -616,24 +619,6 @@ Proof. eapply Mem.load_store_other; eauto; intuition. Qed. -(* -Remark alloc_variables_nextblock: - forall vl g m m', - alloc_variables m vl = Some m' -> - Mem.nextblock m = genv_nextvar g -> - Mem.nextblock m' = genv_nextvar (add_variables g vl). -Proof. - induction vl; simpl; intros until m'. - intros. congruence. - unfold alloc_variable. - caseEq (Mem.alloc m 0 (init_data_list_size (a#1)#2)). intros m1 b ALLOC. - caseEq (store_init_data_list m1 b 0 a#1#2); try congruence. intros m2 STORE REC EQ. - eapply IHvl; eauto. - rewrite (store_init_data_list_nextblock _ _ _ _ STORE). - rewrite (Mem.nextblock_alloc _ _ _ _ _ ALLOC). - simpl. unfold block in *; omega. -Qed. -*) Fixpoint load_store_init_data (m: mem) (b: block) (p: Z) (il: list init_data) {struct il} : Prop := match il with | nil => True @@ -697,8 +682,9 @@ Proof. induction vl; simpl; intros until m'. congruence. unfold alloc_variable. - caseEq (Mem.alloc m 0 (init_data_list_size a#1#2)); intros m1 b1 ALLOC. - caseEq (store_init_data_list m1 b1 0 a#1#2); try congruence. intros m2 STO REC VAL. + set (init := gvar_init a#2). + caseEq (Mem.alloc m 0 (init_data_list_size init)); intros m1 b1 ALLOC. + caseEq (store_init_data_list m1 b1 0 init); try congruence. intros m2 STO REC VAL. transitivity (Mem.load chunk m2 b p). apply IHvl; auto. red. rewrite (store_init_data_list_nextblock _ _ _ _ STO). change (Mem.valid_block m1 b). eauto with mem. @@ -720,23 +706,23 @@ Proof. Qed. Lemma alloc_variables_charact: - forall id init v vl g m m', + forall id gv vl g m m', genv_nextvar g = Mem.nextblock m -> alloc_variables m vl = Some m' -> - list_norepet (map (fun v => v#1#1) vl) -> - In (id, init, v) vl -> + list_norepet (map (@fst ident (globvar V)) vl) -> + In (id, gv) vl -> exists b, find_symbol (add_variables g vl) id = Some b - /\ find_var_info (add_variables g vl) b = Some v - /\ Mem.range_perm m' b 0 (init_data_list_size init) Writable - /\ load_store_init_data m' b 0 init. + /\ find_var_info (add_variables g vl) b = Some gv + /\ Mem.range_perm m' b 0 (init_data_list_size gv.(gvar_init)) Writable + /\ load_store_init_data m' b 0 gv.(gvar_init). Proof. induction vl; simpl. contradiction. intros until m'; intro NEXT. - unfold alloc_variable. destruct a as [[id' init'] v']. simpl. - caseEq (Mem.alloc m 0 (init_data_list_size init')); try congruence. + unfold alloc_variable. destruct a as [id' gv']. simpl. + caseEq (Mem.alloc m 0 (init_data_list_size (gvar_init gv'))); try congruence. intros m1 b ALLOC. - caseEq (store_init_data_list m1 b 0 init'); try congruence. + caseEq (store_init_data_list m1 b 0 (gvar_init gv')); try congruence. intros m2 STORE REC NOREPET IN. inv NOREPET. exploit Mem.alloc_result; eauto. intro BEQ. destruct IN. inv H. @@ -778,15 +764,28 @@ Proof. red. rewrite H1. rewrite <- H3. intuition. Qed. +Theorem find_var_info_not_fresh: + forall p b gv m, + init_mem p = Some m -> + find_var_info (globalenv p) b = Some gv -> Mem.valid_block m b. +Proof. + unfold init_mem; intros. + exploit alloc_variables_nextblock; eauto. rewrite Mem.nextblock_empty. intro. + exploit genv_vars_range; eauto. intros. + generalize (add_variables_nextvar (prog_vars p) (add_functions empty_genv (prog_funct p))). + rewrite add_functions_nextvar. simpl genv_nextvar. intro. + red. rewrite H1. rewrite <- H3. intuition. +Qed. + Theorem find_var_exists: - forall p id init v m, + forall p id gv m, list_norepet (prog_var_names p) -> - In (id, init, v) (prog_vars p) -> + In (id, gv) (prog_vars p) -> init_mem p = Some m -> exists b, find_symbol (globalenv p) id = Some b - /\ find_var_info (globalenv p) b = Some v - /\ Mem.range_perm m b 0 (init_data_list_size init) Writable - /\ load_store_init_data (globalenv p) m b 0 init. + /\ find_var_info (globalenv p) b = Some gv + /\ Mem.range_perm m b 0 (init_data_list_size gv.(gvar_init)) Writable + /\ load_store_init_data (globalenv p) m b 0 gv.(gvar_init). Proof. intros. exploit alloc_variables_charact; eauto. instantiate (1 := Mem.empty). rewrite add_functions_nextvar. rewrite Mem.nextblock_empty; auto. @@ -839,7 +838,7 @@ Lemma alloc_variable_neutral: Mem.inject_neutral thr m'. Proof. intros until m'. unfold alloc_variable. - caseEq (Mem.alloc m 0 (init_data_list_size (id#1)#2)); intros m1 b; intros. + caseEq (Mem.alloc m 0 (init_data_list_size (gvar_init id#2))); intros m1 b; intros. eapply store_init_data_list_neutral with (b := b). eapply Mem.alloc_inject_neutral; eauto. rewrite (Mem.alloc_result _ _ _ _ _ H). auto. @@ -887,7 +886,12 @@ Section MATCH_PROGRAMS. Variables A B V W: Type. Variable match_fun: A -> B -> Prop. -Variable match_var: V -> W -> Prop. +Variable match_varinfo: V -> W -> Prop. + +Inductive match_globvar: globvar V -> globvar W -> Prop := + | match_globvar_intro: forall info1 info2 init ro vo, + match_varinfo info1 info2 -> + match_globvar (mkglobvar info1 init ro vo) (mkglobvar info2 init ro vo). Record match_genvs (ge1: t A V) (ge2: t B W): Prop := { mge_nextfun: genv_nextfun ge1 = genv_nextfun ge2; @@ -901,10 +905,10 @@ Record match_genvs (ge1: t A V) (ge2: t B W): Prop := { exists f, ZMap.get b (genv_funs ge1) = Some f /\ match_fun f tf; mge_vars: forall b v, ZMap.get b (genv_vars ge1) = Some v -> - exists tv, ZMap.get b (genv_vars ge2) = Some tv /\ match_var v tv; + exists tv, ZMap.get b (genv_vars ge2) = Some tv /\ match_globvar v tv; mge_rev_vars: forall b tv, ZMap.get b (genv_vars ge2) = Some tv -> - exists v, ZMap.get b (genv_vars ge1) = Some v /\ match_var v tv + exists v, ZMap.get b (genv_vars ge1) = Some v /\ match_globvar v tv }. Lemma add_function_match: @@ -939,10 +943,10 @@ Proof. Qed. Lemma add_variable_match: - forall ge1 ge2 id idl v1 v2, + forall ge1 ge2 id v1 v2, match_genvs ge1 ge2 -> - match_var v1 v2 -> - match_genvs (add_variable ge1 (id, idl, v1)) (add_variable ge2 (id, idl, v2)). + match_globvar v1 v2 -> + match_genvs (add_variable ge1 (id, v1)) (add_variable ge2 (id, v2)). Proof. intros. destruct H. constructor; simpl. congruence. congruence. congruence. @@ -959,19 +963,18 @@ Proof. Qed. Lemma add_variables_match: - forall vl1 vl2, list_forall2 (match_var_entry match_var) vl1 vl2 -> + forall vl1 vl2, list_forall2 (match_var_entry match_varinfo) vl1 vl2 -> forall ge1 ge2, match_genvs ge1 ge2 -> match_genvs (add_variables ge1 vl1) (add_variables ge2 vl2). Proof. induction 1; intros; simpl. auto. - destruct a1 as [[id1 init1] f1]; destruct b1 as [[id2 init2] f2]. - destruct H. destruct H2. subst. apply IHlist_forall2. apply add_variable_match; auto. + inv H. apply IHlist_forall2. apply add_variable_match; auto. constructor; auto. Qed. Variable p: program A V. Variable p': program B W. -Hypothesis progmatch: match_program match_fun match_var p p'. +Hypothesis progmatch: match_program match_fun match_varinfo p p'. Lemma globalenvs_match: match_genvs (globalenv p) (globalenv p'). @@ -1018,17 +1021,17 @@ Proof. Qed. Theorem find_var_info_match: - forall (b : block) (v : V), + forall (b : block) (v : globvar V), find_var_info (globalenv p) b = Some v -> exists tv, - find_var_info (globalenv p') b = Some tv /\ match_var v tv. + find_var_info (globalenv p') b = Some tv /\ match_globvar v tv. Proof (mge_vars globalenvs_match). Theorem find_var_info_rev_match: - forall (b : block) (tv : W), + forall (b : block) (tv : globvar W), find_var_info (globalenv p') b = Some tv -> exists v, - find_var_info (globalenv p) b = Some v /\ match_var v tv. + find_var_info (globalenv p) b = Some v /\ match_globvar v tv. Proof (mge_rev_vars globalenvs_match). Theorem find_symbol_match: @@ -1052,18 +1055,17 @@ Proof. Qed. Lemma alloc_variables_match: - forall vl1 vl2, list_forall2 (match_var_entry match_var) vl1 vl2 -> + forall vl1 vl2, list_forall2 (match_var_entry match_varinfo) vl1 vl2 -> forall m, alloc_variables (globalenv p') m vl2 = alloc_variables (globalenv p) m vl1. Proof. induction 1; intros; simpl. auto. - destruct a1 as [[id1 init1] v1]; destruct b1 as [[id2 init2] v2]. - destruct H. destruct H1. subst. + inv H. unfold alloc_variable; simpl. - destruct (Mem.alloc m 0 (init_data_list_size init2)). + destruct (Mem.alloc m 0 (init_data_list_size init)). rewrite store_init_data_list_match. - destruct (store_init_data_list (globalenv p) m0 b 0 init2); auto. + destruct (store_init_data_list (globalenv p) m0 b 0 init); auto. Qed. Theorem init_mem_match: @@ -1135,25 +1137,27 @@ Proof. Qed. Theorem find_var_info_transf_partial2: - forall (b: block) (v: V), + forall (b: block) (v: globvar V), find_var_info (globalenv p) b = Some v -> exists v', - find_var_info (globalenv p') b = Some v' /\ transf_var v = OK v'. + find_var_info (globalenv p') b = Some v' /\ transf_globvar transf_var v = OK v'. Proof. intros. exploit find_var_info_match. eexact prog_match. eauto. - intros [tv [X Y]]. exists tv; auto. + intros [tv [X Y]]. exists tv; split; auto. inv Y. unfold transf_globvar; simpl. + rewrite H0; simpl. auto. Qed. Theorem find_var_info_rev_transf_partial2: - forall (b: block) (v': W), + forall (b: block) (v': globvar W), find_var_info (globalenv p') b = Some v' -> exists v, - find_var_info (globalenv p) b = Some v /\ transf_var v = OK v'. + find_var_info (globalenv p) b = Some v /\ transf_globvar transf_var v = OK v'. Proof. intros. exploit find_var_info_rev_match. eexact prog_match. eauto. - intros [v [X Y]]. exists v; auto. + intros [v [X Y]]. exists v; split; auto. inv Y. unfold transf_globvar; simpl. + rewrite H0; simpl. auto. Qed. Theorem find_symbol_transf_partial2: @@ -1182,9 +1186,12 @@ Hypothesis transf_OK: transform_partial_program transf p = OK p'. Remark transf2_OK: transform_partial_program2 transf (fun x => OK x) p = OK p'. Proof. - rewrite <- transf_OK. unfold transform_partial_program2, transform_partial_program. - destruct (map_partial prefix_funct_name transf (prog_funct p)); auto. - rewrite map_partial_identity; auto. + rewrite <- transf_OK. + unfold transform_partial_program2, transform_partial_program. + destruct (map_partial prefix_name transf (prog_funct p)); auto. + simpl. replace (transf_globvar (fun (x : V) => OK x)) with (fun (v: globvar V) => OK v). + rewrite map_partial_identity; auto. + apply extensionality; intros. destruct x; auto. Qed. Theorem find_funct_ptr_transf_partial: @@ -1228,6 +1235,19 @@ Proof. exact (@find_symbol_transf_partial2 _ _ _ _ _ _ _ _ transf2_OK). Qed. +Theorem find_var_info_transf_partial: + forall (b: block), + find_var_info (globalenv p') b = find_var_info (globalenv p) b. +Proof. + intros. case_eq (find_var_info (globalenv p) b); intros. + exploit find_var_info_transf_partial2. eexact transf2_OK. eauto. + intros [v' [P Q]]. monadInv Q. rewrite P. inv EQ. destruct g; auto. + case_eq (find_var_info (globalenv p') b); intros. + exploit find_var_info_rev_transf_partial2. eexact transf2_OK. eauto. + intros [v' [P Q]]. monadInv Q. inv EQ. congruence. + auto. +Qed. + Theorem init_mem_transf_partial: forall m, init_mem p = Some m -> init_mem p' = Some m. Proof. @@ -1295,6 +1315,13 @@ Proof. exact (@find_symbol_transf_partial _ _ _ _ _ _ transf_OK). Qed. +Theorem find_var_info_transf: + forall (b: block), + find_var_info (globalenv tp) b = find_var_info (globalenv p) b. +Proof. + exact (@find_var_info_transf_partial _ _ _ _ _ _ transf_OK). +Qed. + Theorem init_mem_transf: forall m, init_mem p = Some m -> init_mem tp = Some m. Proof. diff --git a/common/Values.v b/common/Values.v index 056cffb..236a5ae 100644 --- a/common/Values.v +++ b/common/Values.v @@ -1029,6 +1029,14 @@ Inductive val_list_inject (mi: meminj): list val -> list val-> Prop:= Hint Resolve val_nil_inject val_cons_inject. +Lemma val_load_result_inject: + forall f chunk v1 v2, + val_inject f v1 v2 -> + val_inject f (Val.load_result chunk v1) (Val.load_result chunk v2). +Proof. + intros. inv H; destruct chunk; simpl; econstructor; eauto. +Qed. + (** Monotone evolution of a memory injection. *) Definition inject_incr (f1 f2: meminj) : Prop := -- cgit v1.2.3