The Symbolic Maze!

October 7, 2010

Follow feliam on Twitter

In this post we’ll exercise the symbolic execution engine KLEE over a funny ASCII Maze (yet another toy example)!

LLVM

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|     |#|
           | | --+ | |
           | |   | | |
           | +-- | | |
           |     |   |
           +-----+---+

The match is between a tiny maze-like game coded in C versus the full-fledged LLVM based symbolic execution engine, KLEE.

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+-- | | |
|     |   |
+-----+---+

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.

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!
Read the rest of this entry »

Follow

Get every new post delivered to your Inbox.