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, 108 insertions, 125 deletions

diff --git a/backend/Deadcodeproof.v b/backend/Deadcodeproof.v
index 6bbf0ae7..72881b94 100644
--- a/backend/Deadcodeproof.v
+++ b/backend/Deadcodeproof.v
@@ -12,28 +12,20 @@
 
 (** Elimination of unneeded computations over RTL: correctness proof. *)
 
-Require Import Coqlib.
-Require Import Errors.
-Require Import Maps.
-Require Import IntvSets.
-Require Import AST.
-Require Import Integers.
-Require Import Floats.
-Require Import Values.
-Require Import Memory.
-Require Import Globalenvs.
-Require Import Events.
-Require Import Smallstep.
-Require Import Op.
-Require Import Registers.
-Require Import RTL.
-Require Import Lattice.
-Require Import Kildall.
-Require Import ValueDomain.
-Require Import ValueAnalysis.
-Require Import NeedDomain.
-Require Import NeedOp.
-Require Import Deadcode.
+Require Import Coqlib Maps Errors Integers Floats Lattice Kildall.
+Require Import AST Linking.
+Require Import Values Memory Globalenvs Events Smallstep.
+Require Import Registers Op RTL.
+Require Import ValueDomain ValueAnalysis NeedDomain NeedOp Deadcode.
+
+Definition match_prog (prog tprog: RTL.program) :=
+  match_program (fun cu f tf => transf_fundef (romem_for cu) f = OK tf) eq prog tprog.
+
+Lemma transf_program_match:
+  forall prog tprog, transf_program prog = OK tprog -> match_prog prog tprog.
+Proof.
+  intros. eapply match_transform_partial_program_contextual; eauto.
+Qed.
 
 (** * Relating the memory states *)
 
@@ -378,75 +370,61 @@ 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.
-Let rm := romem_for_program prog.
 
 Lemma symbols_preserved:
   forall (s: ident), Genv.find_symbol tge s = Genv.find_symbol ge s.
-Proof.
-  intro. unfold ge, tge.
-  apply Genv.find_symbol_transf_partial with (transf_fundef rm).
-  exact TRANSF.
-Qed.
-
-Lemma public_preserved:
-  forall (s: ident), Genv.public_symbol tge s = Genv.public_symbol ge s.
-Proof.
-  intro. unfold ge, tge.
-  apply Genv.public_symbol_transf_partial with (transf_fundef rm).
-  exact TRANSF.
-Qed.
+Proof (Genv.find_symbol_match TRANSF).
 
-Lemma varinfo_preserved:
-  forall b, Genv.find_var_info tge b = Genv.find_var_info ge b.
-Proof.
-  intro. unfold ge, tge.
-  apply Genv.find_var_info_transf_partial with (transf_fundef rm).
-  exact TRANSF.
-Qed.
+Lemma senv_preserved:
+  Senv.equiv ge tge.
+Proof (Genv.senv_match TRANSF).
 
 Lemma functions_translated:
   forall (v: val) (f: RTL.fundef),
   Genv.find_funct ge v = Some f ->
-  exists tf,
-  Genv.find_funct tge v = Some tf /\ transf_fundef rm f = OK tf.
-Proof (Genv.find_funct_transf_partial (transf_fundef rm) _ TRANSF).
+  exists cu tf,
+  Genv.find_funct tge v = Some tf /\ transf_fundef (romem_for cu) f = OK tf /\ linkorder cu prog.
+Proof (Genv.find_funct_match TRANSF).
 
 Lemma function_ptr_translated:
   forall (b: block) (f: RTL.fundef),
   Genv.find_funct_ptr ge b = Some f ->
-  exists tf,
-  Genv.find_funct_ptr tge b = Some tf /\ transf_fundef rm f = OK tf.
-Proof (Genv.find_funct_ptr_transf_partial (transf_fundef rm) _ TRANSF).
+  exists cu tf,
+  Genv.find_funct_ptr tge b = Some tf /\ transf_fundef (romem_for cu) f = OK tf /\ linkorder cu prog.
+Proof (Genv.find_funct_ptr_match TRANSF).
 
 Lemma sig_function_translated:
-  forall f tf,
+  forall rm f tf,
   transf_fundef rm f = OK tf ->
   funsig tf = funsig f.
 Proof.
   intros; destruct f; monadInv H.
   unfold transf_function in EQ.
