[klee-dev] KLEE Crashing
Daniel Schwartz
d.schwartz at columbia.edu
Thu Feb 22 18:37:46 GMT 2018
Hi,
I looked again to see if I missed a child process of this fork but didn't.
I provided all the information I have below:
When I check the running processes, I see:
9667: klee-1.4.0_build_dir/bin/klee --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=90000 --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=/jpeg-90000s-jpeg_hang_test
--min-query-time-to-log=-1 --track-instruction-time=true
libjpeg-read-klee.bc A -sym-files 1 1024 --sym-stdin 32
9668: klee-1.4.0_build_dir/bin/klee --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=90000 --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=/jpeg-90000s-jpeg_hang_test
--min-query-time-to-log=-1 --track-instruction-time=true
libjpeg-read-klee.bc A -sym-files 1 1024 --sym-stdin 32
It's process 9668 that is using 100% CPU and the backtrace as above, is:
(gdb) bt
#0 0x00002b160169ce34 in __libc_fork () at ../nptl/sysdeps/unix/sysv/
linux/x86_64/../fork.c:130
#1 0x000000000080f2a8 in runAndGetCexForked (timeout=0,
hasSolution=@0x7fff287aeaff: false, values=std::vector of length 0,
capacity 0, objects=std::vector of length 1, capacity 1 = {...},
q=0x1b0aceda0, builder=0x53e8290, vc=0x531e1c0) at
/home/dschwartz/klee-1.4.0/lib/Solver/STPSolver.cpp:234
#2 klee::STPSolverImpl::computeInitialValues (this=0x5b9d5d0, query=...,
objects=std::vector of length 1, capacity 1 = {...}, values=std::vector of
length 0, capacity 0,
hasSolution=@0x7fff287aeaff: false) at /home/dschwartz/klee-1.4.0/
lib/Solver/STPSolver.cpp:355
#3 0x00000000007fccc1 in CexCachingSolver::getAssignment
(this=this at entry=0x5d57ac0,
query=..., result=@0x7fff287aec40: 0x8886130)
at /home/dschwartz/klee-1.4.0/lib/Solver/CexCachingSolver.cpp:227
#4 0x00000000007fd89c in CexCachingSolver::computeTruth (this=0x5d57ac0,
query=..., isValid=@0x7fff287aeecf: false)
at /home/dschwartz/klee-1.4.0/lib/Solver/CexCachingSolver.cpp:311
#5 0x00000000007fbade in CachingSolver::computeTruth (this=0x5c31250,
query=..., isValid=@0x7fff287aeecf: false) at /home/dschwartz/klee-1.4.0/
lib/Solver/CachingSolver.cpp:234
#6 0x00000000008095f3 in IndependentSolver::computeTruth (this=0x5ea53e0,
query=..., isValid=@0x7fff287aeecf: false)
at /home/dschwartz/klee-1.4.0/lib/Solver/IndependentSolver.cpp:430
#7 0x00000000005ad77f in klee::TimingSolver::mustBeTrue (this=0x5d589f0,
state=..., expr=..., result=@0x7fff287aeecf: false)
at /home/dschwartz/klee-1.4.0/lib/Core/TimingSolver.cpp:58
#8 0x00000000005ad9e1 in klee::TimingSolver::mustBeFalse (this=0x5d589f0,
state=..., expr=..., result=@0x7fff287aeecf: false)
at /home/dschwartz/klee-1.4.0/lib/Core/TimingSolver.cpp:67
#9 0x00000000005ada58 in klee::TimingSolver::mayBeTrue (this=<optimized
out>, state=..., expr=..., result=@0x7fff287aef7f: true)
at /home/dschwartz/klee-1.4.0/lib/Core/TimingSolver.cpp:73
#10 0x000000000058ef95 in klee::Executor::executeInstruction
(this=this at entry=0x5fac0a0, state=..., ki=ki at entry=0x4b3a9b0)
at /home/dschwartz/klee-1.4.0/lib/Core/Executor.cpp:1734
#11 0x000000000059005e in klee::Executor::run (this=this at entry=0x5fac0a0,
initialState=...) at /home/dschwartz/klee-1.4.0/lib/Core/Executor.cpp:2947
#12 0x00000000005908fe in klee::Executor::runFunctionAsMain
(this=<optimized out>, f=<optimized out>, argc=7, argv=0x5eb57c0,
envp=<optimized out>)
at /home/dschwartz/klee-1.4.0/lib/Core/Executor.cpp:3762
#13 0x00000000005626ff in main (argc=37, argv=0x7fff287af928,
envp=<optimized out>) at /home/dschwartz/klee-1.4.0/tools/klee/main.cpp:1461
I don't see any children process for 9668.
The backtrace for 9667 is:
(gdb) bt
#0 0x00002b160169cd30 in __nanosleep_nocancel () at
../sysdeps/unix/syscall-template.S:81
#1 0x00002b160169cbe4 in __sleep (seconds=0) at ../sysdeps/unix/sysv/linux/
sleep.c:137
#2 0x0000000000561432 in main (argc=37, argv=0x7fff287af928,
envp=0x7fff287afa58) at /home/dschwartz/klee-1.4.0/tools/klee/main.cpp:1185
Thanks in advance for any help!
Best,
Daniel
On Mon, Feb 19, 2018 at 12:15 AM, Daniel Schwartz <d.schwartz at columbia.edu>
wrote:
> Thank you Martin.
>
> Here is the backtrace from gdb:
> (gdb) bt
> #0 0x00002b5816da8e34 in __libc_fork () at ../nptl/sysdeps/unix/sysv/linu
> x/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/Solv
> er/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/linu
> x/x86_64/../fork.c:130
> 130 ../nptl/sysdeps/unix/sysv/linux/x86_64/../fork.c: No such file or
> directory.
>
>
>
> 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
More information about the klee-dev
mailing list