問題タブ [klee]

http://klee.llvm.org/は、シンボリック実行と制約解決によって機能するプログラム分析ツールで、プログラムをクラッシュさせる可能性のある入力を見つけて、テスト ケースとして出力します。これは非常に印象的なエンジニアリングであり、これまでに作成された中で最も徹底的にテストされたソフトウェアの一部と見なされていた Unix ユーティリティのオープンソース実装のコレクションで多数のバグを発見するなど、これまでにいくつかの良い結果を生み出してきました。

私の質問は: それは何をしませんか?

もちろん、そのようなツールには固有の限界があります。ユーザーの心を読み取って、出力がどうあるべきかを推測することはできません。しかし、原理的に不可能なことは別として、ほとんどのプロジェクトはまだ Klee を使用していないようです。現在のバージョンの制限は何ですか? まだ処理できないバグやワークロードの種類は何ですか?

私は KLEE と呼ばれるテスト生成ツールを使用しています。これは、私の C99 コード用に多くのテストを作成します。その後、テストを実行し、gcov でライン カバレッジをチェックします。Gcov は、実行が正常に完了すると、実行の最後にカバレッジ データを更新するようです。

ただし、一部のテストは失敗し (true でない assert ステートメント)、プログラムが中止され、gcov はこの実行でカバーされた行をカウントしません。

gcov が (成功した場合だけでなく) 終了時に情報をフラッシュする方法はありますか?

コンテクスト

私はklee（http://klee.llvm.org）フォークに取り組んでおり、リポジトリをクリーンアップして、「正規の」kleeコードからコンテンツを分離したいと考えています。とにかく、ビルドシステムの理解/拡張に問題があります。

問題

のディレクトリ構造は/lib/次のようになります

Mine私が追加したばかりですが、これまでのところすべてを投入しCore、に移動していMineます。ビルドシステムにこれを正しく行うように指示するにはどうすればよいですか？

私の試み

これを自分で理解することができないので、私は編集しました/lib/Makefile：

に変更しながら/lib/Core/Makefileにをコピーしました。/lib/Mine/MakefileLIBRARYNAME=kleeCoreLIBRARYNAME=kleeMine

警告

これは適切な方法ではないと感じているので、configureスクリプトなどを変更する必要があります。また、リンクしません（ただし、コンパイルします）。

プロジェクト用にKleeをセットアップしようとしていますが、 http： //klee.llvm.org/TestingCoreutils.htmlに従ってcoreutilsをテストするときに問題が発生します。

問題は、Kleeではなくllvmビルド自体にある可能性が高いです。これは、llvm-disを使用して.bcファイルを分解すると、モジュールIDのみが存在し、実際のコードが存在しないためです。

ビルド出力を見ると、奇妙なことに私は次のように思います。

どんなアイデアも評価されます。

私は、C コードのテストを行うプログラム (klee) を使用しています。プログラムで結果を使用する必要があります。

読み取り可能な情報ではありませんが、解決策のいくつかは次の形式の 16 進数データです: '\x0e\x00\x00\x00' 整数に変換する方法については既に質問しましたが、解決策を見つけました。

この種の結果を構造体にも導入する必要があります。サイズはわかりますが、フィールドやその他のことについてはわかります。

私はこれを解決できると思いますが、問題は次のようなものを取得できる場合があることです: '\n\x00\x00\x00'= 13 または '\r\x00\x00\x00' = 10

