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

AddressSanitizer: heap-use-after-free at src/util/obj_hashtable.h:35 #6513

Closed
zhendongsu opened this issue Dec 30, 2022 · 0 comments
Closed

AddressSanitizer: heap-use-after-free at src/util/obj_hashtable.h:35 #6513

zhendongsu opened this issue Dec 30, 2022 · 0 comments

Comments

@zhendongsu
Copy link 

[520] % z3san small.smt2
=================================================================
==2913==ERROR: AddressSanitizer: heap-use-after-free on address 0x6120000c3f4c at pc 0x556a1973569e bp 0x7ffe6f9a9680 sp 0x7ffe6f9a9670
READ of size 4 at 0x6120000c3f4c thread T0
    #0 0x556a1973569d in obj_hash_entry<expr>::get_hash() const ../src/util/obj_hashtable.h:35
    #1 0x556a1973569d in core_hashtable<obj_hash_entry<expr>, obj_ptr_hash<expr>, ptr_eq<expr> >::find_core(expr* const&) const ../src/util/hashtable.h:516
    #2 0x556a1973569d in core_hashtable<obj_hash_entry<expr>, obj_ptr_hash<expr>, ptr_eq<expr> >::contains(expr* const&) const ../src/util/hashtable.h:531
    #3 0x556a1973569d in expr_sparse_mark::is_marked(expr*) const ../src/ast/ast.h:2467
    #4 0x556a1973569d in euf::arith_extract_eq::solve_mul(expr*, expr*, expr*, dependency_manager<ast_manager::expr_dependency_config>::dependency*, vector<euf::dependent_eq, true, unsigned int>&) ../src/ast/simplifiers/extract_eqs.cpp:201
    #5 0x556a1973569d in euf::arith_extract_eq::solve_eq(expr*, expr*, expr*, dependency_manager<ast_manager::expr_dependency_config>::dependency*, vector<euf::dependent_eq, true, unsigned int>&) ../src/ast/simplifiers/extract_eqs.cpp:239
    #6 0x556a19735d9d in euf::arith_extract_eq::get_eqs(dependent_expr const&, vector<euf::dependent_eq, true, unsigned int>&) ../src/ast/simplifiers/extract_eqs.cpp:252
    #7 0x556a196b2521 in euf::solve_eqs::get_eqs(vector<euf::dependent_eq, true, unsigned int>&) ../src/ast/simplifiers/solve_eqs.cpp:56
    #8 0x556a196c97bd in euf::solve_eqs::reduce() ../src/ast/simplifiers/solve_eqs.cpp:236
    #9 0x556a165c2a80 in dependent_expr_state_tactic::operator()(ref<goal> const&, sref_buffer<goal, 16u>&) ../src/tactic/dependent_expr_state_tactic.h:112
    #10 0x556a19678a91 in and_then_tactical::operator()(ref<goal> const&, sref_buffer<goal, 16u>&) ../src/tactic/tactical.cpp:113
    #11 0x556a196798ba in and_then_tactical::operator()(ref<goal> const&, sref_buffer<goal, 16u>&) ../src/tactic/tactical.cpp:122
    #12 0x556a196798ba in and_then_tactical::operator()(ref<goal> const&, sref_buffer<goal, 16u>&) ../src/tactic/tactical.cpp:122
    #13 0x556a196798ba in and_then_tactical::operator()(ref<goal> const&, sref_buffer<goal, 16u>&) ../src/tactic/tactical.cpp:122
    #14 0x556a1966d3f7 in try_for_tactical::operator()(ref<goal> const&, sref_buffer<goal, 16u>&) ../src/tactic/tactical.cpp:1057
    #15 0x556a19673827 in or_else_tactical::operator()(ref<goal> const&, sref_buffer<goal, 16u>&) ../src/tactic/tactical.cpp:342
    #16 0x556a196798ba in and_then_tactical::operator()(ref<goal> const&, sref_buffer<goal, 16u>&) ../src/tactic/tactical.cpp:122
    #17 0x556a196798ba in and_then_tactical::operator()(ref<goal> const&, sref_buffer<goal, 16u>&) ../src/tactic/tactical.cpp:122
    #18 0x556a1966da41 in cond_tactical::operator()(ref<goal> const&, sref_buffer<goal, 16u>&) ../src/tactic/tactical.cpp:1153
    #19 0x556a1966da41 in cond_tactical::operator()(ref<goal> const&, sref_buffer<goal, 16u>&) ../src/tactic/tactical.cpp:1153
    #20 0x556a1966da41 in cond_tactical::operator()(ref<goal> const&, sref_buffer<goal, 16u>&) ../src/tactic/tactical.cpp:1153
    #21 0x556a1966da41 in cond_tactical::operator()(ref<goal> const&, sref_buffer<goal, 16u>&) ../src/tactic/tactical.cpp:1153
    #22 0x556a1966da41 in cond_tactical::operator()(ref<goal> const&, sref_buffer<goal, 16u>&) ../src/tactic/tactical.cpp:1153
    #23 0x556a1966da41 in cond_tactical::operator()(ref<goal> const&, sref_buffer<goal, 16u>&) ../src/tactic/tactical.cpp:1153
    #24 0x556a1966da41 in cond_tactical::operator()(ref<goal> const&, sref_buffer<goal, 16u>&) ../src/tactic/tactical.cpp:1153
    #25 0x556a196798ba in and_then_tactical::operator()(ref<goal> const&, sref_buffer<goal, 16u>&) ../src/tactic/tactical.cpp:122
    #26 0x556a19640cc4 in exec(tactic&, ref<goal> const&, sref_buffer<goal, 16u>&) ../src/tactic/tactic.cpp:165
    #27 0x556a196426e4 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:185
    #28 0x556a1959dea8 in check_sat_core2 ../src/solver/tactic2solver.cpp:233
    #29 0x556a195c275f in solver_na2as::check_sat_core(unsigned int, expr* const*) ../src/solver/solver_na2as.cpp:67
    #30 0x556a195dc5b4 in combined_solver::check_sat_core(unsigned int, expr* const*) ../src/solver/combined_solver.cpp:253
    #31 0x556a195af1e6 in solver::check_sat(unsigned int, expr* const*) ../src/solver/solver.cpp:318
    #32 0x556a19526ac5 in cmd_context::check_sat(unsigned int, expr* const*) ../src/cmd_context/cmd_context.cpp:1700
    #33 0x556a1947eef3 in smt2::parser::parse_check_sat() ../src/parsers/smt2/smt2parser.cpp:2611
    #34 0x556a1947eef3 in smt2::parser::parse_cmd() ../src/parsers/smt2/smt2parser.cpp:2953
    #35 0x556a1947eef3 in smt2::parser::operator()() ../src/parsers/smt2/smt2parser.cpp:3166
    #36 0x556a19434055 in parse_smt2_commands(cmd_context&, std::istream&, bool, params_ref const&, char const*) ../src/parsers/smt2/smt2parser.cpp:3217
    #37 0x556a1656b651 in read_smtlib2_commands(char const*) ../src/shell/smtlib_frontend.cpp:147
    #38 0x556a1653f241 in main ../src/shell/main.cpp:382
    #39 0x7fe5445bfc86 in __libc_start_main (/lib/x86_64-linux-gnu/libc.so.6+0x21c86)
    #40 0x556a1654c2f9 in _start (/local/suz-local/software/z3san/build-12272022201939-7cc58c9/z3+0x20b2f9)

