diff options
-rw-r--r-- | driver/Driver.ml | 17 | ||||
-rw-r--r-- | driver/Optionsprinter.ml | 45 |
2 files changed, 58 insertions, 4 deletions
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 <file>.mach -dasm Save generated assembly in <file>.s -sdump Save info for post-linking validation in <file>.json + -doptions Save the compiler configurations in <file>.opt.json General options: -stdlib <dir> 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 diff --git a/driver/Optionsprinter.ml b/driver/Optionsprinter.ml index 0e3fa379..6302f210 100644 --- a/driver/Optionsprinter.ml +++ b/driver/Optionsprinter.ml @@ -12,12 +12,13 @@ open Clflags open Json +open Machine open Printf let print_list oc name l = p_jmember oc name (p_jarray p_jstring) l -let print_clflags oc ((): unit) = +let print_clflags oc = fprintf oc "{"; print_list oc "prepro_options" !prepro_options; print_list oc "linker_options" !linker_options; @@ -94,3 +95,45 @@ let print_configurations oc lib_path = p_jmember oc "struct_passing_style" print_struct_passing_style Configuration.struct_passing_style; p_jmember oc "struct_return_style" print_struct_return_style Configuration.struct_return_style; fprintf oc "\n}" + +let print_machine oc = + fprintf oc "{"; + p_jmember oc "name" p_jstring !config.name; + p_jmember oc "char_signed" p_jbool !config.char_signed; + p_jmember oc "sizeof_ptr" p_jint !config.sizeof_ptr; + p_jmember oc "sizeof_short" p_jint !config.sizeof_short; + p_jmember oc "sizeof_int" p_jint !config.sizeof_int; + p_jmember oc "sizeof_long" p_jint !config.sizeof_long; + p_jmember oc "sizeof_longlong" p_jint !config.sizeof_longlong; + p_jmember oc "sizeof_float" p_jint !config.sizeof_float; + p_jmember oc "sizeof_double" p_jint !config.sizeof_double; + p_jmember oc "sizeof_longdouble" p_jint !config.sizeof_longdouble; + p_jmember oc "sizeof_void" (p_jopt p_jint) !config.sizeof_void; + p_jmember oc "sizeof_fun" (p_jopt p_jint) !config.sizeof_fun; + p_jmember oc "sizeof_wchar" p_jint !config.sizeof_wchar; + p_jmember oc "wchar_signed" p_jbool !config.wchar_signed; + p_jmember oc "sizeof_size_t" p_jint !config.sizeof_size_t; + p_jmember oc "sizeof_ptrdiff_t" p_jint !config.sizeof_ptrdiff_t; + p_jmember oc "alignof_ptr" p_jint !config.alignof_ptr; + p_jmember oc "alignof_short" p_jint !config.alignof_short; + p_jmember oc "alignof_int" p_jint !config.alignof_int; + p_jmember oc "alignof_long" p_jint !config.alignof_long; + p_jmember oc "alignof_longlong" p_jint !config.alignof_longlong; + p_jmember oc "alignof_float" p_jint !config.alignof_float; + p_jmember oc "alignof_double" p_jint !config.alignof_double; + p_jmember oc "alignof_longdouble" p_jint !config.alignof_longdouble; + p_jmember oc "alignof_void" (p_jopt p_jint) !config.alignof_void; + p_jmember oc "alignof_fun" (p_jopt p_jint) !config.alignof_fun; + p_jmember oc "bigendian" p_jbool !config.bigendian; + p_jmember oc "bitfields_msb_first" p_jbool !config.bitfields_msb_first; + p_jmember oc "supports_unaligned_accesses" p_jbool !config.supports_unaligned_accesses; + fprintf oc "\n}" + +let print file stdlib = + let oc = open_out file in + fprintf oc "{"; + fprintf oc "%a:%t" p_jstring "Clflags" print_clflags; + p_jmember oc "Configurations" print_configurations stdlib; + fprintf oc "%a:%t" p_jstring "Machine" print_machine; + fprintf oc "}"; + close_out oc |