(* *********************************************************************)
(*                                                                     *)
(*              The Compcert verified compiler                         *)
(*                                                                     *)
(*          Xavier Leroy, INRIA Paris-Rocquencourt                     *)
(*                                                                     *)
(*  Copyright Institut National de Recherche en Informatique et en     *)
(*  Automatique.  All rights reserved.  This file is distributed       *)
(*  under the terms of the INRIA Non-Commercial License Agreement.     *)
(*                                                                     *)
(* *********************************************************************)

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

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)
  @@@ time "Inlining" Inlining.transf_program
   @@ print (print_RTL 2)
   @@ time "Renumbering" Renumber.transf_program
   @@ print (print_RTL 3)
   @@ total_if Compopts.optim_constprop (time "Constant propagation" Constprop.transf_program)
   @@ print (print_RTL 4)
   @@ total_if Compopts.optim_constprop (time "Renumbering" Renumber.transf_program)
   @@ print (print_RTL 5)
  @@@ partial_if Compopts.optim_CSE (time "CSE" CSE.transf_program)
   @@ print (print_RTL 6)
  @@@ partial_if Compopts.optim_redundancy (time "Redundancy elimination" Deadcode.transf_program)
   @@ print (print_RTL 7)
  @@@ time "Unused globals" Unusedglob.transform_program
   @@ print (print_RTL 8)
  @@@ time "Register allocation" Allocation.transf_program
   @@ print print_LTL
   @@ time "Branch tunneling" Tunneling.tunnel_program
  @@@ 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 "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.
(* Goal: forall (A : Type) (printer : forall _ : A, unit) (prog : A), @eq A (@print A printer prog) prog *)
  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.
(* Goal: forall (p : Csyntax.program) (tp : Asm.program) (_ : @eq (res Asm.program) (transf_c_program p) (@OK Asm.program tp)), backward_simulation (Csem.semantics p) (Asm.semantics tp) *)
  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.
(* Goal: forall (p : Csyntax.program) (tp : Asm.program) (_ : @eq (res Asm.program) (transf_c_program p) (@OK Asm.program tp)), backward_simulation (Csem.semantics p) (Asm.semantics tp) *)
  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.
(* Goal: forall (p : Csyntax.program) (tp : Asm.program) (_ : @eq (res Asm.program) (transf_c_program p) (@OK Asm.program tp)), backward_simulation (Csem.semantics p) (Asm.semantics tp) *)
  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.
(* Goal: forward_simulation (sem prog) (sem tprog) *)
  unfold match_if. destruct (flag tt).
(* Goal: @eq bool (Globalenvs.Senv.public_symbol (symbolenv sem) id) (Globalenvs.Senv.public_symbol (symbolenv sem) id) *)
- auto.
(* Goal: forall (p : Csyntax.program) (tp : Asm.program) (_ : @eq (res Asm.program) (transf_c_program p) (@OK Asm.program tp)), backward_simulation (Csem.semantics p) (Asm.semantics tp) *)
- 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.
(* Goal: forall (p : Csyntax.program) (tp : Asm.program) (_ : @eq (res Asm.program) (transf_c_program p) (@OK Asm.program tp)), match_prog p tp *)
  intros p tp T.
(* Goal: match_prog p tp *)
  unfold transf_c_program, time in T. simpl in T.
(* Goal: match_prog p tp *)
  destruct (SimplExpr.transl_program p) as [p1|e] eqn:P1; simpl in T; try discriminate.
(* Goal: match_prog p tp *)
  unfold transf_clight_program, time in T. rewrite ! compose_print_identity in T. simpl in T.
(* Goal: match_prog p tp *)
  destruct (SimplLocals.transf_program p1) as [p2|e] eqn:P2; simpl in T; try discriminate.
(* Goal: match_prog p tp *)
  destruct (Cshmgen.transl_program p2) as [p3|e] eqn:P3; simpl in T; try discriminate.
(* Goal: match_prog p tp *)
  destruct (Cminorgen.transl_program p3) as [p4|e] eqn:P4; simpl in T; try discriminate.
(* Goal: match_prog p tp *)
  unfold transf_cminor_program, time in T. rewrite ! compose_print_identity in T. simpl in T.
(* Goal: match_prog p tp *)
  destruct (Selection.sel_program p4) as [p5|e] eqn:P5; simpl in T; try discriminate.
