From 4467453e0edca993c175690b7141d4916af3dc19 Mon Sep 17 00:00:00 2001 From: Bernhard Schommer Date: Mon, 25 Jan 2016 10:03:11 +0100 Subject: Started implementing a printer for Clflags. --- driver/Driver.ml | 1 + 1 file changed, 1 insertion(+) (limited to 'driver/Driver.ml') diff --git a/driver/Driver.ml b/driver/Driver.ml index 78d141c1..d827fd94 100644 --- a/driver/Driver.ml +++ b/driver/Driver.ml @@ -14,6 +14,7 @@ open Printf open Commandline open Camlcoq open Clflags +open Clflagsprinter open Timing (* Location of the compatibility library *) -- cgit From 35c7398e985c51a765c6bbf08719d9df7c285f9c Mon Sep 17 00:00:00 2001 From: Bernhard Schommer Date: Mon, 25 Jan 2016 20:11:09 +0100 Subject: Added printer for Configuration and finished Clflags. --- driver/Driver.ml | 54 ++++++++++++++++++++++++++---------------------------- 1 file changed, 26 insertions(+), 28 deletions(-) (limited to 'driver/Driver.ml') diff --git a/driver/Driver.ml b/driver/Driver.ml index d827fd94..27115f3f 100644 --- a/driver/Driver.ml +++ b/driver/Driver.ml @@ -14,7 +14,7 @@ open Printf open Commandline open Camlcoq open Clflags -open Clflagsprinter +open Optionsprinter open Timing (* Location of the compatibility library *) @@ -283,37 +283,35 @@ let process_c_file sourcename = preprocess sourcename (output_filename_default "-"); "" end else begin - let preproname = if !option_dprepro then + let preproname = if !option_dprepro then output_filename sourcename ".c" ".i" else Filename.temp_file "compcert" ".i" in preprocess sourcename preproname; - if !option_interp then begin - Machine.config := Machine.compcert_interpreter !Machine.config; - let csyntax,_ = parse_c_file sourcename preproname in - if not !option_dprepro then - safe_remove preproname; - Interp.execute csyntax; - "" - end else if !option_S then begin - compile_c_file sourcename preproname - (output_filename ~final:true sourcename ".c" ".s"); - if not !option_dprepro then - safe_remove preproname; - "" - end else begin - let asmname = - if !option_dasm - then output_filename sourcename ".c" ".s" - else Filename.temp_file "compcert" ".s" in - compile_c_file sourcename preproname asmname; - if not !option_dprepro then - safe_remove preproname; - let objname = output_filename ~final: !option_c sourcename ".c" ".o" in - assemble asmname objname; - if not !option_dasm then safe_remove asmname; - objname - end + let name = + 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 preproname + (output_filename ~final:true sourcename ".c" ".s"); + "" + end else begin + let asmname = + if !option_dasm + then output_filename sourcename ".c" ".s" + else Filename.temp_file "compcert" ".s" in + compile_c_file sourcename preproname 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 in + if not !option_dprepro then + safe_remove preproname; + name end (* Processing of a .i / .p file (preprocessed C) *) -- cgit From fa2230c7fc2b20e29251b6b550b046d0dc75f953 Mon Sep 17 00:00:00 2001 From: Bernhard Schommer Date: Wed, 27 Jan 2016 09:05:55 +0100 Subject: Added new option -doptions. The new options dumps the compiler options in a json file per. This includes the clflags, compcert.ini and machine settings. Bug 17988. --- driver/Driver.ml | 17 ++++++++++++++--- 1 file changed, 14 insertions(+), 3 deletions(-) (limited to 'driver/Driver.ml') diff --git a/driver/Driver.ml b/driver/Driver.ml index 27115f3f..81f28309 100644 --- a/driver/Driver.ml +++ b/driver/Driver.ml @@ -14,13 +14,14 @@ open Printf open Commandline open Camlcoq open Clflags -open Optionsprinter open Timing (* Location of the compatibility library *) let stdlib_path = ref Configuration.stdlib_path +let dump_options = ref false + (* Optional sdump suffix *) let sdump_suffix = ref ".json" @@ -311,6 +312,8 @@ let process_c_file sourcename = end in if not !option_dprepro then safe_remove preproname; + if !dump_options then + Optionsprinter.print (output_filename sourcename ".c" ".opt.json") !stdlib_path; name end @@ -323,7 +326,9 @@ let process_i_file sourcename = "" end else if !option_S then begin compile_c_file sourcename sourcename - (output_filename ~final:true sourcename ".c" ".s"); + (output_filename ~final:true sourcename ".c" ".s"); + if !dump_options then + Optionsprinter.print (output_filename sourcename ".c" ".opt.json") !stdlib_path; "" end else begin let asmname = @@ -334,6 +339,8 @@ let process_i_file sourcename = let objname = output_filename ~final: !option_c sourcename ".c" ".o" in assemble asmname objname; if not !option_dasm then safe_remove asmname; + if !dump_options then + Optionsprinter.print (output_filename sourcename ".c" ".opt.json") !stdlib_path; objname end @@ -353,6 +360,8 @@ let process_cminor_file sourcename = let objname = output_filename ~final: !option_c sourcename ".cm" ".o" in assemble asmname objname; if not !option_dasm then safe_remove asmname; + if !dump_options then + Optionsprinter.print (output_filename sourcename ".cm" ".opt.json") !stdlib_path; objname end @@ -495,6 +504,7 @@ Tracing options: -dmach Save generated Mach code in .mach -dasm Save generated assembly in .s -sdump Save info for post-linking validation in .json + -doptions Save the compiler configurations in .opt.json General options: -stdlib Set the path of the Compcert run-time library -v Print external commands before invoking them @@ -620,6 +630,7 @@ let cmdline_actions = Exact "-dasm", Set option_dasm; Exact "-sdump", Set option_sdump; Exact "-sdump-suffix", String (fun s -> option_sdump := true; sdump_suffix:= s); + Exact "-doptions", Set dump_options; (* General options *) Exact "-v", Set option_v; Exact "-stdlib", String(fun s -> stdlib_path := s); @@ -711,6 +722,6 @@ let _ = let linker_args = time "Total compilation time" perform_actions () in if (not nolink) && linker_args <> [] then begin linker (output_filename_default "a.out") linker_args - end + end; with Sys_error msg -> eprintf "I/O error: %s.\n" msg; exit 2 -- cgit