KLEE用于使用pthread的c++代码

Question

我是一个尝试使用KLEE的初学者。我正在使用KLEE自包含包来编写一个c++程序使用pthreads。我已经生成了一个.o文件，并使用了带有以下选项

的KLEE

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

但是我看到我得到警告

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

在.bc文件上使用klee也会得到相同的结果。

我不知道为什么我得到未定义的引用pthread函数。我是不确定pthread的库是否被正确使用。是有办法保证这一点吗?使用llvm-ld也没有帮助。

下面是我使用的llvm-ld命令

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

我不知道为什么有分割故障发生。程序是有效的正常情况下，我用g++编译程序并运行可执行文件。

谁能告诉我我哪里错了?

Answer 1

问题是在Klee中没有现有的pthread支持。因此，当您调用pthread_create()时，Klee将不会响应它(这就是您看到KLEE: WARNING: calling external: pthread_create的原因)。在这种情况下，Klee将会因为这个失败而崩溃。

Answer 2

如果您想在KLEE中使用pthread函数，您可以修改KLEE源代码来模拟多线程的执行。
在KLEE中，有一个数据结构体"ExecutionState"，当你在用户代码中创建线程时，你可以在KLEE中相应地创建一个ExecutionState，并通过线程函数设置ExecutionState的"pc"。因此，您可以覆盖KLEE中的pthread函数，并在Executor.cpp中的"executeInstruction"函数中拦截用户代码对pthread函数的调用。
为了模拟多线程的执行，您应该修改KLEE的搜索器，它用于从所有ExecutionState向量中选择要执行的状态。
所以这是一项艰苦的工作。

Answer 3

截至2010年，KLEE的基本版本不支持任何形式的并行，包括pthread。但是Raimondas Sasnauskas (rwth-aachen)从EPFL获得了关于dslab项目的信息:

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

当前版本的KLEE不支持任何类型的
并行性——你必须自己实现/建模。然而，EPFL的人已经实现了pthread
作为KLEE的扩展，并发表了一篇关于
这个话题:

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

有存档链接:http://web.archive.org/web/20100516044002/http://dslab.epfl.ch/pubs/esd"执行综合:一种自动化软件调试技术"，Cristian Zamfir和George Candea。第五届ACM SIGOPS/EuroSys欧洲计算机系统会议(EuroSys)，法国巴黎，2010年4月

2013年又有一个帖子http://mailman.ic.ac.uk/pipermail/klee-dev/2013-January/000031.html由Cristian Cadar指出KLEE不支持pthreads，并提到KLEE的Cloud9扩展可能处理pthreads:

目前，KLEE对c++的支持有限，不支持pthreads。但是，KLEE的某些扩展可以处理这些方面，例如c++的KLOVER和pthread的Cloud9。取一个更多信息请访问http://klee.llvm.org/Publications.html。