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

Question

我是一个尝试使用KLEE的初学者。我正在使用KLEE自包含包在一个使用pthread的C++程序上运行。我已经生成了一个.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年，Cristian Cadar又发布了一篇http://mailman.ic.ac.uk/pipermail/klee-dev/2013-January/000031.html，指出KLEE不支持pthread，并暗示KLEE的Cloud9扩展可以处理pthread：

目前，KLEE对C++的支持是有限的，并且不支持

。然而，有一些对KLEE的扩展可以处理这些方面，例如，用于C++的KLOVER和用于pthread的Cloud9。查看http://klee.llvm.org/Publications.html以获取更多信息。