From 413bd7681ed70155b7bbc9ab2255801ed41904ea Mon Sep 17 00:00:00 2001 From: Bernhard Schommer Date: Fri, 6 May 2022 12:54:34 +0200 Subject: Simplify handling of file suffixes. Since we are sure that all files passed have a valid extension we can use the OCaml function Filename.remove_extension and don't need to pass the suffixes. Bug 33218 --- driver/Driver.ml | 38 ++++++++++++++++++-------------------- driver/Driveraux.ml | 6 +++--- driver/Driveraux.mli | 2 +- export/ExportDriver.ml | 12 ++++++------ 4 files changed, 28 insertions(+), 30 deletions(-) diff --git a/driver/Driver.ml b/driver/Driver.ml index 0686f193..4266e57e 100644 --- a/driver/Driver.ml +++ b/driver/Driver.ml @@ -30,18 +30,18 @@ let sdump_suffix = ref ".json" let nolink () = !option_c || !option_S || !option_E || !option_interp -let object_filename sourcename suff = +let object_filename sourcename = if nolink () then - output_filename ~final: !option_c sourcename suff ".o" + output_filename ~final: !option_c sourcename ~suffix:".o" else tmp_file ".o" (* From CompCert C AST to asm *) -let compile_c_file sourcename ~sourcesuffix ifile ofile = +let compile_c_file sourcename ifile ofile = (* Prepare to dump Clight, RTL, etc, if requested *) let set_dest dst opt ext = - dst := if !opt then Some (output_filename sourcename sourcesuffix ext) + dst := if !opt then Some (output_filename sourcename ~suffix:ext) else None in set_dest Cprint.destination option_dparse ".parsed.c"; set_dest PrintCsyntax.destination option_dcmedium ".compcert.c"; @@ -73,23 +73,23 @@ let compile_c_file sourcename ~sourcesuffix ifile ofile = (* From C source to asm *) -let compile_i_file sourcename ~sourcesuffix preproname = +let compile_i_file sourcename preproname = if !option_interp then begin Machine.config := Machine.compcert_interpreter !Machine.config; let csyntax = parse_c_file sourcename preproname in Interp.execute csyntax; "" end else if !option_S then begin - compile_c_file sourcename ~sourcesuffix:sourcesuffix preproname - (output_filename ~final:true sourcename sourcesuffix ".s"); + compile_c_file sourcename preproname + (output_filename ~final:true sourcename ~suffix:".s"); "" end else begin let asmname = if !option_dasm - then output_filename sourcename sourcesuffix ".s" + then output_filename sourcename ~suffix:".s" else tmp_file ".s" in - compile_c_file sourcename ~sourcesuffix:sourcesuffix preproname asmname; - let objname = object_filename sourcename sourcesuffix in + compile_c_file sourcename preproname asmname; + let objname = object_filename sourcename in assemble asmname objname; objname end @@ -103,24 +103,24 @@ let process_c_file sourcename = "" end else begin let preproname = if !option_dprepro then - output_filename sourcename ".c" ".i" + output_filename sourcename ~suffix:".i" else tmp_file ".i" in preprocess sourcename preproname; - compile_i_file sourcename ~sourcesuffix:".c" preproname + compile_i_file sourcename preproname end (* Processing of a .i / .p file (preprocessed C) *) -let process_i_file sourcename ~sourcesuffix = +let process_i_file sourcename = ensure_inputfile_exists sourcename; - compile_i_file sourcename ~sourcesuffix:sourcesuffix sourcename + compile_i_file sourcename sourcename (* Processing of .S and .s files *) let process_s_file sourcename = ensure_inputfile_exists sourcename; - let objname = object_filename sourcename ".s" in + let objname = object_filename sourcename in assemble sourcename objname; objname @@ -132,7 +132,7 @@ let process_S_file sourcename = end else begin let preproname = tmp_file ".s" in preprocess sourcename preproname; - let objname = object_filename sourcename ".S" in + let objname = object_filename sourcename in assemble preproname objname; objname end @@ -379,11 +379,9 @@ let cmdline_actions = Suffix ".c", Self (fun s -> push_action process_c_file s; incr num_source_files; incr num_input_files); Suffix ".i", Self (fun s -> - push_action (process_i_file ~sourcesuffix:".i") s; - incr num_source_files; incr num_input_files); + push_action process_i_file s; incr num_source_files; incr num_input_files); Suffix ".p", Self (fun s -> - push_action (process_i_file ~sourcesuffix:".p") s; - incr num_source_files; incr num_input_files); + push_action process_i_file s; incr num_source_files; incr num_input_files); Suffix ".s", Self (fun s -> push_action process_s_file s; incr num_source_files; incr num_input_files); Suffix ".S", Self (fun s -> diff --git a/driver/Driveraux.ml b/driver/Driveraux.ml index 5b2d792e..4b9809a6 100644 --- a/driver/Driveraux.ml +++ b/driver/Driveraux.ml @@ -89,12 +89,12 @@ let command_error n exc = 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 = +let output_filename ?(final = false) source_file ~suffix = match !option_o with | Some file when final -> file | _ -> - Filename.basename (Filename.chop_suffix source_file source_suffix) - ^ output_suffix + Filename.basename (Filename.remove_extension source_file) + ^ suffix (* A variant of [output_filename] where the default output name is fixed *) diff --git a/driver/Driveraux.mli b/driver/Driveraux.mli index 6f0eaddb..47f923f0 100644 --- a/driver/Driveraux.mli +++ b/driver/Driveraux.mli @@ -27,7 +27,7 @@ val tmp_file: string -> string The file will be removed when the program exits. Return the absolute path to the file. *) -val output_filename: ?final:bool -> string -> string -> string -> string +val output_filename: ?final:bool -> string -> suffix:string -> string (** 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. *) diff --git a/export/ExportDriver.ml b/export/ExportDriver.ml index d7980994..365392c3 100644 --- a/export/ExportDriver.ml +++ b/export/ExportDriver.ml @@ -67,7 +67,7 @@ let export_clight sourcename csyntax ofile = let compile_c_file sourcename ifile ofile = let set_dest dst opt ext = - dst := if !opt then Some (output_filename sourcename ".c" ext) + dst := if !opt then Some (output_filename sourcename ~suffix:ext) else None in set_dest Cprint.destination option_dparse ".parsed.c"; set_dest PrintCsyntax.destination option_dcmedium ".compcert.c"; @@ -77,20 +77,20 @@ let compile_c_file sourcename ifile ofile = | Mode_Csyntax -> export_csyntax sourcename cs ofile | Mode_Clight -> export_clight sourcename cs ofile -let output_filename sourcename suff = - let prefixname = Filename.chop_suffix sourcename suff in +let output_filename sourcename = + let prefixname = Filename.remove_extension sourcename in output_filename_default (prefixname ^ ".v") (* Processing of a .c file *) let process_c_file sourcename = ensure_inputfile_exists sourcename; - let ofile = output_filename sourcename ".c" in + let ofile = output_filename sourcename in if !option_E then begin preprocess sourcename "-" end else begin let preproname = if !option_dprepro then - Driveraux.output_filename sourcename ".c" ".i" + Driveraux.output_filename sourcename ~suffix:".i" else Driveraux.tmp_file ".i" in preprocess sourcename preproname; @@ -101,7 +101,7 @@ let process_c_file sourcename = let process_i_file sourcename = ensure_inputfile_exists sourcename; - let ofile = output_filename sourcename ".i" in + let ofile = output_filename sourcename in compile_c_file sourcename sourcename ofile let usage_string = -- cgit