(* Goal: match_prog p tp *)
  destruct (RTLgen.transl_program p5) as [p6|e] eqn:P6; simpl in T; try discriminate.
(* Goal: match_prog p tp *)
  unfold transf_rtl_program, time in T. rewrite ! compose_print_identity in T. simpl in T.
(* Goal: match_prog p tp *)
  set (p7 := total_if optim_tailcalls Tailcall.transf_program p6) in *.
(* Goal: match_prog p tp *)
  destruct (Inlining.transf_program p7) as [p8|e] eqn:P8; simpl in T; try discriminate.
(* Goal: match_prog p tp *)
  set (p9 := Renumber.transf_program p8) in *.
(* Goal: match_prog p tp *)
  set (p10 := total_if optim_constprop Constprop.transf_program p9) in *.
(* Goal: match_prog p tp *)
  set (p11 := total_if optim_constprop Renumber.transf_program p10) in *.
(* Goal: match_prog p tp *)
  destruct (partial_if optim_CSE CSE.transf_program p11) as [p12|e] eqn:P12; simpl in T; try discriminate.
(* Goal: match_prog p tp *)
  destruct (partial_if optim_redundancy Deadcode.transf_program p12) as [p13|e] eqn:P13; simpl in T; try discriminate.
(* Goal: match_prog p tp *)
  destruct (Unusedglob.transform_program p13) as [p14|e] eqn:P14; simpl in T; try discriminate.
(* Goal: match_prog p tp *)
  destruct (Allocation.transf_program p14) as [p15|e] eqn:P15; simpl in T; try discriminate.
(* Goal: match_prog p tp *)
  set (p16 := Tunneling.tunnel_program p15) in *.
(* Goal: match_prog p tp *)
  destruct (Linearize.transf_program p16) as [p17|e] eqn:P17; simpl in T; try discriminate.
(* Goal: match_prog p tp *)
  set (p18 := CleanupLabels.transf_program p17) in *.
(* Goal: match_prog p tp *)
  destruct (partial_if debug Debugvar.transf_program p18) as [p19|e] eqn:P19; simpl in T; try discriminate.
(* Goal: match_prog p tp *)
  destruct (Stacking.transf_program p19) as [p20|e] eqn:P20; simpl in T; try discriminate.
(* Goal: match_prog p tp *)
  unfold match_prog; simpl.
(* Goal: @eq bool (Globalenvs.Senv.public_symbol (symbolenv sem) id) (Globalenvs.Senv.public_symbol (symbolenv sem) id) *)
  exists p1; split. apply SimplExprproof.transf_program_match; auto.
(* Goal: @eq bool (Globalenvs.Senv.public_symbol (symbolenv sem) id) (Globalenvs.Senv.public_symbol (symbolenv sem) id) *)
  exists p2; split. apply SimplLocalsproof.match_transf_program; auto.
(* Goal: @eq bool (Globalenvs.Senv.public_symbol (symbolenv sem) id) (Globalenvs.Senv.public_symbol (symbolenv sem) id) *)
  exists p3; split. apply Cshmgenproof.transf_program_match; auto.
(* Goal: @eq bool (Globalenvs.Senv.public_symbol (symbolenv sem) id) (Globalenvs.Senv.public_symbol (symbolenv sem) id) *)
  exists p4; split. apply Cminorgenproof.transf_program_match; auto.
(* Goal: @eq bool (Globalenvs.Senv.public_symbol (symbolenv sem) id) (Globalenvs.Senv.public_symbol (symbolenv sem) id) *)
  exists p5; split. apply Selectionproof.transf_program_match; auto.
(* Goal: @eq bool (Globalenvs.Senv.public_symbol (symbolenv sem) id) (Globalenvs.Senv.public_symbol (symbolenv sem) id) *)
  exists p6; split. apply RTLgenproof.transf_program_match; auto.
