Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Jump to bottom

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

Open
Deep-Cold opened this issue Aug 14, 2024 · 4 comments
Open

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

Deep-Cold opened this issue Aug 14, 2024 · 4 comments

Comments

@Deep-Cold
Copy link

Deep-Cold commented Aug 14, 2024 •
edited
Loading

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
Copy link
Contributor

ccadar commented Aug 15, 2024

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

@Deep-Cold
Copy link
Author

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
Copy link
Contributor

ccadar commented Sep 2, 2024

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

@Deep-Cold
Copy link
Author

@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

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Assignees
No one assigned
Labels
None yet
Projects
None yet
Milestone
No milestone
Development

No branches or pull requests
2 participants
@ccadar @Deep-Cold