Merged PrintAnnot into PrintAsmaux.

7 files changed, 178 insertions, 200 deletions

diff --git a/arm/TargetPrinter.ml b/arm/TargetPrinter.ml
index c77572db..505c3265 100644
--- a/arm/TargetPrinter.ml
+++ b/arm/TargetPrinter.ml
@@ -300,7 +300,7 @@ module Target (Opt: PRINTER_OPTIONS) : TARGET =
 (* Emit .file / .loc debugging directives *)
        
     let print_file_line oc file line =
-      PrintAnnot.print_file_line oc comment file line
+      print_file_line oc comment file line
         
     let print_location oc loc =
       if loc <> Cutil.no_loc then print_file_line oc (fst loc) (snd loc)
@@ -320,12 +320,12 @@ module Target (Opt: PRINTER_OPTIONS) : TARGET =
           (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
+        print_annot_stmt preg "sp" oc txt targs args
       end
           
     let print_annot_val oc txt args res =
       fprintf oc "%s annotation: " comment;
-      PrintAnnot.print_annot_val preg oc txt args;
+      print_annot_val preg oc txt args;
       match args, res with
       | [IR src], [IR dst] ->
           if dst = src then 0 else (fprintf oc "	mov	%a, %a\n" ireg dst ireg src; 1)
@@ -1005,7 +1005,7 @@ module Target (Opt: PRINTER_OPTIONS) : TARGET =
               print_annot_val oc (extern_atom txt) args res
           | EF_inline_asm(txt, sg, clob) ->
               fprintf oc "%s begin inline assembly\n\t" comment;
-              PrintAnnot.print_inline_asm preg oc (extern_atom txt) sg args res;
+              print_inline_asm preg oc (extern_atom txt) sg args res;
               fprintf oc "%s end inline assembly\n" comment;
               5 (* hoping this is an upper bound...  *)
           | _ ->
diff --git a/backend/PrintAnnot.ml b/backend/PrintAnnot.ml
deleted file mode 100644
index 88f5d8d6..00000000
--- a/backend/PrintAnnot.ml
+++ /dev/null
@@ -1,182 +0,0 @@
-(* *********************************************************************)
-(*                                                                     *)
-(*              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 INRIA Non-Commercial License Agreement.     *)
-(*                                                                     *)
-(* *********************************************************************)
-
-(* Printing annotations in asm syntax *)
-
-open Printf
-open Datatypes
-open Integers
-open Floats
-open Camlcoq
-open AST
-open Memdata
-open Asm
-
-(** 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
-
-
-(** 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 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
-
-(** "True" annotations *)
-
-let re_annot_param = Str.regexp "%%\\|%[1-9][0-9]*"
-
-let rec print_annot print_preg sp_reg_name oc = function
-  | AA_base x -> print_preg oc x
-  | AA_int n -> fprintf oc "%ld" (camlint_of_coqint n)
-  | AA_long n -> fprintf oc "%Ld" (camlint64_of_coqint n)
-  | AA_float n -> fprintf oc "%.18g" (camlfloat_of_coqfloat n)
-  | AA_single n -> fprintf oc "%.18g" (camlfloat_of_coqfloat32 n)
-  | AA_loadstack(chunk, ofs) ->
-      fprintf oc "mem(%s + %ld, %ld)"
-         sp_reg_name
-         (camlint_of_coqint ofs)
-         (camlint_of_coqint (size_chunk chunk))
-  | AA_addrstack ofs ->
-      fprintf oc "(%s + %ld)"
-         sp_reg_name
-         (camlint_of_coqint ofs)
-  | AA_loadglobal(chunk, id, ofs) ->
-      fprintf oc "mem(\"%s\" + %ld, %ld)"
-         (extern_atom id)
-         (camlint_of_coqint ofs)
-         (camlint_of_coqint (size_chunk chunk))
-  | AA_addrglobal(id, ofs) ->
-      fprintf oc "(\"%s\" + %ld)"
-         (extern_atom id)
-         (camlint_of_coqint ofs)
-  | AA_longofwords(hi, lo) ->
-      fprintf oc "(%a * 0x100000000 + %a)"
-        (print_annot print_preg sp_reg_name) hi
-        (print_annot print_preg sp_reg_name) lo
-
-let print_annot_text print_preg sp_reg_name oc txt args =
-  let print_fragment = function
-  | Str.Text s ->
-      output_string oc s
-  | Str.Delim "%%" ->
-      output_char oc '%'
-  | Str.Delim s ->
-      let n = int_of_string (String.sub s 1 (String.length s - 1)) in
-      try
-        print_annot print_preg sp_reg_name oc (List.nth args (n-1))
-      with Failure _ ->
-        fprintf oc "<bad parameter %s>" s in
-  List.iter print_fragment (Str.full_split re_annot_param txt);
-  fprintf oc "\n"
-
-let print_annot_stmt print_preg sp_reg_name oc txt tys args =
-  print_annot_text print_preg sp_reg_name oc txt args
-
-let print_annot_val print_preg oc txt args =
-  print_annot_text print_preg "<internal error>" oc txt
-    (List.map (fun r -> AA_base r) args)
-
-(** Inline assembly *)
-
-let re_asm_param = Str.regexp "%%\\|%[0-9]+"
-
-let print_inline_asm print_preg oc txt sg args res =
-  let operands =
-    if sg.sig_res = None then args else res @ args in
-  let print_fragment = function
-  | Str.Text s ->
-      output_string oc s
-  | Str.Delim "%%" ->
-      output_char oc '%'
-  | Str.Delim s ->
-      let n = int_of_string (String.sub s 1 (String.length s - 1)) in
-      try
-        print_preg oc (List.nth operands n)
-      with Failure _ ->
-        fprintf oc "<bad parameter %s>" s in
-  List.iter print_fragment (Str.full_split re_asm_param txt);
-  fprintf oc "\n"
-
-
-(** Print CompCert version and command-line as asm comment *)
-
-let print_version_and_options oc comment =
-  fprintf oc "%s File generated by CompCert %s\n" comment Configuration.version;
-  fprintf oc "%s Command line:" comment;
-  for i = 1 to Array.length Sys.argv - 1 do
-    fprintf oc " %s" Sys.argv.(i)
-  done;
-  fprintf oc "\n"
-
diff --git a/backend/PrintAsm.ml b/backend/PrintAsm.ml
index 0438a40f..e91b4e03 100644
--- a/backend/PrintAsm.ml
+++ b/backend/PrintAsm.ml
@@ -130,12 +130,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
-  PrintAnnot.reset_filenames ();
-  PrintAnnot.print_version_and_options oc Target.comment;
+  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;
-  PrintAnnot.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 8bc961ef..497760c1 100644
--- a/backend/PrintAsmaux.ml
+++ b/backend/PrintAsmaux.ml
@@ -16,6 +16,7 @@ open Asm
 open Camlcoq
 open DwarfTypes
 open Datatypes
+open Memdata
 open Printf
 open Sections
 
@@ -140,3 +141,162 @@ let re_file_line = Str.regexp "#line:\\(.*\\):\\([1-9][0-9]*\\)$"
 (* Basic printing functions *)
 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
+
+					    
+(** "True" annotations *)
+
+let re_annot_param = Str.regexp "%%\\|%[1-9][0-9]*"
+
+let rec print_annot print_preg sp_reg_name oc = function
+  | AA_base x -> print_preg oc x
+  | AA_int n -> fprintf oc "%ld" (camlint_of_coqint n)
+  | AA_long n -> fprintf oc "%Ld" (camlint64_of_coqint n)
+  | AA_float n -> fprintf oc "%.18g" (camlfloat_of_coqfloat n)
+  | AA_single n -> fprintf oc "%.18g" (camlfloat_of_coqfloat32 n)
+  | AA_loadstack(chunk, ofs) ->
+      fprintf oc "mem(%s + %ld, %ld)"
+         sp_reg_name
+         (camlint_of_coqint ofs)
+         (camlint_of_coqint (size_chunk chunk))
+  | AA_addrstack ofs ->
+      fprintf oc "(%s + %ld)"
+         sp_reg_name
+         (camlint_of_coqint ofs)
+  | AA_loadglobal(chunk, id, ofs) ->
+      fprintf oc "mem(\"%s\" + %ld, %ld)"
+         (extern_atom id)
+         (camlint_of_coqint ofs)
+         (camlint_of_coqint (size_chunk chunk))
+  | AA_addrglobal(id, ofs) ->
+      fprintf oc "(\"%s\" + %ld)"
+         (extern_atom id)
+         (camlint_of_coqint ofs)
+  | AA_longofwords(hi, lo) ->
+      fprintf oc "(%a * 0x100000000 + %a)"
+        (print_annot print_preg sp_reg_name) hi
+        (print_annot print_preg sp_reg_name) lo
+
+let print_annot_text print_preg sp_reg_name oc txt args =
+  let print_fragment = function
+  | Str.Text s ->
+      output_string oc s
+  | Str.Delim "%%" ->
+      output_char oc '%'
+  | Str.Delim s ->
+      let n = int_of_string (String.sub s 1 (String.length s - 1)) in
+      try
+        print_annot print_preg sp_reg_name oc (List.nth args (n-1))
+      with Failure _ ->
+        fprintf oc "<bad parameter %s>" s in
+  List.iter print_fragment (Str.full_split re_annot_param txt);
+  fprintf oc "\n"
+
+let print_annot_stmt print_preg sp_reg_name oc txt tys args =
+  print_annot_text print_preg sp_reg_name oc txt args
+
+let print_annot_val print_preg oc txt args =
+  print_annot_text print_preg "<internal error>" oc txt
+    (List.map (fun r -> AA_base r) args)
+
+(** Inline assembly *)
+
+let re_asm_param = Str.regexp "%%\\|%[0-9]+"
+
+let print_inline_asm print_preg oc txt sg args res =
+  let operands =
+    if sg.sig_res = None then args else res @ args in
+  let print_fragment = function
+  | Str.Text s ->
+      output_string oc s
+  | Str.Delim "%%" ->
+      output_char oc '%'
+  | Str.Delim s ->
+      let n = int_of_string (String.sub s 1 (String.length s - 1)) in
+      try
+        print_preg oc (List.nth operands n)
+      with Failure _ ->
+        fprintf oc "<bad parameter %s>" s in
+  List.iter print_fragment (Str.full_split re_asm_param txt);
+  fprintf oc "\n"
+
+
+(** Print CompCert version and command-line as asm comment *)
+
+let print_version_and_options oc comment =
+  fprintf oc "%s File generated by CompCert %s\n" comment Configuration.version;
+  fprintf oc "%s Command line:" comment;
+  for i = 1 to Array.length Sys.argv - 1 do
+    fprintf oc " %s" Sys.argv.(i)
+  done;
+  fprintf oc "\n"
diff --git a/debug/CtoDwarf.ml b/debug/CtoDwarf.ml
index b1eea8f3..a352e99f 100644
--- a/debug/CtoDwarf.ml
+++ b/debug/CtoDwarf.ml
@@ -459,7 +459,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 =
-  PrintAnnot.add_file (fst decl.gloc);
+  PrintAsmaux.add_file (fst decl.gloc);
   match decl.gdesc with
   | Gtypedef (n,t) -> let ret = typedef_to_dwarf (n,t) decl.gloc in
     typs@ret,decls
diff --git a/ia32/TargetPrinter.ml b/ia32/TargetPrinter.ml
index ca07a172..a53a8fbd 100644
--- a/ia32/TargetPrinter.ml
+++ b/ia32/TargetPrinter.ml
@@ -323,7 +323,7 @@ module Target(System: SYSTEM):TARGET =
 (* Emit .file / .loc debugging directives *)
 
     let print_file_line oc file line =
-      PrintAnnot.print_file_line oc comment file line
+      print_file_line oc comment file line
 
     let print_location oc loc =
       if loc <> Cutil.no_loc then print_file_line oc (fst loc) (snd loc)
@@ -345,12 +345,12 @@ module Target(System: SYSTEM):TARGET =
           (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
+        print_annot_stmt preg "%esp" oc txt targs args
       end
 
     let print_annot_val oc txt args res =
       fprintf oc "%s annotation: " comment;
-      PrintAnnot.print_annot_val preg oc txt args;
+      print_annot_val preg oc txt args;
       match args, res with
       | [IR src], [IR dst] ->
           if dst <> src then fprintf oc "	movl	%a, %a\n" ireg src ireg dst
@@ -873,7 +873,7 @@ module Target(System: SYSTEM):TARGET =
               print_annot_val oc (extern_atom txt) args res
           | EF_inline_asm(txt, sg, clob) ->
               fprintf oc "%s begin inline assembly\n\t" comment;
-              PrintAnnot.print_inline_asm preg oc (extern_atom txt) sg args res;
+              print_inline_asm preg oc (extern_atom txt) sg args res;
               fprintf oc "%s end inline assembly\n" comment
           | _ ->
               assert false
diff --git a/powerpc/TargetPrinter.ml b/powerpc/TargetPrinter.ml
index b05b29c0..3789d62e 100644
--- a/powerpc/TargetPrinter.ml
+++ b/powerpc/TargetPrinter.ml
@@ -132,7 +132,7 @@ module Linux_System : SYSTEM =
 
 
     let print_file_line oc file line =
-      PrintAnnot.print_file_line oc comment file line
+      print_file_line oc comment file line
     
     (* Emit .cfi directives *)      
     let cfi_startproc = cfi_startproc
@@ -203,7 +203,7 @@ module Diab_System : SYSTEM =
       | Section_debug_abbrev -> ".debug_abbrev,,n"
 
     let print_file_line oc file line =
-      PrintAnnot.print_file_line_d2 oc comment file line
+      print_file_line_d2 oc comment file line
 
     (* Emit .cfi directives *)
     let cfi_startproc oc = ()
@@ -240,10 +240,10 @@ module Diab_System : SYSTEM =
           end_addr := label_end;
           fprintf oc "%a:\n" label label_end;
           fprintf oc "	.text\n";
-          PrintAnnot.StringSet.iter (fun file ->
+          StringSet.iter (fun file ->
             let label = new_label () in
             Hashtbl.add filenum file label;
-            fprintf oc ".L%d:	.d2filenum \"%s\"\n" label file) !PrintAnnot.all_files;
+            fprintf oc ".L%d:	.d2filenum \"%s\"\n" label file) !all_files;
           fprintf oc "	.d2_line_end\n"
         end
 
@@ -331,7 +331,7 @@ module Target (System : SYSTEM):TARGET =
           (int_of_string (Str.matched_group 2 txt))
       end else begin
         fprintf oc "%s annotation: " comment;
-        PrintAnnot.print_annot_stmt preg_annot "R1" oc txt targs args
+        print_annot_stmt preg_annot "R1" oc txt targs args
       end
 
     (* Determine if the displacement of a conditional branch fits the short form *)
@@ -652,7 +652,7 @@ module Target (System : SYSTEM):TARGET =
           begin match ef with
           | EF_inline_asm(txt, sg, clob) ->
               fprintf oc "%s begin inline assembly\n\t" comment;
-              PrintAnnot.print_inline_asm preg oc (extern_atom txt) sg args res;
+              print_inline_asm preg oc (extern_atom txt) sg args res;
               fprintf oc "%s end inline assembly\n" comment
           | _ ->
               assert false