-
Notifications
You must be signed in to change notification settings - Fork 170
Reachability benchmarks with overflow #1166
Comments
I already understood why the "solution" using @divyeshunadkat proposed in #1155 to use I don't think there are worse cases than those (using twice *) so one possibility would be to use long long (8 bytes) for the result variables and restrict the nondeterministic values to shorts (2 bytes). I think this we keep the complexity of the benchmarks without resulting in overflow. |
Now that #1155 has been merged, we can proceed to fix the inherited bugs in |
I think there are still problems overflows with
@MartinSpiessl told me the analysis might be unsound so I'm not sure. However, I get errors using Dartagnan in the scaled versions ( |
I need to do so anyway to fix #1200 after the coverage property verdicts got merged first. I will probably open a new PR and close #1200 because the merge conflicts are not worth fixing if I can just regenerate everything from the generation script
Yes, linear integer arithmetic might be unsound, I will have a look. |
I recently found many benchmarks from the reachability category which contain overflow and thus undefined behaviours. These include
nla-digbench/hard.c
as mentioned in #1105 and the ones I mentioned in #1159. Below are some more.The problem also propagates to
nla-digbench-scaling
but I think the best would be to figure it out what to do with the base case and then using the script from @MartinSpiessl to generate the derived versions.The question is how to fix these benchmarks from the reachability perspective (we should additionally keep them as they are for the no-overflow category).
I spent some time trying to find out a general solution, but nothing came to my mind. In issue #1105, it is said that using unsigned would solve the problem, but I don't think this apply to the general case (not event to this particular case, see this): the extra bit might not be enough if e.g. we multiply two non deterministic integers.
I thought adding something like
assume_abort_if_not(X >= 1) <= INT_MAX
andassume_abort_if_not(X >= 1) >= INT_MIN
would do the trick even if we would need the check for every sub-expression, e.g.assert(x*y + a*b == 0)
would require to addhowever I'm not sure this works. I'm performing the verification on optimised code (using -O3 in clang) and I still get a wrong result. While this might be a bug on my verifier, I suspect it is actually that clang performs some aggressive optimisation due to undefined behaviour (this was the way I discover all other overflows).
The text was updated successfully, but these errors were encountered: