diff options
author | Bernhard Schommer <bernhardschommer@gmail.com> | 2015-09-06 20:32:55 +0200 |
---|---|---|
committer | Bernhard Schommer <bernhardschommer@gmail.com> | 2015-09-06 20:32:55 +0200 |
commit | 861292a6c5e58b4f78bef207c717b801b3fc1fed (patch) | |
tree | 970be0db2fb62e66b09c4fb90b2e750c255565e0 | |
parent | dba05a9f6259c82a350987b511bf1a71f113d0ba (diff) | |
download | compcert-861292a6c5e58b4f78bef207c717b801b3fc1fed.tar.gz compcert-861292a6c5e58b4f78bef207c717b801b3fc1fed.zip |
Startet implementation of new Debug interface.
Added a new file debug/Debug.ml which will be the interface between for
generating and printing the debuging information. Currently it contains
only the code for the line directived.
-rw-r--r-- | arm/TargetPrinter.ml | 1 | ||||
-rw-r--r-- | backend/PrintAsm.ml | 4 | ||||
-rw-r--r-- | backend/PrintAsmaux.ml | 71 | ||||
-rw-r--r-- | debug/CtoDwarf.ml | 2 | ||||
-rw-r--r-- | debug/Debug.ml | 86 | ||||
-rw-r--r-- | debug/DwarfPrinter.mli | 1 | ||||
-rw-r--r-- | ia32/TargetPrinter.ml | 1 | ||||
-rw-r--r-- | powerpc/TargetPrinter.ml | 5 |
8 files changed, 95 insertions, 76 deletions
diff --git a/arm/TargetPrinter.ml b/arm/TargetPrinter.ml index 028ff6ed..d0e07958 100644 --- a/arm/TargetPrinter.ml +++ b/arm/TargetPrinter.ml @@ -20,6 +20,7 @@ open AST open Memdata open Asm open PrintAsmaux +open Debug (* Type for the ABI versions *) type float_abi_type = diff --git a/backend/PrintAsm.ml b/backend/PrintAsm.ml index 29409b32..b88a3d50 100644 --- a/backend/PrintAsm.ml +++ b/backend/PrintAsm.ml @@ -134,12 +134,12 @@ module Printer(Target:TARGET) = let print_program oc p db = let module Target = (val (sel_target ()):TARGET) in let module Printer = Printer(Target) in - reset_filenames (); + Debug.reset_filenames (); print_version_and_options oc Target.comment; Target.print_prologue oc; List.iter (Printer.print_globdef oc) p.prog_defs; Target.print_epilogue oc; - close_filenames (); + Debug.close_filenames (); if !Clflags.option_g && Configuration.advanced_debug then begin match db with diff --git a/backend/PrintAsmaux.ml b/backend/PrintAsmaux.ml index 324e7e66..441f8251 100644 --- a/backend/PrintAsmaux.ml +++ b/backend/PrintAsmaux.ml @@ -142,77 +142,6 @@ let cfi_rel_offset = let coqint oc n = fprintf oc "%ld" (camlint_of_coqint n) -(* Printing annotations in asm syntax *) -(** All files used in the debug entries *) -module StringSet = Set.Make(String) -let all_files : StringSet.t ref = ref StringSet.empty -let add_file file = - all_files := StringSet.add file !all_files - - -let filename_info : (string, int * Printlines.filebuf option) Hashtbl.t - = Hashtbl.create 7 - -let last_file = ref "" - -let reset_filenames () = - Hashtbl.clear filename_info; last_file := "" - -let close_filenames () = - Hashtbl.iter - (fun file (num, fb) -> - match fb with Some b -> Printlines.close b | None -> ()) - filename_info; - reset_filenames() - -let enter_filename f = - let num = Hashtbl.length filename_info + 1 in - let filebuf = - if !Clflags.option_S || !Clflags.option_dasm then begin - try Some (Printlines.openfile f) - with Sys_error _ -> None - end else None in - Hashtbl.add filename_info f (num, filebuf); - (num, filebuf) - -(* Add file and line debug location, using GNU assembler-style DWARF2 - directives *) - -let print_file_line oc pref file line = - if !Clflags.option_g && file <> "" then begin - let (filenum, filebuf) = - try - Hashtbl.find filename_info file - with Not_found -> - let (filenum, filebuf as res) = enter_filename file in - fprintf oc " .file %d %S\n" filenum file; - res in - fprintf oc " .loc %d %d\n" filenum line; - match filebuf with - | None -> () - | Some fb -> Printlines.copy oc pref fb line line - end - -(* Add file and line debug location, using DWARF2 directives in the style - of Diab C 5 *) - -let print_file_line_d2 oc pref file line = - if !Clflags.option_g && file <> "" then begin - let (_, filebuf) = - try - Hashtbl.find filename_info file - with Not_found -> - enter_filename file in - if file <> !last_file then begin - fprintf oc " .d2file %S\n" file; - last_file := file - end; - fprintf oc " .d2line %d\n" line; - match filebuf with - | None -> () - | Some fb -> Printlines.copy oc pref fb line line - end - (** Programmer-supplied annotations (__builtin_annot). *) let re_annot_param = Str.regexp "%%\\|%[1-9][0-9]*" diff --git a/debug/CtoDwarf.ml b/debug/CtoDwarf.ml index 063b0823..e37c6043 100644 --- a/debug/CtoDwarf.ml +++ b/debug/CtoDwarf.ml @@ -477,7 +477,7 @@ let union_to_dwarf (n,at,m) env gloc = (* Translate global declarations to there dwarf representation *) let globdecl_to_dwarf env (typs,decls) decl = - PrintAsmaux.add_file (fst decl.gloc); + Debug.add_file (fst decl.gloc); match decl.gdesc with | Gtypedef (n,t) -> let ret = typedef_to_dwarf (Some decl.gloc) (n.name,t) in typs@ret,decls diff --git a/debug/Debug.ml b/debug/Debug.ml new file mode 100644 index 00000000..dfe7fd94 --- /dev/null +++ b/debug/Debug.ml @@ -0,0 +1,86 @@ +(* *********************************************************************) +(* *) +(* The Compcert verified compiler *) +(* *) +(* Xavier Leroy, INRIA Paris-Rocquencourt *) +(* Bernhard Schommer, AbsInt Angewandte Informatik GmbH *) +(* *) +(* Copyright Institut National de Recherche en Informatique et en *) +(* Automatique. All rights reserved. This file is distributed *) +(* under the terms of the INRIA Non-Commercial License Agreement. *) +(* *) +(* *********************************************************************) + +open Printf + +(* Printing annotations in asm syntax *) +(** All files used in the debug entries *) +module StringSet = Set.Make(String) +let all_files : StringSet.t ref = ref StringSet.empty +let add_file file = + all_files := StringSet.add file !all_files + + +let filename_info : (string, int * Printlines.filebuf option) Hashtbl.t + = Hashtbl.create 7 + +let last_file = ref "" + +let reset_filenames () = + Hashtbl.clear filename_info; last_file := "" + +let close_filenames () = + Hashtbl.iter + (fun file (num, fb) -> + match fb with Some b -> Printlines.close b | None -> ()) + filename_info; + reset_filenames() + +let enter_filename f = + let num = Hashtbl.length filename_info + 1 in + let filebuf = + if !Clflags.option_S || !Clflags.option_dasm then begin + try Some (Printlines.openfile f) + with Sys_error _ -> None + end else None in + Hashtbl.add filename_info f (num, filebuf); + (num, filebuf) + + +(* Add file and line debug location, using GNU assembler-style DWARF2 + directives *) + +let print_file_line oc pref file line = + if !Clflags.option_g && file <> "" then begin + let (filenum, filebuf) = + try + Hashtbl.find filename_info file + with Not_found -> + let (filenum, filebuf as res) = enter_filename file in + fprintf oc " .file %d %S\n" filenum file; + res in + fprintf oc " .loc %d %d\n" filenum line; + match filebuf with + | None -> () + | Some fb -> Printlines.copy oc pref fb line line + end + +(* Add file and line debug location, using DWARF2 directives in the style + of Diab C 5 *) + +let print_file_line_d2 oc pref file line = + if !Clflags.option_g && file <> "" then begin + let (_, filebuf) = + try + Hashtbl.find filename_info file + with Not_found -> + enter_filename file in + if file <> !last_file then begin + fprintf oc " .d2file %S\n" file; + last_file := file + end; + fprintf oc " .d2line %d\n" line; + match filebuf with + | None -> () + | Some fb -> Printlines.copy oc pref fb line line + end diff --git a/debug/DwarfPrinter.mli b/debug/DwarfPrinter.mli index 9e0e6693..ccdecffb 100644 --- a/debug/DwarfPrinter.mli +++ b/debug/DwarfPrinter.mli @@ -1,3 +1,4 @@ + (* *********************************************************************) (* *) (* The Compcert verified compiler *) diff --git a/ia32/TargetPrinter.ml b/ia32/TargetPrinter.ml index d1e213e2..9227929b 100644 --- a/ia32/TargetPrinter.ml +++ b/ia32/TargetPrinter.ml @@ -20,6 +20,7 @@ open AST open Memdata open Asm open PrintAsmaux +open Debug module StringSet = Set.Make(String) diff --git a/powerpc/TargetPrinter.ml b/powerpc/TargetPrinter.ml index 409f2cc0..5159850d 100644 --- a/powerpc/TargetPrinter.ml +++ b/powerpc/TargetPrinter.ml @@ -21,6 +21,7 @@ open AST open Memdata open Asm open PrintAsmaux +open Debug (* Recognition of target ABI and asm syntax *) @@ -139,7 +140,7 @@ module Linux_System : SYSTEM = let print_file_line oc file line = - print_file_line oc comment file line + Debug.print_file_line oc comment file line (* Emit .cfi directives *) let cfi_startproc = cfi_startproc @@ -217,7 +218,7 @@ module Diab_System : SYSTEM = let print_file_line oc file line = - print_file_line_d2 oc comment file line + Debug.print_file_line_d2 oc comment file line (* Emit .cfi directives *) let cfi_startproc oc = () |