From 0053b1aa1d26da5d1f995a603b127daf799c2da9 Mon Sep 17 00:00:00 2001 From: xleroy Date: Mon, 21 May 2012 16:26:30 +0000 Subject: Merge of the newmem branch: - Revised memory model with Max and Cur permissions, but without bounds - Constant propagation of 'const' globals - Function inlining at RTL level - (Unprovable) elimination of unreferenced static definitions git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1899 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e --- driver/Clflags.ml | 3 +- driver/Compiler.v | 131 +++++++++++++++++++++++++++++------------------------- driver/Driver.ml | 11 +++-- driver/Interp.ml | 8 ++++ 4 files changed, 87 insertions(+), 66 deletions(-) (limited to 'driver') diff --git a/driver/Clflags.ml b/driver/Clflags.ml index 5003e3e..2be48de 100644 --- a/driver/Clflags.ml +++ b/driver/Clflags.ml @@ -23,13 +23,14 @@ let option_fbitfields = ref false let option_fvararg_calls = ref true let option_fpacked_structs = ref false let option_fsse = ref true +let option_ffloatconstprop = ref 2 let option_dparse = ref false let option_dcmedium = ref false let option_dclight = ref false let option_dcminor = ref false let option_drtl = ref false let option_dtailcall = ref false -let option_dcastopt = ref false +let option_dinlining = ref false let option_dconstprop = ref false let option_dcse = ref false let option_dalloc = ref false diff --git a/driver/Compiler.v b/driver/Compiler.v index be4f981..6fbfacd 100644 --- a/driver/Compiler.v +++ b/driver/Compiler.v @@ -44,6 +44,8 @@ Require Cminorgen. Require Selection. Require RTLgen. Require Tailcall. +Require Inlining. +Require Renumber. Require Constprop. Require CSE. Require Allocation. @@ -67,6 +69,8 @@ Require Cminorgenproof. Require Selectionproof. Require RTLgenproof. Require Tailcallproof. +Require Inliningproof. +Require Renumberproof. Require Constpropproof. Require CSEproof. Require Allocproof. @@ -88,12 +92,13 @@ Require Asmgenproof. (** Pretty-printers (defined in Caml). *) Parameter print_Clight: Clight.program -> unit. Parameter print_Cminor: Cminor.program -> unit. -Parameter print_RTL: RTL.fundef -> unit. -Parameter print_RTL_tailcall: RTL.fundef -> unit. -Parameter print_RTL_constprop: RTL.fundef -> unit. -Parameter print_RTL_cse: RTL.fundef -> unit. -Parameter print_LTLin: LTLin.fundef -> unit. -Parameter print_Mach: Mach.fundef -> unit. +Parameter print_RTL: RTL.program -> unit. +Parameter print_RTL_tailcall: RTL.program -> unit. +Parameter print_RTL_inline: RTL.program -> unit. +Parameter print_RTL_constprop: RTL.program -> unit. +Parameter print_RTL_cse: RTL.program -> unit. +Parameter print_LTLin: LTLin.program -> unit. +Parameter print_Mach: Mach.program -> unit. Open Local Scope string_scope. @@ -120,56 +125,38 @@ Definition print {A: Type} (printer: A -> unit) (prog: A) : A := (** 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. - - There are two ways to compose the compiler passes. The first - translates every function from the Cminor program from Cminor to - RTL, then to LTL, etc, all the way to Asm, and iterates this - transformation for every function. The second translates the whole - Cminor program to a RTL program, then to an LTL program, etc. - Between CminorSel and Asm, we follow the first approach because it has - lower memory requirements. The translation from Clight to Asm - follows the second approach. - - The translation of an RTL function to an Asm function is as follows. *) - -Definition transf_rtl_fundef (f: RTL.fundef) : res Asm.fundef := + pretty-printing and assembling. *) + +Definition transf_rtl_program (f: RTL.program) : res Asm.program := OK f @@ print print_RTL - @@ Tailcall.transf_fundef + @@ Tailcall.transf_program @@ print print_RTL_tailcall - @@ Constprop.transf_fundef + @@@ Inlining.transf_program + @@ Renumber.transf_program + @@ print print_RTL_inline + @@ Constprop.transf_program + @@ Renumber.transf_program @@ print print_RTL_constprop - @@@ CSE.transf_fundef + @@@ CSE.transf_program @@ print print_RTL_cse - @@@ Allocation.transf_fundef - @@ Tunneling.tunnel_fundef - @@@ Linearize.transf_fundef - @@ CleanupLabels.transf_fundef + @@@ Allocation.transf_program + @@ Tunneling.tunnel_program + @@@ Linearize.transf_program + @@ CleanupLabels.transf_program @@ print print_LTLin - @@ Reload.transf_fundef - @@ RRE.transf_fundef - @@@ Stacking.transf_fundef + @@ Reload.transf_program + @@ RRE.transf_program + @@@ Stacking.transf_program @@ print print_Mach - @@@ Asmgen.transf_fundef. - -(* Here is the translation of a CminorSel function to an Asm function. *) - -Definition transf_cminorsel_fundef (f: CminorSel.fundef) : res Asm.fundef := - OK f - @@@ RTLgen.transl_fundef - @@@ transf_rtl_fundef. - -(** The corresponding translations for whole program follow. *) - -Definition transf_rtl_program (p: RTL.program) : res Asm.program := - transform_partial_program transf_rtl_fundef p. + @@@ Asmgen.transf_program. Definition transf_cminor_program (p: Cminor.program) : res Asm.program := OK p @@ print print_Cminor @@ Selection.sel_program - @@@ transform_partial_program transf_cminorsel_fundef. + @@@ RTLgen.transl_program + @@@ transf_rtl_program. Definition transf_clight_program (p: Clight.program) : res Asm.program := OK p @@ -323,21 +310,40 @@ Theorem transf_rtl_program_correct: Proof. intros. assert (F: forward_simulation (RTL.semantics p) (Asm.semantics tp)). - unfold transf_rtl_program, transf_rtl_fundef in H. - repeat TransfProgInv. - repeat rewrite transform_program_print_identity in *. subst. - generalize (transform_partial_program_identity _ _ _ _ X). intro EQ. subst. - - generalize Alloctyping.program_typing_preserved - Tunnelingtyping.program_typing_preserved - Linearizetyping.program_typing_preserved - CleanupLabelstyping.program_typing_preserved - Reloadtyping.program_typing_preserved - RREtyping.program_typing_preserved - Stackingtyping.program_typing_preserved; intros. + unfold transf_rtl_program in H. + repeat rewrite compose_print_identity in H. + simpl in H. + set (p1 := Tailcall.transf_program p) in *. + destruct (Inlining.transf_program p1) as [p11|]_eqn; simpl in H; try discriminate. + set (p12 := Renumber.transf_program p11) in *. + set (p2 := Constprop.transf_program p12) in *. + set (p21 := Renumber.transf_program p2) in *. + destruct (CSE.transf_program p21) as [p3|]_eqn; simpl in H; try discriminate. + destruct (Allocation.transf_program p3) as [p4|]_eqn; simpl in H; try discriminate. + set (p5 := Tunneling.tunnel_program p4) in *. + destruct (Linearize.transf_program p5) as [p6|]_eqn; simpl in H; try discriminate. + set (p7 := CleanupLabels.transf_program p6) in *. + set (p8 := Reload.transf_program p7) in *. + set (p9 := RRE.transf_program p8) in *. + destruct (Stacking.transf_program p9) as [p10|]_eqn; simpl in H; try discriminate. + + assert(TY1: LTLtyping.wt_program p5). + eapply Tunnelingtyping.program_typing_preserved. + eapply Alloctyping.program_typing_preserved; eauto. + assert(TY2: LTLintyping.wt_program p7). + eapply CleanupLabelstyping.program_typing_preserved. + eapply Linearizetyping.program_typing_preserved; eauto. + assert(TY3: Lineartyping.wt_program p9). + eapply RREtyping.program_typing_preserved. + eapply Reloadtyping.program_typing_preserved; eauto. + assert(TY4: Machtyping.wt_program p10). + eapply Stackingtyping.program_typing_preserved; eauto. eapply compose_forward_simulation. apply Tailcallproof.transf_program_correct. + eapply compose_forward_simulation. apply Inliningproof.transf_program_correct. eassumption. + eapply compose_forward_simulation. apply Renumberproof.transf_program_correct. eapply compose_forward_simulation. apply Constpropproof.transf_program_correct. + eapply compose_forward_simulation. apply Renumberproof.transf_program_correct. eapply compose_forward_simulation. apply CSEproof.transf_program_correct. eassumption. eapply compose_forward_simulation. apply Allocproof.transf_program_correct. eassumption. eapply compose_forward_simulation. apply Tunnelingproof.transf_program_correct. @@ -345,8 +351,8 @@ Proof. eapply compose_forward_simulation. apply CleanupLabelsproof.transf_program_correct. eapply compose_forward_simulation. apply Reloadproof.transf_program_correct. eauto. eapply compose_forward_simulation. apply RREproof.transf_program_correct. eauto. - eapply compose_forward_simulation. apply Stackingproof.transf_program_correct. eassumption. eauto 8. - apply Asmgenproof.transf_program_correct; eauto 10. + eapply compose_forward_simulation. apply Stackingproof.transf_program_correct. eassumption. eauto. + apply Asmgenproof.transf_program_correct; eauto. split. auto. apply forward_to_backward_simulation. auto. apply RTL.semantics_receptive. @@ -361,11 +367,14 @@ Theorem transf_cminor_program_correct: Proof. intros. assert (F: forward_simulation (Cminor.semantics p) (Asm.semantics tp)). - unfold transf_cminor_program, transf_cminorsel_fundef in H. - simpl in H. repeat TransfProgInv. + unfold transf_cminor_program in H. + repeat rewrite compose_print_identity in H. + simpl in H. + set (p1 := Selection.sel_program p) in *. + destruct (RTLgen.transl_program p1) as [p2|]_eqn; simpl in H; try discriminate. eapply compose_forward_simulation. apply Selectionproof.transf_program_correct. eapply compose_forward_simulation. apply RTLgenproof.transf_program_correct. eassumption. - exact (fst (transf_rtl_program_correct _ _ P)). + exact (fst (transf_rtl_program_correct _ _ H)). split. auto. apply forward_to_backward_simulation. auto. diff --git a/driver/Driver.ml b/driver/Driver.ml index ff1046d..3d0cc16 100644 --- a/driver/Driver.ml +++ b/driver/Driver.ml @@ -134,7 +134,7 @@ let compile_c_ast sourcename csyntax ofile = set_dest PrintCminor.destination option_dcminor ".cm"; set_dest PrintRTL.destination_rtl option_drtl ".rtl"; set_dest PrintRTL.destination_tailcall option_dtailcall ".tailcall.rtl"; - set_dest PrintRTL.destination_castopt option_dcastopt ".castopt.rtl"; + set_dest PrintRTL.destination_inlining option_dinlining ".inlining.rtl"; set_dest PrintRTL.destination_constprop option_dconstprop ".constprop.rtl"; set_dest PrintRTL.destination_cse option_dcse ".cse.rtl"; set_dest PrintLTLin.destination option_dalloc ".alloc.ltl"; @@ -151,7 +151,7 @@ let compile_c_ast sourcename csyntax ofile = dump_asm asm (Filename.chop_suffix sourcename ".c" ^ ".sdump"); (* Print Asm in text form *) let oc = open_out ofile in - PrintAsm.print_program oc asm; + PrintAsm.print_program oc (Unusedglob.transf_program asm); close_out oc (* From C source to asm *) @@ -371,6 +371,8 @@ Code generation options: (use -fno- to turn off -f) : -fsse (IA32) Use SSE2 instructions for some integer operations [on] -fsmall-data Set maximal size for allocation in small data area -fsmall-const Set maximal size for allocation in small constant area + -ffloat-const-prop Control constant propagation of floats + (=0: none, =1: limited, =2: full; default is full) -Wa, Pass option to the assembler Tracing options: -dparse Save C file after parsing and elaboration in .parse.c @@ -379,7 +381,7 @@ Tracing options: -dcminor Save generated Cminor in .cm -drtl Save unoptimized generated RTL in .rtl -dtailcall Save RTL after tail call optimization in .tailcall.rtl - -dcastopt Save RTL after cast optimization in .castopt.rtl + -dinlining Save RTL after inlining optimization in .inlining.rtl -dconstprop Save RTL after constant propagation in .constprop.rtl -dcse Save RTL after CSE optimization in .cse.rtl -dalloc Save LTL after register allocation in .alloc.ltl @@ -425,7 +427,7 @@ let cmdline_actions = "-dcminor", Set option_dcminor; "-drtl$", Set option_drtl; "-dtailcall$", Set option_dtailcall; - "-dcastopt$", Set option_dcastopt; + "-dinlining$", Set option_dinlining; "-dconstprop$", Set option_dconstprop; "-dcse$", Set option_dcse; "-dalloc$", Set option_dalloc; @@ -464,6 +466,7 @@ let cmdline_actions = linker_options := s :: !linker_options); "-fsmall-data$", Integer(fun n -> option_small_data := n); "-fsmall-const$", Integer(fun n -> option_small_const := n); + "-ffloat-const-prop$", Integer(fun n -> option_ffloatconstprop := n); "-fall$", Self (fun _ -> List.iter (fun r -> r := true) language_support_options); "-fnone$", Self (fun _ -> diff --git a/driver/Interp.ml b/driver/Interp.ml index 62f3093..a74d4d8 100644 --- a/driver/Interp.ml +++ b/driver/Interp.ml @@ -145,6 +145,12 @@ let mem_of_state = function (* Comparing memory states *) +let compare_mem m1 m2 = + Pervasives.compare (m1.Mem.nextblock, m1.Mem.mem_contents) + (m2.Mem.nextblock, m1.Mem.mem_contents) +(* FIXME: should permissions be taken into account? *) + +(* let rec compare_Z_range lo hi f = if coq_Zcompare lo hi = Lt then begin let c = f lo in if c <> 0 then c else compare_Z_range (coq_Zsucc lo) hi f @@ -154,6 +160,7 @@ let compare_mem m1 m2 = if m1 == m2 then 0 else let c = compare m1.Mem.nextblock m2.Mem.nextblock in if c <> 0 then c else compare_Z_range Z0 m1.Mem.nextblock (fun b -> + let ((lo, hi) as bnds) = m1.Mem.bounds b in let c = compare bnds (m2.Mem.bounds b) in if c <> 0 then c else let contents1 = m1.Mem.mem_contents b and contents2 = m2.Mem.mem_contents b in @@ -163,6 +170,7 @@ let compare_mem m1 m2 = let access1 = m1.Mem.mem_access b and access2 = m2.Mem.mem_access b in if access1 == access2 then 0 else compare_Z_range lo hi (fun ofs -> compare (access1 ofs) (access2 ofs))) +*) (* Comparing continuations *) -- cgit v1.2.3