-  destruct (analyze (vanalyze rm f) f); inv EQ; auto.
+  destruct (analyze (ValueAnalysis.analyze rm f) f); inv EQ; auto.
   auto.
 Qed.
 
 Lemma stacksize_translated:
-  forall f tf,
+  forall rm f tf,
   transf_function rm f = OK tf -> tf.(fn_stacksize) = f.(fn_stacksize).
 Proof.
-  unfold transf_function; intros. destruct (analyze (vanalyze rm f) f); inv H; auto.
+  unfold transf_function; intros. destruct (analyze (ValueAnalysis.analyze rm f) f); inv H; auto.
 Qed.
 
+Definition vanalyze (cu: program) (f: function) :=
+  ValueAnalysis.analyze (romem_for cu) f.
+
 Lemma transf_function_at:
-  forall f tf an pc instr,
-  transf_function rm f = OK tf ->
-  analyze (vanalyze rm f) f = Some an ->
+  forall cu f tf an pc instr,
+  transf_function (romem_for cu) f = OK tf ->
+  analyze (vanalyze cu f) f = Some an ->
   f.(fn_code)!pc = Some instr ->
-  tf.(fn_code)!pc = Some(transf_instr (vanalyze rm f) an pc instr).
+  tf.(fn_code)!pc = Some(transf_instr (vanalyze cu f) an pc instr).
 Proof.
-  intros. unfold transf_function in H. rewrite H0 in H. inv H; simpl.
+  intros. unfold transf_function in H. unfold vanalyze in H0. rewrite H0 in H. inv H; simpl.
   rewrite PTree.gmap. rewrite H1; auto.
 Qed.
 
@@ -475,7 +453,10 @@ Lemma find_function_translated:
   forall ros rs fd trs ne,
   find_function ge ros rs = Some fd ->
   eagree rs trs (add_ros_need_all ros ne) ->
