Can the return value of a function call be made symbolic so as to bypass executing that function?

Question

I want avoid doing inter-procedural symbolic execution. Perhaps have a return value that would not have any constraints and might resolve to any possible concrete value.

Is something like this even possible?

The reason I want to do this is that I want to avoid executing certain functions that have a very very big loop and dont really modify global data.

Answer 1

Such functionality is not implemented in Klee. If you want to achieve it, you have to perform that yourself.

The file you should look at is lib/Core/Executor.cpp. Executor handles the job to execute instructions symbolically. The specific function you need to change is called "executeCall". You can check the name of the function. If that matches your target, just set the program counter to the next instruction, and make the returned value as symbolic.

With some work of programming, I think your need is achievable.

Answer 2

If it is possible to manipulate the source code, you can replace those function calls with make_symbolic function where you basically create a fresh symbolic variable and return it as the return of the original function call. Or you could just override those functions to return a fresh symbolic value.