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, 66 insertions, 56 deletions

diff --git a/backend/Inliningspec.v b/backend/Inliningspec.v
index ba62313f..23770cb7 100644
--- a/backend/Inliningspec.v
+++ b/backend/Inliningspec.v
@@ -12,64 +12,60 @@
 
 (** RTL function inlining: relational specification *)
 
-Require Import Coqlib.
-Require Import Wfsimpl.
-Require Import Errors.
-Require Import Maps.
-Require Import AST.
-Require Import Integers.
-Require Import Globalenvs.
-Require Import Op.
-Require Import Registers.
-Require Import RTL.
+Require Import Coqlib Wfsimpl Maps Errors Integers.
+Require Import AST Linking.
+Require Import Op Registers RTL.
 Require Import Inlining.
 
 (** ** Soundness of function environments. *)
 
-(** A (compile-time) function environment is compatible with a
-  (run-time) global environment if the following condition holds. *)
+(** A compile-time function environment is compatible with a whole
+  program if the following condition holds. *)
 
-Definition fenv_compat (ge: genv) (fenv: funenv) : Prop :=
-  forall id b f,
-  fenv!id = Some f -> Genv.find_symbol ge id = Some b ->
-  Genv.find_funct_ptr ge b = Some (Internal f).
+Definition fenv_compat (p: program) (fenv: funenv) : Prop :=
+  forall id f,
+  fenv!id = Some f -> (prog_defmap p)!id = Some (Gfun (Internal f)).
 
-Remark add_globdef_compat:
-  forall ge fenv idg,
-  fenv_compat ge fenv ->
-  fenv_compat (Genv.add_global ge idg) (Inlining.add_globdef fenv idg).
+Lemma funenv_program_compat:
+  forall p, fenv_compat p (funenv_program p).
 Proof.
-  intros. destruct idg as [id gd]. red; simpl; intros.
-  unfold Genv.find_symbol in H1; simpl in H1.
-  unfold Genv.find_funct_ptr; simpl.
-  rewrite PTree.gsspec in H1. destruct (peq id0 id).
-  (* same *)
-  subst id0. inv H1. destruct gd. destruct f0.
-  destruct (should_inline id f0).
-  rewrite PTree.gss in H0. rewrite PTree.gss. inv H0; auto.
-  rewrite PTree.grs in H0; discriminate.
-  rewrite PTree.grs in H0; discriminate.
-  rewrite PTree.grs in H0; discriminate.
-  (* different *)
-  destruct gd. rewrite PTree.gso. eapply H; eauto.
-  destruct f0. destruct (should_inline id f0).
-  rewrite PTree.gso in H0; auto.
-  rewrite PTree.gro in H0; auto.
-  rewrite PTree.gro in H0; auto.
-  red; intros; subst b. eelim Plt_strict. eapply Genv.genv_symb_range; eauto.
-  rewrite PTree.gro in H0; auto. eapply H; eauto.
+  set (P := fun (dm: PTree.t (globdef fundef unit)) (fenv: funenv) =>
+              forall id f,
+              fenv!id = Some f -> dm!id = Some (Gfun (Internal f))).
+  assert (REMOVE: forall dm fenv id g,
+             P dm fenv ->
+             P (PTree.set id g dm) (PTree.remove id fenv)).
+  { unfold P; intros. rewrite PTree.grspec in H0. destruct (PTree.elt_eq id0 id).
+    discriminate.
+    rewrite PTree.gso; auto.
+  }
+  assert (ADD: forall dm fenv idg,
+             P dm fenv ->
+             P (PTree.set (fst idg) (snd idg) dm) (add_globdef fenv idg)).
+  { intros dm fenv [id g]; simpl; intros.
+    destruct g as [ [f|ef] | v]; auto.
+    destruct (should_inline id f); auto.
+    red; intros. rewrite ! PTree.gsspec in *.
+    destruct (peq id0 id); auto. inv H0; auto.
+  }
+  assert (REC: forall l dm fenv,
+            P dm fenv ->
+            P (fold_left (fun x idg => PTree.set (fst idg) (snd idg) x) l dm)
+              (fold_left add_globdef l fenv)).
+  { induction l; simpl; intros. 
+  - auto.
+  - apply IHl. apply ADD; auto. 
+  }
+  intros. apply REC. red; intros.  rewrite PTree.gempty in H; discriminate.
 Qed.
 
