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.

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