c4-project / c4f

The C4 Concurrent C Fuzzer
MIT License
13 stars 1 forks source link

Constant generator KV equations can overflow #243

Open MattWindsor91 opened 3 years ago

MattWindsor91 commented 3 years ago

Suppose we have a variable x with known value -2147483648, and want to generate the constant 0. The constant generator will consider producing the expression x + 2147483648, which is theoretically valid, but 2147483648 is not expressible as a 32-bit integer. Oops, potential undefined behaviour.

I can't get my brain around the correct way of doing this, but I suspect that the right way to fix this has something to do with breaking the addition/subtraction into two stages: one that adds/subs INT_MAX and one that adds/subs the remainder. This, in turn, needs some caution, because the calculation that produces the new addition/subtraction needs to make sure it doesn't overflow or underflow (though, to be honest, the OCaml integer situation is fishy anyway: see #228).