(* Goal: @ex RTL.program (fun p2 : RTL.program => and (@match_if RTL.program optim_tailcalls Tailcallproof.match_prog p6 p2) (@ex RTL.program (fun p3 : RTL.program => and (Inliningproof.match_prog p2 p3) (@ex RTL.program (fun p4 : RTL.program => and (Renumberproof.match_prog p3 p4) (@ex RTL.program (fun p5 : RTL.program => and (@match_if RTL.program optim_constprop Constpropproof.match_prog p4 p5) (@ex RTL.program (fun p6 : RTL.program => and (@match_if RTL.program optim_constprop Renumberproof.match_prog p5 p6) (@ex RTL.program (fun p7 : RTL.program => and (@match_if RTL.program optim_CSE CSEproof.match_prog p6 p7) (@ex RTL.program (fun p8 : RTL.program => and (@match_if RTL.program optim_redundancy Deadcodeproof.match_prog p7 p8) (@ex RTL.program (fun p9 : RTL.program => and (Unusedglobproof.match_prog p8 p9) (@ex LTL.program (fun p10 : LTL.program => and (Allocproof.match_prog p9 p10) (@ex LTL.program (fun p11 : LTL.program => and (Tunnelingproof.match_prog p10 p11) (@ex Linear.program (fun p12 : Linear.program => and (Linearizeproof.match_prog p11 p12) (@ex Linear.program (fun p13 : Linear.program => and (CleanupLabelsproof.match_prog p12 p13) (@ex Linear.program (fun p14 : Linear.program => and (@match_if Linear.program debug Debugvarproof.match_prog p13 p14) (@ex Mach.program (fun p15 : Mach.program => and (Stackingproof.match_prog p14 p15) (@ex Asm.program (fun p16 : Asm.program => and (Asmgenproof.match_prog p15 p16) (@eq Asm.program p16 tp)))))))))))))))))))))))))))))) *)
  exists p7; split. apply total_if_match. apply Tailcallproof.transf_program_match.
(* Goal: @eq bool (Globalenvs.Senv.public_symbol (symbolenv sem) id) (Globalenvs.Senv.public_symbol (symbolenv sem) id) *)
  exists p8; split. apply Inliningproof.transf_program_match; auto.
(* Goal: @eq bool (Globalenvs.Senv.public_symbol (symbolenv sem) id) (Globalenvs.Senv.public_symbol (symbolenv sem) id) *)
  exists p9; split. apply Renumberproof.transf_program_match; auto.
(* Goal: @match_if RTL.program optim_constprop Renumberproof.match_prog p10 p11 *)
(* Goal: @ex RTL.program (fun p2 : RTL.program => and (@match_if RTL.program optim_CSE CSEproof.match_prog p11 p2) (@ex RTL.program (fun p3 : RTL.program => and (@match_if RTL.program optim_redundancy Deadcodeproof.match_prog p2 p3) (@ex RTL.program (fun p4 : RTL.program => and (Unusedglobproof.match_prog p3 p4) (@ex LTL.program (fun p5 : LTL.program => and (Allocproof.match_prog p4 p5) (@ex LTL.program (fun p6 : LTL.program => and (Tunnelingproof.match_prog p5 p6) (@ex Linear.program (fun p7 : Linear.program => and (Linearizeproof.match_prog p6 p7) (@ex Linear.program (fun p8 : Linear.program => and (CleanupLabelsproof.match_prog p7 p8) (@ex Linear.program (fun p9 : Linear.program => and (@match_if Linear.program debug Debugvarproof.match_prog p8 p9) (@ex Mach.program (fun p10 : Mach.program => and (Stackingproof.match_prog p9 p10) (@ex Asm.program (fun p11 : Asm.program => and (Asmgenproof.match_prog p10 p11) (@eq Asm.program p11 tp)))))))))))))))))))) *)
  exists p10; split. apply total_if_match. apply Constpropproof.transf_program_match.
(* Goal: @match_if RTL.program optim_constprop Renumberproof.match_prog p10 p11 *)
(* Goal: @ex RTL.program (fun p2 : RTL.program => and (@match_if RTL.program optim_CSE CSEproof.match_prog p11 p2) (@ex RTL.program (fun p3 : RTL.program => and (@match_if RTL.program optim_redundancy Deadcodeproof.match_prog p2 p3) (@ex RTL.program (fun p4 : RTL.program => and (Unusedglobproof.match_prog p3 p4) (@ex LTL.program (fun p5 : LTL.program => and (Allocproof.match_prog p4 p5) (@ex LTL.program (fun p6 : LTL.program => and (Tunnelingproof.match_prog p5 p6) (@ex Linear.program (fun p7 : Linear.program => and (Linearizeproof.match_prog p6 p7) (@ex Linear.program (fun p8 : Linear.program => and (CleanupLabelsproof.match_prog p7 p8) (@ex Linear.program (fun p9 : Linear.program => and (@match_if Linear.program debug Debugvarproof.match_prog p8 p9) (@ex Mach.program (fun p10 : Mach.program => and (Stackingproof.match_prog p9 p10) (@ex Asm.program (fun p11 : Asm.program => and (Asmgenproof.match_prog p10 p11) (@eq Asm.program p11 tp)))))))))))))))))))) *)
  exists p11; split. apply total_if_match. apply Renumberproof.transf_program_match.
