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):
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.
The problem is here:
|
let shiftInBounds i2 = |
|
(* We only try to fold shifts if the second arg is positive and |
|
less than the size of the type of the first argument. |
|
Otherwise, the semantics are processor-dependent, so let the |
|
compiler sort it out. *) |
|
if machdep then |
|
try |
|
compare_cilint i2 zero_cilint >= 0 && |
|
compare_cilint i2 (cilint_of_int (bitsSizeOf (typeOf e1'))) < 0 |
|
with SizeOfError _ -> false |
|
else false |
Namely, the size check only looks at the number of bits (which is equal for
int and
unsigned int), but doesn't account for the signedness. In the signed case the limit is one less. Maybe
const_if_not_overflow/
truncateCilint can be used to do the check.
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:
cil/src/cil.ml
Lines 2640 to 2650 in 638a407
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.