From 9cc12b684ee6833971c9549aa76cc683ba931090 Mon Sep 17 00:00:00 2001 From: David Monniaux Date: Tue, 21 Apr 2020 22:08:07 +0200 Subject: begin scripting the Compiler.v file --- Makefile | 5 + backend/Unusedglob.v | 2 +- backend/Unusedglobproof.v | 4 +- driver/Compiler.v | 568 ---------------------------------------------- driver/Compiler.vexpand | 533 +++++++++++++++++++++++++++++++++++++++++++ tools/compiler_expand.ml | 62 +++++ 6 files changed, 603 insertions(+), 571 deletions(-) delete mode 100644 driver/Compiler.v create mode 100644 driver/Compiler.vexpand create mode 100644 tools/compiler_expand.ml diff --git a/Makefile b/Makefile index a69f7e2e..2f9ab029 100644 --- a/Makefile +++ b/Makefile @@ -201,6 +201,8 @@ tools/ndfun: tools/ndfun.ml ocamlopt -o tools/ndfun str.cmxa tools/ndfun.ml tools/modorder: tools/modorder.ml ocamlopt -o tools/modorder str.cmxa tools/modorder.ml +tools/compiler_expand: tools/compiler_expand.ml + ocamlopt -o $@ $+ latexdoc: cd doc; $(COQDOC) --latex -o doc/doc.tex -g $(FILES) @@ -216,6 +218,9 @@ latexdoc: @tools/ndfun $*.vp > $*.v || { rm -f $*.v; exit 2; } @chmod a-w $*.v +driver/Compiler.v: driver/Compiler.vexpand tools/compiler_expand + tools/compiler_expand driver/Compiler.vexpand $@ + compcert.ini: Makefile.config (echo "stdlib_path=$(LIBDIR)"; \ echo "prepro=$(CPREPRO)"; \ diff --git a/backend/Unusedglob.v b/backend/Unusedglob.v index 93ca7af4..3b8e19ad 100644 --- a/backend/Unusedglob.v +++ b/backend/Unusedglob.v @@ -126,7 +126,7 @@ Fixpoint filter_globdefs (used: IS.t) (accu defs: list (ident * globdef fundef u Definition global_defined (p: program) (pm: prog_map) (id: ident) : bool := match pm!id with Some _ => true | None => ident_eq id (prog_main p) end. -Definition transform_program (p: program) : res program := +Definition transf_program (p: program) : res program := let pm := prog_defmap p in match used_globals p pm with | None => Error (msg "Unusedglob: analysis failed") diff --git a/backend/Unusedglobproof.v b/backend/Unusedglobproof.v index fa120b6d..160c0b18 100644 --- a/backend/Unusedglobproof.v +++ b/backend/Unusedglobproof.v @@ -428,9 +428,9 @@ Qed. End TRANSFORMATION. Theorem transf_program_match: - forall p tp, transform_program p = OK tp -> match_prog p tp. + forall p tp, transf_program p = OK tp -> match_prog p tp. Proof. - unfold transform_program; intros p tp TR. set (pm := prog_defmap p) in *. + unfold transf_program; intros p tp TR. set (pm := prog_defmap p) in *. destruct (used_globals p pm) as [u|] eqn:U; try discriminate. destruct (IS.for_all (global_defined p pm) u) eqn:DEF; inv TR. exists u; split. diff --git a/driver/Compiler.v b/driver/Compiler.v deleted file mode 100644 index 69041ab0..00000000 --- a/driver/Compiler.v +++ /dev/null @@ -1,568 +0,0 @@ -(* *********************************************************************) -(* *) -(* 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 Profiling. -Require ProfilingExploit. -Require FirstNop. -Require Renumber. -Require Duplicate. -Require Constprop. -Require LICM. -Require CSE. -Require ForwardMoves. -Require CSE2. -Require CSE3. -Require Deadcode. -Require Unusedglob. -Require Allnontrap. -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 Profilingproof. -Require ProfilingExploitproof. -Require FirstNopproof. -Require Renumberproof. -Require Duplicateproof. -Require Constpropproof. -Require LICMproof. -Require CSEproof. -Require ForwardMovesproof. -Require CSE2proof. -Require CSE3proof. -Require Deadcodeproof. -Require Unusedglobproof. -Require Allnontrapproof. -Require Allocproof. -Require Tunnelingproof. -Require Linearizeproof. -Require CleanupLabelsproof. -Require Debugvarproof. -Require Stackingproof. -Require Import 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) - @@ total_if Compopts.profile_arcs (time "Profiling insertion" Profiling.transf_program) - @@ print (print_RTL 3) - @@ total_if Compopts.branch_probabilities (time "Profiling use" ProfilingExploit.transf_program) - @@ print (print_RTL 4) - @@ total_if Compopts.optim_move_loop_invariants (time "Inserting initial nop" FirstNop.transf_program) - @@ print (print_RTL 5) - @@ time "Renumbering" Renumber.transf_program - @@ print (print_RTL 6) - @@@ partial_if Compopts.optim_duplicate (time "Tail-duplicating" Duplicate.transf_program) - @@ print (print_RTL 7) - @@ time "Renumbering pre constprop" Renumber.transf_program - @@ print (print_RTL 8) - @@ total_if Compopts.optim_constprop (time "Constant propagation" Constprop.transf_program) - @@ print (print_RTL 9) - @@@ partial_if Compopts.optim_move_loop_invariants (time "LICM" LICM.transf_program) - @@ print (print_RTL 10) - @@ total_if Compopts.optim_move_loop_invariants (time "Renumbering pre CSE" Renumber.transf_program) - @@ print (print_RTL 11) - @@@ partial_if Compopts.optim_CSE (time "CSE" CSE.transf_program) - @@ print (print_RTL 12) - @@ total_if Compopts.optim_CSE2 (time "CSE2" CSE2.transf_program) - @@ print (print_RTL 13) - @@@ partial_if Compopts.optim_CSE3 (time "CSE3" CSE3.transf_program) - @@ print (print_RTL 14) - @@ total_if Compopts.optim_forward_moves ForwardMoves.transf_program - @@ print (print_RTL 15) - @@@ partial_if Compopts.optim_redundancy (time "Redundancy elimination" Deadcode.transf_program) - @@ print (print_RTL 16) - @@ total_if Compopts.all_loads_nontrap Allnontrap.transf_program - @@ print (print_RTL 17) - @@@ time "Unused globals" Unusedglob.transform_program - @@ print (print_RTL 18) - @@@ 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 "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. - -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 (match_if Compopts.profile_arcs Profilingproof.match_prog) - ::: mkpass (match_if Compopts.branch_probabilities ProfilingExploitproof.match_prog) - ::: mkpass (match_if Compopts.optim_move_loop_invariants FirstNopproof.match_prog) - ::: mkpass Renumberproof.match_prog - ::: mkpass (match_if Compopts.optim_duplicate Duplicateproof.match_prog) - ::: mkpass Renumberproof.match_prog - ::: mkpass (match_if Compopts.optim_constprop Constpropproof.match_prog) - ::: mkpass (match_if Compopts.optim_move_loop_invariants LICMproof.match_prog) - ::: mkpass (match_if Compopts.optim_move_loop_invariants 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_forward_moves ForwardMovesproof.match_prog) - ::: mkpass (match_if Compopts.optim_redundancy Deadcodeproof.match_prog) - ::: mkpass (match_if Compopts.all_loads_nontrap Allnontrapproof.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 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 (p8bis := total_if profile_arcs Profiling.transf_program p8) in *. - set (p8ter := total_if branch_probabilities ProfilingExploit.transf_program p8bis) in *. - set (p9 := total_if Compopts.optim_move_loop_invariants FirstNop.transf_program p8ter) in *. - set (p9bis := Renumber.transf_program p9) in *. - destruct (partial_if optim_duplicate Duplicate.transf_program p9bis) as [p10|e] eqn:P10; simpl in T; try discriminate. - set (p11 := Renumber.transf_program p10) in *. - set (p12 := total_if optim_constprop Constprop.transf_program p11) in *. - destruct (partial_if optim_move_loop_invariants LICM.transf_program p12) as [p12bis|e] eqn:P12bis; simpl in T; try discriminate. - set (p12ter :=(total_if optim_move_loop_invariants Renumber.transf_program p12bis)) in *. - destruct (partial_if optim_CSE CSE.transf_program p12ter) as [p13|e] eqn:P13; simpl in T; try discriminate. - set (p13bis := total_if optim_CSE2 CSE2.transf_program p13) in *. - destruct (partial_if optim_CSE3 CSE3.transf_program p13bis) as [p13ter|e] eqn:P13ter; simpl in T; try discriminate. - set (p13quater := total_if optim_forward_moves ForwardMoves.transf_program p13ter) in *. - destruct (partial_if optim_redundancy Deadcode.transf_program p13quater) as [p14|e] eqn:P14; simpl in T; try discriminate. - set (p14bis := total_if all_loads_nontrap Allnontrap.transf_program p14) in *. - destruct (Unusedglob.transform_program p14bis) as [p15|e] eqn:P15; simpl in T; try discriminate. - destruct (Allocation.transf_program p15) as [p16|e] eqn:P16; simpl in T; try discriminate. - set (p17 := Tunneling.tunnel_program p16) in *. - destruct (Linearize.transf_program p17) as [p18|e] eqn:P18; simpl in T; try discriminate. - set (p19 := CleanupLabels.transf_program p18) in *. - destruct (partial_if debug Debugvar.transf_program p19) as [p20|e] eqn:P20; simpl in T; try discriminate. - destruct (Stacking.transf_program p20) as [p21|e] eqn:P21; 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 p8bis; split. apply total_if_match. apply Profilingproof.transf_program_match; auto. - exists p8ter; split. apply total_if_match. apply ProfilingExploitproof.transf_program_match; auto. - exists p9; split. apply total_if_match. apply FirstNopproof.transf_program_match. - exists p9bis; split. apply Renumberproof.transf_program_match. - exists p10; split. eapply partial_if_match; eauto. apply Duplicateproof.transf_program_match; auto. - exists p11; split. apply Renumberproof.transf_program_match. - exists p12; split. apply total_if_match. apply Constpropproof.transf_program_match. - exists p12bis; split. eapply partial_if_match; eauto. apply LICMproof.transf_program_match. - exists p12ter; split. apply total_if_match; eauto. apply Renumberproof.transf_program_match. - exists p13; split. eapply partial_if_match; eauto. apply CSEproof.transf_program_match. - exists p13bis; split. apply total_if_match. apply CSE2proof.transf_program_match. - exists p13ter; split. eapply partial_if_match; eauto. apply CSE3proof.transf_program_match. - exists p13quater; split. eapply total_if_match; eauto. apply ForwardMovesproof.transf_program_match. - exists p14; split. eapply partial_if_match; eauto. apply Deadcodeproof.transf_program_match. - exists p14bis; split. eapply total_if_match; eauto. apply Allnontrapproof.transf_program_match. - exists p15; split. apply Unusedglobproof.transf_program_match; auto. - exists p16; split. apply Allocproof.transf_program_match; auto. - exists p17; split. apply Tunnelingproof.transf_program_match. - exists p18; split. apply Linearizeproof.transf_program_match; auto. - exists p19; split. apply CleanupLabelsproof.transf_program_match; auto. - exists p20; split. eapply partial_if_match; eauto. apply Debugvarproof.transf_program_match. - exists p21; 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. - 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 p31)). - { - 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 match_if_simulation. eassumption. exact Profilingproof.transf_program_correct. - eapply compose_forward_simulations. - eapply match_if_simulation. eassumption. exact ProfilingExploitproof.transf_program_correct. - eapply compose_forward_simulations. - eapply match_if_simulation. eassumption. exact FirstNopproof.transf_program_correct. - eapply compose_forward_simulations. eapply Renumberproof.transf_program_correct; eassumption. - eapply compose_forward_simulations. - eapply match_if_simulation. eassumption. exact Duplicateproof.transf_program_correct. - eapply compose_forward_simulations. - eapply compose_forward_simulations. eapply Renumberproof.transf_program_correct; eassumption. - eapply match_if_simulation. eassumption. exact Constpropproof.transf_program_correct. - eapply compose_forward_simulations. - eapply match_if_simulation. eassumption. exact LICMproof.transf_program_correct; eassumption. - 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 CSE2proof.transf_program_correct. - eapply compose_forward_simulations. - eapply match_if_simulation. eassumption. exact CSE3proof.transf_program_correct. - eapply compose_forward_simulations. - eapply match_if_simulation. eassumption. exact ForwardMovesproof.transf_program_correct; eassumption. - eapply compose_forward_simulations. - eapply match_if_simulation. eassumption. exact Deadcodeproof.transf_program_correct; eassumption. - eapply compose_forward_simulations. - eapply match_if_simulation. eassumption. exact Allnontrapproof.transf_program_correct. - 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. - 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. diff --git a/driver/Compiler.vexpand b/driver/Compiler.vexpand new file mode 100644 index 00000000..4c7c963a --- /dev/null +++ b/driver/Compiler.vexpand @@ -0,0 +1,533 @@ +(* *********************************************************************) +(* *) +(* 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 Profiling. +Require ProfilingExploit. +Require FirstNop. +Require Renumber. +Require Duplicate. +Require Constprop. +Require LICM. +Require CSE. +Require ForwardMoves. +Require CSE2. +Require CSE3. +Require Deadcode. +Require Unusedglob. +Require Allnontrap. +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 Profilingproof. +Require ProfilingExploitproof. +Require FirstNopproof. +Require Renumberproof. +Require Duplicateproof. +Require Constpropproof. +Require LICMproof. +Require CSEproof. +Require ForwardMovesproof. +Require CSE2proof. +Require CSE3proof. +Require Deadcodeproof. +Require Unusedglobproof. +Require Allnontrapproof. +Require Allocproof. +Require Tunnelingproof. +Require Linearizeproof. +Require CleanupLabelsproof. +Require Debugvarproof. +Require Stackingproof. +Require Import 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) +EXPAND_TRANSF_PROGRAM + @@@ 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 "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. + +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 (match_if Compopts.profile_arcs Profilingproof.match_prog) + ::: mkpass (match_if Compopts.branch_probabilities ProfilingExploitproof.match_prog) + ::: mkpass (match_if Compopts.optim_move_loop_invariants FirstNopproof.match_prog) + ::: mkpass Renumberproof.match_prog + ::: mkpass (match_if Compopts.optim_duplicate Duplicateproof.match_prog) + ::: mkpass Renumberproof.match_prog + ::: mkpass (match_if Compopts.optim_constprop Constpropproof.match_prog) + ::: mkpass (match_if Compopts.optim_move_loop_invariants LICMproof.match_prog) + ::: mkpass (match_if Compopts.optim_move_loop_invariants 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_forward_moves ForwardMovesproof.match_prog) + ::: mkpass (match_if Compopts.optim_redundancy Deadcodeproof.match_prog) + ::: mkpass (match_if Compopts.all_loads_nontrap Allnontrapproof.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 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 (p8bis := total_if profile_arcs Profiling.transf_program p8) in *. + set (p8ter := total_if branch_probabilities ProfilingExploit.transf_program p8bis) in *. + set (p9 := total_if Compopts.optim_move_loop_invariants FirstNop.transf_program p8ter) in *. + set (p9bis := Renumber.transf_program p9) in *. + destruct (partial_if optim_duplicate Duplicate.transf_program p9bis) as [p10|e] eqn:P10; simpl in T; try discriminate. + set (p11 := Renumber.transf_program p10) in *. + set (p12 := total_if optim_constprop Constprop.transf_program p11) in *. + destruct (partial_if optim_move_loop_invariants LICM.transf_program p12) as [p12bis|e] eqn:P12bis; simpl in T; try discriminate. + set (p12ter :=(total_if optim_move_loop_invariants Renumber.transf_program p12bis)) in *. + destruct (partial_if optim_CSE CSE.transf_program p12ter) as [p13|e] eqn:P13; simpl in T; try discriminate. + set (p13bis := total_if optim_CSE2 CSE2.transf_program p13) in *. + destruct (partial_if optim_CSE3 CSE3.transf_program p13bis) as [p13ter|e] eqn:P13ter; simpl in T; try discriminate. + set (p13quater := total_if optim_forward_moves ForwardMoves.transf_program p13ter) in *. + destruct (partial_if optim_redundancy Deadcode.transf_program p13quater) as [p14|e] eqn:P14; simpl in T; try discriminate. + set (p14bis := total_if all_loads_nontrap Allnontrap.transf_program p14) in *. + destruct (Unusedglob.transform_program p14bis) as [p15|e] eqn:P15; simpl in T; try discriminate. + destruct (Allocation.transf_program p15) as [p16|e] eqn:P16; simpl in T; try discriminate. + set (p17 := Tunneling.tunnel_program p16) in *. + destruct (Linearize.transf_program p17) as [p18|e] eqn:P18; simpl in T; try discriminate. + set (p19 := CleanupLabels.transf_program p18) in *. + destruct (partial_if debug Debugvar.transf_program p19) as [p20|e] eqn:P20; simpl in T; try discriminate. + destruct (Stacking.transf_program p20) as [p21|e] eqn:P21; 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 p8bis; split. apply total_if_match. apply Profilingproof.transf_program_match; auto. + exists p8ter; split. apply total_if_match. apply ProfilingExploitproof.transf_program_match; auto. + exists p9; split. apply total_if_match. apply FirstNopproof.transf_program_match. + exists p9bis; split. apply Renumberproof.transf_program_match. + exists p10; split. eapply partial_if_match; eauto. apply Duplicateproof.transf_program_match; auto. + exists p11; split. apply Renumberproof.transf_program_match. + exists p12; split. apply total_if_match. apply Constpropproof.transf_program_match. + exists p12bis; split. eapply partial_if_match; eauto. apply LICMproof.transf_program_match. + exists p12ter; split. apply total_if_match; eauto. apply Renumberproof.transf_program_match. + exists p13; split. eapply partial_if_match; eauto. apply CSEproof.transf_program_match. + exists p13bis; split. apply total_if_match. apply CSE2proof.transf_program_match. + exists p13ter; split. eapply partial_if_match; eauto. apply CSE3proof.transf_program_match. + exists p13quater; split. eapply total_if_match; eauto. apply ForwardMovesproof.transf_program_match. + exists p14; split. eapply partial_if_match; eauto. apply Deadcodeproof.transf_program_match. + exists p14bis; split. eapply total_if_match; eauto. apply Allnontrapproof.transf_program_match. + exists p15; split. apply Unusedglobproof.transf_program_match; auto. + exists p16; split. apply Allocproof.transf_program_match; auto. + exists p17; split. apply Tunnelingproof.transf_program_match. + exists p18; split. apply Linearizeproof.transf_program_match; auto. + exists p19; split. apply CleanupLabelsproof.transf_program_match; auto. + exists p20; split. eapply partial_if_match; eauto. apply Debugvarproof.transf_program_match. + exists p21; 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. + 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 p31)). + { + 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 match_if_simulation. eassumption. exact Profilingproof.transf_program_correct. + eapply compose_forward_simulations. + eapply match_if_simulation. eassumption. exact ProfilingExploitproof.transf_program_correct. + eapply compose_forward_simulations. + eapply match_if_simulation. eassumption. exact FirstNopproof.transf_program_correct. + eapply compose_forward_simulations. eapply Renumberproof.transf_program_correct; eassumption. + eapply compose_forward_simulations. + eapply match_if_simulation. eassumption. exact Duplicateproof.transf_program_correct. + eapply compose_forward_simulations. + eapply compose_forward_simulations. eapply Renumberproof.transf_program_correct; eassumption. + eapply match_if_simulation. eassumption. exact Constpropproof.transf_program_correct. + eapply compose_forward_simulations. + eapply match_if_simulation. eassumption. exact LICMproof.transf_program_correct; eassumption. + 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 CSE2proof.transf_program_correct. + eapply compose_forward_simulations. + eapply match_if_simulation. eassumption. exact CSE3proof.transf_program_correct. + eapply compose_forward_simulations. + eapply match_if_simulation. eassumption. exact ForwardMovesproof.transf_program_correct; eassumption. + eapply compose_forward_simulations. + eapply match_if_simulation. eassumption. exact Deadcodeproof.transf_program_correct; eassumption. + eapply compose_forward_simulations. + eapply match_if_simulation. eassumption. exact Allnontrapproof.transf_program_correct. + 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. + 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. diff --git a/tools/compiler_expand.ml b/tools/compiler_expand.ml new file mode 100644 index 00000000..63808c1f --- /dev/null +++ b/tools/compiler_expand.ml @@ -0,0 +1,62 @@ +type is_partial = TOTAL | PARTIAL;; +type when_triggered = Always | Option of string;; + +let passes = +[| +TOTAL, (Option "optim_tailcalls"), (Some "Tail calls"), "Tailcall"; +PARTIAL, Always, (Some "Inlining"), "Inlining"; +TOTAL, (Option "profile_arcs"), (Some "Profiling insertion"), "Profiling"; +TOTAL, (Option "branch_probabilities"), (Some "Profiling use"), "ProfilingExploit"; +TOTAL, (Option "optim_move_loop_invariants"), (Some "Inserting initial nop"), "FirstNop"; +TOTAL, Always, (Some "Renumbering"), "Renumber"; +PARTIAL, (Option "optim_duplicate"), (Some "Tail-duplicating"), "Duplicate"; +TOTAL, Always, (Some "Renumbering pre constprop"), "Renumber"; +TOTAL, (Option "optim_constprop"), (Some "Constant propagation"), "Constprop"; +PARTIAL, (Option "optim_move_loop_invariants"), (Some "LICM"), "LICM"; +TOTAL, (Option "optim_move_loop_invariants"), (Some "Renumbering pre CSE"), "Renumber"; +PARTIAL, (Option "optim_CSE"), (Some "CSE"), "CSE"; +TOTAL, (Option "optim_CSE2"), (Some "CSE2"), "CSE2"; +PARTIAL, (Option "optim_CSE3"), (Some "CSE3"), "CSE3"; +TOTAL, (Option "optim_forward_moves"), (Some "Forwarding moves"), "ForwardMoves"; +PARTIAL, (Option "optim_redundancy"), (Some "Redundancy elimination"), "Deadcode"; +TOTAL, (Option "all_loads_nontrap"), None, "Allnontrap"; +PARTIAL, Always, (Some "Unused globals"), "Unusedglob" +|];; + +let totality = function TOTAL -> "total" | PARTIAL -> "partial";; + +let print_transf oc = + Array.iteri + (fun i (partial, trigger, time_label, pass_name) -> + output_string oc (match partial with + | TOTAL -> " @@ " + | PARTIAL -> " @@@ "); + (match trigger with + | Always -> () + | Option s -> + Printf.fprintf oc "%s_if Compopts.%s " (totality partial) s); + output_char oc '('; + (match time_label with + | None -> () + | Some s -> + Printf.fprintf oc "time \"%s\" " s); + Printf.fprintf oc "%s.transf_program)\n" pass_name; + Printf.fprintf oc " @@ print (print_RTL %d)\n" (succ i) + ) passes;; + +if (Array.length Sys.argv)<>3 +then exit 1;; + +let filename_in = Sys.argv.(1) and filename_out = Sys.argv.(2) in + let ic = open_in filename_in and oc = open_out filename_out in + try + while true + do + let line = input_line ic in + if line = "EXPAND_TRANSF_PROGRAM" + then print_transf oc + else (output_string oc line; + output_char oc '\n') + done + with End_of_file -> + (close_in ic; close_out oc);; -- cgit