diff options
Diffstat (limited to 'cfrontend/C2C.ml')
| -rw-r--r-- | cfrontend/C2C.ml | 45 |
1 files changed, 45 insertions, 0 deletions
diff --git a/cfrontend/C2C.ml b/cfrontend/C2C.ml index d7f4aff..1abf332 100644 --- a/cfrontend/C2C.ml +++ b/cfrontend/C2C.ml @@ -77,6 +77,14 @@ let builtins_generic = { (* Floating-point absolute value *) "__builtin_fabs", (TFloat(FDouble, []), [TFloat(FDouble, [])], false); + (* Block copy *) + "__builtin_memcpy_aligned", + (TVoid [], + [TPtr(TVoid [], []); + TPtr(TVoid [AConst], []); + TInt(Cutil.size_t_ikind, []); + TInt(Cutil.size_t_ikind, [])], + false); (* Annotations *) "__builtin_annot", (TVoid [], @@ -195,6 +203,38 @@ let register_annotation_val txt targ = Evalof(Evar(intern_string fun_name, Tfunction(targs, tres)), Tfunction(targs, tres)) +(** ** Handling of inlined memcpy functions *) + +let register_inlined_memcpy sz al = + let al = + if al <= 4l then al else 4l in (* max alignment supported by CompCert *) + let name = Printf.sprintf "__builtin_memcpy_sz%ld_al%ld" sz al in + let targs = Tcons(Tpointer(Tvoid, noattr), + Tcons(Tpointer(Tvoid, noattr), Tnil)) + and tres = Tvoid + and ef = EF_memcpy(coqint_of_camlint sz, coqint_of_camlint al) in + register_special_external name ef targs tres; + Evalof(Evar(intern_string name, Tfunction(targs, tres)), + Tfunction(targs, tres)) + +let make_builtin_memcpy args = + match args with + | Econs(dst, Econs(src, Econs(sz, Econs(al, Enil)))) -> + let sz1 = + match Initializers.constval sz with + | CompcertErrors.OK(Vint n) -> camlint_of_coqint n + | _ -> error "ill-formed __builtin_memcpy_aligned (3rd argument must be +a constant)"; 0l in + let al1 = + match Initializers.constval al with + | CompcertErrors.OK(Vint n) -> camlint_of_coqint n + | _ -> error "ill-formed __builtin_memcpy_aligned (4th argument must be +a constant)"; 0l in + let fn = register_inlined_memcpy sz1 al1 in + Ecall(fn, Econs(dst, Econs(src, Enil)), Tvoid) + | _ -> + assert false + (** ** Translation functions *) (** Constants *) @@ -367,6 +407,8 @@ let rec convertExpr env e = Eval(Vint(convertInt i), ty) | C.ESizeof ty1 -> Esizeof(convertTyp env ty1, ty) + | C.EAlignof ty1 -> + Ealignof(convertTyp env ty1, ty) | C.EUnop(C.Ominus, e1) -> Eunop(Oneg, convertExpr env e1, ty) @@ -475,6 +517,9 @@ let rec convertExpr env e = ezero end + | C.ECall({edesc = C.EVar {name = "__builtin_memcpy_aligned"}}, args) -> + make_builtin_memcpy (convertExprList env args) + | C.ECall(fn, args) -> match projFunType env fn.etyp with | None -> |