Interval domain: unsound transfer functions for `div` and `mul`
caballa opened this issue · 2 comments
Issue
The transfer functions for div
and mul
seem wrong.
Steps to reproduce
I was reading the code and found two issues:
-
div
(https://github.com/facebookexperimental/MIRAI/blob/main/checker/src/interval_domain.rs#L126)
The use ofsaturating.add
seems a typo -
mul
(https://github.com/facebookexperimental/MIRAI/blob/main/checker/src/interval_domain.rs#L332)
gives wrong results if negative intervals.
[-4, -2]*[5, 10] = [-20, -20] which is clearly wrong since it doesn't include e.g. -4 * 10 = -40
A sound transfer function would be
[x,y] * [a,b] = [min(x*a, x*b, y*a, y*b), max(x*a, x*b, y*a, y*b)]
[-4, -2]*[5, 10] = [min(-4*5,-4*10,-2*5,-2*10), max(-4*5,-4*10,-2*5,-2*10)] = [-40, -10]
Thanks for reading carefully and being kind enough to report your findings. I've put up a fix for in in hermanventer#7. Since no-one at Meta seems interested to facilitate merges to this repo, the current source of truth for MIRAI is now https://github.com/hermanventer/MIRAI.
This is a really nice project. Thanks for all the effort!