3

私はKLEEを使おうとしている初心者です。pthreads を使用する 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 に答える
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 「Execution Synthesis: A Technique for Automated Software Debugging」、Cristian Zamfir および George Candea。議事録 第 5 回 ACM SIGOPS/EuroSys European Conference on Computer Systems (EuroSys)、パリ、フランス、2010 年 4 月

2013 年には、Christian Cadar による別の投稿http://mailman.ic.ac.uk/pipermail/klee-dev/2013-January/000031.htmlCloud9があり、KLEE は pthreads をサポートしていないことを指摘し、KLEEの拡張について言及しました。 pthread を処理できます:

現在、KLEE は C++ のサポートを制限しており、pthreads はサポートしていません。ただし、これらの側面を処理する KLEE には特定の拡張機能があります。たとえば、C++ 用の KLOVER や pthreads 用の Cloud9 です。詳細については、http://klee.llvm.org/Publications.htmlをご覧ください。

于 2014-04-01T17:12:01.010 に答える