Repository navigation
Support for long and long long bit-field types #315
Description
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?
Activity
bschommer commentedon Sep 19, 2019
As you have noted supporting
longandlong longis not required by the C99 standard, see §6.7.2.1p4:Unfortunately not only the
elab_bitfieldwould require rewriting also the function that actually translates the bit-field inBitfields.mlwould require changes. However at the moment there are no plans to supportlongandlong longfor bit-field members.Risto-Stevcev commentedon Jul 5, 2024
+1 on supporting this, glibc's libm makes use of
long doubleand a lot of software relies on it.xavierleroy commentedon Jul 8, 2024
For the record: this PR is about the integer type
long longused in the context of bit-fields. The floating-pointlong doubletype is a different issue.CompCert "supports"
long doublein a way (with the-flongdoubleflag), by treating it likedouble(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 commentedon Jul 8, 2024
Ah ok, thanks for clarifying