そして、彼らがそれを読み取り可能な情報に変換するために使用する表現の種類を見つけられませんでした..明らかに、Pythonでこれを解決できました： import struct selection = struct.unpack('

私はpytonについて何も知りません.Javaまたはcで解決策を見つけたいと思います. どうもありがとう

シンボリック パラメーターを使用したループの場合、KLEE (シンボリック実行ツール) がどのように機能するかについて質問があります。

このコードで klee を実行すると、テスト ケースは 1 つだけになります。ただし、printf(...) のコメントを削除すると、klee は実行を停止するための何らかの制御が必要になります。これは、n の値を生成するためです: --max-depth= 200

クレーがこのように異なる振る舞いをする理由を理解したいのですが、それは私には意味がありません。このコードに printf がない場合、同じ値が生成されないのはなぜですか。

オプション --optimize が使用されていない場合に同じ動作が発生することがわかりました。Klee の --optimize がどのように機能しているか知っている人はいますか?

同じことについての別の疑問は、彼らが公開した論文の場合、私が理解しているように、彼らのヒューリスティック検索では無限にならないと言われていることです (彼らは飢餓を回避します)。このループの場合、クレーの実行を終了する必要がありますか?

前もって感謝します

このホワイト ペーパーの図 7 の結果を再現するのに問題があります。

http://www.stanford.edu/~engler/klee-osdi-2008.pdf

具体的には、コア util の「tac」コマンドをテストしてみました。

ただし、紙にはバグがあるはずだと書かれていますが、KLEE から報告されたエラー メッセージは表示されません。

一方、core util の「md5sum」コマンドを次のようにテストすると、次のようになります。

KLEE は次のエラーを報告します。

「tac」または「pr」コマンドのバグを発見するために、誰かが私を正しい方向に向けることができますか? どちらも、論文でそれぞれ「\b\b\b\b\b\b\b\t」および「\n」と定義されているファイル「t2.txt」および「t3.txt」が必要な場合です。

すべて/アドバイスをいただければ幸いです。

私はKLEEを使おうとしている初心者です。pthreads を使用する C++ プログラムで KLEE 自己完結型パッケージを使用しています。.o ファイルを生成し、次のオプションで KLEE を使用しました

しかし、私は警告が表示されます

.bc ファイルで klee を使用しても、同じ結果が得られます。

pthread 関数への未定義の参照を取得する理由がわかりません。pthreads のライブラリが適切に使用されているかどうかはわかりません。これを確実にする方法はありますか？llvm-ld を使用しても役に立ちません。

以下は、私が使用したllvm-ldコマンドです

セグメンテーション違反が発生する理由がわかりません。通常、プログラムをコンパイルしg++て実行可能ファイルを実行すると、プログラムは正常に動作します。

誰かが私が間違っているところを教えてもらえますか?

私はクレーが初めてなので、チュートリアルを作り始めました。

コンパイルに使用する場合：

1. llvm-gcc --emit-llvm -c -g get_sign.c その後、klee get_sign.o を使用して実行しようとすると、次のエラーが表示されます: KLEE: ERROR: error loading program 'get_sign.o': Invalid MODULE_CODE_GLOBALVAR record . このエラーは、BitcodeReader.cpp ファイル http://llvm.org/docs/doxygen/html/BitcodeReader_8cpp_source.html の行 01594 で定義されています。

2. clang (LLVM パスに正常に使用しました)、それを使用できないようです: KLEE: エラー: プログラム 'get_sign.o' の読み込み中にエラーが発生しました: 無効なビットコード署名 .

私に何ができるか知っていますか？

また、すでにパスに使用している Clang でコンパイルされた Klee 入力を提供するとよいのですが、エラーが示唆するように、それは可能ですか?

前もって感謝します ！

Klee を LLVM 2.9 に (必要に応じて) インストールするときは、 http://klee.llvm.org/GetStarted.htmlに従いました。

1. 依存関係のインストール 完了

   export C_INCLUDE_PATH=/usr/include/i386-linux-gnu/終わり

   export CPLUS_INCLUDE_PATH/usr/include/i386-linux-gnu/終わり

2. LLVM 2.9 のビルド完了

   llvm-gcc のインストール完了

   llvm-gcc を PATH に追加します

   エクスポート パス=$PATH:/home/alex/llvm2.9/llvm/llvm-gcc-4.2-2.9-i686-linux/llvm-gcc-4.2-2.9-i686-linux/bin/

   LLVM 2.9 のダウンロードとビルド 完了

3. STP DONE を--with-cryptominisat2構成時にビルドし、 DONEをmake OPTIMIZE=-O2 CFLAGS_M32= install作成 します。ulimit -s unlimited
4. llvm-gcc DONE で uclibc をビルドする
5. svn クレー 完了

6. KLEE DONEの設定

   。/構成、設定--with-llvm=/home/alex/llvm2.9/llvm/ --with-stp=/home/alex/llvm2.9/llvm/stp/ --with-uclibc=/home/alex/llvm2.9/llvm/klee-uclibc-0.02-i386/ --with-llvm-build-mode=Release+Asserts --enable-posix-runtime

7. クレーを組み立てる

   とENABLE_OPTIMIZED=1

   エラーはありませんが、警告 " /home/alex/llvm2.9/llvm/klee/Makefile.rules:1175: Bytecode libraries require LLVM capable compiler but none is available ****"があります

ただし、チュートリアルを試すと、segfault エラーが発生します: klee: エラー: リンカー入力 ' /home/alex/llvm2.9/llvm/klee/Release+Asserts/lib/libkleeRuntimeIntrinsic.bca'が見つかりません

これらは、クレーのコンパイル中にまったくビルドされませんでした。どうすればよいか教えていただけますか？多分私の問題はこのスレッドに関連しています: http://thread.gmane.org/gmane.comp.compilers.llvm.klee/923。

助けてくれてありがとう！