From 2570ddd61b1c98b62c8d97fce862654535696844 Mon Sep 17 00:00:00 2001
From: xleroy <xleroy@fca1b0fc-160b-0410-b1d3-a4f43f01ea2e>
Date: Sun, 26 Feb 2012 10:41:07 +0000
Subject: - Support for _Alignof(ty) operator from ISO C 2011   and
 __alignof__(ty), __alignof__(expr) from GCC. - Resurrected
 __builtin_memcpy_aligned, useful for files generated   by Scade KCG 6.

git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1827 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
---
 cfrontend/C2C.ml | 45 +++++++++++++++++++++++++++++++++++++++++++++
 1 file changed, 45 insertions(+)

(limited to 'cfrontend/C2C.ml')

diff --git a/cfrontend/C2C.ml b/cfrontend/C2C.ml
index d7f4aff7..1abf3326 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 ->
-- 
cgit