[klee-dev] KLEE Crashing

[Daniel Schwartz]

Hi All,

I've been running KLEE on various test files and sometimes KLEE stops
forward progression. I've copied information on one such instance below.
Does anyone know what is going on?


Run command:
$ klee-1.4.0 --libc=uclibc --posix-runtime --simplify-sym-indices
--write-cvcs --write-cov --output-module --max-memory=4096
--disable-inlining --use-forked-solver --use-cex-cache
--allow-external-sym-calls  --max-sym-array-size=4096
--max-instruction-time=30. --max-time=10800 --watchdog
--max-memory-inhibit=false --max-solver-time=1  --max-static-fork-pct=1
--max-static-solve-pct=1 --max-static-cpfork-pct=1 --switch-type=internal
--dump-states-on-halt=false --search=random-path --search=nurs:covnew
--use-batching-search --batch-instructions=10000  --output-dir=/test
--min-query-time-to-log=-1 test.bc A -sym-files 1 1024 --sym-stdin 32


>From the log:
KLEE: WARNING: KLEE: WATCHDOG: time expired, attempting halt via INT

KLEE: ctrl-c detected, requesting interpreter to halt.
KLEE: WARNING: KLEE: WATCHDOG: time expired, attempting halt via gdb

Could not attach to process.  If your uid matches the uid of the target
process, check the setting of /proc/sys/kernel/yama/ptrace_scope, or try
again as the root user.  For more details, see /etc/sysctl.d/10-ptrace.conf
ptrace: Operation not permitted.
No symbol table is loaded.  Use the "file" command.
The program is not being run.
KLEE: WARNING: KLEE: WATCHDOG: kill(9)ing child (I tried to be nice)


Additionally, as shown below, the autogenerated run.stats file (and the
klee output directory) is last updated just under 103 minutes into the 180
minute scheduled run.

$ head -1 run.stats; tail -1 run.stats
('Instructions','FullBranches','PartialBranches','NumBranches','UserTime','NumStates','MallocUsage','NumQueries','NumQueryConstructs','NumObjects','WallTime','CoveredInstructions','UncoveredInstructions','QueryTime','SolverTime','CexCacheTime','ForkTime','ResolveTime',)
(20965396,137,280,3226,1.401079e+03,477132,255130544,11460,740979,0,6.134754e+03,6993,93406,4.716927e+03,5.195885e+03,4.722587e+03,6.962366e+02,6.936041e+00)


I welcome all comments/suggestions on better usage of KLEE's configuration
options and am happy to provide more diagnostic information from my
problematic runs.



*********************************
Daniel Schwartz - ds3263 at columbia.edu
M.S. Candidate, Computer Science
Columbia University, 2018
https://www.linkedin.com/in/danielschwartz2/
-------------- next part --------------
HTML attachment scrubbed and removed