From 7999c9ee1f09f7d555e3efc39f030564f76a3354 Mon Sep 17 00:00:00 2001 From: xleroy Date: Mon, 10 May 2010 15:35:02 +0000 Subject: - Extended traces so that pointers within globals are supported as event values. - Revised handling of volatile reads: the execution environment dictates the value read, via the trace of events. git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1345 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e --- cfrontend/Cminorgenproof.v | 133 +++++++++++++++++++++++---------------------- 1 file changed, 69 insertions(+), 64 deletions(-) (limited to 'cfrontend/Cminorgenproof.v') diff --git a/cfrontend/Cminorgenproof.v b/cfrontend/Cminorgenproof.v index 19e13cbe..9f572edb 100644 --- a/cfrontend/Cminorgenproof.v +++ b/cfrontend/Cminorgenproof.v @@ -481,19 +481,6 @@ Record match_env (f: meminj) (cenv: compilenv) Hint Resolve me_low_high. -(** Global environments match if the memory injection [f] leaves unchanged - the references to global symbols and functions. *) - -Record match_globalenvs (f: meminj) : Prop := - mk_match_globalenvs { - mg_symbols: - forall id b, - Genv.find_symbol ge id = Some b -> - f b = Some (b, 0) /\ Genv.find_symbol tge id = Some b; - mg_functions: - forall b, b < 0 -> f b = Some(b, 0) - }. - (** The remainder of this section is devoted to showing preservation of the [match_en] invariant under various assignments and memory stores. First: preservation by memory stores to ``mapped'' blocks @@ -804,6 +791,16 @@ Inductive frame : Type := Definition callstack : Type := list frame. +(** Global environments match if the memory injection [f] leaves unchanged + the references to global symbols and functions. *) + +Inductive match_globalenvs (f: meminj) (bound: Z): Prop := + | mk_match_globalenvs + (POS: bound > 0) + (DOMAIN: forall b, b < bound -> f b = Some(b, 0)) + (IMAGE: forall b1 b2 delta, f b1 = Some(b2, delta) -> b2 < bound -> b1 = b2) + (SYMBOLS: forall id b, Genv.find_symbol ge id = Some b -> b < bound). + (** Matching of call stacks imply: - matching of environments for each of the frames - matching of the global environments @@ -824,8 +821,9 @@ Definition padding_freeable (f: meminj) (m: mem) (tm: mem) (sp: block) (sz: Z) : Inductive match_callstack (f: meminj) (m: mem) (tm: mem): callstack -> Z -> Z -> Prop := | mcs_nil: - forall bound tbound, - match_globalenvs f -> + forall hi bound tbound, + match_globalenvs f hi -> + hi <= bound -> hi <= tbound -> match_callstack f m tm nil bound tbound | mcs_cons: forall cenv tf e te sp lo hi cs bound tbound @@ -841,7 +839,7 @@ Inductive match_callstack (f: meminj) (m: mem) (tm: mem): Lemma match_callstack_match_globalenvs: forall f m tm cs bound tbound, match_callstack f m tm cs bound tbound -> - match_globalenvs f. + exists hi, match_globalenvs f hi. Proof. induction 1; eauto. Qed. @@ -878,7 +876,7 @@ Lemma match_callstack_store_mapped: match_callstack f m' tm' cs lo hi. Proof. induction 4. - constructor; auto. + econstructor; eauto. constructor; auto. eapply match_env_store_mapped; eauto. congruence. eapply padding_freeable_invariant; eauto. @@ -915,7 +913,7 @@ Lemma match_callstack_invariant: match_callstack f m' tm' cs bound tbound. Proof. induction 1; intros. - constructor; auto. + econstructor; eauto. constructor; auto. eapply padding_freeable_invariant; eauto. intros. apply H1. omega. @@ -973,7 +971,9 @@ Lemma match_callstack_incr_bound: bound <= bound' -> tbound <= tbound' -> match_callstack f m tm cs bound' tbound'. Proof. - intros. inversion H; constructor; auto. omega. omega. + intros. inv H. + econstructor; eauto. omega. omega. + constructor; auto. omega. omega. Qed. (** Preservation of [match_callstack] by freeing all blocks allocated @@ -1075,13 +1075,10 @@ Lemma match_callstack_alloc_below: match_callstack f2 m2 tm cs bound tbound. Proof. induction 4; intros. - constructor. - inv H2. constructor. - intros. exploit mg_symbols0; eauto. intros [A B]. auto. - intros. rewrite H1; auto. - exploit Mem.alloc_result; eauto. - generalize (Mem.nextblock_pos m1). - unfold block; omega. + apply mcs_nil with hi; auto. + inv H2. constructor; auto. + intros. destruct (eq_block b1 b). subst. rewrite H2 in H6. omegaContradiction. + rewrite H1 in H2; eauto. constructor; auto. eapply match_env_alloc_other; eauto. omega. destruct (f2 b); auto. destruct p; omega. eapply padding_freeable_invariant; eauto. @@ -1223,15 +1220,15 @@ Proof. intros until m2'. intros UNMAPPED OUTOFREACH INCR SEPARATED BOUNDS. destruct OUTOFREACH as [OUTOFREACH1 OUTOFREACH2]. - induction 1; intros; constructor. + induction 1; intros. (* base case *) - constructor; intros. - exploit mg_symbols; eauto. intros [A B]. auto. - replace (f2 b) with (f1 b). eapply mg_functions; eauto. - symmetry. eapply inject_incr_separated_same; eauto. - red. generalize (Mem.nextblock_pos m1); omega. + apply mcs_nil with hi; auto. + inv H. constructor; auto. + intros. case_eq (f1 b1). + intros [b2' delta'] EQ. rewrite (INCR _ _ _ EQ) in H. inv H. eauto. + intro EQ. exploit SEPARATED; eauto. intros [A B]. elim B. red. omega. (* inductive case *) - auto. auto. + constructor. auto. auto. eapply match_env_external_call; eauto. omega. omega. (* padding-freeable *) red; intros. @@ -1253,14 +1250,24 @@ Qed. Remark external_call_nextblock_incr: forall ef vargs m1 t vres m2, - external_call ef vargs m1 t vres m2 -> + external_call ef (Genv.find_symbol ge) vargs m1 t vres m2 -> Mem.nextblock m1 <= Mem.nextblock m2. Proof. intros. - generalize (external_call_valid_block _ _ _ _ _ _ (Mem.nextblock m1 - 1) H). + generalize (external_call_valid_block _ _ _ _ _ _ _ (Mem.nextblock m1 - 1) H). unfold Mem.valid_block. omega. Qed. +Remark inj_preserves_globals: + forall f hi, + match_globalenvs f hi -> + meminj_preserves_globals (Genv.find_symbol ge) f. +Proof. + intros. inv H. split; intros. + apply DOMAIN. eapply SYMBOLS. eauto. + symmetry. eapply IMAGE; eauto. +Qed. + (** * Soundness of chunk and type inference. *) Lemma load_normalized: @@ -1682,15 +1689,15 @@ Proof. auto. (* var_global_scalar *) simpl in *. - assert (match_globalenvs f). eapply match_callstack_match_globalenvs; eauto. - inv H2. exploit mg_symbols0; eauto. intros [A B]. + exploit match_callstack_match_globalenvs; eauto. intros [bnd MG]. inv MG. assert (chunk0 = chunk). congruence. subst chunk0. assert (val_inject f (Vptr b Int.zero) (Vptr b Int.zero)). - econstructor; eauto. + econstructor; eauto. exploit Mem.loadv_inject; eauto. simpl. eauto. intros [tv [LOAD INJ]]. exists tv; split. eapply eval_Eload; eauto. eapply make_globaladdr_correct; eauto. + rewrite symbols_preserved; auto. auto. Qed. @@ -1714,16 +1721,14 @@ Proof. exists (Vptr sp (Int.repr ofs)); split. eapply make_stackaddr_correct. congruence. (* var_global_scalar *) - assert (match_globalenvs f). eapply match_callstack_match_globalenvs; eauto. - inv H1. exploit mg_symbols0; eauto. intros [A B]. + exploit match_callstack_match_globalenvs; eauto. intros [bnd MG]. inv MG. exists (Vptr b Int.zero); split. - eapply make_globaladdr_correct. eauto. + eapply make_globaladdr_correct; eauto. rewrite symbols_preserved; auto. econstructor; eauto. (* var_global_array *) - assert (match_globalenvs f). eapply match_callstack_match_globalenvs; eauto. - inv H1. exploit mg_symbols0; eauto. intros [A B]. + exploit match_callstack_match_globalenvs; eauto. intros [bnd MG]. inv MG. exists (Vptr b Int.zero); split. - eapply make_globaladdr_correct. eauto. + eapply make_globaladdr_correct; eauto. rewrite symbols_preserved; auto. econstructor; eauto. Qed. @@ -1791,11 +1796,10 @@ Proof. simpl in *. assert (chunk0 = chunk) by congruence. subst chunk0. assert (Mem.storev chunk m (Vptr b Int.zero) v = Some m'). assumption. - assert (match_globalenvs f). eapply match_callstack_match_globalenvs; eauto. - exploit mg_symbols; eauto. intros [A B]. + exploit match_callstack_match_globalenvs; eauto. intros [bnd MG]. inv MG. exploit make_store_correct. eapply make_globaladdr_correct; eauto. - eauto. eauto. eauto. eauto. eauto. + rewrite symbols_preserved; eauto. eauto. eauto. eauto. eauto. auto. intros [tm' [tvrhs' [EVAL' [STORE' TNEXTBLOCK]]]]. exists te; exists tm'. split. eauto. split. auto. @@ -1874,11 +1878,10 @@ Proof. simpl in *. assert (chunk0 = chunk) by congruence. subst chunk0. assert (Mem.storev chunk m (Vptr b Int.zero) v = Some m'). assumption. - assert (match_globalenvs f). eapply match_callstack_match_globalenvs; eauto. - exploit mg_symbols; eauto. intros [A B]. + exploit match_callstack_match_globalenvs; eauto. intros [bnd MG]. inv MG. exploit make_store_correct. eapply make_globaladdr_correct; eauto. - eauto. eauto. eauto. eauto. eauto. + rewrite symbols_preserved; eauto. eauto. eauto. eauto. eauto. eauto. intros [tm' [tvrhs' [EVAL' [STORE' MEMINJ]]]]. exists te'; exists tm'. split. eauto. split. auto. @@ -2601,16 +2604,16 @@ Inductive match_states: Csharpminor.state -> Cminor.state -> Prop := (Returnstate tv tk tm). Remark val_inject_function_pointer: - forall v fd f tv, + forall bound v fd f tv, Genv.find_funct tge v = Some fd -> - match_globalenvs f -> + match_globalenvs f bound -> val_inject f v tv -> tv = v. Proof. intros. exploit Genv.find_funct_inv; eauto. intros [b EQ]. subst v. rewrite Genv.find_funct_find_funct_ptr in H. assert (b < 0). unfold tge in H. eapply Genv.find_funct_ptr_negative; eauto. - assert (f b = Some(b, 0)). eapply mg_functions; eauto. + assert (f b = Some(b, 0)). inv H0. apply DOMAIN. omega. inv H1. rewrite H3 in H6; inv H6. reflexivity. Qed. @@ -3000,8 +3003,8 @@ Proof. exploit transl_expr_correct; eauto. intros [tvf [EVAL1 VINJ1]]. assert (tvf = vf). + exploit match_callstack_match_globalenvs; eauto. intros [bnd MG]. eapply val_inject_function_pointer; eauto. - eapply match_callstack_match_globalenvs; eauto. subst tvf. exploit transl_exprlist_correct; eauto. intros [tvargs [EVAL2 VINJ2]]. @@ -3020,8 +3023,8 @@ Proof. exploit transl_expr_correct; eauto. intros [tvf [EVAL1 VINJ1]]. assert (tvf = vf). + exploit match_callstack_match_globalenvs; eauto. intros [bnd MG]. eapply val_inject_function_pointer; eauto. - eapply match_callstack_match_globalenvs; eauto. subst tvf. exploit transl_exprlist_correct; eauto. intros [tvargs [EVAL2 VINJ2]]. @@ -3167,10 +3170,13 @@ Proof. (* external call *) monadInv TR. + exploit match_callstack_match_globalenvs; eauto. intros [hi MG]. exploit external_call_mem_inject; eauto. + eapply inj_preserves_globals; eauto. intros [f' [vres' [tm' [EC [VINJ [MINJ' [UNMAPPED [OUTOFREACH [INCR SEPARATED]]]]]]]]]. left; econstructor; split. - apply plus_one. econstructor; eauto. + apply plus_one. econstructor. + eapply external_call_symbols_preserved; eauto. exact symbols_preserved. econstructor; eauto. apply match_callstack_incr_bound with (Mem.nextblock m) (Mem.nextblock tm). eapply match_callstack_external_call; eauto. @@ -3202,15 +3208,14 @@ Qed. Lemma match_globalenvs_init: forall m, Genv.init_mem prog = Some m -> - match_globalenvs (Mem.flat_inj (Mem.nextblock m)). + match_globalenvs (Mem.flat_inj (Mem.nextblock m)) (Mem.nextblock m). Proof. intros. constructor. - intros. split. - unfold Mem.flat_inj. rewrite zlt_true. auto. - eapply Genv.find_symbol_not_fresh; eauto. - rewrite <- H0. apply symbols_preserved. - intros. unfold Mem.flat_inj. rewrite zlt_true. auto. - generalize (Mem.nextblock_pos m). omega. + apply Mem.nextblock_pos. + intros. unfold Mem.flat_inj. apply zlt_true; auto. + intros. unfold Mem.flat_inj in H0. + destruct (zlt b1 (Mem.nextblock m)); congruence. + intros. eapply Genv.find_symbol_not_fresh; eauto. Qed. Lemma transl_initial_states: @@ -3231,7 +3236,7 @@ Proof. eapply match_callstate with (f := Mem.flat_inj (Mem.nextblock m0)) (cs := @nil frame). auto. eapply Genv.initmem_inject; eauto. - constructor. apply match_globalenvs_init. auto. + apply mcs_nil with (Mem.nextblock m0). apply match_globalenvs_init; auto. omega. omega. instantiate (1 := gce). constructor. red; auto. constructor. rewrite H2; simpl; auto. Qed. -- cgit