Possible memory leak on migrate_type

[mikhailramalho]

I'm testing a program that Genarro sent me (it's more than 90KLOC) and ESBMC is using a massive amount of memory during symex.

While CBMC uses around 3GB, ESBMC uses 17GB+ memory. Compiling using the leak sanitizer, the GOTO model generation fails because the c2goto binary is leaking on migrate_type, here's one trace:

Direct leak of 16 byte(s) in 1 object(s) allocated from:
    #0 0x5131fb in operator new(unsigned long) /home/nikola/final/llvm.src/projects/compiler-rt/lib/asan/asan_new_delete.cc:78:35
    esbmc/esbmc#1 0x985b52 in get_type_from_pool(typet const&, std::map<typet, irep_container<type2t>, std::less<typet>, std::allocator<std::pair<typet const, irep_container<type2t> > > >&) /home/mramalho/esbmc/build/util/../../src/util/irep2.cpp:812:12
    esbmc/esbmc#2 0x985cf3 in type_poolt::get_signedbv(typet const&) /home/mramalho/esbmc/build/util/../../src/util/irep2.cpp:848:10
    esbmc/esbmc#3 0xb7b68e in migrate_type(typet const&, irep_container<type2t>&, namespacet const*, bool) /home/mramalho/esbmc/build/util/../../src/util/migrate.cpp:288:30
    esbmc/esbmc#4 0xb78958 in real_migrate_type(typet const&, irep_container<type2t>&, namespacet const*, bool) /home/mramalho/esbmc/build/util/../../src/util/migrate.cpp:106:5
    esbmc/esbmc#5 0xb7b5d1 in migrate_type(typet const&, irep_container<type2t>&, namespacet const*, bool) /home/mramalho/esbmc/build/util/../../src/util/migrate.cpp:283:12
    esbmc/esbmc#6 0x622393 in c_sizeof(typet const&, namespacet const&) /home/mramalho/esbmc/build/ansi-c/../../src/ansi-c/c_sizeof.cpp:25:3
    esbmc/esbmc#7 0x67b08e in clang_c_adjust::adjust_sizeof(exprt&) /home/mramalho/esbmc/build/clang-c-frontend/../../src/clang-c-frontend/clang_c_adjust_expr.cpp:472:18
    esbmc/esbmc#8 0x67732d in clang_c_adjust::adjust_expr(exprt&) /home/mramalho/esbmc/build/clang-c-frontend/../../src/clang-c-frontend/clang_c_adjust_expr.cpp:106:5
    esbmc/esbmc#9 0x67bdf8 in clang_c_adjust::adjust_operands(exprt&) /home/mramalho/esbmc/build/clang-c-frontend/../../src/clang-c-frontend/clang_c_adjust_expr.cpp:1238:5
    esbmc/esbmc#10 0x67b3d0 in clang_c_adjust::adjust_expr_binary_arithmetic(exprt&) /home/mramalho/esbmc/build/clang-c-frontend/../../src/clang-c-frontend/clang_c_adjust_expr.cpp:243:3
    esbmc/esbmc#11 0x6774e1 in clang_c_adjust::adjust_expr(exprt&) /home/mramalho/esbmc/build/clang-c-frontend/../../src/clang-c-frontend/clang_c_adjust_expr.cpp:119:5
    esbmc/esbmc#12 0x67bdf8 in clang_c_adjust::adjust_operands(exprt&) /home/mramalho/esbmc/build/clang-c-frontend/../../src/clang-c-frontend/clang_c_adjust_expr.cpp:1238:5
    esbmc/esbmc#13 0x677710 in clang_c_adjust::adjust_expr(exprt&) /home/mramalho/esbmc/build/clang-c-frontend/../../src/clang-c-frontend/clang_c_adjust_expr.cpp:147:5
    esbmc/esbmc#14 0x676e70 in clang_c_adjust::adjust_symbol(symbolt&) /home/mramalho/esbmc/build/clang-c-frontend/../../src/clang-c-frontend/clang_c_adjust_expr.cpp:55:5
    esbmc/esbmc#15 0x676b56 in clang_c_adjust::adjust() /home/mramalho/esbmc/build/clang-c-frontend/../../src/clang-c-frontend/clang_c_adjust_expr.cpp:46:5
    esbmc/esbmc#16 0x63265f in clang_c_languaget::typecheck(contextt&, std::__cxx11::basic_string<char, std::char_traits<char>, std::allocator<char> > const&, message_handlert&) /home/mramalho/esbmc/build/clang-c-frontend/../../src/clang-c-frontend/clang_c_language.cpp:161:15
    esbmc/esbmc#17 0x87a2ea in language_filest::typecheck(contextt&) /home/mramalho/esbmc/build/util/../../src/util/language_file.cpp:99:31
    esbmc/esbmc#18 0x84621c in language_uit::typecheck() /home/mramalho/esbmc/build/langapi/../../src/langapi/language_ui.cpp:182:21
    esbmc/esbmc#19 0x518c2d in c2goto_parseopt::doit() /home/mramalho/esbmc/build/c2goto/../../src/c2goto/c2goto.cpp:54:9
    esbmc/esbmc#20 0x8852d2 in parseoptions_baset::main() /home/mramalho/esbmc/build/util/../../src/util/parseoptions.cpp:50:10
    esbmc/esbmc#21 0x5155db in main /home/mramalho/esbmc/build/c2goto/../../src/c2goto/c2goto.cpp:74:19
    esbmc/esbmc#22 0x7fa8dcea957f in __libc_start_main (/lib64/libc.so.6+0x2057f)

All the leaks happen when calculating the sizeof operator. The full leak report: leak.txt

@jmorse, what do you think? is it false positive?

I tried to remove the new operator and return the object allocated by real_migrate_type but the leak continued. I can't find who's holding a reference for the type2tc object, that's keeping the shared_ptr alive.

[mikhailramalho]

Valgrind seems to agree that this new operator is never freed: output.

Enabling the type_pool map fixes the issue but I don't know the performance implication of the searches on the map.

[jmorse]

Hi,

On 17/01/17 14:03, Mikhail Ramalho wrote: Enabling the type_pool map fixes the issue but I don't know the performance implication of the searches on the map.

Opinion: probably less than malloc.

…

-- Thanks, Jeremy

[github-actions]

Stale issue message

[github-actions]

Stale issue message