search

Z3Prover / z3

The Z3 Theorem Prover
Other
10.29k stars 1.48k forks source link

Master and debug branch: Use after free issue in dyn_ack_manager::del_clause_eh #3479

Closed 5hadowblad3 closed 4 years ago

5hadowblad3 commented 4 years ago

Hi, there.

There is a use after free issue that causes segmentation fault using z3 in both master and debug branch.

To reproduce this issue, simply run z3 poc.smt2 z3-uaf-dyn_ack.smt2.zip

Similar triggering point to #3246, #3347, but this time the condition to trigger the problem relates to garbage collection.

OS: Ubuntu 16.06 commit 37bc4a4

Here is the trace reported by ASAN.

==9354==ERROR: AddressSanitizer: heap-use-after-free on address 0x6070000776c4 at pc 0x0000004610ed bp 0x7ffd5eca7570 sp 0x7ffd5eca7560
READ of size 4 at 0x6070000776c4 thread T0
    #0 0x4610ec in ast::hash() const ../src/ast/ast.h:505
    #1 0x10e6160 in obj_ptr_triple_hash<app, app, app>::operator()(triple<app*, app*, app*> const&) const ../src/util/hash.h:217
    #2 0x10e281e in core_hashtable<obj_triple_hash_entry<app, app, app>, obj_ptr_triple_hash<app, app, app>, default_eq<triple<app*, app*, app*> > >::get_hash(triple<app*, app*, app*> const&) const ../src/util/hashtable.h:156
    #3 0x10dea70 in core_hashtable<obj_triple_hash_entry<app, app, app>, obj_ptr_triple_hash<app, app, app>, default_eq<triple<app*, app*, app*> > >::remove(triple<app*, app*, app*> const&) ../src/util/hashtable.h:549
    #4 0x10d927e in core_hashtable<obj_triple_hash_entry<app, app, app>, obj_ptr_triple_hash<app, app, app>, default_eq<triple<app*, app*, app*> > >::erase(triple<app*, app*, app*> const&) ../src/util/hashtable.h:582
    #5 0x10d1ca5 in smt::dyn_ack_manager::del_clause_eh(smt::clause*) ../src/smt/dyn_ack.cpp:369
    #6 0x10d7c4f in smt::dyn_ack_clause_del_eh::operator()(ast_manager&, smt::clause*) ../src/smt/dyn_ack.cpp:351
    #7 0x1187cbd in smt::clause::deallocate(ast_manager&) ../src/smt/smt_clause.cpp:75
    #8 0x11aa8aa in smt::context::del_clause(bool, smt::clause*) ../src/smt/smt_context.cpp:2041
    #9 0x11aa9c8 in smt::context::del_clauses(old_ptr_vector<smt::clause>&, unsigned int) ../src/smt/smt_context.cpp:2055
    #10 0x11b34be in smt::context::flush() ../src/smt/smt_context.cpp:2934
    #11 0x1197cbe in smt::context::~context() ../src/smt/smt_context.cpp:247
    #12 0x112739d in smt::kernel::imp::~imp() ../src/smt/smt_kernel.cpp:27
    #13 0x1127500 in void deallocf<smt::kernel::imp>(char const*, int, smt::kernel::imp*) ../src/util/memory_manager.h:85
    #14 0x1125429 in smt::kernel::~kernel() ../src/smt/smt_kernel.cpp:225
    #15 0xda2dab in ~smt_solver ../src/smt/smt_solver.cpp:103
    #16 0x46ad3f in void deallocf<check_sat_result>(char const*, int, check_sat_result*) ../src/util/memory_manager.h:85
    #17 0x461be6 in check_sat_result::dec_ref() ../src/solver/check_sat_result.h:49
    #18 0x46c86f in ref<solver>::dec_ref() ../src/util/ref.h:34
    #19 0x46addd in ref<solver>::~ref() ../src/util/ref.h:55
    #20 0x1987786 in combined_solver::~combined_solver() ../src/solver/combined_solver.cpp:45
    #21 0x46ad3f in void deallocf<check_sat_result>(char const*, int, check_sat_result*) ../src/util/memory_manager.h:85
    #22 0x461be6 in check_sat_result::dec_ref() ../src/solver/check_sat_result.h:49
    #23 0x46c86f in ref<solver>::dec_ref() ../src/util/ref.h:34
    #24 0x51bf4a in ref<solver>::operator=(solver*) ../src/util/ref.h:81
    #25 0x1933613 in cmd_context::reset(bool) ../src/cmd_context/cmd_context.cpp:1310
    #26 0x192a37e in cmd_context::~cmd_context() ../src/cmd_context/cmd_context.cpp:503
    #27 0x41f0d6 in read_smtlib2_commands(char const*) ../src/shell/smtlib_frontend.cpp:69
    #28 0x415b1e in main ../src/shell/main.cpp:352
    #29 0x7f364ecaa82f in __libc_start_main (/lib/x86_64-linux-gnu/libc.so.6+0x2082f)
    #30 0x414888 in _start (/home/heqing/dependence/z3-debug/build/z3+0x414888)

