Strengthen the main compiler correctness results to account for separate compilation and linking

Define a "match_prog" relation corresponding to the composition of CompCert's passes.  Use it to show semantic preservation (backward/forward simulations) not just for the compilation of whole programs, but also for the separate compilation of multiple units followed by linking.

1 files changed, 250 insertions, 149 deletions

diff --git a/driver/Compiler.v b/driver/Compiler.v
index ea5849ec..dd752aca 100644
--- a/driver/Compiler.v
+++ b/driver/Compiler.v
@@ -14,15 +14,10 @@
 
 (** Libraries. *)
 Require Import String.
-Require Import Coqlib.
-Require Import Errors.
-Require Import AST.
-Require Import Smallstep.
+Require Import Coqlib Errors.
+Require Import AST Linking Smallstep.
 (** Languages (syntax and semantics). *)
-Require Csyntax.
-Require Csem.
-Require Cstrategy.
-Require Cexec.
+Require Ctypes Csyntax Csem Cstrategy Cexec.
 Require Clight.
 Require Csharpminor.
 Require Cminor.
@@ -192,171 +187,228 @@ Proof.
   intros. destruct x; simpl. rewrite print_identity. auto. auto.
 Qed.
 
-Remark forward_simulation_identity:
-  forall sem, forward_simulation sem sem.
+(** * Relational specification of compilation *)
+
+Definition match_if {A: Type} (flag: unit -> bool) (R: A -> A -> Prop): A -> A -> Prop :=
+  if flag tt then R else eq.
+
+Lemma total_if_match:
+  forall (A: Type) (flag: unit -> bool) (f: A -> A) (rel: A -> A -> Prop) (prog: A),
+  (forall p, rel p (f p)) ->
+  match_if flag rel prog (total_if flag f prog).
 Proof.
-  intros. apply forward_simulation_step with (fun s1 s2 => s2 = s1); intros.
-- auto.
-- exists s1; auto.
-- subst s2; auto.
-- subst s2. exists s1'; auto.
+  intros. unfold match_if, total_if. destruct (flag tt); auto.
 Qed.
 
-Lemma total_if_simulation:
-  forall (A: Type) (sem: A -> semantics) (flag: unit -> bool) (f: A -> A) (prog: A),
-  (forall p, forward_simulation (sem p) (sem (f p))) ->
-  forward_simulation (sem prog) (sem (total_if flag f prog)).
+Lemma partial_if_match:
+  forall (A: Type) (flag: unit -> bool) (f: A -> res A) (rel: A -> A -> Prop) (prog tprog: A),
+  (forall p tp, f p = OK tp -> rel p tp) ->
+  partial_if flag f prog = OK tprog ->
+  match_if flag rel prog tprog.
 Proof.
-  intros. unfold total_if. destruct (flag tt). auto. apply forward_simulation_identity.
+  intros. unfold match_if, partial_if in *. destruct (flag tt). auto. congruence.
 Qed.
 
