Module Compiler


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 Import Duplicatepasses.
Require Tailcall.
Require Tailrec.
Require Inlining.
Require Profiling.
Require ProfilingExploit.
Require Renumber.
Require CSE.
Require Constprop.
Require Intervalprop.
Require CSE.
Require CSE2.
Require CSE3.
Require KillUselessMoves.
Require ForwardMoves.
Require Deadcode.
Require RTLTunneling.
Require Allnontrap.
Require Canary.
Require Renumber.
Require Unusedglob.
Require ForwardMoves.
Require Allocation.
Require LTLTunneling.
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 Tailrecproof.
Require Inliningproof.
Require Profilingproof.
Require ProfilingExploitproof.
Require Renumberproof.
Require CSEproof.
Require Constpropproof.
Require Intervalpropproof.
Require CSEproof.
Require CSE2proof.
Require CSE3proof.
Require KillUselessMovesproof.
Require ForwardMovesproof.
Require Deadcodeproof.
Require RTLTunnelingproof.
Require Allnontrapproof.
Require Canaryproof.
Require Renumberproof.
Require Unusedglobproof.
Require ForwardMovesproof.
Require Allocationproof.
Require LTLTunnelingproof.
Require Linearizeproof.
Require CleanupLabelsproof.
Require Debugvarproof.
Require Stackingproof.
Require Import Asmgenproof.
Command-line flags.
Require Import Compopts.
Require Import BTLpasses.

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: Z -> LTL.program -> unit.
Parameter print_Mach: Mach.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.