0x6070000776c4 is located 20 bytes inside of 76-byte region [0x6070000776b0,0x6070000776fc)
freed by thread T0 here:
    #0 0x7f364fbaa2ca in __interceptor_free (/usr/lib/x86_64-linux-gnu/libasan.so.2+0x982ca)
    #1 0x25463ef in memory::deallocate(void*) ../src/util/memory_manager.cpp:260
    #2 0x24ef596 in small_object_allocator::deallocate(unsigned long, void*) ../src/util/small_object_allocator.cpp:77
    #3 0x21fa3d6 in ast_manager::deallocate_node(ast*, unsigned int) ../src/ast/ast.h:1733
    #4 0x21e7de8 in ast_manager::delete_node(ast*) ../src/ast/ast.cpp:1997
    #5 0x42264c in ast_manager::dec_ref(ast*) ../src/ast/ast.h:1692
    #6 0x45f38a in ref_manager_wrapper<expr, ast_manager>::dec_ref(expr*) ../src/util/ref_vector.h:199
    #7 0x45f340 in ref_vector_core<expr, ref_manager_wrapper<expr, ast_manager> >::dec_ref(expr*) ../src/util/ref_vector.h:37
    #8 0x593a65 in ref_vector_core<expr, ref_manager_wrapper<expr, ast_manager> >::pop_back() ../src/util/ref_vector.h:113
    #9 0x110c9f7 in smt::context::undo_mk_enode() ../src/smt/smt_internalizer.cpp:1024
    #10 0x11c922d in smt::context::mk_enode_trail::undo(smt::context&) ../src/smt/smt_context.h:783
    #11 0x11ce1b7 in void undo_trail_stack<smt::context>(smt::context&, old_ptr_vector<trail<smt::context> >&, unsigned int) ../src/util/trail.h:332
    #12 0x11a9e63 in smt::context::undo_trail_stack(unsigned int) ../src/smt/smt_context.cpp:1974
    #13 0x11b345a in smt::context::flush() ../src/smt/smt_context.cpp:2931
    #14 0x1197cbe in smt::context::~context() ../src/smt/smt_context.cpp:247
    #15 0x112739d in smt::kernel::imp::~imp() ../src/smt/smt_kernel.cpp:27
    #16 0x1127500 in void deallocf<smt::kernel::imp>(char const*, int, smt::kernel::imp*) ../src/util/memory_manager.h:85
    #17 0x1125429 in smt::kernel::~kernel() ../src/smt/smt_kernel.cpp:225
    #18 0xda2dab in ~smt_solver ../src/smt/smt_solver.cpp:103
    #19 0x46ad3f in void deallocf<check_sat_result>(char const*, int, check_sat_result*) ../src/util/memory_manager.h:85
    #20 0x461be6 in check_sat_result::dec_ref() ../src/solver/check_sat_result.h:49
    #21 0x46c86f in ref<solver>::dec_ref() ../src/util/ref.h:34
    #22 0x46addd in ref<solver>::~ref() ../src/util/ref.h:55
    #23 0x1987786 in combined_solver::~combined_solver() ../src/solver/combined_solver.cpp:45
    #24 0x46ad3f in void deallocf<check_sat_result>(char const*, int, check_sat_result*) ../src/util/memory_manager.h:85
    #25 0x461be6 in check_sat_result::dec_ref() ../src/solver/check_sat_result.h:49
    #26 0x46c86f in ref<solver>::dec_ref() ../src/util/ref.h:34
    #27 0x51bf4a in ref<solver>::operator=(solver*) ../src/util/ref.h:81
    #28 0x1933613 in cmd_context::reset(bool) ../src/cmd_context/cmd_context.cpp:1310
    #29 0x192a37e in cmd_context::~cmd_context() ../src/cmd_context/cmd_context.cpp:503

