******************* This email from originates from outside Imperial. Do not click on links and attachments unless you recognise the sender. If you trust the sender, add them to your safe senders list https://spam.ic.ac.uk/SpamConsole/Senders.aspx to disable email stamping for this address. ******************* Hi all,
I have run into a strange problem when running KLEE on some real programs. In my research project, I need to collect some hard-to-solve smt2 formulas from symbolic execution of programs. Given a specific timeout value, constraint solver like STP is not able to solve the collected formula and returns Timeout response. As I understand it, it's quite common that symbolic execution of large real-world programs produces path constraints that cannot be solved by state-of-the-art constraint solvers easily. However, when I used KLEE to analyse real program such as GNU bc version 1.07 even for 10 hours, KLEE didn't generate enough timeout constraints (only 10) if I set timeout value as 30s using the --max-solver-time= option. Futhermore, if I sent these generated constraints to STP solver used in KLEE backend and solved them independently, I found that these constraints were all solved very soon (under 5s). I'm quite confused about it. I generate constraints with the following command: $ klee --simplify-sym-indices --output-module --max-memory=1000 --use-forked-solver --use-cex-cache --disable-inlining --optimize --libc=uclibc --posix-runtime --external-calls=all --only-output-states-covering-new --watchdog --max-memory-inhibit=false --use-query-log=solver:smt2 --max-static-fork-pct=1 --max-static-solve-pct=1 --max-static-cpfork-pct=1 --dump-states-on-halt=false --max-sym-array-size=4096 --max-solver-time=30 --min-query-time-to-log=10 --max-time=36000 --search=random-path --search=nurs:covnew --use-batching-search --batch-instructions=10000 --write-smt2s ./bc.bc --sym-args 0 1 10 --sym-args 0 2 2 --sym-files 1 8 --sym-stdin 8 --sym-stdout My KLEE version: KLEE 2.1-pre (https://klee.github.io) Build mode: RelWithDebInfo (Asserts: ON) Build revision: 3af34e6095ee64332c089c98128dcfbcccced65e LLVM (http://llvm.org/): LLVM version 6.0.0 Optimized build. Default target: x86_64-pc-linux-gnu Host CPU: skylake My STP version: STP version 2.3.3 STP version SHA string 22007fb09bd91a0049109c8ab09a92b6475ca024 STP compilation options CMAKE_CXX_COMPILER = /usr/bin/c++ | CMAKE_CXX_FLAGS = -Wall -Wextra -Wunused -pedantic -Wsign-compare -fno-omit-frame-pointer -Wtype-limits -Wuninitialized -Wno-deprecated -Wstrict-aliasing -Wpointer-arith -Wpointer-arith -Wformat-nonliteral -Winit-self -Wparentheses -Wunreachable-code | COMPILE_DEFINES = -D__STDC_LIMIT_MACROS -DUSE_CRYPTOMINISAT | ONLY_SIMPLE = OFF | Boost_FOUND = 1 | STATICCOMPILE = OFF | TUNE_NATIVE = OFF | COVERAGE = OFF | FORCE_CMS = OFF | LIBS = /usr/local/lib/libminisat.so | ENABLE_TESTING = OFF | ENABLE_PYTHON_INTERFACE = ON | PYTHON_EXECUTABLE = /usr/bin/python2.7 | PYTHON_LIBRARY = /usr/lib/x86_64-linux-gnu/libpython2.7.so | PYTHON_INCLUDE_DIRS = /usr/include/python2.7 | | compilation date time = Nov 18 2019 06:46:27 c compiled with gcc version 5.4.0 20160609 Thank you so much. Regards, Ziqi Shuai
_______________________________________________ klee-dev mailing list [email protected] https://mailman.ic.ac.uk/mailman/listinfo/klee-dev
