使用pthreads的C++代码的KLEE

我是一个尝试使用KLEE的初学者。我正在使用KLEE自包含软件包在使用pthreads的C++程序上。我已经生成.o文件，并使用KLEE使用下列选项使用pthreads的C++代码的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文件使用克利也给了我同样的结果。

我不确定为什么我得到未定义的pthread函数参考。我是不确定用于pthread的库是否正确使用。有有办法确保这一点？使用llvm-ld也无济于事。

下面是我用

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

我不知道为什么会出现分段故障发生LLVM-ld命令。该程序的工作原理罚款时，我正常编译程序g++和运行可执行文件。

有人能告诉我我要去哪里吗？

来源

2013-01-07 Dimurali

问题是Klee中没有现有的pthread支持。因此，当您拨打pthread_create()时，Klee不会回应（这就是您看到KLEE: WARNING: calling external: pthread_create的原因）。在这种情况下，克利将因此失败而崩溃。

来源

2013-02-19 12:48:41 byteocean

截至2010年，KLEE的基本版本不支持任何形式的并行，包括pthread。但Raimondas Sasnauskas（RWTH-亚琛）大约有来自EPFL dslab的项目信息：

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

KLEE的当前版本不支持
并行的任何一种 - 你必须实现/建模你自己。然而，从EPFL人已经实现了并行线程
支持的一个扩展KLEE并发表了很好的一篇关于
这个话题：

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

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

2013年有一个更受克里斯蒂安Cadar发布http://mailman.ic.ac.uk/pipermail/klee-dev/2013-January/000031.html指出，KLEE不支持并行线程，以求佛是Cloud9扩展克利可能会处理pthreads：

目前，KLEE对C++的支持有限，不支持 pthreads。然而，KLEE有一些扩展来处理这些方面，例如用于C++的KLOVER和用于pthread的Cloud9。以看http://klee.llvm.org/Publications.html欲知更多信息。

来源

2014-04-01 17:12:01 osgx

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

来源

2015-10-22 09:17:10 wangxf

使用pthreads的C++代码的KLEE

回答

相关问题