Print_annot should produce a string.

5 files changed, 54 insertions, 40 deletions

diff --git a/arm/TargetPrinter.ml b/arm/TargetPrinter.ml
index 6f1cb6c1..0626a371 100644
--- a/arm/TargetPrinter.ml
+++ b/arm/TargetPrinter.ml
@@ -81,6 +81,11 @@ struct
     | FR r -> freg oc r
     | _    -> assert false
 
+  let preg_annot = function
+    | IR r -> int_reg_name r
+    | FR r -> float_reg_name r
+    | _ -> assert false
+
   let condition_name = function
     | TCeq -> "eq"
     | TCne -> "ne"
@@ -730,11 +735,11 @@ struct
     | Pbuiltin(ef, args, res) ->
       begin match ef with
         | EF_annot(txt, targs) ->
-          fprintf oc "%s annotation: " comment;
-          print_annot_text preg "sp" oc (camlstring_of_coqstring txt) args;
+          fprintf oc "%s annotation: %s\n" comment
+          (annot_text preg_annot "sp" (camlstring_of_coqstring txt) args);
           0
         | EF_debug(kind, txt, targs) ->
-          print_debug_info comment print_file_line preg "sp" oc
+          print_debug_info comment print_file_line preg_annot "sp" oc
             (P.to_int kind) (extern_atom txt) args;
           0
         | EF_inline_asm(txt, sg, clob) ->
diff --git a/backend/PrintAsmaux.ml b/backend/PrintAsmaux.ml
index f54c8698..df3445ea 100644
--- a/backend/PrintAsmaux.ml
+++ b/backend/PrintAsmaux.ml
@@ -150,62 +150,61 @@ let ptrofs oc n =
 
 let re_annot_param = Str.regexp "%%\\|%[1-9][0-9]*"
 
-let rec print_annot print_preg sp_reg_name oc = function
-  | BA x -> print_preg oc x
-  | BA_int n -> fprintf oc "%ld" (camlint_of_coqint n)
-  | BA_long n -> fprintf oc "%Ld" (camlint64_of_coqint n)
-  | BA_float n -> fprintf oc "%.18g" (camlfloat_of_coqfloat n)
-  | BA_single n -> fprintf oc "%.18g" (camlfloat_of_coqfloat32 n)
+let rec annot_arg preg_string sp_reg_name = function
+  | BA x -> preg_string x
+  | BA_int n -> sprintf "%ld" (camlint_of_coqint n)
+  | BA_long n -> sprintf "%Ld" (camlint64_of_coqint n)
+  | BA_float n -> sprintf "%.18g" (camlfloat_of_coqfloat n)
+  | BA_single n -> sprintf "%.18g" (camlfloat_of_coqfloat32 n)
   | BA_loadstack(chunk, ofs) ->
-      fprintf oc "mem(%s + %ld, %ld)"
+      sprintf "mem(%s + %ld, %ld)"
          sp_reg_name
          (camlint_of_coqint ofs)
          (camlint_of_coqint (size_chunk chunk))
   | BA_addrstack ofs ->
-      fprintf oc "(%s + %ld)"
+      sprintf "(%s + %ld)"
          sp_reg_name
          (camlint_of_coqint ofs)
   | BA_loadglobal(chunk, id, ofs) ->
-      fprintf oc "mem(\"%s\" + %ld, %ld)"
+      sprintf "mem(\"%s\" + %ld, %ld)"
          (extern_atom id)
          (camlint_of_coqint ofs)
          (camlint_of_coqint (size_chunk chunk))
   | BA_addrglobal(id, ofs) ->
-      fprintf oc "(\"%s\" + %ld)"
+      sprintf "(\"%s\" + %ld)"
          (extern_atom id)
          (camlint_of_coqint ofs)
   | BA_splitlong(hi, lo) ->
-      fprintf oc "(%a * 0x100000000 + %a)"
-        (print_annot print_preg sp_reg_name) hi
-        (print_annot print_preg sp_reg_name) lo
+      sprintf "(%s * 0x100000000 + %s)"
+        (annot_arg preg_string sp_reg_name hi)
+         (annot_arg preg_string sp_reg_name lo)
   | BA_addptr(a1, a2) ->
-      fprintf oc "(%a + %a)"
-        (print_annot print_preg sp_reg_name) a1
-        (print_annot print_preg sp_reg_name) a2
+      sprintf "(%s + %s)"
+        (annot_arg preg_string sp_reg_name a1)
+        (annot_arg preg_string sp_reg_name a2)
 
-let print_annot_text print_preg sp_reg_name oc txt args =
-  let print_fragment = function
+let annot_text preg_string sp_reg_name txt args =
+  let fragment = function
   | Str.Text s ->
-      output_string oc s
+      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))
+        annot_arg preg_string sp_reg_name (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"
+        sprintf "<bad parameter %s>" s in
+  String.concat "" (List.map fragment (Str.full_split re_annot_param txt))
 
 (* Printing of [EF_debug] info.  To be completed. *)
 
 let re_file_line = Str.regexp "#line:\\(.*\\):\\([1-9][0-9]*\\)$"
 
-let print_debug_info comment print_line print_preg sp_name oc kind txt args =
+let print_debug_info comment print_line preg_string sp_name oc kind txt args =
   let print_debug_args oc args =
     List.iter
-      (fun a -> fprintf oc " %a" (print_annot print_preg sp_name) a)
+      (fun a -> fprintf oc " %s" (annot_arg preg_string sp_name a))
       args in
   match kind with
   | 1 ->  (* line number *)
diff --git a/powerpc/TargetPrinter.ml b/powerpc/TargetPrinter.ml
index cb5f2304..bff2a7fa 100644
--- a/powerpc/TargetPrinter.ml
+++ b/powerpc/TargetPrinter.ml
@@ -335,9 +335,9 @@ module Target (System : SYSTEM):TARGET =
 
     (* For printing annotations, use the full register names [rN] and [fN]
        to avoid ambiguity with constants. *)
-    let preg_annot oc = function
-      | IR r -> fprintf oc "r%s" (int_reg_name r)
-      | FR r -> fprintf oc "f%s" (float_reg_name r)
+    let preg_annot = function
+      | IR r -> sprintf "r%s" (int_reg_name r)
+      | FR r -> sprintf "f%s" (float_reg_name r)
       | _    -> assert false
 
     (* Encoding masks for rlwinm instructions *)
@@ -834,8 +834,8 @@ module Target (System : SYSTEM):TARGET =
       | Pbuiltin(ef, args, res) ->
           begin match ef with
           | EF_annot(txt, targs) ->
-              fprintf oc "%s annotation: " comment;
-              print_annot_text preg_annot "r1" oc (camlstring_of_coqstring txt) args
+              fprintf oc "%s annotation: %s\n" comment
+              (annot_text preg_annot "r1" (camlstring_of_coqstring txt) args)
           | EF_debug(kind, txt, targs) ->
               print_debug_info comment print_file_line preg_annot "r1" oc
                                (P.to_int kind) (extern_atom txt) args
diff --git a/riscV/TargetPrinter.ml b/riscV/TargetPrinter.ml
index 7a369832..65339d35 100644
--- a/riscV/TargetPrinter.ml
+++ b/riscV/TargetPrinter.ml
@@ -97,6 +97,11 @@ module Target : TARGET =
       | FR r -> freg oc r
       | _    -> assert false
 
+    let preg_annot = function
+      | IR r -> int_reg_name r
+      | FR r -> float_reg_name r
+      | _ -> assert false
+
 (* Names of sections *)
 
     let name_of_section = function
@@ -585,10 +590,10 @@ module Target : TARGET =
       | Pbuiltin(ef, args, res) ->
          begin match ef with
           | EF_annot(txt, targs) ->
-              fprintf oc "%s annotation: " comment;
-              print_annot_text preg "sp" oc (camlstring_of_coqstring txt) args
+              fprintf oc "%s annotation: %s\n" comment
+              (annot_text preg_annot "sp" (camlstring_of_coqstring txt) args)
           | EF_debug(kind, txt, targs) ->
-              print_debug_info comment print_file_line preg "sp" oc
+              print_debug_info comment print_file_line preg_annot "sp" oc
                                (P.to_int kind) (extern_atom txt) args
           | EF_inline_asm(txt, sg, clob) ->
               fprintf oc "%s begin inline assembly\n\t" comment;
diff --git a/x86/TargetPrinter.ml b/x86/TargetPrinter.ml
index 4a576df3..f61d7686 100644
--- a/x86/TargetPrinter.ml
+++ b/x86/TargetPrinter.ml
@@ -66,6 +66,11 @@ let preg oc = function
   | FR r -> freg oc r
   | _    -> assert false
 
+let preg_annot = function
+  | IR r -> if Archi.ptr64 then int64_reg_name r else int32_reg_name r
+  | FR r -> float_reg_name r
+  | _ -> assert false
+
 let z oc n = output_string oc (Z.to_string n)
 
 (* 32/64 bit dependencies *)
@@ -736,10 +741,10 @@ module Target(System: SYSTEM):TARGET =
       | Pbuiltin(ef, args, res) ->
           begin match ef with
           | EF_annot(txt, targs) ->
-              fprintf oc "%s annotation: " comment;
-              print_annot_text preg "%esp" oc (camlstring_of_coqstring txt) args
+              fprintf oc "%s annotation: %s\n" comment
+              (annot_text preg_annot "%esp" (camlstring_of_coqstring txt) args)
           | EF_debug(kind, txt, targs) ->
-              print_debug_info comment print_file_line preg "%esp" oc
+              print_debug_info comment print_file_line preg_annot "%esp" oc
                                (P.to_int kind) (extern_atom txt) args
           | EF_inline_asm(txt, sg, clob) ->
               fprintf oc "%s begin inline assembly\n\t" comment;