Bool Integer Promotion Crash [Codex]

[mgordon]

Summary

CH-C can crash while reconstructing proof-obligation expressions when an arithmetic expression combines an unsigned long value with _Bool.

Reproducer

See repros/bool_integer_promotion.c.

typedef unsigned long UV;

void grow(UV len, UV offset, _Bool add_one) {
    UV bytes = (len + offset + add_one) * sizeof(UV);
    (void)bytes;
}

Observed Failure

In SPEC CPU 2017 perlbench, analysis of ext/re/re_comp.c:S_invlist_set_len failed in iteration 0 with:

CCHFailure in function: S_invlist_set_len:
Failure Missing case in integer promotion: unsigned long and bool

Cause

get_integer_promotion did not promote IBool before applying the usual arithmetic conversion cases. C _Bool should be subject to integer promotion and become int before combining with larger integer types.

Minimal Fix

Treat IBool like the other small integer types in the local promote helper:

| IBool | IChar | ISChar | IShort -> IInt

bool_integer_promotion.c