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.

2 files changed, 257 insertions, 154 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.
diff --git a/driver/Complements.v b/driver/Complements.v
index 8651f2ff..f7598758 100644
--- a/driver/Complements.v
+++ b/driver/Complements.v
@@ -80,17 +80,19 @@ Theorem transf_cstrategy_program_preservation:
 Proof.
   assert (WBT: forall p, well_behaved_traces (Cstrategy.semantics p)).
     intros. eapply ssr_well_behaved. apply Cstrategy.semantics_strongly_receptive.
-  intros. intuition.
+  intros. 
+  assert (MATCH: match_prog p tp) by (apply transf_c_program_match; auto).
+  intuition auto.
   eapply forward_simulation_behavior_improves; eauto.
-    apply (fst (transf_cstrategy_program_correct _ _ H)).
+    apply (proj1 (cstrategy_semantic_preservation _ _ MATCH)).
   exploit backward_simulation_behavior_improves.
-    apply (snd (transf_cstrategy_program_correct _ _ H)).
+    apply (proj2 (cstrategy_semantic_preservation _ _ MATCH)).
     eauto.
   intros [beh1 [A B]]. exists beh1; split; auto. rewrite atomic_behaviors; auto.
   eapply forward_simulation_same_safe_behavior; eauto.
-    apply (fst (transf_cstrategy_program_correct _ _ H)).
+    apply (proj1 (cstrategy_semantic_preservation _ _ MATCH)).
   exploit backward_simulation_same_safe_behavior.
-    apply (snd (transf_cstrategy_program_correct _ _ H)).
+    apply (proj2 (cstrategy_semantic_preservation _ _ MATCH)).
     intros. rewrite <- atomic_behaviors in H2; eauto. eauto.
     intros. rewrite atomic_behaviors; auto.
 Qed.