Hi Martin, Done. Thank you again.
Thanks, Daniel ********************************* Daniel Schwartz - [email protected] 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 <[email protected] > 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 <[email protected]> > 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@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@entry=0x5fac0a0, state=..., ki=ki@entry=0x4b3a9b0) > > at /home/dschwartz/klee-1.4.0/lib/Core/Executor.cpp:1734 > > #11 0x000000000059005e in klee::Executor::run (this=this@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 < > [email protected]> 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@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@entry=0x431b240, state=..., ki=ki@entry=0x4b4f8a0) > > at [redacted]/klee-1.4.0/lib/Core/Executor.cpp:1734 > > #11 0x000000000059005e in klee::Executor::run (this=this@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 < > [email protected]> 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: [email protected] > > ---------------------------------------------------- > > > > > > > > --------------------------------------------------- > Martin Nowack > Research Assistant > > Technische Universität Dresden > Computer Science > Institute of Systems Architecture > Systems Engineering > 01062 Dresden > > Phone: +49 351 463 39608 > Email: [email protected] > ---------------------------------------------------- > >
_______________________________________________ klee-dev mailing list [email protected] https://mailman.ic.ac.uk/mailman/listinfo/klee-dev
