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.

1 files changed, 159 insertions, 0 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