(* Goal: @eq bool (Globalenvs.Senv.public_symbol (symbolenv sem) id) (Globalenvs.Senv.public_symbol (symbolenv sem) id) *)
  exists p12; split. eapply partial_if_match; eauto. apply CSEproof.transf_program_match.
(* Goal: @eq bool (Globalenvs.Senv.public_symbol (symbolenv sem) id) (Globalenvs.Senv.public_symbol (symbolenv sem) id) *)
  exists p13; split. eapply partial_if_match; eauto. apply Deadcodeproof.transf_program_match.
(* Goal: @eq bool (Globalenvs.Senv.public_symbol (symbolenv sem) id) (Globalenvs.Senv.public_symbol (symbolenv sem) id) *)
  exists p14; split. apply Unusedglobproof.transf_program_match; auto.
(* Goal: @eq bool (Globalenvs.Senv.public_symbol (symbolenv sem) id) (Globalenvs.Senv.public_symbol (symbolenv sem) id) *)
  exists p15; split. apply Allocproof.transf_program_match; auto.
(* Goal: @ex LTL.program (fun p2 : LTL.program => and (Tunnelingproof.match_prog p15 p2) (@ex Linear.program (fun p3 : Linear.program => and (Linearizeproof.match_prog p2 p3) (@ex Linear.program (fun p4 : Linear.program => and (CleanupLabelsproof.match_prog p3 p4) (@ex Linear.program (fun p5 : Linear.program => and (@match_if Linear.program debug Debugvarproof.match_prog p4 p5) (@ex Mach.program (fun p6 : Mach.program => and (Stackingproof.match_prog p5 p6) (@ex Asm.program (fun p7 : Asm.program => and (Asmgenproof.match_prog p6 p7) (@eq Asm.program p7 tp)))))))))))) *)
  exists p16; split. apply Tunnelingproof.transf_program_match.
(* Goal: @eq bool (Globalenvs.Senv.public_symbol (symbolenv sem) id) (Globalenvs.Senv.public_symbol (symbolenv sem) id) *)
  exists p17; split. apply Linearizeproof.transf_program_match; auto.
(* Goal: @eq bool (Globalenvs.Senv.public_symbol (symbolenv sem) id) (Globalenvs.Senv.public_symbol (symbolenv sem) id) *)
  exists p18; split. apply CleanupLabelsproof.transf_program_match; auto.
(* Goal: @eq bool (Globalenvs.Senv.public_symbol (symbolenv sem) id) (Globalenvs.Senv.public_symbol (symbolenv sem) id) *)
  exists p19; split. eapply partial_if_match; eauto. apply Debugvarproof.transf_program_match.
(* Goal: @eq bool (Globalenvs.Senv.public_symbol (symbolenv sem) id) (Globalenvs.Senv.public_symbol (symbolenv sem) id) *)
  exists p20; split. apply Stackingproof.transf_program_match; auto.
(* Goal: @eq bool (Globalenvs.Senv.public_symbol (symbolenv sem) id) (Globalenvs.Senv.public_symbol (symbolenv sem) id) *)
  exists tp; split. apply Asmgenproof.transf_program_match; auto.
(* Goal: @eq Asm.program tp tp *)
  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.
(* Goal: forall (p : Csyntax.program) (tp : Asm.program) (_ : @eq (res Asm.program) (transf_c_program p) (@OK Asm.program tp)), backward_simulation (Csem.semantics p) (Asm.semantics tp) *)
  intros. apply forward_simulation_step with (fun s1 s2 => s2 = s1); intros.
