diff options
author | Xavier Leroy <xavier.leroy@inria.fr> | 2016-11-17 13:40:49 +0100 |
---|---|---|
committer | Xavier Leroy <xavier.leroy@inria.fr> | 2016-11-17 13:48:43 +0100 |
commit | 252a3b44b1cda99344a7554d1d770cabc47a3102 (patch) | |
tree | 09179d0a80fc537c9a1ead0c64ac8646ebd2453a /cfrontend | |
parent | a3c1aed82d88df7592e63531dc8ce24482da1c28 (diff) | |
download | compcert-252a3b44b1cda99344a7554d1d770cabc47a3102.tar.gz compcert-252a3b44b1cda99344a7554d1d770cabc47a3102.zip |
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.
Diffstat (limited to 'cfrontend')
-rw-r--r-- | cfrontend/C2C.ml | 28 |
1 files changed, 16 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), |