Interval domain: Add wrap-around behavior

[jerhard]

Goal

The interval domain should be improved by supporting wrap-arounds when possible, instead of going to top when a wrap around occurs.

For unsigned integer types, handling wrap-arounds precisely (when possible) should be the default (and only) behavior. For signed integer types, the precise handling should only be activated when ana.int.wrap_on_signed_overflow is enabled.

Example

E.g., the interval domain should be able to handle something like the following pseudo code:

unsinged int x = MAX_INT; //MAX_INT for unsigned
int top;
if(top){
  x--;
} 
//[x -> [MAX_INT-1; MAX_INT]]
x = x + 2;
//[x -> [0; 1]

[michael-schwarz]

Is the plan here to then also add intervals [a,b] that are not normal in the sense that a <= b? I guess in most cases (except the one you constructed above where there is a must-overflow), the result of operations will be such non-normal intervals.

[jerhard]

Is the plan here to then also add intervals [a,b] that are not normal in the sense that a <= b?

No, I wouldn't plan to implement "circular intervals" here, because I think that would complicate the implementation quite a bit. It would only be for must-overflows.

[jerhard]

This is already implemented with setting the option sem.int.signed_overflow assume_wraparound.