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.

1 files changed, 6 insertions, 0 deletions

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