Definition transf_rtl_program (f: RTL.program) : res Asm.program :=
   OK f
   @@ print (print_RTL 0)
   @@ total_if Compopts.optim_tailcalls (time "Tail calls" Tailcall.transf_program)
   @@ print (print_RTL 1)
  @@@ partial_if Compopts.optim_tailrec (time "Tail recursion" Tailrec.transf_program)
   @@ print (print_RTL 2)
  @@@ (time "Inlining" Inlining.transf_program)
   @@ print (print_RTL 3)
   @@ total_if Compopts.profile_arcs (time "Profiling insertion" Profiling.transf_program)
   @@ print (print_RTL 4)
   @@ total_if Compopts.branch_probabilities (time "Profiling use" ProfilingExploit.transf_program)
   @@ print (print_RTL 5)
   @@ (time "Renumbering" Renumber.transf_program)
   @@ print (print_RTL 6)
  @@@ partial_if Compopts.optim_CSE (time "CSE" CSE.transf_program)
   @@ print (print_RTL 7)
  @@@ (time "Static Prediction + inverting conditions" Staticpredict.transf_program)
   @@ print (print_RTL 8)
  @@@ (time "Unrolling one iteration out of innermost loops" Unrollsingle.transf_program)
   @@ print (print_RTL 9)
   @@ (time "Renumbering pre tail duplication" Renumber.transf_program)
   @@ print (print_RTL 10)
  @@@ (time "Performing tail duplication" Tailduplicate.transf_program)
   @@ print (print_RTL 11)
   @@ (time "Renumbering pre unrolling" Renumber.transf_program)
   @@ print (print_RTL 12)
  @@@ (time "Unrolling the body of innermost loops" Unrollbody.transf_program)
   @@ print (print_RTL 13)
   @@ (time "Renumbering pre rotate" Renumber.transf_program)
   @@ print (print_RTL 14)
  @@@ (time "Loop Rotate" Looprotate.transf_program)
   @@ print (print_RTL 15)
   @@ (time "Renumbering pre constprop" Renumber.transf_program)
   @@ print (print_RTL 16)
   @@ total_if Compopts.optim_constprop (time "Constant propagation" Constprop.transf_program)
   @@ print (print_RTL 17)
   @@ total_if Compopts.optim_intervalprop (time "Interval propagation" Intervalprop.transf_program)
   @@ print (print_RTL 18)
  @@@ partial_if Compopts.optim_lct_promote (time "Int promotion" BTL_IntPromotionpasses.transf_program)
   @@ print (print_RTL 19)
   @@ (time "Renumbering pre CSE" Renumber.transf_program)
   @@ print (print_RTL 20)
  @@@ partial_if Compopts.optim_CSE (time "CSE" CSE.transf_program)
   @@ print (print_RTL 21)
   @@ total_if Compopts.optim_CSE2 (time "CSE2" CSE2.transf_program)
   @@ print (print_RTL 22)
  @@@ partial_if Compopts.optim_CSE3 (time "CSE3" CSE3.transf_program)
   @@ print (print_RTL 23)
   @@ total_if Compopts.optim_CSE3 (time "Kill useless moves after CSE3" KillUselessMoves.transf_program)
   @@ print (print_RTL 24)
   @@ total_if Compopts.optim_forward_moves (time "Forwarding moves" ForwardMoves.transf_program)
   @@ print (print_RTL 25)
  @@@ partial_if Compopts.optim_redundancy (time "Redundancy elimination" Deadcode.transf_program)
   @@ print (print_RTL 26)
  @@@ (time "RTL Branch Tunneling" RTLTunneling.transf_program)
   @@ print (print_RTL 27)
   @@ total_if Compopts.all_loads_nontrap (Allnontrap.transf_program)
   @@ print (print_RTL 28)
   @@ total_if Compopts.stack_protector (time "Canary" Canary.transf_program)
   @@ print (print_RTL 29)
   @@ total_if Compopts.stack_protector (time "Post-canary renumber" Renumber.transf_program)
   @@ print (print_RTL 30)
  @@@ (time "Unused globals" Unusedglob.transf_program)
   @@ print (print_RTL 31)
   @@ total_if Compopts.btl_bb (time "Renumbering pre BTL (BB)" Renumber.transf_program)
   @@ print (print_RTL 32)
  @@@ partial_if Compopts.btl_bb (time "BTL BBpasses" BTL_BBpasses.transf_program)
   @@ print (print_RTL 33)
  @@@ partial_if Compopts.lct_tun (time "RTL Tunneling post LCT" RTLTunneling.transf_program)
   @@ print (print_RTL 34)
   @@ total_if Compopts.btl_sb (time "Renumbering pre BTL (SB)" Renumber.transf_program)
   @@ print (print_RTL 35)
  @@@ partial_if Compopts.btl_sb (time "BTL SBpasses" BTL_SBpasses.transf_program)
   @@ print (print_RTL 36)
   @@ total_if Compopts.optim_forward_moves (time "Forwarding moves post scheduling" ForwardMoves.transf_program)
   @@ print (print_RTL 37)
   @@ total_if Compopts.optim_constprop2 (time "Post-BTL constant propagation" Constprop.transf_program)
   @@ print (print_RTL 38)
   @@ total_if Compopts.final_renumber (time "Final renumber" Renumber.transf_program)
  @@@ (time "Register allocation" Allocation.transf_program)
   @@ print (print_LTL 1)
  @@@ (time "LTL Branch tunneling" LTLTunneling.transf_program)
   @@ print (print_LTL 2)
  @@@ (time "CFG linearization" Linearize.transf_program)
   @@ (time "Label cleanup" CleanupLabels.transf_program)
  @@@ partial_if Compopts.debug (time "Debugging info for local variables" Debugvar.transf_program)
  @@@ (time "Mach generation" Stacking.transf_program)
   @@ print (print_Mach)
  @@@ time "Total Mach->Asm generation" Asmgen.transf_program.
   
Definition transf_cminor_program (p: Cminor.program) : res Asm.program :=
   OK p
   @@ print print_Cminor
  @@@ time "Instruction selection" Selection.sel_program
  @@@ time "RTL generation" RTLgen.transl_program
  @@@ transf_rtl_program.

Definition transf_clight_program (p: Clight.program) : res Asm.program :=
  OK p
   @@ print print_Clight
  @@@ time "Simplification of locals" SimplLocals.transf_program
  @@@ time "C#minor generation" Cshmgen.transl_program
  @@@ time "Cminor generation" Cminorgen.transl_program
  @@@ transf_cminor_program.

Definition transf_c_program (p: Csyntax.program) : res Asm.program :=
  OK p
  @@@ time "Clight generation" SimplExpr.transl_program
  @@@ transf_clight_program.

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.

