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 --- arm/Asm.v | 2 +- arm/Asmgenproof.v | 17 +- backend/Allocproof.v | 1 + backend/CSEproof.v | 1 + backend/Cminor.v | 4 +- backend/CminorSel.v | 2 +- backend/Constpropproof.v | 1 + backend/LTL.v | 2 +- backend/LTLin.v | 2 +- backend/Linear.v | 2 +- backend/Linearizeproof.v | 1 + backend/Machabstr.v | 2 +- backend/Machabstr2concr.v | 12 +- backend/Machconcr.v | 2 +- backend/Machtyping.v | 2 +- backend/RTL.v | 2 +- backend/RTLgenproof.v | 1 + backend/Reloadproof.v | 1 + backend/Selectionproof.v | 4 + backend/Stackingproof.v | 1 + backend/Tailcallproof.v | 1 + backend/Tunnelingproof.v | 1 + cfrontend/Cminorgenproof.v | 133 +++++------ cfrontend/Csem.v | 4 +- cfrontend/Csharpminor.v | 2 +- cfrontend/Cshmgenproof3.v | 1 + common/Determinism.v | 34 ++- common/Events.v | 541 +++++++++++++++++++++++++++------------------ common/Globalenvs.v | 70 +++--- driver/Complements.v | 4 +- powerpc/Asm.v | 2 +- powerpc/Asmgenproof.v | 3 +- 32 files changed, 507 insertions(+), 351 deletions(-) diff --git a/arm/Asm.v b/arm/Asm.v index 13c2e57b..7a3fe208 100644 --- a/arm/Asm.v +++ b/arm/Asm.v @@ -616,7 +616,7 @@ Inductive step: state -> trace -> state -> Prop := forall b ef args res rs m t rs' m', rs PC = Vptr b Int.zero -> Genv.find_funct_ptr ge b = Some (External ef) -> - external_call ef args m t res m' -> + external_call ef (Genv.find_symbol ge) args m t res m' -> extcall_arguments rs m ef.(ef_sig) args -> rs' = (rs#(loc_external_result ef.(ef_sig)) <- res #PC <- (rs IR14)) -> diff --git a/arm/Asmgenproof.v b/arm/Asmgenproof.v index eec0c655..0a1180c6 100644 --- a/arm/Asmgenproof.v +++ b/arm/Asmgenproof.v @@ -1130,14 +1130,25 @@ Proof. econstructor; eauto with coqlib. Qed. -Lemma exec_function_external_prop: forall (s : list stackframe) (fb : block) (ms : Mach.regset) (m : mem) (t0 : trace) (ms' : RegEq.t -> val) (ef : external_function) (args : list val) (res : val) (m': mem), Genv.find_funct_ptr ge fb = Some (External ef) -> external_call ef args m t0 res m' -> Machconcr.extcall_arguments ms m (parent_sp s) (ef_sig ef) args -> ms' = Regmap.set (Conventions.loc_result (ef_sig ef)) res ms -> exec_instr_prop (Machconcr.Callstate s fb ms m) t0 (Machconcr.Returnstate s ms' m'). Proof. +Lemma exec_function_external_prop: + forall (s : list stackframe) (fb : block) (ms : Mach.regset) + (m : mem) (t0 : trace) (ms' : RegEq.t -> val) + (ef : external_function) (args : list val) (res : val) (m': mem), + Genv.find_funct_ptr ge fb = Some (External ef) -> + external_call ef (Genv.find_symbol ge) args m t0 res m' -> + Machconcr.extcall_arguments ms m (parent_sp s) (ef_sig ef) args -> + ms' = Regmap.set (Conventions.loc_result (ef_sig ef)) res ms -> + exec_instr_prop (Machconcr.Callstate s fb ms m) + t0 (Machconcr.Returnstate s ms' m'). +Proof. intros; red; intros; inv MS. exploit functions_translated; eauto. intros [tf [A B]]. simpl in B. inv B. left; exists (State (rs#(loc_external_result (ef_sig ef)) <- res #PC <- (rs IR14)) m'); split. - apply plus_one. eapply exec_step_external; eauto. - eauto. eapply extcall_arguments_match; eauto. + apply plus_one. eapply exec_step_external; eauto. + eapply external_call_symbols_preserved; eauto. exact symbols_preserved. + eapply extcall_arguments_match; eauto. econstructor; eauto. unfold loc_external_result. auto with ppcgen. Qed. diff --git a/backend/Allocproof.v b/backend/Allocproof.v index 3f526aa4..b845323f 100644 --- a/backend/Allocproof.v +++ b/backend/Allocproof.v @@ -717,6 +717,7 @@ Proof. injection H7; intro EQ; inv EQ. econstructor; split. eapply exec_function_external; eauto. + eapply external_call_symbols_preserved; eauto. exact symbols_preserved. eapply match_states_return; eauto. (* return *) diff --git a/backend/CSEproof.v b/backend/CSEproof.v index fcc867af..ce577aca 100644 --- a/backend/CSEproof.v +++ b/backend/CSEproof.v @@ -935,6 +935,7 @@ Proof. (* external function *) simpl. econstructor; split. eapply exec_function_external; eauto. + eapply external_call_symbols_preserved; eauto. exact symbols_preserved. econstructor; eauto. (* return *) diff --git a/backend/Cminor.v b/backend/Cminor.v index f2f03c5d..cc4afa50 100644 --- a/backend/Cminor.v +++ b/backend/Cminor.v @@ -496,7 +496,7 @@ Inductive step: state -> trace -> state -> Prop := step (Callstate (Internal f) vargs k m) E0 (State f f.(fn_body) k (Vptr sp Int.zero) e m') | step_external_function: forall ef vargs k m t vres m', - external_call ef vargs m t vres m' -> + external_call ef (Genv.find_symbol ge) vargs m t vres m' -> step (Callstate (External ef) vargs k m) t (Returnstate vres k m') @@ -595,7 +595,7 @@ Inductive eval_funcall: eval_funcall m (Internal f) vargs t m3 vres | eval_funcall_external: forall ef m args t res m', - external_call ef args m t res m' -> + external_call ef (Genv.find_symbol ge) args m t res m' -> eval_funcall m (External ef) args t m' res (** Execution of a statement: [exec_stmt ge f sp e m s t e' m' out] diff --git a/backend/CminorSel.v b/backend/CminorSel.v index 231af8fb..65dd4dec 100644 --- a/backend/CminorSel.v +++ b/backend/CminorSel.v @@ -354,7 +354,7 @@ Inductive step: state -> trace -> state -> Prop := step (Callstate (Internal f) vargs k m) E0 (State f f.(fn_body) k (Vptr sp Int.zero) e m') | step_external_function: forall ef vargs k m t vres m', - external_call ef vargs m t vres m' -> + external_call ef (Genv.find_symbol ge) vargs m t vres m' -> step (Callstate (External ef) vargs k m) t (Returnstate vres k m') diff --git a/backend/Constpropproof.v b/backend/Constpropproof.v index 6671960c..b5c3b1e3 100644 --- a/backend/Constpropproof.v +++ b/backend/Constpropproof.v @@ -415,6 +415,7 @@ Proof. (* external function *) simpl. econstructor; split. eapply exec_function_external; eauto. + eapply external_call_symbols_preserved; eauto. exact symbols_preserved. constructor; auto. (* return *) diff --git a/backend/LTL.v b/backend/LTL.v index 2a1172ab..4aa8afc5 100644 --- a/backend/LTL.v +++ b/backend/LTL.v @@ -228,7 +228,7 @@ Inductive step: state -> trace -> state -> Prop := E0 (State s f (Vptr stk Int.zero) f.(fn_entrypoint) (init_locs args f.(fn_params)) m') | exec_function_external: forall s ef t args res m m', - external_call ef args m t res m' -> + external_call ef (Genv.find_symbol ge) args m t res m' -> step (Callstate s (External ef) args m) t (Returnstate s res m') | exec_return: diff --git a/backend/LTLin.v b/backend/LTLin.v index c3b432ba..64017c30 100644 --- a/backend/LTLin.v +++ b/backend/LTLin.v @@ -225,7 +225,7 @@ Inductive step: state -> trace -> state -> Prop := E0 (State s f (Vptr stk Int.zero) f.(fn_code) (init_locs args f.(fn_params)) m') | exec_function_external: forall s ef args t res m m', - external_call ef args m t res m' -> + external_call ef (Genv.find_symbol ge) args m t res m' -> step (Callstate s (External ef) args m) t (Returnstate s res m') | exec_return: diff --git a/backend/Linear.v b/backend/Linear.v index be07b827..7d21651d 100644 --- a/backend/Linear.v +++ b/backend/Linear.v @@ -314,7 +314,7 @@ Inductive step: state -> trace -> state -> Prop := E0 (State s f (Vptr stk Int.zero) f.(fn_code) (call_regs rs) m') | exec_function_external: forall s ef args res rs1 rs2 m t m', - external_call ef args m t res m' -> + external_call ef (Genv.find_symbol ge) args m t res m' -> args = List.map rs1 (Conventions.loc_arguments ef.(ef_sig)) -> rs2 = Locmap.set (R (Conventions.loc_result ef.(ef_sig))) res rs1 -> step (Callstate s (External ef) rs1 m) diff --git a/backend/Linearizeproof.v b/backend/Linearizeproof.v index 5d670650..fcb1acfb 100644 --- a/backend/Linearizeproof.v +++ b/backend/Linearizeproof.v @@ -684,6 +684,7 @@ Proof. (* external function *) monadInv H6. econstructor; split. apply plus_one. eapply exec_function_external; eauto. + eapply external_call_symbols_preserved; eauto. exact symbols_preserved. econstructor; eauto. (* return *) diff --git a/backend/Machabstr.v b/backend/Machabstr.v index ceaf9a68..bbc7e7d8 100644 --- a/backend/Machabstr.v +++ b/backend/Machabstr.v @@ -303,7 +303,7 @@ Inductive step: state -> trace -> state -> Prop := f.(fn_code) rs empty_frame m') | exec_function_external: forall s ef args res rs1 rs2 m t m', - external_call ef args m t res m' -> + external_call ef (Genv.find_symbol ge) args m t res m' -> extcall_arguments (parent_function s) rs1 (parent_frame s) ef.(ef_sig) args -> rs2 = (rs1#(Conventions.loc_result ef.(ef_sig)) <- res) -> step (Callstate s (External ef) rs1 m) diff --git a/backend/Machabstr2concr.v b/backend/Machabstr2concr.v index b766ed0d..b8232971 100644 --- a/backend/Machabstr2concr.v +++ b/backend/Machabstr2concr.v @@ -407,12 +407,12 @@ Qed. (** [frame_match] is preserved by external calls. *) Lemma frame_match_external_call: - forall fr sp base mm ms mm' ms' ef vargs vres t vargs' vres', + forall symb fr sp base mm ms mm' ms' ef vargs vres t vargs' vres', frame_match fr sp base mm ms -> Mem.extends mm ms -> - external_call ef vargs mm t vres mm' -> + external_call ef symb vargs mm t vres mm' -> Mem.extends mm' ms' -> - external_call ef vargs' ms t vres' ms' -> + external_call ef symb vargs' ms t vres' ms' -> mem_unchanged_on (loc_out_of_bounds mm) ms ms' -> frame_match fr sp base mm' ms'. Proof. @@ -420,7 +420,7 @@ Proof. eapply external_call_valid_block; eauto. eapply external_call_valid_block; eauto. auto. - rewrite (external_call_bounds _ _ _ _ _ _ _ H1); auto. + rewrite (external_call_bounds _ _ _ _ _ _ _ _ H1); auto. red; intros. apply A; auto. red. omega. intros. exploit fm_contents_match0; eauto. intros [v [C D]]. exists v; split; auto. @@ -814,9 +814,9 @@ Lemma match_stacks_external_call: match_stacks s ts mm ms -> forall ef vargs t vres mm' ms' vargs' vres', Mem.extends mm ms -> - external_call ef vargs mm t vres mm' -> + external_call ef (Genv.find_symbol ge) vargs mm t vres mm' -> Mem.extends mm' ms' -> - external_call ef vargs' ms t vres' ms' -> + external_call ef (Genv.find_symbol ge) vargs' ms t vres' ms' -> mem_unchanged_on (loc_out_of_bounds mm) ms ms' -> match_stacks s ts mm' ms'. Proof. diff --git a/backend/Machconcr.v b/backend/Machconcr.v index a6be4bc2..90d08f1f 100644 --- a/backend/Machconcr.v +++ b/backend/Machconcr.v @@ -233,7 +233,7 @@ Inductive step: state -> trace -> state -> Prop := | exec_function_external: forall s fb rs m t rs' ef args res m', Genv.find_funct_ptr ge fb = Some (External ef) -> - external_call ef args m t res m' -> + external_call ef (Genv.find_symbol ge) args m t res m' -> extcall_arguments rs m (parent_sp s) ef.(ef_sig) args -> rs' = (rs#(Conventions.loc_result ef.(ef_sig)) <- res) -> step (Callstate s fb rs m) diff --git a/backend/Machtyping.v b/backend/Machtyping.v index c2e797ae..b0673ca8 100644 --- a/backend/Machtyping.v +++ b/backend/Machtyping.v @@ -285,7 +285,7 @@ Proof. apply wt_empty_frame. econstructor; eauto. apply wt_setreg; auto. - generalize (external_call_well_typed _ _ _ _ _ _ H). + generalize (external_call_well_typed _ _ _ _ _ _ _ H). unfold proj_sig_res, Conventions.loc_result. destruct (sig_res (ef_sig ef)). destruct t0; simpl; auto. diff --git a/backend/RTL.v b/backend/RTL.v index c5d4d7d0..c8220e5d 100644 --- a/backend/RTL.v +++ b/backend/RTL.v @@ -282,7 +282,7 @@ Inductive step: state -> trace -> state -> Prop := m') | exec_function_external: forall s ef args res t m m', - external_call ef args m t res m' -> + external_call ef (Genv.find_symbol ge) args m t res m' -> step (Callstate s (External ef) args m) t (Returnstate s res m') | exec_return: diff --git a/backend/RTLgenproof.v b/backend/RTLgenproof.v index a15095bd..92f4cc91 100644 --- a/backend/RTLgenproof.v +++ b/backend/RTLgenproof.v @@ -1320,6 +1320,7 @@ Proof. monadInv TF. econstructor; split. left; apply plus_one. eapply exec_function_external; eauto. + eapply external_call_symbols_preserved; eauto. exact symbols_preserved. constructor; auto. (* return *) diff --git a/backend/Reloadproof.v b/backend/Reloadproof.v index bf728fae..1fa000c9 100644 --- a/backend/Reloadproof.v +++ b/backend/Reloadproof.v @@ -1310,6 +1310,7 @@ Proof. intros [res' [tm' [A [B [C D]]]]]. left; econstructor; split. apply plus_one. eapply exec_function_external; eauto. + eapply external_call_symbols_preserved; eauto. exact symbols_preserved. econstructor; eauto. simpl. rewrite Locmap.gss. auto. intros. rewrite Locmap.gso. auto. diff --git a/backend/Selectionproof.v b/backend/Selectionproof.v index 1da7884e..0d1a1ee7 100644 --- a/backend/Selectionproof.v +++ b/backend/Selectionproof.v @@ -469,6 +469,10 @@ Proof. econstructor. simpl. rewrite call_cont_commut. rewrite find_label_commut. rewrite H. simpl. reflexivity. constructor; auto. + (* external call *) + econstructor; split. + econstructor. eapply external_call_symbols_preserved; eauto. exact symbols_preserved. + constructor; auto. Qed. Lemma sel_initial_states: diff --git a/backend/Stackingproof.v b/backend/Stackingproof.v index f44eac2e..fbe4b68f 100644 --- a/backend/Stackingproof.v +++ b/backend/Stackingproof.v @@ -1574,6 +1574,7 @@ Proof. exploit transl_external_arguments; eauto. intro EXTARGS. econstructor; split. apply plus_one. eapply exec_function_external; eauto. + eapply external_call_symbols_preserved; eauto. exact symbols_preserved. econstructor; eauto. intros. unfold Regmap.set. case (RegEq.eq r (loc_result (ef_sig ef))); intro. rewrite e. rewrite Locmap.gss; auto. rewrite Locmap.gso; auto. diff --git a/backend/Tailcallproof.v b/backend/Tailcallproof.v index 0ca4c028..0535cbfb 100644 --- a/backend/Tailcallproof.v +++ b/backend/Tailcallproof.v @@ -557,6 +557,7 @@ Proof. intros [res' [m2' [A [B [C D]]]]]. left. exists (Returnstate s' res' m2'); split. simpl. econstructor; eauto. + eapply external_call_symbols_preserved; eauto. exact symbols_preserved. constructor; auto. (* returnstate *) diff --git a/backend/Tunnelingproof.v b/backend/Tunnelingproof.v index 4cbcbd4f..3f0a27d0 100644 --- a/backend/Tunnelingproof.v +++ b/backend/Tunnelingproof.v @@ -335,6 +335,7 @@ Proof. (* external function *) simpl. left; econstructor; split. eapply exec_function_external; eauto. + eapply external_call_symbols_preserved; eauto. exact symbols_preserved. simpl. econstructor; eauto. (* return *) inv H3. inv H1. 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. diff --git a/cfrontend/Csem.v b/cfrontend/Csem.v index 5f8bbf14..4e4c3795 100644 --- a/cfrontend/Csem.v +++ b/cfrontend/Csem.v @@ -901,7 +901,7 @@ Inductive step: state -> trace -> state -> Prop := E0 (State f f.(fn_body) k e m2) | step_external_function: forall id targs tres vargs k m vres t m', - external_call (external_function id targs tres) vargs m t vres m' -> + external_call (external_function id targs tres) (Genv.find_symbol ge) vargs m t vres m' -> step (Callstate (External id targs tres) vargs k m) t (Returnstate vres k m') @@ -1106,7 +1106,7 @@ with eval_funcall: mem -> fundef -> list val -> trace -> mem -> val -> Prop := Mem.free_list m3 (blocks_of_env e) = Some m4 -> eval_funcall m (Internal f) vargs t m4 vres | eval_funcall_external: forall m id targs tres vargs t vres m', - external_call (external_function id targs tres) vargs m t vres m' -> + external_call (external_function id targs tres) (Genv.find_symbol ge) vargs m t vres m' -> eval_funcall m (External id targs tres) vargs t m' vres. Scheme exec_stmt_ind2 := Minimality for exec_stmt Sort Prop diff --git a/cfrontend/Csharpminor.v b/cfrontend/Csharpminor.v index 2fddc6c2..4c61918d 100644 --- a/cfrontend/Csharpminor.v +++ b/cfrontend/Csharpminor.v @@ -516,7 +516,7 @@ Inductive step: state -> trace -> state -> Prop := E0 (State f f.(fn_body) k e m2) | step_external_function: forall ef vargs k m t vres m', - external_call ef vargs m t vres m' -> + external_call ef (Genv.find_symbol ge) vargs m t vres m' -> step (Callstate (External ef) vargs k m) t (Returnstate vres k m') diff --git a/cfrontend/Cshmgenproof3.v b/cfrontend/Cshmgenproof3.v index 7e3658b5..99450dee 100644 --- a/cfrontend/Cshmgenproof3.v +++ b/cfrontend/Cshmgenproof3.v @@ -1561,6 +1561,7 @@ Proof. exploit match_cont_is_call_cont; eauto. intros [A B]. econstructor; split. apply plus_one. constructor. eauto. + eapply external_call_symbols_preserved; eauto. exact symbols_preserved. econstructor; eauto. (* returnstate 0 *) diff --git a/common/Determinism.v b/common/Determinism.v index 862d5a58..02fb860a 100644 --- a/common/Determinism.v +++ b/common/Determinism.v @@ -45,11 +45,21 @@ Axiom traceinf_extensionality: the world to [w]. *) Inductive world: Type := - World: (ident -> list eventval -> option (eventval * world)) -> world. + World (io: ident -> list eventval -> option (eventval * world)) + (vload: memory_chunk -> ident -> int -> option (eventval * world)) + (vstore: memory_chunk -> ident -> int -> eventval -> option world). -Definition nextworld (w: world) (evname: ident) (evargs: list eventval) : +Definition nextworld_io (w: world) (evname: ident) (evargs: list eventval) : option (eventval * world) := - match w with World f => f evname evargs end. + match w with World io vl vs => io evname evargs end. + +Definition nextworld_vload (w: world) (chunk: memory_chunk) (id: ident) (ofs: int) : + option (eventval * world) := + match w with World io vl vs => vl chunk id ofs end. + +Definition nextworld_vstore (w: world) (chunk: memory_chunk) (id: ident) (ofs: int) (v: eventval): + option world := + match w with World io vl vs => vs chunk id ofs v end. (** A trace is possible in a given world if all events correspond to non-stuck external calls according to the given world. @@ -63,12 +73,14 @@ Definition nextworld (w: world) (evname: ident) (evargs: list eventval) : Inductive possible_event: world -> event -> world -> Prop := | possible_event_syscall: forall w1 evname evargs evres w2, - nextworld w1 evname evargs = Some (evres, w2) -> + nextworld_io w1 evname evargs = Some (evres, w2) -> possible_event w1 (Event_syscall evname evargs evres) w2 - | possible_event_load: forall w label, - possible_event w (Event_load label) w - | possible_event_store: forall w label, - possible_event w (Event_store label) w. + | possible_event_vload: forall w1 chunk id ofs evres w2, + nextworld_vload w1 chunk id ofs = Some (evres, w2) -> + possible_event w1 (Event_vload chunk id ofs evres) w2 + | possible_event_vstore: forall w1 chunk id ofs evarg w2, + nextworld_vstore w1 chunk id ofs evarg = Some w2 -> + possible_event w1 (Event_vstore chunk id ofs evarg) w2. Inductive possible_trace: world -> trace -> world -> Prop := | possible_trace_nil: forall w, @@ -213,9 +225,9 @@ Proof. destruct t2; simpl; auto. destruct t2; simpl. destruct ev; auto. inv H1. inv H; inv H5; auto; intros. - subst. rewrite H in H1; inv H1. split; eauto. - eauto. - eauto. + destruct H2. subst. rewrite H in H1; inv H1. split; eauto. + destruct H2. destruct H3. subst. rewrite H in H1; inv H1. split; eauto. + destruct H2. destruct H3. destruct H4. subst. rewrite H in H1; inv H1. eauto. Qed. Lemma step_deterministic: diff --git a/common/Events.v b/common/Events.v index ad1fc518..a666b405 100644 --- a/common/Events.v +++ b/common/Events.v @@ -29,28 +29,38 @@ Require Import Memory. input/output events, which represent the actions of the program that the external world can observe. CompCert leaves much flexibility as to the exact content of events: the only requirement is that they - do not expose pointer values nor memory states, because these + do not expose memory states nor pointer values + (other than pointers to global variables), because these are not preserved literally during compilation. For concreteness, we use the following type for events. Each event represents either: - A system call (e.g. an input/output operation), recording the - name of the system call, its int-or-float parameters, - and its int-or-float result. + name of the system call, its parameters, and its result. -- A volatile load from a memory location, recording a label - associated with the read (e.g. a global variable name or a source code position). +- A volatile load from a global memory location, recording the chunk + and address being read and the value just read. -- A volatile store to a memory location, also recording a label. +- A volatile store to a global memory location, recording the chunk + and address being written and the value stored there. + + The values attached to these events are of the following form. + 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. + | EVfloat: float -> eventval + | EVptr_global: ident -> int -> eventval + | EVptr_local: eventval. Inductive event: Type := | Event_syscall: ident -> list eventval -> eventval -> event - | Event_load: ident -> event - | Event_store: ident -> event. + | Event_vload: memory_chunk -> ident -> int -> eventval -> event + | Event_vstore: memory_chunk -> ident -> int -> eventval -> event. (** The dynamic semantics for programs collect traces of events. Traces are of two kinds: finite (type [trace]) or infinite (type [traceinf]). *) @@ -236,6 +246,107 @@ Transparent Eappinf. simpl. f_equal. apply IHt. Qed. +(** * Relating values and event values *) + +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). + +(** Some properties of these translation predicates. *) + +Lemma val_of_eventval_type: + forall ev ty v, + val_of_eventval 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. +Proof. + intros. inv H; inv H0; constructor; auto. +Qed. + +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). + +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. +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. +Qed. + +Lemma val_of_eventval_inject: + forall ev ty v, + meminj_preserves_globals -> + val_of_eventval 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. +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. +Proof. + intros. inv H0; inv H1; auto. + exploit (H id id0); eauto. congruence. + elim (H5 _ H2). + elim (H2 _ H5). +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. +Proof. + intros. inv H; inv H0; auto. congruence. +Qed. + +End EVENTVAL. + (** * Semantics of external functions *) (** Each external function is of one of the following kinds: *) @@ -245,15 +356,20 @@ Inductive extfun_kind: signature -> Type := (** A system call. Takes integer-or-float arguments, produces a result that is an integer or a float, does not modify the memory, and produces an [Event_syscall] event in the trace. *) - | EF_load (label: ident) (chunk: memory_chunk): extfun_kind (mksignature (Tint :: nil) (Some (type_of_chunk chunk))) + | 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. - Produces an [Event_load] event containing the given label. *) - | EF_store (label: ident) (chunk: memory_chunk): extfun_kind (mksignature (Tint :: type_of_chunk chunk :: nil) None) + 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. *) + | 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 containing the given label. *) + Produces an [Event_store] event. *) | 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. @@ -268,15 +384,19 @@ 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 values of the arguments passed to this function - the memory state before the call - the result value of the call - the memory state after the call - the trace generated by the call (can be empty). - -We now specify the expected properties of this predicate. *) +Definition extcall_sem : Type := + (ident -> option block) -> list val -> mem -> trace -> val -> mem -> Prop. + +(** We now specify the expected properties of this predicate. *) + Definition mem_unchanged_on (P: block -> Z -> Prop) (m_before m_after: mem): Prop := (forall b ofs p, P b ofs -> Mem.perm m_before b ofs p -> Mem.perm m_after b ofs p) @@ -304,52 +424,52 @@ Definition inject_separated (f f': meminj) (m1 m2: mem): Prop := Fixpoint matching_traces (t1 t2: trace) {struct t1} : Prop := match t1, t2 with | Event_syscall name1 args1 res1 :: t1', Event_syscall name2 args2 res2 :: t2' => - name1 = name2 -> args1 = args2 -> res1 = res2 /\ matching_traces t1' t2' - | Event_load name1 :: t1', Event_load name2 :: t2' => - name1 = name2 -> matching_traces t1' t2' - | Event_store name1 :: t1', Event_store name2 :: t2' => - name1 = name2 -> matching_traces t1' t2' + name1 = name2 /\ args1 = args2 -> res1 = res2 /\ matching_traces t1' t2' + | Event_vload chunk1 id1 ofs1 res1 :: t1', Event_vload chunk2 id2 ofs2 res2 :: t2' => + chunk1 = chunk2 /\ id1 = id2 /\ ofs1 = ofs2 -> res1 = res2 /\ matching_traces t1' t2' + | Event_vstore chunk1 id1 ofs1 arg1 :: t1', Event_vstore chunk2 id2 ofs2 arg2 :: t2' => + chunk1 = chunk2 /\ id1 = id2 /\ ofs1 = ofs2 /\ arg1 = arg2 -> matching_traces t1' t2' | _, _ => True end. -Record extcall_properties (sem: list val -> mem -> trace -> val -> mem -> Prop) +Record extcall_properties (sem: extcall_sem) (sg: signature) : Prop := mk_extcall_properties { (** The return value of an external call must agree with its signature. *) ec_well_typed: - forall vargs m1 t vres m2, - sem vargs m1 t vres m2 -> + forall symb vargs m1 t vres m2, + sem symb 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 vargs m1 t vres m2, - sem vargs m1 t vres m2 -> + forall symb vargs m1 t vres m2, + sem symb vargs m1 t vres m2 -> List.length vargs = List.length sg.(sig_args); (** External calls cannot invalidate memory blocks. (Remember that freeing a block does not invalidate its block identifier.) *) ec_valid_block: - forall vargs m1 t vres m2 b, - sem vargs m1 t vres m2 -> + forall symb vargs m1 t vres m2 b, + sem symb 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 vargs m1 t vres m2 b, - sem vargs m1 t vres m2 -> + forall symb vargs m1 t vres m2 b, + sem symb 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 vargs m1 t vres m2 m1' vargs', - sem vargs m1 t vres m2 -> + forall symb vargs m1 t vres m2 m1' vargs', + sem symb vargs m1 t vres m2 -> Mem.extends m1 m1' -> Val.lessdef_list vargs vargs' -> exists vres', exists m2', - sem vargs' m1' t vres' m2' + sem symb vargs' m1' t vres' m2' /\ Val.lessdef vres vres' /\ Mem.extends m2 m2' /\ mem_unchanged_on (loc_out_of_bounds m1) m1' m2'; @@ -357,12 +477,13 @@ Record extcall_properties (sem: list val -> mem -> trace -> val -> mem -> Prop) (** External calls must commute with memory injections, in the following sense. *) ec_mem_inject: - forall vargs m1 t vres m2 f m1' vargs', - sem vargs m1 t vres m2 -> + forall symb vargs m1 t vres m2 f m1' vargs', + meminj_preserves_globals symb f -> + sem symb vargs m1 t vres m2 -> Mem.inject f m1 m1' -> val_list_inject f vargs vargs' -> exists f', exists vres', exists m2', - sem vargs' m1' t vres' m2' + sem symb vargs' m1' t vres' m2' /\ val_inject f' vres vres' /\ Mem.inject f' m2 m2' /\ mem_unchanged_on (loc_unmapped f) m1 m2 @@ -374,64 +495,111 @@ Record extcall_properties (sem: list val -> mem -> trace -> val -> mem -> Prop) if the observable traces match, the return states must be identical. *) ec_determ: - forall vargs m t1 vres1 m1 t2 vres2 m2, - sem vargs m t1 vres1 m1 -> sem vargs m t2 vres2 m2 -> + 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 -> matching_traces t1 t2 -> t1 = t2 /\ vres1 = vres2 /\ m1 = m2 }. (** ** Semantics of volatile loads *) -Inductive extcall_load_sem (label: ident) (chunk: memory_chunk): - list val -> mem -> trace -> val -> mem -> Prop := - | extcall_load_sem_intro: forall b ofs m vres, - Mem.load chunk m b (Int.signed ofs) = Some vres -> - extcall_load_sem label chunk (Vptr b ofs :: nil) m (Event_load label :: nil) vres m. - -Lemma extcall_load_ok: - forall label chunk, - extcall_properties (extcall_load_sem label chunk) +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'. + +Lemma volatile_load_ok: + forall chunk, + extcall_properties (volatile_load_sem chunk) (mksignature (Tint :: nil) (Some (type_of_chunk chunk))). Proof. intros; constructor; intros. - inv H. unfold proj_sig_res. simpl. eapply Mem.load_type; eauto. + inv H. unfold proj_sig_res. simpl. eapply Mem.load_type; eauto. inv H. simpl. auto. - inv H. auto. + inv H. eauto with mem. - inv H. auto. + inv H. eapply Mem.bounds_store; eauto. - inv H. inv H1. inv H6. inv H4. - exploit Mem.load_extends; eauto. intros [v2 [A B]]. - exists v2; exists m1'; intuition. - constructor; auto. - red. auto. - - inv H. inv H1. inv H6. - assert (Mem.loadv chunk m2 (Vptr b ofs) = Some vres). auto. - exploit Mem.loadv_inject; eauto. intros [v2 [A B]]. - inv H4. - exists f; exists v2; exists m1'; intuition. - constructor. auto. - red; auto. - red; 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. + + 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. + 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; intros. congruence. - inv H; inv H0. intuition 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. + intuition congruence. Qed. (** ** Semantics of volatile stores *) -Inductive extcall_store_sem (label: ident) (chunk: memory_chunk): - list val -> mem -> trace -> val -> mem -> Prop := - | extcall_store_sem_intro: forall b ofs v m m', +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 -> Mem.store chunk m b (Int.signed ofs) v = Some m' -> - extcall_store_sem label chunk (Vptr b ofs :: v :: nil) m (Event_store label :: nil) Vundef m'. - -Lemma extcall_store_ok: - forall label chunk, - extcall_properties (extcall_store_sem label chunk) + volatile_store_sem chunk symb + (Vptr b ofs :: v :: nil) m + (Event_vstore chunk id ofs ev :: nil) + Vundef m'. + +Lemma volatile_store_ok: + forall chunk, + extcall_properties (volatile_store_sem chunk) (mksignature (Tint :: type_of_chunk chunk :: nil) None). Proof. intros; constructor; intros. @@ -444,63 +612,63 @@ Proof. inv H. eapply Mem.bounds_store; eauto. - inv H. inv H1. inv H6. inv H7. inv H4. + inv H. inv H1. inv H6. inv H8. inv H7. exploit Mem.store_within_extends; eauto. intros [m' [A B]]. exists Vundef; exists m'; intuition. - constructor; auto. + constructor; auto. eapply eventval_of_val_lessdef; eauto. 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 H2. + eapply Mem.store_valid_access_3. eexact H4. intros [C D]. 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 H4). unfold loc_out_of_bounds, Intv.In; simpl. omega. + red; intros. generalize (H x H6). unfold loc_out_of_bounds, Intv.In; simpl. omega. simpl; omega. simpl; omega. - inv H. inv H1. inv H6. inv H7. - 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. + inv H0. inv H2. inv H7. inv H9. inv H10. + exploit Mem.store_mapped_inject; eauto. intros [m2' [A B]]. exists f; exists Vundef; exists m2'; intuition. - constructor; auto. + 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. split; intros. eapply Mem.perm_store_1; eauto. - rewrite <- H4. eapply Mem.load_store_other; eauto. - left. exploit (H1 ofs0). generalize (size_chunk_pos chunk0). omega. + 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 <- H4. eapply Mem.load_store_other; eauto. + rewrite <- H2. 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 H2. + eapply Mem.store_valid_access_3. eexact H5. intros [C D]. 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 (H1 x H5). eauto. unfold Intv.In; simpl. omega. + red; intros. exploit (H0 x H8). eauto. unfold Intv.In; simpl. omega. simpl; omega. simpl; omega. red; intros. congruence. - inv H; inv H0. intuition congruence. + inv H0; inv H1. + assert (id = id0) by (eapply H; eauto). + exploit eventval_of_val_determ. eauto. eexact H4. eexact H14. intros. + intuition congruence. Qed. (** ** Semantics of dynamic memory allocation (malloc) *) -Inductive extcall_malloc_sem: - list val -> mem -> trace -> val -> mem -> Prop := - | extcall_malloc_sem_intro: forall n m m' b m'', +Inductive extcall_malloc_sem: extcall_sem := + | extcall_malloc_sem_intro: forall symb 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 (Vint n :: nil) m E0 (Vptr b Int.zero) m''. + extcall_malloc_sem symb (Vint n :: nil) m E0 (Vptr b Int.zero) m''. Lemma extcall_malloc_ok: extcall_properties extcall_malloc_sem @@ -541,7 +709,7 @@ Proof. econstructor; eauto. eapply UNCHANGED; eauto. - inv H. inv H1. inv H5. inv H7. + inv H0. inv H2. inv H6. inv H8. exploit Mem.alloc_parallel_inject; eauto. apply Zle_refl. apply Zle_refl. intros [f' [m3' [b' [ALLOC [A [B [C D]]]]]]]. exploit Mem.store_mapped_inject. eexact A. eauto. eauto. @@ -553,21 +721,20 @@ Proof. eapply UNCHANGED; eauto. eapply UNCHANGED; eauto. red; intros. destruct (eq_block b1 b). - subst b1. rewrite C in H1. inv H1. eauto with mem. - rewrite D in H1. congruence. auto. + subst b1. rewrite C in H2. inv H2. eauto with mem. + rewrite D in H2. congruence. auto. - inv H; inv H0. intuition congruence. + inv H0; inv H1. intuition congruence. Qed. (** ** Semantics of dynamic memory deallocation (free) *) -Inductive extcall_free_sem: - list val -> mem -> trace -> val -> mem -> Prop := - | extcall_free_sem_intro: forall b lo sz m m', +Inductive extcall_free_sem: extcall_sem := + | extcall_free_sem_intro: forall symb 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 (Vptr b lo :: nil) m E0 Vundef m'. + extcall_free_sem symb (Vptr b lo :: nil) m E0 Vundef m'. Lemma extcall_free_ok: extcall_properties extcall_free_sem @@ -592,7 +759,7 @@ Proof. inv H. unfold proj_sig_res. simpl. auto. - inv H. auto. + inv H. auto. inv H. eauto with mem. @@ -609,19 +776,19 @@ Proof. exploit Mem.range_perm_in_bounds. eapply Mem.free_range_perm. eexact H4. omega. omega. - inv H. inv H1. inv H8. inv H6. + inv H0. inv H2. inv H7. inv H9. exploit Mem.load_inject; eauto. intros [vsz [A B]]. inv B. assert (Mem.range_perm m1 b (Int.signed lo - 4) (Int.signed lo + Int.signed sz) Freeable). eapply Mem.free_range_perm; eauto. exploit Mem.address_inject; eauto. apply Mem.perm_implies with Freeable; auto with mem. - apply H. instantiate (1 := lo). omega. + apply H0. instantiate (1 := lo). omega. intro EQ. assert (Mem.range_perm m1' b2 (Int.signed lo + delta - 4) (Int.signed lo + delta + Int.signed sz) Freeable). red; intros. replace ofs with ((ofs - delta) + delta) by omega. - eapply Mem.perm_inject; eauto. apply H. omega. - destruct (Mem.range_perm_free _ _ _ _ H1) as [m2' FREE]. + eapply Mem.perm_inject; eauto. apply H0. omega. + destruct (Mem.range_perm_free _ _ _ _ H2) as [m2' FREE]. exists f; exists Vundef; exists m2'; intuition. econstructor. @@ -630,7 +797,7 @@ Proof. rewrite EQ. auto. assert (Mem.free_list m1 ((b, Int.signed lo - 4, Int.signed lo + Int.signed sz) :: nil) = Some m2). - simpl. rewrite H4. auto. + simpl. rewrite H5. auto. eapply Mem.free_inject; eauto. intros. destruct (eq_block b b1). subst b. assert (delta0 = delta) by congruence. subst delta0. @@ -640,108 +807,30 @@ Proof. exploit Mem.inject_no_overlap. eauto. eauto. eauto. eauto. instantiate (1 := ofs + delta0 - delta). apply Mem.perm_implies with Freeable; auto with mem. - apply H. omega. eauto with mem. + apply H0. omega. eauto with mem. unfold block; omega. eapply UNCHANGED; eauto. omega. intros. - red in H6. left. congruence. + red in H7. left. congruence. eapply UNCHANGED; eauto. omega. intros. destruct (eq_block b' b2); auto. subst b'. right. - red in H6. generalize (H6 _ _ H5). intros. - exploit Mem.range_perm_in_bounds. eexact H. omega. intros. omega. + red in H7. generalize (H7 _ _ H6). intros. + exploit Mem.range_perm_in_bounds. eexact H0. omega. intros. omega. red; intros. congruence. - inv H; inv H0. intuition congruence. + inv H0; inv H1. intuition congruence. Qed. (** ** Semantics of system calls. *) -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). - -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). - -Inductive extcall_io_sem (name: ident) (sg: signature): - list val -> mem -> trace -> val -> mem -> Prop := - | extcall_io_sem_intro: forall vargs m args res vres, - eventval_list_match args (sig_args sg) vargs -> - eventval_match res (proj_sig_res sg) vres -> - extcall_io_sem name sg vargs m (Event_syscall name args res :: E0) vres m. - -Remark 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. -Qed. - -Remark 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. - -Remark eventval_match_inject: - forall f 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; constructor. -Qed. - -Remark eventval_match_inject_2: - forall f ev ty v, - eventval_match ev ty v -> val_inject f v v. -Proof. - induction 1; constructor. -Qed. - -Remark eventval_list_match_inject: - forall f 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. - -Remark 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. - -Remark 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. -Qed. - -Remark 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. -Qed. - -Remark 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. +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. Lemma extcall_io_ok: forall name sg, @@ -749,9 +838,9 @@ Lemma extcall_io_ok: Proof. intros; constructor; intros. - inv H. inv H1; constructor. + inv H. eapply val_of_eventval_type; eauto. - inv H. eapply eventval_list_match_length; eauto. + inv H. auto. inv H; auto. @@ -759,21 +848,34 @@ Proof. inv H. exists vres; exists m1'; intuition. - econstructor; eauto. eapply eventval_list_match_lessdef; eauto. + 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. red; auto. - inv H. + inv H0. exists f; exists vres; exists m1'; intuition. - econstructor; eauto. eapply eventval_list_match_inject; eauto. - eapply eventval_match_inject_2; eauto. + 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. red; auto. red; auto. red; intros; congruence. - inv H; inv H0. simpl in H1. - assert (args = args0) by (eapply eventval_list_match_determ_2; eauto). - destruct H1; auto. subst. - intuition. eapply eventval_match_determ_1; eauto. + 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. Qed. (** ** Combined semantics of external calls *) @@ -789,12 +891,11 @@ Qed. This predicate is used in the semantics of all CompCert languages. *) -Definition external_call (ef: external_function): - list val -> mem -> trace -> val -> mem -> Prop := +Definition external_call (ef: external_function): extcall_sem := match classify_external_function ef with | EF_syscall sg name => extcall_io_sem name sg - | EF_load label chunk => extcall_load_sem label chunk - | EF_store label chunk => extcall_store_sem label chunk + | EF_vload chunk => volatile_load_sem chunk + | EF_vstore chunk => volatile_store_sem chunk | EF_malloc => extcall_malloc_sem | EF_free => extcall_free_sem end. @@ -805,8 +906,8 @@ Theorem external_call_spec: Proof. intros. unfold external_call. destruct (classify_external_function ef). apply extcall_io_ok. - apply extcall_load_ok. - apply extcall_store_ok. + apply volatile_load_ok. + apply volatile_store_ok. apply extcall_malloc_ok. apply extcall_free_ok. Qed. @@ -818,3 +919,15 @@ 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. *) + +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. +Proof. + intros. replace symb2 with symb1; auto. + symmetry. apply extensionality. auto. +Qed. diff --git a/common/Globalenvs.v b/common/Globalenvs.v index 9dbf9022..65ae06c1 100644 --- a/common/Globalenvs.v +++ b/common/Globalenvs.v @@ -71,7 +71,9 @@ Record t: Type := mkgenv { genv_nextvar_pos: genv_nextvar > 0; genv_symb_range: forall id b, PTree.get id genv_symb = Some b -> b <> 0 /\ genv_nextfun < b /\ b < genv_nextvar; genv_funs_range: forall b f, ZMap.get b genv_funs = Some f -> genv_nextfun < b < 0; - genv_vars_range: forall b v, ZMap.get b genv_vars = Some v -> 0 < b < genv_nextvar + genv_vars_range: forall b v, ZMap.get b genv_vars = Some v -> 0 < b < genv_nextvar; + genv_vars_inj: forall id1 id2 b, + PTree.get id1 genv_symb = Some b -> PTree.get id2 genv_symb = Some b -> id1 = id2 }. (** ** Lookup functions *) @@ -111,7 +113,7 @@ Program Definition add_function (ge: t) (idf: ident * F) : t := ge.(genv_vars) (ge.(genv_nextfun) - 1) ge.(genv_nextvar) - _ _ _ _ _. + _ _ _ _ _ _. Next Obligation. destruct ge; simpl; omega. Qed. @@ -131,6 +133,15 @@ Qed. Next Obligation. destruct ge; eauto. Qed. +Next Obligation. + destruct ge; simpl in *. + rewrite PTree.gsspec in H. rewrite PTree.gsspec in H0. + destruct (peq id1 i); destruct (peq id2 i). + congruence. + exploit genv_symb_range0; eauto. intros [A B]. inv H. omegaContradiction. + exploit genv_symb_range0; eauto. intros [A B]. inv H0. omegaContradiction. + eauto. +Qed. Program Definition add_variable (ge: t) (idv: ident * list init_data * V) : t := @mkgenv @@ -139,7 +150,7 @@ Program Definition add_variable (ge: t) (idv: ident * list init_data * V) : t := (ZMap.set ge.(genv_nextvar) (Some idv#2) ge.(genv_vars)) ge.(genv_nextfun) (ge.(genv_nextvar) + 1) - _ _ _ _ _. + _ _ _ _ _ _. Next Obligation. destruct ge; auto. Qed. @@ -159,9 +170,18 @@ Next Obligation. destruct (ZIndexed.eq b genv_nextvar0). subst; omega. exploit genv_vars_range0; eauto. omega. Qed. +Next Obligation. + destruct ge; simpl in *. + rewrite PTree.gsspec in H. rewrite PTree.gsspec in H0. + destruct (peq id1 i); destruct (peq id2 i). + congruence. + exploit genv_symb_range0; eauto. intros [A B]. inv H. omegaContradiction. + exploit genv_symb_range0; eauto. intros [A B]. inv H0. omegaContradiction. + eauto. +Qed. Program Definition empty_genv : t := - @mkgenv (PTree.empty block) (ZMap.init None) (ZMap.init None) (-1) 1 _ _ _ _ _. + @mkgenv (PTree.empty block) (ZMap.init None) (ZMap.init None) (-1) 1 _ _ _ _ _ _. Next Obligation. omega. Qed. @@ -177,6 +197,9 @@ Qed. Next Obligation. rewrite ZMap.gi in H. discriminate. Qed. +Next Obligation. + rewrite PTree.gempty in H. discriminate. +Qed. Definition add_functions (ge: t) (fl: list (ident * F)) : t := List.fold_left add_function fl ge. @@ -435,38 +458,13 @@ Proof. Qed. Theorem global_addresses_distinct: - forall p id1 id2 b1 b2, - id1<>id2 -> - find_symbol (globalenv p) id1 = Some b1 -> - find_symbol (globalenv p) id2 = Some b2 -> - b1<>b2. -Proof. - intros until b2; intro DIFF. - - set (P := fun ge => find_symbol ge id1 = Some b1 -> find_symbol ge id2 = Some b2 -> b1 <> b2). - - assert (forall fl ge, P ge -> P (add_functions ge fl)). - induction fl; intros; simpl. auto. - apply IHfl. red. unfold find_symbol; simpl. - repeat rewrite PTree.gsspec. - fold ident. destruct (peq id1 a#1); destruct (peq id2 a#1). - congruence. - intros. inversion H0. exploit genv_symb_range; eauto. unfold block; omega. - intros. inversion H1. exploit genv_symb_range; eauto. unfold block; omega. - auto. - - assert (forall vl ge, P ge -> P (add_variables ge vl)). - induction vl; intros; simpl. auto. - apply IHvl. red. unfold find_symbol; simpl. - repeat rewrite PTree.gsspec. - fold ident. destruct (peq id1 a#1#1); destruct (peq id2 a#1#1). - congruence. - intros. inversion H1. exploit genv_symb_range; eauto. unfold block; omega. - intros. inversion H2. exploit genv_symb_range; eauto. unfold block; omega. - auto. - - change (P (globalenv p)). unfold globalenv. apply H0. apply H. - red; unfold find_symbol; simpl; intros. rewrite PTree.gempty in H1. congruence. + forall ge id1 id2 b1 b2, + id1 <> id2 -> + find_symbol ge id1 = Some b1 -> + find_symbol ge id2 = Some b2 -> + b1 <> b2. +Proof. + intros. red; intros; subst. elim H. destruct ge. eauto. Qed. (** * Construction of the initial memory state *) diff --git a/driver/Complements.v b/driver/Complements.v index b76a99f9..a67d61e4 100644 --- a/driver/Complements.v +++ b/driver/Complements.v @@ -64,7 +64,9 @@ Proof. congruence. assert (ef0 = ef) by congruence. subst ef0. assert (args0 = args). eapply extcall_arguments_deterministic; eauto. subst args0. - exploit external_call_determ. eexact H4. eexact H9. auto. + exploit external_call_determ. + instantiate (1 := Genv.find_symbol ge). exact (Genv.genv_vars_inj ge). + eexact H4. eexact H9. auto. intros [A [B C]]. subst. intuition congruence. Qed. diff --git a/powerpc/Asm.v b/powerpc/Asm.v index fe6cf864..f4a8a1f4 100644 --- a/powerpc/Asm.v +++ b/powerpc/Asm.v @@ -881,7 +881,7 @@ Inductive step: state -> trace -> state -> Prop := forall b ef args res rs m t rs' m', rs PC = Vptr b Int.zero -> Genv.find_funct_ptr ge b = Some (External ef) -> - external_call ef args m t res m' -> + external_call ef (Genv.find_symbol ge) args m t res m' -> extcall_arguments rs m ef.(ef_sig) args -> rs' = (rs#(loc_external_result ef.(ef_sig)) <- res #PC <- (rs LR)) -> diff --git a/powerpc/Asmgenproof.v b/powerpc/Asmgenproof.v index 5be47347..6a484517 100644 --- a/powerpc/Asmgenproof.v +++ b/powerpc/Asmgenproof.v @@ -1335,7 +1335,7 @@ Lemma exec_function_external_prop: (m : mem) (t0 : trace) (ms' : RegEq.t -> val) (ef : external_function) (args : list val) (res : val) (m': mem), Genv.find_funct_ptr ge fb = Some (External ef) -> - external_call ef args m t0 res m' -> + external_call ef (Genv.find_symbol ge) args m t0 res m' -> Machconcr.extcall_arguments ms m (parent_sp s) (ef_sig ef) args -> ms' = Regmap.set (Conventions.loc_result (ef_sig ef)) res ms -> exec_instr_prop (Machconcr.Callstate s fb ms m) @@ -1347,6 +1347,7 @@ Proof. left; exists (State (rs#(loc_external_result (ef_sig ef)) <- res #PC <- (rs LR)) m'); split. apply plus_one. eapply exec_step_external; eauto. + eapply external_call_symbols_preserved; eauto. exact symbols_preserved. eapply extcall_arguments_match; eauto. econstructor; eauto. unfold loc_external_result. auto with ppcgen. -- cgit