False positive when using a small integer index

[arthaud]

Using a small integer (e.g, uint8_t, int16_t, etc.) as a loop counter usually results into false positives.

For instance:

#include <stdint.h>

void f(int* p, uint16_t n) {
    for (uint16_t i = 0; i < n; i++) {
        p[i] = i;
    }
}

int main() {
    int tab[10];
    f(tab, 10);
    return 0;
}

IKOS returns:

test.c:5:14: warning: possible buffer overflow, pointer '&p[(uint64_t)i]' accesses 4 bytes at offset between 0 and 262140 bytes of local variable 'tab' of size 40 bytes
        p[i] = i;
             ^

The problem comes from the integer promotion rule in C. The comparison i < n actually turns into (unsigned)i < (unsigned)n, which creates temporary variables in the LLVM bitcode:

%4 = zext i16 %.0 to i32, !dbg !25
%5 = zext i16 %1 to i32, !dbg !27
%6 = icmp slt i32 %4, %5, !dbg !28

This results in a lose of precision in the analyzer, similar to #97.
A temporary workaround is to use a relational domain such as dbm or polyhedra.

This false positive appears in our benchmarks:

• 19 times in aeroquad
• 14 times in mnav
• at least 5 times in BioSentinel