Fix incorrect integer promotion for bit-fields

[Copilot]

• Add bit-field integer promotion fix (ISO 6.3.1.1) for _Generic, unary ops, switch, doBinOp, variadic args
• Fix merge regression in UNARY MINUS case
• Add test case bitfield4.c and register in testcil.pl
• Refactor: merge integralPromotionBitfield into integralPromotion with optional ?width:int arg — integralPromotion t applies regular promotion; integralPromotion ~width:w t applies bit-field-aware promotion; integralPromotion ?width t passes an int option through (used in integralPromotionE)
• Refactor: replace bitfieldWidthOfExp: exp -> int option with bitfieldWidthOfLval: lval -> int option that takes lval directly; call sites match Lval lv explicitly
• Fix OCaml optional arg syntax: use ?width (giving width : int option inside) instead of ?(width : int option = None) which would require callers to pass ~width:(Some 5)

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]

This looks kinda copy-paste-y. I wonder if an optional argument on integralPromotion would be nicer. It was quite OK in Goblint: goblint/analyzer#1739.

[Copilot]

Done in 6c76a45. integralPromotionBitfield is removed; integralPromotion now takes an optional ?width:int argument. Without it, regular promotion applies; with ~width:w, bit-field-aware promotion is used. The TEnum recursive call forwards ?width using OCaml's pass-through syntax.

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