From e4723d142aa7b1229cdf5989340342d7c5ce870c Mon Sep 17 00:00:00 2001
From: Xavier Leroy <xavier.leroy@inria.fr>
Date: Sun, 6 Mar 2016 10:31:26 +0100
Subject: Update the back-end proofs to the new linking framework.

---
 backend/Debugvarproof.v | 81 ++++++++++++++++++++-----------------------------
 1 file changed, 33 insertions(+), 48 deletions(-)

(limited to 'backend/Debugvarproof.v')

diff --git a/backend/Debugvarproof.v b/backend/Debugvarproof.v
index 73e32103..110c0f26 100644
--- a/backend/Debugvarproof.v
+++ b/backend/Debugvarproof.v
@@ -12,28 +12,23 @@
 
 (** Correctness proof for the [Debugvar] pass. *)
 
-Require Import Coqlib.
-Require Import Axioms.
-Require Import Maps.
-Require Import Iteration.
-Require Import AST.
-Require Import Integers.
-Require Import Floats.
-Require Import Values.
-Require Import Memory.
-Require Import Events.
-Require Import Globalenvs.
-Require Import Smallstep.
-Require Import Op.
-Require Import Errors.
-Require Import Machregs.
-Require Import Locations.
-Require Import Conventions.
-Require Import Linear.
+Require Import Axioms Coqlib Maps Iteration Errors.
+Require Import Integers Floats AST Linking.
+Require Import Values Memory Events Globalenvs Smallstep.
+Require Import Machregs Locations Conventions Op Linear.
 Require Import Debugvar.
 
 (** * Relational characterization of the transformation *)
 
+Definition match_prog (p tp: program) :=
+  match_program (fun _ f tf => transf_fundef f = OK tf) eq p tp.
+
+Lemma transf_program_match:
+  forall p tp, transf_program p = OK tp -> match_prog p tp.
+Proof.
+  intros. eapply match_transform_partial_program; eauto.
+Qed.
+
 Inductive match_code: code -> code -> Prop :=
   | match_code_nil:
       match_code nil nil
@@ -294,38 +289,32 @@ Section PRESERVATION.
 Variable prog: program.
 Variable tprog: program.
 
-Hypothesis TRANSF: transf_program prog = OK tprog.
+Hypothesis TRANSF: match_prog prog tprog.
 
 Let ge := Genv.globalenv prog.
 Let tge := Genv.globalenv tprog.
 
+Lemma symbols_preserved:
+  forall (s: ident), Genv.find_symbol tge s = Genv.find_symbol ge s.
+Proof (Genv.find_symbol_match TRANSF).
+
+Lemma senv_preserved:
+  Senv.equiv ge tge.
+Proof (Genv.senv_match TRANSF).
+
 Lemma functions_translated:
-  forall v f,
+  forall (v: val) (f: fundef),
   Genv.find_funct ge v = Some f ->
   exists tf,
   Genv.find_funct tge v = Some tf /\ transf_fundef f = OK tf.
-Proof (Genv.find_funct_transf_partial transf_fundef _ TRANSF).
+Proof (Genv.find_funct_transf_partial TRANSF).
 
 Lemma function_ptr_translated:
-  forall v f,
-  Genv.find_funct_ptr ge v = Some f ->
+  forall (b: block) (f: fundef),
+  Genv.find_funct_ptr ge b = Some f ->
   exists tf,
-  Genv.find_funct_ptr tge v = Some tf /\ transf_fundef f = OK tf.
-Proof (Genv.find_funct_ptr_transf_partial transf_fundef _ TRANSF).
-
-Lemma symbols_preserved:
-  forall id,
-  Genv.find_symbol tge id = Genv.find_symbol ge id.
-Proof (Genv.find_symbol_transf_partial transf_fundef _ TRANSF).
-
-Lemma public_preserved:
-  forall id,
-  Genv.public_symbol tge id = Genv.public_symbol ge id.
-Proof (Genv.public_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).
+  Genv.find_funct_ptr tge b = Some tf /\ transf_fundef f = OK tf.
+Proof (Genv.find_funct_ptr_transf_partial TRANSF).
 
 Lemma sig_preserved:
   forall f tf,
@@ -488,8 +477,7 @@ Proof.
   eapply plus_left.
   econstructor; 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; eauto. apply senv_preserved.
   apply eval_add_delta_ranges. traceEq.
   constructor; auto.
 - (* label *)
@@ -530,8 +518,7 @@ Proof.
 - (* external function *)
   monadInv H8. econstructor; split.
   apply plus_one. econstructor; 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 *)
   inv H3. inv H1.
@@ -547,10 +534,8 @@ Proof.
   intros. inversion H.
   exploit function_ptr_translated; eauto. intros [tf [A B]].
   exists (Callstate nil tf (Locmap.init Vundef) m0); split.
-  econstructor; eauto. eapply Genv.init_mem_transf_partial; eauto.
-  replace (prog_main tprog) with (prog_main prog).
-  rewrite symbols_preserved. eauto.
-  symmetry. apply (transform_partial_program_main transf_fundef _ TRANSF).
+  econstructor; eauto. eapply (Genv.init_mem_transf_partial TRANSF); eauto.
+  rewrite (match_program_main TRANSF), symbols_preserved. auto.
   rewrite <- H3. apply sig_preserved. auto.
   constructor. constructor. auto.
 Qed.
@@ -566,7 +551,7 @@ Theorem transf_program_correct:
   forward_simulation (semantics prog) (semantics tprog).
 Proof.
   eapply forward_simulation_plus.
-  eexact public_preserved.
+  apply senv_preserved.
   eexact transf_initial_states.
   eexact transf_final_states.
   eexact transf_step_correct.
-- 
cgit