New support for inserting ais-annotations.

The ais annotations can be inserted via the new ais variants of
the builtin annotation. They mainly differe in that they have an
address format specifier '%addr' which will be replaced by the
adress in the binary.

The implementation simply prints a label for the builtin call
alongside a the text of the annotation as comment and inserts the
annotation together as acii string in a separate section
'ais_annotations' and replaces the usages of the address format
specifiers by the address of the label of the builtin call.

3 files changed, 44 insertions, 7 deletions

diff --git a/cfrontend/C2C.ml b/cfrontend/C2C.ml
index 4dbd6c05..a7ee353a 100644
--- a/cfrontend/C2C.ml
+++ b/cfrontend/C2C.ml
@@ -132,9 +132,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 builtins_generic = {
   Builtins.typedefs = [];
-  Builtins.functions = [
+  Builtins.functions =
+    ais_annot_functions
+    @[
     (* Integer arithmetic *)
     "__builtin_bswap",
     (TInt(IUInt, []), [TInt(IUInt, [])], false);
@@ -828,7 +840,7 @@ let rec convertExpr env e =
       | {edesc = C.EConst(CStr txt)} :: args1 ->
           let targs1 = convertTypArgs env [] args1 in
           Ebuiltin(
-             AST.EF_annot(coqstring_of_camlstring txt, typlist_of_typelist targs1),
+             AST.EF_annot(P.of_int 1,coqstring_of_camlstring txt, typlist_of_typelist targs1),
             targs1, convertExprList env args1, convertTyp env e.etyp)
       | _ ->
           error "argument 1 of '__builtin_annot' must be a string literal";
@@ -840,7 +852,32 @@ let rec convertExpr env e =
       | [ {edesc = C.EConst(CStr txt)}; arg ] ->
           let targ = convertTyp env
                          (Cutil.default_argument_conversion env arg.etyp) in
-          Ebuiltin(AST.EF_annot_val(coqstring_of_camlstring txt, typ_of_type targ),
+          Ebuiltin(AST.EF_annot_val(P.of_int 1,coqstring_of_camlstring txt, typ_of_type targ),
+                   Tcons(targ, Tnil), convertExprList env [arg],
+                   convertTyp env e.etyp)
+      | _ ->
+          error "argument 1 of '__builtin_annot_intval' 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 targs1 = convertTypArgs env [] args1 in
+          Ebuiltin(
+             AST.EF_annot(P.of_int 2,coqstring_of_camlstring 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_intval"}}, args) when Configuration.elf_target ->
+      begin match args with
+      | [ {edesc = C.EConst(CStr txt)}; arg ] ->
+          let targ = convertTyp env
+                         (Cutil.default_argument_conversion env arg.etyp) in
+          Ebuiltin(AST.EF_annot_val(P.of_int 2,coqstring_of_camlstring txt, typ_of_type targ),
                    Tcons(targ, Tnil), convertExprList env [arg],
                    convertTyp env e.etyp)
       | _ ->
diff --git a/cfrontend/Cexec.v b/cfrontend/Cexec.v
index 15818317..bea579fc 100644
--- a/cfrontend/Cexec.v
+++ b/cfrontend/Cexec.v
@@ -512,8 +512,8 @@ Definition do_external (ef: external_function):
   | EF_malloc => do_ef_malloc
   | EF_free => do_ef_free
   | EF_memcpy sz al => do_ef_memcpy sz al
-  | EF_annot text targs => do_ef_annot text targs
-  | EF_annot_val text targ => do_ef_annot_val text targ
+  | EF_annot kind text targs => do_ef_annot text targs
+  | EF_annot_val kind text targ => do_ef_annot_val text targ
   | EF_inline_asm text sg clob => do_inline_assembly text sg ge
   | EF_debug kind text targs => do_ef_debug kind text targs
   end.
diff --git a/cfrontend/PrintCsyntax.ml b/cfrontend/PrintCsyntax.ml
index 6366906a..6e016cb3 100644
--- a/cfrontend/PrintCsyntax.ml
+++ b/cfrontend/PrintCsyntax.ml
@@ -253,10 +253,10 @@ let rec expr p (prec, e) =
       fprintf p "__builtin_memcpy_aligned@[<hov 1>(%ld,@ %ld,@ %a)@]"
                 (camlint_of_coqint sz) (camlint_of_coqint al)
                 exprlist (true, args)
-  | Ebuiltin(EF_annot(txt, _), _, args, _) ->
+  | Ebuiltin(EF_annot(_,txt, _), _, args, _) ->
       fprintf p "__builtin_annot@[<hov 1>(%S%a)@]"
                 (camlstring_of_coqstring txt) exprlist (false, args)
-  | Ebuiltin(EF_annot_val(txt, _), _, args, _) ->
+  | Ebuiltin(EF_annot_val(_,txt, _), _, args, _) ->
       fprintf p "__builtin_annot_intval@[<hov 1>(%S%a)@]"
                 (camlstring_of_coqstring txt) exprlist (false, args)
   | Ebuiltin(EF_external(id, sg), _, args, _) ->