[klee-dev] Constraint timeout problem

[帅子琦]

*******************
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
-------------- next part --------------
HTML attachment scrubbed and removed