Update the back-end proofs to the new linking framework.

1 files changed, 28 insertions, 41 deletions

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.