-  exists tfd, find_function tge ros trs = Some tfd /\ transf_fundef rm fd = OK tfd.
+  exists cu tfd,
+     find_function tge ros trs = Some tfd
+  /\ transf_fundef (romem_for cu) fd = OK tfd
+  /\ linkorder cu prog.
 Proof.
   intros. destruct ros as [r|id]; simpl in *.
 - assert (LD: Val.lessdef rs#r trs#r) by eauto with na. inv LD.
@@ -489,30 +470,33 @@ Qed.
 
 Inductive match_stackframes: stackframe -> stackframe -> Prop :=
   | match_stackframes_intro:
-      forall res f sp pc e tf te an
-        (FUN: transf_function rm f = OK tf)
-        (ANL: analyze (vanalyze rm f) f = Some an)
+      forall res f sp pc e tf te cu an
+        (LINK: linkorder cu prog)
+        (FUN: transf_function (romem_for cu) f = OK tf)
+        (ANL: analyze (vanalyze cu f) f = Some an)
         (RES: forall v tv,
               Val.lessdef v tv ->
               eagree (e#res <- v) (te#res<- tv)
-                     (fst (transfer f (vanalyze rm f) pc an!!pc))),
+                     (fst (transfer f (vanalyze cu f) pc an!!pc))),
       match_stackframes (Stackframe res f (Vptr sp Int.zero) pc e)
                         (Stackframe res tf (Vptr sp Int.zero) pc te).
 
 Inductive match_states: state -> state -> Prop :=
   | match_regular_states:
-      forall s f sp pc e m ts tf te tm an
+      forall s f sp pc e m ts tf te tm cu an
         (STACKS: list_forall2 match_stackframes s ts)
-        (FUN: transf_function rm f = OK tf)
-        (ANL: analyze (vanalyze rm f) f = Some an)
-        (ENV: eagree e te (fst (transfer f (vanalyze rm f) pc an!!pc)))
-        (MEM: magree m tm (nlive ge sp (snd (transfer f (vanalyze rm f) pc an!!pc)))),
+        (LINK: linkorder cu prog)
+        (FUN: transf_function (romem_for cu) f = OK tf)
+        (ANL: analyze (vanalyze cu f) f = Some an)
+        (ENV: eagree e te (fst (transfer f (vanalyze cu f) pc an!!pc)))
+        (MEM: magree m tm (nlive ge sp (snd (transfer f (vanalyze cu f) pc an!!pc)))),
       match_states (State s f (Vptr sp Int.zero) pc e m)
                    (State ts tf (Vptr sp Int.zero) pc te tm)
   | match_call_states:
-      forall s f args m ts tf targs tm
+      forall s f args m ts tf targs tm cu
         (STACKS: list_forall2 match_stackframes s ts)
-        (FUN: transf_fundef rm f = OK tf)
+        (LINK: linkorder cu prog)
+        (FUN: transf_fundef (romem_for cu) f = OK tf)
         (ARGS: Val.lessdef_list args targs)
         (MEM: Mem.extends m tm),
       match_states (Callstate s f args m)
@@ -528,21 +512,22 @@ Inductive match_states: state -> state -> Prop :=
 (** [match_states] and CFG successors *)
 
 Lemma analyze_successors:
-  forall f an pc instr pc',
-  analyze (vanalyze rm f) f = Some an ->
+  forall cu f an pc instr pc',
+  analyze (vanalyze cu f) f = Some an ->
   f.(fn_code)!pc = Some instr ->
   In pc' (successors_instr instr) ->
-  NA.ge an!!pc (transfer f (vanalyze rm f) pc' an!!pc').
+  NA.ge an!!pc (transfer f (vanalyze cu f) pc' an!!pc').
 Proof.
   intros. eapply DS.fixpoint_solution; eauto.
   intros. unfold transfer; rewrite H2. destruct a. apply DS.L.eq_refl.
 Qed.
 
 Lemma match_succ_states:
-  forall s f sp pc e m ts tf te tm an pc' instr ne nm
+  forall s f sp pc e m ts tf te tm an pc' cu instr ne nm
+    (LINK: linkorder cu prog)
     (STACKS: list_forall2 match_stackframes s ts)
-    (FUN: transf_function rm f = OK tf)
-    (ANL: analyze (vanalyze rm f) f = Some an)
+    (FUN: transf_function (romem_for cu) f = OK tf)
+    (ANL: analyze (vanalyze cu f) f = Some an)
     (INSTR: f.(fn_code)!pc = Some instr)
     (SUCC: In pc' (successors_instr instr))
     (ANPC: an!!pc = (ne, nm))
@@ -720,7 +705,7 @@ Ltac TransfInstr :=
   | [INSTR: (fn_code _)!_ = Some _,
      FUN: transf_function _ _ = OK _,
      ANL: analyze _ _ = Some _ |- _ ] =>
-       generalize (transf_function_at _ _ _ _ _ FUN ANL INSTR);
+       generalize (transf_function_at _ _ _ _ _ _ FUN ANL INSTR);
        intro TI;
        unfold transf_instr in TI
   end.
@@ -825,7 +810,7 @@ Ltac UseTransfer :=
 
 - (* store *)
   TransfInstr; UseTransfer.
-  destruct (nmem_contains nm (aaddressing (vanalyze rm f) # pc addr args)
+  destruct (nmem_contains nm (aaddressing (vanalyze cu f) # pc addr args)
              (size_chunk chunk)) eqn:CONTAINS.
 + (* preserved *)
   simpl in *.
@@ -854,39 +839,41 @@ Ltac UseTransfer :=
 
 - (* call *)
   TransfInstr; UseTransfer.
-  exploit find_function_translated; eauto 2 with na. intros (tfd & A & B).
+  exploit find_function_translated; eauto 2 with na. intros (cu' & tfd & A & B & C).
   econstructor; split.
-  eapply exec_Icall; eauto. apply sig_function_translated; auto.
-  constructor.
-  constructor; auto. econstructor; eauto.
+  eapply exec_Icall; eauto. eapply sig_function_translated; eauto.
+  eapply match_call_states with (cu := cu'); eauto.
+  constructor; auto. eapply match_stackframes_intro with (cu := cu); eauto.
   intros.
   edestruct analyze_successors; eauto. simpl; eauto.
   eapply eagree_ge; eauto. rewrite ANPC. simpl.
   apply eagree_update; eauto with na.
-  auto. eauto 2 with na. eapply magree_extends; eauto. apply nlive_all.
+  eauto 2 with na.
+  eapply magree_extends; eauto. apply nlive_all.
 
 - (* tailcall *)
   TransfInstr; UseTransfer.
-  exploit find_function_translated; eauto 2 with na. intros (tfd & A & B).
+  exploit find_function_translated; eauto 2 with na. intros (cu' & tfd & A & B & L).
   exploit magree_free. eauto. eauto. instantiate (1 := nlive ge stk nmem_all).
   intros; eapply nlive_dead_stack; eauto.
   intros (tm' & C & D).
   econstructor; split.
-  eapply exec_Itailcall; eauto. apply sig_function_translated; auto.
+  eapply exec_Itailcall; eauto. eapply sig_function_translated; eauto.
   erewrite stacksize_translated by eauto. eexact C.
-  constructor; eauto 2 with na. eapply magree_extends; eauto. apply nlive_all.
+  eapply match_call_states with (cu := cu'); eauto 2 with na.
+  eapply magree_extends; eauto. apply nlive_all.
 
 - (* builtin *)
   TransfInstr; UseTransfer. revert ENV MEM TI.
-  functional induction (transfer_builtin (vanalyze rm f)#pc ef args res ne nm);
+  functional induction (transfer_builtin (vanalyze cu f)#pc ef args res ne nm);
   simpl in *; intros.
 + (* volatile load *)
   inv H0. inv H6. rename b1 into v1.
   destruct (transfer_builtin_arg All
               (kill_builtin_res res ne,
-              nmem_add nm (aaddr_arg (vanalyze rm f) # pc a1)
+              nmem_add nm (aaddr_arg (vanalyze cu f) # pc a1)
                 (size_chunk chunk)) a1) as (ne1, nm1) eqn: TR.
-  inversion SS; subst. exploit transfer_builtin_arg_sound; eauto.
+  InvSoundState. exploit transfer_builtin_arg_sound; eauto.
   intros (tv1 & A & B & C & D).
   inv H1. simpl in B. inv B.
   assert (X: exists tvres, volatile_load ge chunk tm b ofs t tvres /\ Val.lessdef vres tvres).
@@ -904,9 +891,8 @@ Ltac UseTransfer :=
   eapply exec_Ibuiltin; eauto.
   apply eval_builtin_args_preserved with (ge1 := ge). exact symbols_preserved.
   constructor. eauto. constructor.
-  eapply external_call_symbols_preserved.
+  eapply external_call_symbols_preserved. apply senv_preserved.
   constructor. simpl. eauto.
-  exact symbols_preserved. exact public_preserved. exact varinfo_preserved.
   eapply match_succ_states; eauto. simpl; auto.
   apply eagree_set_res; auto.
   eapply magree_monotone; eauto. intros. apply incl_nmem_add; auto.
@@ -915,7 +901,7 @@ Ltac UseTransfer :=
   destruct (transfer_builtin_arg (store_argument chunk)
               (kill_builtin_res res ne, nm) a2) as (ne2, nm2) eqn: TR2.
   destruct (transfer_builtin_arg All (ne2, nm2) a1) as (ne1, nm1) eqn: TR1.
-  inversion SS; subst.
+  InvSoundState.
   exploit transfer_builtin_arg_sound. eexact H4. eauto. eauto. eauto. eauto. eauto.
   intros (tv1 & A1 & B1 & C1 & D1).
   exploit transfer_builtin_arg_sound. eexact H3. eauto. eauto. eauto. eauto. eauto.
@@ -926,21 +912,21 @@ Ltac UseTransfer :=
   eapply exec_Ibuiltin; eauto.
   apply eval_builtin_args_preserved with (ge1 := ge). exact symbols_preserved.
   constructor. eauto. constructor. eauto. constructor.
-  eapply external_call_symbols_preserved. simpl; eauto.
-  exact symbols_preserved. exact public_preserved. exact varinfo_preserved.
+  eapply external_call_symbols_preserved. apply senv_preserved.
+  simpl; eauto.
   eapply match_succ_states; eauto. simpl; auto.
   apply eagree_set_res; auto.
 + (* memcpy *)
   rewrite e1 in TI.
   inv H0. inv H6. inv H7. rename b1 into v1. rename b0 into v2.
-  set (adst := aaddr_arg (vanalyze rm f) # pc dst) in *.
-  set (asrc := aaddr_arg (vanalyze rm f) # pc src) in *.
+  set (adst := aaddr_arg (vanalyze cu f) # pc dst) in *.
+  set (asrc := aaddr_arg (vanalyze cu f) # pc src) in *.
   destruct (transfer_builtin_arg All
               (kill_builtin_res res ne,
                nmem_add (nmem_remove nm adst sz) asrc sz) dst)
            as (ne2, nm2) eqn: TR2.
   destruct (transfer_builtin_arg All (ne2, nm2) src) as (ne1, nm1) eqn: TR1.
-  inversion SS; subst.
+  InvSoundState.
   exploit transfer_builtin_arg_sound. eexact H3. eauto. eauto. eauto. eauto. eauto.
   intros (tv1 & A1 & B1 & C1 & D1).
   exploit transfer_builtin_arg_sound. eexact H4. eauto. eauto. eauto. eauto. eauto.
@@ -948,7 +934,7 @@ Ltac UseTransfer :=
   inv H1.
   exploit magree_loadbytes. eauto. eauto.
   intros. eapply nlive_add; eauto.
-  unfold asrc, vanalyze, rm; rewrite AN; eapply aaddr_arg_sound_1; eauto.
+  unfold asrc, vanalyze; rewrite AN; eapply aaddr_arg_sound_1; eauto.
   intros (tbytes & P & Q).
   exploit magree_storebytes_parallel.
   eapply magree_monotone. eexact D2.
@@ -957,7 +943,7 @@ Ltac UseTransfer :=
   eauto.
   instantiate (1 := nlive ge sp0 nm).
   intros. eapply nlive_remove; eauto.
-  unfold adst, vanalyze, rm; rewrite AN; eapply aaddr_arg_sound_1; eauto.
+  unfold adst, vanalyze; rewrite AN; eapply aaddr_arg_sound_1; eauto.
   erewrite Mem.loadbytes_length in H1 by eauto.
   rewrite nat_of_Z_eq in H1 by omega. auto.
   eauto.
@@ -966,51 +952,49 @@ Ltac UseTransfer :=
   eapply exec_Ibuiltin; eauto.
   apply eval_builtin_args_preserved with (ge1 := ge). exact symbols_preserved.
   constructor. eauto. constructor. eauto. constructor.
-  eapply external_call_symbols_preserved. simpl.
+  eapply external_call_symbols_preserved. apply senv_preserved.
   simpl in B1; inv B1. simpl in B2; inv B2. econstructor; eauto.
-  exact symbols_preserved. exact public_preserved. exact varinfo_preserved.
   eapply match_succ_states; eauto. simpl; auto.
   apply eagree_set_res; auto.
 + (* memcpy eliminated *)
   rewrite e1 in TI.
   inv H0. inv H6. inv H7. rename b1 into v1. rename b0 into v2.
-  set (adst := aaddr_arg (vanalyze rm f) # pc dst) in *.
-  set (asrc := aaddr_arg (vanalyze rm f) # pc src) in *.
+  set (adst := aaddr_arg (vanalyze cu f) # pc dst) in *.
+  set (asrc := aaddr_arg (vanalyze cu f) # pc src) in *.
   inv H1.
   econstructor; split.
   eapply exec_Inop; eauto.
   eapply match_succ_states; eauto. simpl; auto.
   destruct res; auto. apply eagree_set_undef; auto.
   eapply magree_storebytes_left; eauto.
-  exploit aaddr_arg_sound. eauto. eauto.
+  exploit aaddr_arg_sound; eauto. 
   intros (bc & A & B & C).
   intros. eapply nlive_contains; eauto.
   erewrite Mem.loadbytes_length in H0 by eauto.
   rewrite nat_of_Z_eq in H0 by omega. auto.
 + (* annot *)
   destruct (transfer_builtin_args (kill_builtin_res res ne, nm) _x1) as (ne1, nm1) eqn:TR.
-  inversion SS; subst.
+  InvSoundState.
   exploit transfer_builtin_args_sound; eauto. intros (tvl & A & B & C & D).
   inv H1.
   econstructor; split.
   eapply exec_Ibuiltin; eauto.
   apply eval_builtin_args_preserved with (ge1 := ge); eauto. exact symbols_preserved.
-  eapply external_call_symbols_preserved. simpl; constructor.
-  eapply eventval_list_match_lessdef; eauto 2 with na.
-  exact symbols_preserved. exact public_preserved. exact varinfo_preserved.
+  eapply external_call_symbols_preserved. apply senv_preserved.
+  constructor. eapply eventval_list_match_lessdef; eauto 2 with na.
   eapply match_succ_states; eauto. simpl; auto.
   apply eagree_set_res; auto.
 + (* annot val *)
   destruct (transfer_builtin_args (kill_builtin_res res ne, nm) _x1) as (ne1, nm1) eqn:TR.
-  inversion SS; subst.
+  InvSoundState.
   exploit transfer_builtin_args_sound; eauto. intros (tvl & A & B & C & D).
   inv H1. inv B. inv H6.
   econstructor; split.
   eapply exec_Ibuiltin; eauto.
   apply eval_builtin_args_preserved with (ge1 := ge); eauto. exact symbols_preserved.
-  eapply external_call_symbols_preserved. simpl; constructor.
+  eapply external_call_symbols_preserved. apply senv_preserved.
+  constructor.
   eapply eventval_match_lessdef; eauto 2 with na.
-  exact symbols_preserved. exact public_preserved. exact varinfo_preserved.
   eapply match_succ_states; eauto. simpl; auto.
   apply eagree_set_res; auto.
 + (* debug *)
@@ -1027,7 +1011,7 @@ Ltac UseTransfer :=
   }
   clear y TI.
   destruct (transfer_builtin_args (kill_builtin_res res ne, nmem_all) _x0) as (ne1, nm1) eqn:TR.
-  inversion SS; subst.
+  InvSoundState.
   exploit transfer_builtin_args_sound; eauto. intros (tvl & A & B & C & D).
   exploit external_call_mem_extends; eauto 2 with na.
   eapply magree_extends; eauto. intros. apply nlive_all.
@@ -1035,8 +1019,7 @@ Ltac UseTransfer :=
   econstructor; split.
   eapply exec_Ibuiltin; eauto.
   apply 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.
   eapply match_succ_states; eauto. simpl; auto.
   apply eagree_set_res; auto.
   eapply mextends_agree; eauto.
@@ -1071,8 +1054,8 @@ Ltac UseTransfer :=
   eapply magree_extends; eauto. apply nlive_all.
 
 - (* internal function *)
-  monadInv FUN. generalize EQ. unfold transf_function. intros EQ'.
-  destruct (analyze (vanalyze rm f) f) as [an|] eqn:AN; inv EQ'.
+  monadInv FUN. generalize EQ. unfold transf_function. fold (vanalyze cu f). intros EQ'.
+  destruct (analyze (vanalyze cu f) f) as [an|] eqn:AN; inv EQ'.
   exploit Mem.alloc_extends; eauto. apply Zle_refl. apply Zle_refl.
   intros (tm' & A & B).
   econstructor; split.
@@ -1087,8 +1070,7 @@ Ltac UseTransfer :=
   simpl in FUN. inv FUN.
   econstructor; split.
   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.
   econstructor; eauto.
 
 - (* return *)
@@ -1103,14 +1085,15 @@ Lemma transf_initial_states:
   exists st2, initial_state tprog st2 /\ match_states st1 st2.
 Proof.
   intros. inversion H.
-  exploit function_ptr_translated; eauto. intros (tf & A & B).
+  exploit function_ptr_translated; eauto. intros (cu & tf & A & B & C).
   exists (Callstate nil tf nil m0); split.
   econstructor; eauto.
-  eapply Genv.init_mem_transf_partial; eauto.
-  rewrite (transform_partial_program_main _ _ TRANSF).
+  eapply (Genv.init_mem_match TRANSF); eauto.
+  replace (prog_main tprog) with (prog_main prog). 
   rewrite symbols_preserved. eauto.
-  rewrite <- H3. apply sig_function_translated; auto.
-  constructor. constructor. auto. constructor. apply Mem.extends_refl.
+  symmetry; eapply match_program_main; eauto.
+  rewrite <- H3. eapply sig_function_translated; eauto.
+  econstructor; eauto. constructor. apply Mem.extends_refl.
 Qed.
 
 Lemma transf_final_states:
@@ -1128,7 +1111,7 @@ Proof.
   intros.
   apply forward_simulation_step with
      (match_states := fun s1 s2 => sound_state prog s1 /\ match_states s1 s2).
-- exact public_preserved.
+- apply senv_preserved.
 - simpl; intros. exploit transf_initial_states; eauto. intros [st2 [A B]].
   exists st2; intuition. eapply sound_initial; eauto.
 - simpl; intros. destruct H. eapply transf_final_states; eauto.