[klee-dev] KLEE aborts with tcmalloc error

Thu Apr 16 09:31:50 BST 2020

*******************
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 == 0x55d3f3080000 @ 
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 0x00007fcd3755ec2f llvm::sys::PrintStackTrace(llvm::raw_ostream&) 
(/usr/lib/llvm-7/lib/libLLVM-7.so.1+0x9cec2f)
#1 0x00007fcd3755d132 llvm::sys::RunSignalHandlers() 
(/usr/lib/llvm-7/lib/libLLVM-7.so.1+0x9cd132)
#2 0x00007fcd3755ef42 (/usr/lib/llvm-7/lib/libLLVM-7.so.1+0x9cef42)
#3 0x00007fcd366cf840 (/lib/x86_64-linux-gnu/libc.so.6+0x37840)
#4 0x00007fcd366cf7bb gsignal (/lib/x86_64-linux-gnu/libc.so.6+0x377bb)
#5 0x00007fcd366ba535 abort (/lib/x86_64-linux-gnu/libc.so.6+0x22535)
#6 0x00007fcd374f8e13 llvm::report_bad_alloc_error(char const*, bool) 
(/usr/lib/llvm-7/lib/libLLVM-7.so.1+0x968e13)
#7 0x00007fcd374f8e92 (/usr/lib/llvm-7/lib/libLLVM-7.so.1+0x968e92)
#8 0x00007fcd3a5bf748 _init 
(/usr/lib/x86_64-linux-gnu/libtcmalloc.so.4+0x17748)
#9 0x00007fcd3a5dfef5 tcmalloc::allocate_full_cpp_throw_oom(unsigned 
long) (/usr/lib/x86_64-linux-gnu/libtcmalloc.so.4+0x37ef5)
#10 0x00007fcd36b25eeb std::__cxx11::basic_string<char, 
std::char_traits<char>, std::allocator<char> >::_M_mutate(unsigned long, 
unsigned long, char const*, unsigned long) 
(/usr/lib/x86_64-linux-gnu/libstdc++.so.6+0x11deeb)
#11 0x00007fcd36b27483 std::__cxx11::basic_string<char, 
std::char_traits<char>, std::allocator<char> >::_M_append(char const*, 
unsigned long) (/usr/lib/x86_64-linux-gnu/libstdc++.so.6+0x11f483)
#12 0x00007fcd37542edf llvm::raw_ostream::write(char const*, unsigned 
long) (/usr/lib/llvm-7/lib/libLLVM-7.so.1+0x9b2edf)
#13 0x000055cef2d33460 (klee+0x14c460)
#14 0x000055cef2d334ca (klee+0x14c4ca)
#15 0x000055cef2d334ca (klee+0x14c4ca)
#16 0x000055cef2d334ca (klee+0x14c4ca)
#17 0x000055cef2d334ca (klee+0x14c4ca)
#18 0x000055cef2d334ca (klee+0x14c4ca)
#19 0x000055cef2d334ca (klee+0x14c4ca)
#20 0x000055cef2d334ca (klee+0x14c4ca)
#21 0x000055cef2d334ca (klee+0x14c4ca)
#22 0x000055cef2d334ca (klee+0x14c4ca)
#23 0x000055cef2d334ca (klee+0x14c4ca)
#24 0x000055cef2d334ca (klee+0x14c4ca)
#25 0x000055cef2d334ca (klee+0x14c4ca)
#26 0x000055cef2d334ca (klee+0x14c4ca)
#27 0x000055cef2d334ca (klee+0x14c4ca)
#28 0x000055cef2d334ca (klee+0x14c4ca)
#29 0x000055cef2d334ca (klee+0x14c4ca)
#30 0x000055cef2d334ca (klee+0x14c4ca)
#31 0x000055cef2d334ca (klee+0x14c4ca)
#32 0x000055cef2d334ca (klee+0x14c4ca)
#33 0x000055cef2d334ca (klee+0x14c4ca)
#34 0x000055cef2d334ca (klee+0x14c4ca)
#35 0x000055cef2d334ca (klee+0x14c4ca)
#36 0x000055cef2d334ca (klee+0x14c4ca)
#37 0x000055cef2d334ca (klee+0x14c4ca)
#38 0x000055cef2d334ca (klee+0x14c4ca)
#39 0x000055cef2d334ca (klee+0x14c4ca)
#40 0x000055cef2d334ca (klee+0x14c4ca)
#41 0x000055cef2d334ca (klee+0x14c4ca)
#42 0x000055cef2d334ca (klee+0x14c4ca)
#43 0x000055cef2d334ca (klee+0x14c4ca)
#44 0x000055cef2d334ca (klee+0x14c4ca)
#45 0x000055cef2d334ca (klee+0x14c4ca)
#46 0x000055cef2d334ca (klee+0x14c4ca)
#47 0x000055cef2d334ca (klee+0x14c4ca)
#48 0x000055cef2d334ca (klee+0x14c4ca)
#49 0x000055cef2d334ca (klee+0x14c4ca)
#50 0x000055cef2d334ca (klee+0x14c4ca)
#51 0x000055cef2d334ca (klee+0x14c4ca)
#52 0x000055cef2d334ca (klee+0x14c4ca)
#53 0x000055cef2d334ca (klee+0x14c4ca)
#54 0x000055cef2d334ca (klee+0x14c4ca)
#55 0x000055cef2d334ca (klee+0x14c4ca)
#56 0x000055cef2d334ca (klee+0x14c4ca)
#57 0x000055cef2d334ca (klee+0x14c4ca)
#58 0x000055cef2d334ca (klee+0x14c4ca)
#59 0x000055cef2d334ca (klee+0x14c4ca)
#60 0x000055cef2d334ca (klee+0x14c4ca)
#61 0x000055cef2d334ca (klee+0x14c4ca)
#62 0x000055cef2d334ca (klee+0x14c4ca)
#63 0x000055cef2d334ca (klee+0x14c4ca)
#64 0x000055cef2d334ca (klee+0x14c4ca)
#65 0x000055cef2d334ca (klee+0x14c4ca)
#66 0x000055cef2d334ca (klee+0x14c4ca)
#67 0x000055cef2d334ca (klee+0x14c4ca)
#68 0x000055cef2d334ca (klee+0x14c4ca)
#69 0x000055cef2d334ca (klee+0x14c4ca)
#70 0x000055cef2d334ca (klee+0x14c4ca)
#71 0x000055cef2d334ca (klee+0x14c4ca)
#72 0x000055cef2d334ca (klee+0x14c4ca)
#73 0x000055cef2d334ca (klee+0x14c4ca)
#74 0x000055cef2d334ca (klee+0x14c4ca)
#75 0x000055cef2d334ca (klee+0x14c4ca)
#76 0x000055cef2d334ca (klee+0x14c4ca)
#77 0x000055cef2d334ca (klee+0x14c4ca)
#78 0x000055cef2d334ca (klee+0x14c4ca)
#79 0x000055cef2d334ca (klee+0x14c4ca)
#80 0x000055cef2d334ca (klee+0x14c4ca)
#81 0x000055cef2d334ca (klee+0x14c4ca)
#82 0x000055cef2d334ca (klee+0x14c4ca)
#83 0x000055cef2d334ca (klee+0x14c4ca)
#84 0x000055cef2d334ca (klee+0x14c4ca)
#85 0x000055cef2d334ca (klee+0x14c4ca)
#86 0x000055cef2d334ca (klee+0x14c4ca)
#87 0x000055cef2d334ca (klee+0x14c4ca)
#88 0x000055cef2d334ca (klee+0x14c4ca)
#89 0x000055cef2d334ca (klee+0x14c4ca)
#90 0x000055cef2d334ca (klee+0x14c4ca)
#91 0x000055cef2d334ca (klee+0x14c4ca)
#92 0x000055cef2d334ca (klee+0x14c4ca)
#93 0x000055cef2d334ca (klee+0x14c4ca)
#94 0x000055cef2d334ca (klee+0x14c4ca)
#95 0x000055cef2d334ca (klee+0x14c4ca)
#96 0x000055cef2d334ca (klee+0x14c4ca)
#97 0x000055cef2d334ca (klee+0x14c4ca)
#98 0x000055cef2d334ca (klee+0x14c4ca)
#99 0x000055cef2d334ca (klee+0x14c4ca)
#100 0x000055cef2d334ca (klee+0x14c4ca)
#101 0x000055cef2d334ca (klee+0x14c4ca)
#102 0x000055cef2d334ca (klee+0x14c4ca)
#103 0x000055cef2d334ca (klee+0x14c4ca)
#104 0x000055cef2d334ca (klee+0x14c4ca)
#105 0x000055cef2d334ca (klee+0x14c4ca)
#106 0x000055cef2d334ca (klee+0x14c4ca)
#107 0x000055cef2d334ca (klee+0x14c4ca)
#108 0x000055cef2d334ca (klee+0x14c4ca)
#109 0x000055cef2d334ca (klee+0x14c4ca)
#110 0x000055cef2d334ca (klee+0x14c4ca)
#111 0x000055cef2d334ca (klee+0x14c4ca)
#112 0x000055cef2d334ca (klee+0x14c4ca)
#113 0x000055cef2d334ca (klee+0x14c4ca)
#114 0x000055cef2d334ca (klee+0x14c4ca)
#115 0x000055cef2d334ca (klee+0x14c4ca)
#116 0x000055cef2d334ca (klee+0x14c4ca)
#117 0x000055cef2d334ca (klee+0x14c4ca)
#118 0x000055cef2d334ca (klee+0x14c4ca)
#119 0x000055cef2d334ca (klee+0x14c4ca)
#120 0x000055cef2d334ca (klee+0x14c4ca)
#121 0x000055cef2d334ca (klee+0x14c4ca)
#122 0x000055cef2d334ca (klee+0x14c4ca)
#123 0x000055cef2d334ca (klee+0x14c4ca)
#124 0x000055cef2d334ca (klee+0x14c4ca)
#125 0x000055cef2d334ca (klee+0x14c4ca)
#126 0x000055cef2d334ca (klee+0x14c4ca)
#127 0x000055cef2d334ca (klee+0x14c4ca)
#128 0x000055cef2d334ca (klee+0x14c4ca)
#129 0x000055cef2d334ca (klee+0x14c4ca)
#130 0x000055cef2d334ca (klee+0x14c4ca)
#131 0x000055cef2d334ca (klee+0x14c4ca)
#132 0x000055cef2d334ca (klee+0x14c4ca)
#133 0x000055cef2d334ca (klee+0x14c4ca)
#134 0x000055cef2d334ca (klee+0x14c4ca)
#135 0x000055cef2d334ca (klee+0x14c4ca)
#136 0x000055cef2d334ca (klee+0x14c4ca)
#137 0x000055cef2d334ca (klee+0x14c4ca)
#138 0x000055cef2d334ca (klee+0x14c4ca)
#139 0x000055cef2d334ca (klee+0x14c4ca)
#140 0x000055cef2d334ca (klee+0x14c4ca)
#141 0x000055cef2d334ca (klee+0x14c4ca)
#142 0x000055cef2d334ca (klee+0x14c4ca)
#143 0x000055cef2d334ca (klee+0x14c4ca)
#144 0x000055cef2d334ca (klee+0x14c4ca)
#145 0x000055cef2d334ca (klee+0x14c4ca)
#146 0x000055cef2d334ca (klee+0x14c4ca)
#147 0x000055cef2d334ca (klee+0x14c4ca)
#148 0x000055cef2d334ca (klee+0x14c4ca)
#149 0x000055cef2d334ca (klee+0x14c4ca)
#150 0x000055cef2d334ca (klee+0x14c4ca)
#151 0x000055cef2d334ca (klee+0x14c4ca)
#152 0x000055cef2d334ca (klee+0x14c4ca)
#153 0x000055cef2d334ca (klee+0x14c4ca)
#154 0x000055cef2d334ca (klee+0x14c4ca)
#155 0x000055cef2d334ca (klee+0x14c4ca)
#156 0x000055cef2d334ca (klee+0x14c4ca)
#157 0x000055cef2d334ca (klee+0x14c4ca)
#158 0x000055cef2d334ca (klee+0x14c4ca)
#159 0x000055cef2d334ca (klee+0x14c4ca)
#160 0x000055cef2d334ca (klee+0x14c4ca)
#161 0x000055cef2d334ca (klee+0x14c4ca)
#162 0x000055cef2d334ca (klee+0x14c4ca)
#163 0x000055cef2d334ca (klee+0x14c4ca)
#164 0x000055cef2d334ca (klee+0x14c4ca)
#165 0x000055cef2d334ca (klee+0x14c4ca)
#166 0x000055cef2d334ca (klee+0x14c4ca)
#167 0x000055cef2d334ca (klee+0x14c4ca)
#168 0x000055cef2d334ca (klee+0x14c4ca)
#169 0x000055cef2d334ca (klee+0x14c4ca)
#170 0x000055cef2d334ca (klee+0x14c4ca)
#171 0x000055cef2d334ca (klee+0x14c4ca)
#172 0x000055cef2d334ca (klee+0x14c4ca)
#173 0x000055cef2d334ca (klee+0x14c4ca)
#174 0x000055cef2d334ca (klee+0x14c4ca)
#175 0x000055cef2d334ca (klee+0x14c4ca)
#176 0x000055cef2d334ca (klee+0x14c4ca)
#177 0x000055cef2d334ca (klee+0x14c4ca)
#178 0x000055cef2d334ca (klee+0x14c4ca)
#179 0x000055cef2d334ca (klee+0x14c4ca)
#180 0x000055cef2d334ca (klee+0x14c4ca)
#181 0x000055cef2d334ca (klee+0x14c4ca)
#182 0x000055cef2d334ca (klee+0x14c4ca)
#183 0x000055cef2d334ca (klee+0x14c4ca)
#184 0x000055cef2d334ca (klee+0x14c4ca)
#185 0x000055cef2d334ca (klee+0x14c4ca)
#186 0x000055cef2d334ca (klee+0x14c4ca)
#187 0x000055cef2d334ca (klee+0x14c4ca)
#188 0x000055cef2d334ca (klee+0x14c4ca)
#189 0x000055cef2d334ca (klee+0x14c4ca)
#190 0x000055cef2d334ca (klee+0x14c4ca)
#191 0x000055cef2d334ca (klee+0x14c4ca)
#192 0x000055cef2d334ca (klee+0x14c4ca)
#193 0x000055cef2d334ca (klee+0x14c4ca)
#194 0x000055cef2d334ca (klee+0x14c4ca)
#195 0x000055cef2d334ca (klee+0x14c4ca)
#196 0x000055cef2d334ca (klee+0x14c4ca)
#197 0x000055cef2d334ca (klee+0x14c4ca)
#198 0x000055cef2d334ca (klee+0x14c4ca)
#199 0x000055cef2d334ca (klee+0x14c4ca)
#200 0x000055cef2d334ca (klee+0x14c4ca)
#201 0x000055cef2d334ca (klee+0x14c4ca)
#202 0x000055cef2d334ca (klee+0x14c4ca)
#203 0x000055cef2d334ca (klee+0x14c4ca)
#204 0x000055cef2d334ca (klee+0x14c4ca)
#205 0x000055cef2d339f3 (klee+0x14c9f3)
#206 0x000055cef2d33ce3 (klee+0x14cce3)
#207 0x000055cef2d34038 (klee+0x14d038)
#208 0x000055cef2d345ad (klee+0x14d5ad)
#209 0x000055cef2d33e6d (klee+0x14ce6d)
#210 0x000055cef2d34038 (klee+0x14d038)
#211 0x000055cef2d345ad (klee+0x14d5ad)
#212 0x000055cef2d33e6d (klee+0x14ce6d)
#213 0x000055cef2d34038 (klee+0x14d038)
#214 0x000055cef2d345ad (klee+0x14d5ad)
#215 0x000055cef2d33e6d (klee+0x14ce6d)
#216 0x000055cef2d34038 (klee+0x14d038)
#217 0x000055cef2d345ad (klee+0x14d5ad)
#218 0x000055cef2d33e6d (klee+0x14ce6d)
#219 0x000055cef2d34038 (klee+0x14d038)
#220 0x000055cef2d345ad (klee+0x14d5ad)
#221 0x000055cef2d33e6d (klee+0x14ce6d)
#222 0x000055cef2d34038 (klee+0x14d038)
#223 0x000055cef2d345ad (klee+0x14d5ad)
#224 0x000055cef2d33e6d (klee+0x14ce6d)
#225 0x000055cef2d34038 (klee+0x14d038)
#226 0x000055cef2d3494d (klee+0x14d94d)
#227 0x000055cef2d33e05 (klee+0x14ce05)
#228 0x000055cef2d34038 (klee+0x14d038)
#229 0x000055cef2d3494d (klee+0x14d94d)
#230 0x000055cef2d33e05 (klee+0x14ce05)
#231 0x000055cef2d34038 (klee+0x14d038)
#232 0x000055cef2d3494d (klee+0x14d94d)
#233 0x000055cef2d33e05 (klee+0x14ce05)
#234 0x000055cef2d34038 (klee+0x14d038)
#235 0x000055cef2d345ad (klee+0x14d5ad)
#236 0x000055cef2d33e6d (klee+0x14ce6d)
#237 0x000055cef2d34038 (klee+0x14d038)
#238 0x000055cef2d345ad (klee+0x14d5ad)
#239 0x000055cef2d33e6d (klee+0x14ce6d)
#240 0x000055cef2d34038 (klee+0x14d038)
#241 0x000055cef2d345ad (klee+0x14d5ad)
#242 0x000055cef2d33e6d (klee+0x14ce6d)
#243 0x000055cef2d34038 (klee+0x14d038)
#244 0x000055cef2d345ad (klee+0x14d5ad)
#245 0x000055cef2d33e6d (klee+0x14ce6d)
#246 0x000055cef2d34038 (klee+0x14d038)
#247 0x000055cef2d345ad (klee+0x14d5ad)
#248 0x000055cef2d33e6d (klee+0x14ce6d)
#249 0x000055cef2d34038 (klee+0x14d038)
#250 0x000055cef2d3494d (klee+0x14d94d)
#251 0x000055cef2d33e05 (klee+0x14ce05)
#252 0x000055cef2d34038 (klee+0x14d038)
#253 0x000055cef2d3494d (klee+0x14d94d)
#254 0x000055cef2d33e05 (klee+0x14ce05)
#255 0x000055cef2d34038 (klee+0x14d038)
Aborted