Support for long and long long bit-field types

[tgduckworth]

I ran into an issue recently in which CompCert could not compile a struct with bit-field members of type long. It was straightforward to find where this restriction was enforced, but I've had a more difficult time trying to pinpoint the motivation for it. Supporting long and long long would be considered implementing extended bit-field types according to the C99 standard, and CompCert already does this by supporting (I believe) the use of char and short for this purpose.

From elab_bitfield within elab_field_group within Elab.ml:

...
let ik =
  match unroll env' ty with
  | TInt(ik, _) -> ik
  | TEnum(_, _) -> enum_ikind
  | _ -> ILongLong (* trigger next error message *) in
if integer_rank ik > integer_rank IInt then begin
  error loc
    "the type of bit-field '%a' must be an integer type no bigger than 'int'" pp_field id;
  None,env
...

It seems trivial to rewrite the above as follows.

...
let ik, ik_failure =
  match unroll env' ty with
  | TInt(ik, _) -> ik, false
  | TEnum(_, _) -> enum_ikind, false
  | _ -> ILongLong, true (* trigger next error message *) in
if ik_failure then begin
  error loc
    "the type of bit-field '%a' must be an integer type" pp_field id;
  None,env
...

That being said, I want to respect the intent behind the original error, so if some phase following this elaboration relies on the assumption that there were no bit-fields using a higher-rank carrier type, I would want to be more careful about making changes. Would anyone happen to know whether such an assumption is used?

[bschommer]

As you have noted supporting long and long long is not required by the C99 standard, see §6.7.2.1p4:

A bit-field shall have a type that is a qualified or unqualified version of _Bool, signed
int, unsigned int, or some other implementation-defined type.

Unfortunately not only the elab_bitfield would require rewriting also the function that actually translates the bit-field in Bitfields.ml would require changes. However at the moment there are no plans to support long and long long for bit-field members.

[Risto-Stevcev]

+1 on supporting this, glibc's libm makes use of long double and a lot of software relies on it.

[xavierleroy]

For the record: this PR is about the integer type long long used in the context of bit-fields. The floating-point long double type is a different issue.

CompCert "supports" long double in a way (with the -flongdouble flag), by treating it like double (64-bit FP numbers),. This is a correct implementation according to ISO C, and the ABI-conformant implementation for ARM 32 bits, but doesn't provide extra precision w.r.t. double, and does not conform to the x86 ABIs, among others.

Given CompCert's focus on embedded systems, which generally don't use x86 and are happy with single- or double-precision FP, it's unlikely that CompCert will support extended-precision FP in the near future.

[Risto-Stevcev]

Ah ok, thanks for clarifying