Skip to content

Instantly share code, notes, and snippets.

What would you like to do?
A Driver for the Symbolic Maze
#include <klee/klee.h>
#include <stdlib.h>
#include "RegisterState.h"
extern int mcsema_main(RegState *);
// this will call the main() of the original application
// Note: mcsema includes the option to auto-generate these drivers
// but they will *NOT* work with KLEE, because the auto generation
// code uses mmap(), which KLEE can't deal with.
int maze_driver(int argc, const char* argv[])
RegState rState;
unsigned long stack[4096*10];
memset(&rState, 0, sizeof(rState));
//set up the stack
stack[(4096*9)+1] = (uint32_t)argc;
stack[(4096*9)+2] = (uint32_t)argv;
rState.ESP = (unsigned long) &stack[4096*9];
return rState.EAX;
// klee_make_symbolic_range taken from:
// This function marks a part of memory as symbolic by creating a
// new allocation and copying it over an existing memory area.
// The existing area will then become symbolic.
void klee_make_symbolic_range(void* addr, size_t offset,
size_t nbytes, const char* name) {
assert(addr != NULL && "Must pass a valid addr");
assert(name != NULL && "Must pass a valid name");
if(nbytes == 0)
void* start = addr + offset;
klee_check_memory_access(start, nbytes);
void* symbolic_data = malloc(nbytes);
klee_make_symbolic(symbolic_data, nbytes, name);
memcpy(start, symbolic_data, nbytes);
// this will override the read() imported by
// the original maze program.
// Any data processed by the read() call
// will become symbolic input
int read(int fd, char* input, size_t size) {
klee_make_symbolic_range(input, 0, size, "syminput");
return 0;
// this will override the exit() imported by
// the original maze program.
// When the exit status code is 1, the maze has a solution.
// to help us identify successful solutions, we will throw
// a klee assert so we can easily find correct solutions
// amongst all the results.
int exit(int status) {
if(status == 1) {
// mark when we found success
int sleep(int seconds) {
// disable sleep since the default sleep will use signals
// and that will interfere with KLEE.
// KLEE might be able to handle it with the
// -posix-runtime switch, but we redefine stdlib primitives
// that will conflict with -posix-runtime
return 0;
// simply call the original program's main
int main(int argc, const char *argv[]) {
return maze_driver(argc, argv);
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
You can’t perform that action at this time.