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.

[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.

[michael-schwarz]

I have now manually cleaned up the mess:

The key insights are:

• Using an expression of type bitfield as the controlling expression in _Generic does not cause arithmetic promotion to happen. What happens is lvalue conversion, which amounts to dropping type qualifiers.
• In an expression for which arithmetic promotion is applied to its arguments, bitfields are promoted to int, even if their type is larger, as long as int can contain the range.

We thus have:

struct X {
  long x : 7;   /* signed long 7-bit: range fits in int -> promote to int */
} sx;

int main() {
  int r1 = _Generic(sx.x + 0, int : 1, default : -1); 
  // r1 == 1
  // sx.x + 0 caused arithmetic promotion of sx.x to int

  /* Unary + also triggers integer promotion */
  int r2 = _Generic(+sx.x, int : 1, default : -1);
  // r2 == 1
  // uplus  caused arithmetic promotion of sx.x to int

  /* Direct bit-field access does not itself trigger integer promotion. */
  int r6 = _Generic(sx.x, int : 1, default : -1);
  // r 6 == -1
  // sx.x causes no promotion
}