previously allocated by thread T0 here:
    #0 0x7f364fbaa602 in malloc (/usr/lib/x86_64-linux-gnu/libasan.so.2+0x98602)
    #1 0x254643b in memory::allocate(unsigned long) ../src/util/memory_manager.cpp:268
    #2 0x24ef5c7 in small_object_allocator::allocate(unsigned long) ../src/util/small_object_allocator.cpp:103
    #3 0x21fa3a6 in ast_manager::allocate_node(unsigned int) ../src/ast/ast.h:1729
    #4 0x21ea1a7 in ast_manager::mk_app_core(func_decl*, unsigned int, expr* const*) ../src/ast/ast.cpp:2235
    #5 0x21eb692 in ast_manager::mk_app(func_decl*, unsigned int, expr* const*) ../src/ast/ast.cpp:2351
    #6 0x21e807d in ast_manager::mk_app(int, int, unsigned int, parameter const*, unsigned int, expr* const*, sort*) ../src/ast/ast.cpp:2028
    #7 0x154f8de in smt::theory_array_base::mk_select(unsigned int, expr* const*) ../src/smt/theory_array_base.cpp:50
    #8 0x15533c9 in smt::theory_array_base::assert_extensionality_core(smt::enode*, smt::enode*) ../src/smt/theory_array_base.cpp:346
    #9 0x1554720 in smt::theory_array_base::propagate() ../src/smt/theory_array_base.cpp:428
    #10 0x11a6b03 in smt::context::propagate_theories() ../src/smt/smt_context.cpp:1657
    #11 0x11a7898 in smt::context::propagate() ../src/smt/smt_context.cpp:1740
    #12 0x11bdbf2 in smt::context::bounded_search() ../src/smt/smt_context.cpp:3762
    #13 0x11bbe1b in smt::context::search() ../src/smt/smt_context.cpp:3646
    #14 0x11ba3a3 in smt::context::check(unsigned int, expr* const*, bool) ../src/smt/smt_context.cpp:3531
    #15 0x1126e64 in smt::kernel::imp::check(unsigned int, expr* const*) ../src/smt/smt_kernel.cpp:116
    #16 0x1125b45 in smt::kernel::check(unsigned int, expr* const*) ../src/smt/smt_kernel.cpp:296
    #17 0xda3ab4 in check_sat_core2 ../src/smt/smt_solver.cpp:190
    #18 0x197197f in solver_na2as::check_sat_core(unsigned int, expr* const*) ../src/solver/solver_na2as.cpp:67
    #19 0x19860b8 in combined_solver::check_sat_core(unsigned int, expr* const*) ../src/solver/combined_solver.cpp:219
    #20 0x1970359 in solver::check_sat(unsigned int, expr* const*) ../src/solver/solver.cpp:330
    #21 0x19363a0 in cmd_context::check_sat(unsigned int, expr* const*) ../src/cmd_context/cmd_context.cpp:1581
    #22 0x18c29a3 in smt2::parser::parse_check_sat() ../src/parsers/smt2/smt2parser.cpp:2596
    #23 0x18c693f in smt2::parser::parse_cmd() ../src/parsers/smt2/smt2parser.cpp:2938
    #24 0x18c8051 in smt2::parser::operator()() ../src/parsers/smt2/smt2parser.cpp:3130
    #25 0x18a7036 in parse_smt2_commands(cmd_context&, std::istream&, bool, params_ref const&, char const*) ../src/parsers/smt2/smt2parser.cpp:3179
    #26 0x41f02b in read_smtlib2_commands(char const*) ../src/shell/smtlib_frontend.cpp:89
    #27 0x415b1e in main ../src/shell/main.cpp:352
    #28 0x7f364ecaa82f in __libc_start_main (/lib/x86_64-linux-gnu/libc.so.6+0x2082f)

SUMMARY: AddressSanitizer: heap-use-after-free ../src/ast/ast.h:505 ast::hash() const
Shadow bytes around the buggy address:
  0x0c0e80006e80: fa fa fd fd fd fd fd fd fd fd fd fd fa fa fa fa
  0x0c0e80006e90: fd fd fd fd fd fd fd fd fd fd fa fa fa fa fd fd
  0x0c0e80006ea0: fd fd fd fd fd fd fd fd fa fa fa fa 00 00 00 00
  0x0c0e80006eb0: 00 00 00 00 00 fa fa fa fa fa fd fd fd fd fd fd
  0x0c0e80006ec0: fd fd fd fd fa fa fa fa fd fd fd fd fd fd fd fd
=>0x0c0e80006ed0: fd fd fa fa fa fa fd fd[fd]fd fd fd fd fd fd fd
  0x0c0e80006ee0: fa fa fa fa fd fd fd fd fd fd fd fd fd fd fa fa
  0x0c0e80006ef0: fa fa fd fd fd fd fd fd fd fd fd fd fa fa fa fa
  0x0c0e80006f00: 00 00 00 00 00 00 00 00 00 00 fa fa fa fa 00 00
  0x0c0e80006f10: 00 00 00 00 00 00 00 04 fa fa fa fa 00 00 00 00
  0x0c0e80006f20: 00 00 00 00 00 00 fa fa fa fa 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
  Heap right redzone:      fb
  Freed heap region:       fd
  Stack left redzone:      f1
  Stack mid redzone:       f2
  Stack right redzone:     f3
  Stack partial redzone:   f4
  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
==9354==ABORTING
rainoftime commented 4 years ago

Seems duplicate with https://github.com/Z3Prover/z3/issues/3423

5hadowblad3 commented 4 years ago

A bit different from the previous issues, may need extra attention to avoid incomplete fix.

NikolajBjorner commented 4 years ago

makes more sense to file under #3423, the stacks are about the same and fix is aimed to delay undo_trail_stack until after the clauses are finalized.