| Age | Commit message (Collapse) | Author |
|---|
|
|
|
|
|
Otherwise optimizations done in klee won't have any effect.
Signed-off-by: Jiri Slaby <jirislaby@gmail.com>
|
|
``test/Feature/SolverTimeout.c`` test fails there.
The error message I see in TravisCI is
```
Command 2: "/home/travis/build/klee/build/klee/Release+Asserts/bin/klee" "--output-dir=/home/travis/build/klee/build/klee/test/Feature/Output/SolverTimeout.c.tmp.klee-out" "--max-solver-time=1" "/home/travis/build/klee/build/klee/test/Feature/Output/SolverTimeout.c.tmp1.bc"
Command 2 Result: -11
Command 2 Output:
Command 2 Stderr:
KLEE: output directory is "/home/travis/build/klee/build/klee/test/Feature/Output/SolverTimeout.c.tmp.klee-out"
KLEE: WARNING: undefined reference to function: printf
KLEE: ERROR: (location information missing) divide by zero
KLEE: NOTE: now ignoring this error at this location
0 klee 0x0000000000da87d2 llvm::sys::PrintStackTrace(_IO_FILE*) + 34
1 klee 0x0000000000da85c9
2 libpthread.so.0 0x00007fca19936cb0
3 libz3.so 0x00007fca19079826
4 librt.so.1 0x00007fca1747640c
5 libpthread.so.0 0x00007fca1992ee9a
6 libc.so.6 0x00007fca1776c38d clone + 109
```
The issue appears to be racey as I had to run several copies of KLEE in
parallel for the bug to occur using Z3 4.4.1. I managed to get a
coredump and got the backtrace from gdb for the crash which is
```
#0 0x00007f4841b11c46 in scoped_timer::imp::sig_handler (s=..., s@entry=...) at ../src/util/scoped_timer.cpp:112
#1 0x00007f484031e0ff in timer_sigev_thread (arg=0x7f48380008c0) at ../nptl/sysdeps/unix/sysv/linux/timer_routines.c:63
#2 0x00007f484291c182 in start_thread (arg=0x7f483db46700) at pthread_create.c:312
#3 0x00007f484061b47d in clone () at ../sysdeps/unix/sysv/linux/x86_64/clone.S:111
```
The crash appears to be in Z3 itself but I can't reproduce the issue when using the
version of Z3 from the master branch.
For now we simply workaround the issue by not running the
``test/Feature/SolverTimeout.c`` test when using Z3 as the solver.
We should revisit this issue when another stable release of Z3 is made.
|
|
parallel.
- It would be nice if there was an easier way to do this that didn't involve
editing all of the tests (like running each test in its own directory), but
this approach fixes #146 and doesn't involve changing 'lit' or writing a
wrapper harness. My assumption is a lot of tests start are derived from
another one, so hopefully following this convention won't be burdensome, and
I updated 'make check' so that it will produce an error if any test runs klee
without --output-dir (by checking for the existing of klee-last files).
- This also helps with #147 but I still can't fully run tests in parallel (I
start hitting STP errors).
|
|
STP. More specifically, command-line options max-stp-time, use-forked-stp and stp-optimize-divides renamed to max-solver-time, use-forked-solver and solver-optimize-divides, respectively.
Option of running the SMT solver in a separate process (i.e. forked) set to true by default.
Options of running SMT solver forked and with optimized divides made available to Kleaver as well.
|
|
also used. Thanks to Paul Marinescu for reporting and debugging this.
The patch also disables the STP timeout by default.
git-svn-id: https://llvm.org/svn/llvm-project/klee/trunk@154300 91177308-0d34-0410-b5e6-96231b3b80d8
|
