Merge pull request #93 from AbsInt/separate-compilation

This pull request implements "approach A" to separate compilation in CompCert from the paper

Lightweight verification of separate compilation
by Jeehoon Kang, Yoonseung Kim, Chung-Kil Hur, Derek Dreyer, Viktor Vafeiadis,
POPL 2016, pages 178-190

In a nutshell, semantic preservation is still stated and proved in terms of a whole C program and a whole assembly program. However, the whole C program can be the result of syntactic linking of several C compilation units, each unit being separated compiled by CompCert to produce assembly unit, and these assembly units being linked together to produce the whole assembly program.

This way, the statement of semantic preservation and its proof now take into account the fact that each compilation unit is compiled separately, knowing only a fragment of the whole program (i.e. the current compilation unit) rather than the whole program.

1 files changed, 33 insertions, 48 deletions

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.