(* Goal: @eq bool (Globalenvs.Senv.public_symbol (symbolenv sem) id) (Globalenvs.Senv.public_symbol (symbolenv sem) id) *)
- auto.
(* Goal: @eq bool (Globalenvs.Senv.public_symbol (symbolenv sem) id) (Globalenvs.Senv.public_symbol (symbolenv sem) id) *)
- exists s1; auto.
(* Goal: @eq bool (Globalenvs.Senv.public_symbol (symbolenv sem) id) (Globalenvs.Senv.public_symbol (symbolenv sem) id) *)
- subst s2; auto.
(* Goal: @eq bool (Globalenvs.Senv.public_symbol (symbolenv sem) id) (Globalenvs.Senv.public_symbol (symbolenv sem) id) *)
- 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.
(* Goal: forall (p : Csyntax.program) (tp : Asm.program) (_ : @eq (res Asm.program) (transf_c_program p) (@OK Asm.program tp)), backward_simulation (Csem.semantics p) (Asm.semantics tp) *)
  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 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.
  }
(* Goal: @eq bool (Globalenvs.Senv.public_symbol (symbolenv sem) id) (Globalenvs.Senv.public_symbol (symbolenv sem) id) *)
  split. auto.
  apply forward_to_backward_simulation.
(* Goal: @eq bool (Globalenvs.Senv.public_symbol (symbolenv sem) id) (Globalenvs.Senv.public_symbol (symbolenv sem) id) *)
  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.
(* Goal: forall (p : Csyntax.program) (tp : Asm.program) (_ : @eq (res Asm.program) (transf_c_program p) (@OK Asm.program tp)), backward_simulation (Csem.semantics p) (Asm.semantics tp) *)
  intros.
(* Goal: backward_simulation (Csem.semantics p) (Asm.semantics tp) *)
  apply compose_backward_simulation with (atomic (Cstrategy.semantics p)).
  eapply sd_traces; eapply Asm.semantics_determinate.
(* Goal: backward_simulation (Csem.semantics p) (atomic (Cstrategy.semantics p)) *)
(* Goal: backward_simulation (atomic (Cstrategy.semantics p)) (Asm.semantics tp) *)
  apply factor_backward_simulation.
(* Goal: backward_simulation (Csem.semantics p) (Cstrategy.semantics p) *)
(* Goal: single_events (Csem.semantics p) *)
(* Goal: well_behaved_traces (Cstrategy.semantics p) *)
(* Goal: backward_simulation (atomic (Cstrategy.semantics p)) (Asm.semantics tp) *)
  apply Cstrategy.strategy_simulation.
(* Goal: single_events (Csem.semantics p) *)
(* Goal: well_behaved_traces (Cstrategy.semantics p) *)
(* Goal: backward_simulation (atomic (Cstrategy.semantics p)) (Asm.semantics tp) *)
  apply Csem.semantics_single_events.
  eapply ssr_well_behaved; eapply Cstrategy.semantics_strongly_receptive.
(* Goal: backward_simulation (atomic (Cstrategy.semantics p)) (Asm.semantics tp) *)
  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.
(* Goal: forall (p : Csyntax.program) (tp : Asm.program) (_ : @eq (res Asm.program) (transf_c_program p) (@OK Asm.program tp)), backward_simulation (Csem.semantics p) (Asm.semantics tp) *)
  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.
(* Goal: forall (p : Csyntax.program) (tp : Asm.program) (_ : @eq (res Asm.program) (transf_c_program p) (@OK Asm.program tp)), backward_simulation (Csem.semantics p) (Asm.semantics tp) *)
  intros.
  assert (nlist_forall2 match_prog c_units asm_units).
(* Goal: forall (p : Csyntax.program) (tp : Asm.program) (_ : @eq (res Asm.program) (transf_c_program p) (@OK Asm.program tp)), backward_simulation (Csem.semantics p) (Asm.semantics tp) *)
  { 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).
(* Goal: @eq bool (Globalenvs.Senv.public_symbol (symbolenv sem) id) (Globalenvs.Senv.public_symbol (symbolenv sem) id) *)
  { eapply link_list_compose_passes; eauto. }
  destruct H2 as (asm_program & P & Q).
(* Goal: @eq bool (Globalenvs.Senv.public_symbol (symbolenv sem) id) (Globalenvs.Senv.public_symbol (symbolenv sem) id) *)
  exists asm_program; split; auto. apply c_semantic_preservation; auto.
Qed.
