About the unexpected error in the (std::nothrow) version of new together with initialization.

[Deep-Cold]

When running the test program below, KLEE will generate a single path with the ERROR. If the similar sentence appears in a complex program, KLEE will also generate a single path, which is not a normal behavior.

#include <new>
#include "klee/klee.h"
int main()
{
    auto ptr = new uint8_t[256]();
    return 0;
}

KLEE: Using STP solver backend
KLEE: SAT solver: MiniSat
KLEE: WARNING: undefined reference to variable: _ZSt7nothrow
KLEE: WARNING: undefined reference to function: _ZnamRKSt9nothrow_t
KLEE: WARNING ONCE: calling external: _ZnamRKSt9nothrow_t(256, 94101726496032) at tmp.cpp:5 13
KLEE: ERROR: src/runtime/Freestanding/memset.c:15: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location

KLEE: done: total instructions = 71
KLEE: done: completed paths = 0
KLEE: done: partially completed paths = 1
KLEE: done: generated tests = 1

And the issue will disappear if I delete either (std::nothrow) or the initialization parentheses.

    auto ptr = new (std::nothrow) uint8_t[256];

The running log will become the texts below.

KLEE: Using STP solver backend
KLEE: SAT solver: MiniSat
KLEE: WARNING: undefined reference to variable: _ZSt7nothrow
KLEE: WARNING: undefined reference to function: _ZnamRKSt9nothrow_t
KLEE: WARNING ONCE: calling external: _ZnamRKSt9nothrow_t(256, 94866783363304) at tmp.cpp:5 7

KLEE: done: total instructions = 7
KLEE: done: completed paths = 1
KLEE: done: partially completed paths = 0
KLEE: done: generated tests = 1

If I delete (std::nothrow):

    auto ptr = new uint8_t[256]();

The log will become:

KLEE: Using STP solver backend
KLEE: SAT solver: MiniSat
KLEE: WARNING ONCE: Alignment of memory from call "_Znam" is not modelled. Using alignment of 8.

KLEE: done: total instructions = 130
KLEE: done: completed paths = 1
KLEE: done: partially completed paths = 0
KLEE: done: generated tests = 1

The current version of KLEE I used is 3.0 with LLVM version 13.0.1

[ccadar]

@Deep-Cold how do you run KLEE? Have you enabled support for C++? Note the "calling external" message in the output.

[Deep-Cold]

Thanks @ccadar, we actually installed KLEE with C++ support enabled. But the calling external message still exists referencing to std::nothrow. Is there any other additional options in running commands we need to enable?

The compiling and execution commands we used are below:

clang++ -emit-llvm -c -g tmp.cpp -o tmp.bc -I ./klee/include
klee tmp.bc

[ccadar]

@Deep-Cold I can't reproduce this behaviour, can you try the latest version of KLEE?

[Deep-Cold]

@ccadar I change my klee version

KLEE 3.2-pre (https://klee-se.org/)
  Build mode: RelWithDebInfo (Asserts: ON)
  Build revision: 4a4d75cc1331beae7f7f81b5fbc34caccfa0fa7b

Ubuntu LLVM version 13.0.1

  Optimized build.
  Default target: x86_64-pc-linux-gnu
  Host CPU: goldmont

The issue still exist. Maybe I pasted the wrong original code. The issue appears on the code below.

#include <new>
#include "klee/klee.h"

int main()
{
        auto ptr = new (std::nothrow) uint8_t[256]();
    return 0;
}

And the result is:

KLEE: Using STP solver backend
KLEE: SAT solver: CryptoMiniSat
KLEE: Deterministic allocator: Using quarantine queue size 8
KLEE: Deterministic allocator: globals (start-address=0x7f09897fc000 size=10 GiB)
KLEE: Deterministic allocator: constants (start-address=0x7f07097fc000 size=10 GiB)
KLEE: Deterministic allocator: heap (start-address=0x7e07097fc000 size=1024 GiB)
KLEE: Deterministic allocator: stack (start-address=0x7de7097fc000 size=128 GiB)
KLEE: WARNING: undefined reference to variable: _ZSt7nothrow
KLEE: WARNING: undefined reference to function: _ZnamRKSt9nothrow_t
KLEE: WARNING ONCE: calling external: _ZnamRKSt9nothrow_t(256, 139679475154944) at tmp.cpp:6 16
KLEE: ERROR: runtime/Freestanding/memset.c:15: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location

KLEE: done: total instructions = 36
KLEE: done: completed paths = 0
KLEE: done: partially completed paths = 1
KLEE: done: generated tests = 1