diff options
-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, 76 insertions, 95 deletions
diff --git a/arm/TargetPrinter.ml b/arm/TargetPrinter.ml index d0e07958..028ff6ed 100644 --- a/arm/TargetPrinter.ml +++ b/arm/TargetPrinter.ml @@ -20,7 +20,6 @@ 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 b88a3d50..29409b32 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 - Debug.reset_filenames (); + 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; - Debug.close_filenames (); + 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 441f8251..324e7e66 100644 --- a/backend/PrintAsmaux.ml +++ b/backend/PrintAsmaux.ml @@ -142,6 +142,77 @@ 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 e37c6043..063b0823 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 = - Debug.add_file (fst decl.gloc); + PrintAsmaux.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 deleted file mode 100644 index dfe7fd94..00000000 --- a/debug/Debug.ml +++ /dev/null @@ -1,86 +0,0 @@ -(* *********************************************************************) -(* *) -(* 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 ccdecffb..9e0e6693 100644 --- a/debug/DwarfPrinter.mli +++ b/debug/DwarfPrinter.mli @@ -1,4 +1,3 @@ - (* *********************************************************************) (* *) (* The Compcert verified compiler *) diff --git a/ia32/TargetPrinter.ml b/ia32/TargetPrinter.ml index 9227929b..d1e213e2 100644 --- a/ia32/TargetPrinter.ml +++ b/ia32/TargetPrinter.ml @@ -20,7 +20,6 @@ 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 5159850d..409f2cc0 100644 --- a/powerpc/TargetPrinter.ml +++ b/powerpc/TargetPrinter.ml @@ -21,7 +21,6 @@ open AST open Memdata open Asm open PrintAsmaux -open Debug (* Recognition of target ABI and asm syntax *) @@ -140,7 +139,7 @@ module Linux_System : SYSTEM = let print_file_line oc file line = - Debug.print_file_line oc comment file line + print_file_line oc comment file line (* Emit .cfi directives *) let cfi_startproc = cfi_startproc @@ -218,7 +217,7 @@ module Diab_System : SYSTEM = let print_file_line oc file line = - Debug.print_file_line_d2 oc comment file line + print_file_line_d2 oc comment file line (* Emit .cfi directives *) let cfi_startproc oc = () |