[klee-dev] KLEE Crashing

[Daniel Schwartz]

Thank you Martin.

Here is the backtrace from gdb:
(gdb) bt
#0  0x00002b5816da8e34 in __libc_fork () at
../nptl/sysdeps/unix/sysv/linux/x86_64/../fork.c:130
#1  0x000000000080f0b8 in runAndGetCexForked (timeout=0,
hasSolution=@0x7fffb2ea1cbf: false, values=std::vector of length 0,
capacity 0, objects=std::vector of length 1, capacity 1 = {...},
    q=0x203ec87b0, builder=0x43cbd00, vc=0x4c35bc0) at
[redacted]/klee-1.4.0/lib/Solver/STPSolver.cpp:234
#2  klee::STPSolverImpl::computeInitialValues (this=0x51dc920, query=...,
objects=std::vector of length 1, capacity 1 = {...}, values=std::vector of
length 0, capacity 0,
    hasSolution=@0x7fffb2ea1cbf: false) at [redacted]
/klee-1.4.0/lib/Solver/STPSolver.cpp:355
#3  0x00000000007fcad1 in CexCachingSolver::getAssignment
(this=this at entry=0x4c62390,
query=..., result=@0x7fffb2ea1e00: 0x7bf40a0)
    at [redacted]/klee-1.4.0/lib/Solver/CexCachingSolver.cpp:227
#4  0x00000000007fd6ac in CexCachingSolver::computeTruth (this=0x4c62390,
query=..., isValid=@0x7fffb2ea208f: false)
    at [redacted]/klee-1.4.0/lib/Solver/CexCachingSolver.cpp:311
#5  0x00000000007fb8ee in CachingSolver::computeTruth (this=0x4fc9850,
query=..., isValid=@0x7fffb2ea208f: false) at [redacted]/
klee-1.4.0/lib/Solver/CachingSolver.cpp:234
#6  0x0000000000809403 in IndependentSolver::computeTruth (this=0x51783e0,
query=..., isValid=@0x7fffb2ea208f: false)
    at [redacted]/klee-1.4.0/lib/Solver/IndependentSolver.cpp:430
#7  0x00000000005ad58f in klee::TimingSolver::mustBeTrue (this=0x3860df0,
state=..., expr=..., result=@0x7fffb2ea208f: false)
    at [redacted]/klee-1.4.0/lib/Core/TimingSolver.cpp:58
#8  0x00000000005ad7f1 in klee::TimingSolver::mustBeFalse (this=0x3860df0,
state=..., expr=..., result=@0x7fffb2ea208f: false)
    at [redacted]/klee-1.4.0/lib/Core/TimingSolver.cpp:67
#9  0x00000000005ad868 in klee::TimingSolver::mayBeTrue (this=<optimized
out>, state=..., expr=..., result=@0x7fffb2ea213f: true)
    at [redacted]/klee-1.4.0/lib/Core/TimingSolver.cpp:73
#10 0x000000000058ef95 in klee::Executor::executeInstruction
(this=this at entry=0x431b240, state=..., ki=ki at entry=0x4b4f8a0)
    at [redacted]/klee-1.4.0/lib/Core/Executor.cpp:1734
#11 0x000000000059005e in klee::Executor::run (this=this at entry=0x431b240,
initialState=...) at [redacted]/klee-1.4.0/lib/Core/Executor.cpp:2947
#12 0x00000000005908fe in klee::Executor::runFunctionAsMain
(this=<optimized out>, f=<optimized out>, argc=7, argv=0x49ae670,
envp=<optimized out>)
    at [redacted]/klee-1.4.0/lib/Core/Executor.cpp:3762
#13 0x00000000005626ff in main (argc=36, argv=0x7fffb2ea2ae8,
envp=<optimized out>) at [redacted]/klee-1.4.0/tools/klee/main.cpp:1461


Here are the last 3 lines of gdb output from running:
$ gdb attach [pid]
Loaded symbols for /lib64/ld-linux-x86-64.so.2
0x00002b5816da8e34 in __libc_fork () at
../nptl/sysdeps/unix/sysv/linux/x86_64/../fork.c:130
130 ../nptl/sysdeps/unix/sysv/linux/x86_64/../fork.c: No such file or
directory.




*********************************
Daniel Schwartz - ds3263 at columbia.edu
M.S. Candidate, Computer Science
Columbia University, 2018
https://www.linkedin.com/in/danielschwartz2/

On Wed, Feb 14, 2018 at 3:00 AM, Martin Nowack <martin.nowack1 at tu-dresden.de
> wrote:

> Hi Daniel,
>
> KLEE is not crashing but the timeout (--max-time=10800) is reached.
> The thing what happens in your case is that the KLEE watchdog process
> tries to kill KLEE vie attaching to it using gdb. So KLEE does not
> terminate or does not have enough time to terminate.
>
> It could be that KLEE is waiting on an external call which does not return.
> Try to attach via gdb to the KLEE process (remember you have to take the
> child pid) and make a backtrace so we would know more.
>
> For this one, you have to change the ptrace_scope:
>
> > 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.
>
> Best,
> Martin
> ---------------------------------------------------
> Martin Nowack
> Research Assistant
>
> Technische Universität Dresden
> Computer Science
> Institute of Systems Architecture
> Systems Engineering
> 01062 Dresden
>
> Phone: +49 351 463 39608
> Email: martin.nowack1 at tu-dresden.de
> ----------------------------------------------------
>
>
-------------- next part --------------
HTML attachment scrubbed and removed