 |
VS. |
Maze dimensions: 11x7
Player pos: 1x1 Iteration no. 0
Program the player moves with
a sequence of 'w', 's', 'a' or 'd'
Try to reach the prize(#)!
+-+---+---+
|X| |#|
| | --+ | |
| | | | |
| +-- | | |
| | |
+-----+---+
|
How many solutions do you think it has?
The Maze
The thing is coded in C and the impatient can download it from here. This simple ASCII game asks you first to feed it with directions. You should enter them as a batch list of actions. As "usual"; a is Left, d is Right, w is Up and s is Down. It has this looks ...Player pos: 1x4 Iteration no. 2. Action: s. +-+---+---+ |X| |#| |X| --+ | | |X| | | | |X+-- | | | | | | +-----+---+
The KLEE
KLEE is a symbolic interpreter of LLVM bitcode. It runs code compiled/assembled into LLVM symbolically. That's running a program considering its input(or some other variables) to be symbols instead of concrete values like 100 or "cacho". In very few words, a symbolic execution runs through the code propagating symbols and conditions; forking execution at symbol dependant branches and asking the companion SMT solver for path feasibility or counter-examples. For more info on this check out this, this or even this. Find it interesting? Keep reading!The idea
Use KLEE to automatically solve our small puzzle.Dissecting the code
Lets take a walk through the maze code. First it hardcodes the map as a static global rw variable.#define H 7
#define W 11
char maze[H][W] = { "+-+---+---+",
"| | |#|",
"| | --+ | |",
"| | | | |",
"| +-- | | |",
"| | |",
"+-----+---+" };
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");
}
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';
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 lose!\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 lose\n");
exit(-2);
}
maze[y][x]='X';
draw (); //draw it
i++;
sleep(1); //me wait to human
}
printf("You lose\n");
}
By hand...
Now considering you have it in maze.c. It should compile with a line like thisgcc maze.c -o maze
Run it! In a couple of tries you'll get to the priceless '#'. Maybe using this solution:
ssssddddwwaawwddddssssddwwww
Yere you have a screen cast of me wining! Vivaaaa!!
By KLEE
Let's see if KLEE is able to find the solution. First, for even start thinking about KLEE we need to get a copy of the LLVM toolchain, and compile our maze to LLVM bitcode. Here we have use LLVM 2.7 and llvm-gcc. You may want to take a tour to KLEE's official tutorials here. Once you have the LLVM thing in place, a compile and test cycle for the maze.c using LLVM will be like this...llvm-gcc -c --emit-llvm maze.c -o maze.bc
lli maze.bc
That will run the LLVM bitcode representation of our maze in the interpreter. But for testing it with KLEE we need to mark something in the code as symbolic. Let's mark all maze inputs as symbolic, that's the array of actions the maze code reads at the very beginning of the main function. KLEE will gain 'symbolic control' over the array of actions. In code, that's done by changing this line ...
read(0,program,ITERS);
klee_make_symbolic(program,ITERS,"program");
#include <klee/klee.h>
Symbolic execution, the chamigo way:
- Say.. every input is marked as a symbol.
- Not the concrete value like 1 or "cachho", but a symbolic variable representing every possible value.
- Then the program evolves...adding restrictions to this symbols.
- At some point it may face a branch that depends on such symbols.
- On that case it checks feasibility of the different paths using a SMT solver.
- If feasible, then it dives into each path repeating this basic algorithm
- Of course if an error cond is reached, the SMT solver is asked for a way to reach that specific spot
Hello, is mr. memory corruption here?! Let's give it a try...
llvm-gcc -c -Ipath/to/klee --emit-llvm maze_klee.c -o maze_klee.bc
klee maze.bc
Here there is the screen cast of the a run...
As you could check at the end of the demo, KLEE finds 321 different paths...
KLEE: done: total instructions = 112773
KLEE: done: completed paths = 321
KLEE: done: generated tests = 318
... and it throws the test cases to generate all them to the klee-last folder...
$ls klee-last/
assembly.ll test000078.ktest test000158.ktest
info 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
Each test case could be retrieved with the ktest-tool like this...
$ktest-tool klee-last/test000222.ktest
ktest file : 'klee-last/test000222.ktest'
args : ['maze_klee.o']
num objects: 1
object 0: name: 'program'
object 0: size: 29
object 0: data: 'ssssddddwwaawwddddssssddwwwd\x00'
So in this case you may take that input to the original maze and check what it does.
Ok, so far so good but I'm not ktest-tooling every possible test case and check if it is a maze solution! We need a way for KLEE to help us tell the normal test cases apart from the ones that actually reaches the "You win!" state.
Note also that KLEE haven't found any error on the maze code. By design KLEE will issue a warning when any "well known" error condition(like a wrongly indexed memory access) is detected.
How to flag the portion of code we are interested in?
There is a klee_assert() function that pretty much do the same thing that a common C assert, it forces a condition to be true otherwise it aborts execution! You could check out the complete KLEE C interface here. But we already have what we need... a way to mark certain program part(with an assert) so KLEE will scream when it reach it. In the code, that's done by replacing this line ...printf ("You win!\n");
printf ("You win!\n");
klee_assert(0); //Signal The solution!!
$ls -1 klee-last/ |grep -A2 -B2 err
test000096.ktest
test000097.ktest
test000098.assert.err
test000098.ktest
test000098.pc
Let's see what's the input that triggers this error/maze solution...
$ktest-tool klee-last/test000098.ktest
ktest file : 'klee-last/test000098.ktest'
args : ['maze_klee.o']
num objects: 1
object 0: name: 'program'
object 0: size: 29
object 0: data: 'sddwddddssssddwwww\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00'
So it propose the solution...
sddwddddssssddwwww
HEY! That's odd, it seems too short to even reach the other end of the maze! Lets try that input on the original maze...
Typical!! There are fake walls! And KLEE made its way through it! Excellent! But wait a minute it doesn't suppose to find every possible solution? Where is our trivial solution? Why KLEE was unable to find it?
Well in most cases (apparently) you need only one way to reach an error condition, so KLEE wont show you the other ways to reach the same error state. We desperately need to use one of the 10000 KLEE options. We need to run it like this..
$klee --emit-all-errors maze_klee.o
Check out the KLEE crazy run...
Now it gives 4 different "solutions"...
$ktest-tool klee-last/test000097.ktest
ktest file : 'klee-last/test000097.ktest'
args : ['maze_klee.o']
num objects: 1
object 0: name: 'program'
object 0: size: 29
object 0: data: '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 file : 'klee-last/test000136.ktest'
args : ['maze_klee.o']
num objects: 1
object 0: name: 'program'
object 0: size: 29
object 0: data: 'sddwddddssssddwwww\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00'
$ktest-tool klee-last/test000239.ktest
ktest file : 'klee-last/test000239.ktest'
args : ['maze_klee.o']
num objects: 1
object 0: name: 'program'
object 0: size: 29
object 0: data: 'ssssddddwwaawwddddsddw\x00\x00\x00\x00\x00\x00\x00'
$ktest-tool klee-last/test000268.ktest
ktest file : 'klee-last/test000268.ktest'
args : ['maze_klee.o']
num objects: 1
object 0: name: 'program'
object 0: size: 29
object 0: data: 'ssssddddwwaawwddddssssddwwww\x00'
There are 4 posible solutions!!
- ssssddddwwaawwddddssssddwwww
- ssssddddwwaawwddddsddw
- sddwddddssssddwwww
- sddwddddsddw
No comments:
Post a Comment