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.