Unsound IKOS assumes all code is unreachable

[peckto]

With some c++ code I'm experiencing the situation, that IKOS thinks all code is dead, which is obviously not the case.

Example from libtins (https://github.com/mfontanini/libtins):
1) This works well:

void TCP::seq(uint32_t new_seq) {
    header_.seq = Endian::host_to_be(new_seq);
}

ikos -f text -e _ZN4Tins3TCP3seqEj -DHAVE_PCAP_IMMEDIATE_MODE=1 -DHAVE_PCAP_TIMESTAMP_PRECISION=1 -Dtins_EXPORTS -Iinclude -DNDEBUG src/tcp.cpp

# Summary:
Total number of checks                : 16
Total number of unreachable checks    : 0
Total number of safe checks           : 10
Total number of definite unsafe checks: 0
Total number of warnings              : 6

The program is potentially UNSAFE

# Results
include/tins/endianness.h: In function 'Tins::Endian::do_change_endian(unsigned int)':
include/tins/endianness.h:104:16: warning: ignored side effect of call to extern function 'llvm.bswap.i32'. Analysis might be unsound.
        return TINS_BYTE_SWAP_32(data);
               ^
src/tcp.cpp: In function 'Tins::TCP::seq(unsigned int)':
src/tcp.cpp:134:5: warning: variable 'this' might be uninitialized
    header_.seq = Endian::host_to_be(new_seq);
    ^
[...]

2) In this file, all code is detected as dead:

SessionKeys::SessionKeys(const ptk_type& ptk, bool is_ccmp)
: ptk_(ptk), is_ccmp_(is_ccmp) {
    if (ptk_.size() != PTK_SIZE) {
        throw invalid_handshake();
    }
}

ikos -f text -e _ZN4Tins6Crypto4WPA211SessionKeysC2ERKSt6vectorIhSaIhEEb -DHAVE_PCAP_IMMEDIATE_MODE=1 -DHAVE_PCAP_TIMESTAMP_PRECISION=1 -Dtins_EXPORTS -Iinclude -DNDEBUG src/crypto.cpp

# Summary:
Total number of checks                : 11
Total number of unreachable checks    : 11
Total number of safe checks           : 0
Total number of definite unsafe checks: 0
Total number of warnings              : 0

The program is SAFE

# Results
src/crypto.cpp: In function 'Tins::Crypto::WPA2::SessionKeys::SessionKeys(std::vector<unsigned char, std::allocator<unsigned char> > const&, bool)':
src/crypto.cpp:421:14: unreachable: code is dead
: ptk_(ptk), is_ccmp_(is_ccmp) {
             ^
src/crypto.cpp: In function 'Tins::Crypto::WPA2::SessionKeys::SessionKeys(std::vector<unsigned char, std::allocator<unsigned char> > const&, bool)':
src/crypto.cpp:422:21: unreachable: code is dead
    if (ptk_.size() != PTK_SIZE) {
                    ^
src/crypto.cpp: In function 'Tins::Crypto::WPA2::SessionKeys::SessionKeys(std::vector<unsigned char, std::allocator<unsigned char> > const&, bool)':
src/crypto.cpp:422:21: unreachable: code is dead
    if (ptk_.size() != PTK_SIZE) {
                    ^
src/crypto.cpp: In function 'Tins::Crypto::WPA2::SessionKeys::SessionKeys(std::vector<unsigned char, std::allocator<unsigned char> > const&, bool)':
src/crypto.cpp:423:9: unreachable: code is dead
        throw invalid_handshake();
        ^
src/crypto.cpp: In function 'Tins::Crypto::WPA2::SessionKeys::SessionKeys(std::vector<unsigned char, std::allocator<unsigned char> > const&, bool)':
src/crypto.cpp:423:9: unreachable: code is dead
        throw invalid_handshake();
[...]

It seems like, IKOS assumes, the function body will never be entered.
If I add a hard coded error (eg. divide by zero, array out of bounds) to the first line of the function body, this error is not detected by IKOS. Interestingly, its also not reported as unreachable.

I assume, this issue is not directly related to the function which is analyzed, because the code does not seem to be special.
More over, I assume, its related to some global initialization done by some header file.

Does anyone face similar problems?
Do I hit a limitation regarding c++?

This issue might be related to #130.

[peckto]

I found a trivial example, where IKOS assumes all code is dead:

#include <map>

void init() {
    std::map<int, int> m;
}

int foo(int i) {
   return 1 / (i - 1); // divide by zero error
}

int main(int argc, char *argv[]) {
    init();
    foo(argc);
    return 0;
}

IKOS also reports dead code in stl_map.h:

The program is SAFE

# Results
main.cpp: In function 'init()':
main.cpp:5:1: unreachable: code is dead
}
^
main.cpp: In function 'main':
main.cpp:13:5: unreachable: code is dead
    foo(argc);
    ^
main.cpp: In function 'main':
main.cpp:14:5: unreachable: code is dead
    return 0;
    ^
/usr/include/c++/10/bits/stl_map.h: In function 'std::map<int, int, std::less<int>, std::allocator<std::pair<int const, int> > >::~map()':
/usr/include/c++/10/bits/stl_map.h:302:22: unreachable: code is dead
      ~map() = default;
                     ^
/usr/include/c++/10/bits/stl_tree.h: In function 'std::_Rb_tree<int, std::pair<int const, int>, std::_Select1st<std::pair<int const, int> >, std::less<int>, std::allocator<std::pair<int const, int> > >::~_Rb_tree()':
/usr/include/c++/10/bits/stl_tree.h:991:9: unreachable: code is dead
      { _M_erase(_M_begin()); }
        ^
/usr/include/c++/10/bits/stl_tree.h: In function 'std::_Rb_tree<int, std::pair<int const, int>, std::_Select1st<std::pair<int const, int> >, std::less<int>, std::allocator<std::pair<int const, int> > >::~_Rb_tree()':
/usr/include/c++/10/bits/stl_tree.h:991:31: unreachable: code is dead
      { _M_erase(_M_begin()); }
                              ^
/usr/include/c++/10/bits/stl_tree.h: In function 'std::_Rb_tree<int, std::pair<int const, int>, std::_Select1st<std::pair<int const, int> >, std::less<int>, std::allocator<std::pair<int const, int> > >::~_Rb_tree()':
/usr/include/c++/10/bits/stl_tree.h:991:31: unreachable: code is dead
      { _M_erase(_M_begin()); }
                              ^
/usr/include/c++/10/bits/stl_tree.h: In function 'std::_Rb_tree<int, std::pair<int const, int>, std::_Select1st<std::pair<int const, int> >, std::less<int>, std::allocator<std::pair<int const, int> > >::~_Rb_tree()':
/usr/include/c++/10/bits/stl_tree.h:991:31: unreachable: code is dead
      { _M_erase(_M_begin()); }
                              ^
/usr/include/c++/10/bits/stl_tree.h: In function 'std::_Rb_tree<int, std::pair<int const, int>, std::_Select1st<std::pair<int const, int> >, std::less<int>, std::allocator<std::pair<int const, int> > >::~_Rb_tree()':
/usr/include/c++/10/bits/stl_tree.h:991:31: unreachable: code is dead
      { _M_erase(_M_begin()); }
                              ^

Is there any way to get reason, way IKOS assumes the code is unreachable?
When removing the call to init() IKOS correctly finds the bug in function foo.

[arthaud]

This is most likely a bug in ikos related to the analysis of C++.
Unfortunately I won't have time to investigate this.
In general, ikos is not very mature on C++ code, I would recommend sticking with C.