diff options
author | xleroy <xleroy@fca1b0fc-160b-0410-b1d3-a4f43f01ea2e> | 2010-05-23 15:26:33 +0000 |
---|---|---|
committer | xleroy <xleroy@fca1b0fc-160b-0410-b1d3-a4f43f01ea2e> | 2010-05-23 15:26:33 +0000 |
commit | 3a050b22f37f3c79a10a8ebae3d292fa77e91b76 (patch) | |
tree | 16a0d9366f6805cfc9726c0b80dd8da84cb63a3d /backend | |
parent | 7999c9ee1f09f7d555e3efc39f030564f76a3354 (diff) | |
download | compcert-3a050b22f37f3c79a10a8ebae3d292fa77e91b76.tar.gz compcert-3a050b22f37f3c79a10a8ebae3d292fa77e91b76.zip |
More faithful semantics for volatile reads and writes.
git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1346 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
Diffstat (limited to 'backend')
-rw-r--r-- | backend/Allocproof.v | 11 | ||||
-rw-r--r-- | backend/CSEproof.v | 7 | ||||
-rw-r--r-- | backend/Cminor.v | 4 | ||||
-rw-r--r-- | backend/CminorSel.v | 2 | ||||
-rw-r--r-- | backend/Constpropproof.v | 10 | ||||
-rw-r--r-- | backend/LTL.v | 2 | ||||
-rw-r--r-- | backend/LTLin.v | 2 | ||||
-rw-r--r-- | backend/Linear.v | 2 | ||||
-rw-r--r-- | backend/Linearizeproof.v | 7 | ||||
-rw-r--r-- | backend/Machabstr.v | 2 | ||||
-rw-r--r-- | backend/Machabstr2concr.v | 12 | ||||
-rw-r--r-- | backend/Machconcr.v | 2 | ||||
-rw-r--r-- | backend/RTL.v | 2 | ||||
-rw-r--r-- | backend/RTLgenproof.v | 8 | ||||
-rw-r--r-- | backend/Reloadproof.v | 7 | ||||
-rw-r--r-- | backend/Selectionproof.v | 10 | ||||
-rw-r--r-- | backend/Stackingproof.v | 11 | ||||
-rw-r--r-- | backend/Tailcallproof.v | 7 | ||||
-rw-r--r-- | backend/Tunnelingproof.v | 7 |
19 files changed, 90 insertions, 25 deletions
diff --git a/backend/Allocproof.v b/backend/Allocproof.v index b845323f..c5d6adc3 100644 --- a/backend/Allocproof.v +++ b/backend/Allocproof.v @@ -418,6 +418,14 @@ Proof. exact TRANSF. Qed. +Lemma varinfo_preserved: + forall b, Genv.find_var_info tge b = Genv.find_var_info ge b. +Proof. + intro. unfold ge, tge. + apply Genv.find_var_info_transf_partial with transf_fundef. + exact TRANSF. +Qed. + Lemma functions_translated: forall (v: val) (f: RTL.fundef), Genv.find_funct ge v = Some f -> @@ -717,7 +725,8 @@ Proof. injection H7; intro EQ; inv EQ. econstructor; split. eapply exec_function_external; eauto. - eapply external_call_symbols_preserved; eauto. exact symbols_preserved. + eapply external_call_symbols_preserved; eauto. + exact symbols_preserved. exact varinfo_preserved. eapply match_states_return; eauto. (* return *) diff --git a/backend/CSEproof.v b/backend/CSEproof.v index ce577aca..445c1af9 100644 --- a/backend/CSEproof.v +++ b/backend/CSEproof.v @@ -735,6 +735,10 @@ Lemma symbols_preserved: forall (s: ident), Genv.find_symbol tge s = Genv.find_symbol ge s. Proof (Genv.find_symbol_transf transf_fundef prog). +Lemma varinfo_preserved: + forall b, Genv.find_var_info tge b = Genv.find_var_info ge b. +Proof (Genv.find_var_info_transf transf_fundef prog). + Lemma functions_translated: forall (v: val) (f: RTL.fundef), Genv.find_funct ge v = Some f -> @@ -935,7 +939,8 @@ Proof. (* external function *) simpl. econstructor; split. eapply exec_function_external; eauto. - eapply external_call_symbols_preserved; eauto. exact symbols_preserved. + eapply external_call_symbols_preserved; eauto. + exact symbols_preserved. exact varinfo_preserved. econstructor; eauto. (* return *) diff --git a/backend/Cminor.v b/backend/Cminor.v index cc4afa50..bdfb379a 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 (Genv.find_symbol ge) vargs m t vres m' -> + external_call ef 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 (Genv.find_symbol ge) args m t res m' -> + external_call ef 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 65dd4dec..1e87419f 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 (Genv.find_symbol ge) vargs m t vres m' -> + external_call ef 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 b5c3b1e3..16f839fc 100644 --- a/backend/Constpropproof.v +++ b/backend/Constpropproof.v @@ -146,6 +146,13 @@ Proof. apply Genv.find_symbol_transf. Qed. +Lemma varinfo_preserved: + forall b, Genv.find_var_info tge b = Genv.find_var_info ge b. +Proof. + intros; unfold ge, tge, tprog, transf_program. + apply Genv.find_var_info_transf. +Qed. + Lemma functions_translated: forall (v: val) (f: fundef), Genv.find_funct ge v = Some f -> @@ -415,7 +422,8 @@ Proof. (* external function *) simpl. econstructor; split. eapply exec_function_external; eauto. - eapply external_call_symbols_preserved; eauto. exact symbols_preserved. + eapply external_call_symbols_preserved; eauto. + exact symbols_preserved. exact varinfo_preserved. constructor; auto. (* return *) diff --git a/backend/LTL.v b/backend/LTL.v index 4aa8afc5..a44f3fa4 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 (Genv.find_symbol ge) args m t res m' -> + external_call ef 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 64017c30..806a7aa9 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 (Genv.find_symbol ge) args m t res m' -> + external_call ef 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 7d21651d..71310a97 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 (Genv.find_symbol ge) args m t res m' -> + external_call ef 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 fcb1acfb..5f0a2a4e 100644 --- a/backend/Linearizeproof.v +++ b/backend/Linearizeproof.v @@ -63,6 +63,10 @@ Lemma symbols_preserved: Genv.find_symbol tge id = Genv.find_symbol ge id. Proof (Genv.find_symbol_transf_partial transf_fundef _ TRANSF). +Lemma varinfo_preserved: + forall b, Genv.find_var_info tge b = Genv.find_var_info ge b. +Proof (Genv.find_var_info_transf_partial transf_fundef _ TRANSF). + Lemma sig_preserved: forall f tf, transf_fundef f = OK tf -> @@ -684,7 +688,8 @@ Proof. (* external function *) monadInv H6. econstructor; split. apply plus_one. eapply exec_function_external; eauto. - eapply external_call_symbols_preserved; eauto. exact symbols_preserved. + eapply external_call_symbols_preserved; eauto. + exact symbols_preserved. exact varinfo_preserved. econstructor; eauto. (* return *) diff --git a/backend/Machabstr.v b/backend/Machabstr.v index bbc7e7d8..060c6c2b 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 (Genv.find_symbol ge) args m t res m' -> + external_call ef 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 b8232971..481b561c 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 symb fr sp base mm ms mm' ms' ef vargs vres t vargs' vres', + forall (ge: genv) 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 symb vargs mm t vres mm' -> + external_call ef ge vargs mm t vres mm' -> Mem.extends mm' ms' -> - external_call ef symb vargs' ms t vres' ms' -> + external_call ef ge 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 (Genv.find_symbol ge) vargs mm t vres mm' -> + external_call ef ge vargs mm t vres mm' -> Mem.extends mm' ms' -> - external_call ef (Genv.find_symbol ge) vargs' ms t vres' ms' -> + external_call ef 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 90d08f1f..5b63fa8f 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 (Genv.find_symbol ge) args m t res m' -> + external_call ef 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/RTL.v b/backend/RTL.v index c8220e5d..a17c74ee 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 (Genv.find_symbol ge) args m t res m' -> + external_call ef 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 92f4cc91..a96dfbfd 100644 --- a/backend/RTLgenproof.v +++ b/backend/RTLgenproof.v @@ -388,6 +388,11 @@ Proof. intro. inversion H. reflexivity. Qed. +Lemma varinfo_preserved: + forall b, Genv.find_var_info tge b = Genv.find_var_info ge b. +Proof + (Genv.find_var_info_transf_partial transl_fundef _ TRANSL). + (** Correctness of the code generated by [add_move]. *) Lemma tr_move_correct: @@ -1320,7 +1325,8 @@ Proof. monadInv TF. econstructor; split. left; apply plus_one. eapply exec_function_external; eauto. - eapply external_call_symbols_preserved; eauto. exact symbols_preserved. + eapply external_call_symbols_preserved; eauto. + exact symbols_preserved. exact varinfo_preserved. constructor; auto. (* return *) diff --git a/backend/Reloadproof.v b/backend/Reloadproof.v index 1fa000c9..155f7b1b 100644 --- a/backend/Reloadproof.v +++ b/backend/Reloadproof.v @@ -813,6 +813,10 @@ Lemma symbols_preserved: Genv.find_symbol tge id = Genv.find_symbol ge id. Proof (@Genv.find_symbol_transf _ _ _ transf_fundef prog). +Lemma varinfo_preserved: + forall b, Genv.find_var_info tge b = Genv.find_var_info ge b. +Proof (@Genv.find_var_info_transf _ _ _ transf_fundef prog). + Lemma sig_preserved: forall f, funsig (transf_fundef f) = LTLin.funsig f. Proof. @@ -1310,7 +1314,8 @@ 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. + eapply external_call_symbols_preserved; eauto. + exact symbols_preserved. exact varinfo_preserved. econstructor; eauto. simpl. rewrite Locmap.gss. auto. intros. rewrite Locmap.gso. auto. diff --git a/backend/Selectionproof.v b/backend/Selectionproof.v index 0d1a1ee7..e03085a9 100644 --- a/backend/Selectionproof.v +++ b/backend/Selectionproof.v @@ -319,6 +319,13 @@ Proof. intros. destruct f; reflexivity. Qed. +Lemma varinfo_preserved: + forall b, Genv.find_var_info tge b = Genv.find_var_info ge b. +Proof. + intros; unfold ge, tge, tprog, sel_program. + apply Genv.find_var_info_transf. +Qed. + (** Semantic preservation for expressions. *) Lemma sel_expr_correct: @@ -471,7 +478,8 @@ Proof. constructor; auto. (* external call *) econstructor; split. - econstructor. eapply external_call_symbols_preserved; eauto. exact symbols_preserved. + econstructor. eapply external_call_symbols_preserved; eauto. + exact symbols_preserved. exact varinfo_preserved. constructor; auto. Qed. diff --git a/backend/Stackingproof.v b/backend/Stackingproof.v index fbe4b68f..4406187f 100644 --- a/backend/Stackingproof.v +++ b/backend/Stackingproof.v @@ -1139,6 +1139,14 @@ Proof. exact TRANSF. Qed. +Lemma varinfo_preserved: + forall b, Genv.find_var_info tge b = Genv.find_var_info ge b. +Proof. + intros. unfold ge, tge. + apply Genv.find_var_info_transf_partial with transf_fundef. + exact TRANSF. +Qed. + Lemma functions_translated: forall v f, Genv.find_funct ge v = Some f -> @@ -1574,7 +1582,8 @@ 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. + eapply external_call_symbols_preserved; eauto. + exact symbols_preserved. exact varinfo_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 0535cbfb..2eed6e8d 100644 --- a/backend/Tailcallproof.v +++ b/backend/Tailcallproof.v @@ -240,6 +240,10 @@ Lemma symbols_preserved: forall (s: ident), Genv.find_symbol tge s = Genv.find_symbol ge s. Proof (Genv.find_symbol_transf transf_fundef prog). +Lemma varinfo_preserved: + forall b, Genv.find_var_info tge b = Genv.find_var_info ge b. +Proof (Genv.find_var_info_transf transf_fundef prog). + Lemma functions_translated: forall (v: val) (f: RTL.fundef), Genv.find_funct ge v = Some f -> @@ -557,7 +561,8 @@ 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. + eapply external_call_symbols_preserved; eauto. + exact symbols_preserved. exact varinfo_preserved. constructor; auto. (* returnstate *) diff --git a/backend/Tunnelingproof.v b/backend/Tunnelingproof.v index 3f0a27d0..774ce853 100644 --- a/backend/Tunnelingproof.v +++ b/backend/Tunnelingproof.v @@ -160,6 +160,10 @@ Lemma symbols_preserved: Genv.find_symbol tge id = Genv.find_symbol ge id. Proof (@Genv.find_symbol_transf _ _ _ tunnel_fundef p). +Lemma varinfo_preserved: + forall b, Genv.find_var_info tge b = Genv.find_var_info ge b. +Proof (@Genv.find_var_info_transf _ _ _ tunnel_fundef p). + Lemma sig_preserved: forall f, funsig (tunnel_fundef f) = funsig f. Proof. @@ -335,7 +339,8 @@ Proof. (* external function *) simpl. left; econstructor; split. eapply exec_function_external; eauto. - eapply external_call_symbols_preserved; eauto. exact symbols_preserved. + eapply external_call_symbols_preserved; eauto. + exact symbols_preserved. exact varinfo_preserved. simpl. econstructor; eauto. (* return *) inv H3. inv H1. |