-Lemma partial_if_simulation:
-  forall (A: Type) (sem: A -> semantics) (flag: unit -> bool) (f: A -> res A) (prog tprog: A),
-  partial_if flag f prog = OK tprog ->
-  (forall p tp, f p = OK tp -> forward_simulation (sem p) (sem tp)) ->
-  forward_simulation (sem prog) (sem tprog).
+Instance TransfIfLink {A: Type} {LA: Linker A}
+                      (flag: unit -> bool) (transf: A -> A -> Prop) (TL: TransfLink transf)
+                      : TransfLink (match_if flag transf).
+Proof.
+  unfold match_if. destruct (flag tt).
+- auto.
+- red; intros. subst tp1 tp2. exists p; auto.
+Qed.
+
+(** This is the list of compilation passes of CompCert in relational style.
+  Each pass is characterized by a [match_prog] relation between its
+  input code and its output code.  The [mkpass] and [:::] combinators,
+  defined in module [Linking], ensure that the passes are composable
+  (the output language of a pass is the input language of the next pass)
+  and that they commute with linking (property [TransfLink], inferred
+  by the type class mechanism of Coq). *)
+
+Local Open Scope linking_scope.
+
+Definition CompCert's_passes :=
+      mkpass SimplExprproof.match_prog
+  ::: mkpass SimplLocalsproof.match_prog
+  ::: mkpass Cshmgenproof.match_prog
+  ::: mkpass Cminorgenproof.match_prog
+  ::: mkpass Selectionproof.match_prog
+  ::: mkpass RTLgenproof.match_prog
+  ::: mkpass (match_if Compopts.optim_tailcalls Tailcallproof.match_prog)
+  ::: mkpass Inliningproof.match_prog
+  ::: mkpass Renumberproof.match_prog
+  ::: mkpass (match_if Compopts.optim_constprop Constpropproof.match_prog)
+  ::: mkpass (match_if Compopts.optim_constprop Renumberproof.match_prog)
+  ::: mkpass (match_if Compopts.optim_CSE CSEproof.match_prog)
+  ::: mkpass (match_if Compopts.optim_redundancy Deadcodeproof.match_prog)
+  ::: mkpass Unusedglobproof.match_prog
+  ::: mkpass Allocproof.match_prog
+  ::: mkpass Tunnelingproof.match_prog
+  ::: mkpass Linearizeproof.match_prog
+  ::: mkpass CleanupLabelsproof.match_prog
+  ::: mkpass (match_if Compopts.debug Debugvarproof.match_prog)
+  ::: mkpass Stackingproof.match_prog
+  ::: mkpass Asmgenproof.match_prog
+  ::: pass_nil _.
+
+(** Composing the [match_prog] relations above, we obtain the relation
+  between CompCert C sources and Asm code that characterize CompCert's
+  compilation. *)
+
+Definition match_prog: Csyntax.program -> Asm.program -> Prop :=
+  pass_match (compose_passes CompCert's_passes).
+
+(** The [transf_c_program] function, when successful, produces
+  assembly code that is in the [match_prog] relation with the source C program. *)
+
+Theorem transf_c_program_match:
+  forall p tp,
+  transf_c_program p = OK tp ->
+  match_prog p tp.
 Proof.
-  intros. unfold partial_if in *. destruct (flag tt). eauto. inv H. apply forward_simulation_identity.
+  intros p tp T.
+  unfold transf_c_program, time in T. simpl in T.
+  destruct (SimplExpr.transl_program p) as [p1|e] eqn:P1; simpl in T; try discriminate.
+  unfold transf_clight_program, time in T. rewrite ! compose_print_identity in T. simpl in T.
+  destruct (SimplLocals.transf_program p1) as [p2|e] eqn:P2; simpl in T; try discriminate.
+  destruct (Cshmgen.transl_program p2) as [p3|e] eqn:P3; simpl in T; try discriminate.
+  destruct (Cminorgen.transl_program p3) as [p4|e] eqn:P4; simpl in T; try discriminate.
+  unfold transf_cminor_program, time in T. rewrite ! compose_print_identity in T. simpl in T.
+  destruct (Selection.sel_program p4) as [p5|e] eqn:P5; simpl in T; try discriminate.
+  destruct (RTLgen.transl_program p5) as [p6|e] eqn:P6; simpl in T; try discriminate.
+  unfold transf_rtl_program, time in T. rewrite ! compose_print_identity in T. simpl in T.
+  set (p7 := total_if optim_tailcalls Tailcall.transf_program p6) in *.
+  destruct (Inlining.transf_program p7) as [p8|e] eqn:P8; simpl in T; try discriminate.
+  set (p9 := Renumber.transf_program p8) in *.
+  set (p10 := total_if optim_constprop Constprop.transf_program p9) in *.
+  set (p11 := total_if optim_constprop Renumber.transf_program p10) in *.
+  destruct (partial_if optim_CSE CSE.transf_program p11) as [p12|e] eqn:P12; simpl in T; try discriminate.
+  destruct (partial_if optim_redundancy Deadcode.transf_program p12) as [p13|e] eqn:P13; simpl in T; try discriminate.
+  destruct (Unusedglob.transform_program p13) as [p14|e] eqn:P14; simpl in T; try discriminate.
+  destruct (Allocation.transf_program p14) as [p15|e] eqn:P15; simpl in T; try discriminate.
+  set (p16 := Tunneling.tunnel_program p15) in *.
+  destruct (Linearize.transf_program p16) as [p17|e] eqn:P17; simpl in T; try discriminate.
+  set (p18 := CleanupLabels.transf_program p17) in *.
+  destruct (partial_if debug Debugvar.transf_program p18) as [p19|e] eqn:P19; simpl in T; try discriminate.
+  destruct (Stacking.transf_program p19) as [p20|e] eqn:P20; simpl in T; try discriminate.
+  unfold match_prog; simpl. 
+  exists p1; split. apply SimplExprproof.transf_program_match; auto.
+  exists p2; split. apply SimplLocalsproof.match_transf_program; auto.
+  exists p3; split. apply Cshmgenproof.transf_program_match; auto.
+  exists p4; split. apply Cminorgenproof.transf_program_match; auto.
+  exists p5; split. apply Selectionproof.transf_program_match; auto.
+  exists p6; split. apply RTLgenproof.transf_program_match; auto.
+  exists p7; split. apply total_if_match. apply Tailcallproof.transf_program_match.
+  exists p8; split. apply Inliningproof.transf_program_match; auto.
+  exists p9; split. apply Renumberproof.transf_program_match; auto.
+  exists p10; split. apply total_if_match. apply Constpropproof.transf_program_match.
+  exists p11; split. apply total_if_match. apply Renumberproof.transf_program_match.
+  exists p12; split. eapply partial_if_match; eauto. apply CSEproof.transf_program_match.
+  exists p13; split. eapply partial_if_match; eauto. apply Deadcodeproof.transf_program_match.
+  exists p14; split. apply Unusedglobproof.transf_program_match; auto.
+  exists p15; split. apply Allocproof.transf_program_match; auto.
+  exists p16; split. apply Tunnelingproof.transf_program_match.
+  exists p17; split. apply Linearizeproof.transf_program_match; auto.
+  exists p18; split. apply CleanupLabelsproof.transf_program_match; auto.
+  exists p19; split. eapply partial_if_match; eauto. apply Debugvarproof.transf_program_match.
+  exists p20; split. apply Stackingproof.transf_program_match; auto.
+  exists tp; split. apply Asmgenproof.transf_program_match; auto. 
+  reflexivity.
 Qed.
 
 (** * Semantic preservation *)
 
-(** We prove that the [transf_program] translations preserve semantics
-  by constructing the following simulations:
-- Forward simulations from [Cstrategy] / [Cminor] / [RTL] to [Asm]
+(** We now prove that the whole CompCert compiler (as characterized by the
+  [match_prog] relation) preserves semantics by constructing 
+  the following simulations:
+- Forward simulations from [Cstrategy] to [Asm]
   (composition of the forward simulations for each pass).
 - Backward simulations for the same languages
   (derived from the forward simulation, using receptiveness of the source
   language and determinacy of [Asm]).
 - Backward simulation from [Csem] to [Asm]
   (composition of two backward simulations).
+*)
 
-These results establish the correctness of the whole compiler! *)
-
-Theorem transf_rtl_program_correct:
-  forall p tp,
-  transf_rtl_program p = OK tp ->
-  forward_simulation (RTL.semantics p) (Asm.semantics tp)
-  * backward_simulation (RTL.semantics p) (Asm.semantics tp).
-Proof.
-  intros.
-  assert (F: forward_simulation (RTL.semantics p) (Asm.semantics tp)).
-  unfold transf_rtl_program, time in H.
-  repeat rewrite compose_print_identity in H.
-  simpl in H.
-  set (p1 := total_if optim_tailcalls Tailcall.transf_program p) in *.
-  destruct (Inlining.transf_program p1) as [p11|] eqn:?; simpl in H; try discriminate.
-  set (p12 := Renumber.transf_program p11) in *.
-  set (p2 := total_if optim_constprop Constprop.transf_program p12) in *.
-  set (p21 := total_if optim_constprop Renumber.transf_program p2) in *.
-  destruct (partial_if optim_CSE CSE.transf_program p21) as [p3|] eqn:?; simpl in H; try discriminate.
-  destruct (partial_if optim_redundancy Deadcode.transf_program p3) as [p31|] eqn:?; simpl in H; try discriminate.
-  destruct (Unusedglob.transform_program p31) as [p32|] eqn:?; simpl in H; try discriminate.
-  destruct (Allocation.transf_program p32) as [p4|] eqn:?; simpl in H; try discriminate.
-  set (p5 := Tunneling.tunnel_program p4) in *.
-  destruct (Linearize.transf_program p5) as [p6|] eqn:?; simpl in H; try discriminate.
-  set (p7 := CleanupLabels.transf_program p6) in *.
-  destruct (partial_if debug Debugvar.transf_program p7) as [p71|] eqn:?; simpl in H; try discriminate.
-  destruct (Stacking.transf_program p71) as [p8|] eqn:?; simpl in H; try discriminate.
-  apply compose_forward_simulation with (RTL.semantics p1).
-    apply total_if_simulation. apply Tailcallproof.transf_program_correct.
-  apply compose_forward_simulation with (RTL.semantics p11).
-    apply Inliningproof.transf_program_correct; auto.
-  apply compose_forward_simulation with (RTL.semantics p12).
-    apply Renumberproof.transf_program_correct.
-  apply compose_forward_simulation with (RTL.semantics p2).
-    apply total_if_simulation. apply Constpropproof.transf_program_correct.
-  apply compose_forward_simulation with (RTL.semantics p21).
-    apply total_if_simulation. apply Renumberproof.transf_program_correct.
-  apply compose_forward_simulation with (RTL.semantics p3).
-    eapply partial_if_simulation; eauto.  apply CSEproof.transf_program_correct.
-  apply compose_forward_simulation with (RTL.semantics p31).
-    eapply partial_if_simulation; eauto. apply Deadcodeproof.transf_program_correct.
-  apply compose_forward_simulation with (RTL.semantics p32).
-    apply Unusedglobproof.transf_program_correct; auto.
-  apply compose_forward_simulation with (LTL.semantics p4).
-    apply Allocproof.transf_program_correct; auto.
-  apply compose_forward_simulation with (LTL.semantics p5).
-    apply Tunnelingproof.transf_program_correct.
-  apply compose_forward_simulation with (Linear.semantics p6).
-    apply Linearizeproof.transf_program_correct; auto.
-  apply compose_forward_simulation with (Linear.semantics p7).
-    apply CleanupLabelsproof.transf_program_correct.
-  apply compose_forward_simulation with (Linear.semantics p71).
-    eapply partial_if_simulation; eauto. apply Debugvarproof.transf_program_correct.
-  apply compose_forward_simulation with (Mach.semantics Asmgenproof0.return_address_offset p8).
-    apply Stackingproof.transf_program_correct.
-    exact Asmgenproof.return_address_exists.
-    auto.
-  apply Asmgenproof.transf_program_correct; eauto.
-  split. auto.
-  apply forward_to_backward_simulation. auto.
-  apply RTL.semantics_receptive.
-  apply Asm.semantics_determinate.
-Qed.
-
-Theorem transf_cminor_program_correct:
-  forall p tp,
-  transf_cminor_program p = OK tp ->
-  forward_simulation (Cminor.semantics p) (Asm.semantics tp)
-  * backward_simulation (Cminor.semantics p) (Asm.semantics tp).
+Remark forward_simulation_identity:
+  forall sem, forward_simulation sem sem.
 Proof.
-  intros.
-  assert (F: forward_simulation (Cminor.semantics p) (Asm.semantics tp)).
-  unfold transf_cminor_program, time in H.
-  repeat rewrite compose_print_identity in H.
-  simpl in H.
-  destruct (Selection.sel_program p) as [p1|] eqn:?; simpl in H; try discriminate.
-  destruct (RTLgen.transl_program p1) as [p2|] eqn:?; simpl in H; try discriminate.
-  eapply compose_forward_simulation. apply Selectionproof.transf_program_correct. eauto.
-  eapply compose_forward_simulation. apply RTLgenproof.transf_program_correct. eassumption.
-  exact (fst (transf_rtl_program_correct _ _ H)).
-
-  split. auto.
-  apply forward_to_backward_simulation. auto.
-  apply Cminor.semantics_receptive.
-  apply Asm.semantics_determinate.
+  intros. apply forward_simulation_step with (fun s1 s2 => s2 = s1); intros.
+- auto.
+- exists s1; auto.
+- subst s2; auto.
+- subst s2. exists s1'; auto.
 Qed.
 
-Theorem transf_clight_program_correct:
-  forall p tp,
-  transf_clight_program p = OK tp ->
-  forward_simulation (Clight.semantics1 p) (Asm.semantics tp)
-  * backward_simulation (Clight.semantics1 p) (Asm.semantics tp).
+Lemma match_if_simulation:
+  forall (A: Type) (sem: A -> semantics) (flag: unit -> bool) (transf: A -> A -> Prop) (prog tprog: A),
+  match_if flag transf prog tprog ->
+  (forall p tp, transf p tp -> forward_simulation (sem p) (sem tp)) ->
+  forward_simulation (sem prog) (sem tprog).
 Proof.
-  intros.
-  assert (F: forward_simulation (Clight.semantics1 p) (Asm.semantics tp)).
-  revert H; unfold transf_clight_program, time; simpl.
-  rewrite print_identity.
-  caseEq (SimplLocals.transf_program p); simpl; try congruence; intros p0 EQ0.
-  caseEq (Cshmgen.transl_program p0); simpl; try congruence; intros p1 EQ1.
-  caseEq (Cminorgen.transl_program p1); simpl; try congruence; intros p2 EQ2.
-  intros EQ3.
-  eapply compose_forward_simulation. apply SimplLocalsproof.transf_program_correct. eauto.
-  eapply compose_forward_simulation. apply Cshmgenproof.transl_program_correct. eauto.
-  eapply compose_forward_simulation. apply Cminorgenproof.transl_program_correct. eauto.
-  exact (fst (transf_cminor_program_correct _ _ EQ3)).
-
-  split. auto.
-  apply forward_to_backward_simulation. auto.
-  apply Clight.semantics_receptive.
-  apply Asm.semantics_determinate.
+  intros. unfold match_if in *. destruct (flag tt). eauto. subst. apply forward_simulation_identity.
 Qed.
 
-Theorem transf_cstrategy_program_correct:
+Theorem cstrategy_semantic_preservation:
   forall p tp,
-  transf_c_program p = OK tp ->
+  match_prog p tp ->
   forward_simulation (Cstrategy.semantics p) (Asm.semantics tp)
-  * backward_simulation (atomic (Cstrategy.semantics p)) (Asm.semantics tp).
+  /\ backward_simulation (atomic (Cstrategy.semantics p)) (Asm.semantics tp).
 Proof.
-  intros.
-  assert (F: forward_simulation (Cstrategy.semantics p) (Asm.semantics tp)).
-  revert H; unfold transf_c_program, time; simpl.
-  caseEq (SimplExpr.transl_program p); simpl; try congruence; intros p0 EQ0.
-  intros EQ1.
-  eapply compose_forward_simulation. apply SimplExprproof.transl_program_correct. eauto.
-  exact (fst (transf_clight_program_correct _ _ EQ1)).
-
+  intros p tp M. unfold match_prog, pass_match in M; simpl in M.
+Ltac DestructM :=
+  match goal with
+    [ H: exists p, _ /\ _ |- _ ] => 
+      let p := fresh "p" in let M := fresh "M" in let MM := fresh "MM" in
+      destruct H as (p & M & MM); clear H
+  end.
+  repeat DestructM. subst tp.
+  assert (F: forward_simulation (Cstrategy.semantics p) (Asm.semantics p21)).
+  {
+  eapply compose_forward_simulations.
+    eapply SimplExprproof.transl_program_correct; eassumption.
+  eapply compose_forward_simulations.
+    eapply SimplLocalsproof.transf_program_correct; eassumption.
+  eapply compose_forward_simulations.
+    eapply Cshmgenproof.transl_program_correct; eassumption.
+  eapply compose_forward_simulations.
+    eapply Cminorgenproof.transl_program_correct; eassumption.
+  eapply compose_forward_simulations.
+    eapply Selectionproof.transf_program_correct; eassumption.
+  eapply compose_forward_simulations.
+    eapply RTLgenproof.transf_program_correct; eassumption.
+  eapply compose_forward_simulations.
+    eapply match_if_simulation. eassumption. exact Tailcallproof.transf_program_correct.
+  eapply compose_forward_simulations.
+    eapply Inliningproof.transf_program_correct; eassumption.
+  eapply compose_forward_simulations. eapply Renumberproof.transf_program_correct; eassumption.
+  eapply compose_forward_simulations.
+    eapply match_if_simulation. eassumption. exact Constpropproof.transf_program_correct.
+  eapply compose_forward_simulations.
+    eapply match_if_simulation. eassumption. exact Renumberproof.transf_program_correct.
+  eapply compose_forward_simulations.
+    eapply match_if_simulation. eassumption. exact CSEproof.transf_program_correct.
+  eapply compose_forward_simulations.
+    eapply match_if_simulation. eassumption. exact Deadcodeproof.transf_program_correct; eassumption.
+  eapply compose_forward_simulations.
+    eapply Unusedglobproof.transf_program_correct; eassumption.
+  eapply compose_forward_simulations.
+    eapply Allocproof.transf_program_correct; eassumption.
+  eapply compose_forward_simulations.
+    eapply Tunnelingproof.transf_program_correct; eassumption.
+  eapply compose_forward_simulations.
+    eapply Linearizeproof.transf_program_correct; eassumption.
+  eapply compose_forward_simulations.
+    eapply CleanupLabelsproof.transf_program_correct; eassumption.
+  eapply compose_forward_simulations.
+    eapply match_if_simulation. eassumption. exact Debugvarproof.transf_program_correct.
+  eapply compose_forward_simulations.
+    eapply Stackingproof.transf_program_correct with (return_address_offset := Asmgenproof0.return_address_offset).
+    exact Asmgenproof.return_address_exists.
+    eassumption.
+  eapply Asmgenproof.transf_program_correct; eassumption.
+  }
   split. auto.
   apply forward_to_backward_simulation.
   apply factor_forward_simulation. auto. eapply sd_traces. eapply Asm.semantics_determinate.
@@ -364,9 +416,9 @@ Proof.
   apply Asm.semantics_determinate.
 Qed.
 
-Theorem transf_c_program_correct:
+Theorem c_semantic_preservation:
   forall p tp,
-  transf_c_program p = OK tp ->
+  match_prog p tp ->
   backward_simulation (Csem.semantics p) (Asm.semantics tp).
 Proof.
   intros.
@@ -376,5 +428,54 @@ Proof.
   apply Cstrategy.strategy_simulation.
   apply Csem.semantics_single_events.
   eapply ssr_well_behaved; eapply Cstrategy.semantics_strongly_receptive.
-  exact (snd (transf_cstrategy_program_correct _ _ H)).
+  exact (proj2 (cstrategy_semantic_preservation _ _ H)).
+Qed.
+
+(** * Correctness of the CompCert compiler *)
+
+(** Combining the results above, we obtain semantic preservation for two
+  usage scenarios of CompCert: compilation of a single monolithic program,
+  and separate compilation of multiple source files followed by linking.
+
+  In the monolithic case, we have a whole C program [p] that is
+  compiled in one run of CompCert to a whole Asm program [tp].
+  Then, [tp] preserves the semantics of [p], in the sense that there
+  exists a backward simulation of the dynamic semantics of [p]
+  by the dynamic semantics of [tp]. *)
+
+Theorem transf_c_program_correct:
+  forall p tp,
+  transf_c_program p = OK tp ->
+  backward_simulation (Csem.semantics p) (Asm.semantics tp).
+Proof.
+  intros. apply c_semantic_preservation. apply transf_c_program_match; auto.
+Qed.
+
+(** Here is the separate compilation case.  Consider a nonempty list [c_units]
+  of C source files (compilation units), [C1 ,,, Cn].  Assume that every
+  C compilation unit [Ci] is successfully compiled by CompCert, obtaining
+  an Asm compilation unit [Ai].  Let [asm_unit] be the nonempty list
+  [A1 ... An].  Further assume that the C units [C1 ... Cn] can be linked
+  together to produce a whole C program [c_program].  Then, the generated
+  Asm units can be linked together, producing a whole Asm program
+  [asm_program].  Moreover, [asm_program] preserves the semantics of
+  [c_program], in the sense that there exists a backward simulation of
+  the dynamic semantics of [asm_program] by the dynamic semantics of [c_program].
+*)
+
+Theorem separate_transf_c_program_correct:
+  forall c_units asm_units c_program,
+  nlist_forall2 (fun cu tcu => transf_c_program cu = OK tcu) c_units asm_units ->
+  link_list c_units = Some c_program ->
+  exists asm_program, 
+      link_list asm_units = Some asm_program
+   /\ backward_simulation (Csem.semantics c_program) (Asm.semantics asm_program).
+Proof.
+  intros. 
+  assert (nlist_forall2 match_prog c_units asm_units).
+  { eapply nlist_forall2_imply. eauto. simpl; intros. apply transf_c_program_match; auto. }
+  assert (exists asm_program, link_list asm_units = Some asm_program /\ match_prog c_program asm_program).
+  { eapply link_list_compose_passes; eauto. }
+  destruct H2 as (asm_program & P & Q).
+  exists asm_program; split; auto. apply c_semantic_preservation; auto.
 Qed.