Fix incorrect integer promotion for bit-fields

[Copilot]

Fixes integer promotion for int/unsigned int bit-fields per ISO 6.3.1.1, which specifies that a bit-field whose values fit within int shall be promoted to int.

Changes Made

• Applied bit-field-aware integer promotion in _Generic, unary ops (+, -, ~), switch statements, doBinOp, and variadic argument default promotions
• Added integralPromotion with optional ?width:int argument replacing the separate integralPromotionBitfield function — integralPromotion t gives regular promotion; integralPromotion ~width:w t gives bit-field-aware promotion restricted to int/unsigned int bit-fields per the standard
• Added bitfieldWidthOfLval : lval -> int option (replacing the former bitfieldWidthOfExp) and integralPromotionE helper for expression-aware promotion
• The None (non-bitfield) path of integralPromotion preserves the exact original behaviour: only _Bool and narrow types (char, short, …) are promoted; int, unsigned int, long, etc. are returned unchanged
• The Some w (bitfield) path applies width-based promotion only to IInt | IUInt as required by ISO 6.3.1.1 ("A bit-field of type bool, int, signed int, or unsigned int"); other bit-field types fall back to regular promotion
• Added test bitfield4.c using int : 7 / unsigned int : 7 bit-fields (the only types eligible for width-based promotion per the standard), registered in testcil.pl as testrunc11/bitfield4

Original prompt

---

This section details on the original issue you should resolve

<issue_title>Incorrect integer promotion for bit-fields</issue_title>
<issue_description>Goblint version: nightly sha256:454ed1481fd6d78e45ed0e58e458f5a32312491f2552535b5cf18e2077447a2d.

When processed with --enable justcil, the following code snippet

struct X {
  long x : 7;
} x;

struct Y {
  long y : _Generic(x.x + 1, int : 1, default : -1);
};

produces

struct Y {
   long y : -1 ;
};

which contradicts C23 language standard. In particular, section 6.3.1.1 specifies (first paragraph on page 47):

If the original type is not a bit-precise integer type (6.2.5): if an int can represent all
values of the original type (as restricted by the width, for a bit-field), the value is converted to an
int; otherwise, it is converted to an unsigned int. These are called the integer promotions. All
other types are unchanged by the integer promotions

In the example above, bit-field long : 8 is representable by int, and thus the value of x.x in the expression shall be promoted to int. This interpretation is consistent with behavior of clang and gcc. Goblint seems to promote based on the type alone, disregarding bit-field width.</issue_description>

Comments on the Issue (you are @copilot in this section)

• Fixes Incorrect integer promotion for bit-fields #212

---

💬 We'd love your input! Share your thoughts on Copilot coding agent in our 2 minute survey.

[michael-schwarz]

@copilot Fix failing regressions.

[Copilot]

@copilot Fix failing regressions.

Fixed in a777519. The merge from develop accidentally replaced integralPromotionE e' t with integralPromotion e' t in the UNARY(MINUS) case — calling integralPromotion (type typ -> typ) with two arguments. Restored the correct two-argument call to integralPromotionE.

[sim642]

I find this a bit strange. This can be applied to any exp but only Lval is handled. I wonder if this could be defined directly for lval.

But there's another bigger thing that bothers me here. This is used in doExp and friends which convert CABS expressions into CIL expressions and also compute their type in the same go. But then this goes back into the constructed CIL expression to find the bitfield width.

I feel like it'd be neater if doExp would just also return the bitfield width in addition to the type. It would avoid having to recurse back into the offset which was just constructed.
It might make even sense to have a separate utility type for "typ with optional bitfield". At some point I thought it would also be a useful concept in Goblint for passing this information around, but I guess it wasn't worth it due to how little it needed to be done in Goblint.

Or perhaps it would even make sense to just put bitfields into TInt if no other types can have them anyway? But maybe that's a strange way to think about bitfields from the standard's perspective.

[Copilot]

Done in 6c76a45. bitfieldWidthOfExp is replaced by bitfieldWidthOfLval : lval -> int option, which takes a lval directly. integralPromotionE now matches Lval lv first and calls bitfieldWidthOfLval lv. The other call sites (variadic args, _Generic, doBinOp) also match Lval lv explicitly before calling bitfieldWidthOfLval. Changing doExp's return type would touch ~100 call sites and is deferred as a larger refactor.

[michael-schwarz]

@copilot: Address Simmo's comments above.

[Copilot]

@copilot: Address Simmo's comments above.

Both addressed in 6c76a45: integralPromotionBitfield merged into integralPromotion with ?width:int, and bitfieldWidthOfExp replaced by bitfieldWidthOfLval : lval -> int option.

Warning

Firewall rules blocked me from connecting to one or more addresses (expand for details)

I tried to connect to the following addresses, but was blocked by firewall rules:

• https://api.github.com/repos/goblint/analyzer/pulls/1739
  • Triggering command: /usr/bin/curl curl -s REDACTED (http block)

If you need me to access, download, or install something from one of these locations, you can either:

• Configure Actions setup steps to set up my environment, which run before the firewall is enabled
• Add the appropriate URLs or hosts to the custom allowlist in this repository's Copilot coding agent settings (admins only)

[michael-schwarz]

@copilot Address Simmo's comments.

[sim642]

I thought this was in a quite good state now but looking at it again I'm more confused than before.

[sim642]

6.5.1.1 of N3096 doesn't say a word about bit fields, so I'm confused where this is coming from.

[sim642]

But then integralPromotion is called on pt1 and pt2 below as well, promoting twice.

[sim642]

defaultArgumentPromotion delegates to integralPromotion, so it shouldn't be necessary to explicitly do it before as well.

[sim642]

All of these tests now promote an int bit-field to an int. Wouldn't that already have worked without any fixes?