The whole compiler and its proof of semantic preservation

Libraries.

Require Import String.
Require Import Coqlib Errors.
Require Import AST Linking Smallstep.

Languages (syntax and semantics).

Require Ctypes Csyntax Csem Cstrategy Cexec.
Require Clight.
Require Csharpminor.
Require Cminor.
Require CminorSel.
Require RTL.
Require LTL.
Require Linear.
Require Mach.
Require Asm.

Translation passes.

Require Initializers.
Require SimplExpr.
Require SimplLocals.
Require Cshmgen.
Require Cminorgen.
Require Selection.
Require RTLgen.
Require Tailcall.
Require Inlining.
Require Renumber.
Require Constprop.
Require CSE.
Require Deadcode.
Require Unusedglob.

SSA middle-end passes

Require RTLnorm.
Require RTLdfs.
Require RTLdfsgen.
Require SSAvalid.
Require SCCPopt.
Require GVNopt.
Require CSSAgen.
Require RTLpargen.
Require RTLparcleanup.
Require RTLdpar.

Require Allocation.
Require Tunneling.
Require Linearize.
Require CleanupLabels.
Require Debugvar.
Require Stacking.
Require Asmgen.

Proofs of semantic preservation.

Require SimplExprproof.
Require SimplLocalsproof.
Require Cshmgenproof.
Require Cminorgenproof.
Require Selectionproof.
Require RTLgenproof.
Require Tailcallproof.
Require Inliningproof.
Require Renumberproof.
Require Constpropproof.
Require CSEproof.
Require Deadcodeproof.
Require Unusedglobproof.

Require RTLnormproof.
Require RTLdfsproof.
Require SSAvalidproof.
Require SCCPoptproof.
Require GVNoptproof.
Require CSSAproof CSSAgenwf.
Require RTLparproof.
Require RTLparcleanup.
Require RTLdparproof.

Require Allocproof.
Require Tunnelingproof.
Require Linearizeproof.
Require CleanupLabelsproof.
Require Debugvarproof.
Require Stackingproof.
Require Asmgenproof.

Command-line flags.

Require Import Compopts.

Pretty-printers (defined in Caml).

Parameter print_Clight: Clight.program -> unit.
Parameter print_Cminor: Cminor.program -> unit.
Parameter print_RTL: Z -> RTL.program -> unit.
Parameter print_LTL: LTL.program -> unit.
Parameter print_Mach: Mach.program -> unit.

Parameter print_RTL_norm: RTLdfs.program -> unit.
Parameter print_SSA: Z -> SSA.program -> unit.
Parameter print_CSSA: CSSA.program -> unit.
Parameter print_RTLpar: RTLpar.program -> unit.

Local Open Scope string_scope.

Composing the translation passes

We first define useful monadic composition operators, along with funny (but convenient) notations.

Definition apply_total (A B: Type) (x: res A) (f: A -> B) : res B :=
  match x with Error msg => Error msg | OK x1 => OK (f x1) end.

Definition apply_partial (A B: Type)
                         (x: res A) (f: A -> res B) : res B :=
  match x with Error msg => Error msg | OK x1 => f x1 end.

Notation "a @@@ b" :=
   (apply_partial _ _ a b) (at level 50, left associativity).
Notation "a @@ b" :=
   (apply_total _ _ a b) (at level 50, left associativity).

Definition print {A: Type} (printer: A -> unit) (prog: A) : A :=
  let unused := printer prog in prog.

Definition time {A B: Type} (name: string) (f: A -> B) : A -> B := f.

Definition total_if {A: Type}
          (flag: unit -> bool) (f: A -> A) (prog: A) : A :=
  if flag tt then f prog else prog.

Definition partial_if {A: Type}
          (flag: unit -> bool) (f: A -> res A) (prog: A) : res A :=
  if flag tt then f prog else OK prog.

We define three translation functions for whole programs: one starting with a C program, one with a Cminor program, one with an RTL program. The three translations produce Asm programs ready for pretty-printing and assembling.

Force Initializers and Cexec to be extracted as well.

Definition transl_init := Initializers.transl_init.
Definition cexec_do_step := Cexec.do_step.

The following lemmas help reason over compositions of passes.

Lemma print_identity:
forall (A: Type) (printer: A -> unit) (prog: A),
print printer prog = prog.

Proof.

intros; unfold print. destruct (printer prog); auto.
Qed.

Lemma compose_print_identity:
forall (A: Type) (x: res A) (f: A -> unit),
x @@ print f = x.

Proof.

intros. destruct x; simpl. rewrite print_identity. auto. auto.
Qed.

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. unfold match_if, total_if. destruct (flag tt); auto.
Qed.

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 match_if, partial_if in *. destruct (flag tt). auto. congruence.
Qed.

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).

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 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.

The transf_c_program_via_SSA function, when successful, produces assembly code that is in the match_prog_SSA relation with the source C program.

