ラビリンス
ラビリンス自体はCプログラムであり、そのコードはここで取得できます 。 開始後、ゲームは一連のステップ（a-左へステップ、d-右へ、w-上およびs-下）に入ることを期待しています。 次のようになります。
プレーヤーの位置：1x4 反復番号 2.アクション：s。 +-+ --- + --- + | X | |＃| | X | -+ | | | X | | | | | X +-| | | | | | + ----- + --- +
見かけの単純さにもかかわらず、迷路は1つの秘密を隠しているため、複数の解決策があります。
クリー
KLEEはLLVMビットコードの文字インタープリターです。 フロントエンドで生成されたコードを実行できます。 シンボリック実行の本質は、起動されたプログラムのすべての入力値に特定の値が含まれるのではなく、可能な値に対するシンボリックな制限が含まれることにあります。 実行中に、既存の変数（プログラム実行パスで分岐する場合）と同様に、新しいシンボリック変数を作成できます（たとえば、値がシンボリックオペランドを使用した何らかの操作の結果に依存する場合）。 2番目の場合、KLEEはSMTソルバーを使用して、原則として、所定のパスに沿ってプログラムを実行できるかどうかを判断します。
このトピックに興味がある場合は、 こちらをご覧になり、 こちらまたはこちらをお読みください。
投稿のアイデアは単純です-ラビリンスプログラムに文字列を入力し、KLEEがソリューションを見つける方法を確認します。
コードを分析しましょう
迷路は、文字の2次元配列として定義されます。
#define H 7 #define W 11 char maze[H][W] = { "+-+---+---+", "| | |#|", "| | --+ | |", "| | | | |", "| +-- | | |", "| | |", "+-----+---+" };
draw（）のタスクは、画面上に配列を描くことです。
void draw () { int i, j; for (i = 0; i < H; i++) { for (j = 0; j < W; j++) printf ("%c", maze[i][j]); printf ("\n"); } printf ("\n"); }
メイン（）関数は、プレーヤーの位置を格納する変数、反復子、およびアクションを格納する28バイトの配列を宣言することから始まります。 次に、プレーヤーの初期位置が（1,1）に設定され、この時点で十字が描かれます。
int main (int argc, char *argv[]) { int x, y; //Player position int ox, oy; //Old player position int i = 0; //Iteration number #define ITERS 28 char program[ITERS]; x = 1; y = 1; maze[y][x]='X';
プレイヤーがそこに導入した内容をstdinから読み取ります。
read(0,program,ITERS);
さらに、サイクルの各反復で、ユーザーの古い座標を保存し、ユーザーを新しい場所に移動します。
while(i < ITERS) { ox = x; //Save old player position oy = y; switch (program[i]) { case 'w': y--; break; case 's': y++; break; case 'a': x--; break; case 'd': x++; break; default: printf("Wrong command!(only w,s,a,d accepted!)\n"); printf("You loose!\n"); exit(-1); }
プレイヤーが最後に到達した場合-おめでとうございます。
if (maze[y][x] == '#') { printf ("You win!\n"); printf ("Your solution \n",program); exit (1); }
何かが間違っている場合-私たちは立っていた場所に戻ります。
if (maze[y][x] != ' ' && !((y == 2 && maze[y][x] == '|' && x > 0 && x < W))) { x = ox; y = oy; }
壁にぶつかった場合、プレーヤーは負けました。
if (ox==x && oy==y){ printf("You loose\n"); exit(-2); }
まあ、何も起こらなかったら、私たちは一歩踏み出しました。 プレーヤーを動かし、絵を描き、イテレーターを増やして最初に戻ります。
maze[y][x]='X'; draw (); //draw it i++; sleep(1); //me wait to human }
迷路を手動で行きましょう
突然自分でゲームを完了したい場合、ほとんどの場合、次の解決策が得られます。
そして今、KLEE
まず、LLVM、トランスレーターC-> LLVM IR（llvm-gccまたはclang）、そして実際にはKLEEが必要です。 ほとんどのLinuxディストリビューションでは、これらのパッケージがリポジトリに既にあります。
mace.cをLLVMビットコードに変換するには、次のコマンドを実行する必要があります
$ llvm-gcc -c –emit-llvm maze.c -o maze.bc
前述のように、llvm-gccの代わりにclangを使用できます。
このコマンドの結果、maze.bcファイルを取得しました。これは、mazeプログラムのビットコードです。 LLVMインタープリターでも実行できます。
$ lli maze.bc
KLEEを使用してコードをテストするには、一部の変数を記号としてマークする必要があります。 この場合、main（）の先頭で宣言されたアクションの配列になります。 だから、行を置き換えます
read(0,program,ITERS);
に
klee_make_symbolic(program,ITERS,"program");
KLEEヘッダーファイルを追加することを忘れないでください
#include <klee/klee.h>
これで、KLEEは実行可能なあらゆるパス（および迷路の廊下）を通過できるようになります。 さらに、これらのパスが何らかのエラー（たとえば、バッファオーバーフロー）につながる可能性がある場合、KLEEはこれについて通知します。 実施します
$ klee maze.bc
そして、次の図を観察します。
最後の3つの投稿からわかるように、KLEEは321の異なるパスを見つけました。 確かに、これは正しい決定ではありません。
KLEE：完了：指示合計= 112773 KLEE：完了：完了したパス= 321 KLEE：完了：生成されたテスト= 318
詳細レポートは、klee-lastディレクトリに保存されます
$ ls klee-last / assembly.ll test000078.ktest test000158.ktest 情報test000079.ktest test000159.ktest messages.txt test000080.ktest test000160.ktest run.istats test000081.ktest test000161.ktest run.stats test000082.ktest test000162.ktest test000001.ktest test000083.ktest test000163.ktest test000075.ktest test000155.ktest warnings.txt
各テストは、ktest-toolユーティリティを使用して表示できます。
$ ktest-tool klee-last / test000222.ktest ktestファイル： 'klee-last / test000222.ktest' args：['maze_klee.o'] num個のオブジェクト：1 オブジェクト0：名前：「プログラム」 オブジェクト0：サイズ：29 オブジェクト0：データ： 'ssssddddwwaawwddddssssddwwwd \ x00′
この場合、ここからプログラム変数の値を取得し、その値をラビリンスプログラムに渡すことでテストを再生できます。
そのため、プログラムで可能なすべてのパスを見つけました。 しかし、すべての適切なソリューションを見つけるために各テストを見てはいけません！ KLEEに、「You win！」に到達するテストを強調する必要があります。
KLEEインターフェースにはklee_assert（）関数が含まれています。これは、Cの類似のassert（）と同じことを行います。ブール式の値を計算し、falseの場合、プログラムの実行を中断します。 私たちの場合、これは医師が注文したものです。
行の後に追加
printf ("You win!\n");
klee_assert（）への無条件呼び出し
printf ("You win!\n"); klee_assert(0); //Signal The solution!!
現在、KLEEはすべての可能な実行パスのテストの生成を停止しませんが、klee_assert（）につながるテストの名前には.errが含まれます。
$ ls -1 klee-last / | grep -A2 -B2 err test000096.ktest test000097.ktest test000098.assert.err test000098.ktest test000098.pc
それらの1つを見てみましょう。
$ ktest-tool klee-last / test000098.ktest ktestファイル： 'klee-last / test000098.ktest' args：['maze_klee.o'] num個のオブジェクト：1 オブジェクト0：名前：「プログラム」 オブジェクト0：サイズ：29 オブジェクト0：データ： 'sddwddddssssddwwww \ x00 \ x00 \ x00 \ x00 \ x00 \ x00 \ x00 \ x00 \ x00 \ x00 \ x00′
したがって、提案されたKLEEソリューションはsddwddddssssddwwwwです
ねえ 短く見えます！ 実際の迷路で試してみましょう：
わかった!!! 迷路には偽の壁があります！ そして、KLEEはそれらを安全に通過しました！ でも、もしKLEEがすべての解決策を見つけることだったとしたら、私たちの最初の場所はどこですか？ KLEEが彼を見つけられなかったのはなぜですか？
まあ、通常、エラー自体を探しているのであれば、エラーに対する1つの方法で十分であり、別の方法は必要ありません。 したがって、この場合、10,000個のコマンドラインオプションのいずれかを使用します。
$ klee –emit-all-errors maze_klee.o
結果を見てみましょう：
迷路の4つの可能な解決策である4つのテストを受け取りました。
$ ktest-tool klee-last / test000097.ktest ktestファイル： 'klee-last / test000097.ktest' args：['maze_klee.o'] num個のオブジェクト：1 オブジェクト0：名前：「プログラム」 オブジェクト0：サイズ：29 オブジェクト0：データ： 'sddwddddsddw \ x00 \ x00 \ x00 \ x00 \ x00 \ x00 \ x00 \ x00 \ x00 \ x00 \ x00 \ x00 \ x00 \ x00 \ x00 \ x00 \ x00′ $ ktest-tool klee-last / test000136.ktest ktestファイル： 'klee-last / test000136.ktest' args：['maze_klee.o'] num個のオブジェクト：1 オブジェクト0：名前：「プログラム」 オブジェクト0：サイズ：29 オブジェクト0：データ： 'sddwddddssssddwwww \ x00 \ x00 \ x00 \ x00 \ x00 \ x00 \ x00 \ x00 \ x00 \ x00 \ x00′ $ ktest-tool klee-last / test000239.ktest ktestファイル： 'klee-last / test000239.ktest' args：['maze_klee.o'] num個のオブジェクト：1 オブジェクト0：名前：「プログラム」 オブジェクト0：サイズ：29 オブジェクト0：データ： 'ssssddddwwaawwddddsddw \ x00 \ x00 \ x00 \ x00 \ x00 \ x00 \ x00′ $ ktest-tool klee-last / test000268.ktest ktestファイル： 'klee-last / test000268.ktest' args：['maze_klee.o'] num個のオブジェクト：1 オブジェクト0：名前：「プログラム」 オブジェクト0：サイズ：29 オブジェクト0：データ： 'ssssddddwwaawwddddssssddwwww \ x00′
したがって、この迷路の解決策：
1.ssssddddddwwaawwddddssssddwwww
2. ssssddddwwaawwddddsddw
3. sddwddddssssddwwww
4. sddwddddsddw