diff options
Diffstat (limited to 'backend')
-rw-r--r-- | backend/PrintAsm.ml | 4 | ||||
-rw-r--r-- | backend/PrintAsmaux.ml | 71 |
2 files changed, 73 insertions, 2 deletions
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]*" |