-Lemma funenv_program_compat:
-  forall p, fenv_compat (Genv.globalenv p) (funenv_program p).
+Lemma fenv_compat_linkorder:
+  forall cunit prog fenv,
+  linkorder cunit prog -> fenv_compat cunit fenv -> fenv_compat prog fenv.
 Proof.
-  intros.
-  unfold Genv.globalenv, funenv_program.
-  assert (forall gl ge fenv,
-         fenv_compat ge fenv ->
-         fenv_compat (Genv.add_globals ge gl) (fold_left add_globdef gl fenv)).
-    induction gl; simpl; intros. auto. apply IHgl. apply add_globdef_compat; auto.
-  apply H. red; intros. rewrite PTree.gempty in H0; discriminate.
+  intros; red; intros. apply H0 in H1. 
+  destruct (prog_defmap_linkorder _ _ _ _ H H1) as (gd' & P & Q). 
+  inv Q. inv H3. auto.
 Qed.
 
 (** ** Properties of shifting *)
@@ -684,29 +680,45 @@ Qed.
 
 End INLINING_BODY_SPEC.
 
+End INLINING_SPEC.
+
 (** ** Relational specification of the translation of a function *)
 
-Inductive tr_function: function -> function -> Prop :=
-  | tr_function_intro: forall f f' ctx,
-      tr_funbody f'.(fn_stacksize) ctx f f'.(fn_code) ->
+Inductive tr_function: program -> function -> function -> Prop :=
+  | tr_function_intro: forall p fenv f f' ctx,
+      fenv_compat p fenv ->
+      tr_funbody fenv f'.(fn_stacksize) ctx f f'.(fn_code) ->
       ctx.(dstk) = 0 ->
       ctx.(retinfo) = None ->
       f'.(fn_sig) = f.(fn_sig) ->
       f'.(fn_params) = sregs ctx f.(fn_params) ->
       f'.(fn_entrypoint) = spc ctx f.(fn_entrypoint) ->
       0 <= fn_stacksize f' < Int.max_unsigned ->
-      tr_function f f'.
+      tr_function p f f'.
+
+Lemma tr_function_linkorder:
+  forall cunit prog f f',
+  linkorder cunit prog ->
+  tr_function cunit f f' ->
+  tr_function prog f f'.
+Proof.
+  intros. inv H0. econstructor; eauto. eapply fenv_compat_linkorder; eauto. 
+Qed.
 
 Lemma transf_function_spec:
-  forall f f', transf_function fenv f = OK f' -> tr_function f f'.
+  forall cunit f f',
+  transf_function (funenv_program cunit) f = OK f' ->
+  tr_function cunit f f'.
 Proof.
   intros. unfold transf_function in H.
+  set (fenv := funenv_program cunit) in *.
   destruct (expand_function fenv f initstate) as [ctx s i] eqn:?.
   destruct (zlt (st_stksize s) Int.max_unsigned); inv H.
   monadInv Heqr. set (ctx := initcontext x x0 (max_reg_function f) (fn_stacksize f)) in *.
 Opaque initstate.
   destruct INCR3. inversion EQ1. inversion EQ.
-  apply tr_function_intro with ctx; auto.
+  apply tr_function_intro with fenv ctx; auto.
+  apply funenv_program_compat.
   eapply expand_cfg_spec with (fe := fenv); eauto.
     red; auto.
     unfold ctx; rewrite <- H1; rewrite <- H2; rewrite <- H3; simpl. xomega.
@@ -718,5 +730,3 @@ Opaque initstate.
   simpl. split; auto. destruct INCR2. destruct INCR1. destruct INCR0. destruct INCR.
   simpl. change 0 with (st_stksize initstate). omega.
 Qed.
-
-End INLINING_SPEC.