Print symbols as symbols.

This allows us to replacing them by their address in valex and
additionally checking them.
Bug 22438

4 files changed, 61 insertions, 36 deletions

diff --git a/arm/AsmToJSON.ml b/arm/AsmToJSON.ml
index 22adc44c..276ceecc 100644
--- a/arm/AsmToJSON.ml
+++ b/arm/AsmToJSON.ml
@@ -130,10 +130,11 @@ let pp_arg pp = function
 
 let pp_instructions pp ic =
   let ic = List.filter (fun s -> match s with
-      | Pbuiltin (ef,_,_) ->
+      | Pbuiltin (ef,args,_) ->
         begin match ef with
-          | EF_inline_asm _
-          | EF_annot _ -> true
+          | EF_inline_asm _ -> true
+          | EF_annot  (kind,txt,targs) ->
+            P.to_int kind = 2 && AisAnnot.json_ais_annot TargetPrinter.preg_annot "r13" (camlstring_of_coqstring txt) args <> []
           | _ -> false
         end
       (* Only debug relevant *)
@@ -156,19 +157,18 @@ let pp_instructions pp ic =
           instruction pp "Pinlineasm" [Id];
           Diagnostics.(warning no_loc Inline_asm_sdump "inline assembler is not supported in sdump")
         | EF_annot (kind,txt, targs) ->
-          let annot_string = PrintAsmaux.annot_text TargetPrinter.preg_annot "r1" (camlstring_of_coqstring txt) args in
-          let len = String.length annot_string in
-          let buf = Buffer.create len in
-          String.iter (fun c -> begin match c with
-              | '\\' | '"' -> Buffer.add_char buf '\\'
-              | _ -> () end;
-              Buffer.add_char buf c) annot_string;
-          let annot_string = Buffer.contents buf in
-        let kind = match P.to_int kind with
-          | 1 -> "normal"
-          | 2 -> "ais"
-          | _ -> assert false in
-          instruction pp "Pannot" [String kind;String annot_string]
+
+          begin match P.to_int kind with
+          | 2 ->
+            let annots = AisAnnot.json_ais_annot TargetPrinter.preg_annot "r13" (camlstring_of_coqstring txt) args in
+            let annots = List.map (function
+                | AisAnnot.String s -> String s
+                | AisAnnot.Symbol s -> Atom s
+                | AisAnnot.Label _ -> assert false (* should never happen *)
+              ) annots in
+            instruction pp "Pannot" annots
+          | _ -> assert false
+          end
         (* Builtins that are not exported to JSON *)
         | EF_annot_val _
         | EF_builtin _
diff --git a/backend/AisAnnot.ml b/backend/AisAnnot.ml
index d10dc8d4..5983f417 100644
--- a/backend/AisAnnot.ml
+++ b/backend/AisAnnot.ml
@@ -113,7 +113,7 @@ let loc_of_txt txt =
 
 let re_ais_annot_param = Str.regexp "%%\\|%[el][0-9]+\\|%here\\|\007"
 
-let add_ais_annot lbl preg_string sp_reg_name txt args =
+let ais_annot_txt warn lbl preg_string sp_reg_name txt args =
   let fragment = function
     | Str.Delim "%here" ->
       [Label lbl]
@@ -138,8 +138,11 @@ let add_ais_annot lbl preg_string sp_reg_name txt args =
       List.concat (List.map fragment (Str.full_split re_ais_annot_param txt))
     with
     | Bad_parameter s ->
-      let loc = loc_of_txt txt in
-      warning loc Wrong_ais_parameter "wrong ais parameter %s" s; []
+      if warn then begin
+        let loc = loc_of_txt txt in
+        warning loc Wrong_ais_parameter "wrong ais parameter %s" s
+      end;
+      []
   in
   let rec merge acc = function
     | [] -> List.rev acc
@@ -149,10 +152,20 @@ let add_ais_annot lbl preg_string sp_reg_name txt args =
       merge acc (String (s1 ^ s2) :: rest)
     | String s:: rest  ->  merge ((String s)::acc) rest
   in
-  let annot = merge [] annot in
+  merge [] annot
+
+let add_ais_annot lbl preg_string sp_reg_name txt args =
+  let annot = ais_annot_txt true lbl preg_string sp_reg_name txt args in
   if annot <> [] then
     ais_annot_list := (annot)::!ais_annot_list
 
+let json_ais_annot preg_string sp_reg_name txt args =
+  let txt = ais_annot_txt false 0 preg_string sp_reg_name txt args in
+  let t_to_json = function
+    | Label _ -> String "%here"
+    | s -> s in
+  (List.map t_to_json txt)
+
 let validate_ais_annot env loc txt args =
   let used_params = Array.make (List.length args) false in
   let fragment arg =
diff --git a/backend/AisAnnot.mli b/backend/AisAnnot.mli
index 59676b26..6bed2eaa 100644
--- a/backend/AisAnnot.mli
+++ b/backend/AisAnnot.mli
@@ -33,3 +33,12 @@ val validate_ais_annot: Env.t -> string * int -> string -> C.exp list -> unit
     that no volatile variables or float expressions are used as well as that no illegal format
     specifier is used in the [txt]
 *)
