From fb202a70ccc2872aa3849854c09810a6bee268e5 Mon Sep 17 00:00:00 2001 From: xleroy Date: Sun, 8 May 2011 08:39:30 +0000 Subject: powerpc/PrintAsm.ml arm/PrintAsm.ml: updated (no label elimination). Added -dmach option and corresponding printer for Mach code. CleanupLabelsproof.v: fixed for ARM Driver.ml: -E sends output to stdout; support for .s and .S source files. cparser/Elab.ml: spurious comment deleted. git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1648 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e --- driver/Clflags.ml | 1 + driver/Compiler.v | 7 ++++--- driver/Driver.ml | 49 +++++++++++++++++++++++++++++++++++++++++-------- 3 files changed, 46 insertions(+), 11 deletions(-) (limited to 'driver') diff --git a/driver/Clflags.ml b/driver/Clflags.ml index b34b10a8..c47d0f34 100644 --- a/driver/Clflags.ml +++ b/driver/Clflags.ml @@ -31,6 +31,7 @@ let option_dcastopt = ref false let option_dconstprop = ref false let option_dcse = ref false let option_dalloc = ref false +let option_dmach = ref false let option_dasm = ref false let option_E = ref false let option_S = ref false diff --git a/driver/Compiler.v b/driver/Compiler.v index bde63089..d8810a4c 100644 --- a/driver/Compiler.v +++ b/driver/Compiler.v @@ -92,6 +92,7 @@ Parameter print_RTL_castopt: 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. Open Local Scope string_scope. @@ -113,7 +114,7 @@ Notation "a @@ b" := (apply_total _ _ a b) (at level 50, left associativity). Definition print {A: Type} (printer: A -> unit) (prog: A) : A := - match printer prog with tt => prog end. + let unused := printer prog in prog. (** We define three translation functions for whole programs: one starting with a C program, one with a Cminor program, one with an @@ -149,6 +150,7 @@ Definition transf_rtl_fundef (f: RTL.fundef) : res Asm.fundef := @@ print print_LTLin @@ Reload.transf_fundef @@@ Stacking.transf_fundef + @@ print print_Mach @@@ Asmgen.transf_fundef. (* Here is the translation of a CminorSel function to an Asm function. *) @@ -316,7 +318,7 @@ Proof. Reloadtyping.program_typing_preserved Stackingtyping.program_typing_preserved; intros. - eapply Asmgenproof.transf_program_correct; eauto 6. + eapply Asmgenproof.transf_program_correct; eauto 8. eapply Stackingproof.transf_program_correct; eauto 6. eapply Reloadproof.transf_program_correct; eauto. eapply CleanupLabelsproof.transf_program_correct; eauto. @@ -341,7 +343,6 @@ Proof. eapply transf_rtl_program_correct; eauto. eapply RTLgenproof.transf_program_correct; eauto. eapply Selectionproof.transf_program_correct; eauto. - rewrite print_identity. auto. Qed. Theorem transf_c_program_correct: diff --git a/driver/Driver.ml b/driver/Driver.ml index ee48ffca..87b15694 100644 --- a/driver/Driver.ml +++ b/driver/Driver.ml @@ -46,16 +46,18 @@ let print_error oc msg = (* From C to preprocessed C *) let preprocess ifile ofile = + let output = + if ofile = "-" then "" else sprintf "> %s" ofile in let cmd = - sprintf "%s -D__COMPCERT__ %s %s %s > %s" + sprintf "%s -D__COMPCERT__ %s %s %s %s" Configuration.prepro (if Configuration.need_stdlib_wrapper then sprintf "-I%s" !stdlib_path else "") (quote_options !prepro_options) - ifile ofile in + ifile output in if command cmd <> 0 then begin - safe_remove ofile; + if ofile <> "-" then safe_remove ofile; eprintf "Error during preprocessing.\n"; exit 2 end @@ -103,6 +105,7 @@ let compile_c_file sourcename ifile ofile = 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"; + set_dest PrintMach.destination option_dmach ".mach"; (* Convert to Asm *) let asm = match Compiler.transf_c_program csyntax with @@ -152,7 +155,6 @@ let assemble ifile ofile = sprintf "%s -o %s %s" Configuration.asm ofile ifile in let retcode = command cmd in - if not !option_dasm then safe_remove ifile; if retcode <> 0 then begin safe_remove ofile; eprintf "Error during assembling.\n"; @@ -177,7 +179,7 @@ let linker exe_name files = let process_c_file sourcename = let prefixname = Filename.chop_suffix sourcename ".c" in if !option_E then begin - preprocess sourcename (prefixname ^ ".i") + preprocess sourcename "-" end else begin let preproname = Filename.temp_file "compcert" ".i" in preprocess sourcename preproname; @@ -189,7 +191,8 @@ let process_c_file sourcename = then prefixname ^ ".s" else Filename.temp_file "compcert" ".s" in compile_c_file sourcename preproname asmname; - assemble asmname (prefixname ^ ".o") + assemble asmname (prefixname ^ ".o"); + if not !option_dasm then safe_remove asmname end end; prefixname ^ ".o" @@ -206,7 +209,27 @@ let process_cminor_file sourcename = then prefixname ^ ".s" else Filename.temp_file "compcert" ".s" in compile_cminor_file sourcename asmname; - assemble asmname (prefixname ^ ".o") + assemble asmname (prefixname ^ ".o"); + if not !option_dasm then safe_remove asmname + end; + prefixname ^ ".o" + +(* Processing of .S and .s files *) + +let process_s_file sourcename = + let prefixname = Filename.chop_suffix sourcename ".s" in + assemble sourcename (prefixname ^ ".o"); + prefixname ^ ".o" + +let process_S_file sourcename = + let prefixname = Filename.chop_suffix sourcename ".s" in + if !option_E then begin + preprocess sourcename "-" + end else begin + let preproname = Filename.temp_file "compcert" ".s" in + preprocess sourcename preproname; + assemble preproname (prefixname ^ ".o"); + safe_remove preproname end; prefixname ^ ".o" @@ -217,10 +240,12 @@ let usage_string = Recognized source files: .c C source file .cm Cminor source file + .s Assembly file + .S Assembly file, to be run through the preprocessor .o Object file .a Library file Processing options: - -E Preprocess only, save result in .i + -E Preprocess only, send result to standard output -S Compile to assembler only, save result in .s -c Compile to object file only (no linking), result in .o Preprocessing options: @@ -248,6 +273,7 @@ Tracing options: -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 + -dmach Save generated Mach code in .mach -dasm Save generated assembly in .s Linking options: -l Link library @@ -332,6 +358,7 @@ let cmdline_actions = "-dconstprop$", Set option_dconstprop; "-dcse$", Set option_dcse; "-dalloc$", Set option_dalloc; + "-dmach$", Set option_dmach; "-dasm$", Set option_dasm; "-E$", Set option_E; "-S$", Set option_S; @@ -343,6 +370,12 @@ let cmdline_actions = ".*\\.cm$", Self (fun s -> let objfile = process_cminor_file s in linker_options := objfile :: !linker_options); + ".*\\.s$", Self (fun s -> + let objfile = process_s_file s in + linker_options := objfile :: !linker_options); + ".*\\.S$", Self (fun s -> + let objfile = process_S_file s in + linker_options := objfile :: !linker_options); ".*\\.[oa]$", Self (fun s -> linker_options := s :: !linker_options); "-fsmall-data$", Integer(fun n -> option_small_data := n); -- cgit