Re: [klee-dev] KLEE aborts with tcmalloc error
As you can see from the log ("LLVM ERROR: out of memory") the run
exhausted all available memory. This is not that surprising for a 36h
run. When you enable query logging, memory consumption increases
further, as the textual representation of the queries can become massive
after a long run.
Best,
Cristian
On 16/04/2020 09:31, Hooman wrote:
Dear all,
I run klee with following options:
klee --simplify-sym-indices --write-cvcs --write-cov --output-module
--disable-inlining --optimize --use-forked-solver --use-cex-cache
--libc=uclibc --posix-runtime --external-calls=all
--only-output-states-covering-new --max-memory-inhibit=false
--max-static-fork-pct=1 --max-static-solve-pct=1
--max-static-cpfork-pct=1 --switch-type=internal --search=random-path
--search=nurs:covnew --max-memory=16000 --max-sym-array-size=4096
-use-query-log=solver:smt2 -log-timed-out-queries
-min-query-time-to-log=20 --max-solver-time=20
after like 36 hours of running I get the attached results and klee
aborts. The interesting fact is that when I run the same experiment
without -use-query-log=solver:smt2 -log-timed-out-queries
-min-query-time-to-log=20 options, the experiment finishes. I would
appreciate any help.
Kind regards,
Hooman
Attached error upon abortion:
tcmalloc: large alloc 1330126848 bytes == 0x55d304afc000 @
0x7fcd3a5bff2d 0x7fcd3a5dff8b 0x7fcd36b25eeb 0x7fcd36b27483
0x7fcd37542edf 0x55cef2d2c686 0x55cef2d32cc7 0x55cef2d33c12
0x55cef2d34038 0x55cef2d334f8 0x55cef2d334ca 0x55cef2d334ca
0x55cef2d334ca 0x55cef2d334ca 0x55cef2d334ca 0x55cef2d334ca
0x55cef2d334ca 0x55cef2d334ca 0x55cef2d334ca 0x55cef2d334ca
0x55cef2d334ca 0x55cef2d334ca 0x55cef2d334ca 0x55cef2d334ca
0x55cef2d334ca 0x55cef2d334ca 0x55cef2d334ca 0x55cef2d334ca
0x55cef2d334ca 0x55cef2d334ca 0x55cef2d334ca
tcmalloc: large alloc 2660245504 bytes == 0x55d353f7e000 @
0x7fcd3a5bff2d 0x7fcd3a5dff8b 0x7fcd36b25eeb 0x7fcd36b27483
0x7fcd37542edf 0x55cef2d35438 0x55cef2d33dde 0x55cef2d34038
0x55cef2d345ad 0x55cef2d33e6d 0x55cef2d34038 0x55cef2d356b0
0x55cef2d33dde 0x55cef2d34038 0x55cef2d345ad 0x55cef2d33e6d
0x55cef2d34038 0x55cef2d3676e 0x55cef2d33d3d 0x55cef2d34038
0x55cef2d345ad 0x55cef2d33e6d 0x55cef2d34038 0x55cef2d356b0
0x55cef2d33dde 0x55cef2d34038 0x55cef2d345ad 0x55cef2d33e6d
0x55cef2d34038 0x55cef2d345ad 0x55cef2d33e6d
tcmalloc: large alloc 5320482816 bytes == 0x55d3f308 @
0x7fcd3a5bff2d 0x7fcd3a5dff8b 0x7fcd36b25eeb 0x7fcd36b27483
0x7fcd37542edf 0x55cef2d2c686 0x55cef2d32dbd 0x55cef2d33c12
0x55cef2d34038 0x55cef2d334f8 0x55cef2d334ca 0x55cef2d334ca
0x55cef2d334ca 0x55cef2d334ca 0x55cef2d334ca 0x55cef2d334ca
0x55cef2d334ca 0x55cef2d334ca 0x55cef2d334ca 0x55cef2d334ca
0x55cef2d334ca 0x55cef2d334ca 0x55cef2d334ca 0x55cef2d334ca
0x55cef2d334ca 0x55cef2d334ca 0x55cef2d334ca 0x55cef2d334ca
0x55cef2d334ca 0x55cef2d334ca 0x55cef2d334ca
tcmalloc: large alloc 10640957440 bytes == 0x55d530282000 @
0x7fcd3a5bff2d 0x7fcd3a5dff8b 0x7fcd36b25eeb 0x7fcd36b27483
0x7fcd37542edf 0x55cef2d34478 0x55cef2d33e6d 0x55cef2d34038
0x55cef2d356b0 0x55cef2d33dde 0x55cef2d34038 0x55cef2d345ad
0x55cef2d33e6d 0x55cef2d34038 0x55cef2d3676e 0x55cef2d33d3d
0x55cef2d34038 0x55cef2d345ad 0x55cef2d33e6d 0x55cef2d34038
0x55cef2d356b0 0x55cef2d33dde 0x55cef2d34038 0x55cef2d345ad
0x55cef2d33e6d 0x55cef2d34038 0x55cef2d345ad 0x55cef2d33e6d
0x55cef2d34038 0x55cef2d35111 0x55cef2d33d8b
tcmalloc: large alloc 21281906688 bytes == (nil) @ 0x7fcd3a5bff2d
0x7fcd3a5dff8b 0x7fcd36b25eeb 0x7fcd36b27483 0x7fcd37542edf
0x55cef2d33460 0x55cef2d334ca 0x55cef2d334ca 0x55cef2d334ca
0x55cef2d334ca 0x55cef2d334ca 0x55cef2d334ca 0x55cef2d334ca
0x55cef2d334ca 0x55cef2d334ca 0x55cef2d334ca 0x55cef2d334ca
0x55cef2d334ca 0x55cef2d334ca 0x55cef2d334ca 0x55cef2d334ca
0x55cef2d334ca 0x55cef2d334ca 0x55cef2d334ca 0x55cef2d334ca
0x55cef2d334ca 0x55cef2d334ca 0x55cef2d334ca 0x55cef2d334ca
0x55cef2d334ca 0x55cef2d334ca
LLVM ERROR: out of memory
LLVMSymbolizer: error reading file: No such file or directory
#0 0x7fcd3755ec2f llvm::sys::PrintStackTrace(llvm::raw_ostream&)
(/usr/lib/llvm-7/lib/libLLVM-7.so.1+0x9cec2f)
#1 0x7fcd3755d132 llvm::sys::RunSignalHandlers()
(/usr/lib/llvm-7/lib/libLLVM-7.so.1+0x9cd132)
#2 0x7fcd3755ef42 (/usr/lib/llvm-7/lib/libLLVM-7.so.1+0x9cef42)
#3 0x7fcd366cf840 (/lib/x86_64-linux-gnu/libc.so.6+0x37840)
#4 0x7fcd366cf7bb gsignal (/lib/x86_64-linux-gnu/libc.so.6+0x377bb)
#5 0x7fcd366ba535 abort (/lib/x86_64-linux-gnu/libc.so.6+0x22535)
#6 0x7fcd374f8e13 llvm::report_bad_alloc_error(char const*, bool)
(/usr/lib/llvm-7/lib/libLLVM-7.so.1+0x968e13)
#7 0x7fcd374f8e92 (/usr/lib/llvm-7/lib/libLLVM-7.so.1+0x968e92)
#8 0x7fcd3a5bf748 _init
(/usr/lib/x86_64-linux-gnu/libtcmalloc.so.4+0x17748)
#9 0x7fcd3a5dfef5 tcmalloc::allocate_full_cpp_throw_oom(unsigned
long) (/usr/lib/x86_64-linux-gnu/libtcmalloc.so.4+0x37ef5)
#10 0x7fcd36b25eeb std::__cxx11::basic_stringstd::char_traits, std::allocator
[klee-dev] KLEE aborts with tcmalloc error
*** This email originates from outside Imperial. Do not click on links and attachments unless you recognise the sender. If you trust the sender, add them to your safe senders list https://spam.ic.ac.uk/SpamConsole/Senders.aspx to disable email stamping for this address. *** Dear all, I run klee with following options: klee --simplify-sym-indices --write-cvcs --write-cov --output-module --disable-inlining --optimize --use-forked-solver --use-cex-cache --libc=uclibc --posix-runtime --external-calls=all --only-output-states-covering-new --max-memory-inhibit=false --max-static-fork-pct=1 --max-static-solve-pct=1 --max-static-cpfork-pct=1 --switch-type=internal --search=random-path --search=nurs:covnew --max-memory=16000 --max-sym-array-size=4096 -use-query-log=solver:smt2 -log-timed-out-queries -min-query-time-to-log=20 --max-solver-time=20 after like 36 hours of running I get the attached results and klee aborts. The interesting fact is that when I run the same experiment without -use-query-log=solver:smt2 -log-timed-out-queries -min-query-time-to-log=20 options, the experiment finishes. I would appreciate any help. Kind regards, Hooman Attached error upon abortion: tcmalloc: large alloc 1330126848 bytes == 0x55d304afc000 @ 0x7fcd3a5bff2d 0x7fcd3a5dff8b 0x7fcd36b25eeb 0x7fcd36b27483 0x7fcd37542edf 0x55cef2d2c686 0x55cef2d32cc7 0x55cef2d33c12 0x55cef2d34038 0x55cef2d334f8 0x55cef2d334ca 0x55cef2d334ca 0x55cef2d334ca 0x55cef2d334ca 0x55cef2d334ca 0x55cef2d334ca 0x55cef2d334ca 0x55cef2d334ca 0x55cef2d334ca 0x55cef2d334ca 0x55cef2d334ca 0x55cef2d334ca 0x55cef2d334ca 0x55cef2d334ca 0x55cef2d334ca 0x55cef2d334ca 0x55cef2d334ca 0x55cef2d334ca 0x55cef2d334ca 0x55cef2d334ca 0x55cef2d334ca tcmalloc: large alloc 2660245504 bytes == 0x55d353f7e000 @ 0x7fcd3a5bff2d 0x7fcd3a5dff8b 0x7fcd36b25eeb 0x7fcd36b27483 0x7fcd37542edf 0x55cef2d35438 0x55cef2d33dde 0x55cef2d34038 0x55cef2d345ad 0x55cef2d33e6d 0x55cef2d34038 0x55cef2d356b0 0x55cef2d33dde 0x55cef2d34038 0x55cef2d345ad 0x55cef2d33e6d 0x55cef2d34038 0x55cef2d3676e 0x55cef2d33d3d 0x55cef2d34038 0x55cef2d345ad 0x55cef2d33e6d 0x55cef2d34038 0x55cef2d356b0 0x55cef2d33dde 0x55cef2d34038 0x55cef2d345ad 0x55cef2d33e6d 0x55cef2d34038 0x55cef2d345ad 0x55cef2d33e6d tcmalloc: large alloc 5320482816 bytes == 0x55d3f308 @ 0x7fcd3a5bff2d 0x7fcd3a5dff8b 0x7fcd36b25eeb 0x7fcd36b27483 0x7fcd37542edf 0x55cef2d2c686 0x55cef2d32dbd 0x55cef2d33c12 0x55cef2d34038 0x55cef2d334f8 0x55cef2d334ca 0x55cef2d334ca 0x55cef2d334ca 0x55cef2d334ca 0x55cef2d334ca 0x55cef2d334ca 0x55cef2d334ca 0x55cef2d334ca 0x55cef2d334ca 0x55cef2d334ca 0x55cef2d334ca 0x55cef2d334ca 0x55cef2d334ca 0x55cef2d334ca 0x55cef2d334ca 0x55cef2d334ca 0x55cef2d334ca 0x55cef2d334ca 0x55cef2d334ca 0x55cef2d334ca 0x55cef2d334ca tcmalloc: large alloc 10640957440 bytes == 0x55d530282000 @ 0x7fcd3a5bff2d 0x7fcd3a5dff8b 0x7fcd36b25eeb 0x7fcd36b27483 0x7fcd37542edf 0x55cef2d34478 0x55cef2d33e6d 0x55cef2d34038 0x55cef2d356b0 0x55cef2d33dde 0x55cef2d34038 0x55cef2d345ad 0x55cef2d33e6d 0x55cef2d34038 0x55cef2d3676e 0x55cef2d33d3d 0x55cef2d34038 0x55cef2d345ad 0x55cef2d33e6d 0x55cef2d34038 0x55cef2d356b0 0x55cef2d33dde 0x55cef2d34038 0x55cef2d345ad 0x55cef2d33e6d 0x55cef2d34038 0x55cef2d345ad 0x55cef2d33e6d 0x55cef2d34038 0x55cef2d35111 0x55cef2d33d8b tcmalloc: large alloc 21281906688 bytes == (nil) @ 0x7fcd3a5bff2d 0x7fcd3a5dff8b 0x7fcd36b25eeb 0x7fcd36b27483 0x7fcd37542edf 0x55cef2d33460 0x55cef2d334ca 0x55cef2d334ca 0x55cef2d334ca 0x55cef2d334ca 0x55cef2d334ca 0x55cef2d334ca 0x55cef2d334ca 0x55cef2d334ca 0x55cef2d334ca 0x55cef2d334ca 0x55cef2d334ca 0x55cef2d334ca 0x55cef2d334ca 0x55cef2d334ca 0x55cef2d334ca 0x55cef2d334ca 0x55cef2d334ca 0x55cef2d334ca 0x55cef2d334ca 0x55cef2d334ca 0x55cef2d334ca 0x55cef2d334ca 0x55cef2d334ca 0x55cef2d334ca 0x55cef2d334ca LLVM ERROR: out of memory LLVMSymbolizer: error reading file: No such file or directory #0 0x7fcd3755ec2f llvm::sys::PrintStackTrace(llvm::raw_ostream&) (/usr/lib/llvm-7/lib/libLLVM-7.so.1+0x9cec2f) #1 0x7fcd3755d132 llvm::sys::RunSignalHandlers() (/usr/lib/llvm-7/lib/libLLVM-7.so.1+0x9cd132) #2 0x7fcd3755ef42 (/usr/lib/llvm-7/lib/libLLVM-7.so.1+0x9cef42) #3 0x7fcd366cf840 (/lib/x86_64-linux-gnu/libc.so.6+0x37840) #4 0x7fcd366cf7bb gsignal (/lib/x86_64-linux-gnu/libc.so.6+0x377bb) #5 0x7fcd366ba535 abort (/lib/x86_64-linux-gnu/libc.so.6+0x22535) #6 0x7fcd374f8e13 llvm::report_bad_alloc_error(char const*, bool) (/usr/lib/llvm-7/lib/libLLVM-7.so.1+0x968e13) #7 0x7fcd374f8e92 (/usr/lib/llvm-7/lib/libLLVM-7.so.1+0x968e92) #8 0x7fcd3a5bf748 _init (/usr/lib/x86_64-linux-gnu/libtcmalloc.so.4+0x17748) #9 0x7fcd3a5dfef5 tcmalloc::allocate_full_cpp_throw_oom(unsigned long) (/usr/lib/x86_64-linux-gnu/libtcmalloc.so.4+0x37ef5) #10 0x7fcd36b25eeb std::__cxx11::basic_stringstd::char_traits, std::allocator >::_M_mutate(unsigned long, unsigned long,
