[klee-dev] KLEE Crashing
Daniel Schwartz
d.schwartz at columbia.edu
Thu Feb 22 21:39:01 GMT 2018
Hi Martin,
Done. Thank you again.
Thanks,
Daniel
*********************************
Daniel Schwartz - ds3263 at columbia.edu
M.S. Candidate, Computer Science
Columbia University, 2018
https://www.linkedin.com/in/danielschwartz2/
On Thu, Feb 22, 2018 at 4:12 PM, Martin Nowack <martin.nowack1 at tu-dresden.de
> wrote:
> 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 --------------
HTML attachment scrubbed and removed
More information about the klee-dev
mailing list