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, 35 insertions, 24 deletions

diff --git a/cfrontend/C2C.ml b/cfrontend/C2C.ml
index b8134599..c18a6e03 100644
--- a/cfrontend/C2C.ml
+++ b/cfrontend/C2C.ml
@@ -119,6 +119,10 @@ let currentLocation = ref Cutil.no_loc
 
 let updateLoc l = currentLocation := l
 
+let currentFunction = ref ""
+
+let updateFunction f = currentFunction := f
+
 let error fmt =
   Diagnostics.error !currentLocation fmt
 
@@ -140,21 +144,21 @@ let string_of_errmsg msg =
 
 (** ** The builtin environment *)
 
-(* let ais_annot_functions =
- *   if Configuration.elf_target then
- *     [(\* Ais Annotations, only available for ELF targets *\)
- *       "__builtin_ais_annot",
- *       (TVoid [],
- *        [TPtr(TInt(IChar, [AConst]), [])],
- *        true);]
- *   else
- *     [] *)
+let ais_annot_functions =
+  if Configuration.elf_target then
+    [(* Ais Annotations, only available for ELF targets *)
+       "__builtin_ais_annot",
+     (TVoid [],
+      [TPtr(TInt(IChar, [AConst]), [])],
+      true);]
+  else
+    []
 
 let builtins_generic = {
   Builtins.typedefs = [];
   Builtins.functions =
-    (* ais_annot_functions
-     * @ *)
+    ais_annot_functions
+      @
     [
     (* Integer arithmetic *)
     "__builtin_bswap",
@@ -871,19 +875,25 @@ let rec convertExpr env e =
           ezero
       end
 
-  (* | C.ECall({edesc = C.EVar {name = "__builtin_ais_annot"}}, args) when Configuration.elf_target ->
-   *     begin match args with
-   *     | {edesc = C.EConst(CStr txt)} :: args1 ->
-   *       let file,line = !currentLocation in
-   *       let loc_string = Printf.sprintf "# file %s, line %d\n" file line in
-   *       let targs1 = convertTypArgs env [] args1 in
-   *         Ebuiltin(
-   *            AST.EF_annot(P.of_int 2,coqstring_of_camlstring (loc_string ^ txt), typlist_of_typelist targs1),
-   *           targs1, convertExprList env args1, convertTyp env e.etyp)
-   *     | _ ->
-   *         error "argument 1 of '__builtin_ais_annot' must be a string literal";
-   *         ezero
-   *     end *)
+  | C.ECall({edesc = C.EVar {name = "__builtin_ais_annot"}}, args) when Configuration.elf_target ->
+      begin match args with
+      | {edesc = C.EConst(CStr txt)} :: args1 ->
+        let file,line = !currentLocation in
+        let fun_name = !currentFunction in
+        let loc_string = Printf.sprintf "# file:%s line:%d function:%s\n" file line fun_name in
+        let targs1 = convertTypArgs env [] args1 in
+        List.iter (fun exp -> if Cutil.is_float_type env exp.etyp then begin
+            error "floating point types are not supported in ais annotations"
+          end else if Cutil.is_volatile_variable env exp then begin
+            error "access to volatile variables are not supported in ais annotations"
+          end) args1;
+          Ebuiltin(
+             AST.EF_annot(P.of_int 2,coqstring_of_camlstring (loc_string ^ txt), typlist_of_typelist targs1),
+            targs1, convertExprList env args1, convertTyp env e.etyp)
+      | _ ->
+          error "argument 1 of '__builtin_ais_annot' must be a string literal";
+          ezero
+      end
 
  | C.ECall({edesc = C.EVar {name = "__builtin_memcpy_aligned"}}, args) ->
       make_builtin_memcpy (convertExprList env args)
@@ -1135,6 +1145,7 @@ and convertSwitch env is_64 = function
 
 let convertFundef loc env fd =
   checkFunctionType env fd.fd_ret (Some fd.fd_params);
+  updateFunction fd.fd_name.name;
   if fd.fd_vararg && not !Clflags.option_fvararg_calls then
     unsupported "variable-argument function (consider adding option [-fvararg-calls])";
   let ret =