The Symbolic Maze!
October 7, 2010
In this post we’ll exercise the symbolic execution engine KLEE over a funny ASCII Maze (yet another toy example)!
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 »