+
+val json_ais_annot: ('a -> string) -> string -> string -> 'a AST.builtin_arg list -> t list
+(** [json_ais_annot lbl preg spreg txt args] prints the ais annotation [txt] were the format
+    specifiers are replace according to their type:
+    -e: general expressions
+    -l: l-value expressions
+    -here: the address of the ais annotation [lbl]
+    for json export.
+*)
diff --git a/powerpc/AsmToJSON.ml b/powerpc/AsmToJSON.ml
index eaa4c48b..720d09a6 100644
--- a/powerpc/AsmToJSON.ml
+++ b/powerpc/AsmToJSON.ml
@@ -111,10 +111,15 @@ let mnemonic_names  =["Padd"; "Paddc"; "Padde"; "Paddi"; "Paddic"; "Paddis"; "Pa
 
 let pp_instructions pp ic =
   let ic = List.filter (fun s -> match s with
-      | Pbuiltin (ef,_,_) ->
+      | Pbuiltin (ef,args,_) ->
         begin match ef with
-          | EF_inline_asm _
-          | EF_annot _ -> true
+          | EF_inline_asm _ -> true
+          | EF_annot (kind,txt,targs) ->
+            begin match  P.to_int kind with
+              | 1 -> false
+              | 2 ->  AisAnnot.json_ais_annot preg_annot "r1" (camlstring_of_coqstring txt) args <> []
+              | _ -> false
+            end
           | _ -> false
         end
       | Pcfi_adjust _  (* Only debug relevant *)
@@ -342,19 +347,17 @@ let pp_instructions pp ic =
         instruction pp "Pinlineasm" [Id];
         Diagnostics.(warning no_loc Inline_asm_sdump "inline assembler is not supported in sdump")
       | EF_annot (kind,txt,targs) ->
-        let annot_string = PrintAsmaux.annot_text preg_annot "r1" (camlstring_of_coqstring txt) args in
-        let len = String.length annot_string in
-        let buf = Buffer.create len in
-        String.iter (fun c -> begin match c with
-            | '\\' | '"' -> Buffer.add_char buf '\\'
-            | _ -> () end;
-            Buffer.add_char buf c) annot_string;
-        let annot_string = Buffer.contents buf in
-        let kind = match P.to_int kind with
-          | 1 -> "normal"
-          | 2 -> "ais"
-          | _ -> assert false in
-        instruction pp "Pannot" [String kind;String annot_string]
+        begin match P.to_int kind with
+          | 2 ->
+            let annots = AisAnnot.json_ais_annot preg_annot "r1" (camlstring_of_coqstring txt) args in
+            let annots = List.map (function
+                | AisAnnot.String s -> String s
+                | AisAnnot.Symbol s -> Atom s
+                | AisAnnot.Label _ -> assert false (* should never happen *)
+              ) annots in
+            instruction pp "Pannot" annots
+          | _ -> assert false
+        end
       | EF_annot_val _
       | EF_builtin _
       | EF_debug _