False positive because of unknown intrinsic function

[gh2375]

Code:

#include <new>

int main(int argc, char * argv[])
{
    int n = 10;
    int * arr = new int[n];

    for(int * p = arr; n > 0; n--, p++)
        new (p) int();

    delete[] arr;

    return 0;
}

Output:

# Results
main-placement-new.cpp: In function 'main':
main-placement-new.cpp:10:3: warning: possible buffer overflow, could not bound index for access of dynamic memory allocated at 'main:7:14'
                new (p) int();
                ^

System:

MSYS2

Version:

d9a9c44e1ff23c533dc49bcab40328961ef70abb

[arthaud]

The problem is more clear with 79942e6469bbcbe8a9e0acaf651a65cba1653502:

test.cpp: In function 'main':
test.cpp:6:17: warning: ignored side effect of call to extern function 'llvm.umul.with.overflow.i64'. Analysis might be unsound.
    int * arr = new int[n];
                ^
test.cpp: In function 'main':
test.cpp:9:9: warning: possible buffer overflow, could not bound index for access of dynamic memory allocated at 'main:6:17'
        new (p) int();
        ^

LLVM has an intrinsic llvm.umul.with.overflow.i64 to compute the size of the array, i.e n * sizeof(int) and check for overflows. I will have to teach this intrinsic to ikos.

[ivanperez-keera]

"I will have to teach this intrinsic to ikos."

Looking at what I've seen so far to fix #221, it sound like this should be something I could potentially attack in the next version of IKOS.

It sounds like it would be a matter of:

• Adding the intrinsic to: ar/include/ikos/ar/semantic/intrinsic.hpp
• Mapping a function to the intrinsic somewhere in: frontend/llvm/src/import/
• Modify the checkers that can make use of this information in: analyzer/src/checker and analyzer/include/ikos/analyzer/analysis.

I'm unsure about what I'd need to do in: ar/src/semantic/intrinsic.cpp > ikos_assert.

Does this look close to the steps that would be needed?

[arthaud]

There are multiple functions in ar/src/semantic/intrinsic.cpp. For Intrinsic::type I think this takes 2 u64 and returns a u64.

You will also need to implement the behavior of the intrinsic in the analyzer: https://github.com/NASA-SW-VnV/ikos/blob/master/analyzer/include/ikos/analyzer/analysis/execution_engine/numerical.hpp#L1895