Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Jump to bottom

heap-use-after-free at /src/ast/ast.h:502 #5942

Closed
merlinsun opened this issue Apr 3, 2022 · 0 comments
Closed

heap-use-after-free at /src/ast/ast.h:502 #5942

merlinsun opened this issue Apr 3, 2022 · 0 comments

Comments

@merlinsun
Copy link

Hi,
For this instance, z3 25feb0e debug build

$ cat delta.smt2
(declare-const x Int)
(declare-fun v () String)
(assert (= "0" (str.substr v 0 x)))
(check-sat)
$ z3debug delta.smt2
=================================================================
==7374==ERROR: AddressSanitizer: heap-use-after-free on address 0x607000044744 at pc 0x55e0b5f3b7f7 bp 0x7ffc2a5bb5d0 sp 0x7ffc2a5bb5c0
READ of size 4 at 0x607000044744 thread T0
    #0 0x55e0b5f3b7f6 in ast::hash() const ../src/ast/ast.h:502
    #1 0x55e0b6115a1d in obj_ptr_hash<expr>::operator()(expr*) const ../src/util/hash.h:168
    #2 0x55e0b6114d24 in core_hashtable<obj_hash_entry<expr>, obj_ptr_hash<expr>, ptr_eq<expr> >::get_hash(expr* const&) const ../src/util/hashtable.h:152
    #3 0x55e0b616a25e in core_hashtable<obj_hash_entry<expr>, obj_ptr_hash<expr>, ptr_eq<expr> >::remove(expr* const&) ../src/util/hashtable.h:558
    #4 0x55e0b706f6e8 in insert_obj_trail<expr>::undo() ../src/util/trail.h:368
    #5 0x55e0b6709991 in undo_trail_stack(ptr_vector<trail>&, unsigned int) ../src/util/trail.h:388
    #6 0x55e0b67099f0 in trail_stack::reset() ../src/util/trail.h:403
    #7 0x55e0b6fff47d in smt::theory_seq::~theory_seq() ../src/smt/theory_seq.cpp:292
    #8 0x55e0b6d111c5 in void deallocf<smt::theory>(char const*, int, smt::theory*) (/root/z3debug/build/z3+0x15021c5)
    #9 0x55e0b6d1c6c0 in delete_proc<smt::theory>::operator()(smt::theory*) ../src/util/util.h:163
    #10 0x55e0b6d19486 in delete_proc<smt::theory> std::for_each<smt::theory**, delete_proc<smt::theory> >(smt::theory**, smt::theory**, delete_proc<smt::theory>) (/root/z3debug/build/z3+0x150a486)
    #11 0x55e0b6d14272 in plugin_manager<smt::theory>::reset() ../src/util/plugin_manager.h:33
    #12 0x55e0b6d0ba55 in plugin_manager<smt::theory>::~plugin_manager() (/root/z3debug/build/z3+0x14fca55)
    #13 0x55e0b6cbacf3 in smt::context::~context() ../src/smt/smt_context.cpp:182
    #14 0x55e0b6ea152f in smt::kernel::imp::~imp() ../src/smt/smt_kernel.cpp:27
    #15 0x55e0b6ea155c in void deallocf<smt::kernel::imp>(char const*, int, smt::kernel::imp*) ../src/util/memory_manager.h:85
    #16 0x55e0b6e9e6c1 in smt::kernel::~kernel() ../src/smt/smt_kernel.cpp:59
    #17 0x55e0b693ee3c in void deallocf<smt::kernel>(char const*, int, smt::kernel*) (/root/z3debug/build/z3+0x112fe3c)
    #18 0x55e0b693a468 in smt_tactic::scoped_init_ctx::~scoped_init_ctx() (/root/z3debug/build/z3+0x112b468)
    #19 0x55e0b693dba8 in smt_tactic::operator()(ref<goal> const&, sref_buffer<goal, 16u>&) ../src/smt/tactic/smt_tactic_core.cpp:308
    #20 0x55e0b80673e1 in and_then_tactical::operator()(ref<goal> const&, sref_buffer<goal, 16u>&) ../src/tactic/tactical.cpp:121
    #21 0x55e0b80729ae in cond_tactical::operator()(ref<goal> const&, sref_buffer<goal, 16u>&) ../src/tactic/tactical.cpp:1123
    #22 0x55e0b80729ae in cond_tactical::operator()(ref<goal> const&, sref_buffer<goal, 16u>&) ../src/tactic/tactical.cpp:1123
    #23 0x55e0b80729ae in cond_tactical::operator()(ref<goal> const&, sref_buffer<goal, 16u>&) ../src/tactic/tactical.cpp:1123
    #24 0x55e0b80729ae in cond_tactical::operator()(ref<goal> const&, sref_buffer<goal, 16u>&) ../src/tactic/tactical.cpp:1123
    #25 0x55e0b80729ae in cond_tactical::operator()(ref<goal> const&, sref_buffer<goal, 16u>&) ../src/tactic/tactical.cpp:1123
    #26 0x55e0b80729ae in cond_tactical::operator()(ref<goal> const&, sref_buffer<goal, 16u>&) ../src/tactic/tactical.cpp:1123
    #27 0x55e0b80729ae in cond_tactical::operator()(ref<goal> const&, sref_buffer<goal, 16u>&) ../src/tactic/tactical.cpp:1123
    #28 0x55e0b80729ae in cond_tactical::operator()(ref<goal> const&, sref_buffer<goal, 16u>&) ../src/tactic/tactical.cpp:1123
    #29 0x55e0b80729ae in cond_tactical::operator()(ref<goal> const&, sref_buffer<goal, 16u>&) ../src/tactic/tactical.cpp:1123
    #30 0x55e0b80729ae in cond_tactical::operator()(ref<goal> const&, sref_buffer<goal, 16u>&) ../src/tactic/tactical.cpp:1123
    #31 0x55e0b80729ae in cond_tactical::operator()(ref<goal> const&, sref_buffer<goal, 16u>&) ../src/tactic/tactical.cpp:1123
    #32 0x55e0b80729ae in cond_tactical::operator()(ref<goal> const&, sref_buffer<goal, 16u>&) ../src/tactic/tactical.cpp:1123
    #33 0x55e0b80673e1 in and_then_tactical::operator()(ref<goal> const&, sref_buffer<goal, 16u>&) ../src/tactic/tactical.cpp:121
    #34 0x55e0b806f4c4 in unary_tactical::operator()(ref<goal> const&, sref_buffer<goal, 16u>&) ../src/tactic/tactical.cpp:843
    #35 0x55e0b80a35a5 in exec(tactic&, ref<goal> const&, sref_buffer<goal, 16u>&) ../src/tactic/tactic.cpp:153
    #36 0x55e0b80a3b5e 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> >&) ../src/tactic/tactic.cpp:173
    #37 0x55e0b7fcf621 in check_sat_core2 ../src/solver/tactic2solver.cpp:225
    #38 0x55e0b7fcc574 in solver_na2as::check_sat_core(unsigned int, expr* const*) ../src/solver/solver_na2as.cpp:67
    #39 0x55e0b7ff425f in combined_solver::check_sat_core(unsigned int, expr* const*) ../src/solver/combined_solver.cpp:252
    #40 0x55e0b7fe8344 in solver::check_sat(unsigned int, expr* const*) ../src/solver/solver.cpp:318
    #41 0x55e0b7f5ef4f in cmd_context::check_sat(unsigned int, expr* const*) ../src/cmd_context/cmd_context.cpp:1702
    #42 0x55e0b7f15ba0 in smt2::parser::parse_check_sat() ../src/parsers/smt2/smt2parser.cpp:2611
    #43 0x55e0b7f1a034 in smt2::parser::parse_cmd() ../src/parsers/smt2/smt2parser.cpp:2953
    #44 0x55e0b7f1be87 in smt2::parser::operator()() ../src/parsers/smt2/smt2parser.cpp:3162
    #45 0x55e0b7ef15e1 in parse_smt2_commands(cmd_context&, std::istream&, bool, params_ref const&, char const*) ../src/parsers/smt2/smt2parser.cpp:3211
    #46 0x55e0b5ed90dc in read_smtlib2_commands(char const*) ../src/shell/smtlib_frontend.cpp:142
    #47 0x55e0b5eeeb70 in main ../src/shell/main.cpp:371
    #48 0x7f01781320b2 in __libc_start_main (/lib/x86_64-linux-gnu/libc.so.6+0x240b2)
    #49 0x55e0b5ec82cd in _start (/root/z3debug/build/z3+0x6b92cd)

0x607000044744 is located 20 bytes inside of 76-byte region [0x607000044730,0x60700004477c)
freed by thread T0 here:
    #0 0x7f017877c40f in __interceptor_free ../../../../src/libsanitizer/asan/asan_malloc_linux.cc:122
    #1 0x55e0b912c18d in memory::deallocate(void*) ../src/util/memory_manager.cpp:265
    #2 0x55e0b913e0a2 in small_object_allocator::deallocate(unsigned long, void*) ../src/util/small_object_allocator.cpp:77
    #3 0x55e0b8bf1ede in ast_manager::deallocate_node(ast*, unsigned int) ../src/ast/ast.h:1676
    #4 0x55e0b8bd8953 in ast_manager::delete_node(ast*) ../src/ast/ast.cpp:1911
    #5 0x55e0b5ed55b2 in ast_manager::dec_ref(ast*) ../src/ast/ast.h:1635
    #6 0x55e0b5ed73c4 in ref_manager_wrapper<expr, ast_manager>::dec_ref(expr*) ../src/util/ref_vector.h:227
    #7 0x55e0b5ed72e6 in ref_vector_core<expr, ref_manager_wrapper<expr, ast_manager> >::dec_ref(expr*) ../src/util/ref_vector.h:37
    #8 0x55e0b60ac1a5 in ref_vector_core<expr, ref_manager_wrapper<expr, ast_manager> >::pop_back() ../src/util/ref_vector.h:126
    #9 0x55e0b61bd168 in push_back_vector<ref_vector<expr, ast_manager> >::undo() ../src/util/trail.h:217
    #10 0x55e0b6709991 in undo_trail_stack(ptr_vector<trail>&, unsigned int) ../src/util/trail.h:388
    #11 0x55e0b67099f0 in trail_stack::reset() ../src/util/trail.h:403
    #12 0x55e0b6fff47d in smt::theory_seq::~theory_seq() ../src/smt/theory_seq.cpp:292
    #13 0x55e0b6d111c5 in void deallocf<smt::theory>(char const*, int, smt::theory*) (/root/z3debug/build/z3+0x15021c5)
    #14 0x55e0b6d1c6c0 in delete_proc<smt::theory>::operator()(smt::theory*) ../src/util/util.h:163
    #15 0x55e0b6d19486 in delete_proc<smt::theory> std::for_each<smt::theory**, delete_proc<smt::theory> >(smt::theory**, smt::theory**, delete_proc<smt::theory>) (/root/z3debug/build/z3+0x150a486)
    #16 0x55e0b6d14272 in plugin_manager<smt::theory>::reset() ../src/util/plugin_manager.h:33
    #17 0x55e0b6d0ba55 in plugin_manager<smt::theory>::~plugin_manager() (/root/z3debug/build/z3+0x14fca55)
    #18 0x55e0b6cbacf3 in smt::context::~context() ../src/smt/smt_context.cpp:182
    #19 0x55e0b6ea152f in smt::kernel::imp::~imp() ../src/smt/smt_kernel.cpp:27
    #20 0x55e0b6ea155c in void deallocf<smt::kernel::imp>(char const*, int, smt::kernel::imp*) ../src/util/memory_manager.h:85
    #21 0x55e0b6e9e6c1 in smt::kernel::~kernel() ../src/smt/smt_kernel.cpp:59
    #22 0x55e0b693ee3c in void deallocf<smt::kernel>(char const*, int, smt::kernel*) (/root/z3debug/build/z3+0x112fe3c)
    #23 0x55e0b693a468 in smt_tactic::scoped_init_ctx::~scoped_init_ctx() (/root/z3debug/build/z3+0x112b468)
    #24 0x55e0b693dba8 in smt_tactic::operator()(ref<goal> const&, sref_buffer<goal, 16u>&) ../src/smt/tactic/smt_tactic_core.cpp:308
    #25 0x55e0b80673e1 in and_then_tactical::operator()(ref<goal> const&, sref_buffer<goal, 16u>&) ../src/tactic/tactical.cpp:121
    #26 0x55e0b80729ae in cond_tactical::operator()(ref<goal> const&, sref_buffer<goal, 16u>&) ../src/tactic/tactical.cpp:1123
    #27 0x55e0b80729ae in cond_tactical::operator()(ref<goal> const&, sref_buffer<goal, 16u>&) ../src/tactic/tactical.cpp:1123
    #28 0x55e0b80729ae in cond_tactical::operator()(ref<goal> const&, sref_buffer<goal, 16u>&) ../src/tactic/tactical.cpp:1123
    #29 0x55e0b80729ae in cond_tactical::operator()(ref<goal> const&, sref_buffer<goal, 16u>&) ../src/tactic/tactical.cpp:1123

previously allocated by thread T0 here:
    #0 0x7f017877c808 in __interceptor_malloc ../../../../src/libsanitizer/asan/asan_malloc_linux.cc:144
    #1 0x55e0b912c1dd in memory::allocate(unsigned long) ../src/util/memory_manager.cpp:273
    #2 0x55e0b913e0d5 in small_object_allocator::allocate(unsigned long) ../src/util/small_object_allocator.cpp:103
    #3 0x55e0b8bf1eaa in ast_manager::allocate_node(unsigned int) ../src/ast/ast.h:1672
    #4 0x55e0b8bdb4a3 in ast_manager::mk_app_core(func_decl*, unsigned int, expr* const*) ../src/ast/ast.cpp:2155
    #5 0x55e0b8bdcde1 in ast_manager::mk_app(func_decl*, unsigned int, expr* const*) ../src/ast/ast.cpp:2271
    #6 0x55e0b8bd8cdb in ast_manager::mk_app(int, int, unsigned int, parameter const*, unsigned int, expr* const*, sort*) ../src/ast/ast.cpp:1943
    #7 0x55e0b8bd8d2a in ast_manager::mk_app(int, int, unsigned int, expr* const*) ../src/ast/ast.cpp:1948
    #8 0x55e0b704584b in seq_util::str::mk_concat(expr*, expr*) const ../src/ast/seq_decl_plugin.h:286
    #9 0x55e0b83eb9b7 in seq::axioms::mk_concat(expr*, expr*) ../src/ast/rewriter/seq_axioms.h:45
    #10 0x55e0b83cf12e in seq::axioms::extract_prefix_axiom(expr*, expr*, expr*) ../src/ast/rewriter/seq_axioms.cpp:339
    #11 0x55e0b83c9972 in seq::axioms::extract_axiom(expr*) ../src/ast/rewriter/seq_axioms.cpp:213
    #12 0x55e0b704c317 in smt::seq_axioms::add_extract_axiom(expr*) (/root/z3debug/build/z3+0x183d317)
    #13 0x55e0b7031dc1 in smt::theory_seq::deque_axiom(expr*) ../src/smt/theory_seq.cpp:2653
    #14 0x55e0b7030b19 in smt::theory_seq::propagate() ../src/smt/theory_seq.cpp:2603
    #15 0x55e0b6cd2b15 in smt::context::propagate_theories() ../src/smt/smt_context.cpp:1629
    #16 0x55e0b6cd3d20 in smt::context::propagate() ../src/smt/smt_context.cpp:1717
    #17 0x55e0b6ceb8cd in smt::context::init_assumptions(ref_vector<expr, ast_manager> const&) ../src/smt/smt_context.cpp:3299
    #18 0x55e0b6cf021c in smt::context::check(unsigned int, expr* const*, bool) ../src/smt/smt_context.cpp:3591
    #19 0x55e0b6cef417 in smt::context::setup_and_check(bool) ../src/smt/smt_context.cpp:3529
    #20 0x55e0b6e9eebe in smt::kernel::setup_and_check() ../src/smt/smt_kernel.cpp:124
    #21 0x55e0b693bf49 in smt_tactic::operator()(ref<goal> const&, sref_buffer<goal, 16u>&) ../src/smt/tactic/smt_tactic_core.cpp:207
    #22 0x55e0b80673e1 in and_then_tactical::operator()(ref<goal> const&, sref_buffer<goal, 16u>&) ../src/tactic/tactical.cpp:121
    #23 0x55e0b80729ae in cond_tactical::operator()(ref<goal> const&, sref_buffer<goal, 16u>&) ../src/tactic/tactical.cpp:1123
    #24 0x55e0b80729ae in cond_tactical::operator()(ref<goal> const&, sref_buffer<goal, 16u>&) ../src/tactic/tactical.cpp:1123
    #25 0x55e0b80729ae in cond_tactical::operator()(ref<goal> const&, sref_buffer<goal, 16u>&) ../src/tactic/tactical.cpp:1123
    #26 0x55e0b80729ae in cond_tactical::operator()(ref<goal> const&, sref_buffer<goal, 16u>&) ../src/tactic/tactical.cpp:1123
    #27 0x55e0b80729ae in cond_tactical::operator()(ref<goal> const&, sref_buffer<goal, 16u>&) ../src/tactic/tactical.cpp:1123
    #28 0x55e0b80729ae in cond_tactical::operator()(ref<goal> const&, sref_buffer<goal, 16u>&) ../src/tactic/tactical.cpp:1123
    #29 0x55e0b80729ae in cond_tactical::operator()(ref<goal> const&, sref_buffer<goal, 16u>&) ../src/tactic/tactical.cpp:1123

SUMMARY: AddressSanitizer: heap-use-after-free ../src/ast/ast.h:502 in ast::hash() const
==7374==ABORTING
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Assignees
No one assigned
Labels
None yet
Projects
None yet
Milestone
No milestone
Development

No branches or pull requests
1 participant
@merlinsun