From 252a3b44b1cda99344a7554d1d770cabc47a3102 Mon Sep 17 00:00:00 2001
From: Xavier Leroy <xavier.leroy@inria.fr>
Date: Thu, 17 Nov 2016 13:40:49 +0100
Subject: C2C: revise typing and translation of __builtin_memcpy_aligned

This fixes two issues:
1- The 'size' and 'alignment' arguments of __builtin_memcpy_aligned were declared with type 'unsigned int', which is not good for a 64-bit platform.
2- The corresponding arguments were not cast to type 'unsigned int', causing compilation errors if e.g. the size argument is a 64-bit integer.
(Reported by Michael Schmidt.)

The fix:
1- Evaluate the 3rd and 4th arguments at type size_t
2- Support both Vint and Vlong as results of this evaluation
3- Declare these arguments with type 'unsigned long'.

Supporting work: in lib/Camlcoq.ml, add Z.modulo and Z.is_power2 operations.

Concerning part 3 of the fix, type size_t would be better for future
platforms where size_t is bigger than unsigned long, but some more
work is needed to delay the evaluation of C2C.builtins_generic to
after Cutil.size_t_ikind() is stable, or, equivalently, to evaluate
the cparser/ machine configuration before C2C initializes.
---
 cfrontend/C2C.ml | 28 ++++++++++++++++------------
 1 file changed, 16 insertions(+), 12 deletions(-)

(limited to 'cfrontend/C2C.ml')

diff --git a/cfrontend/C2C.ml b/cfrontend/C2C.ml
index 7ba39be4..439cc584 100644
--- a/cfrontend/C2C.ml
+++ b/cfrontend/C2C.ml
@@ -143,8 +143,8 @@ let builtins_generic = {
          (TVoid [],
            [TPtr(TVoid [], []);
             TPtr(TVoid [AConst], []);
-            TInt(IUInt, []);
-            TInt(IUInt, [])],
+            TInt(IULong, []);
+            TInt(IULong, [])],
           false);
     (* Annotations *)
     "__builtin_annot",
@@ -359,22 +359,26 @@ let globals_for_strings globs =
 
 (** ** Handling of inlined memcpy functions *)
 
+let constant_size_t a =
+  match Initializers.constval_cast !comp_env a Ctyping.size_t with
+  | Errors.OK(Vint n) -> Some(Integers.Int.unsigned n)
+  | Errors.OK(Vlong n) -> Some(Integers.Int64.unsigned n)
+  | _ -> None
+
 let make_builtin_memcpy args =
   match args with
   | Econs(dst, Econs(src, Econs(sz, Econs(al, Enil)))) ->
       let sz1 =
-        match Initializers.constval !comp_env sz with
-        | Errors.OK(Vint n) -> n
-        | Errors.OK(Vlong n) -> n
-        | _ -> error "size argument of '__builtin_memcpy_aligned' must be a constant"; Integers.Int.zero in
+        match constant_size_t sz with
+        | Some n -> n
+        | None -> error "size argument of '__builtin_memcpy_aligned' must be a constant"; Z.zero in
       let al1 =
-        match Initializers.constval !comp_env al with
-        | Errors.OK(Vint n) -> n
-        | Errors.OK(Vlong n) -> n
-        | _ -> error "alignment argument of '__builtin_memcpy_aligned' must be a constant"; Integers.Int.one in
-      if Integers.Int64.is_power2 al1 = None then
+        match constant_size_t al with
+        | Some n -> n
+        | None -> error "alignment argument of '__builtin_memcpy_aligned' must be a constant"; Z.one in
+      if not (Z.is_power2 al1) then
         error "alignment argument of '__builtin_memcpy_aligned' must be a power of 2";
-      if Integers.Int64.modu sz1 al1 <> Integers.Int.zero then
+      if not (Z.eq (Z.modulo sz1 al1) Z.zero) then
         error "alignment argument of '__builtin_memcpy_aligned' must be a divisor of the size";
       (* Issue #28: must decay array types to pointer types *)
       Ebuiltin(EF_memcpy(sz1, al1),
-- 
cgit