[klee-dev] KLEE for stateful C API

[Niklaus Leuenberger]

Hello klee-dev members,

I'm currently testing out a few approaches on how to test and fuzz a
stateful C API. In the process thereof I found KLEE and am fascinated
by it. I managed to get it to work and am now asking if my approach is
ok or if it has some major drawbacks or problems.

Let's suppose we have following simple but buggy stateful API:
---
#include <assert.h>
static int g_state;
void setState(int state) {
    g_state = state;
}
void run(void) {
    if (g_state == 123) {
        assert(0);
    }
}
---
If the state is set to 123 and then run() is invoked the placed assertion fails.

For this I have written following KLEE harness:
---
#include "klee/klee.h"
#include "buggy_api.h"
int main(void) {
    for (int i = 0; i < 2; ++i) { // sequentially call 2 APIs
        int f_select = klee_choose(2); // what API to call
        if (f_select == 0) {
            int state = 0;
            klee_make_symbolic(&state, sizeof(state), "state");
            setState(state);
        } else if (f_select == 1) {
            run();
        }
    }
    return 0;
}
---

When running with KLEE, the sequence of calls necessary to trigger the
assertion is found almost immediately. But when extending it with more
functions, each doubles the runtime. So it scales rather poorly on
larger APIs.
Is this how I can use KLEE for checking an API? Or does someone have
pointers to a better approach?

Best Regards,
Niklaus Leuenberger