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.

1 files changed, 40 insertions, 3 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)
       | _ ->