From b7ece9390230882513633413f13f5cf7a34040db Mon Sep 17 00:00:00 2001 From: xleroy Date: Mon, 8 Oct 2012 13:29:20 +0000 Subject: Generate output files in current directory; can be overriden with -o option git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2061 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e --- Changelog | 6 ++++ driver/Clflags.ml | 2 +- driver/Driver.ml | 91 +++++++++++++++++++++++++++++++++++-------------------- 3 files changed, 65 insertions(+), 34 deletions(-) diff --git a/Changelog b/Changelog index f8c7784..056b2e3 100644 --- a/Changelog +++ b/Changelog @@ -18,10 +18,16 @@ Performance improvements: Internal simplifications: - Clight, Csharpminor, Cminor: suppressed the "Econdition" conditional expressions, no longer useful. +- Clight: a single loop form, the three C loops are derived forms. +- Clight: volatile memory accesses are materialized as builtin operations. +- Clight: removed dependencies on CompCert C syntax and semantics. - Cminor: suppressed the "Oboolval" and "Onotbool" operators, which can be expressed in terms of "Ocmpu" at no performance costs. Other changes: +- For compatibility with other C compilers, output files are now generated + in the current directory, by default; output file name can be controlled + with the -o option, somewhat like with GCC. - IA32/MacOS X: now supports referencing global variables defined in shared libraries; old hack for stdio is no longer needed. - PowerPC/MacOS X: this port was removed, as recent version of MacOS X diff --git a/driver/Clflags.ml b/driver/Clflags.ml index 47336b5..96c7901 100644 --- a/driver/Clflags.ml +++ b/driver/Clflags.ml @@ -15,7 +15,6 @@ let prepro_options = ref ([]: string list) let linker_options = ref ([]: string list) let assembler_options = ref ([]: string list) -let exe_name = ref "a.out" let option_flonglong = ref true let option_flongdouble = ref false let option_fstruct_return = ref false @@ -38,6 +37,7 @@ let option_dalloc = ref false let option_dmach = ref false let option_dasm = ref false let option_sdump = ref false +let option_o = ref (None: string option) let option_E = ref false let option_S = ref false let option_c = ref false diff --git a/driver/Driver.ml b/driver/Driver.ml index 3ee4b6b..87007a7 100644 --- a/driver/Driver.ml +++ b/driver/Driver.ml @@ -52,6 +52,24 @@ let print_error oc msg = List.iter print_one_error msg; output_char oc '\n' +(* Determine names for output files. We use -o option if specified + and if this is the final destination file (not a dump file). + Otherwise, we generate a file in the current directory. *) + +let output_filename ?(final = false) source_file source_suffix output_suffix = + match !option_o with + | Some file when final -> option_o := None; file + | _ -> + Filename.basename (Filename.chop_suffix source_file source_suffix) + ^ output_suffix + +(* A variant of [output_filename] where the default output name is fixed *) + +let output_filename_default default_file = + match !option_o with + | Some file -> option_o := None; file + | None -> default_file + (* From C to preprocessed C *) let preprocess ifile ofile = @@ -91,7 +109,7 @@ let parse_c_file sourcename ifile = safe_remove ifile; (* Save C AST if requested *) if !option_dparse then begin - let ofile = Filename.chop_suffix sourcename ".c" ^ ".parsed.c" in + let ofile = output_filename sourcename ".c" ".parsed.c" in let oc = open_out ofile in Cprint.program (Format.formatter_of_out_channel oc) ast; close_out oc @@ -104,7 +122,7 @@ let parse_c_file sourcename ifile = flush stderr; (* Save CompCert C AST if requested *) if !option_dcmedium then begin - let ofile = Filename.chop_suffix sourcename ".c" ^ ".compcert.c" in + let ofile = output_filename sourcename ".c" ".compcert.c" in let oc = open_out ofile in PrintCsyntax.print_program (Format.formatter_of_out_channel oc) csyntax; close_out oc @@ -128,7 +146,7 @@ let dump_asm asm destfile = let compile_c_ast sourcename csyntax ofile = (* Prepare to dump Clight, RTL, etc, if requested *) let set_dest dst opt ext = - dst := if !opt then Some (Filename.chop_suffix sourcename ".c" ^ ext) + dst := if !opt then Some (output_filename sourcename ".c" ext) else None in set_dest PrintClight.destination option_dclight ".light.c"; set_dest PrintCminor.destination option_dcminor ".cm"; @@ -148,7 +166,7 @@ let compile_c_ast sourcename csyntax ofile = exit 2 in (* Dump Asm in binary format *) if !option_sdump then - dump_asm asm (Filename.chop_suffix sourcename ".c" ^ ".sdump"); + dump_asm asm (output_filename sourcename ".c" ".sdump"); (* Print Asm in text form *) let oc = open_out ofile in PrintAsm.print_program oc (Unusedglob.transf_program asm); @@ -220,64 +238,71 @@ let linker exe_name files = let option_interp = ref false let process_c_file sourcename = - let prefixname = Filename.chop_suffix sourcename ".c" in if !option_E then begin - preprocess sourcename "-" + preprocess sourcename (output_filename_default "-"); + "" end else begin let preproname = Filename.temp_file "compcert" ".i" in preprocess sourcename preproname; if !option_interp then begin let csyntax = parse_c_file sourcename preproname in - Interp.execute csyntax + Interp.execute csyntax; + "" end else if !option_S then begin - compile_c_file sourcename preproname (prefixname ^ ".s") + compile_c_file sourcename preproname + (output_filename ~final:true sourcename ".c" ".s"); + "" end else begin let asmname = if !option_dasm - then prefixname ^ ".s" + then output_filename sourcename ".c" ".s" else Filename.temp_file "compcert" ".s" in compile_c_file sourcename preproname asmname; - assemble asmname (prefixname ^ ".o"); - if not !option_dasm then safe_remove asmname + let objname = output_filename ~final: !option_c sourcename ".c" ".o" in + assemble asmname objname; + if not !option_dasm then safe_remove asmname; + objname end - end; - prefixname ^ ".o" + end (* Processing of a .cm file *) let process_cminor_file sourcename = - let prefixname = Filename.chop_suffix sourcename ".cm" in if !option_S then begin - compile_cminor_file sourcename (prefixname ^ ".s") + compile_cminor_file sourcename + (output_filename ~final:true sourcename ".cm" ".s"); + "" end else begin let asmname = if !option_dasm - then prefixname ^ ".s" + then output_filename sourcename ".cm" ".s" else Filename.temp_file "compcert" ".s" in compile_cminor_file sourcename asmname; - assemble asmname (prefixname ^ ".o"); - if not !option_dasm then safe_remove asmname - end; - prefixname ^ ".o" + let objname = output_filename ~final: !option_c sourcename ".c" ".o" in + assemble asmname objname; + if not !option_dasm then safe_remove asmname; + objname + end (* 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 objname = output_filename ~final: !option_c sourcename ".s" ".o" in + assemble sourcename objname; + objname let process_S_file sourcename = - let prefixname = Filename.chop_suffix sourcename ".s" in if !option_E then begin - preprocess sourcename "-" + preprocess sourcename (output_filename_default "-"); + "" end else begin let preproname = Filename.temp_file "compcert" ".s" in preprocess sourcename preproname; - assemble preproname (prefixname ^ ".o"); - safe_remove preproname - end; - prefixname ^ ".o" + let objname = output_filename ~final: !option_c sourcename ".S" ".o" in + assemble preproname objname; + safe_remove preproname; + objname + end (* Command-line parsing *) @@ -350,9 +375,10 @@ Recognized source files: .o Object file .a Library file Processing options: + -c Compile to object file only (no linking), result in .o -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 + -o Generate output in Preprocessing options: -I Add to search path for #include files -D= Define preprocessor symbol @@ -392,7 +418,6 @@ Tracing options: Linking options: -l Link library -L Add to search path for libraries - -o Generate executable in (default: a.out) -Wl, Pass option to the linker General options: -stdlib Set the path of the Compcert run-time library [MacOS X only] @@ -420,7 +445,7 @@ let cmdline_actions = "-U$", String(fun s -> prepro_options := s :: "-U" :: !prepro_options); "-[IDU].", Self(fun s -> prepro_options := s :: !prepro_options); "-[lL].", Self(fun s -> linker_options := s :: !linker_options); - "-o$", String(fun s -> exe_name := s); + "-o$", String(fun s -> option_o := Some s); "-stdlib$", String(fun s -> stdlib_path := s); "-dparse$", Set option_dparse; "-dc$", Set option_dcmedium; @@ -497,5 +522,5 @@ let _ = if !linker_options <> [] && not (!option_c || !option_S || !option_E || !option_interp) then begin - linker !exe_name !linker_options + linker (output_filename_default "a.out") !linker_options end -- cgit v1.2.3