Definition match_prog_SSA: Csyntax.program -> Asm.program -> Prop :=
pass_match (compose_passes CompCertSSA's_passes).

Lemma simpl_total_if : forall (A: Type) (x: A) b (f: A -> A),
OK x @@ total_if b f = OK (total_if b f x).

Proof.

reflexivity.
Qed.

Lemma simpl_partial_total : forall (A B:Type) (x: A) (f: A -> res B),
(OK x @@@ f) = f x.

Proof.

reflexivity.
Qed.

Theorem transf_c_program_via_SSA_match:
  forall p tp,
  transf_c_program_via_SSA p = OK tp ->
  match_prog_SSA p tp.

Proof.

  intros p tp T.
  unfold transf_c_program_via_SSA, 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_via_SSA, 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_via_SSA, 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_via_SSA, time in T. rewrite ! compose_print_identity in T.
  rewrite simpl_total_if in T; rewrite simpl_partial_total 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 (RTLnorm.transl_program p14) as [p141|e] eqn:P141; simpl in T; try discriminate.
  destruct (RTLdfsgen.transf_program p141) as [p142|e] eqn:P142; simpl in T; try discriminate.
  destruct (SSAvalid.transf_program p142) as [p143|e] eqn:P143; simpl in T; try discriminate.
  set (p144 := GVNopt.transf_program p143) in *.
  set (p145 := SCCPopt.transf_program p144) in *.

  destruct (CSSAgen.transl_program p145) as [p146|e] eqn: P146; simpl in T; try discriminate.
  destruct (RTLpargen.transl_program p146) as [p147|e] eqn: P147; simpl in T; try discriminate.
  destruct (RTLparcleanup.transl_program p147) as [p148|e] eqn: P148; simpl in T; try discriminate.
  destruct (RTLdpar.transl_program p148) as [p149|e] eqn:P149; simpl in T; try discriminate.

  set (p150 := Renumber.transf_program p149) in *.

  destruct (Allocation.transf_program p150) 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_SSA; 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 p141; split. apply RTLnormproof.transf_program_match; auto.
  exists p142; split. apply RTLdfsproof.transf_program_match; auto.
  exists p143; split. apply SSAvalidproof.transf_program_match; auto.
  exists p144; split. apply GVNoptproof.transf_program_match; auto.
  exists p145; split. apply SCCPoptproof.transf_program_match; auto.

  exists p146; split. apply CSSAproof.transf_program_match; auto.
  exists p147; split. apply RTLparproof.transf_program_match; auto.
  exists p148; split. apply RTLparcleanup.transf_program_match; auto.
  exists p149; split. apply RTLdparproof.transf_program_match; auto.

  exists p150; split. apply Renumberproof.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 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).

Remark forward_simulation_identity:
forall sem, forward_simulation sem sem.

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.
Qed.

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. unfold match_if in *. destruct (flag tt). eauto. subst. apply forward_simulation_identity.
Qed.

Theorem cstrategy_semantic_preservation:
  forall p tp,
  match_prog p tp ->
  forward_simulation (Cstrategy.semantics p) (Asm.semantics tp)
  /\ backward_simulation (atomic (Cstrategy.semantics p)) (Asm.semantics tp).

Proof.

Theorem cstrategy_semantic_preservation_via_SSA:
  forall p tp,
  match_prog_SSA p tp ->
  forward_simulation (Cstrategy.semantics p) (Asm.semantics tp)
  /\ backward_simulation (atomic (Cstrategy.semantics p)) (Asm.semantics tp).

Proof.

Theorem c_semantic_preservation:
  forall p tp,
  match_prog p tp ->
  backward_simulation (Csem.semantics p) (Asm.semantics tp).

Proof.

  intros.
  apply compose_backward_simulation with (atomic (Cstrategy.semantics p)).
  eapply sd_traces; eapply Asm.semantics_determinate.
  apply factor_backward_simulation.
  apply Cstrategy.strategy_simulation.
  apply Csem.semantics_single_events.
  eapply ssr_well_behaved; eapply Cstrategy.semantics_strongly_receptive.
  exact (proj2 (cstrategy_semantic_preservation _ _ H)).
Qed.

Theorem c_semantic_preservation_via_SSA:
  forall p tp,
  match_prog_SSA p tp ->
  backward_simulation (Csem.semantics p) (Asm.semantics tp).

Proof.

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.

Theorem transf_c_program_correct_via_SSA:
  forall p tp,
  transf_c_program_via_SSA p = OK tp ->
  backward_simulation (Csem.semantics p) (Asm.semantics tp).

Proof.

intros. apply c_semantic_preservation_via_SSA.
apply transf_c_program_via_SSA_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.

Theorem separate_transf_c_program_via_SSA_correct:
  forall c_units asm_units c_program,
  nlist_forall2 (fun cu tcu => transf_c_program_via_SSA 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_SSA c_units asm_units).
  { eapply nlist_forall2_imply. eauto. simpl; intros. apply transf_c_program_via_SSA_match; auto. }
  assert (exists asm_program, link_list asm_units = Some asm_program /\ match_prog_SSA 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_via_SSA; auto.
Qed.

Module Compiler

Composing the translation passes

Relational specification of compilation

Semantic preservation

Correctness of the CompCert compiler