[klee-dev] KLEE Crashing
Martin Nowack
martin.nowack1 at tu-dresden.de
Thu Feb 22 21:12:45 GMT 2018
Hi Daniel,
This is strange - hanging at __libc_fork() with 100% cpu load should not happen.
Can you open a bug report on GitHub and we try to continue there?
* And could you add there what system you have (Linux distribution)
* Add the code around: __libc_fork () at ../nptl/sysdeps/unix/sysv/linux/x86_64/../fork.c:130,
I would like to know what’s going on there.
Thanks a lot,
Martin
> On 22. Feb 2018, at 19:37, Daniel Schwartz <d.schwartz at columbia.edu> wrote:
>
> 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/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.
>
>
>
> 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
> ----------------------------------------------------
>
>
>
---------------------------------------------------
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 --------------
A non-text attachment was scrubbed...
Name: smime.p7s
Type: application/pkcs7-signature
Size: 5101 bytes
Desc: not available
URL: <http://mailman.ic.ac.uk/pipermail/klee-dev/attachments/20180222/d95d868e/attachment.p7s>
More information about the klee-dev
mailing list