0x6120000c3f4c is located 12 bytes inside of 260-byte region [0x6120000c3f40,0x6120000c4044)
freed by thread T0 here:
    #0 0x7fe5455cb7a8 in __interceptor_free (/usr/lib/x86_64-linux-gnu/libasan.so.4+0xde7a8)
    #1 0x556a1b3ba854 in memory::deallocate(void*) ../src/util/memory_manager.cpp:286
    #2 0x556a1adead03 in ast_manager::deallocate_node(ast*, unsigned int) ../src/ast/ast.h:1691
    #3 0x556a1adead03 in ast_manager::delete_node(ast*) ../src/ast/ast.cpp:1918
    #4 0x556a196c959b in ast_manager::dec_ref(ast*) ../src/ast/ast.h:1650
    #5 0x556a196c959b in dependent_expr::~dependent_expr() ../src/ast/simplifiers/dependent_expr.h:88
    #6 0x556a196c959b in void std::_Destroy<dependent_expr>(dependent_expr*) /usr/include/c++/7/bits/stl_construct.h:98
    #7 0x556a196c959b in dependent_expr* std::_Destroy_n_aux<false>::__destroy_n<dependent_expr*, unsigned int>(dependent_expr*, unsigned int) /usr/include/c++/7/bits/stl_construct.h:148
    #8 0x556a196c959b in dependent_expr* std::_Destroy_n<dependent_expr*, unsigned int>(dependent_expr*, unsigned int) /usr/include/c++/7/bits/stl_construct.h:182
    #9 0x556a196c959b in dependent_expr* std::destroy_n<dependent_expr*, unsigned int>(dependent_expr*, unsigned int) /usr/include/c++/7/bits/stl_construct.h:228
    #10 0x556a196c959b in vector<dependent_expr, true, unsigned int>::destroy_elements() ../src/util/vector.h:169
    #11 0x556a196c959b in vector<dependent_expr, true, unsigned int>::reset() ../src/util/vector.h:388
    #12 0x556a196c959b in euf::solve_eqs::reduce() ../src/ast/simplifiers/solve_eqs.cpp:233
    #13 0x556a165c2a80 in dependent_expr_state_tactic::operator()(ref<goal> const&, sref_buffer<goal, 16u>&) ../src/tactic/dependent_expr_state_tactic.h:112
    #14 0x556a19678a91 in and_then_tactical::operator()(ref<goal> const&, sref_buffer<goal, 16u>&) ../src/tactic/tactical.cpp:113
    #15 0x556a196798ba in and_then_tactical::operator()(ref<goal> const&, sref_buffer<goal, 16u>&) ../src/tactic/tactical.cpp:122
    #16 0x556a196798ba in and_then_tactical::operator()(ref<goal> const&, sref_buffer<goal, 16u>&) ../src/tactic/tactical.cpp:122
    #17 0x556a196798ba in and_then_tactical::operator()(ref<goal> const&, sref_buffer<goal, 16u>&) ../src/tactic/tactical.cpp:122
    #18 0x556a1966d3f7 in try_for_tactical::operator()(ref<goal> const&, sref_buffer<goal, 16u>&) ../src/tactic/tactical.cpp:1057
    #19 0x556a19673827 in or_else_tactical::operator()(ref<goal> const&, sref_buffer<goal, 16u>&) ../src/tactic/tactical.cpp:342
    #20 0x556a196798ba in and_then_tactical::operator()(ref<goal> const&, sref_buffer<goal, 16u>&) ../src/tactic/tactical.cpp:122
    #21 0x556a196798ba in and_then_tactical::operator()(ref<goal> const&, sref_buffer<goal, 16u>&) ../src/tactic/tactical.cpp:122
    #22 0x556a1966da41 in cond_tactical::operator()(ref<goal> const&, sref_buffer<goal, 16u>&) ../src/tactic/tactical.cpp:1153
    #23 0x556a1966da41 in cond_tactical::operator()(ref<goal> const&, sref_buffer<goal, 16u>&) ../src/tactic/tactical.cpp:1153
    #24 0x556a1966da41 in cond_tactical::operator()(ref<goal> const&, sref_buffer<goal, 16u>&) ../src/tactic/tactical.cpp:1153
    #25 0x556a1966da41 in cond_tactical::operator()(ref<goal> const&, sref_buffer<goal, 16u>&) ../src/tactic/tactical.cpp:1153
    #26 0x556a1966da41 in cond_tactical::operator()(ref<goal> const&, sref_buffer<goal, 16u>&) ../src/tactic/tactical.cpp:1153
    #27 0x556a1966da41 in cond_tactical::operator()(ref<goal> const&, sref_buffer<goal, 16u>&) ../src/tactic/tactical.cpp:1153
    #28 0x556a1966da41 in cond_tactical::operator()(ref<goal> const&, sref_buffer<goal, 16u>&) ../src/tactic/tactical.cpp:1153
    #29 0x556a196798ba in and_then_tactical::operator()(ref<goal> const&, sref_buffer<goal, 16u>&) ../src/tactic/tactical.cpp:122
    #30 0x556a19640cc4 in exec(tactic&, ref<goal> const&, sref_buffer<goal, 16u>&) ../src/tactic/tactic.cpp:165
    #31 0x556a196426e4 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:185
    #32 0x556a1959dea8 in check_sat_core2 ../src/solver/tactic2solver.cpp:233
    #33 0x556a195c275f in solver_na2as::check_sat_core(unsigned int, expr* const*) ../src/solver/solver_na2as.cpp:67
    #34 0x556a195dc5b4 in combined_solver::check_sat_core(unsigned int, expr* const*) ../src/solver/combined_solver.cpp:253
    #35 0x556a195af1e6 in solver::check_sat(unsigned int, expr* const*) ../src/solver/solver.cpp:318
    #36 0x556a19526ac5 in cmd_context::check_sat(unsigned int, expr* const*) ../src/cmd_context/cmd_context.cpp:1700
    #37 0x556a1947eef3 in smt2::parser::parse_check_sat() ../src/parsers/smt2/smt2parser.cpp:2611
    #38 0x556a1947eef3 in smt2::parser::parse_cmd() ../src/parsers/smt2/smt2parser.cpp:2953
    #39 0x556a1947eef3 in smt2::parser::operator()() ../src/parsers/smt2/smt2parser.cpp:3166
    #40 0x556a19434055 in parse_smt2_commands(cmd_context&, std::istream&, bool, params_ref const&, char const*) ../src/parsers/smt2/smt2parser.cpp:3217

