Reactivated and improved ais annotations.

The ais annotations are now handled in a separate file shared
between all architectures. Also two different variants of
replacements are supported, %e which expands to ais expressions
and %l which also expands to an ais expression but is guaranted to
be usable as l-value in the ais annotation. Otherwise the new
warning is Wrong_is_parameter is generated.

Also an error message is generated if floating point variables are
used in ais annotations since a3 does not support them at the
moment.

Additionally an error message is generated for plain volatile
variables used, since they will enforce a volatile load and result
in the value being passed to the annotation instead of the address
as other global variables.

4 files changed, 204 insertions, 22 deletions

diff --git a/backend/AisAnnot.ml b/backend/AisAnnot.ml
new file mode 100644
index 00000000..f4dab4c9
--- /dev/null
+++ b/backend/AisAnnot.ml
@@ -0,0 +1,159 @@
+(* *********************************************************************)
+(*                                                                     *)
+(*              The Compcert verified compiler                         *)
+(*                                                                     *)
+(*          Bernhard Schommer, AbsInt Angewandte Informatik GmbH       *)
+(*                                                                     *)
+(*  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.     *)
+(*                                                                     *)
+(* *********************************************************************)
+
+open AST
+open Camlcoq
+open Diagnostics
+open Memdata
+open Printf
+
+type t =
+  | Label of int
+  | String of string
+  | Symbol of ident
+
+let offset ofs =
+  let ofs = camlint_of_coqint ofs in
+  if ofs = 0l then "" else sprintf " + %ld" ofs
+
+let size_chunk c =
+  sprintf "%ld" (camlint_of_coqint (size_chunk c))
+
+let addr_global id ofs =
+  let addr_o = "("
+  and addr_e = sprintf "%s)" (offset ofs) in
+  [String addr_o;Symbol id;String addr_e]
+
+exception Bad_parameter of string
+exception Unknown_parameter of string
+exception Unknown_type of char
+
+let ais_expr_arg lval preg_string sp_reg_name arg =
+  let preg reg = sprintf "reg(\"%s\")" (preg_string reg)
+  and sp = sprintf "reg(\"%s\")" sp_reg_name
+  and simple s = [String s]
+  and lval ty =
+    if lval then
+      let msg = sprintf "expected register or memory cell but found %s" ty in
+      raise (Bad_parameter msg)
+  in
+  let rec ais_arg = function
+  | BA x -> simple (preg x)
+  | BA_int n -> lval "constant"; simple (sprintf "%ld" (camlint_of_coqint n))
+  | BA_long n ->lval "constant"; simple (sprintf "%Ld" (camlint64_of_coqint n))
+  | BA_float _
+  | BA_single _ -> assert false (* Should never occur and be avoided in C2C *)
+  | BA_loadstack(chunk, ofs) ->
+    let loadstack = sprintf "mem(%s%s, %s)" sp
+                       (offset ofs)
+                       (size_chunk chunk) in
+    simple loadstack
+  | BA_addrstack ofs ->
+    lval "stack cell";
+    let addrstack  = sprintf "(%s%s)" sp (offset ofs) in
+    simple addrstack
+  | BA_loadglobal(chunk, id, ofs) ->
+    let mem_o = "mem("
+    and mem_e = sprintf "%s, %s)"
+        (offset ofs)
+        (size_chunk chunk) in
+    [String mem_o;Symbol id;String mem_e]
+  | BA_addrglobal(id, ofs) ->
+    lval "global address";
+    addr_global id ofs
+  | BA_splitlong(hi, lo) ->
+    combine " * 0x100000000 + " hi lo
+  | BA_addptr(a1, a2) ->
+    combine " + " a1 a2
+  and combine mid arg1 arg2 =
+    lval "pointer computation";
+    let op_br = simple "("
+    and mid = simple mid
+    and cl_br = simple ")"
+    and arg1 = ais_arg arg1
+    and arg2 = ais_arg arg2 in
+    op_br@arg1@mid@arg2@cl_br in
+  ais_arg arg
+
+let ais_annot_list: (t list) list ref = ref []
+
+let get_ais_annots () =
+  let annots = !ais_annot_list in
+  ais_annot_list := [];
+  List.rev annots
+
+let re_loc_param = Str.regexp "# file:\\([^ ]+\\) line:\\([^ ]+\\)"
+
+let loc_of_txt txt =
+  try
+    let pos = String.index txt '\n' in
+    let txt = String.sub txt 0 (pos -1) in
+    if Str.string_partial_match re_loc_param txt 0 then
+      let file = Str.matched_group 1 txt
+      and line = int_of_string (Str.matched_group 2 txt) in
+      file,line
+    else
+      no_loc
+  with _ ->
+    no_loc
+
+let re_ais_annot_param = Str.regexp "%%\\|%[aelp][1-9][0-9]*\\|%here\\|\007"
+
+let add_ais_annot lbl preg_string sp_reg_name txt args =
+  let fragment = function
+    | Str.Delim "%here" ->
+      [Label lbl]
+    | Str.Text s ->
+      [String s]
+    | Str.Delim "%%" ->
+      [String "%"]
+    | Str.Delim "\007" ->
+      [String "\007\000"]
+    | Str.Delim s ->
+      let typ = String.get s 1
+      and n = int_of_string (String.sub s 2 (String.length s - 2)) in
+      let arg = try
+          List.nth args (n-1)
+        with _ ->
+           raise (Unknown_parameter s) in
+      begin match typ with
+        | 'e' -> ais_expr_arg false preg_string sp_reg_name arg
+        | 'l' -> ais_expr_arg true preg_string sp_reg_name arg
+        | _ -> raise (Unknown_type typ)
+      end
+  in
+  let loc = loc_of_txt txt in
+  let warn t s =
+    warning loc Wrong_ais_parameter "%s %s" t s; []
+  in
+  let annot  =
+    try
+      List.concat (List.map fragment (Str.full_split re_ais_annot_param txt))
+    with
+    | Bad_parameter s ->
+      warn "wrong ais parameter" s
+    | Unknown_parameter s ->
+      warn "unknown parameter" s
+    | Unknown_type c ->
+      warn "unknown format argument" (String.make 1 c)
+  in
+  let rec merge acc = function
+    | [] -> List.rev acc
+    | (Label _ as lbl):: rest ->  merge (lbl::acc) rest
+    | (Symbol _ as sym) :: rest -> merge (sym::acc) rest
+    | String s1 :: String s2 :: rest ->
+      merge acc (String (s1 ^ s2) :: rest)
+    | String s:: rest  ->  merge ((String s)::acc) rest
+  in
+  let annot = merge [] annot in
+  if annot <> [] then
+    ais_annot_list := (annot)::!ais_annot_list
diff --git a/backend/AisAnnot.mli b/backend/AisAnnot.mli
new file mode 100644
index 00000000..7219369c
--- /dev/null
+++ b/backend/AisAnnot.mli
@@ -0,0 +1,31 @@
+(* *********************************************************************)
+(*                                                                     *)
+(*              The Compcert verified compiler                         *)
+(*                                                                     *)
+(*          Bernhard Schommer, AbsInt Angewandte Informatik GmbH       *)
+(*                                                                     *)
+(*  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.     *)
+(*                                                                     *)
+(* *********************************************************************)
+
+type t =
+  | Label of int        (** label argument, used for current location*)
+  | String of string    (** text part of the ais annotation *)
+  | Symbol of AST.ident (** symbol argument, used in variable and function addresses *)
+
+val add_ais_annot : int -> ('a -> string) -> string -> string -> 'a AST.builtin_arg list -> unit
+(** [add_ais_annot lbl preg spreg txt args] adds the ais annotation [txt] were the format
+    specifiers are replace according to their type:
+    -a: area definitions
+    -e: general expressions
+    -l: l-value expressions
+    -p: program location
+    -here: the address of the ais annotation [lbl]
+    and [preg] is used to get the names of the registers, as well as [spreg] the name of the
+    stack pointer and [args] the arguments reference in the replacements
+*)
+
+val get_ais_annots: unit -> (t list) list
+(** [get_ais_annots ()] return the list of all ais annotations and reset it *)
diff --git a/backend/PrintAsm.ml b/backend/PrintAsm.ml
index 44c6b409..04ecbae3 100644
--- a/backend/PrintAsm.ml
+++ b/backend/PrintAsm.ml
@@ -18,6 +18,7 @@ open PrintAsmaux
 open Printf
 open Sections
 open TargetPrinter
+open AisAnnot
 
 module Printer(Target:TARGET) =
   struct
@@ -148,21 +149,24 @@ module Printer(Target:TARGET) =
       | Gvar v -> print_var oc name v
 
     let print_ais_annot oc =
-      let annots = List.rev !ais_annot_list in
+      let annots = get_ais_annots () in
       if annots <> [] then begin
         Target.section oc Section_ais_annotation;
-        let annot_part oc lbl = function
-          |  Str.Delim _  ->
-            fprintf oc "	.byte 7,%d\n" (if Archi.ptr64 then 8 else 4) ;
-            fprintf oc "	%s %a\n" Target.address Target.label lbl
-          | Str.Text a -> fprintf oc "	.ascii %S\n" a in
-        let annot oc (lbl,str) =
-          List.iter (annot_part oc lbl) str;
+        let print_addr oc pp_addr addr =
+          fprintf oc "	.byte 7,%d\n" (if Archi.ptr64 then 8 else 4);
+          fprintf oc "	%s %a\n" Target.address pp_addr addr in
+        let annot_part oc = function
+          | AisAnnot.Label lbl  ->
+            print_addr oc Target.label lbl
+          | AisAnnot.Symbol symb ->
+            print_addr oc Target.symbol symb
+          | AisAnnot.String a -> fprintf oc "	.ascii %S\n" a in
+        let annot oc str =
+          List.iter (annot_part oc) str;
           fprintf oc "	.ascii \"\\n\"\n"
         in
         List.iter (annot oc) annots
-      end;
-      ais_annot_list := []
+      end
 
     module DwarfTarget: DwarfTypes.DWARF_TARGET =
       struct
diff --git a/backend/PrintAsmaux.ml b/backend/PrintAsmaux.ml
index d985d5a4..f9ed569f 100644
--- a/backend/PrintAsmaux.ml
+++ b/backend/PrintAsmaux.ml
@@ -212,18 +212,6 @@ let annot_text preg_string sp_reg_name txt args =
         sprintf "<bad parameter %s>" s in
   String.concat "" (List.map fragment (Str.full_split re_annot_param txt))
 
-let ais_annot_list: (int * Str.split_result list) list ref = ref []
-
-let re_annot_addr = Str.regexp "%addr"
-let re_annot_quote = Str.regexp "\007"
-
-let ais_annot_text lbl preg_string sp_reg_name txt args =
-  let annot = annot_text preg_string sp_reg_name txt args in
-  let annot = Str.global_replace re_annot_quote "\007\000" annot in
-  let annots = Str.full_split re_annot_addr annot in
-  ais_annot_list := (lbl,annots)::!ais_annot_list;
-  annot
-
 (* Printing of [EF_debug] info.  To be completed. *)
 
 let re_file_line = Str.regexp "#line:\\(.*\\):\\([1-9][0-9]*\\)$"