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/Clflagsprinter.ml | 41 +++++++++++++++++++++++++++++++++++++++++ driver/Driver.ml | 1 + lib/Json.ml | 33 +++++++++++++++++++++++++++++++++ powerpc/AsmToJSON.ml | 17 +++++------------ 4 files changed, 80 insertions(+), 12 deletions(-) create mode 100644 driver/Clflagsprinter.ml create mode 100644 lib/Json.ml diff --git a/driver/Clflagsprinter.ml b/driver/Clflagsprinter.ml new file mode 100644 index 00000000..11dcc818 --- /dev/null +++ b/driver/Clflagsprinter.ml @@ -0,0 +1,41 @@ +(* *********************************************************************) +(* *) +(* The Compcert verified compiler *) +(* *) +(* Bernhard Schommer, AbsInt Angewandte Informatik GmbH *) +(* *) +(* AbsInt Angewandte Informatik GmbH. All rights reserved. This file *) +(* is distributed under the terms of the INRIA Non-Commercial *) +(* License Agreement. *) +(* *) +(* *********************************************************************) + +open Clflags +open Json +open Printf + +let print_member oc name p_mem mem = + fprintf oc "\n%a:%a" p_jstring name p_mem mem + +let print_list oc name l = + print_member oc name (p_jarray p_jstring) l + +let print oc ((): unit) = + fprintf oc "{"; + print_list oc "Preprocessor Options" !prepro_options; + print_list oc "Linker Options" !linker_options; + print_list oc "Assembler Options" !assembler_options; + print_member oc "Flongdouble" p_jbool !option_flongdouble; + print_member oc "Fstruct_passing" p_jbool !option_fstruct_passing; + print_member oc "Fbitfields" p_jbool !option_fbitfields; + print_member oc "Fvarag_calls" p_jbool !option_fvararg_calls; + print_member oc "Funprototyped" p_jbool !option_funprototyped; + print_member oc "Fpacked_structs" p_jbool !option_fpacked_structs; + print_member oc "Ffpu" p_jbool !option_ffpu; + print_member oc "Ffloatconstprop" p_jint !option_ffloatconstprop; + print_member oc "Ftailcalls" p_jbool !option_ftailcalls; + print_member oc "Fconstprop" p_jbool !option_fconstprop; + print_member oc "Fcse" p_jbool !option_fcse; + print_member oc "Fredundance" p_jbool !option_fredundancy; + + fprintf oc "\n}" 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 *) diff --git a/lib/Json.ml b/lib/Json.ml new file mode 100644 index 00000000..db2de5d4 --- /dev/null +++ b/lib/Json.ml @@ -0,0 +1,33 @@ +(* *********************************************************************) +(* *) +(* The Compcert verified compiler *) +(* *) +(* Bernhard Schommer, AbsInt Angewandte Informatik GmbH *) +(* *) +(* AbsInt Angewandte Informatik GmbH. All rights reserved. This file *) +(* is distributed under the terms of the INRIA Non-Commercial *) +(* License Agreement. *) +(* *) +(* *********************************************************************) + +open Printf + +(* Simple functions for JSON printing *) + +(* Print a string as json string *) +let p_jstring oc s = fprintf oc "\"%s\"" s + +(* Print a list as json array *) +let p_jarray elem oc l = + match l with + | [] -> fprintf oc "[]" + | hd::tail -> + output_string oc "["; elem oc hd; + List.iter (fprintf oc ",%a" elem) tail; + output_string oc "]" + +(* Print a bool as json bool *) +let p_jbool oc = fprintf oc "%B" + +(* Print a int as json int *) +let p_jint oc = fprintf oc "%d" diff --git a/powerpc/AsmToJSON.ml b/powerpc/AsmToJSON.ml index 42ad4f97..4ca7dbde 100644 --- a/powerpc/AsmToJSON.ml +++ b/powerpc/AsmToJSON.ml @@ -17,11 +17,10 @@ open AST open BinNums open C2C open Camlcoq +open Json open Printf open Sections -let p_jstring oc s = fprintf oc "\"%s\"" s - let p_ireg oc = function | GPR0 -> fprintf oc "{\"Register\":\"r0\"}" | GPR1 -> fprintf oc "{\"Register\":\"r1\"}" @@ -129,12 +128,6 @@ let p_crbit oc c = let p_label oc l = fprintf oc "{\"Label\":%ld}" (P.to_int32 l) -let p_list elem oc l = - match l with - | [] -> fprintf oc "[]" - | hd::tail -> - output_string oc "["; elem oc hd;List.iter (fprintf oc ",%a" elem) tail;output_string oc "]" - type instruction_arg = | Ireg of ireg | Freg of freg @@ -156,7 +149,7 @@ let p_arg oc = function | Atom a -> p_atom_constant oc a let p_instruction oc ic = - let p_args oc l= fprintf oc "%a:%a" p_jstring "Args" (p_list p_arg) l + let p_args oc l= fprintf oc "%a:%a" p_jstring "Args" (p_jarray p_arg) l and inst_name oc s = fprintf oc"%a:%a" p_jstring "Instruction Name" p_jstring s in let first = ref true in let sep oc = if !first then first := false else output_string oc ", " in @@ -385,7 +378,7 @@ let p_vardef oc (name,v) = fprintf oc "{\"Var Name\":%a,\"Var Readonly\":%B,\"Var Volatile\":%B,\n\"Var Storage Class\":%a,\n\"Var Alignment\":%a,\n\"Var Section\":%a,\n\"Var Init\":%a}\n" p_atom name v.gvar_readonly v.gvar_volatile p_storage static p_int_opt alignment p_section section - (p_list p_init_data) v.gvar_init + (p_jarray p_init_data) v.gvar_init let p_program oc prog = let prog_vars,prog_funs = List.fold_left (fun (vars,funs) (ident,def) -> @@ -394,5 +387,5 @@ let p_program oc prog = | Gvar v -> (ident,v)::vars,funs | _ -> vars,funs) ([],[]) prog.prog_defs in fprintf oc "{\"Global Variables\":%a,\n\"Functions\":%a}" - (p_list p_vardef) prog_vars - (p_list p_fundef) prog_funs + (p_jarray p_vardef) prog_vars + (p_jarray p_fundef) prog_funs -- 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/Clflagsprinter.ml | 41 -------------- driver/Driver.ml | 54 +++++++++---------- driver/Optionsprinter.ml | 96 +++++++++++++++++++++++++++++++++ lib/Json.ml | 9 ++++ powerpc/AsmToJSON.ml | 136 ++++++++++++++++++++++++----------------------- 5 files changed, 201 insertions(+), 135 deletions(-) delete mode 100644 driver/Clflagsprinter.ml create mode 100644 driver/Optionsprinter.ml diff --git a/driver/Clflagsprinter.ml b/driver/Clflagsprinter.ml deleted file mode 100644 index 11dcc818..00000000 --- a/driver/Clflagsprinter.ml +++ /dev/null @@ -1,41 +0,0 @@ -(* *********************************************************************) -(* *) -(* The Compcert verified compiler *) -(* *) -(* Bernhard Schommer, AbsInt Angewandte Informatik GmbH *) -(* *) -(* AbsInt Angewandte Informatik GmbH. All rights reserved. This file *) -(* is distributed under the terms of the INRIA Non-Commercial *) -(* License Agreement. *) -(* *) -(* *********************************************************************) - -open Clflags -open Json -open Printf - -let print_member oc name p_mem mem = - fprintf oc "\n%a:%a" p_jstring name p_mem mem - -let print_list oc name l = - print_member oc name (p_jarray p_jstring) l - -let print oc ((): unit) = - fprintf oc "{"; - print_list oc "Preprocessor Options" !prepro_options; - print_list oc "Linker Options" !linker_options; - print_list oc "Assembler Options" !assembler_options; - print_member oc "Flongdouble" p_jbool !option_flongdouble; - print_member oc "Fstruct_passing" p_jbool !option_fstruct_passing; - print_member oc "Fbitfields" p_jbool !option_fbitfields; - print_member oc "Fvarag_calls" p_jbool !option_fvararg_calls; - print_member oc "Funprototyped" p_jbool !option_funprototyped; - print_member oc "Fpacked_structs" p_jbool !option_fpacked_structs; - print_member oc "Ffpu" p_jbool !option_ffpu; - print_member oc "Ffloatconstprop" p_jint !option_ffloatconstprop; - print_member oc "Ftailcalls" p_jbool !option_ftailcalls; - print_member oc "Fconstprop" p_jbool !option_fconstprop; - print_member oc "Fcse" p_jbool !option_fcse; - print_member oc "Fredundance" p_jbool !option_fredundancy; - - fprintf oc "\n}" 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) *) diff --git a/driver/Optionsprinter.ml b/driver/Optionsprinter.ml new file mode 100644 index 00000000..0e3fa379 --- /dev/null +++ b/driver/Optionsprinter.ml @@ -0,0 +1,96 @@ +(* *********************************************************************) +(* *) +(* The Compcert verified compiler *) +(* *) +(* Bernhard Schommer, AbsInt Angewandte Informatik GmbH *) +(* *) +(* AbsInt Angewandte Informatik GmbH. All rights reserved. This file *) +(* is distributed under the terms of the INRIA Non-Commercial *) +(* License Agreement. *) +(* *) +(* *********************************************************************) + +open Clflags +open Json +open Printf + +let print_list oc name l = + p_jmember oc name (p_jarray p_jstring) l + +let print_clflags oc ((): unit) = + fprintf oc "{"; + print_list oc "prepro_options" !prepro_options; + print_list oc "linker_options" !linker_options; + print_list oc "assembler_options" !assembler_options; + p_jmember oc "flongdouble" p_jbool !option_flongdouble; + p_jmember oc "fstruct_passing" p_jbool !option_fstruct_passing; + p_jmember oc "fbitfields" p_jbool !option_fbitfields; + p_jmember oc "fvarag_calls" p_jbool !option_fvararg_calls; + p_jmember oc "funprototyped" p_jbool !option_funprototyped; + p_jmember oc "fpacked_structs" p_jbool !option_fpacked_structs; + p_jmember oc "ffpu" p_jbool !option_ffpu; + p_jmember oc "ffloatconstprop" p_jint !option_ffloatconstprop; + p_jmember oc "ftailcalls" p_jbool !option_ftailcalls; + p_jmember oc "fconstprop" p_jbool !option_fconstprop; + p_jmember oc "fcse" p_jbool !option_fcse; + p_jmember oc "fredundance" p_jbool !option_fredundancy; + p_jmember oc "falignfunctions" (p_jopt p_jint) !option_falignfunctions; + p_jmember oc "falignbranchtargets" p_jint !option_falignbranchtargets; + p_jmember oc "faligncondbranchs" p_jint !option_faligncondbranchs; + p_jmember oc "finline_asm" p_jbool !option_finline_asm; + p_jmember oc "mthumb" p_jbool !option_mthumb; + p_jmember oc "Osize" p_jbool !option_Osize; + p_jmember oc "dprepro" p_jbool !option_dprepro; + p_jmember oc "dparse" p_jbool !option_dparse; + p_jmember oc "dcmedium" p_jbool !option_dcmedium; + p_jmember oc "dclight" p_jbool !option_dclight; + p_jmember oc "dcminor" p_jbool !option_dcminor; + p_jmember oc "drtl" p_jbool !option_drtl; + p_jmember oc "dltl" p_jbool !option_dltl; + p_jmember oc "dalloctrace" p_jbool !option_dalloctrace; + p_jmember oc "dmach" p_jbool !option_dmach; + p_jmember oc "dasm" p_jbool !option_dasm; + p_jmember oc "sdump" p_jbool !option_sdump; + p_jmember oc "g" p_jbool !option_g; + p_jmember oc "gdwarf" p_jint !option_gdwarf; + p_jmember oc "gdepth" p_jint !option_gdepth; + p_jmember oc "o" (p_jopt p_jstring) !option_o; + p_jmember oc "E" p_jbool !option_E; + p_jmember oc "S" p_jbool !option_S; + p_jmember oc "c" p_jbool !option_c; + p_jmember oc "v" p_jbool !option_v; + p_jmember oc "interp" p_jbool !option_interp; + p_jmember oc "small_data" p_jint !option_small_data; + p_jmember oc "small_data" p_jint !option_small_const; + p_jmember oc "timings" p_jbool !option_timings; + p_jmember oc "rename_static" p_jbool !option_rename_static; + fprintf oc "\n}" + +let print_struct_passing_style oc = function + | Configuration.SP_ref_callee -> p_jstring oc "SP_ref_callee" + | Configuration.SP_ref_caller -> p_jstring oc "SP_ref_caller" + | Configuration.SP_split_args -> p_jstring oc "SP_split_args" + +let print_struct_return_style oc = function + | Configuration.SR_int1248 -> p_jstring oc "SR_int1248" + | Configuration.SR_int1to4 -> p_jstring oc "SR_int1to4" + | Configuration.SR_int1to8 -> p_jstring oc "SR_int1to8" + | Configuration.SR_ref -> p_jstring oc "SR_ref" + +let print_configurations oc lib_path = + fprintf oc "{"; + p_jmember oc "arch" p_jstring Configuration.arch; + p_jmember oc "model" p_jstring Configuration.model; + p_jmember oc "abi" p_jstring Configuration.abi; + p_jmember oc "system" p_jstring Configuration.abi; + print_list oc "prepro" Configuration.prepro; + print_list oc "asm" Configuration.asm; + print_list oc "linker" Configuration.linker; + p_jmember oc "asm_supports_cfi" p_jbool Configuration.asm_supports_cfi; + p_jmember oc "stdlib_path" p_jstring lib_path; + p_jmember oc "has_runtime_lib" p_jbool Configuration.has_runtime_lib; + p_jmember oc "has_standard_headers" p_jbool Configuration.has_standard_headers; + p_jmember oc "advanced_debug" p_jbool Configuration.advanced_debug; + 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}" diff --git a/lib/Json.ml b/lib/Json.ml index db2de5d4..4aa91e95 100644 --- a/lib/Json.ml +++ b/lib/Json.ml @@ -31,3 +31,12 @@ let p_jbool oc = fprintf oc "%B" (* Print a int as json int *) let p_jint oc = fprintf oc "%d" + +(* Print a member *) +let p_jmember oc name p_mem mem = + fprintf oc "\n%a:%a" p_jstring name p_mem mem + +(* Print optional value *) +let p_jopt p_elem oc = function + | None -> output_string oc "null" + | Some i -> p_elem oc i diff --git a/powerpc/AsmToJSON.ml b/powerpc/AsmToJSON.ml index 4ca7dbde..4f6a1864 100644 --- a/powerpc/AsmToJSON.ml +++ b/powerpc/AsmToJSON.ml @@ -21,73 +21,77 @@ open Json open Printf open Sections -let p_ireg oc = function - | GPR0 -> fprintf oc "{\"Register\":\"r0\"}" - | GPR1 -> fprintf oc "{\"Register\":\"r1\"}" - | GPR2 -> fprintf oc "{\"Register\":\"r2\"}" - | GPR3 -> fprintf oc "{\"Register\":\"r3\"}" - | GPR4 -> fprintf oc "{\"Register\":\"r4\"}" - | GPR5 -> fprintf oc "{\"Register\":\"r5\"}" - | GPR6 -> fprintf oc "{\"Register\":\"r6\"}" - | GPR7 -> fprintf oc "{\"Register\":\"r7\"}" - | GPR8 -> fprintf oc "{\"Register\":\"r8\"}" - | GPR9 -> fprintf oc "{\"Register\":\"r9\"}" - | GPR10 -> fprintf oc "{\"Register\":\"r10\"}" - | GPR11 -> fprintf oc "{\"Register\":\"r11\"}" - | GPR12 -> fprintf oc "{\"Register\":\"r12\"}" - | GPR13 -> fprintf oc "{\"Register\":\"r13\"}" - | GPR14 -> fprintf oc "{\"Register\":\"r14\"}" - | GPR15 -> fprintf oc "{\"Register\":\"r15\"}" - | GPR16 -> fprintf oc "{\"Register\":\"r16\"}" - | GPR17 -> fprintf oc "{\"Register\":\"r17\"}" - | GPR18 -> fprintf oc "{\"Register\":\"r18\"}" - | GPR19 -> fprintf oc "{\"Register\":\"r19\"}" - | GPR20 -> fprintf oc "{\"Register\":\"r20\"}" - | GPR21 -> fprintf oc "{\"Register\":\"r21\"}" - | GPR22 -> fprintf oc "{\"Register\":\"r22\"}" - | GPR23 -> fprintf oc "{\"Register\":\"r23\"}" - | GPR24 -> fprintf oc "{\"Register\":\"r24\"}" - | GPR25 -> fprintf oc "{\"Register\":\"r25\"}" - | GPR26 -> fprintf oc "{\"Register\":\"r26\"}" - | GPR27 -> fprintf oc "{\"Register\":\"r27\"}" - | GPR28 -> fprintf oc "{\"Register\":\"r28\"}" - | GPR29 -> fprintf oc "{\"Register\":\"r29\"}" - | GPR30 -> fprintf oc "{\"Register\":\"r30\"}" - | GPR31 -> fprintf oc "{\"Register\":\"r31\"}" +let p_ireg oc reg = + let num = match reg with + | GPR0 -> 0 + | GPR1 -> 1 + | GPR2 -> 2 + | GPR3 -> 3 + | GPR4 -> 4 + | GPR5 -> 5 + | GPR6 -> 6 + | GPR7 -> 7 + | GPR8 -> 8 + | GPR9 -> 9 + | GPR10 -> 10 + | GPR11 -> 11 + | GPR12 -> 12 + | GPR13 -> 13 + | GPR14 -> 14 + | GPR15 -> 15 + | GPR16 -> 16 + | GPR17 -> 17 + | GPR18 -> 18 + | GPR19 -> 19 + | GPR20 -> 20 + | GPR21 -> 21 + | GPR22 -> 22 + | GPR23 -> 23 + | GPR24 -> 24 + | GPR25 -> 25 + | GPR26 -> 26 + | GPR27 -> 27 + | GPR28 -> 28 + | GPR29 -> 29 + | GPR30 -> 30 + | GPR31 -> 31 + in p_jmember oc "Register" (fun oc -> fprintf oc "r%d") num -let p_freg oc = function - | FPR0 -> fprintf oc "{\"Register\":\"f0\"}" - | FPR1 -> fprintf oc "{\"Register\":\"f1\"}" - | FPR2 -> fprintf oc "{\"Register\":\"f2\"}" - | FPR3 -> fprintf oc "{\"Register\":\"f3\"}" - | FPR4 -> fprintf oc "{\"Register\":\"f4\"}" - | FPR5 -> fprintf oc "{\"Register\":\"f5\"}" - | FPR6 -> fprintf oc "{\"Register\":\"f6\"}" - | FPR7 -> fprintf oc "{\"Register\":\"f7\"}" - | FPR8 -> fprintf oc "{\"Register\":\"f8\"}" - | FPR9 -> fprintf oc "{\"Register\":\"f9\"}" - | FPR10 -> fprintf oc "{\"Register\":\"f10\"}" - | FPR11 -> fprintf oc "{\"Register\":\"f11\"}" - | FPR12 -> fprintf oc "{\"Register\":\"f12\"}" - | FPR13 -> fprintf oc "{\"Register\":\"f13\"}" - | FPR14 -> fprintf oc "{\"Register\":\"f14\"}" - | FPR15 -> fprintf oc "{\"Register\":\"f15\"}" - | FPR16 -> fprintf oc "{\"Register\":\"f16\"}" - | FPR17 -> fprintf oc "{\"Register\":\"f17\"}" - | FPR18 -> fprintf oc "{\"Register\":\"f18\"}" - | FPR19 -> fprintf oc "{\"Register\":\"f19\"}" - | FPR20 -> fprintf oc "{\"Register\":\"f20\"}" - | FPR21 -> fprintf oc "{\"Register\":\"f21\"}" - | FPR22 -> fprintf oc "{\"Register\":\"f22\"}" - | FPR23 -> fprintf oc "{\"Register\":\"f23\"}" - | FPR24 -> fprintf oc "{\"Register\":\"f24\"}" - | FPR25 -> fprintf oc "{\"Register\":\"f25\"}" - | FPR26 -> fprintf oc "{\"Register\":\"f26\"}" - | FPR27 -> fprintf oc "{\"Register\":\"f27\"}" - | FPR28 -> fprintf oc "{\"Register\":\"f28\"}" - | FPR29 -> fprintf oc "{\"Register\":\"f29\"}" - | FPR30 -> fprintf oc "{\"Register\":\"f30\"}" - | FPR31 -> fprintf oc "{\"Register\":\"f31\"}" +let p_freg oc reg = + let num = match reg with + | FPR0 -> 0 + | FPR1 -> 1 + | FPR2 -> 2 + | FPR3 -> 3 + | FPR4 -> 4 + | FPR5 -> 5 + | FPR6 -> 6 + | FPR7 -> 7 + | FPR8 -> 8 + | FPR9 -> 9 + | FPR10 -> 10 + | FPR11 -> 11 + | FPR12 -> 12 + | FPR13 -> 13 + | FPR14 -> 14 + | FPR15 -> 15 + | FPR16 -> 16 + | FPR17 -> 17 + | FPR18 -> 18 + | FPR19 -> 19 + | FPR20 -> 20 + | FPR21 -> 21 + | FPR22 -> 22 + | FPR23 -> 23 + | FPR24 -> 24 + | FPR25 -> 25 + | FPR26 -> 26 + | FPR27 -> 27 + | FPR28 -> 28 + | FPR29 -> 29 + | FPR30 -> 30 + | FPR31 -> 31 + in p_jmember oc "Register" (fun oc -> fprintf oc "f%d") num let p_preg oc = function | IR ir -> p_ireg oc ir -- 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 ++++++++++++++--- 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 .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 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 -- cgit From 659a1b55f454fc262826e4edf7d938f01ae04263 Mon Sep 17 00:00:00 2001 From: Bernhard Schommer Date: Wed, 27 Jan 2016 09:31:45 +0100 Subject: Added version and compiler working directory to options dump. --- driver/Optionsprinter.ml | 4 ++++ 1 file changed, 4 insertions(+) diff --git a/driver/Optionsprinter.ml b/driver/Optionsprinter.ml index 6302f210..f046b40a 100644 --- a/driver/Optionsprinter.ml +++ b/driver/Optionsprinter.ml @@ -132,6 +132,10 @@ let print_machine oc = let print file stdlib = let oc = open_out file in fprintf oc "{"; + p_jmember oc "Version" p_jstring Version.version; + p_jmember oc "Buildnr" p_jstring Version.buildnr; + p_jmember oc "Tag" p_jstring Version.tag; + p_jmember oc "Cwd" p_jstring (Sys.getcwd ()); 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; -- cgit