previously allocated by thread T0 here:
    #0 0x7fe5455cbb40 in __interceptor_malloc (/usr/lib/x86_64-linux-gnu/libasan.so.4+0xdeb40)
    #1 0x556a1b3baa7d in memory::allocate(unsigned long) ../src/util/memory_manager.cpp:301
    #2 0x556a1ae11066 in ast_manager::allocate_node(unsigned int) ../src/ast/ast.h:1687
    #3 0x556a1ae11066 in ast_manager::mk_app_core(func_decl*, unsigned int, expr* const*) ../src/ast/ast.cpp:2170
    #4 0x556a1ae000c5 in ast_manager::mk_app(func_decl*, unsigned int, expr* const*) ../src/ast/ast.cpp:2288
    #5 0x556a1ae0f32a in ast_manager::mk_app(int, int, unsigned int, parameter const*, unsigned int, expr* const*, sort*) ../src/ast/ast.cpp:1950
    #6 0x556a1ae0f32a in ast_manager::mk_app(int, int, unsigned int, expr* const*) ../src/ast/ast.cpp:1955
    #7 0x556a1ac0b450 in arith_util::mk_add(unsigned int, expr* const*) const ../src/ast/arith_decl_plugin.h:445
    #8 0x556a1ac0b450 in expr2polynomial::imp::to_expr(obj_ref<polynomial::polynomial, polynomial::manager> const&, bool, obj_ref<expr, ast_manager>&) ../src/ast/expr2polynomial.cpp:456
    #9 0x556a18f2ce6a in factor_tactic::rw_cfg::mk_split_eq(polynomial::manager::factors const&, obj_ref<expr, ast_manager>&) ../src/tactic/arith/factor_tactic.cpp:74
    #10 0x556a18f2ce6a in factor_tactic::rw_cfg::factor(func_decl*, expr*, expr*, obj_ref<expr, ast_manager>&) ../src/tactic/arith/factor_tactic.cpp:201
    #11 0x556a18f328ed in factor_tactic::rw_cfg::reduce_app(func_decl*, unsigned int, expr* const*, obj_ref<expr, ast_manager>&, obj_ref<app, ast_manager>&) ../src/tactic/arith/factor_tactic.cpp:230
    #12 0x556a18f328ed in void rewriter_tpl<factor_tactic::rw_cfg>::process_app<false>(app*, rewriter_core::frame&) ../src/ast/rewriter/rewriter_def.h:316
    #13 0x556a18f33f0d in void rewriter_tpl<factor_tactic::rw_cfg>::resume_core<false>(obj_ref<expr, ast_manager>&, obj_ref<app, ast_manager>&) ../src/ast/rewriter/rewriter_def.h:787
    #14 0x556a18f350dd in void rewriter_tpl<factor_tactic::rw_cfg>::main_loop<false>(expr*, obj_ref<expr, ast_manager>&, obj_ref<app, ast_manager>&) ../src/ast/rewriter/rewriter_def.h:746
    #15 0x556a18f360db in factor_tactic::imp::operator()(ref<goal> const&, sref_buffer<goal, 16u>&) ../src/tactic/arith/factor_tactic.cpp:269
    #16 0x556a18f360db in factor_tactic::operator()(ref<goal> const&, sref_buffer<goal, 16u>&) ../src/tactic/arith/factor_tactic.cpp:313
    #17 0x556a1966c1fc in cleanup_tactical::operator()(ref<goal> const&, sref_buffer<goal, 16u>&) ../src/tactic/tactical.cpp:1032
    #18 0x556a19678a91 in and_then_tactical::operator()(ref<goal> const&, sref_buffer<goal, 16u>&) ../src/tactic/tactical.cpp:113
    #19 0x556a196798ba in and_then_tactical::operator()(ref<goal> const&, sref_buffer<goal, 16u>&) ../src/tactic/tactical.cpp:122
    #20 0x556a196798ba in and_then_tactical::operator()(ref<goal> const&, sref_buffer<goal, 16u>&) ../src/tactic/tactical.cpp:122
    #21 0x556a1966d3f7 in try_for_tactical::operator()(ref<goal> const&, sref_buffer<goal, 16u>&) ../src/tactic/tactical.cpp:1057
    #22 0x556a19673827 in or_else_tactical::operator()(ref<goal> const&, sref_buffer<goal, 16u>&) ../src/tactic/tactical.cpp:342
    #23 0x556a196798ba in and_then_tactical::operator()(ref<goal> const&, sref_buffer<goal, 16u>&) ../src/tactic/tactical.cpp:122
    #24 0x556a196798ba in and_then_tactical::operator()(ref<goal> const&, sref_buffer<goal, 16u>&) ../src/tactic/tactical.cpp:122
    #25 0x556a1966da41 in cond_tactical::operator()(ref<goal> const&, sref_buffer<goal, 16u>&) ../src/tactic/tactical.cpp:1153
    #26 0x556a1966da41 in cond_tactical::operator()(ref<goal> const&, sref_buffer<goal, 16u>&) ../src/tactic/tactical.cpp:1153
    #27 0x556a1966da41 in cond_tactical::operator()(ref<goal> const&, sref_buffer<goal, 16u>&) ../src/tactic/tactical.cpp:1153
    #28 0x556a1966da41 in cond_tactical::operator()(ref<goal> const&, sref_buffer<goal, 16u>&) ../src/tactic/tactical.cpp:1153
    #29 0x556a1966da41 in cond_tactical::operator()(ref<goal> const&, sref_buffer<goal, 16u>&) ../src/tactic/tactical.cpp:1153
    #30 0x556a1966da41 in cond_tactical::operator()(ref<goal> const&, sref_buffer<goal, 16u>&) ../src/tactic/tactical.cpp:1153
    #31 0x556a1966da41 in cond_tactical::operator()(ref<goal> const&, sref_buffer<goal, 16u>&) ../src/tactic/tactical.cpp:1153
    #32 0x556a196798ba in and_then_tactical::operator()(ref<goal> const&, sref_buffer<goal, 16u>&) ../src/tactic/tactical.cpp:122
    #33 0x556a19640cc4 in exec(tactic&, ref<goal> const&, sref_buffer<goal, 16u>&) ../src/tactic/tactic.cpp:165
    #34 0x556a196426e4 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:185
    #35 0x556a1959dea8 in check_sat_core2 ../src/solver/tactic2solver.cpp:233

