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 MazeThe 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 ...
It's really small I know! But the code hides a nasty trick, and at the end, you'll see, it has more than one way to solve it.
Player pos: 1x4 Iteration no. 2. Action: s. +-+---+---+ |X| |#| |X| --+ | | |X| | | | |X+-- | | | | | | +-----+---+
The KLEEKLEE 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 ideaUse KLEE to automatically solve our small puzzle.
Dissecting the codeLets take a walk through the maze code. First it hardcodes the map as a static global rw variable. Sets up a convenient function to draw the maze state on the screen... On the main function there are local variables to hold the position of the ''player'', the iteration counter, and a 28bytes array of the actions... The initial player position is set to (1,1), the first free cell in the map. And the player 'sprite' is the letter 'X' ... At this point we are ready to start! So it asks for directions. It reads all actions at once as an array of chars. It will execute up to ITERS iterations or commands. Now it iterates over the array of actions in variable 'program'... Different actions change the position of the player in the different axis and directions. As "usual"; a is Left, d is Right, w is Up and s is Down. Checks if the prize has been hit! If affirmative... You win! If something is wrong do not advance, backtrack to the saved state! If crashed to a wall or if you couldn't move! Exit, You lose! Ok, basically if we can move.. we move! Put the player in the correct position in the map. And draw the new state. Increment the iteration counter (used to select next action in the array), wait a second and loop. If you haven't won so far.. you lose. Ok, that's all of it.
By hand...Now considering you have it in maze.c. It should compile with a line like this
gcc maze.c -o maze
Run it! In a couple of tries you'll get to the priceless '#'. Maybe using this solution:
ssssddddwwaawwddddssssddwwwwYere you have a screen cast of me wining! Vivaaaa!!
By KLEELet'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.bcThat 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 ... ... by ... Also you will need to add the klee header at the beginning of the code... Now KLEE will find every possible code/maze path reachable from any input. If some of those paths lead to a typical error condition like a memory failure or such, KLEE will signal it! 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.bcHere 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.txtEach 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 ... ... by this two ... Now KLEE will assert a synthetic failure when it reaches the "You win state" (that means the 'player' hit the '#).OK, if you compile it to LLVM and run KLEE on the new version it flags one test case as being also an error...
$ls -1 klee-last/ |grep -A2 -B2 err test000096.ktest test000097.ktest test000098.assert.err test000098.ktest test000098.pcLet'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.oCheck 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!!