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, 123 insertions, 141 deletions

diff --git a/backend/Constpropproof.v b/backend/Constpropproof.v
index ad9068ab..4e76c641 100644
--- a/backend/Constpropproof.v
+++ b/backend/Constpropproof.v
@@ -12,35 +12,30 @@
 
 (** Correctness proof for constant propagation. *)
 
-Require Import Coqlib.
-Require Import Maps.
-Require Compopts.
-Require Import AST.
-Require Import Integers.
-Require Import Values.
-Require Import Events.
-Require Import Memory.
-Require Import Globalenvs.
-Require Import Smallstep.
-Require Import Op.
-Require Import Registers.
-Require Import RTL.
-Require Import Lattice.
-Require Import Kildall.
-Require Import ValueDomain.
-Require Import ValueAOp.
-Require Import ValueAnalysis.
-Require Import ConstpropOp.
-Require Import Constprop.
-Require Import ConstpropOpproof.
+Require Import Coqlib Maps Integers Floats Lattice Kildall.
+Require Import AST Linking.
+Require Import Values Events Memory Globalenvs Smallstep.
+Require Compopts Machregs.
+Require Import Op Registers RTL.
+Require Import Liveness ValueDomain ValueAOp ValueAnalysis.
+Require Import ConstpropOp ConstpropOpproof Constprop.
+
+Definition match_prog (prog tprog: program) :=
+  match_program (fun cu f tf => tf = transf_fundef (romem_for cu) f) eq prog tprog.
+
+Lemma transf_program_match:
+  forall prog, match_prog prog (transf_program prog).
+Proof.
+  intros. eapply match_transform_program_contextual. auto.
+Qed.
 
 Section PRESERVATION.
 
 Variable prog: program.
-Let tprog := transf_program prog.
+Variable tprog: program.
+Hypothesis TRANSL: match_prog prog tprog.
 Let ge := Genv.globalenv prog.
 Let tge := Genv.globalenv tprog.
-Let rm := romem_for_program prog.
 
 (** * Correctness of the code transformation *)
 
@@ -49,45 +44,32 @@ Let rm := romem_for_program prog.
 
 Lemma symbols_preserved:
   forall (s: ident), Genv.find_symbol tge s = Genv.find_symbol ge s.
-Proof.
-  intros; unfold ge, tge, tprog, transf_program.
-  apply Genv.find_symbol_transf.
-Qed.
-
-Lemma public_preserved:
-  forall (s: ident), Genv.public_symbol tge s = Genv.public_symbol ge s.
-Proof.
-  intros; unfold ge, tge, tprog, transf_program.
-  apply Genv.public_symbol_transf.
-Qed.
+Proof (Genv.find_symbol_match TRANSL).
 
-Lemma varinfo_preserved:
-  forall b, Genv.find_var_info tge b = Genv.find_var_info ge b.
-Proof.
-  intros; unfold ge, tge, tprog, transf_program.
-  apply Genv.find_var_info_transf.
-Qed.
+Lemma senv_preserved:
+  Senv.equiv ge tge.
+Proof (Genv.senv_match TRANSL).
 
 Lemma functions_translated:
   forall (v: val) (f: fundef),
   Genv.find_funct ge v = Some f ->
-  Genv.find_funct tge v = Some (transf_fundef rm f).
+  exists cunit, Genv.find_funct tge v = Some (transf_fundef (romem_for cunit) f) /\ linkorder cunit prog.
 Proof.
-  intros.
-  exact (Genv.find_funct_transf (transf_fundef rm) _ _ H).
+  intros. exploit (Genv.find_funct_match TRANSL); eauto. 
+  intros (cu & tf & A & B & C). subst tf. exists cu; auto.
 Qed.
 
 Lemma function_ptr_translated:
   forall (b: block) (f: fundef),
   Genv.find_funct_ptr ge b = Some f ->
-  Genv.find_funct_ptr tge b = Some (transf_fundef rm f).
+  exists cunit, Genv.find_funct_ptr tge b = Some (transf_fundef (romem_for cunit) f) /\ linkorder cunit prog.
 Proof.
-  intros.
-  exact (Genv.find_funct_ptr_transf (transf_fundef rm) _ _ H).
+  intros. exploit (Genv.find_funct_ptr_match TRANSL); eauto. 
+  intros (cu & tf & A & B & C). subst tf. exists cu; auto.
 Qed.
 
 Lemma sig_function_translated:
