1 files changed, 67 insertions, 20 deletions

diff --git a/cfrontend/C2C.ml b/cfrontend/C2C.ml
index 84e24640..a7ee353a 100644
--- a/cfrontend/C2C.ml
+++ b/cfrontend/C2C.ml
@@ -132,12 +132,34 @@ 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);
+    "__builtin_bswap32",
+      (TInt(IUInt, []), [TInt(IUInt, [])], false);
+    "__builtin_bswap16",
+      (TInt(IUShort, []), [TInt(IUShort, [])], false);
     (* Floating-point absolute value *)
     "__builtin_fabs",
-      (TFloat(FDouble, []), [TFloat(FDouble, [])], false);
+    (TFloat(FDouble, []), [TFloat(FDouble, [])], false);
+    (* Float arithmetic *)
+    "__builtin_fsqrt",
+    (TFloat(FDouble, []), [TFloat(FDouble, [])], false);
     (* Block copy *)
     "__builtin_memcpy_aligned",
          (TVoid [],
@@ -200,63 +222,63 @@ let builtins_generic = {
           [TPtr(TVoid [], []); TInt(IULong, [])],
           false);
   (* Helper functions for int64 arithmetic *)
-    "__i64_dtos",
+    "__compcert_i64_dtos",
         (TInt(ILongLong, []),
          [TFloat(FDouble, [])],
          false);
-    "__i64_dtou",
+    "__compcert_i64_dtou",
         (TInt(IULongLong, []),
          [TFloat(FDouble, [])],
          false);
-    "__i64_stod",
+    "__compcert_i64_stod",
         (TFloat(FDouble, []),
          [TInt(ILongLong, [])],
          false);
-    "__i64_utod",
+    "__compcert_i64_utod",
         (TFloat(FDouble, []),
          [TInt(IULongLong, [])],
          false);
-    "__i64_stof",
+    "__compcert_i64_stof",
         (TFloat(FFloat, []),
          [TInt(ILongLong, [])],
          false);
-    "__i64_utof",
+    "__compcert_i64_utof",
         (TFloat(FFloat, []),
          [TInt(IULongLong, [])],
          false);
-    "__i64_sdiv",
+    "__compcert_i64_sdiv",
         (TInt(ILongLong, []),
          [TInt(ILongLong, []); TInt(ILongLong, [])],
          false);
-    "__i64_udiv",
+    "__compcert_i64_udiv",
         (TInt(IULongLong, []),
          [TInt(IULongLong, []); TInt(IULongLong, [])],
          false);
-    "__i64_smod",
+    "__compcert_i64_smod",
         (TInt(ILongLong, []),
          [TInt(ILongLong, []); TInt(ILongLong, [])],
          false);
-    "__i64_umod",
+    "__compcert_i64_umod",
         (TInt(IULongLong, []),
          [TInt(IULongLong, []); TInt(IULongLong, [])],
          false);
-    "__i64_shl",
+    "__compcert_i64_shl",
         (TInt(ILongLong, []),
          [TInt(ILongLong, []); TInt(IInt, [])],
          false);
-    "__i64_shr",
+    "__compcert_i64_shr",
         (TInt(IULongLong, []),
          [TInt(IULongLong, []); TInt(IInt, [])],
          false);
-    "__i64_sar",
+    "__compcert_i64_sar",
         (TInt(ILongLong, []),
          [TInt(ILongLong, []); TInt(IInt, [])],
          false);
-    "__i64_smulh",
+    "__compcert_i64_smulh",
         (TInt(ILongLong, []),
          [TInt(ILongLong, []); TInt(ILongLong, [])],
          false);
-    "__i64_umulh",
+    "__compcert_i64_umulh",
         (TInt(IULongLong, []),
          [TInt(IULongLong, []); TInt(IULongLong, [])],
          false)
@@ -818,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";
@@ -830,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)
       | _ ->
@@ -1130,7 +1177,7 @@ let convertFundef loc env fd =
 (** External function declaration *)
 
 let re_builtin = Str.regexp "__builtin_"
-let re_runtime = Str.regexp "__i64_"
+let re_runtime = Str.regexp "__compcert_i64_"
 
 let convertFundecl env (sto, id, ty, optinit) =
   let (args, res, cconv) =