Global 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 (match_if Compopts.optim_tailrec Tailrecproof.match_prog)
  ::: mkpass (Inliningproof.match_prog)
  ::: mkpass (match_if Compopts.profile_arcs Profilingproof.match_prog)
  ::: mkpass (match_if Compopts.branch_probabilities ProfilingExploitproof.match_prog)
  ::: mkpass (Renumberproof.match_prog)
  ::: mkpass (match_if Compopts.optim_CSE CSEproof.match_prog)
  ::: mkpass (Staticpredictproof.match_prog)
  ::: mkpass (Unrollsingleproof.match_prog)
  ::: mkpass (Renumberproof.match_prog)
  ::: mkpass (Tailduplicateproof.match_prog)
  ::: mkpass (Renumberproof.match_prog)
  ::: mkpass (Unrollbodyproof.match_prog)
  ::: mkpass (Renumberproof.match_prog)
  ::: mkpass (Looprotateproof.match_prog)
  ::: mkpass (Renumberproof.match_prog)
  ::: mkpass (match_if Compopts.optim_constprop Constpropproof.match_prog)
  ::: mkpass (match_if Compopts.optim_intervalprop Intervalpropproof.match_prog)
  ::: mkpass (match_if Compopts.optim_lct_promote BTL_IntPromotionpassesproof.match_prog)
  ::: mkpass (Renumberproof.match_prog)
  ::: mkpass (match_if Compopts.optim_CSE CSEproof.match_prog)
  ::: mkpass (match_if Compopts.optim_CSE2 CSE2proof.match_prog)
  ::: mkpass (match_if Compopts.optim_CSE3 CSE3proof.match_prog)
  ::: mkpass (match_if Compopts.optim_CSE3 KillUselessMovesproof.match_prog)
  ::: mkpass (match_if Compopts.optim_forward_moves ForwardMovesproof.match_prog)
  ::: mkpass (match_if Compopts.optim_redundancy Deadcodeproof.match_prog)
  ::: mkpass (RTLTunnelingproof.match_prog)
  ::: mkpass (match_if Compopts.all_loads_nontrap Allnontrapproof.match_prog)
  ::: mkpass (match_if Compopts.stack_protector Canaryproof.match_prog)
  ::: mkpass (match_if Compopts.stack_protector Renumberproof.match_prog)
  ::: mkpass (Unusedglobproof.match_prog)
  ::: mkpass (match_if Compopts.btl_bb Renumberproof.match_prog)
  ::: mkpass (match_if Compopts.btl_bb BTL_BBpassesproof.match_prog)
  ::: mkpass (match_if Compopts.lct_tun RTLTunnelingproof.match_prog)
  ::: mkpass (match_if Compopts.btl_sb Renumberproof.match_prog)
  ::: mkpass (match_if Compopts.btl_sb BTL_SBpassesproof.match_prog)
  ::: mkpass (match_if Compopts.optim_forward_moves ForwardMovesproof.match_prog)
  ::: mkpass (match_if Compopts.optim_constprop2 Constpropproof.match_prog)
  ::: mkpass (match_if Compopts.final_renumber Renumberproof.match_prog)
  ::: mkpass (Allocationproof.match_prog)
  ::: mkpass (LTLTunnelingproof.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 p tp T.
  unfold transf_c_program, time in T. cbn in T.
  destruct (SimplExpr.transl_program p) as [p1|e] eqn:P1; cbn in T; try discriminate.
  unfold transf_clight_program, time in T. rewrite ! compose_print_identity in T. cbn in T.
  destruct (SimplLocals.transf_program p1) as [p2|e] eqn:P2; cbn in T; try discriminate.
  destruct (Cshmgen.transl_program p2) as [p3|e] eqn:P3; cbn in T; try discriminate.
  destruct (Cminorgen.transl_program p3) as [p4|e] eqn:P4; cbn in T; try discriminate.
  unfold transf_cminor_program, time in T. rewrite ! compose_print_identity in T. cbn in T.
  destruct (Selection.sel_program p4) as [p5|e] eqn:P5; cbn in T; try discriminate.
  destruct (RTLgen.transl_program p5) as [p6|e] eqn:P6; cbn in T; try discriminate.
  unfold transf_rtl_program, time in T. rewrite ! compose_print_identity in T.
  cbn in T.
set (p7 := total_if optim_tailcalls Tailcall.transf_program p6) in *.
destruct (partial_if optim_tailrec Tailrec.transf_program p7) as [p8|e] eqn:P8; cbn in T; try discriminate.
destruct (Inlining.transf_program p8) as [p9|e] eqn:P9; cbn in T; try discriminate.
set (p10 := total_if profile_arcs Profiling.transf_program p9) in *.
set (p11 := total_if branch_probabilities ProfilingExploit.transf_program p10) in *.
set (p12 := Renumber.transf_program p11) in *.
destruct (partial_if optim_CSE CSE.transf_program p12) as [p13|e] eqn:P13; cbn in T; try discriminate.
destruct (Staticpredict.transf_program p13) as [p14|e] eqn:P14; cbn in T; try discriminate.
destruct (Unrollsingle.transf_program p14) as [p15|e] eqn:P15; cbn in T; try discriminate.
set (p16 := Renumber.transf_program p15) in *.
destruct (Tailduplicate.transf_program p16) as [p17|e] eqn:P17; cbn in T; try discriminate.
set (p18 := Renumber.transf_program p17) in *.
destruct (Unrollbody.transf_program p18) as [p19|e] eqn:P19; cbn in T; try discriminate.
set (p20 := Renumber.transf_program p19) in *.
destruct (Looprotate.transf_program p20) as [p21|e] eqn:P21; cbn in T; try discriminate.
set (p22 := Renumber.transf_program p21) in *.
set (p23 := total_if optim_constprop Constprop.transf_program p22) in *.
set (p24 := total_if optim_intervalprop Intervalprop.transf_program p23) in *.
destruct (partial_if optim_lct_promote BTL_IntPromotionpasses.transf_program p24) as [p25|e] eqn:P25; cbn in T; try discriminate.
set (p26 := Renumber.transf_program p25) in *.
destruct (partial_if optim_CSE CSE.transf_program p26) as [p27|e] eqn:P27; cbn in T; try discriminate.
set (p28 := total_if optim_CSE2 CSE2.transf_program p27) in *.
destruct (partial_if optim_CSE3 CSE3.transf_program p28) as [p29|e] eqn:P29; cbn in T; try discriminate.
set (p30 := total_if optim_CSE3 KillUselessMoves.transf_program p29) in *.
set (p31 := total_if optim_forward_moves ForwardMoves.transf_program p30) in *.
destruct (partial_if optim_redundancy Deadcode.transf_program p31) as [p32|e] eqn:P32; cbn in T; try discriminate.
destruct (RTLTunneling.transf_program p32) as [p33|e] eqn:P33; cbn in T; try discriminate.
set (p34 := total_if all_loads_nontrap Allnontrap.transf_program p33) in *.
set (p35 := total_if stack_protector Canary.transf_program p34) in *.
set (p36 := total_if stack_protector Renumber.transf_program p35) in *.
destruct (Unusedglob.transf_program p36) as [p37|e] eqn:P37; cbn in T; try discriminate.
set (p38 := total_if btl_bb Renumber.transf_program p37) in *.
destruct (partial_if btl_bb BTL_BBpasses.transf_program p38) as [p39|e] eqn:P39; cbn in T; try discriminate.
destruct (partial_if lct_tun RTLTunneling.transf_program p39) as [p40|e] eqn:P40; cbn in T; try discriminate.
set (p41 := total_if btl_sb Renumber.transf_program p40) in *.
destruct (partial_if btl_sb BTL_SBpasses.transf_program p41) as [p42|e] eqn:P42; cbn in T; try discriminate.
set (p43 := total_if optim_forward_moves ForwardMoves.transf_program p42) in *.
set (p44 := total_if optim_constprop2 Constprop.transf_program p43) in *.
set (p45 := total_if final_renumber Renumber.transf_program p44) in *.
destruct (Allocation.transf_program p45) as [p46|e] eqn:P46; cbn in T; try discriminate.
destruct (LTLTunneling.transf_program p46) as [p47|e] eqn:P47; cbn in T; try discriminate.
destruct (Linearize.transf_program p47) as [p48|e] eqn:P48; cbn in T; try discriminate.
set (p49 := CleanupLabels.transf_program p48) in *.
destruct (partial_if debug Debugvar.transf_program p49) as [p50|e] eqn:P50; cbn in T; try discriminate.
destruct (Stacking.transf_program p50) as [p51|e] eqn:P51; cbn 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; auto.
  exists p8; split. eapply partial_if_match; eauto. apply Tailrecproof.transf_program_match; auto.
  exists p9; split. apply Inliningproof.transf_program_match; auto.
  exists p10; split. apply total_if_match. apply Profilingproof.transf_program_match; auto.
  exists p11; split. apply total_if_match. apply ProfilingExploitproof.transf_program_match; auto.
  exists p12; split. apply Renumberproof.transf_program_match; auto.
  exists p13; split. eapply partial_if_match; eauto. apply CSEproof.transf_program_match; auto.
  exists p14; split. apply Staticpredictproof.transf_program_match; auto.
  exists p15; split. apply Unrollsingleproof.transf_program_match; auto.
  exists p16; split. apply Renumberproof.transf_program_match; auto.
  exists p17; split. apply Tailduplicateproof.transf_program_match; auto.
  exists p18; split. apply Renumberproof.transf_program_match; auto.
  exists p19; split. apply Unrollbodyproof.transf_program_match; auto.
  exists p20; split. apply Renumberproof.transf_program_match; auto.
  exists p21; split. apply Looprotateproof.transf_program_match; auto.
  exists p22; split. apply Renumberproof.transf_program_match; auto.
  exists p23; split. apply total_if_match. apply Constpropproof.transf_program_match; auto.
  exists p24; split. apply total_if_match. apply Intervalpropproof.transf_program_match; auto.
  exists p25; split. eapply partial_if_match; eauto. apply BTL_IntPromotionpassesproof.transf_program_match; auto.
  exists p26; split. apply Renumberproof.transf_program_match; auto.
  exists p27; split. eapply partial_if_match; eauto. apply CSEproof.transf_program_match; auto.
  exists p28; split. apply total_if_match. apply CSE2proof.transf_program_match; auto.
  exists p29; split. eapply partial_if_match; eauto. apply CSE3proof.transf_program_match; auto.
  exists p30; split. apply total_if_match. apply KillUselessMovesproof.transf_program_match; auto.
  exists p31; split. apply total_if_match. apply ForwardMovesproof.transf_program_match; auto.
  exists p32; split. eapply partial_if_match; eauto. apply Deadcodeproof.transf_program_match; auto.
  exists p33; split. apply RTLTunnelingproof.transf_program_match; auto.
  exists p34; split. apply total_if_match. apply Allnontrapproof.transf_program_match; auto.
  exists p35; split. apply total_if_match. apply Canaryproof.transf_program_match; auto.
  exists p36; split. apply total_if_match. apply Renumberproof.transf_program_match; auto.
  exists p37; split. apply Unusedglobproof.transf_program_match; auto.
  exists p38; split. apply total_if_match. apply Renumberproof.transf_program_match; auto.
  exists p39; split. eapply partial_if_match; eauto. apply BTL_BBpassesproof.transf_program_match; auto.
  exists p40; split. eapply partial_if_match; eauto. apply RTLTunnelingproof.transf_program_match; auto.
  exists p41; split. apply total_if_match. apply Renumberproof.transf_program_match; auto.
  exists p42; split. eapply partial_if_match; eauto. apply BTL_SBpassesproof.transf_program_match; auto.
  exists p43; split. apply total_if_match. apply ForwardMovesproof.transf_program_match; auto.
  exists p44; split. apply total_if_match. apply Constpropproof.transf_program_match; auto.
  exists p45; split. apply total_if_match. apply Renumberproof.transf_program_match; auto.
  exists p46; split. apply Allocationproof.transf_program_match; auto.
  exists p47; split. apply LTLTunnelingproof.transf_program_match; auto.
  exists p48; split. apply Linearizeproof.transf_program_match; auto.
  exists p49; split. apply CleanupLabelsproof.transf_program_match; auto.
  exists p50; split. eapply partial_if_match; eauto. apply Debugvarproof.transf_program_match; auto.
  exists p51; 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:

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.
  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 p52)
         ).
  {
  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. eapply Tailcallproof.transf_program_correct; eassumption. eapply compose_forward_simulations.
    eapply match_if_simulation. eassumption. eapply Tailrecproof.transf_program_correct; eassumption. eapply compose_forward_simulations.
    eapply Inliningproof.transf_program_correct; eassumption. eapply compose_forward_simulations.
    eapply match_if_simulation. eassumption. eapply Profilingproof.transf_program_correct; eassumption. eapply compose_forward_simulations.
    eapply match_if_simulation. eassumption. eapply ProfilingExploitproof.transf_program_correct; eassumption. eapply compose_forward_simulations.
    eapply Renumberproof.transf_program_correct; eassumption. eapply compose_forward_simulations.
    eapply match_if_simulation. eassumption. eapply CSEproof.transf_program_correct; eassumption. eapply compose_forward_simulations.
    eapply Staticpredictproof.transf_program_correct; eassumption. eapply compose_forward_simulations.
    eapply Unrollsingleproof.transf_program_correct; eassumption. eapply compose_forward_simulations.
    eapply Renumberproof.transf_program_correct; eassumption. eapply compose_forward_simulations.
    eapply Tailduplicateproof.transf_program_correct; eassumption. eapply compose_forward_simulations.
    eapply Renumberproof.transf_program_correct; eassumption. eapply compose_forward_simulations.
    eapply Unrollbodyproof.transf_program_correct; eassumption. eapply compose_forward_simulations.
    eapply Renumberproof.transf_program_correct; eassumption. eapply compose_forward_simulations.
    eapply Looprotateproof.transf_program_correct; eassumption. eapply compose_forward_simulations.
    eapply Renumberproof.transf_program_correct; eassumption. eapply compose_forward_simulations.
    eapply match_if_simulation. eassumption. eapply Constpropproof.transf_program_correct; eassumption. eapply compose_forward_simulations.
    eapply match_if_simulation. eassumption. eapply Intervalpropproof.transf_program_correct; eassumption. eapply compose_forward_simulations.
    eapply match_if_simulation. eassumption. eapply BTL_IntPromotionpassesproof.transf_program_correct; eassumption. eapply compose_forward_simulations.
    eapply Renumberproof.transf_program_correct; eassumption. eapply compose_forward_simulations.
    eapply match_if_simulation. eassumption. eapply CSEproof.transf_program_correct; eassumption. eapply compose_forward_simulations.
    eapply match_if_simulation. eassumption. eapply CSE2proof.transf_program_correct; eassumption. eapply compose_forward_simulations.
    eapply match_if_simulation. eassumption. eapply CSE3proof.transf_program_correct; eassumption. eapply compose_forward_simulations.
    eapply match_if_simulation. eassumption. eapply KillUselessMovesproof.transf_program_correct; eassumption. eapply compose_forward_simulations.
    eapply match_if_simulation. eassumption. eapply ForwardMovesproof.transf_program_correct; eassumption. eapply compose_forward_simulations.
    eapply match_if_simulation. eassumption. eapply Deadcodeproof.transf_program_correct; eassumption. eapply compose_forward_simulations.
    eapply RTLTunnelingproof.transf_program_correct; eassumption. eapply compose_forward_simulations.
    eapply match_if_simulation. eassumption. eapply Allnontrapproof.transf_program_correct; eassumption. eapply compose_forward_simulations.
    eapply match_if_simulation. eassumption. eapply Canaryproof.transf_program_correct; eassumption. eapply compose_forward_simulations.
    eapply match_if_simulation. eassumption. eapply Renumberproof.transf_program_correct; eassumption. eapply compose_forward_simulations.
    eapply Unusedglobproof.transf_program_correct; eassumption. eapply compose_forward_simulations.
    eapply match_if_simulation. eassumption. eapply Renumberproof.transf_program_correct; eassumption. eapply compose_forward_simulations.
    eapply match_if_simulation. eassumption. eapply BTL_BBpassesproof.transf_program_correct; eassumption. eapply compose_forward_simulations.
    eapply match_if_simulation. eassumption. eapply RTLTunnelingproof.transf_program_correct; eassumption. eapply compose_forward_simulations.
    eapply match_if_simulation. eassumption. eapply Renumberproof.transf_program_correct; eassumption. eapply compose_forward_simulations.
    eapply match_if_simulation. eassumption. eapply BTL_SBpassesproof.transf_program_correct; eassumption. eapply compose_forward_simulations.
    eapply match_if_simulation. eassumption. eapply ForwardMovesproof.transf_program_correct; eassumption. eapply compose_forward_simulations.
    eapply match_if_simulation. eassumption. eapply Constpropproof.transf_program_correct; eassumption. eapply compose_forward_simulations.
    eapply match_if_simulation. eassumption. eapply Renumberproof.transf_program_correct; eassumption.
  eapply compose_forward_simulations.
    eapply Allocationproof.transf_program_correct; eassumption.
  eapply compose_forward_simulations.
    eapply LTLTunnelingproof.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.
  apply atomic_receptive. apply Cstrategy.semantics_strongly_receptive.
  apply Asm.semantics_determinate.
Qed.

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.

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.
Generated by coq2html