SUMMARY: AddressSanitizer: heap-use-after-free ../src/util/obj_hashtable.h:35 in obj_hash_entry<expr>::get_hash() const
Shadow bytes around the buggy address:
  0x0c2480010790: fd fd fd fd fd fd fd fd fd fd fd fd fd fd fd fd
  0x0c24800107a0: fd fd fd fd fd fd fd fd fd fd fa fa fa fa fa fa
  0x0c24800107b0: fa fa fa fa fa fa fa fa fd fd fd fd fd fd fd fd
  0x0c24800107c0: fd fd fd fd fd fd fd fd fd fd fd fd fd fd fd fd
  0x0c24800107d0: fd fd fd fd fd fd fd fd fd fd fa fa fa fa fa fa
=>0x0c24800107e0: fa fa fa fa fa fa fa fa fd[fd]fd fd fd fd fd fd
  0x0c24800107f0: fd fd fd fd fd fd fd fd fd fd fd fd fd fd fd fd
  0x0c2480010800: fd fd fd fd fd fd fd fd fd fa fa fa fa fa fa fa
  0x0c2480010810: fa fa fa fa fa fa fa fa 00 00 00 00 00 00 00 00
  0x0c2480010820: 00 00 00 00 00 00 00 00 00 00 00 00 00 00 00 00
  0x0c2480010830: 00 00 00 00 00 00 00 00 00 00 00 00 00 00 00 00
Shadow byte legend (one shadow byte represents 8 application bytes):
  Addressable:           00
  Partially addressable: 01 02 03 04 05 06 07 
  Heap left redzone:       fa
  Freed heap region:       fd
  Stack left redzone:      f1
  Stack mid redzone:       f2
  Stack right redzone:     f3
  Stack after return:      f5
  Stack use after scope:   f8
  Global redzone:          f9
  Global init order:       f6
  Poisoned by user:        f7
  Container overflow:      fc
  Array cookie:            ac
  Intra object redzone:    bb
  ASan internal:           fe
  Left alloca redzone:     ca
  Right alloca redzone:    cb
==2913==ABORTING
[521] % 
[521] % cat small.smt2
(declare-fun a () Real)
(declare-fun b () Real)
(declare-fun c () Real)
(declare-fun d () Real)
(declare-fun e () Real)
(declare-fun f () Real)
(declare-fun g () Real)
(declare-fun h () Real)
(declare-fun i () Real)
(declare-fun j () Real)
(declare-fun k () Real)
(declare-fun l () Real)
(declare-fun m () Real)
(declare-fun n () Real)
(declare-fun o () Real)
(assert (= (* i o) (* m j) h))
(assert (= (+ g k o) 0))
(assert (distinct (* h a b) a))
(assert (= h (- d b)))
(assert (= (- c n l) e g))
(assert (= j c (+ d (* e f))))
(assert (> o 0))
(check-sat)
NikolajBjorner added a commit that referenced this issue Dec 30, 2022
@NikolajBjorner
fix #6513
293627c 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
hgvk94 pushed a commit to hgvk94/z3 that referenced this issue Mar 27, 2023
@NikolajBjorner @hgvk94
fix Z3Prover#6513
81e77fb 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
hgvk94 pushed a commit to hgvk94/z3 that referenced this issue Mar 27, 2023
@NikolajBjorner @hgvk94
fix Z3Prover#6513
100c733 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
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
@zhendongsu