Conversation
|
Personally, I am a bit skeptical about this, it seems like it is blurring the distinction between intervals and def_exc ranges even more? Maybe we can align on what we want out of Def_Exc at a Gobcon? |
It's already on the agenda!
It certainly brings them closer, but last time this was discussed there wasn't a clear plan to go either way with it. It would also be straightforward to make this configurable: general handling can also do everything we have right now. |
Is this not just |
For unsigned ikinds, things like For signed ikinds, we don't really get a sign analysis because we have things like |
|
The plan is not to go for this right now, but just document the implicit assumption in #1726. |
In relation to a thesis I'm supervising, the matter came up whether def_exc exclusion range (in bits) may be something like [4, 6], i.e. 15..63. Such things could arise from joining definite 15 and 63, for example. My intuition about the domain is that conceptually this should be fine.
Turns out that our implementation does not handle such things, but always requires the range to include 0. But this assumption doesn't seem to be documented anywhere, nor is it even
asserted anywhere.It was even difficult to find out that we have such implicit assumption. The reason we do is in how we construct exclusion ranges: always based on some
ikindboundaries, i.e. in multiples of 8 and always including 0.So in this PR I quickly tried to change that, but only for positive ranges for now by modifying
IntDomain0.Size.min_range_sign_agnostic. Although it should be generalizable to negative ones as well.A few things break immediately, but they seem to be also easily fixed. Although it's far from clear whether some abstract operations still make the implicit assumption.
Of course this begs the question whether we should have this. At some point I thought about removing the exclusion ranges entirely because all
IntDomainoperations now getikinds, but I think the counterargument was that we can still find out slightly more precise things than the type with these ranges, particularly about booleans. So if we have the ranges, we should use them to their full potential like this.