From e62820c430e52fa72edd6f1c21bd867eb0f3c467 Mon Sep 17 00:00:00 2001 From: Bernhard Schommer Date: Tue, 2 Dec 2014 17:22:49 +0100 Subject: Renamed the printer module for the Abbreviations and deactivated adding the -g option to the assembler. --- driver/Driver.ml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'driver') diff --git a/driver/Driver.ml b/driver/Driver.ml index fec87420..6ba30d74 100644 --- a/driver/Driver.ml +++ b/driver/Driver.ml @@ -499,7 +499,7 @@ let cmdline_actions = Exact "-fall", Self (fun _ -> set_all language_support_options); Exact "-fnone", Self (fun _ -> unset_all language_support_options); (* Debugging options *) - Exact "-g", Self (fun s -> option_g := true; push_linker_arg s); + Exact "-g", Self (fun s -> option_g := true); (* Code generation options -- more below *) Exact "-O0", Self (fun _ -> unset_all optimization_options); Exact "-O", Self (fun _ -> set_all optimization_options); -- cgit From b3c67667b7121b7f2e50700ec6da4bd780dee426 Mon Sep 17 00:00:00 2001 From: Bernhard Schommer Date: Mon, 16 Mar 2015 12:23:29 +0100 Subject: Started implementing the printing functions for the debug info. Added a global target dependend option to activate the printing only for targets wher it works. --- driver/Configuration.ml | 6 ++++++ 1 file changed, 6 insertions(+) (limited to 'driver') diff --git a/driver/Configuration.ml b/driver/Configuration.ml index 0012dc0c..48c31767 100644 --- a/driver/Configuration.ml +++ b/driver/Configuration.ml @@ -93,4 +93,10 @@ let asm_supports_cfi = | "false" -> false | v -> bad_config "asm_supports_cfi" [v] +let advanced_debug = + match get_config_string "advanced_debug" with + | "true" -> true + | "false" -> false + | v -> bad_config "advanced_debug" [v] + let version = get_config_string "version" -- cgit From f750e0ac9ee99072cca8361f591015f1f82681fa Mon Sep 17 00:00:00 2001 From: Bernhard Schommer Date: Wed, 18 Mar 2015 18:36:09 +0100 Subject: Added function to convert C types into their dwarf represnation. --- driver/Driver.ml | 5 +++-- 1 file changed, 3 insertions(+), 2 deletions(-) (limited to 'driver') diff --git a/driver/Driver.ml b/driver/Driver.ml index d8b28285..f14b2671 100644 --- a/driver/Driver.ml +++ b/driver/Driver.ml @@ -15,6 +15,7 @@ open Commandline open Camlcoq open Clflags open Timing +open CtoDwarf (* Location of the compatibility library *) @@ -181,7 +182,7 @@ let compile_c_ast sourcename csyntax ofile = dump_asm asm (output_filename sourcename ".c" ".sdump"); (* Print Asm in text form *) let oc = open_out ofile in - PrintAsm.print_program oc asm; + PrintAsm.print_program oc asm None; close_out oc (* From C source to asm *) @@ -212,7 +213,7 @@ let compile_cminor_file ifile ofile = exit 2 | Errors.OK p -> let oc = open_out ofile in - PrintAsm.print_program oc p; + PrintAsm.print_program oc p None; close_out oc with Parsing.Parse_error -> eprintf "File %s, character %d: Syntax error\n" -- cgit From 253e8e9b72a1204f334460af0ffc7893d3e4b752 Mon Sep 17 00:00:00 2001 From: Bernhard Schommer Date: Thu, 19 Mar 2015 11:18:10 +0100 Subject: Activating the printing of the debug information for supported architecture. --- driver/Driver.ml | 16 ++++++++++------ 1 file changed, 10 insertions(+), 6 deletions(-) (limited to 'driver') diff --git a/driver/Driver.ml b/driver/Driver.ml index f14b2671..80a5891c 100644 --- a/driver/Driver.ml +++ b/driver/Driver.ml @@ -129,6 +129,9 @@ let parse_c_file sourcename ifile = Cprint.program (Format.formatter_of_out_channel oc) ast; close_out oc end; + let debug = if !option_g && Configuration.advanced_debug then + Some (program_to_dwarf ast sourcename) + else None in (* Conversion to Csyntax *) let csyntax = match Timing.time "CompCert C generation" C2C.convertProgram ast with @@ -142,7 +145,7 @@ let parse_c_file sourcename ifile = PrintCsyntax.print_program (Format.formatter_of_out_channel oc) csyntax; close_out oc end; - csyntax + csyntax,debug (* Dump Asm code in binary format for the validator *) @@ -158,7 +161,7 @@ let dump_asm asm destfile = (* From CompCert C AST to asm *) -let compile_c_ast sourcename csyntax ofile = +let compile_c_ast sourcename csyntax ofile debug = (* Prepare to dump Clight, RTL, etc, if requested *) let set_dest dst opt ext = dst := if !opt then Some (output_filename sourcename ".c" ext) @@ -182,13 +185,14 @@ let compile_c_ast sourcename csyntax ofile = dump_asm asm (output_filename sourcename ".c" ".sdump"); (* Print Asm in text form *) let oc = open_out ofile in - PrintAsm.print_program oc asm None; + PrintAsm.print_program oc asm debug; close_out oc (* From C source to asm *) let compile_c_file sourcename ifile ofile = - compile_c_ast sourcename (parse_c_file sourcename ifile) ofile + let ast,debug = parse_c_file sourcename ifile in + compile_c_ast sourcename ast ofile debug (* From Cminor to asm *) @@ -266,7 +270,7 @@ let process_c_file sourcename = let preproname = Filename.temp_file "compcert" ".i" in preprocess sourcename preproname; if !option_interp then begin - let csyntax = parse_c_file sourcename preproname in + let csyntax,_ = parse_c_file sourcename preproname in safe_remove preproname; Interp.execute csyntax; "" @@ -293,7 +297,7 @@ let process_c_file sourcename = let process_i_file sourcename = if !option_interp then begin - let csyntax = parse_c_file sourcename sourcename in + let csyntax,_ = parse_c_file sourcename sourcename in Interp.execute csyntax; "" end else if !option_S then begin -- cgit From 2ebf8bfda476966209d681470ebe6301fb10db0a Mon Sep 17 00:00:00 2001 From: Bernhard Schommer Date: Tue, 24 Mar 2015 16:07:45 +0100 Subject: Added missing functions for printing the structs and unions. Still missing printing of packed structs. --- driver/Driver.ml | 12 ++++-------- 1 file changed, 4 insertions(+), 8 deletions(-) (limited to 'driver') diff --git a/driver/Driver.ml b/driver/Driver.ml index 80a5891c..1191982d 100644 --- a/driver/Driver.ml +++ b/driver/Driver.ml @@ -15,7 +15,6 @@ open Commandline open Camlcoq open Clflags open Timing -open CtoDwarf (* Location of the compatibility library *) @@ -118,20 +117,17 @@ let parse_c_file sourcename ifile = ^ (if !option_fpacked_structs then "p" else "") in (* Parsing and production of a simplified C AST *) - let ast = + let ast,debug = match Parse.preprocessed_file simplifs sourcename ifile with - | None -> exit 2 - | Some p -> p in + | None,_ -> exit 2 + | Some p,d -> p,d in (* Save C AST if requested *) if !option_dparse then begin let ofile = output_filename sourcename ".c" ".parsed.c" in let oc = open_out ofile in Cprint.program (Format.formatter_of_out_channel oc) ast; close_out oc - end; - let debug = if !option_g && Configuration.advanced_debug then - Some (program_to_dwarf ast sourcename) - else None in + end; (* Conversion to Csyntax *) let csyntax = match Timing.time "CompCert C generation" C2C.convertProgram ast with -- cgit