From 252a3b44b1cda99344a7554d1d770cabc47a3102 Mon Sep 17 00:00:00 2001 From: Xavier Leroy 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. --- lib/Camlcoq.ml | 6 ++++++ 1 file changed, 6 insertions(+) (limited to 'lib/Camlcoq.ml') 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 -- cgit