- Back to origins: suppress Mfloat64al32 chunk and align Mfloat64 to 4.

- Revised printing of intermediate RTL code.


git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2403 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e

3 files changed, 19 insertions, 38 deletions

diff --git a/driver/Clflags.ml b/driver/Clflags.ml
index 4d6e3f6..5d068b6 100644
--- a/driver/Clflags.ml
+++ b/driver/Clflags.ml
@@ -33,12 +33,7 @@ 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_dinlining = ref false
-let option_dconstprop = ref false
-let option_dcse = ref false
-let option_ddeadcode = ref false
-let option_dalloc = ref false
+let option_dltl = ref false
 let option_dalloctrace = ref false
 let option_dmach = ref false
 let option_dasm = ref false
diff --git a/driver/Compiler.v b/driver/Compiler.v
index d088bc9..d3628b5 100644
--- a/driver/Compiler.v
+++ b/driver/Compiler.v
@@ -74,12 +74,7 @@ Require Asmgenproof.
 (** Pretty-printers (defined in Caml). *)
 Parameter print_Clight: Clight.program -> unit.
 Parameter print_Cminor: Cminor.program -> 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_RTL_deadcode: RTL.program -> unit.
+Parameter print_RTL: Z -> RTL.program -> unit.
 Parameter print_LTL: LTL.program -> unit.
 Parameter print_Mach: Mach.program -> unit.
 
@@ -112,19 +107,21 @@ Definition print {A: Type} (printer: A -> unit) (prog: A) : A :=
 
 Definition transf_rtl_program (f: RTL.program) : res Asm.program :=
    OK f
-   @@ print print_RTL
+   @@ print (print_RTL 0)
    @@ Tailcall.transf_program
-   @@ print print_RTL_tailcall
+   @@ print (print_RTL 1)
   @@@ Inlining.transf_program
+   @@ print (print_RTL 2)
    @@ Renumber.transf_program
-   @@ print print_RTL_inline
+   @@ print (print_RTL 3)
    @@ Constprop.transf_program
+   @@ print (print_RTL 4)
    @@ Renumber.transf_program
-   @@ print print_RTL_constprop
+   @@ print (print_RTL 5)
   @@@ CSE.transf_program
-   @@ print print_RTL_cse
+   @@ print (print_RTL 6)
   @@@ Deadcode.transf_program
-   @@ print print_RTL_deadcode
+   @@ print (print_RTL 7)
   @@@ Allocation.transf_program
    @@ print print_LTL
    @@ Tunneling.tunnel_program
diff --git a/driver/Driver.ml b/driver/Driver.ml
index d5b99d4..c35ac1f 100644
--- a/driver/Driver.ml
+++ b/driver/Driver.ml
@@ -147,14 +147,9 @@ let compile_c_ast sourcename csyntax ofile =
                    else None in
   set_dest PrintClight.destination option_dclight ".light.c";
   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_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 PrintRTL.destination_deadcode option_ddeadcode ".deadcode.rtl";
+  set_dest PrintRTL.destination option_drtl ".rtl";
   set_dest Regalloc.destination_alloctrace option_dalloctrace ".alloctrace";
-  set_dest PrintLTL.destination option_dalloc ".alloc.ltl";
+  set_dest PrintLTL.destination option_dltl ".ltl";
   set_dest PrintMach.destination option_dmach ".mach";
   (* Convert to Asm *)
   let asm =
@@ -427,12 +422,8 @@ Tracing options:
   -dc            Save generated Compcert C in <file>.compcert.c
   -dclight       Save generated Clight in <file>.light.c
   -dcminor       Save generated Cminor in <file>.cm
-  -drtl          Save unoptimized generated RTL in <file>.rtl
-  -dtailcall     Save RTL after tail call optimization in <file>.tailcall.rtl
-  -dinlining     Save RTL after inlining optimization in <file>.inlining.rtl
-  -dconstprop    Save RTL after constant propagation in <file>.constprop.rtl
-  -dcse          Save RTL after CSE optimization in <file>.cse.rtl
-  -dalloc        Save LTL after register allocation in <file>.alloc.ltl
+  -drtl          Save RTL at various optimization points in <file>.rtl.<n>
+  -dltl          Save LTL after register allocation in <file>.ltl
   -dmach         Save generated Mach code in <file>.mach
   -dasm          Save generated assembly in <file>.s
   -sdump         Save info for post-linking validation in <file>.sdump
@@ -476,12 +467,7 @@ let cmdline_actions =
   "-dclight$", Set option_dclight;
   "-dcminor", Set option_dcminor;
   "-drtl$", Set option_drtl;
-  "-dtailcall$", Set option_dtailcall;
-  "-dinlining$", Set option_dinlining;
-  "-dconstprop$", Set option_dconstprop;
-  "-dcse$", Set option_dcse;
-  "-ddeadcode$", Set option_ddeadcode;
-  "-dalloc$", Set option_dalloc;
+  "-dltl$", Set option_dltl;
   "-dalloctrace$", Set option_dalloctrace;
   "-dmach$", Set option_dmach;
   "-dasm$", Set option_dasm;
@@ -534,7 +520,10 @@ let cmdline_actions =
   @ f_opt "sse" option_ffpu (* backward compatibility *)
 
 let _ =
-  Gc.set { (Gc.get()) with Gc.minor_heap_size = 524288 };
+  Gc.set { (Gc.get()) with
+              Gc.minor_heap_size = 524288; (* 512k *)
+              Gc.major_heap_increment = 4194304 (* 4M *)
+         };
   Printexc.record_backtrace true;
   Machine.config :=
     begin match Configuration.arch with