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, 329 insertions, 231 deletions

diff --git a/backend/Selectionproof.v b/backend/Selectionproof.v
index 8051df59..aad3add4 100644
--- a/backend/Selectionproof.v
+++ b/backend/Selectionproof.v
@@ -15,6 +15,7 @@
 Require Import Coqlib.
 Require Import Maps.
 Require Import AST.
+Require Import Linking.
 Require Import Errors.
 Require Import Integers.
 Require Import Values.
@@ -37,6 +38,92 @@ Require Import SelectLongproof.
 Local Open Scope cminorsel_scope.
 Local Open Scope error_monad_scope.
 
+(** * Relational specification of instruction selection *)
+
+Definition match_fundef (cunit: Cminor.program) (f: Cminor.fundef) (tf: CminorSel.fundef) : Prop :=
+  exists hf, helper_functions_declared cunit hf /\ sel_fundef (prog_defmap cunit) hf f = OK tf.
+
+Definition match_prog (p: Cminor.program) (tp: CminorSel.program) :=
+  match_program match_fundef eq p tp.
+
+(** Processing of helper functions *)
+
+Lemma record_globdefs_sound:
+  forall dm id gd, (record_globdefs dm)!id = Some gd -> dm!id = Some gd.
+Proof.
+  intros. 
+  set (f := fun m id gd => if globdef_of_interest gd then PTree.set id gd m else m) in *.
+  set (P := fun m m' => m'!id = Some gd -> m!id = Some gd).
+  assert (X: P dm (PTree.fold f dm (PTree.empty _))).
+  { apply PTree_Properties.fold_rec.
+  - unfold P; intros. rewrite <- H0; auto.
+  - red. rewrite ! PTree.gempty. auto.
+  - unfold P; intros. rewrite PTree.gsspec. unfold f in H3. 
+    destruct (globdef_of_interest v).
+    + rewrite PTree.gsspec in H3. destruct (peq id k); auto.
+    + apply H2 in H3. destruct (peq id k). congruence. auto. }
+  apply X. auto.
+Qed.
+
+Lemma lookup_helper_correct_1:
+  forall globs name sg id,
+  lookup_helper globs name sg = OK id ->
+  globs!id = Some (Gfun (External (EF_runtime name sg))).
+Proof.
+  intros.
+  set (P := fun (m: PTree.t globdef) res => res = Some id -> m!id = Some(Gfun(External (EF_runtime name sg)))).
+  assert (P globs (PTree.fold (lookup_helper_aux name sg) globs None)).
+  { apply PTree_Properties.fold_rec; red; intros.
+  - rewrite <- H0. apply H1; auto.
+  - discriminate.
+  - assert (EITHER: k = id /\ v = Gfun (External (EF_runtime name sg))
+                \/  a = Some id).
+    { unfold lookup_helper_aux in H3. destruct v; auto. destruct f; auto. destruct e; auto.
+      destruct (String.string_dec name name0); auto.
+      destruct (signature_eq sg sg0); auto.
+      inversion H3. left; split; auto. repeat f_equal; auto. }
+    destruct EITHER as [[X Y] | X].
+    subst k v. apply PTree.gss.
+    apply H2 in X. rewrite PTree.gso by congruence. auto.
+  }
+  red in H0. unfold lookup_helper in H.
+  destruct (PTree.fold (lookup_helper_aux name sg) globs None); inv H. auto.
+Qed.
+
+Lemma lookup_helper_correct:
+  forall p name sg id,
+  lookup_helper (record_globdefs (prog_defmap p)) name sg = OK id ->
+  helper_declared p id name sg.
+Proof.
+  intros. apply lookup_helper_correct_1 in H. apply record_globdefs_sound in H. auto.
+Qed.
+
+Lemma get_helpers_correct:
+  forall p hf,
+  get_helpers (prog_defmap p) = OK hf -> helper_functions_declared p hf.
+Proof.
+  intros. monadInv H. red; simpl. auto 20 using lookup_helper_correct.
+Qed.
+
+Theorem transf_program_match:
+  forall p tp, sel_program p = OK tp -> match_prog p tp.
+Proof.
+  intros. monadInv H. 
+  eapply match_transform_partial_program_contextual. eexact EQ0.
+  intros. exists x; split; auto. apply get_helpers_correct; auto.
+Qed.
+
+Lemma helper_functions_declared_linkorder:
+  forall (p p': Cminor.program) hf,
+  helper_functions_declared p hf -> linkorder p p' -> helper_functions_declared p' hf.
+Proof.
+  intros. 
+  assert (X: forall id name sg, helper_declared p id name sg -> helper_declared p' id name sg).
+  { unfold helper_declared; intros.
+    destruct (prog_defmap_linkorder _ _ _ _ H0 H1) as (gd & P & Q). 
+    inv Q. inv H3. auto. }
+  red in H. decompose [Logic.and] H; clear H. red; auto 20.
+Qed.
 
 (** * Correctness of the instruction selection functions for expressions *)
 
@@ -46,75 +133,68 @@ Variable prog: Cminor.program.
 Variable tprog: CminorSel.program.
 Let ge := Genv.globalenv prog.
 Let tge := Genv.globalenv tprog.
-Variable hf: helper_functions.
-Hypothesis HELPERS: helper_functions_declared ge hf.
-Hypothesis TRANSFPROG: transform_partial_program (sel_fundef hf ge) prog = OK tprog.
+Hypothesis TRANSF: match_prog prog tprog.
 
 Lemma symbols_preserved:
   forall (s: ident), Genv.find_symbol tge s = Genv.find_symbol ge s.
-Proof.
-  intros. eapply Genv.find_symbol_transf_partial; eauto.
-Qed.
+Proof (Genv.find_symbol_match TRANSF).
 
-Lemma public_preserved:
-  forall (s: ident), Genv.public_symbol tge s = Genv.public_symbol ge s.
-Proof.
-  intros. eapply Genv.public_symbol_transf_partial; eauto.
-Qed.
+Lemma senv_preserved:
+  Senv.equiv (Genv.to_senv ge) (Genv.to_senv tge).
+Proof (Genv.senv_match TRANSF).
 
 Lemma function_ptr_translated:
   forall (b: block) (f: Cminor.fundef),
   Genv.find_funct_ptr ge b = Some f ->
-  exists tf, Genv.find_funct_ptr tge b = Some tf /\ sel_fundef hf ge f = OK tf.
-Proof.
-  intros. eapply Genv.find_funct_ptr_transf_partial; eauto.
-Qed.
+  exists cu tf, Genv.find_funct_ptr tge b = Some tf /\ match_fundef cu f tf /\ linkorder cu prog.
+Proof (Genv.find_funct_ptr_match TRANSF).
 
 Lemma functions_translated:
   forall (v v': val) (f: Cminor.fundef),
   Genv.find_funct ge v = Some f ->
   Val.lessdef v v' ->
-  exists tf, Genv.find_funct tge v' = Some tf /\ sel_fundef hf ge f = OK tf.
+  exists cu tf, Genv.find_funct tge v' = Some tf /\ match_fundef cu f tf /\ linkorder cu prog.
 Proof.
   intros. inv H0.
-  eapply Genv.find_funct_transf_partial; eauto.
-  simpl in H. discriminate.
+  eapply Genv.find_funct_match; eauto. 
+  discriminate.
 Qed.
 
 Lemma sig_function_translated:
-  forall f tf, sel_fundef hf ge f = OK tf -> funsig tf = Cminor.funsig f.
+  forall cu f tf, match_fundef cu f tf -> funsig tf = Cminor.funsig f.
 Proof.
-  intros. destruct f; monadInv H; auto. monadInv EQ. auto.
+  intros. destruct H as (hf & P & Q). destruct f; monadInv Q; auto. monadInv EQ; auto.
 Qed.
 
 Lemma stackspace_function_translated:
-  forall f tf, sel_function hf ge f = OK tf -> fn_stackspace tf = Cminor.fn_stackspace f.
+  forall dm hf f tf, sel_function dm hf f = OK tf -> fn_stackspace tf = Cminor.fn_stackspace f.
 Proof.
   intros. monadInv H. auto.
 Qed.
 
-Lemma varinfo_preserved:
-  forall b, Genv.find_var_info tge b = Genv.find_var_info ge b.
+Lemma helper_functions_preserved:
+  forall hf, helper_functions_declared prog hf -> helper_functions_declared tprog hf.
 Proof.
-  intros; eapply Genv.find_var_info_transf_partial; eauto.
+  assert (X: forall id name sg, helper_declared prog id name sg -> helper_declared tprog id name sg).
+  { unfold helper_declared; intros. 
+    generalize (match_program_defmap _ _ _ _ _ TRANSF id).
+    unfold Cminor.fundef; rewrite H; intros R; inv R. inv H2.
+    destruct H4 as (cu & A & B). monadInv B. auto. }
+  unfold helper_functions_declared; intros. decompose [Logic.and] H; clear H. auto 20. 
 Qed.
 
-Lemma helper_declared_preserved:
-  forall id name sg, helper_declared ge id name sg -> helper_declared tge id name sg.
-Proof.
-  intros id name sg (b & A & B).
-  exploit function_ptr_translated; eauto. simpl. intros (tf & P & Q). inv Q.
-  exists b; split; auto. rewrite symbols_preserved. auto.
-Qed.
+Section CMCONSTR.
+
+Variable cunit: Cminor.program.
+Variable hf: helper_functions.
+Hypothesis LINK: linkorder cunit prog.
+Hypothesis HF: helper_functions_declared cunit hf.
 
-Let HELPERS': helper_functions_declared tge hf.
+Let HF': helper_functions_declared tprog hf.
 Proof.
-  red in HELPERS; decompose [Logic.and] HELPERS.
-  red. auto 20 using helper_declared_preserved.
+  apply helper_functions_preserved. eapply helper_functions_declared_linkorder; eauto.
 Qed.
 
-Section CMCONSTR.
-
 Variable sp: val.
 Variable e: env.
 Variable m: mem.
@@ -172,6 +252,7 @@ Lemma eval_sel_unop:
   forall le op a1 v1 v,
   eval_expr tge sp e m le a1 v1 ->
   eval_unop op v1 = Some v ->
+  
   exists v', eval_expr tge sp e m le (sel_unop hf op a1) v' /\ Val.lessdef v v'.
 Proof.
   destruct op; simpl; intros; FuncInv; try subst v.
@@ -276,26 +357,30 @@ Proof.
 Qed.
 
 Lemma classify_call_correct:
-  forall sp e m a v fd,
+  forall unit sp e m a v fd,
+  linkorder unit prog ->
   Cminor.eval_expr ge sp e m a v ->
   Genv.find_funct ge v = Some fd ->
-  match classify_call ge a with
+  match classify_call (prog_defmap unit) a with
   | Call_default => True
   | Call_imm id => exists b, Genv.find_symbol ge id = Some b /\ v = Vptr b Int.zero
   | Call_builtin ef => fd = External ef
   end.
 Proof.
   unfold classify_call; intros.
-  destruct (expr_is_addrof_ident a) as [id|] eqn:?.
+  destruct (expr_is_addrof_ident a) as [id|] eqn:EA; auto.
   exploit expr_is_addrof_ident_correct; eauto. intros EQ; subst a.
-  inv H. inv H2.
-  destruct (Genv.find_symbol ge id) as [b|] eqn:?.
-  rewrite Genv.find_funct_find_funct_ptr in H0.
-  rewrite H0.
-  destruct fd. exists b; auto.
-  destruct (ef_inline e0). auto. exists b; auto.
-  simpl in H0. discriminate.
-  auto.
+  inv H0. inv H3.
+  destruct (Genv.find_symbol ge id) as [b|] eqn:FS; try discriminate.
+  rewrite Genv.find_funct_find_funct_ptr in H1. 
+  assert (DFL: exists b1, Genv.find_symbol ge id = Some b1 /\ Vptr b Int.zero = Vptr b1 Int.zero) by (exists b; auto).
+  unfold globdef; destruct (prog_defmap unit)!id as [[[f|ef] |gv] |] eqn:G; auto.
+  destruct (ef_inline ef) eqn:INLINE; auto.
+  destruct (prog_defmap_linkorder _ _ _ _ H G) as (gd & P & Q).
+  inv Q. inv H2. 
+- apply Genv.find_def_symbol in P. destruct P as (b' & X & Y). fold ge in X, Y. 
+  rewrite <- Genv.find_funct_ptr_iff in Y. congruence.
+- simpl in INLINE. discriminate.
 Qed.
 
 (** Translation of [switch] statements *)
@@ -547,6 +632,13 @@ Qed.
 
 (** Semantic preservation for expressions. *)
 
+Section EXPRESSIONS.
+
+Variable cunit: Cminor.program.
+Variable hf: helper_functions.
+Hypothesis LINK: linkorder cunit prog.
+Hypothesis HF: helper_functions_declared cunit hf.
+
 Lemma sel_expr_correct:
   forall sp e m a v,
   Cminor.eval_expr ge sp e m a v ->
@@ -576,7 +668,7 @@ Proof.
   exploit IHeval_expr1; eauto. intros [v1' [A B]].
   exploit IHeval_expr2; eauto. intros [v2' [C D]].
   exploit eval_binop_lessdef; eauto. intros [v' [E F]].
-  exploit eval_sel_binop. eexact A. eexact C. eauto. intros [v'' [P Q]].
+  exploit eval_sel_binop. eexact LINK. eexact HF. eexact A. eexact C. eauto. intros [v'' [P Q]].
   exists v''; split; eauto. eapply Val.lessdef_trans; eauto.
   (* Eload *)
   exploit IHeval_expr; eauto. intros [vaddr' [A B]].
@@ -641,51 +733,89 @@ Proof.
   intros. destruct oid; simpl; auto. apply set_var_lessdef; auto.
 Qed.
 
+End EXPRESSIONS.
+
 (** Semantic preservation for functions and statements. *)
 
-Inductive match_cont: Cminor.cont -> CminorSel.cont -> Prop :=
-  | match_cont_stop:
-      match_cont Cminor.Kstop Kstop
-  | match_cont_seq: forall s s' k k',
-      sel_stmt hf ge s = OK s' ->
-      match_cont k k' ->
-      match_cont (Cminor.Kseq s k) (Kseq s' k')
-  | match_cont_block: forall k k',
-      match_cont k k' ->
-      match_cont (Cminor.Kblock k) (Kblock k')
-  | match_cont_call: forall id f sp e k f' e' k',
-      sel_function hf ge f = OK f' ->
-      match_cont k k' -> env_lessdef e e' ->
-      match_cont (Cminor.Kcall id f sp e k) (Kcall id f' sp e' k').
+(*
+Inductive match_call_cont: Cminor.cont -> CminorSel.cont -> Prop :=
+  | match_call_cont_stop:
+      match_call_cont Cminor.Kstop Kstop
+  | match_call_cont_call: forall cunit hf id f sp e k f' e' k',
+      linkorder cunit prog ->
+      helper_functions_declared cunit hf ->
+      sel_function (prog_defmap cunit) hf f = OK f' ->
+      match_cont cunit hf k k' -> env_lessdef e e' ->
+      match_call_cont (Cminor.Kcall id f sp e k) (Kcall id f' sp e' k')
+
+with match_cont: Cminor.program -> helper_functions -> Cminor.cont -> CminorSel.cont -> Prop :=
+  | match_cont_stop: forall cunit hf,
+      match_cont cunit hf Cminor.Kstop Kstop
+  | match_cont_seq: forall cunit hf s s' k k',
+      sel_stmt (prog_defmap cunit) hf s = OK s' ->
+      match_cont cunit hf k k' ->
+      match_cont cunit hf (Cminor.Kseq s k) (Kseq s' k')
+  | match_cont_block: forall cunit hf k k',
+      match_cont cunit hf k k' ->
+      match_cont cunit hf (Cminor.Kblock k) (Kblock k')
+  | match_cont_call: forall cunit hf id f sp e k f' e' k',
+      match_call_cont (Cminor.Kcall id f sp e k) (Kcall id f' sp e' k') ->
+      match_cont cunit hf (Cminor.Kcall id f sp e k) (Kcall id f' sp e' k').
+*)
+
+Inductive match_cont: Cminor.program -> helper_functions -> Cminor.cont -> CminorSel.cont -> Prop :=
+  | match_cont_stop: forall cunit hf,
+      match_cont cunit hf Cminor.Kstop Kstop
+  | match_cont_seq: forall cunit hf s s' k k',
+      sel_stmt (prog_defmap cunit) hf s = OK s' ->
+      match_cont cunit hf k k' ->
+      match_cont cunit hf (Cminor.Kseq s k) (Kseq s' k')
+  | match_cont_block: forall cunit hf k k',
+      match_cont cunit hf k k' ->
+      match_cont cunit hf (Cminor.Kblock k) (Kblock k')
+  | match_cont_call: forall cunit' hf' cunit hf id f sp e k f' e' k',
+      linkorder cunit prog ->
+      helper_functions_declared cunit hf ->
+      sel_function (prog_defmap cunit) hf f = OK f' ->
+      match_cont cunit hf k k' -> env_lessdef e e' ->
+      match_cont cunit' hf' (Cminor.Kcall id f sp e k) (Kcall id f' sp e' k').
+
+Definition match_call_cont (k: Cminor.cont) (k': CminorSel.cont) : Prop :=
+  forall cunit hf, match_cont cunit hf k k'.
 
 Inductive match_states: Cminor.state -> CminorSel.state -> Prop :=
-  | match_state: forall f f' s k s' k' sp e m e' m'
-        (TF: sel_function hf ge f = OK f')
-        (TS: sel_stmt hf ge s = OK s')
-        (MC: match_cont k k')
+  | match_state: forall cunit hf f f' s k s' k' sp e m e' m'
+        (LINK: linkorder cunit prog)
+        (HF: helper_functions_declared cunit hf)
+        (TF: sel_function (prog_defmap cunit) hf f = OK f')
+        (TS: sel_stmt (prog_defmap cunit) hf s = OK s')
+        (MC: match_cont cunit hf k k')
         (LD: env_lessdef e e')
         (ME: Mem.extends m m'),
       match_states
         (Cminor.State f s k sp e m)
         (State f' s' k' sp e' m')
-  | match_callstate: forall f f' args args' k k' m m'
-        (TF: sel_fundef hf ge f = OK f')
-        (MC: match_cont k k')
+  | match_callstate: forall cunit f f' args args' k k' m m'
+        (LINK: linkorder cunit prog)
+        (TF: match_fundef cunit f f')
+        (MC: match_call_cont k k')
         (LD: Val.lessdef_list args args')
         (ME: Mem.extends m m'),
       match_states
         (Cminor.Callstate f args k m)
         (Callstate f' args' k' m')
   | match_returnstate: forall v v' k k' m m'
-        (MC: match_cont k k')
+        (MC: match_call_cont k k')
         (LD: Val.lessdef v v')
         (ME: Mem.extends m m'),
       match_states
         (Cminor.Returnstate v k m)
         (Returnstate v' k' m')
-  | match_builtin_1: forall ef args args' optid f sp e k m al f' e' k' m'
-        (TF: sel_function hf ge f = OK f')
-        (MC: match_cont k k')
+  | match_builtin_1: forall cunit hf ef args args' optid f sp e k m al f' e' k' m'
+        (LINK: linkorder cunit prog)
+        (HF: helper_functions_declared cunit hf)
+        (TF: sel_function (prog_defmap cunit) hf f = OK f')
+        (MC: match_cont cunit hf k k')
         (LDA: Val.lessdef_list args args')
         (LDE: env_lessdef e e')
         (ME: Mem.extends m m')
@@ -693,9 +823,11 @@ Inductive match_states: Cminor.state -> CminorSel.state -> Prop :=
       match_states
         (Cminor.Callstate (External ef) args (Cminor.Kcall optid f sp e k) m)
         (State f' (Sbuiltin (sel_builtin_res optid) ef al) k' sp e' m')
-  | match_builtin_2: forall v v' optid f sp e k m f' e' m' k'
-        (TF: sel_function hf ge f = OK f')
-        (MC: match_cont k k')
+  | match_builtin_2: forall cunit hf v v' optid f sp e k m f' e' m' k'
+        (LINK: linkorder cunit prog)
+        (HF: helper_functions_declared cunit hf)
+        (TF: sel_function (prog_defmap cunit) hf f = OK f')
+        (MC: match_cont cunit hf k k')
         (LDV: Val.lessdef v v')
         (LDE: env_lessdef e e')
         (ME: Mem.extends m m'),
@@ -703,19 +835,50 @@ Inductive match_states: Cminor.state -> CminorSel.state -> Prop :=
         (Cminor.Returnstate v (Cminor.Kcall optid f sp e k) m)
         (State f' Sskip k' sp (set_builtin_res (sel_builtin_res optid) v' e') m').
 
+(*
+Remark call_cont_commut_1:
+  forall cunit hf k k', match_cont cunit hf k k' ->
+  forall cunit' hf', match_cont cunit' hf' (Cminor.call_cont k) (call_cont k').
+Proof.
+  induction 1; simpl; auto; intros; econstructor; eauto.
+Qed.
+
+Remark call_cont_commut_2:
+  forall cunit hf k k', match_cont cunit hf k k' -> match_cont cunit hf (Cminor.call_cont k) (call_cont k').
+Proof.
+  intros. eapply call_cont_commut_1; eauto.
+Qed.
+*)
+
 Remark call_cont_commut:
-  forall k k', match_cont k k' -> match_cont (Cminor.call_cont k) (call_cont k').
+  forall cunit hf k k', match_cont cunit hf k k' -> match_call_cont (Cminor.call_cont k) (call_cont k').
 Proof.
-  induction 1; simpl; auto. constructor. constructor; auto.
+  induction 1; simpl; auto; red; intros; econstructor; eauto.
+Qed.
+
+Remark match_is_call_cont:
+  forall cunit hf k k', match_cont cunit hf k k' -> Cminor.is_call_cont k -> match_call_cont k k'.
+Proof.
+  destruct 1; intros; try contradiction; red; intros; econstructor; eauto.
+Qed.
+
+Remark match_call_cont_cont:
+  forall k k', match_call_cont k k' -> exists cunit hf, match_cont cunit hf k k'.
+Proof.
+  intros. refine (let cunit : Cminor.program := _ in _). 
+  econstructor. apply nil. apply nil. apply xH.
+  refine (let hf : helper_functions := _ in _).
+  econstructor; apply xH.
+  exists cunit, hf; auto.
 Qed.
 
 Remark find_label_commut:
-  forall lbl s k s' k',
-  match_cont k k' ->
-  sel_stmt hf ge s = OK s' ->
+  forall cunit hf lbl s k s' k',
+  match_cont cunit hf k k' ->
+  sel_stmt (prog_defmap cunit) hf s = OK s' ->
   match Cminor.find_label lbl s k, find_label lbl s' k' with
   | None, None => True
-  | Some(s1, k1), Some(s1', k1') => sel_stmt hf ge s1 = OK s1' /\ match_cont k1 k1'
+  | Some(s1, k1), Some(s1', k1') => sel_stmt (prog_defmap cunit) hf s1 = OK s1' /\ match_cont cunit hf k1 k1'
   | _, _ => False
   end.
 Proof.
@@ -723,9 +886,9 @@ Proof.
 (* store *)
   unfold store. destruct (addressing m (sel_expr hf e)); simpl; auto.
 (* call *)
-  destruct (classify_call ge e); simpl; auto.
+  destruct (classify_call (prog_defmap cunit) e); simpl; auto.
 (* tailcall *)
-  destruct (classify_call ge e); simpl; auto.
+  destruct (classify_call (prog_defmap cunit) e); simpl; auto.
 (* seq *)
   exploit (IHs1 (Cminor.Kseq s2 k)). constructor; eauto. eauto.
   destruct (Cminor.find_label lbl s1 (Cminor.Kseq s2 k)) as [[sx kx] | ];
@@ -767,48 +930,50 @@ Lemma sel_step_correct:
 Proof.
   induction 1; intros T1 ME; inv ME; try (monadInv TS).
 - (* skip seq *)
-  inv MC. left; econstructor; split. econstructor. constructor; auto.
+  inv MC. left; econstructor; split. econstructor. econstructor; eauto.
 - (* skip block *)
-  inv MC. left; econstructor; split. econstructor. constructor; auto.
+  inv MC. left; econstructor; split. econstructor. econstructor; eauto.
 - (* skip call *)
   exploit Mem.free_parallel_extends; eauto. intros [m2' [A B]].
   left; econstructor; split.
   econstructor. inv MC; simpl in H; simpl; auto.
   eauto.
   erewrite stackspace_function_translated; eauto.
-  constructor; auto.
+  econstructor; eauto. eapply match_is_call_cont; eauto.
 - (* assign *)
   exploit sel_expr_correct; eauto. intros [v' [A B]].
   left; econstructor; split.
   econstructor; eauto.
-  constructor; auto. apply set_var_lessdef; auto.
+  econstructor; eauto. apply set_var_lessdef; auto.
 - (* store *)
-  exploit sel_expr_correct. eexact H. eauto. eauto. intros [vaddr' [A B]].
-  exploit sel_expr_correct. eexact H0. eauto. eauto. intros [v' [C D]].
+  exploit sel_expr_correct. eauto. eauto. eexact H. eauto. eauto. intros [vaddr' [A B]].
+  exploit sel_expr_correct. eauto. eauto. eexact H0. eauto. eauto. intros [v' [C D]].
   exploit Mem.storev_extends; eauto. intros [m2' [P Q]].
   left; econstructor; split.
   eapply eval_store; eauto.
-  constructor; auto.
+  econstructor; eauto.
 - (* Scall *)
   exploit classify_call_correct; eauto.
-  destruct (classify_call ge a) as [ | id | ef].
+  destruct (classify_call (prog_defmap cunit) a) as [ | id | ef].
 + (* indirect *)
   exploit sel_expr_correct; eauto. intros [vf' [A B]].
   exploit sel_exprlist_correct; eauto. intros [vargs' [C D]].
-  exploit functions_translated; eauto. intros (fd' & U & V).
+  exploit functions_translated; eauto. intros (cunit' & fd' & U & V & W).
   left; econstructor; split.
   econstructor; eauto. econstructor; eauto.
-  apply sig_function_translated; auto.
-  constructor; auto. constructor; auto.
+  eapply sig_function_translated; eauto.
+  eapply match_callstate with (cunit := cunit'); eauto.
+  red; intros. eapply match_cont_call with (cunit := cunit); eauto. 
 + (* direct *)
   intros [b [U V]].
   exploit sel_exprlist_correct; eauto. intros [vargs' [C D]].
-  exploit functions_translated; eauto. intros (fd' & X & Y).
+  exploit functions_translated; eauto. intros (cunit' & fd' & X & Y & Z).
   left; econstructor; split.
   econstructor; eauto.
   subst vf. econstructor; eauto. rewrite symbols_preserved; eauto.
-  apply sig_function_translated; auto.
-  constructor; auto. constructor; auto.
+  eapply sig_function_translated; eauto.
+  eapply match_callstate with (cunit := cunit'); eauto.
+  red; intros; eapply match_cont_call with (cunit := cunit); eauto. 
 + (* turned into Sbuiltin *)
   intros EQ. subst fd.
   exploit sel_builtin_args_correct; eauto. intros [vargs' [C D]].
@@ -819,43 +984,44 @@ Proof.
   erewrite <- stackspace_function_translated in P by eauto.
   exploit sel_expr_correct; eauto. intros [vf' [A B]].
   exploit sel_exprlist_correct; eauto. intros [vargs' [C D]].
-  exploit functions_translated; eauto. intros [fd' [E F]].
+  exploit functions_translated; eauto. intros (cunit' & fd' & E & F & G).
   left; econstructor; split.
-  exploit classify_call_correct; eauto.
-  destruct (classify_call ge a) as [ | id | ef]; intros.
-  econstructor; eauto. econstructor; eauto. apply sig_function_translated; auto.
+  exploit classify_call_correct. eexact LINK. eauto. eauto. 
+  destruct (classify_call (prog_defmap cunit)) as [ | id | ef]; intros.
+  econstructor; eauto. econstructor; eauto. eapply sig_function_translated; eauto.
   destruct H2 as [b [U V]]. subst vf. inv B.
-  econstructor; eauto. econstructor; eauto. rewrite symbols_preserved; eauto. apply sig_function_translated; auto.
-  econstructor; eauto. econstructor; eauto. apply sig_function_translated; auto.
-  constructor; auto. apply call_cont_commut; auto.
+  econstructor; eauto. econstructor; eauto. rewrite symbols_preserved; eauto. eapply sig_function_translated; eauto.
+  econstructor; eauto. econstructor; eauto. eapply sig_function_translated; eauto.
+  eapply match_callstate with (cunit := cunit'); eauto.
+  eapply call_cont_commut; eauto.
 - (* Sbuiltin *)
   exploit sel_builtin_args_correct; eauto. intros [vargs' [P Q]].
   exploit external_call_mem_extends; eauto.
   intros [vres' [m2 [A [B [C D]]]]].
   left; econstructor; split.
-  econstructor. eauto. eapply external_call_symbols_preserved; eauto.
-  exact symbols_preserved. exact public_preserved. exact varinfo_preserved.
-  constructor; auto. apply sel_builtin_res_correct; auto.
+  econstructor. eauto. eapply external_call_symbols_preserved; eauto. apply senv_preserved.
+  econstructor; eauto. apply sel_builtin_res_correct; auto.
 - (* Seq *)
   left; econstructor; split.
-  constructor. constructor; auto. constructor; auto.
+  constructor.
+  econstructor; eauto. constructor; auto.
 - (* Sifthenelse *)
   exploit sel_expr_correct; eauto. intros [v' [A B]].
   assert (Val.bool_of_val v' b). inv B. auto. inv H0.
   left; exists (State f' (if b then x else x0) k' sp e' m'); split.
   econstructor; eauto. eapply eval_condexpr_of_expr; eauto.
-  constructor; auto. destruct b; auto.
+  econstructor; eauto. destruct b; auto.
 - (* Sloop *)
-  left; econstructor; split. constructor. constructor; auto.
+  left; econstructor; split. constructor. econstructor; eauto.
   constructor; auto. simpl; rewrite EQ; auto.
 - (* Sblock *)
-  left; econstructor; split. constructor. constructor; auto. constructor; auto.
+  left; econstructor; split. constructor. econstructor; eauto. constructor; auto.
 - (* Sexit seq *)
-  inv MC. left; econstructor; split. constructor. constructor; auto.
+  inv MC. left; econstructor; split. constructor. econstructor; eauto.
 - (* Sexit0 block *)
-  inv MC. left; econstructor; split. constructor. constructor; auto.
+  inv MC. left; econstructor; split. constructor. econstructor; eauto.
 - (* SexitS block *)
-  inv MC. left; econstructor; split. constructor. constructor; auto.
+  inv MC. left; econstructor; split. constructor. econstructor; eauto.
 - (* Sswitch *)
   inv H0; simpl in TS.
 + set (ct := compile_switch Int.modulus default cases) in *.
@@ -863,69 +1029,70 @@ Proof.
   exploit sel_expr_correct; eauto. intros [v' [A B]]. inv B.
   left; econstructor; split.
   econstructor. eapply sel_switch_int_correct; eauto.
-  constructor; auto.
+  econstructor; eauto.
 + set (ct := compile_switch Int64.modulus default cases) in *.
   destruct (validate_switch Int64.modulus default cases ct) eqn:VALID; inv TS.
   exploit sel_expr_correct; eauto. intros [v' [A B]]. inv B.
   left; econstructor; split.
   econstructor. eapply sel_switch_long_correct; eauto.
-  constructor; auto.
+  econstructor; eauto.
 - (* Sreturn None *)
   exploit Mem.free_parallel_extends; eauto. intros [m2' [P Q]].
   erewrite <- stackspace_function_translated in P by eauto.
   left; econstructor; split.
   econstructor. simpl; eauto.
-  constructor; auto. apply call_cont_commut; auto.
+  econstructor; eauto. eapply call_cont_commut; eauto.
 - (* Sreturn Some *)
   exploit Mem.free_parallel_extends; eauto. intros [m2' [P Q]].
   erewrite <- stackspace_function_translated in P by eauto.
   exploit sel_expr_correct; eauto. intros [v' [A B]].
   left; econstructor; split.
   econstructor; eauto.
-  constructor; auto. apply call_cont_commut; auto.
+  econstructor; eauto. eapply call_cont_commut; eauto.
 - (* Slabel *)
-  left; econstructor; split. constructor. constructor; auto.
+  left; econstructor; split. constructor. econstructor; eauto.
 - (* Sgoto *)
-  assert (sel_stmt hf ge (Cminor.fn_body f) = OK (fn_body f')).
+  assert (sel_stmt (prog_defmap cunit) hf (Cminor.fn_body f) = OK (fn_body f')).
   { monadInv TF; simpl; auto. }
-  exploit (find_label_commut lbl (Cminor.fn_body f) (Cminor.call_cont k)).
-    apply call_cont_commut; eauto. eauto.
+  exploit (find_label_commut cunit hf lbl (Cminor.fn_body f) (Cminor.call_cont k)).
+    eapply call_cont_commut; eauto. eauto.
   rewrite H.
   destruct (find_label lbl (fn_body f') (call_cont k'0))
   as [[s'' k'']|] eqn:?; intros; try contradiction.
   destruct H1.
   left; econstructor; split.
   econstructor; eauto.
-  constructor; auto.
+  econstructor; eauto.
 - (* internal function *)
+  destruct TF as (hf & HF & TF). specialize (MC cunit hf). 
   monadInv TF. generalize EQ; intros TF; monadInv TF.
   exploit Mem.alloc_extends. eauto. eauto. apply Zle_refl. apply Zle_refl.
   intros [m2' [A B]].
   left; econstructor; split.
   econstructor; simpl; eauto.
-  constructor; simpl; auto. apply set_locals_lessdef. apply set_params_lessdef; auto.
+  econstructor; simpl; eauto. apply set_locals_lessdef. apply set_params_lessdef; auto.
 - (* external call *)
+  destruct TF as (hf & HF & TF). 
   monadInv TF.
   exploit external_call_mem_extends; eauto.
   intros [vres' [m2 [A [B [C D]]]]].
   left; econstructor; split.
-  econstructor. eapply external_call_symbols_preserved; eauto.
-  exact symbols_preserved. exact public_preserved. exact varinfo_preserved.
-  constructor; auto.
+  econstructor. eapply external_call_symbols_preserved; eauto. apply senv_preserved.
+  econstructor; eauto.
 - (* external call turned into a Sbuiltin *)
   exploit external_call_mem_extends; eauto.
   intros [vres' [m2 [A [B [C D]]]]].
   left; econstructor; split.
-  econstructor. eauto. eapply external_call_symbols_preserved; eauto.
-  exact symbols_preserved. exact public_preserved. exact varinfo_preserved.
-  constructor; auto.
+  econstructor. eauto. eapply external_call_symbols_preserved; eauto. apply senv_preserved.
+  econstructor; eauto.
 - (* return *)
+  apply match_call_cont_cont in MC. destruct MC as (cunit0 & hf0 & MC). 
   inv MC.
   left; econstructor; split.
   econstructor.
-  constructor; auto. destruct optid; simpl; auto. apply set_var_lessdef; auto.
+  econstructor; eauto. destruct optid; simpl; auto. apply set_var_lessdef; auto.
 - (* return of an external call turned into a Sbuiltin *)
-  right; split. simpl; omega. split. auto. constructor; auto.
+  right; split. simpl; omega. split. auto. econstructor; eauto.
   apply sel_builtin_res_correct; auto.
 Qed.
 
@@ -933,118 +1100,49 @@ Lemma sel_initial_states:
   forall S, Cminor.initial_state prog S ->
   exists R, initial_state tprog R /\ match_states S R.
 Proof.
-  induction 1.
-  exploit function_ptr_translated; eauto. intros (f' & A & B).
+  destruct 1.
+  exploit function_ptr_translated; eauto. intros (cu & f' & A & B & C).
   econstructor; split.
   econstructor.
-  eapply Genv.init_mem_transf_partial; eauto.
-  simpl. fold tge. rewrite symbols_preserved.
-  erewrite transform_partial_program_main by eauto. eexact H0.
-  eauto.
-  rewrite <- H2. apply sig_function_translated; auto.
-  constructor; auto. constructor. apply Mem.extends_refl.
+  eapply (Genv.init_mem_match TRANSF); eauto.
+  rewrite (match_program_main TRANSF). fold tge. rewrite symbols_preserved. eauto.
+  eexact A.
+  rewrite <- H2. eapply sig_function_translated; eauto.
+  econstructor; eauto. red; intros; constructor. apply Mem.extends_refl.
 Qed.
 
 Lemma sel_final_states:
   forall S R r,
   match_states S R -> Cminor.final_state S r -> final_state R r.
 Proof.
-  intros. inv H0. inv H. inv MC. inv LD. constructor.
-Qed.
-
-End PRESERVATION.
-
-(** Processing of helper functions *)
-
-Lemma record_globdefs_sound:
-  forall p id fd,
-  (record_globdefs p)!id = Some (Gfun fd) ->
-  exists b, Genv.find_symbol (Genv.globalenv p) id = Some b
-         /\ Genv.find_funct_ptr (Genv.globalenv p) b = Some fd.
-Proof.
-  intros until fd.
-  set (P := fun (m: PTree.t globdef) (ge: Genv.t Cminor.fundef unit) =>
-               m!id = Some (Gfun fd) ->
-               exists b, Genv.find_symbol ge id = Some b
-                      /\ Genv.find_funct_ptr ge b = Some fd).
-  assert (REC: forall gl m ge,
-             P m ge ->
-             P (fold_left record_globdef gl m) (Genv.add_globals ge gl)).
-  {
-    induction gl; simpl; intros.
-  - auto.
-  - apply IHgl. red. destruct a as [id1 gd1]; simpl; intros.
-    unfold Genv.find_symbol; simpl. rewrite PTree.gsspec. destruct (peq id id1).
-    + subst id1. exists (Genv.genv_next ge); split; auto.
-      replace gd1 with (@Gfun Cminor.fundef unit fd).
-      unfold Genv.find_funct_ptr; simpl. apply PTree.gss.
-      destruct (globdef_of_interest gd1).
-      rewrite PTree.gss in H0; congruence.
-      rewrite PTree.grs in H0; congruence.
-    + assert (m!id = Some (Gfun fd)).
-      { destruct (globdef_of_interest gd1).
-        rewrite PTree.gso in H0; auto.
-        rewrite PTree.gro in H0; auto. }
-      exploit H; eauto. intros (b & A & B).
-      exists b; split; auto. unfold Genv.find_funct_ptr; simpl.
-      destruct gd1; auto. rewrite PTree.gso; auto.
-      apply Plt_ne. eapply Genv.genv_symb_range; eauto.
-  }
-  eapply REC. red; intros. rewrite PTree.gempty in H; discriminate.
-Qed.
-
-Lemma lookup_helper_correct_1:
-  forall globs name sg id,
-  lookup_helper globs name sg = OK id ->
-  globs!id = Some (Gfun (External (EF_external name sg))).
-Proof.
-  intros.
-  set (P := fun (m: PTree.t globdef) res => res = Some id -> m!id = Some(Gfun(External (EF_external name sg)))).
-  assert (P globs (PTree.fold (lookup_helper_aux name sg) globs None)).
-  { apply PTree_Properties.fold_rec; red; intros.
-  - rewrite <- H0. apply H1; auto.
-  - discriminate.
-  - assert (EITHER: k = id /\ v = Gfun (External (EF_external name sg))
-                \/  a = Some id).
-    { unfold lookup_helper_aux in H3. destruct v; auto. destruct f; auto. destruct e; auto.
-      destruct (String.string_dec name name0); auto.
-      destruct (signature_eq sg sg0); auto.
-      inversion H3. left; split; auto. repeat f_equal; auto. }
-    destruct EITHER as [[X Y] | X].
-    subst k v. apply PTree.gss.
-    apply H2 in X. rewrite PTree.gso by congruence. auto.
-  }
-  red in H0. unfold lookup_helper in H.
-  destruct (PTree.fold (lookup_helper_aux name sg) globs None); inv H. auto.
+  intros. inv H0. inv H.
+  apply match_call_cont_cont in MC. destruct MC as (cunit0 & hf0 & MC). 
+  inv MC. inv LD. constructor.
 Qed.
 
-Lemma lookup_helper_correct:
-  forall p name sg id,
-  lookup_helper (record_globdefs p) name sg = OK id ->
-  helper_declared (Genv.globalenv p) id name sg.
+Theorem transf_program_correct:
+  forward_simulation (Cminor.semantics prog) (CminorSel.semantics tprog).
 Proof.
-  intros. apply lookup_helper_correct_1 in H. apply record_globdefs_sound in H. auto.
+  apply forward_simulation_opt with (match_states := match_states) (measure := measure).
+  apply senv_preserved. 
+  apply sel_initial_states; auto.
+  apply sel_final_states; auto.
+  apply sel_step_correct; auto.
 Qed.
 
-Theorem get_helpers_correct:
-  forall p hf,
-  get_helpers p = OK hf -> helper_functions_declared (Genv.globalenv p) hf.
-Proof.
-  intros. monadInv H. red; simpl. auto 20 using lookup_helper_correct.
-Qed.
+End PRESERVATION.
 
-(** All together *)
+(** ** Commutation with linking *)
 
-Theorem transf_program_correct:
-  forall prog tprog,
-  sel_program prog = OK tprog ->
-  forward_simulation (Cminor.semantics prog) (CminorSel.semantics tprog).
+Instance TransfSelectionLink : TransfLink match_prog.
 Proof.
-  intros. unfold sel_program in H.
-  destruct (get_helpers prog) as [hf|] eqn:G; simpl in H; try discriminate.
-  apply forward_simulation_opt with (match_states := match_states prog tprog hf) (measure := measure).
-  eapply public_preserved; eauto.
-  apply sel_initial_states; auto.
-  apply sel_final_states; auto.
-  apply sel_step_correct; auto. eapply get_helpers_correct; eauto.
+  red; intros. destruct (link_linkorder _ _ _ H) as [LO1 LO2].
+  eapply link_match_program; eauto.
+  intros. elim H3; intros hf1 [A1 B1]. elim H4; intros hf2 [A2 B2].
+Local Transparent Linker_fundef.
+  simpl in *. destruct f1, f2; simpl in *; monadInv B1; monadInv B2; simpl.
+- discriminate.
+- destruct e; inv H2. econstructor; eauto.
+- destruct e; inv H2. econstructor; eauto.
+- destruct (external_function_eq e e0); inv H2. econstructor; eauto. 
 Qed.