diff options
-rw-r--r-- | arm/PrintAsm.ml | 35 | ||||
-rw-r--r-- | backend/PrintAnnot.ml | 67 | ||||
-rw-r--r-- | ia32/PrintAsm.ml | 31 | ||||
-rw-r--r-- | lib/Printlines.ml | 111 | ||||
-rw-r--r-- | lib/Printlines.mli | 28 | ||||
-rw-r--r-- | powerpc/PrintAsm.ml | 57 |
6 files changed, 243 insertions, 86 deletions
diff --git a/arm/PrintAsm.ml b/arm/PrintAsm.ml index c7157aac..7f511912 100644 --- a/arm/PrintAsm.ml +++ b/arm/PrintAsm.ml @@ -35,7 +35,6 @@ module type PRINTER_OPTIONS = val cfi_endproc: out_channel -> unit val cfi_adjust: out_channel -> int32 -> unit val cfi_rel_offset: out_channel -> string -> int32 -> unit - val thumb: bool end (* Module containing the printing functions *) @@ -162,7 +161,7 @@ let neg_condition_name = function mode. *) let thumbS oc = - if Opt.thumb then output_char oc 's' + if !Clflags.option_mthumb then output_char oc 's' (* Names of sections *) @@ -322,24 +321,11 @@ let is_immediate_float32 bits = (* Emit .file / .loc debugging directives *) -let filename_num : (string, int) Hashtbl.t = Hashtbl.create 7 - let print_file_line oc file line = - if !Clflags.option_g && file <> "" then begin - let filenum = - try - Hashtbl.find filename_num file - with Not_found -> - let n = Hashtbl.length filename_num + 1 in - Hashtbl.add filename_num file n; - fprintf oc " .file %d %S\n" n file; - n - in fprintf oc " .loc %d %s\n" filenum line - end + PrintAnnot.print_file_line oc comment file line let print_location oc loc = - if loc <> Cutil.no_loc then - print_file_line oc (fst loc) (string_of_int (snd loc)) + if loc <> Cutil.no_loc then print_file_line oc (fst loc) (snd loc) (* Built-ins. They come in two flavors: - annotation statements: take their arguments in registers or stack @@ -354,7 +340,8 @@ let re_file_line = Str.regexp "#line:\\(.*\\):\\([1-9][0-9]*\\)$" let print_annot_stmt oc txt targs args = if Str.string_match re_file_line txt 0 then begin - print_file_line oc (Str.matched_group 1 txt) (Str.matched_group 2 txt) + print_file_line oc (Str.matched_group 1 txt) + (int_of_string (Str.matched_group 2 txt)) end else begin fprintf oc "%s annotation: " comment; PrintAnnot.print_annot_stmt preg "sp" oc txt targs args @@ -1189,7 +1176,7 @@ let print_globdef oc (name, gdef) = end) let print_program oc p = - let module Opt = (struct + let module Opt : PRINTER_OPTIONS = struct let vfpv3 = Configuration.model >= "armv7" @@ -1229,12 +1216,10 @@ let print_program oc p = else (fun _ _ _ -> ()) - let thumb = !Clflags.option_mthumb - - end: PRINTER_OPTIONS) in + end in let module Printer = AsmPrinter(Opt) in + PrintAnnot.reset_filenames(); PrintAnnot.print_version_and_options oc Printer.comment; - Hashtbl.clear Printer.filename_num; fprintf oc " .syntax unified\n"; fprintf oc " .arch %s\n" (match Configuration.model with @@ -1246,6 +1231,6 @@ let print_program oc p = fprintf oc " .fpu %s\n" (if Opt.vfpv3 then "vfpv3-d16" else "vfpv2"); fprintf oc " .%s\n" (if !Clflags.option_mthumb then "thumb" else "arm"); - List.iter (Printer.print_globdef oc) p.prog_defs - + List.iter (Printer.print_globdef oc) p.prog_defs; + PrintAnnot.close_filenames() diff --git a/backend/PrintAnnot.ml b/backend/PrintAnnot.ml index d24635a6..54174b9f 100644 --- a/backend/PrintAnnot.ml +++ b/backend/PrintAnnot.ml @@ -21,6 +21,73 @@ open AST open Memdata open Asm +(** Line number annotations *) + +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 DWARF1 directives in the style + of Diab C 5 *) + +let print_file_line_d1 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 " .d1file %S\n" file; + last_file := file + end; + fprintf oc " .d1line %d\n" line; + match filebuf with + | None -> () + | Some fb -> Printlines.copy oc pref fb line line + end + +(** "True" annotations *) + let re_annot_param = Str.regexp "%%\\|%[1-9][0-9]*" type arg_value = diff --git a/ia32/PrintAsm.ml b/ia32/PrintAsm.ml index 649fd292..b0ef0180 100644 --- a/ia32/PrintAsm.ml +++ b/ia32/PrintAsm.ml @@ -264,8 +264,7 @@ let transl_label lbl = Hashtbl.add current_function_labels lbl lbl'; lbl' - -(* basic printing functions *) +(* Basic printing functions *) let comment = "#" @@ -308,6 +307,7 @@ let name_of_neg_condition = function (* Names of sections *) + let section oc sec = fprintf oc " %s\n" (name_of_section sec) @@ -338,24 +338,11 @@ let need_masks = ref false (* Emit .file / .loc debugging directives *) -let filename_num : (string, int) Hashtbl.t = Hashtbl.create 7 - let print_file_line oc file line = - if !Clflags.option_g && file <> "" then begin - let filenum = - try - Hashtbl.find filename_num file - with Not_found -> - let n = Hashtbl.length filename_num + 1 in - Hashtbl.add filename_num file n; - fprintf oc " .file %d %S\n" n file; - n - in fprintf oc " .loc %d %s\n" filenum line - end + PrintAnnot.print_file_line oc comment file line let print_location oc loc = - if loc <> Cutil.no_loc then - print_file_line oc (fst loc) (string_of_int (snd loc)) + if loc <> Cutil.no_loc then print_file_line oc (fst loc) (snd loc) (* Emit .cfi directives *) @@ -383,7 +370,8 @@ let re_file_line = Str.regexp "#line:\\(.*\\):\\([1-9][0-9]*\\)$" let print_annot_stmt oc txt targs args = if Str.string_match re_file_line txt 0 then begin - print_file_line oc (Str.matched_group 1 txt) (Str.matched_group 2 txt) + print_file_line oc (Str.matched_group 1 txt) + (int_of_string (Str.matched_group 2 txt)) end else begin fprintf oc "%s annotation: " comment; PrintAnnot.print_annot_stmt preg "ESP" oc txt targs args @@ -1042,7 +1030,6 @@ end) type target = ELF | MacOS | Cygwin - let print_program oc p = let target = match Configuration.system with @@ -1057,8 +1044,8 @@ let print_program oc p = | Cygwin -> (module Cygwin_System:SYSTEM)):SYSTEM) in let module Printer = AsmPrinter(Target) in PrintAnnot.print_version_and_options oc Printer.comment; + PrintAnnot.reset_filenames(); Printer.need_masks := false; - Hashtbl.clear Printer.filename_num; List.iter (Printer.print_globdef oc) p.prog_defs; if !Printer.need_masks then begin Printer.section oc (Section_const true); @@ -1073,5 +1060,5 @@ let print_program oc p = fprintf oc "%a: .long 0x7FFFFFFF, 0xFFFFFFFF, 0xFFFFFFFF, 0xFFFFFFFF\n" Target.raw_symbol "__abss_mask" end; - Target.print_epilogue oc - + Target.print_epilogue oc; + PrintAnnot.close_filenames() diff --git a/lib/Printlines.ml b/lib/Printlines.ml new file mode 100644 index 00000000..e0805f15 --- /dev/null +++ b/lib/Printlines.ml @@ -0,0 +1,111 @@ +(* *********************************************************************) +(* *) +(* The Compcert verified compiler *) +(* *) +(* Xavier Leroy, INRIA Paris-Rocquencourt *) +(* *) +(* Copyright Institut National de Recherche en Informatique et en *) +(* Automatique. All rights reserved. This file is distributed *) +(* under the terms of the GNU General Public License as published by *) +(* the Free Software Foundation, either version 2 of the License, or *) +(* (at your option) any later version. This file is also distributed *) +(* under the terms of the INRIA Non-Commercial License Agreement. *) +(* *) +(* *********************************************************************) + +(* Print lines from a file *) + +type filebuf = { + chan: in_channel; + mutable lineno: int (* current line number *) +} + +(* Invariant: the current position of [b.chan] is + the first character of line number [b.lineno]. *) + +let openfile f = + { chan = open_in f; + lineno = 1 } + +let close b = + close_in b.chan + +(* Position [b] to the beginning of line [dest], which must be greater + or equal to the current line. + Return [true] if success, [false] if this line does not exist. *) + +let forward b dest = + assert (dest >= b.lineno); + try + while b.lineno <> dest do + let c = input_char b.chan in + if c = '\n' then b.lineno <- b.lineno + 1; + done; + true + with End_of_file -> + false + +(* Position [b] to the beginning of line [dest], which must be less than + the current line. *) + +let backward_buf = lazy (String.create 65536) + (* 65536 to match [IO_BUFFER_SIZE] in the OCaml runtime. + lazy to allocate on demand. *) + +let backward b dest = + assert (1 <= dest && dest < b.lineno); + let buf = Lazy.force backward_buf in + let rec backward pos idx = + (* pos is the file position corresponding to index 0 in buf *) + (* idx is the current index in buf *) + if idx <= 0 then begin + if pos = 0 then begin + (* beginning of file reached = beginning of line 1. *) + (* assert (dest = 1 && b.lineno = 1) *) + seek_in b.chan 0; + b.lineno <- 1 + end else begin + let pos' = max 0 (pos - String.length buf) in + let len = pos - pos' in + seek_in b.chan pos'; + really_input b.chan buf 0 len; + backward pos' (pos - pos') + end + end else if buf.[idx-1] = '\n' then begin + (* Reached beginning of current line *) + if b.lineno = dest then begin + (* Found line number dest *) + seek_in b.chan (pos + idx) + end else begin + (* Move into previous line *) + b.lineno <- b.lineno - 1; + backward pos (idx - 1) + end + end else + backward pos (idx - 1) + in + backward (pos_in b.chan) 0 + +(* Absolute positioning *) + +let move b dest = + if dest >= b.lineno then forward b dest else (backward b dest; true) + +(* Main function: copy lines from [first] to [last] to [oc], prefixed + by [pref]. *) + +let copy oc pref b first last = + if move b first then begin + output_string oc pref; + try + while b.lineno <= last do + let c = input_char b.chan in + output_char oc c; + if c = '\n' then begin + b.lineno <- b.lineno + 1; + if b.lineno <= last then output_string oc pref + end + done + with End_of_file -> + output_char oc '\n' + end diff --git a/lib/Printlines.mli b/lib/Printlines.mli new file mode 100644 index 00000000..79201f86 --- /dev/null +++ b/lib/Printlines.mli @@ -0,0 +1,28 @@ +(* *********************************************************************) +(* *) +(* The Compcert verified compiler *) +(* *) +(* Xavier Leroy, INRIA Paris-Rocquencourt *) +(* *) +(* Copyright Institut National de Recherche en Informatique et en *) +(* Automatique. All rights reserved. This file is distributed *) +(* under the terms of the GNU General Public License as published by *) +(* the Free Software Foundation, either version 2 of the License, or *) +(* (at your option) any later version. This file is also distributed *) +(* under the terms of the INRIA Non-Commercial License Agreement. *) +(* *) +(* *********************************************************************) + +(** Print lines from a file *) + +type filebuf + (** The type of buffers on opened files *) + +val openfile: string -> filebuf + (** Open the file with the given name. *) +val close: filebuf -> unit + (** Close the file underlying the given buffer. *) +val copy: out_channel -> string -> filebuf -> int -> int -> unit + (** [copy oc pref buf first last] copies lines number [first] + to [last], included, to the channel [oc]. Each line is + prefixed by [pref]. *) diff --git a/powerpc/PrintAsm.ml b/powerpc/PrintAsm.ml index 760ed275..f058cde5 100644 --- a/powerpc/PrintAsm.ml +++ b/powerpc/PrintAsm.ml @@ -31,8 +31,7 @@ module type SYSTEM = val freg: out_channel -> freg -> unit val creg: out_channel -> int -> unit val name_of_section: section_name -> string - val print_file_line: out_channel -> string -> string -> unit - val reset_file_line: unit -> unit + val print_file_line: out_channel -> string -> int -> unit val cfi_startproc: out_channel -> unit val cfi_endproc: out_channel -> unit val cfi_adjust: out_channel -> int32 -> unit @@ -71,8 +70,8 @@ let float_reg_name = function | FPR24 -> "24" | FPR25 -> "25" | FPR26 -> "26" | FPR27 -> "27" | FPR28 -> "28" | FPR29 -> "29" | FPR30 -> "30" | FPR31 -> "31" -module Linux_System = - (struct +module Linux_System : SYSTEM = + struct let comment = "#" let constant oc cst = @@ -120,20 +119,8 @@ module Linux_System = sprintf ".section \"%s\",\"a%s%s\",@progbits" s (if wr then "w" else "") (if ex then "x" else "") - let filename_num : (string, int) Hashtbl.t = Hashtbl.create 7 - let reset_file_line () = Hashtbl.clear filename_num let print_file_line oc file line = - if !Clflags.option_g && file <> "" then begin - let filenum = - try - Hashtbl.find filename_num file - with Not_found -> - let n = Hashtbl.length filename_num + 1 in - Hashtbl.add filename_num file n; - fprintf oc " .file %d %S\n" n file; - n - in fprintf oc " .loc %d %s\n" filenum line - end + PrintAnnot.print_file_line oc comment file line (* Emit .cfi directives *) let cfi_startproc = @@ -164,10 +151,10 @@ module Linux_System = let print_prologue oc = () - end:SYSTEM) + end -module Diab_System = - (struct +module Diab_System : SYSTEM = + struct let comment = ";" let constant oc cst = @@ -214,16 +201,8 @@ module Diab_System = | false, true -> 'c' (* text *) | false, false -> 'r') (* const *) - let last_file = ref "" - let reset_file_line () = last_file := "" let print_file_line oc file line = - if !Clflags.option_g && file <> "" then begin - if file <> !last_file then begin - fprintf oc " .d1file %S\n" file; - last_file := file - end; - fprintf oc " .d1line %s\n" line - end + PrintAnnot.print_file_line_d1 oc comment file line (* Emit .cfi directives *) let cfi_startproc oc = () @@ -233,17 +212,16 @@ module Diab_System = let cfi_adjust oc delta = () let cfi_rel_offset oc reg ofs = () - let print_prologue oc = fprintf oc " .xopt align-fill-text=0x60000000\n"; if !Clflags.option_g then fprintf oc " .xopt asm-debug-on\n" - end:SYSTEM) + end module AsmPrinter (Target : SYSTEM) = - (struct + struct open Target (* On-the-fly label renaming *) @@ -306,9 +284,7 @@ let section oc sec = fprintf oc " %s\n" name let print_location oc loc = - if loc <> Cutil.no_loc then - print_file_line oc (fst loc) (string_of_int (snd loc)) - + if loc <> Cutil.no_loc then print_file_line oc (fst loc) (snd loc) (* Encoding masks for rlwinm instructions *) @@ -335,7 +311,8 @@ let re_file_line = Str.regexp "#line:\\(.*\\):\\([1-9][0-9]*\\)$" let print_annot_stmt oc txt targs args = if Str.string_match re_file_line txt 0 then begin - print_file_line oc (Str.matched_group 1 txt) (Str.matched_group 2 txt) + print_file_line oc (Str.matched_group 1 txt) + (int_of_string (Str.matched_group 2 txt)) end else begin fprintf oc "%s annotation: " comment; PrintAnnot.print_annot_stmt preg "R1" oc txt targs args @@ -857,7 +834,7 @@ let print_globdef oc (name, gdef) = | Gfun f -> print_fundef oc name f | Gvar v -> print_var oc name v - end) + end type target = Linux | Diab @@ -870,9 +847,11 @@ let print_program oc p = let module Target = (val (match target with | Linux -> (module Linux_System:SYSTEM) | Diab -> (module Diab_System:SYSTEM)):SYSTEM) in - Target.reset_file_line(); + PrintAnnot.reset_filenames(); PrintAnnot.print_version_and_options oc Target.comment; let module Printer = AsmPrinter(Target) in Target.print_prologue oc; - List.iter (Printer.print_globdef oc) p.prog_defs + List.iter (Printer.print_globdef oc) p.prog_defs; + PrintAnnot.close_filenames() + |