-  forall f,
+  forall rm f,
   funsig (transf_fundef rm f) = funsig f.
 Proof.
   intros. destruct f; reflexivity.
@@ -110,12 +92,17 @@ Lemma transf_ros_correct:
   ematch bc rs ae ->
   find_function ge ros rs = Some f ->
   regs_lessdef rs rs' ->
-  find_function tge (transf_ros ae ros) rs' = Some (transf_fundef rm f).
+  exists cunit, 
+     find_function tge (transf_ros ae ros) rs' = Some (transf_fundef (romem_for cunit) f)
+  /\ linkorder cunit prog.
 Proof.
   intros until rs'; intros GE EM FF RLD. destruct ros; simpl in *.
 - (* function pointer *)
   generalize (EM r); fold (areg ae r); intro VM. generalize (RLD r); intro LD.
-  assert (DEFAULT: find_function tge (inl _ r) rs' = Some (transf_fundef rm f)).
+  assert (DEFAULT:
+    exists cunit, 
+       find_function tge (inl _ r) rs' = Some (transf_fundef (romem_for cunit) f)
+    /\ linkorder cunit prog).
   {
     simpl. inv LD. apply functions_translated; auto. rewrite <- H0 in FF; discriminate.
   }
@@ -162,35 +149,45 @@ Proof.
     eapply vmatch_ptr_stk; eauto.
 Qed.
 
-Inductive match_pc (f: function) (ae: AE.t): nat -> node -> node -> Prop :=
+Inductive match_pc (f: function) (rs: regset) (m: mem): nat -> node -> node -> Prop :=
   | match_pc_base: forall n pc,
-      match_pc f ae n pc pc
+      match_pc f rs m n pc pc
   | match_pc_nop: forall n pc s pcx,
       f.(fn_code)!pc = Some (Inop s) ->
-      match_pc f ae n s pcx ->
-      match_pc f ae (S n) pc pcx
-  | match_pc_cond: forall n pc cond args s1 s2 b pcx,
+      match_pc f rs m n s pcx ->
+      match_pc f rs m (S n) pc pcx
+  | match_pc_cond: forall n pc cond args s1 s2 pcx,
       f.(fn_code)!pc = Some (Icond cond args s1 s2) ->
-      resolve_branch (eval_static_condition cond (aregs ae args)) = Some b ->
-      match_pc f ae n (if b then s1 else s2) pcx ->
-      match_pc f ae (S n) pc pcx.
+      (forall b,
+        eval_condition cond rs##args m = Some b ->
+        match_pc f rs m n (if b then s1 else s2) pcx) ->
+      match_pc f rs m (S n) pc pcx.
 
 Lemma match_successor_rec:
-  forall f ae n pc, match_pc f ae n pc (successor_rec n f ae pc).
+  forall f rs m bc ae,
+  ematch bc rs ae ->
+  forall n pc,
+  match_pc f rs m n pc (successor_rec n f ae pc).
 Proof.
   induction n; simpl; intros.
 - apply match_pc_base.
 - destruct (fn_code f)!pc as [[]|] eqn:INSTR; try apply match_pc_base.
-  eapply match_pc_nop; eauto.
-  destruct (resolve_branch (eval_static_condition c (aregs ae l))) as [b|] eqn:COND.
-  eapply match_pc_cond; eauto.
-  apply match_pc_base.
++ eapply match_pc_nop; eauto.
++ destruct (resolve_branch (eval_static_condition c (aregs ae l))) as [b|] eqn:STATIC;
+  try apply match_pc_base.
+  eapply match_pc_cond; eauto. intros b' DYNAMIC.
+  assert (b = b').
+  { eapply resolve_branch_sound; eauto. 
+    rewrite <- DYNAMIC. apply eval_static_condition_sound with bc. 
+    apply aregs_sound; auto. }
+  subst b'. apply IHn. 
 Qed.
 
 Lemma match_successor:
-  forall f ae pc, match_pc f ae num_iter pc (successor f ae pc).
+  forall f rs m bc ae pc,
+  ematch bc rs ae -> match_pc f rs m num_iter pc (successor f ae pc).
 Proof.
-  unfold successor; intros. apply match_successor_rec.
+  intros. eapply match_successor_rec; eauto.
 Qed.
 
 Lemma builtin_arg_reduction_correct:
@@ -300,29 +297,31 @@ Qed.
 
 Inductive match_stackframes: stackframe -> stackframe -> Prop :=
    match_stackframe_intro:
-      forall res sp pc rs f rs',
+      forall res sp pc rs f rs' cu,
+      linkorder cu prog ->
       regs_lessdef rs rs' ->
     match_stackframes
         (Stackframe res f sp pc rs)
-        (Stackframe res (transf_function rm f) sp pc rs').
+        (Stackframe res (transf_function (romem_for cu) f) sp pc rs').
 
 Inductive match_states: nat -> state -> state -> Prop :=
   | match_states_intro:
-      forall s sp pc rs m f s' pc' rs' m' bc ae n
-           (MATCH: ematch bc rs ae)
+      forall s sp pc rs m f s' pc' rs' m' cu n
+           (LINK: linkorder cu prog)
            (STACKS: list_forall2 match_stackframes s s')
-           (PC: match_pc f ae n pc pc')
+           (PC: match_pc f rs m n pc pc')
            (REGS: regs_lessdef rs rs')
            (MEM: Mem.extends m m'),
       match_states n (State s f sp pc rs m)
-                    (State s' (transf_function rm f) sp pc' rs' m')
+                    (State s' (transf_function (romem_for cu) f) sp pc' rs' m')
   | match_states_call:
-      forall s f args m s' args' m'
+      forall s f args m s' args' m' cu
+           (LINK: linkorder cu prog)
            (STACKS: list_forall2 match_stackframes s s')
            (ARGS: Val.lessdef_list args args')
            (MEM: Mem.extends m m'),
       match_states O (Callstate s f args m)
-                     (Callstate s' (transf_fundef rm f) args' m')
+                     (Callstate s' (transf_fundef (romem_for cu) f) args' m')
   | match_states_return:
       forall s v m s' v' m'
            (STACKS: list_forall2 match_stackframes s s')
@@ -333,21 +332,19 @@ Inductive match_states: nat -> state -> state -> Prop :=
                      (Returnstate s' v' m').
 
 Lemma match_states_succ:
-  forall s f sp pc rs m s' rs' m',
-  sound_state prog (State s f sp pc rs m) ->
+  forall s f sp pc rs m s' rs' m' cu,
+  linkorder cu prog ->
   list_forall2 match_stackframes s s' ->
   regs_lessdef rs rs' ->
   Mem.extends m m' ->
   match_states O (State s f sp pc rs m)
-                 (State s' (transf_function rm f) sp pc rs' m').
+                 (State s' (transf_function (romem_for cu) f) sp pc rs' m').
 Proof.
-  intros. inv H.
-  apply match_states_intro with (bc := bc) (ae := ae); auto.
-  constructor.
+  intros. apply match_states_intro; auto. constructor. 
 Qed.
 
 Lemma transf_instr_at:
-  forall f pc i,
+  forall rm f pc i,
   f.(fn_code)!pc = Some i ->
   (transf_function rm f).(fn_code)!pc = Some(transf_instr f (analyze rm f) rm pc i).
 Proof.
@@ -357,8 +354,8 @@ Qed.
 Ltac TransfInstr :=
   match goal with
   | H1: (PTree.get ?pc (fn_code ?f) = Some ?instr),
-    H2: (analyze (romem_for_program prog) ?f)#?pc = VA.State ?ae ?am |- _ =>
-      fold rm in H2; generalize (transf_instr_at _ _ _ H1); unfold transf_instr; rewrite H2
+    H2: (analyze ?rm ?f)#?pc = VA.State ?ae ?am |- _ =>
+      generalize (transf_instr_at rm _ _ _ H1); unfold transf_instr; rewrite H2
   end.
 
 (** The proof of simulation proceeds by case analysis on the transition
@@ -367,38 +364,38 @@ Ltac TransfInstr :=
 Lemma transf_step_correct:
   forall s1 t s2,
   step ge s1 t s2 ->
-  forall n1 s1' (SS1: sound_state prog s1) (SS2: sound_state prog s2) (MS: match_states n1 s1 s1'),
+  forall n1 s1' (SS: sound_state prog s1) (MS: match_states n1 s1 s1'),
   (exists n2, exists s2', step tge s1' t s2' /\ match_states n2 s2 s2')
   \/ (exists n2, n2 < n1 /\ t = E0 /\ match_states n2 s2 s1')%nat.
 Proof.
-  induction 1; intros; inv SS1; inv MS; try (inv PC; try congruence).
+  induction 1; intros; inv MS; try InvSoundState; try (inv PC; try congruence).
 
-  (* Inop, preserved *)
+- (* Inop, preserved *)
   rename pc'0 into pc. TransfInstr; intros.
   left; econstructor; econstructor; split.
   eapply exec_Inop; eauto.
   eapply match_states_succ; eauto.
 
-  (* Inop, skipped over *)
+- (* Inop, skipped over *)
   assert (s0 = pc') by congruence. subst s0.
   right; exists n; split. omega. split. auto.
-  apply match_states_intro with bc0 ae0; auto.
+  apply match_states_intro; auto.
 
-  (* Iop *)
+- (* Iop *)
   rename pc'0 into pc. TransfInstr.
   set (a := eval_static_operation op (aregs ae args)).
   set (ae' := AE.set res a ae).
   assert (VMATCH: vmatch bc v a) by (eapply eval_static_operation_sound; eauto with va).
   assert (MATCH': ematch bc (rs#res <- v) ae') by (eapply ematch_update; eauto).
   destruct (const_for_result a) as [cop|] eqn:?; intros.
-  (* constant is propagated *)
++ (* constant is propagated *)
   exploit const_for_result_correct; eauto. intros (v' & A & B).
   left; econstructor; econstructor; split.
   eapply exec_Iop; eauto.
-  apply match_states_intro with bc ae'; auto.
-  apply match_successor.
+  apply match_states_intro; auto.
+  eapply match_successor; eauto.
   apply set_reg_lessdef; auto.
-  (* operator is strength-reduced *)
++ (* operator is strength-reduced *)
   assert(OP:
      let (op', args') := op_strength_reduction op args (aregs ae args) in
      exists v',
@@ -413,24 +410,24 @@ Proof.
   left; econstructor; econstructor; split.
   eapply exec_Iop; eauto.
   erewrite eval_operation_preserved. eexact EV''. exact symbols_preserved.
-  apply match_states_intro with bc ae'; auto.
-  apply match_successor.
+  apply match_states_intro; auto.
+  eapply match_successor; eauto.
   apply set_reg_lessdef; auto. eapply Val.lessdef_trans; eauto.
 
-  (* Iload *)
+- (* Iload *)
   rename pc'0 into pc. TransfInstr.
   set (aa := eval_static_addressing addr (aregs ae args)).
   assert (VM1: vmatch bc a aa) by (eapply eval_static_addressing_sound; eauto with va).
-  set (av := loadv chunk rm am aa).
+  set (av := loadv chunk (romem_for cu) am aa).
   assert (VM2: vmatch bc v av) by (eapply loadv_sound; eauto).
   destruct (const_for_result av) as [cop|] eqn:?; intros.
-  (* constant-propagated *)
++ (* constant-propagated *)
   exploit const_for_result_correct; eauto. intros (v' & A & B).
   left; econstructor; econstructor; split.
   eapply exec_Iop; eauto.
   eapply match_states_succ; eauto.
   apply set_reg_lessdef; auto.
-  (* strength-reduced *)
++ (* strength-reduced *)
   assert (ADDR:
      let (addr', args') := addr_strength_reduction addr args (aregs ae args) in
      exists a',
@@ -449,7 +446,7 @@ Proof.
   eapply exec_Iload; eauto.
   eapply match_states_succ; eauto. apply set_reg_lessdef; auto.
 
-  (* Istore *)
+- (* Istore *)
   rename pc'0 into pc. TransfInstr.
   assert (ADDR:
      let (addr', args') := addr_strength_reduction addr args (aregs ae args) in
@@ -469,9 +466,9 @@ Proof.
   eapply exec_Istore; eauto.
   eapply match_states_succ; eauto.
 
-  (* Icall *)
+- (* Icall *)
   rename pc'0 into pc.
-  exploit transf_ros_correct; eauto. intro FIND'.
+  exploit transf_ros_correct; eauto. intros (cu' & FIND & LINK').
   TransfInstr; intro.
   left; econstructor; econstructor; split.
   eapply exec_Icall; eauto. apply sig_function_translated; auto.
@@ -479,17 +476,17 @@ Proof.
   econstructor; eauto.
   apply regs_lessdef_regs; auto.
 
-  (* Itailcall *)
+- (* Itailcall *)
   exploit Mem.free_parallel_extends; eauto. intros [m2' [A B]].
-  exploit transf_ros_correct; eauto. intros FIND'.
+  exploit transf_ros_correct; eauto. intros (cu' & FIND & LINK').
   TransfInstr; intro.
   left; econstructor; econstructor; split.
   eapply exec_Itailcall; eauto. apply sig_function_translated; auto.
   constructor; auto.
   apply regs_lessdef_regs; auto.
 
-  (* Ibuiltin *)
-  rename pc'0 into pc. clear MATCH. TransfInstr; intros.
+- (* Ibuiltin *)
+  rename pc'0 into pc. TransfInstr; intros.
 Opaque builtin_strength_reduction.
   exploit builtin_strength_reduction_correct; eauto. intros (vargs' & P & Q).
   exploit (@eval_builtin_args_lessdef _ ge (fun r => rs#r) (fun r => rs'#r)).
@@ -500,13 +497,12 @@ Opaque builtin_strength_reduction.
   left; econstructor; econstructor; split.
   eapply exec_Ibuiltin; eauto.
   eapply eval_builtin_args_preserved. eexact symbols_preserved. 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.
   eapply match_states_succ; eauto.
   apply set_res_lessdef; auto.
 
-  (* Icond, preserved *)
-  rename pc' into pc. TransfInstr.
+- (* Icond, preserved *)
+  rename pc'0 into pc. TransfInstr.
   set (ac := eval_static_condition cond (aregs ae args)).
   assert (C: cmatch (eval_condition cond rs ## args m) ac)
   by (eapply eval_static_condition_sound; eauto with va).
@@ -514,7 +510,7 @@ Opaque builtin_strength_reduction.
   generalize (cond_strength_reduction_correct bc ae rs m EM cond args (aregs ae args) (refl_equal _)).
   destruct (cond_strength_reduction cond args (aregs ae args)) as [cond' args'].
   intros EV1 TCODE.
-  left; exists O; exists (State s' (transf_function rm f) (Vptr sp0 Int.zero) (if b then ifso else ifnot) rs' m'); split.
+  left; exists O; exists (State s' (transf_function (romem_for cu) f) (Vptr sp0 Int.zero) (if b then ifso else ifnot) rs' m'); split.
   destruct (resolve_branch ac) eqn: RB.
   assert (b0 = b) by (eapply resolve_branch_sound; eauto). subst b0.
   destruct b; eapply exec_Inop; eauto.
@@ -522,20 +518,15 @@ Opaque builtin_strength_reduction.
   eapply eval_condition_lessdef with (vl1 := rs##args'); eauto. eapply regs_lessdef_regs; eauto. congruence.
   eapply match_states_succ; eauto.
 
-  (* Icond, skipped over *)
+- (* Icond, skipped over *)
   rewrite H1 in H; inv H.
-  set (ac := eval_static_condition cond (aregs ae0 args)) in *.
-  assert (C: cmatch (eval_condition cond rs ## args m) ac)
-  by (eapply eval_static_condition_sound; eauto with va).
-  rewrite H0 in C.
-  assert (b0 = b) by (eapply resolve_branch_sound; eauto). subst b0.
-  right; exists n; split. omega. split. auto.
+  right; exists n; split. omega. split. auto. 
   econstructor; eauto.
 
-  (* Ijumptable *)
+- (* Ijumptable *)
   rename pc'0 into pc.
-  assert (A: (fn_code (transf_function rm f))!pc = Some(Ijumptable arg tbl)
-             \/ (fn_code (transf_function rm f))!pc = Some(Inop pc')).
+  assert (A: (fn_code (transf_function (romem_for cu) f))!pc = Some(Ijumptable arg tbl)
+             \/ (fn_code (transf_function (romem_for cu) f))!pc = Some(Inop pc')).
   { TransfInstr.
     destruct (areg ae arg) eqn:A; auto.
     generalize (EM arg). fold (areg ae arg); rewrite A.
@@ -543,23 +534,20 @@ Opaque builtin_strength_reduction.
     rewrite H1. auto. }
   assert (rs'#arg = Vint n).
   { generalize (REGS arg). rewrite H0. intros LD; inv LD; auto. }
-  left; exists O; exists (State s' (transf_function rm f) (Vptr sp0 Int.zero) pc' rs' m'); split.
+  left; exists O; exists (State s' (transf_function (romem_for cu) f) (Vptr sp0 Int.zero) pc' rs' m'); split.
   destruct A. eapply exec_Ijumptable; eauto. eapply exec_Inop; eauto.
   eapply match_states_succ; eauto.
 
-  (* Ireturn *)
+- (* Ireturn *)
   exploit Mem.free_parallel_extends; eauto. intros [m2' [A B]].
   left; exists O; exists (Returnstate s' (regmap_optget or Vundef rs') m2'); split.
   eapply exec_Ireturn; eauto. TransfInstr; auto.
   constructor; auto.
   destruct or; simpl; auto.
 
-  (* internal function *)
+- (* internal function *)
   exploit Mem.alloc_extends. eauto. eauto. apply Zle_refl. apply Zle_refl.
   intros [m2' [A B]].
-  assert (X: exists bc ae, ematch bc (init_regs args (fn_params f)) ae).
-  { inv SS2. exists bc0; exists ae; auto. }
-  destruct X as (bc1 & ae1 & MATCH).
   simpl. unfold transf_function.
   left; exists O; econstructor; split.
   eapply exec_function_internal; simpl; eauto.
@@ -567,19 +555,15 @@ Opaque builtin_strength_reduction.
   constructor.
   apply init_regs_lessdef; auto.
 
-  (* external function *)
+- (* external function *)
   exploit external_call_mem_extends; eauto.
   intros [v' [m2' [A [B [C D]]]]].
   simpl. left; econstructor; econstructor; split.
   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 *)
-  assert (X: exists bc ae, ematch bc (rs#res <- vres) ae).
-  { inv SS2. exists bc0; exists ae; auto. }
-  destruct X as (bc1 & ae1 & MATCH).
+- (* return *)
   inv H4. inv H1.
   left; exists O; econstructor; split.
   eapply exec_return; eauto.
@@ -591,15 +575,15 @@ Lemma transf_initial_states:
   exists n, exists st2, initial_state tprog st2 /\ match_states n st1 st2.
 Proof.
   intros. inversion H.
-  exploit function_ptr_translated; eauto. intro FIND.
-  exists O; exists (Callstate nil (transf_fundef rm f) nil m0); split.
+  exploit function_ptr_translated; eauto. intros (cu & FIND & LINK).
+  exists O; exists (Callstate nil (transf_fundef (romem_for cu) f) nil m0); split.
   econstructor; eauto.
-  apply Genv.init_mem_transf; auto.
+  apply (Genv.init_mem_match TRANSL); auto.
   replace (prog_main tprog) with (prog_main prog).
   rewrite symbols_preserved. eauto.
-  reflexivity.
+  symmetry; eapply match_program_main; eauto.
   rewrite <- H3. apply sig_function_translated.
-  constructor. constructor. constructor. apply Mem.extends_refl.
+  constructor. auto. constructor. constructor. apply Mem.extends_refl.
 Qed.
 
 Lemma transf_final_states:
@@ -615,9 +599,7 @@ Qed.
 Theorem transf_program_correct:
   forward_simulation (RTL.semantics prog) (RTL.semantics tprog).
 Proof.
-  apply Forward_simulation with
-     (fsim_order := lt)
-     (fsim_match_states := fun n s1 s2 => sound_state prog s1 /\ match_states n s1 s2).
+  apply Forward_simulation with lt (fun n s1 s2 => sound_state prog s1 /\ match_states n s1 s2); constructor.
 - apply lt_wf.
 - simpl; intros. exploit transf_initial_states; eauto. intros (n & st2 & A & B).
   exists n, st2; intuition. eapply sound_initial; eauto.
@@ -629,7 +611,7 @@ Proof.
   intros [ [n2 [s2' [A B]]] | [n2 [A [B C]]]].
   exists n2; exists s2'; split; auto. left; apply plus_one; auto.
   exists n2; exists s2; split; auto. right; split; auto. subst t; apply star_refl.
-- eexact public_preserved.
+- apply senv_preserved.
 Qed.
 
 End PRESERVATION.