[klee-dev] KLEE for stateful C API

[Frank Busse]

Hi,


On Mon, 2 May 2022 09:50:23 +0200
Niklaus Leuenberger <niklaus.leuenb at gmail.com> wrote:

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

What I find a little odd here is that you drop the constraints of the
global state every time you get f_select == 0. Is this supposed to be a
reset and if so, would everything afterwards not be covered by a
similar path starting from the initial state?

> 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?

Hard to give recommendations without more knowledge about the problem.
In general: KLEE tries to execute all paths - if your program has a lot
of paths, than that's the issue. ;) You can also play with KLEE's flags,
e.g. disable test generation (--write-no-tests) or use a less expensive
search strategy (--search=[dfs,bfs,random-state]).

You can also check KLEE's stats to see where it spends time or branches
heavily, see: https://klee.github.io/tutorials/testing-coreutils/ (Step
6).



Kind regards,

Frank