使用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

回答

相關問題