int main() {
int displayMask = 1 << 31;
return 0;
}
CIL's constFold is happy to fold 1 << 31 itself, but doesn't account for the fact that the result would be INT_MAX + 1, which is a signed overflow. Since CIL does this simplification, we cannot detect this signed overflow in Goblint and thus are unsound.
Minimized from a no-overflow task that could end up at SV-COMP 2023 (https://gitlab.com/sosy-lab/benchmarking/sv-benchmarks/-/merge_requests/1370):
CIL's
constFoldis happy to fold1 << 31itself, but doesn't account for the fact that the result would beINT_MAX + 1, which is a signed overflow. Since CIL does this simplification, we cannot detect this signed overflow in Goblint and thus are unsound.The problem is here: https://github.com/goblint/cil/blob/638a407306d3ce1646ef2536af173d9ba38cfd33/src/cil.ml#L2640-L2650 Namely, the size check only looks at the number of bits (which is equal for
intandunsigned int), but doesn't account for the signedness. In the signed case the limit is one less. Maybeconst_if_not_overflow/truncateCilintcan be used to do the check.