Created
November 24, 2014 03:14
-
-
Save artemdinaburg/acda0f88215f3efdddc8 to your computer and use it in GitHub Desktop.
A Driver for the Symbolic Maze
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
#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); | |
} |
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment