[ASan] OpenMP leaks - Githubissues

When running the following Z3 regression tests with ASan

regressions/smt2/strategy-par-or-3.smt2
regressions/smt2/strategy-par-or-1.smt2
regressions/smt2/strategy-par-or-2.smt2

leaks are reported. To be clear I don't think there's anything we can do about this because we're seeing internal implementation details of the OpenMP library that Clang uses so

The leak is real inside Clang's OpenMP library and cannot be fixed by us

This is a false positive due to ASan's LeakSanitizer component not knowing how Clang's OpenMP library is implemented.

I could be wrong of course. I'm not really familiar with OpenMP.

For now I will suppress these in CI. When we have time we should try to reproduce this with the latest Clang release and if it persists we should report this to the ASan developers.

=================================================================
==1838==ERROR: LeakSanitizer: detected memory leaks

Direct leak of 416 byte(s) in 1 object(s) allocated from:
    #0 0x5500a8 in __interceptor_malloc (/home/user/z3_build/z3+0x5500a8)
    #1 0x7ffff6e6f03c  (/usr/lib/x86_64-linux-gnu/libomp.so.5+0x1803c)
    #2 0x7ffff6e6f13a in ___kmp_allocate (/usr/lib/x86_64-linux-gnu/libomp.so.5+0x1813a)
    #3 0x7ffff6eaa2b4  (/usr/lib/x86_64-linux-gnu/libomp.so.5+0x532b4)
    #4 0x7ffff6eaa5c1  (/usr/lib/x86_64-linux-gnu/libomp.so.5+0x535c1)
    #5 0x7ffff6ec5d91  (/usr/lib/x86_64-linux-gnu/libomp.so.5+0x6ed91)
    #6 0x7ffff6e973e6  (/usr/lib/x86_64-linux-gnu/libomp.so.5+0x403e6)
    #7 0x7ffff6e90567 in __kmp_fork_call (/usr/lib/x86_64-linux-gnu/libomp.so.5+0x39567)
    #8 0x7ffff6e84f4e in __kmpc_fork_call (/usr/lib/x86_64-linux-gnu/libomp.so.5+0x2df4e)
    #9 0x137a7a5 in par_tactical::operator()(ref<goal> const&, sref_buffer<goal, 16u>&, ref<model_converter>&, ref<proof_converter>&, obj_ref<dependency_manager<ast_manager::expr_dependency_config>::dependency, ast_manager>&) /home/user/z3_src/src/tactic/tactical.cpp:509:17
    #10 0x1384d3b in unary_tactical::operator()(ref<goal> const&, sref_buffer<goal, 16u>&, ref<model_converter>&, ref<proof_converter>&, obj_ref<dependency_manager<ast_manager::expr_dependency_config>::dependency, ast_manager>&) /home/user/z3_src/src/tactic/tactical.cpp:907:14
    #11 0x138a704 in exec(tactic&, ref<goal> const&, sref_buffer<goal, 16u>&, ref<model_converter>&, ref<proof_converter>&, obj_ref<dependency_manager<ast_manager::expr_dependency_config>::dependency, ast_manager>&) /home/user/z3_src/src/tactic/tactic.cpp:167:9
    #12 0x138ad51 in check_sat(tactic&, ref<goal>&, ref<model>&, labels_vec&, obj_ref<app, ast_manager>&, obj_ref<dependency_manager<ast_manager::expr_dependency_config>::dependency, ast_manager>&, std::__cxx11::basic_string<char, std::char_traits<char>, std::allocator<char> >&) /home/user/z3_src/src/tactic/tactic.cpp:190:9
    #13 0x19056a9 in check_sat_using_tactict_cmd::execute(cmd_context&) /home/user/z3_src/src/cmd_context/tactic_cmds.cpp:229:25
    #14 0x1929b8a in smt2::parser::parse_ext_cmd(int, int) /home/user/z3_src/src/parsers/smt2/smt2parser.cpp:2815:33
    #15 0x19220a5 in smt2::parser::parse_cmd() /home/user/z3_src/src/parsers/smt2/smt2parser.cpp:2913:13
    #16 0x191dc1f in smt2::parser::operator()() /home/user/z3_src/src/parsers/smt2/smt2parser.cpp:3021:29
    #17 0x191cc8f in parse_smt2_commands(cmd_context&, std::istream&, bool, params_ref const&, char const*) /home/user/z3_src/src/parsers/smt2/smt2parser.cpp:3070:12
    #18 0x32d8d55 in read_smtlib2_commands(char const*) /home/user/z3_src/src/shell/smtlib_frontend.cpp:129:18
    #19 0x32d2513 in main /home/user/z3_src/src/shell/main.cpp:358:28
    #20 0x7ffff689782f in __libc_start_main (/lib/x86_64-linux-gnu/libc.so.6+0x2082f)

