From 1e29e518e62ad88e9c2e2b180beb07434a07cdd7 Mon Sep 17 00:00:00 2001 From: Xavier Leroy Date: Mon, 3 Nov 2014 10:11:23 +0100 Subject: Record public global definitions via field "prog_public" in AST.program. For the moment, this field is ignored. --- common/AST.v | 28 +++++++++++++++++++++++++--- 1 file changed, 25 insertions(+), 3 deletions(-) (limited to 'common') diff --git a/common/AST.v b/common/AST.v index 1c46389e..75286bd6 100644 --- a/common/AST.v +++ b/common/AST.v @@ -201,6 +201,8 @@ Record globvar (V: Type) : Type := mkglobvar { (** Whole programs consist of: - a collection of global definitions (name and description); +- a set of public names (the names that are visible outside + this compilation unit); - the name of the ``main'' function that serves as entry point in the program. A global definition is either a global function or a global variable. @@ -218,6 +220,7 @@ Implicit Arguments Gvar [F V]. Record program (F V: Type) : Type := mkprogram { prog_defs: list (ident * globdef F V); + prog_public: list ident; prog_main: ident }. @@ -244,6 +247,7 @@ Definition transform_program_globdef (idg: ident * globdef A V) : ident * globde Definition transform_program (p: program A V) : program B V := mkprogram (List.map transform_program_globdef p.(prog_defs)) + p.(prog_public) p.(prog_main). Lemma transform_program_function: @@ -295,7 +299,8 @@ Fixpoint transf_globdefs (l: list (ident * globdef A V)) : res (list (ident * gl end. Definition transform_partial_program2 (p: program A V) : res (program B W) := - do gl' <- transf_globdefs p.(prog_defs); OK(mkprogram gl' p.(prog_main)). + do gl' <- transf_globdefs p.(prog_defs); + OK (mkprogram gl' p.(prog_public) p.(prog_main)). Lemma transform_partial_program2_function: forall p tp i tf, @@ -363,6 +368,14 @@ Proof. intros. monadInv H. reflexivity. Qed. +Lemma transform_partial_program2_public: + forall p tp, + transform_partial_program2 p = OK tp -> + tp.(prog_public) = p.(prog_public). +Proof. + intros. monadInv H. reflexivity. +Qed. + (** Additionally, we can also "augment" the program with new global definitions and a different "main" function. *) @@ -373,7 +386,7 @@ Variable new_main: ident. Definition transform_partial_augment_program (p: program A V) : res (program B W) := do gl' <- transf_globdefs p.(prog_defs); - OK(mkprogram (gl' ++ new_globs) new_main). + OK(mkprogram (gl' ++ new_globs) p.(prog_public) new_main). Lemma transform_partial_augment_program_main: forall p tp, @@ -416,6 +429,14 @@ Proof. apply transform_partial_program2_main. Qed. +Lemma transform_partial_program_public: + forall p tp, + transform_partial_program p = OK tp -> + tp.(prog_public) = p.(prog_public). +Proof. + apply transform_partial_program2_public. +Qed. + Lemma transform_partial_program_function: forall p tp i tf, transform_partial_program p = OK tp -> @@ -480,7 +501,8 @@ Definition match_program (new_globs : list (ident * globdef B W)) (p1: program A V) (p2: program B W) : Prop := (exists tglob, list_forall2 match_globdef p1.(prog_defs) tglob /\ p2.(prog_defs) = tglob ++ new_globs) /\ - p2.(prog_main) = new_main. + p2.(prog_main) = new_main /\ + p2.(prog_public) = p1.(prog_public). End MATCH_PROGRAM. -- cgit From ad8c37d0ebb36cb2e54baeacf5a4c7ff145b1a99 Mon Sep 17 00:00:00 2001 From: Xavier Leroy Date: Mon, 3 Nov 2014 17:40:22 +0100 Subject: Add Genv.public_symbol operation. Restrict pointer event values to public global names. Update proofs accordingly. PowerPC and ARM need updating. --- common/AST.v | 9 ++ common/Events.v | 403 +++++++++++++++++++++++++++++++--------------------- common/Globalenvs.v | 82 ++++++++++- common/Smallstep.v | 28 ++-- 4 files changed, 342 insertions(+), 180 deletions(-) (limited to 'common') diff --git a/common/AST.v b/common/AST.v index 75286bd6..9c29a374 100644 --- a/common/AST.v +++ b/common/AST.v @@ -657,6 +657,15 @@ Proof. Defined. Global Opaque external_function_eq. +(** Global variables referenced by an external function *) + +Definition globals_external (ef: external_function) : list ident := + match ef with + | EF_vload_global _ id _ => id :: nil + | EF_vstore_global _ id _ => id :: nil + | _ => nil + end. + (** Function definitions are the union of internal and external functions. *) Inductive fundef (F: Type): Type := diff --git a/common/Events.v b/common/Events.v index 8787a14b..175655be 100644 --- a/common/Events.v +++ b/common/Events.v @@ -276,6 +276,7 @@ Inductive eventval_match: eventval -> typ -> val -> Prop := | ev_match_single: forall f, eventval_match (EVsingle f) Tsingle (Vsingle f) | ev_match_ptr: forall id b ofs, + Genv.public_symbol ge id = true -> Genv.find_symbol ge id = Some b -> eventval_match (EVptr_global id ofs) Tint (Vptr b ofs). @@ -318,45 +319,6 @@ Proof. 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, 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). - -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. inv H; inv H0; try constructor; auto. - 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 eventval_match_inject_2: - forall ev ty v, - eventval_match ev ty v -> val_inject f v v. -Proof. - induction 1; auto. - destruct glob_pres as [A [B C]]. - exploit A; eauto. intro EQ. - econstructor; eauto. rewrite Int.add_zero; auto. -Qed. - -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. - induction 1; intros. inv H; constructor. - inv H1. constructor. eapply eventval_match_inject; eauto. eauto. -Qed. - (** Determinism *) Lemma eventval_match_determ_1: @@ -388,7 +350,7 @@ Definition eventval_valid (ev: eventval) : Prop := | EVlong _ => True | EVfloat _ => True | EVsingle _ => True - | EVptr_global id ofs => exists b, Genv.find_symbol ge id = Some b + | EVptr_global id ofs => Genv.public_symbol ge id = true end. Definition eventval_type (ev: eventval) : typ := @@ -407,19 +369,21 @@ Lemma eventval_match_receptive: exists v2, eventval_match ev2 ty v2. Proof. intros. inv H; destruct ev2; simpl in H2; try discriminate. - exists (Vint i0); constructor. - destruct H1 as [b EQ]. exists (Vptr b i1); constructor; auto. - exists (Vlong i0); constructor. - exists (Vfloat f1); constructor. - exists (Vsingle f1); constructor; auto. - exists (Vint i); constructor. - destruct H1 as [b' EQ]. exists (Vptr b' i0); constructor; auto. +- exists (Vint i0); constructor. +- simpl in H1; exploit Genv.public_symbol_exists; eauto. intros [b FS]. + exists (Vptr b i1); constructor; auto. +- exists (Vlong i0); constructor. +- exists (Vfloat f0); constructor. +- exists (Vsingle f0); constructor; auto. +- exists (Vint i); constructor. +- simpl in H1. exploit Genv.public_symbol_exists. eexact H1. intros [b' FS]. + exists (Vptr b' i0); constructor; auto. Qed. Lemma eventval_match_valid: forall ev ty v, eventval_match ev ty v -> eventval_valid ev. Proof. - destruct 1; simpl; auto. exists b; auto. + destruct 1; simpl; auto. Qed. Lemma eventval_match_same_type: @@ -439,6 +403,15 @@ Variables F1 V1 F2 V2: Type. Variable ge1: Genv.t F1 V1. Variable ge2: Genv.t F2 V2. +Hypothesis public_preserved: + forall id, Genv.public_symbol ge2 id = Genv.public_symbol ge1 id. + +Lemma eventval_valid_preserved: + forall ev, eventval_valid ge1 ev -> eventval_valid ge2 ev. +Proof. + intros. destruct ev; simpl in *; auto. rewrite <- H; auto. +Qed. + Hypothesis symbols_preserved: forall id, Genv.find_symbol ge2 id = Genv.find_symbol ge1 id. @@ -446,7 +419,9 @@ Lemma eventval_match_preserved: forall ev ty v, eventval_match ge1 ev ty v -> eventval_match ge2 ev ty v. Proof. - induction 1; constructor; auto. rewrite symbols_preserved; auto. + induction 1; constructor; auto. + rewrite public_preserved; auto. + rewrite symbols_preserved; auto. Qed. Lemma eventval_list_match_preserved: @@ -456,14 +431,68 @@ Proof. induction 1; constructor; auto. eapply eventval_match_preserved; eauto. Qed. -Lemma eventval_valid_preserved: - forall ev, eventval_valid ge1 ev -> eventval_valid ge2 ev. +End EVENTVAL_INV. + +(** Used for the semantics of volatile memory accesses. Move to [Globalenv] ? *) + +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. + +(** Compatibility with memory injections *) + +Section EVENTVAL_INJECT. + +Variables F1 V1 F2 V2: Type. +Variable f: block -> option (block * Z). +Variable ge1: Genv.t F1 V1. +Variable ge2: Genv.t F2 V2. + +Definition symbols_inject : Prop := + (forall id, Genv.public_symbol ge2 id = Genv.public_symbol ge1 id) +/\ (forall id b1 b2 delta, + f b1 = Some(b2, delta) -> Genv.find_symbol ge1 id = Some b1 -> + delta = 0 /\ Genv.find_symbol ge2 id = Some b2) +/\ (forall id b1, + Genv.public_symbol ge1 id = true -> Genv.find_symbol ge1 id = Some b1 -> + exists b2, f b1 = Some(b2, 0) /\ Genv.find_symbol ge2 id = Some b2) +/\ (forall b1 b2 delta, + f b1 = Some(b2, delta) -> + block_is_volatile ge2 b2 = block_is_volatile ge1 b1). + +Hypothesis symb_inj: symbols_inject. + +Lemma eventval_match_inject: + forall ev ty v1 v2, + eventval_match ge1 ev ty v1 -> val_inject f v1 v2 -> eventval_match ge2 ev ty v2. Proof. - unfold eventval_valid; destruct ev; auto. - intros [b A]. exists b; rewrite symbols_preserved; auto. + intros. inv H; inv H0; try constructor; auto. + destruct symb_inj as (A & B & C & D). exploit C; eauto. intros [b3 [EQ FS]]. rewrite H4 in EQ; inv EQ. + rewrite Int.add_zero. constructor; auto. rewrite A; auto. Qed. -End EVENTVAL_INV. +Lemma eventval_match_inject_2: + forall ev ty v1, + eventval_match ge1 ev ty v1 -> + exists v2, eventval_match ge2 ev ty v2 /\ val_inject f v1 v2. +Proof. + intros. inv H; try (econstructor; split; eauto; constructor; fail). + destruct symb_inj as (A & B & C & D). exploit C; eauto. intros [b2 [EQ FS]]. + exists (Vptr b2 ofs); split. econstructor; eauto. + econstructor; eauto. rewrite Int.add_zero; auto. +Qed. + +Lemma eventval_list_match_inject: + forall evl tyl vl1, eventval_list_match ge1 evl tyl vl1 -> + forall vl2, val_list_inject f vl1 vl2 -> eventval_list_match ge2 evl tyl vl2. +Proof. + induction 1; intros. inv H; constructor. + inv H1. constructor. eapply eventval_match_inject; eauto. eauto. +Qed. + +End EVENTVAL_INJECT. (** * Matching traces. *) @@ -501,8 +530,8 @@ 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. +Hypothesis public_preserved: + forall id, Genv.public_symbol ge2 id = Genv.public_symbol ge1 id. Lemma match_traces_preserved: forall t1 t2, match_traces ge1 t1 t2 -> match_traces ge2 t1 t2. @@ -531,12 +560,6 @@ Fixpoint output_trace (t: trace) : Prop := (** * Semantics of volatile memory accesses *) -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. - Inductive volatile_load (F V: Type) (ge: Genv.t F V): memory_chunk -> mem -> block -> int -> trace -> val -> Prop := | volatile_load_vol: forall chunk m b ofs id ev v, @@ -600,7 +623,8 @@ Definition inject_separated (f f': meminj) (m1 m2: mem): Prop := ~Mem.valid_block m1 b1 /\ ~Mem.valid_block m2 b2. Record extcall_properties (sem: extcall_sem) - (sg: signature) : Prop := mk_extcall_properties { + (sg: signature) (free_globals: list ident) : Prop := + mk_extcall_properties { (** The return value of an external call must agree with its signature. *) ec_well_typed: @@ -612,6 +636,7 @@ Record extcall_properties (sem: extcall_sem) 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 id, Genv.public_symbol ge2 id = Genv.public_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; @@ -653,13 +678,16 @@ Record extcall_properties (sem: extcall_sem) (** External calls must commute with memory injections, in the following sense. *) ec_mem_inject: - 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 -> + forall F1 V1 F2 V2 (ge1: Genv.t F1 V1) (ge2: Genv.t F2 V2) vargs m1 t vres m2 f m1' vargs', + symbols_inject f ge1 ge2 -> + (forall id b1, + In id free_globals -> Genv.find_symbol ge1 id = Some b1 -> + exists b2, f b1 = Some(b2, 0) /\ Genv.find_symbol ge2 id = Some b2) -> + sem F1 V1 ge1 vargs m1 t vres m2 -> Mem.inject f m1 m1' -> val_list_inject f vargs vargs' -> exists f', exists vres', exists m2', - sem F V ge vargs' m1' t vres' m2' + sem F2 V2 ge2 vargs' m1' t vres' m2' /\ val_inject f' vres vres' /\ Mem.inject f' m2 m2' /\ Mem.unchanged_on (loc_unmapped f) m1 m2 @@ -696,15 +724,16 @@ Inductive volatile_load_sem (chunk: memory_chunk) (F V: Type) (ge: Genv.t F V): Lemma volatile_load_preserved: forall F1 V1 (ge1: Genv.t F1 V1) F2 V2 (ge2: Genv.t F2 V2) chunk m b ofs t v, (forall id, Genv.find_symbol ge2 id = Genv.find_symbol ge1 id) -> + (forall id, Genv.public_symbol ge2 id = Genv.public_symbol ge1 id) -> (forall b, block_is_volatile ge2 b = block_is_volatile ge1 b) -> volatile_load ge1 chunk m b ofs t v -> volatile_load ge2 chunk m b ofs t v. Proof. - intros. inv H1; constructor; auto. - rewrite H0; auto. + intros. inv H2; constructor; auto. + rewrite H1; auto. rewrite H; auto. eapply eventval_match_preserved; eauto. - rewrite H0; auto. + rewrite H1; auto. Qed. Lemma volatile_load_extends: @@ -718,35 +747,28 @@ Proof. exploit Mem.load_extends; eauto. intros [v' [A B]]. exists v'; split; auto. constructor; auto. Qed. -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_inject: - forall F V (ge: Genv.t F V) f chunk m b ofs t v b' ofs' m', - meminj_preserves_globals ge f -> - volatile_load ge chunk m b ofs t v -> + forall F1 V1 F2 V2 (ge1: Genv.t F1 V1) (ge2: Genv.t F2 V2) f chunk m b ofs t v b' ofs' m', + symbols_inject f ge1 ge2 -> + volatile_load ge1 chunk m b ofs t v -> val_inject f (Vptr b ofs) (Vptr b' ofs') -> Mem.inject f m m' -> - exists v', volatile_load ge chunk m' b' ofs' t v' /\ val_inject f v v'. -Proof. - intros. inv H0. - inv H1. exploit (proj1 H); eauto. intros EQ; rewrite H8 in EQ; inv EQ. - rewrite Int.add_zero. exists (Val.load_result chunk v0); split. - constructor; auto. - apply val_load_result_inject. eapply eventval_match_inject_2; eauto. - exploit Mem.loadv_inject; eauto. simpl; eauto. simpl; intros [v' [A B]]. exists v'; split; auto. - constructor; auto. rewrite <- H3. inv H1. eapply meminj_preserves_block_is_volatile; eauto. + exists v', volatile_load ge2 chunk m' b' ofs' t v' /\ val_inject f v v'. +Proof. + intros until m'; intros SI VL VI MI. generalize SI; intros (A & B & C & D). + inv VL. +- (* volatile load *) + inv VI. exploit B; eauto. intros [U V]. subst delta. + exploit eventval_match_inject_2; eauto. intros (v2 & X & Y). + rewrite Int.add_zero. exists (Val.load_result chunk v2); split. + constructor; auto. + erewrite D; eauto. + apply val_load_result_inject. auto. +- (* normal load *) + exploit Mem.loadv_inject; eauto. simpl; eauto. simpl; intros (v2 & X & Y). + exists v2; split; auto. + constructor; auto. + inv VI. erewrite D; eauto. Qed. Lemma volatile_load_receptive: @@ -763,14 +785,15 @@ Qed. Lemma volatile_load_ok: forall chunk, extcall_properties (volatile_load_sem chunk) - (mksignature (Tint :: nil) (Some (type_of_chunk chunk)) cc_default). + (mksignature (Tint :: nil) (Some (type_of_chunk chunk)) cc_default) + nil. Proof. intros; constructor; intros. (* well typed *) unfold proj_sig_res; simpl. inv H. inv H0. apply Val.load_result_type. eapply Mem.load_type; eauto. (* symbols *) - inv H1. constructor. eapply volatile_load_preserved; eauto. + inv H2. constructor. eapply volatile_load_preserved; eauto. (* valid blocks *) inv H; auto. (* max perms *) @@ -782,7 +805,7 @@ Proof. exploit volatile_load_extends; eauto. intros [v' [A B]]. exists v'; exists m1'; intuition. constructor; auto. (* mem injects *) - inv H0. inv H2. inv H7. inversion H5; subst. + inv H1. inv H3. inv H8. inversion H6; subst. exploit volatile_load_inject; eauto. intros [v' [A B]]. exists f; exists v'; exists m1'; intuition. constructor; auto. red; intros. congruence. @@ -825,14 +848,15 @@ 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). + (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 H1. econstructor. rewrite H; eauto. eapply volatile_load_preserved; eauto. + inv H2. econstructor. rewrite H; eauto. eapply volatile_load_preserved; eauto. (* valid blocks *) inv H; auto. (* max perm *) @@ -843,9 +867,10 @@ Proof. inv H. inv H1. exploit volatile_load_extends; eauto. intros [v' [A B]]. exists v'; exists m1'; intuition. econstructor; eauto. (* inject *) - inv H0. inv H2. - assert (val_inject f (Vptr b ofs) (Vptr b ofs)). - exploit (proj1 H); eauto. intros EQ. econstructor. eauto. rewrite Int.add_zero; auto. + 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. @@ -872,15 +897,16 @@ Inductive volatile_store_sem (chunk: memory_chunk) (F V: Type) (ge: Genv.t F V): Lemma volatile_store_preserved: forall F1 V1 (ge1: Genv.t F1 V1) F2 V2 (ge2: Genv.t F2 V2) chunk m1 b ofs v t m2, (forall id, Genv.find_symbol ge2 id = Genv.find_symbol ge1 id) -> + (forall id, Genv.public_symbol ge2 id = Genv.public_symbol ge1 id) -> (forall b, block_is_volatile ge2 b = block_is_volatile ge1 b) -> volatile_store ge1 chunk m1 b ofs v t m2 -> volatile_store ge2 chunk m1 b ofs v t m2. Proof. - intros. inv H1; constructor; auto. - rewrite H0; auto. + intros. inv H2; constructor; auto. + rewrite H1; auto. rewrite H; auto. eapply eventval_match_preserved; eauto. - rewrite H0; auto. + rewrite H1; auto. Qed. Lemma volatile_store_readonly: @@ -922,38 +948,44 @@ Proof. Qed. Lemma volatile_store_inject: - forall F V (ge: Genv.t F V) f chunk m1 b ofs v t m2 m1' b' ofs' v', - meminj_preserves_globals ge f -> - volatile_store ge chunk m1 b ofs v t m2 -> + forall F1 V1 F2 V2 (ge1: Genv.t F1 V1) (ge2: Genv.t F2 V2) f chunk m1 b ofs v t m2 m1' b' ofs' v', + symbols_inject f ge1 ge2 -> + volatile_store ge1 chunk m1 b ofs v t m2 -> val_inject f (Vptr b ofs) (Vptr b' ofs') -> val_inject f v v' -> Mem.inject f m1 m1' -> exists m2', - volatile_store ge chunk m1' b' ofs' v' t m2' + volatile_store ge2 chunk m1' b' ofs' v' t m2' /\ Mem.inject f m2 m2' /\ Mem.unchanged_on (loc_unmapped f) m1 m2 /\ Mem.unchanged_on (loc_out_of_reach f m1) m1' m2'. Proof. - intros. inv H0. -- inv H1. exploit (proj1 H); eauto. intros EQ; rewrite H9 in EQ; inv EQ. - rewrite Int.add_zero. exists m1'. intuition. - constructor; auto. - eapply eventval_match_inject; eauto. apply val_load_result_inject; auto. -- assert (Mem.storev chunk m1 (Vptr b ofs) v = Some m2). simpl; auto. + intros until v'; intros SI VS AI VI MI. + generalize SI; intros (P & Q & R & S). + inv VS. +- (* volatile store *) + inv AI. exploit Q; eauto. intros [A B]. subst delta. + rewrite Int.add_zero. exists m1'; split. + constructor; auto. erewrite S; eauto. + eapply eventval_match_inject; eauto. apply val_load_result_inject. auto. + intuition auto with mem. +- (* normal store *) + inversion AI; subst. + assert (Mem.storev chunk m1 (Vptr b ofs) v = Some m2). simpl; auto. exploit Mem.storev_mapped_inject; eauto. intros [m2' [A B]]. - inv H1. exists m2'; intuition. -+ constructor; auto. rewrite <- H4. eapply meminj_preserves_block_is_volatile; eauto. + exists m2'; intuition auto. ++ constructor; auto. erewrite S; eauto. + eapply Mem.store_unchanged_on; eauto. - unfold loc_unmapped; intros. congruence. + unfold loc_unmapped; intros. inv AI; congruence. + eapply Mem.store_unchanged_on; eauto. unfold loc_out_of_reach; intros. red; intros. simpl in A. assert (EQ: Int.unsigned (Int.add ofs (Int.repr delta)) = Int.unsigned ofs + delta) by (eapply Mem.address_inject; eauto with mem). rewrite EQ in *. - eelim H6; eauto. - exploit Mem.store_valid_access_3. eexact H5. intros [P Q]. + eelim H3; eauto. + exploit Mem.store_valid_access_3. eexact H0. intros [X Y]. apply Mem.perm_cur_max. apply Mem.perm_implies with Writable; auto with mem. - apply P. omega. + apply X. omega. Qed. Lemma volatile_store_receptive: @@ -966,13 +998,14 @@ Qed. Lemma volatile_store_ok: forall chunk, extcall_properties (volatile_store_sem chunk) - (mksignature (Tint :: type_of_chunk chunk :: nil) None cc_default). + (mksignature (Tint :: type_of_chunk chunk :: nil) None cc_default) + nil. Proof. intros; constructor; intros. (* well typed *) unfold proj_sig_res; simpl. inv H; constructor. (* symbols preserved *) - inv H1. constructor. eapply volatile_store_preserved; eauto. + inv H2. constructor. eapply volatile_store_preserved; eauto. (* valid block *) inv H. inv H1. auto. eauto with mem. (* perms *) @@ -984,7 +1017,7 @@ Proof. exploit volatile_store_extends; eauto. intros [m2' [A [B C]]]. exists Vundef; exists m2'; intuition. constructor; auto. (* mem inject *) - inv H0. inv H2. inv H7. inv H8. inversion H5; subst. + inv H1. inv H3. inv H8. inv H9. inversion H6; 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 *) @@ -1021,13 +1054,14 @@ 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). + (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 H1. econstructor. rewrite H; eauto. eapply volatile_store_preserved; eauto. + inv H2. econstructor. rewrite H; eauto. eapply volatile_store_preserved; eauto. (* valid block *) inv H. inv H2. auto. eauto with mem. (* perms *) @@ -1040,13 +1074,13 @@ Proof. 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 H0. destruct H0 as [b [P Q]]. - exploit (proj1 H). eauto. intros EQ. - assert (val_inject f (Vptr b ofs) (Vptr b ofs)). econstructor; eauto. rewrite Int.add_zero; auto. - exploit ec_mem_inject. eapply volatile_store_ok. eauto. eexact Q. eauto. eauto. + 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 b; auto. + rewrite volatile_store_global_charact. exists b2; auto. (* trace length *) inv H. inv H1; simpl; omega. (* receptive *) @@ -1069,7 +1103,8 @@ Inductive extcall_malloc_sem (F V: Type) (ge: Genv.t F V): Lemma extcall_malloc_ok: extcall_properties extcall_malloc_sem - (mksignature (Tint :: nil) (Some Tint) cc_default). + (mksignature (Tint :: nil) (Some Tint) cc_default) + nil. Proof. assert (UNCHANGED: forall (P: block -> Z -> Prop) m n m' b m'', @@ -1089,7 +1124,7 @@ Proof. (* well typed *) inv H. unfold proj_sig_res; simpl. auto. (* symbols preserved *) - inv H1; econstructor; eauto. + inv H2; econstructor; eauto. (* valid block *) inv H. eauto with mem. (* perms *) @@ -1109,7 +1144,7 @@ Proof. econstructor; eauto. eapply UNCHANGED; eauto. (* mem injects *) - inv H0. inv H2. inv H6. inv H8. + inv H1. inv H3. inv H7. inv H9. 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. @@ -1121,8 +1156,8 @@ Proof. eapply UNCHANGED; eauto. eapply UNCHANGED; eauto. red; intros. destruct (eq_block b1 b). - subst b1. rewrite C in H2. inv H2. eauto with mem. - rewrite D in H2. congruence. auto. + subst b1. rewrite C in H3. inv H3. eauto with mem. + rewrite D in H3 by auto. congruence. (* trace length *) inv H; simpl; omega. (* receptive *) @@ -1144,13 +1179,14 @@ Inductive extcall_free_sem (F V: Type) (ge: Genv.t F V): Lemma extcall_free_ok: extcall_properties extcall_free_sem - (mksignature (Tint :: nil) None cc_default). + (mksignature (Tint :: nil) None cc_default) + nil. Proof. constructor; intros. (* well typed *) inv H. unfold proj_sig_res. simpl. auto. (* symbols preserved *) - inv H1; econstructor; eauto. + inv H2; econstructor; eauto. (* valid block *) inv H. eauto with mem. (* perms *) @@ -1173,13 +1209,13 @@ Proof. eapply Mem.free_range_perm. eexact H4. eauto. } tauto. (* mem inject *) - inv H0. inv H2. inv H7. inv H9. + inv H1. inv H3. inv H8. inv H10. 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 H0. instantiate (1 := lo). omega. + apply H1. instantiate (1 := lo). omega. intro EQ. exploit Mem.free_parallel_inject; eauto. intros (m2' & C & D). exists f, Vundef, m2'; split. @@ -1191,9 +1227,9 @@ 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 H7; eauto. + intros. red; intros. eelim H8; eauto. apply Mem.perm_cur_max. apply Mem.perm_implies with Freeable; auto with mem. - apply H0. omega. + apply H1. omega. split. auto. red; intros. congruence. (* trace length *) @@ -1221,13 +1257,15 @@ Inductive extcall_memcpy_sem (sz al: Z) (F V: Type) (ge: Genv.t F V): list val - Lemma extcall_memcpy_ok: forall sz al, - extcall_properties (extcall_memcpy_sem sz al) (mksignature (Tint :: Tint :: nil) None cc_default). + extcall_properties (extcall_memcpy_sem sz al) + (mksignature (Tint :: Tint :: nil) None cc_default) + nil. Proof. intros. constructor. - (* return type *) intros. inv H. constructor. - (* change of globalenv *) - intros. inv H1. econstructor; eauto. + intros. inv H2. econstructor; eauto. - (* valid blocks *) intros. inv H. eauto with mem. - (* perms *) @@ -1253,7 +1291,7 @@ Proof. erewrite list_forall2_length; eauto. tauto. - (* injections *) - intros. inv H0. inv H2. inv H14. inv H15. inv H11. inv H12. + intros. inv H1. inv H3. inv H15. inv H16. inv H12. inv H13. destruct (zeq sz 0). + (* special case sz = 0 *) assert (bytes = nil). @@ -1304,7 +1342,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 H2; eauto. + eelim H3; 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. @@ -1340,13 +1378,15 @@ Inductive extcall_annot_sem (text: ident) (targs: list annot_arg) (F V: Type) (g Lemma extcall_annot_ok: forall text targs, - extcall_properties (extcall_annot_sem text targs) (mksignature (annot_args_typ targs) None cc_default). + extcall_properties (extcall_annot_sem text targs) + (mksignature (annot_args_typ targs) None cc_default) + nil. Proof. intros; constructor; intros. (* well typed *) inv H. simpl. auto. (* symbols *) - inv H1. econstructor; eauto. + inv H2. econstructor; eauto. eapply eventval_list_match_preserved; eauto. (* valid blocks *) inv H; auto. @@ -1360,7 +1400,7 @@ Proof. econstructor; eauto. eapply eventval_list_match_lessdef; eauto. (* mem injects *) - inv H0. + inv H1. exists f; exists Vundef; exists m1'; intuition. econstructor; eauto. eapply eventval_list_match_inject; eauto. @@ -1384,13 +1424,15 @@ Inductive extcall_annot_val_sem (text: ident) (targ: typ) (F V: Type) (ge: Genv. Lemma extcall_annot_val_ok: forall text targ, - extcall_properties (extcall_annot_val_sem text targ) (mksignature (targ :: nil) (Some targ) cc_default). + extcall_properties (extcall_annot_val_sem text targ) + (mksignature (targ :: nil) (Some targ) cc_default) + nil. Proof. intros; constructor; intros. (* well typed *) inv H. unfold proj_sig_res; simpl. eapply eventval_match_type; eauto. (* symbols *) - inv H1. econstructor; eauto. + inv H2. econstructor; eauto. eapply eventval_match_preserved; eauto. (* valid blocks *) inv H; auto. @@ -1404,7 +1446,7 @@ Proof. econstructor; eauto. eapply eventval_match_lessdef; eauto. (* mem inject *) - inv H0. inv H2. inv H7. + inv H1. inv H3. inv H8. exists f; exists v'; exists m1'; intuition. econstructor; eauto. eapply eventval_match_inject; eauto. @@ -1429,14 +1471,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. + forall id sg, extcall_properties (external_functions_sem id sg) sg nil. (** We treat inline assembly similarly. *) Parameter inline_assembly_sem: ident -> extcall_sem. Axiom inline_assembly_properties: - forall id, extcall_properties (inline_assembly_sem id) (mksignature nil None cc_default). + forall id, extcall_properties (inline_assembly_sem id) (mksignature nil None cc_default) nil. (** ** Combined semantics of external calls *) @@ -1469,9 +1511,9 @@ Definition external_call (ef: external_function): extcall_sem := Theorem external_call_spec: forall ef, - extcall_properties (external_call ef) (ef_sig ef). + extcall_properties (external_call ef) (ef_sig ef) (globals_external ef). Proof. - intros. unfold external_call, ef_sig. destruct ef. + intros. unfold external_call, ef_sig, globals_external; destruct ef. apply external_functions_properties. apply external_functions_properties. apply volatile_load_ok. @@ -1492,7 +1534,7 @@ Definition external_call_valid_block ef := ec_valid_block (external_call_spec ef Definition external_call_max_perm ef := ec_max_perm (external_call_spec ef). Definition external_call_readonly ef := ec_readonly (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_mem_inject_gen ef := ec_mem_inject (external_call_spec ef). Definition external_call_trace_length ef := ec_trace_length (external_call_spec ef). Definition external_call_receptive ef := ec_receptive (external_call_spec ef). Definition external_call_determ ef := ec_determ (external_call_spec ef). @@ -1503,11 +1545,12 @@ Lemma external_call_symbols_preserved: 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 id, Genv.public_symbol ge2 id = Genv.public_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. + intros. unfold block_is_volatile. rewrite H2. auto. Qed. Require Import Errors. @@ -1517,6 +1560,7 @@ Lemma external_call_symbols_preserved_2: (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 id, Genv.public_symbol ge2 id = Genv.public_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 -> @@ -1526,9 +1570,9 @@ Proof. 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. + exploit H2; 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. + exploit H3; eauto. intros [g1 [A B]]. congruence. auto. Qed. @@ -1545,6 +1589,40 @@ Proof. unfold Plt, Ple in *; zify; omega. Qed. +(** Special case of [external_call_mem_inject_gen] (for backward compatibility) *) + +Definition meminj_preserves_globals (F V: Type) (ge: Genv.t F V) (f: block -> option (block * Z)) : Prop := + (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 external_call_mem_inject: + forall ef F V (ge: Genv.t F V) vargs m1 t vres m2 f m1' vargs', + meminj_preserves_globals ge f -> + external_call ef ge vargs m1 t vres m2 -> + Mem.inject f m1 m1' -> + val_list_inject f vargs vargs' -> + exists f', exists vres', exists m2', + external_call ef ge vargs' m1' t vres' m2' + /\ val_inject f' vres vres' + /\ Mem.inject f' m2 m2' + /\ Mem.unchanged_on (loc_unmapped f) m1 m2 + /\ Mem.unchanged_on (loc_out_of_reach f m1) m1' m2' + /\ inject_incr f f' + /\ inject_separated f f' m1 m1'. +Proof. + intros. destruct H as (A & B & C). eapply external_call_mem_inject_gen; eauto. + 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. + + unfold block_is_volatile; simpl. + destruct (Genv.find_var_info ge b1) as [gv1|] eqn:V1. + * 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. +Qed. + (** Corollaries of [external_call_determ]. *) Lemma external_call_match_traces: @@ -1658,6 +1736,7 @@ Lemma external_call_symbols_preserved': 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 id, Genv.public_symbol ge2 id = Genv.public_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. diff --git a/common/Globalenvs.v b/common/Globalenvs.v index e4772e25..eb98e876 100644 --- a/common/Globalenvs.v +++ b/common/Globalenvs.v @@ -82,6 +82,7 @@ Variable V: Type. (**r The type of information attached to variables *) (** The type of global environments. *) Record t: Type := mkgenv { + genv_public: list ident; (**r which symbol names are public *) genv_symb: PTree.t block; (**r mapping symbol -> block *) genv_funs: PTree.t F; (**r mapping function pointer -> definition *) genv_vars: PTree.t (globvar V); (**r mapping variable pointer -> info *) @@ -112,6 +113,14 @@ Definition symbol_address (ge: t) (id: ident) (ofs: int) : val := | None => Vundef end. +(** [public_symbol ge id] says whether the name [id] is public and defined. *) + +Definition public_symbol (ge: t) (id: ident) : bool := + match find_symbol ge id with + | None => false + | Some _ => In_dec ident_eq id ge.(genv_public) + end. + (** [find_funct_ptr ge b] returns the function description associated with the given address. *) @@ -144,6 +153,7 @@ Definition find_var_info (ge: t) (b: block) : option (globvar V) := Program Definition add_global (ge: t) (idg: ident * globdef F V) : t := @mkgenv + ge.(genv_public) (PTree.set idg#1 ge.(genv_next) ge.(genv_symb)) (match idg#2 with | Gfun f => PTree.set ge.(genv_next) f ge.(genv_funs) @@ -208,8 +218,8 @@ Proof. induction gl1; simpl; intros. auto. rewrite IHgl1; auto. Qed. -Program Definition empty_genv : t := - @mkgenv (PTree.empty _) (PTree.empty _) (PTree.empty _) 1%positive _ _ _ _ _. +Program Definition empty_genv (pub: list ident): t := + @mkgenv pub (PTree.empty _) (PTree.empty _) (PTree.empty _) 1%positive _ _ _ _ _. Next Obligation. rewrite PTree.gempty in H. discriminate. Qed. @@ -227,7 +237,7 @@ Next Obligation. Qed. Definition globalenv (p: program F V) := - add_globals empty_genv p.(prog_defs). + add_globals (empty_genv p.(prog_public)) p.(prog_defs). (** Proof principles *) @@ -277,6 +287,14 @@ End GLOBALENV_PRINCIPLES. (** ** Properties of the operations over global environments *) +Theorem public_symbol_exists: + forall ge id, public_symbol ge id = true -> exists b, find_symbol ge id = Some b. +Proof. + unfold public_symbol; intros. destruct (find_symbol ge id) as [b|]. + exists b; auto. + discriminate. +Qed. + Theorem shift_symbol_address: forall ge id ofs n, symbol_address ge id (Int.add ofs n) = Val.add (symbol_address ge id ofs) (Vint n). @@ -486,6 +504,21 @@ Proof. rewrite IHgl. auto. Qed. +Remark genv_public_add_globals: + forall gl ge, + genv_public (add_globals ge gl) = genv_public ge. +Proof. + induction gl; simpl; intros. + auto. + rewrite IHgl; auto. +Qed. + +Theorem globalenv_public: + forall p, genv_public (globalenv p) = prog_public p. +Proof. + unfold globalenv; intros. rewrite genv_public_add_globals. auto. +Qed. + (** * Construction of the initial memory state *) Section INITMEM. @@ -1092,7 +1125,7 @@ Lemma init_mem_genv_next: forall p m, Proof. unfold init_mem; intros. exploit alloc_globals_nextblock; eauto. rewrite Mem.nextblock_empty. intro. - generalize (genv_next_add_globals (prog_defs p) empty_genv). + generalize (genv_next_add_globals (prog_defs p) (empty_genv (prog_public p))). fold (globalenv p). simpl genv_next. intros. congruence. Qed. @@ -1606,6 +1639,17 @@ Proof. intros. destruct globalenvs_match. unfold find_symbol. auto. Qed. +Theorem public_symbol_match: + forall (s : ident), + ~In s (map fst new_globs) -> + public_symbol (globalenv p') s = public_symbol (globalenv p) s. +Proof. + intros. unfold public_symbol. rewrite find_symbol_match by auto. + destruct (find_symbol (globalenv p) s); auto. + rewrite ! globalenv_public. + destruct progmatch as (P & Q & R). rewrite R. auto. +Qed. + Hypothesis new_ids_fresh : forall s', find_symbol (globalenv p) s' <> None -> ~In s' (map fst new_globs). @@ -1804,6 +1848,14 @@ Proof. intros. eapply find_symbol_match. eexact prog_match. auto. Qed. +Theorem public_symbol_transf_augment: + forall (s: ident), + ~ In s (map fst new_globs) -> + public_symbol (globalenv p') s = public_symbol (globalenv p) s. +Proof. + intros. eapply public_symbol_match. eexact prog_match. auto. +Qed. + Theorem init_mem_transf_augment: (forall s', find_symbol (globalenv p) s' <> None -> ~ In s' (map fst new_globs)) -> @@ -1910,6 +1962,14 @@ Proof. auto. Qed. +Theorem public_symbol_transf_partial2: + forall (s: ident), + public_symbol (globalenv p') s = public_symbol (globalenv p) s. +Proof. + pose proof (@public_symbol_transf_augment _ _ _ _ _ _ _ _ _ _ transf_augment_OK). + auto. +Qed. + Theorem init_mem_transf_partial2: forall m, init_mem p = Some m -> init_mem p' = Some m. Proof. @@ -1968,6 +2028,13 @@ Proof. exact (@find_symbol_transf_partial2 _ _ _ _ _ _ _ _ transf_OK). Qed. +Theorem public_symbol_transf_partial: + forall (s: ident), + public_symbol (globalenv p') s = public_symbol (globalenv p) s. +Proof. + exact (@public_symbol_transf_partial2 _ _ _ _ _ _ _ _ transf_OK). +Qed. + Theorem find_var_info_transf_partial: forall (b: block), find_var_info (globalenv p') b = find_var_info (globalenv p) b. @@ -2047,6 +2114,13 @@ Proof. exact (@find_symbol_transf_partial _ _ _ _ _ _ transf_OK). Qed. +Theorem public_symbol_transf: + forall (s: ident), + public_symbol (globalenv tp) s = public_symbol (globalenv p) s. +Proof. + exact (@public_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. diff --git a/common/Smallstep.v b/common/Smallstep.v index 02b18fc8..e74101b5 100644 --- a/common/Smallstep.v +++ b/common/Smallstep.v @@ -516,8 +516,8 @@ Record forward_simulation (L1 L2: semantics) : Type := exists i', exists s2', (Plus L2 s2 t s2' \/ (Star L2 s2 t s2' /\ fsim_order i' i)) /\ fsim_match_states i' s1' s2'; - fsim_symbols_preserved: - forall id, Genv.find_symbol (globalenv L2) id = Genv.find_symbol (globalenv L1) id + fsim_public_preserved: + forall id, Genv.public_symbol (globalenv L2) id = Genv.public_symbol (globalenv L1) id }. Implicit Arguments forward_simulation []. @@ -548,8 +548,8 @@ Section FORWARD_SIMU_DIAGRAMS. Variable L1: semantics. Variable L2: semantics. -Hypothesis symbols_preserved: - forall id, Genv.find_symbol (globalenv L2) id = Genv.find_symbol (globalenv L1) id. +Hypothesis public_preserved: + forall id, Genv.public_symbol (globalenv L2) id = Genv.public_symbol (globalenv L1) id. Variable match_states: state L1 -> state L2 -> Prop. @@ -809,7 +809,7 @@ Proof. right; split. subst t; apply star_refl. red. right. auto. exists s3; auto. (* symbols *) - intros. transitivity (Genv.find_symbol (globalenv L2) id); apply fsim_symbols_preserved; auto. + intros. transitivity (Genv.public_symbol (globalenv L2) id); apply fsim_public_preserved; auto. Qed. End COMPOSE_SIMULATIONS. @@ -927,8 +927,8 @@ Record backward_simulation (L1 L2: semantics) : Type := exists i', exists s1', (Plus L1 s1 t s1' \/ (Star L1 s1 t s1' /\ bsim_order i' i)) /\ bsim_match_states i' s1' s2'; - bsim_symbols_preserved: - forall id, Genv.find_symbol (globalenv L2) id = Genv.find_symbol (globalenv L1) id + bsim_public_preserved: + forall id, Genv.public_symbol (globalenv L2) id = Genv.public_symbol (globalenv L1) id }. (** An alternate form of the simulation diagram *) @@ -957,8 +957,8 @@ Section BACKWARD_SIMU_DIAGRAMS. Variable L1: semantics. Variable L2: semantics. -Hypothesis symbols_preserved: - forall id, Genv.find_symbol (globalenv L2) id = Genv.find_symbol (globalenv L1) id. +Hypothesis public_preserved: + forall id, Genv.public_symbol (globalenv L2) id = Genv.public_symbol (globalenv L1) id. Variable match_states: state L1 -> state L2 -> Prop. @@ -1201,7 +1201,7 @@ Proof. (* simulation *) exact bb_simulation. (* symbols *) - intros. transitivity (Genv.find_symbol (globalenv L2) id); apply bsim_symbols_preserved; auto. + intros. transitivity (Genv.public_symbol (globalenv L2) id); apply bsim_public_preserved; auto. Qed. End COMPOSE_BACKWARD_SIMULATIONS. @@ -1298,7 +1298,7 @@ Proof. subst. inv H1. elim H2; auto. right; intuition. eapply match_traces_preserved with (ge1 := (globalenv L2)); auto. - intros; symmetry; apply (fsim_symbols_preserved FS). + intros; symmetry; apply (fsim_public_preserved FS). Qed. Lemma f2b_determinacy_star: @@ -1492,7 +1492,7 @@ Proof. (* simulation *) exact f2b_simulation_step. (* symbols preserved *) - exact (fsim_symbols_preserved FS). + exact (fsim_public_preserved FS). Qed. End FORWARD_TO_BACKWARD. @@ -1614,7 +1614,7 @@ Proof. (* simulation *) exact ffs_simulation. (* symbols preserved *) - simpl. exact (fsim_symbols_preserved sim). + simpl. exact (fsim_public_preserved sim). Qed. End FACTOR_FORWARD_SIMULATION. @@ -1711,7 +1711,7 @@ Proof. (* simulation *) exact fbs_simulation. (* symbols *) - simpl. exact (bsim_symbols_preserved sim). + simpl. exact (bsim_public_preserved sim). Qed. End FACTOR_BACKWARD_SIMULATION. -- cgit