In -g -S mode, annotate the generated asm file with the C source code in comments.

Refactor printing of .loc debug directives in backend/PrintAnnot.ml

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()
+