`def_exc` ranges for `int` and `short` tops not correct in memOutOfBounds analysis

[karoliineh]

When running the following modifications of test 01-oob-heap-simple.c:

// PARAM: --set ana.activated[+] memOutOfBounds --enable ana.int.interval
#include <stdlib.h>

int main(int argc, char const *argv[]) {
    char *ptr = malloc(5 * sizeof(char));
    int r;

    *ptr = 'a';//NOWARN
    *(ptr + 1) = 'b';//NOWARN
    *(ptr + 10) = 'c';//WARN
    *(ptr + r) = 'd';//WARN

    free(ptr);

    return 0;
}

// PARAM: --set ana.activated[+] memOutOfBounds --enable ana.int.interval
#include <stdlib.h>

int main(int argc, char const *argv[]) {
    char *ptr = malloc(5 * sizeof(char));
    short r;

    *ptr = 'a';//NOWARN
    *(ptr + 1) = 'b';//NOWARN
    *(ptr + 10) = 'c';//WARN
    *(ptr + r) = 'd';//WARN

    free(ptr);

    return 0;
}

The corresponding warnings are: [Warning][Behavior > Undefined > MemoryOutOfBoundsAccess][CWE-823] Could not compare pointer size (5) with offset ((Unknown int([-31,32]),[-2147483648,2147483647])). Memory out-of-bounds access may occur (tests/regression/74-invalid_deref/01-oob-heap-simple.c:11:5-11:21) [Warning][Behavior > Undefined > MemoryOutOfBoundsAccess][CWE-823] Could not compare pointer size (5) with offset ((Unknown int([-15,16]),[-32768,32767])). Memory out-of-bounds access may occur (tests/regression/74-invalid_deref/01-oob-heap-simple.c:11:5-11:21)

It is fine with long, though, yielding: [Warning][Behavior > Undefined > MemoryOutOfBoundsAccess][CWE-823] Could not compare pointer size ((5,[5,5])) with offset ((Unknown int([-63,63]),[-9223372036854775808,9223372036854775807])). Memory out-of-bounds access may occur (tests/regression/74-invalid_deref/01-oob-heap-simple.c:11:5-11:21)

[michael-schwarz]

Just to be sure I understand the issue: What would be the expected outcome? And is this a precision problem or a soundness problem?

[mrstanb]

Looking at it, I think it shouldn't actually have any effect on soundness, right?

[sim642]

The expected outcome is that for int it is [-31,31], not [-31,32], and for short it is [-15,15], not [-15,16], because those are the normal bit ranges for those types. It's some kind of consistency issue that such larger-than-type ranges somehow arise at all.

It might impact precision if intervals aren't used at the same time, but it could also lead to some odd bugs. For example, in context of #1312, these incorrect ranges mean that is_top_of returns false for them, as if they're more precise than [-31,31], which they are not. So some lattice property is violated: is_top_of (and potentially many other operations) have been implemented with the assumption that [-31,31] is the unique top element.

[michael-schwarz]

I think the type inside offsets is ptrdiff_ikind, which might be related to how they arise here.