KLEE解决迷宫问题

2017-06-09

这是KLEE的第三篇tutorial，感觉还是挺有意思的，虽然简单还是记录一下，原文在此。

问题描述

问题也比较简单，给出一个路径，在下面的迷宫中从’X’走到’#’，a表示左，d表示右，w表示上，s表示下。

"+-+---+---+"
"|X|     |#|"
"| | --+ | |"
"| |   | | |"
"| +-- | | |"
"|     |   |"
"+-----+---+" 

传统方法

// http://feliam.wordpress.com/2010/10/07/the-symbolic-maze/ ‎
// twitter.com/feliam
/*
* It's a maze!
* Use a,s,d,w to move "through" it.
*/

#include<string.h>
#include<stdio.h>
#include<stdlib.h>


/**
* Maze hardcoded dimensions
*/
#define H 7
#define W 11
/**
* Tha maze map
*/
char maze[H][W] = { "+-+---+---+",
					"| |     |#|",
					"| | --+ | |",
					"| |   | | |",
					"| +-- | | |",
					"|     |   |",
					"+-----+---+" };

/**
* Draw the maze state in the screen!
*/
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");
}


/**
* The main function
*/
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];

//Initial position
		x = 1;
		y = 1;
	maze[y][x]='X';

//Print some info
	printf ("Maze dimensions: %dx%d\n", W, H);
	printf ("Player pos: %dx%d\n", x, y);
	printf ("Iteration no. %d\n",i);
	printf ("Program the player moves with a sequence of 'w', 's', 'a' and 'd'\n");
	printf ("Try to reach the price(#)!\n");

//Draw the maze
	draw ();    
//Read the directions 'program' to execute...
	read(0,program,ITERS);

//Iterate and run 'program'
		while(i < ITERS)
		{
		//Save old player position
				ox = x;
				oy = y;
		//Move polayer position depending on the actual command
				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 hit the price, You Win!!            
				if (maze[y][x] == '#')
					{
							printf ("You win!\n");
							printf ("Your solution <%42s>\n",program);
							exit (1);
					}
		//If something is wrong do not advance
				if (maze[y][x] != ' '
					&&
					!((y == 2 && maze[y][x] == '|' && x > 0 && x < W)))
					{
							x = ox;
							y = oy;
					}
		
		//Print new maze state and info...
		printf ("Player pos: %dx%d\n", x, y);
		printf ("Iteration no. %d. Action: %c. %s\n",i,program[i], ((ox==x && oy==y)?"Blocked!":""));
		
		//If crashed to a wall! Exit, you loose
		if (ox==x && oy==y){
					printf("You loose\n");
				exit(-2);
		}
		//put the player on the maze...
		maze[y][x]='X';
		//draw it
				draw ();
		//increment iteration
				i++;
				//me wait to human
				sleep(1);
		}
//You couldn't make it! You loose!       
printf("You loose\n");
}

程序是很简单的，就是给一串输入，然后依次判断，最终给出win或者loose的输出。可以通过观察看到一个解ssssddddwwaawwddddssssddwwww，当然也可以用回溯算法让程序找解。这里我们主要看看用KLEE如何找解。

KLEE求解

KLEE的作用主要是将输入符号化，所以，首先首先将read调用改成klee_make_symbolic，这样就符号化了program变量，当然需要包含头文件#include <klee\/klee.h>。

//read(0,program,ITERS);
klee_make_symbolic(program,ITERS,"program");

这样之后KLEE就会找出所有的路径，但是这样是不够的，因为我们只对win的路径感兴趣，所以需要由一个flag来表示。我们可以在

printf ("You win!\n");

这个语句之后增加一个

klee_assert(0);

这样只要找到一个成功的路径，就会触发一个assert。开始执行。

$ clang -I ../klee/include -emit-llvm -c maze.c
$ klee maze.bc 
...
KLEE: done: total instructions = 127519
KLEE: done: completed paths = 309
KLEE: done: generated tests = 306
test@ubuntu:~/kleestudy$ ls klee-last/*.err
klee-last/test000135.assert.err
test@ubuntu:~/kleestudy$ ktest-tool klee-last/test000135.ktest
ktest file : 'klee-last/test000135.ktest'
args       : ['maze.bc']
num objects: 1
object    0: name: 'program'
object    0: size: 28
object    0: data: 'sddwddddsddwssssssssssssssss'

我们看到输出一个解，

sddwddddsddwssssssssssssssss

直接用这个待入之前的第二节的程序，可以看到是正确的。这里我们注意到KLEE这里输出的解跟我们肉眼的解是不一样的。确实是这样，大多数情况下，KLEE只会输出一个错误状态的路径。要输出所有这个路径的所有输入，需要使用-emit-all-errors：

$ klee -emit-all-errors maze.bc
test@ubuntu:~/kleestudy$ ls klee-last/*.err
klee-last/test000139.assert.err  klee-last/test000238.assert.err
klee-last/test000220.assert.err  klee-last/test000301.assert.err

我们看到输出了四个解。其实从运行的时候可以看出，y==2的时候穿墙了，代码里面也看得出来。

技术 100

符号执行 2