A Driver for the Symbolic Maze

maze_driver.c

#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];

    mcsema_main(&rState);

    return rState.EAX;
}

// klee_make_symbolic_range taken from:
// https://keeda.stanford.edu/pipermail/klee-dev/2011-July/000685.html
// 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)
                return;

        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);
        free(symbolic_data);
}

// 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
                klee_assert(0);
        }
}

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);
}