diff options
Diffstat (limited to 'cfrontend/C2C.ml')
-rw-r--r-- | cfrontend/C2C.ml | 87 |
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) = |