KLEE Slow Execution Compared to LLI

Open homyhost opened this issue 5 years ago • 1 comments

Dear all,

I am trying to execute part of a program symbolically. before using klee_make_symbolic() function, I have some functions which are supposed to be executed natively because I have not made anything symbolic yet. However, this part is executed much slower compared to when I execute it lli. I have tried it with KLEE 2.2-pre and KLEE 2.1-pre both. I also tried it with llvm 6 and llvm 7. In the following, you can find the command-line and execution time in each case: klee --optimize --libc=uclibc --posix-runtime ./bench.bc with execution time of: 1m44s lli-6.0 --force-interpreter=true bench.bc with execution time of: 15s

I extracted the problematic part and made a small benchmark as a proof of concept which is attached here.

Kind regards, Hooman Asadian

PoC.zip

Apr 17 '20 13:04 homyhost

This benchmark seems to have loads of stack arrays, I think it's the same issue as #332.

Apr 21 '20 10:04 kren1