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, 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.