CODEWITHSUNDEEP
llvmklee
Dimurali
Dimurali

Reputation: 31

KLEE for C++ code that uses pthreads

I am a beginner trying to use KLEE. I am using the KLEE self contained package to on a C++ program that uses pthreads. I have generated a .o file and used KLEE with the following option

klee --libc=uclibc --posix-runtime test.o

But i see i get warning

KLEE: NOTE: Using model:
/home/pgbovine/klee/Release+Asserts/lib/libkleeRuntimePOSIX.bca

KLEE: output directory = "klee-out-4"
KLEE: WARNING: undefined reference to function: klee_get_valuel
KLEE: WARNING: undefined reference to function: pthread_create
KLEE: WARNING: undefined reference to function: pthread_exit
KLEE: WARNING: undefined reference to function: pthread_join
KLEE: WARNING: executable has module level assembly (ignoring)
KLEE: WARNING: calling external: syscall(54, 0, 21505, 571522624)
KLEE: WARNING: calling __user_main with extra arguments.
KLEE: WARNING: calling external: pthread_create(571589384, 0, 563903904, 571574176)
0  klee 0x08965ab8
[pid  1846] +++ killed by SIGSEGV +++

+++ killed by SIGSEGV +++
Segmentation fault

Using klee on a .bc file also gives me the same result.

I am not sure why i get undefined reference to pthread functions. I am not sure if the libraries for pthreads are being used properly. Is there a way to ensure this? Using the llvm-ld also does not help.

Below is the llvm-ld command that i used

 llvm-ld tests.bc -l=/usr/lib/libpthread.a

I am not sure why there Segmentation fault occurs. The program works fine when i normally compile the programs with g++ and run the executable file.

Could someone tell me where i am going wrong?

Upvotes: 3

Views: 1626

Answers (3)

wangxf
wangxf

Reputation: 160

If you want to use the pthread function in KLEE, you can modify the KLEE source code to simulate the execution of multi-thread.
In KLEE, there is a data struct "ExecutionState", and when you create a thread in user code, you can create a ExecutionState in KLEE accordingly, and set "pc" of ExecutionState by thread function. So you can overwrite the pthread functions in KLEE, and intercept the calling of pthread function by user code in the "executeInstruction" function in Executor.cpp.
To simulate the execution of multi-thread, you should modify the searcher of KLEE, which is used to select state to execute from the all the ExecutionState vector.
So it is a hard work.

Upvotes: 1

osgx
osgx

Reputation: 94475

As of 2010, basic version of KLEE does not support any form of parallelism, including pthread. But Raimondas Sasnauskas (rwth-aachen) has information about dslab's project from EPFL:

https://mailman.cs.umd.edu/pipermail/otter-dev/2010-December/000435.html

The current release of KLEE does not support any kind of
parallelism -- you have to implement/model it on your own. Nevertheless, people from EPFL have already implemented pthread
support as an extension to KLEE and published a nice paper about
this topic:

http://dslab.epfl.ch/pubs/esd

There is archived link: http://web.archive.org/web/20100516044002/http://dslab.epfl.ch/pubs/esd "Execution Synthesis: A Technique for Automated Software Debugging", Cristian Zamfir and George Candea. Proc. 5th ACM SIGOPS/EuroSys European Conference on Computer Systems (EuroSys), Paris France, April 2010

In 2013 there was one more posting http://mailman.ic.ac.uk/pipermail/klee-dev/2013-January/000031.html by Cristian Cadar noting that KLEE doesn't support pthreads, with metion that Cloud9 extension of KLEE may handle pthreads:

Currently, KLEE has limited support for C++, and no support for pthreads. However, there are certain extensions to KLEE that handle these aspects, e.g., KLOVER for C++ and Cloud9 for pthreads. Take a look at http://klee.llvm.org/Publications.html for more information.

Upvotes: 0

byteocean
byteocean

Reputation: 99

The issue is that there is no existing pthread support in Klee. Hence, when you call pthread_create(), the Klee will not respond to it(that's why you see KLEE: WARNING: calling external: pthread_create). In this case, Klee will crash due to this failure.

Upvotes: 3

Related Questions