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.

2 files changed, 22 insertions, 12 deletions

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),
diff --git a/lib/Camlcoq.ml b/lib/Camlcoq.ml
index 5b5d37ee..63a31181 100644
--- a/lib/Camlcoq.ml
+++ b/lib/Camlcoq.ml
@@ -170,6 +170,8 @@ module Z = struct
   let add = Z.add
   let sub = Z.sub
   let mul = Z.mul
+  let div = Z.div
+  let modulo = Z.modulo
   let eq x y = (Z.compare x y = Eq)
   let lt x y = (Z.compare x y = Lt)
   let gt x y = (Z.compare x y = Gt)
@@ -247,9 +249,13 @@ module Z = struct
 
   let to_string = dec
 
+  let is_power2 x =
+    gt x zero && eq (Z.coq_land x (pred x)) zero
+
   let (+) = add
   let (-) = sub
   let ( * ) = mul
+  let ( / ) = div
   let (=) = eq
   let (<) = lt
   let (<=) = le