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.

3 files changed, 32 insertions, 62 deletions

diff --git a/ia32/Asmexpand.ml b/ia32/Asmexpand.ml
index 7ca31902..61beeb00 100644
--- a/ia32/Asmexpand.ml
+++ b/ia32/Asmexpand.ml
@@ -460,4 +460,4 @@ let expand_fundef id = function
       Errors.OK (External ef)
 
 let expand_program (p: Asm.program) : Asm.program Errors.res =
-  AST.transform_partial_ident_program expand_fundef p
+  AST.transform_partial_program2 expand_fundef (fun id v -> Errors.OK v) p
diff --git a/ia32/Asmgen.v b/ia32/Asmgen.v
index 91122898..fd0d5bc5 100644
--- a/ia32/Asmgen.v
+++ b/ia32/Asmgen.v
@@ -12,16 +12,9 @@
 
 (** Translation from Mach to IA32 Asm. *)
 
-Require Import Coqlib.
-Require Import Errors.
-Require Import AST.
-Require Import Integers.
-Require Import Floats.
-Require Import Memdata.
-Require Import Op.
-Require Import Locations.
-Require Import Mach.
-Require Import Asm.
+Require Import Coqlib Errors.
+Require Import Integers Floats AST Memdata.
+Require Import Op Locations Mach Asm.
 
 Open Local Scope string_scope.
 Open Local Scope error_monad_scope.
diff --git a/ia32/Asmgenproof.v b/ia32/Asmgenproof.v
index 105347e7..28237237 100644
--- a/ia32/Asmgenproof.v
+++ b/ia32/Asmgenproof.v
@@ -12,56 +12,43 @@
 
 (** Correctness proof for x86 generation: main proof. *)
 
-Require Import Coqlib.
-Require Import Errors.
-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 Locations.
-Require Import Mach.
-Require Import Conventions.
-Require Import Asm.
-Require Import Asmgen.
-Require Import Asmgenproof0.
-Require Import Asmgenproof1.
+Require Import Coqlib Errors.
+Require Import Integers Floats AST Linking.
+Require Import Values Memory Events Globalenvs Smallstep.
+Require Import Op Locations Mach Conventions Asm.
+Require Import Asmgen Asmgenproof0 Asmgenproof1.
+
+Definition match_prog (p: Mach.program) (tp: Asm.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.
 
 Section PRESERVATION.
 
 Variable prog: Mach.program.
 Variable tprog: Asm.program.
-Hypothesis TRANSF: transf_program prog = Errors.OK tprog.
-
+Hypothesis TRANSF: match_prog prog tprog.
 Let ge := Genv.globalenv prog.
 Let tge := Genv.globalenv tprog.
 
 Lemma symbols_preserved:
-  forall id, Genv.find_symbol tge id = Genv.find_symbol ge id.
-Proof.
-  intros. unfold ge, tge.
-  apply Genv.find_symbol_transf_partial with transf_fundef.
-  exact TRANSF.
-Qed.
+  forall (s: ident), Genv.find_symbol tge s = Genv.find_symbol ge s.
+Proof (Genv.find_symbol_match TRANSF).
 
-Lemma public_preserved:
-  forall id, Genv.public_symbol tge id = Genv.public_symbol ge id.
-Proof.
-  intros. unfold ge, tge.
-  apply Genv.public_symbol_transf_partial with transf_fundef.
-  exact TRANSF.
-Qed.
+Lemma senv_preserved:
+  Senv.equiv ge tge.
+Proof (Genv.senv_match TRANSF).
 
 Lemma functions_translated:
   forall b f,
   Genv.find_funct_ptr ge b = Some f ->
-  exists tf, Genv.find_funct_ptr tge b = Some tf /\ transf_fundef f = Errors.OK tf.
-Proof
-  (Genv.find_funct_ptr_transf_partial transf_fundef _ TRANSF).
+  exists tf,
+  Genv.find_funct_ptr tge b = Some tf /\ transf_fundef f = OK tf.
+Proof (Genv.find_funct_ptr_transf_partial TRANSF).
 
 Lemma functions_transl:
   forall fb f tf,
@@ -73,14 +60,6 @@ Proof.
   monadInv B. rewrite H0 in EQ; inv EQ; auto.
 Qed.
 
-Lemma varinfo_preserved:
-  forall b, Genv.find_var_info tge b = Genv.find_var_info ge b.
-Proof.
-  intros. unfold ge, tge.
-  apply Genv.find_var_info_transf_partial with transf_fundef.
-  exact TRANSF.
-Qed.
-
 (** * Properties of control flow *)
 
 Lemma transf_function_no_overflow:
@@ -682,8 +661,7 @@ Opaque loadind.
   eapply find_instr_tail; eauto.
   erewrite <- sp_val by 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.
   eauto.
   econstructor; eauto.
   instantiate (2 := tf); instantiate (1 := x).
@@ -866,8 +844,7 @@ Transparent destroyed_at_function_entry.
   intros [res' [m2' [P [Q [R S]]]]].
   left; econstructor; split.
   apply plus_one. eapply exec_step_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.
   econstructor; eauto.
   unfold loc_external_result.
   apply agree_set_other; auto. apply agree_set_mregs; auto.
@@ -885,7 +862,7 @@ Proof.
   intros. inversion H. unfold ge0 in *.
   econstructor; split.
   econstructor.
-  eapply Genv.init_mem_transf_partial; eauto.
+  eapply (Genv.init_mem_transf_partial TRANSF); eauto.
   replace (Genv.symbol_address (Genv.globalenv tprog) (prog_main tprog) Int.zero)
      with (Vptr fb Int.zero).
   econstructor; eauto.
@@ -893,7 +870,7 @@ Proof.
   apply Mem.extends_refl.
   split. auto. simpl. unfold Vzero; congruence. intros. rewrite Regmap.gi. auto.
   unfold Genv.symbol_address.
-  rewrite (transform_partial_program_main _ _ TRANSF).
+  rewrite (match_program_main TRANSF).
   rewrite symbols_preserved.
   unfold ge; rewrite H1. auto.
 Qed.
@@ -911,7 +888,7 @@ Theorem transf_program_correct:
   forward_simulation (Mach.semantics return_address_offset prog) (Asm.semantics tprog).
 Proof.
   eapply forward_simulation_star with (measure := measure).
-  eexact public_preserved.
+  apply senv_preserved.
   eexact transf_initial_states.
   eexact transf_final_states.
   exact step_simulation.