Direct leak of 112 byte(s) in 1 object(s) allocated from:
    #0 0x5500a8 in __interceptor_malloc (/home/user/z3_build/z3+0x5500a8)
    #1 0x7ffff6e6f03c  (/usr/lib/x86_64-linux-gnu/libomp.so.5+0x1803c)
    #2 0x7ffff6e6f13a in ___kmp_allocate (/usr/lib/x86_64-linux-gnu/libomp.so.5+0x1813a)
    #3 0x7ffff6e8f454 in __kmp_fork_call (/usr/lib/x86_64-linux-gnu/libomp.so.5+0x38454)
    #4 0x7ffff6e84f4e in __kmpc_fork_call (/usr/lib/x86_64-linux-gnu/libomp.so.5+0x2df4e)
    #5 0x137a7a5 in par_tactical::operator()(ref<goal> const&, sref_buffer<goal, 16u>&, ref<model_converter>&, ref<proof_converter>&, obj_ref<dependency_manager<ast_manager::expr_dependency_config>::dependency, ast_manager>&) /home/user/z3_src/src/tactic/tactical.cpp:509:17
    #6 0x1384d3b in unary_tactical::operator()(ref<goal> const&, sref_buffer<goal, 16u>&, ref<model_converter>&, ref<proof_converter>&, obj_ref<dependency_manager<ast_manager::expr_dependency_config>::dependency, ast_manager>&) /home/user/z3_src/src/tactic/tactical.cpp:907:14
    #7 0x138a704 in exec(tactic&, ref<goal> const&, sref_buffer<goal, 16u>&, ref<model_converter>&, ref<proof_converter>&, obj_ref<dependency_manager<ast_manager::expr_dependency_config>::dependency, ast_manager>&) /home/user/z3_src/src/tactic/tactic.cpp:167:9
    #8 0x138ad51 in check_sat(tactic&, ref<goal>&, ref<model>&, labels_vec&, obj_ref<app, ast_manager>&, obj_ref<dependency_manager<ast_manager::expr_dependency_config>::dependency, ast_manager>&, std::__cxx11::basic_string<char, std::char_traits<char>, std::allocator<char> >&) /home/user/z3_src/src/tactic/tactic.cpp:190:9
    #9 0x19056a9 in check_sat_using_tactict_cmd::execute(cmd_context&) /home/user/z3_src/src/cmd_context/tactic_cmds.cpp:229:25
    #10 0x1929b8a in smt2::parser::parse_ext_cmd(int, int) /home/user/z3_src/src/parsers/smt2/smt2parser.cpp:2815:33
    #11 0x19220a5 in smt2::parser::parse_cmd() /home/user/z3_src/src/parsers/smt2/smt2parser.cpp:2913:13
    #12 0x191dc1f in smt2::parser::operator()() /home/user/z3_src/src/parsers/smt2/smt2parser.cpp:3021:29
    #13 0x191cc8f in parse_smt2_commands(cmd_context&, std::istream&, bool, params_ref const&, char const*) /home/user/z3_src/src/parsers/smt2/smt2parser.cpp:3070:12
    #14 0x32d8d55 in read_smtlib2_commands(char const*) /home/user/z3_src/src/shell/smtlib_frontend.cpp:129:18
    #15 0x32d2513 in main /home/user/z3_src/src/shell/main.cpp:358:28
    #16 0x7ffff689782f in __libc_start_main (/lib/x86_64-linux-gnu/libc.so.6+0x2082f)

SUMMARY: AddressSanitizer: 528 byte(s) leaked in 2 allocation(s).

Z3Prover / z3

[ASan] OpenMP leaks #1308