From e4723d142aa7b1229cdf5989340342d7c5ce870c Mon Sep 17 00:00:00 2001 From: Xavier Leroy Date: Sun, 6 Mar 2016 10:31:26 +0100 Subject: Update the back-end proofs to the new linking framework. --- backend/RTLgenproof.v | 69 +++++++++++++++++++++------------------------------ 1 file changed, 28 insertions(+), 41 deletions(-) (limited to 'backend/RTLgenproof.v') diff --git a/backend/RTLgenproof.v b/backend/RTLgenproof.v index f458de8b..ace822fd 100644 --- a/backend/RTLgenproof.v +++ b/backend/RTLgenproof.v @@ -12,23 +12,10 @@ (** Correctness proof for RTL generation. *) -Require Import Coqlib. -Require Import Maps. -Require Import AST. -Require Import Integers. -Require Import Values. -Require Import Memory. -Require Import Events. -Require Import Smallstep. -Require Import Globalenvs. -Require Import Switch. -Require Import Registers. -Require Import Cminor. -Require Import Op. -Require Import CminorSel. -Require Import RTL. -Require Import RTLgen. -Require Import RTLgenspec. +Require Import Coqlib Maps AST Linking. +Require Import Integers Values Memory Events Smallstep Globalenvs. +Require Import Switch Registers Cminor Op CminorSel RTL. +Require Import RTLgen RTLgenspec. (** * Correspondence between Cminor environments and RTL register sets *) @@ -361,11 +348,20 @@ Qed. Require Import Errors. +Definition match_prog (p: CminorSel.program) (tp: RTL.program) := + match_program (fun cu f tf => transl_fundef f = Errors.OK tf) eq p tp. + +Lemma transf_program_match: + forall p tp, transl_program p = OK tp -> match_prog p tp. +Proof. + intros. apply match_transform_partial_program; auto. +Qed. + Section CORRECTNESS. Variable prog: CminorSel.program. Variable tprog: RTL.program. -Hypothesis TRANSL: transl_program prog = OK tprog. +Hypothesis TRANSL: match_prog prog tprog. Let ge : CminorSel.genv := Genv.globalenv prog. Let tge : RTL.genv := Genv.globalenv tprog. @@ -376,12 +372,7 @@ Let tge : RTL.genv := Genv.globalenv tprog. Lemma symbols_preserved: forall (s: ident), Genv.find_symbol tge s = Genv.find_symbol ge s. Proof - (Genv.find_symbol_transf_partial transl_fundef _ TRANSL). - -Lemma public_preserved: - forall (s: ident), Genv.public_symbol tge s = Genv.public_symbol ge s. -Proof - (Genv.public_symbol_transf_partial transl_fundef _ TRANSL). + (Genv.find_symbol_transf_partial TRANSL). Lemma function_ptr_translated: forall (b: block) (f: CminorSel.fundef), @@ -389,7 +380,7 @@ Lemma function_ptr_translated: exists tf, Genv.find_funct_ptr tge b = Some tf /\ transl_fundef f = OK tf. Proof - (Genv.find_funct_ptr_transf_partial transl_fundef _ TRANSL). + (Genv.find_funct_ptr_transf_partial TRANSL). Lemma functions_translated: forall (v: val) (f: CminorSel.fundef), @@ -397,7 +388,7 @@ Lemma functions_translated: exists tf, Genv.find_funct tge v = Some tf /\ transl_fundef f = OK tf. Proof - (Genv.find_funct_transf_partial transl_fundef _ TRANSL). + (Genv.find_funct_transf_partial TRANSL). Lemma sig_transl_function: forall (f: CminorSel.fundef) (tf: RTL.fundef), @@ -414,10 +405,10 @@ Proof. intro. inversion H. reflexivity. Qed. -Lemma varinfo_preserved: - forall b, Genv.find_var_info tge b = Genv.find_var_info ge b. +Lemma senv_preserved: + Senv.equiv (Genv.to_senv ge) (Genv.to_senv tge). Proof - (Genv.find_var_info_transf_partial transl_fundef _ TRANSL). + (Genv.senv_transf_partial TRANSL). (** Correctness of the code generated by [add_move]. *) @@ -720,8 +711,7 @@ Proof. change (rs1#rd <- v') with (regmap_setres (BR rd) v' rs1). eapply exec_Ibuiltin; eauto. eapply eval_builtin_args_trivial. - eapply external_call_symbols_preserved; eauto. - exact symbols_preserved. exact public_preserved. exact varinfo_preserved. + eapply external_call_symbols_preserved; eauto. apply senv_preserved. reflexivity. (* Match-env *) split. eauto with rtlg. @@ -754,8 +744,7 @@ Proof. eapply star_left. eapply exec_Icall; eauto. simpl. rewrite symbols_preserved. rewrite H. eauto. auto. eapply star_left. eapply exec_function_external. - eapply external_call_symbols_preserved; eauto. - exact symbols_preserved. exact public_preserved. exact varinfo_preserved. + eapply external_call_symbols_preserved; eauto. apply senv_preserved. apply star_one. apply exec_return. reflexivity. reflexivity. reflexivity. (* Match-env *) @@ -1422,8 +1411,7 @@ Proof. left. eapply plus_right. eexact E. eapply exec_Ibuiltin. eauto. eapply eval_builtin_args_preserved with (ge1 := ge); eauto. exact symbols_preserved. - eapply external_call_symbols_preserved. eauto. - exact symbols_preserved. exact public_preserved. exact varinfo_preserved. + eapply external_call_symbols_preserved. apply senv_preserved. eauto. traceEq. econstructor; eauto. constructor. eapply match_env_update_res; eauto. @@ -1540,8 +1528,7 @@ Proof. edestruct external_call_mem_extends as [tvres [tm' [A [B [C D]]]]]; eauto. econstructor; split. left; apply plus_one. eapply exec_function_external; eauto. - eapply external_call_symbols_preserved. eauto. - exact symbols_preserved. exact public_preserved. exact varinfo_preserved. + eapply external_call_symbols_preserved; eauto. apply senv_preserved. constructor; auto. (* return *) @@ -1559,9 +1546,9 @@ Proof. induction 1. exploit function_ptr_translated; eauto. intros [tf [A B]]. econstructor; split. - econstructor. apply (Genv.init_mem_transf_partial _ _ TRANSL); eauto. - rewrite (transform_partial_program_main _ _ TRANSL). fold tge. - rewrite symbols_preserved. eauto. + econstructor. apply (Genv.init_mem_transf_partial TRANSL); eauto. + replace (prog_main tprog) with (prog_main prog). rewrite symbols_preserved; eauto. + symmetry; eapply match_program_main; eauto. eexact A. rewrite <- H2. apply sig_transl_function; auto. constructor. auto. constructor. @@ -1579,7 +1566,7 @@ Theorem transf_program_correct: forward_simulation (CminorSel.semantics prog) (RTL.semantics tprog). Proof. eapply forward_simulation_star_wf with (order := lt_state). - eexact public_preserved. + apply senv_preserved. eexact transl_initial_states. eexact transl_final_states. apply lt_state_wf. -- cgit