3

我是一个尝试使用 KLEE 的初学者。我在使用 pthread 的 C++ 程序上使用 KLEE 自包含包。我生成了一个 .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 函数的未定义引用。我不确定是否正确使用了 pthreads 库。有没有办法确保这一点？使用 llvm-ld 也无济于事。

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

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

我不确定为什么会出现分段错误。当我通常编译程序g++并运行可执行文件时，该程序运行良好。

有人能告诉我哪里出错了吗？

4

3 回答 3

3

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

于 2013-02-19T12:48:41.300 回答
1

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

于 2015-10-22T09:17:10.383 回答
0

截至 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，并提到Cloud9KLEE 的扩展可以处理 pthreads：

目前，KLEE 对 C++ 的支持有限，不支持 pthread。但是，KLEE 的某些扩展可以处理这些方面，例如，用于 C++ 的 KLOVER 和用于 pthread 的 Cloud9。查看http://klee.llvm.org/Publications.html了解更多信息。

于 2014-04-01T17:12:01.010 回答