heap buffer overflows in mk_app_core

[5hadowblad3]

Hi, there.

There is a buffer overflow in z3 (commit 65b2037) that causes the segmentation fault.

To reproduce, run
z3 poc.smt2
z3-overflow_mk_app_core.smt2.zip

Here is the trace reported by ASAN:

==55623==ERROR: AddressSanitizer: heap-buffer-overflow on address 0x625000007100 at pc 0x7f91fb52aa6a bp 0x7f91f693f0b0 sp 0x7f91f693e858
READ of size 8193 at 0x625000007100 thread T4
    #0 0x7f91fb52aa69  (/usr/lib/x86_64-linux-gnu/libasan.so.2+0x46a69)
    #1 0x7f91fb52adfc in __interceptor_writev (/usr/lib/x86_64-linux-gnu/libasan.so.2+0x46dfc)
    #2 0x7f91faff52e4 in std::__basic_file<char>::xsputn_2(char const*, long, char const*, long) (/usr/lib/x86_64-linux-gnu/libstdc++.so.6+0xb02e4)
    #3 0x7f91fb02fe71 in std::basic_filebuf<char, std::char_traits<char> >::xsputn(char const*, long) (/usr/lib/x86_64-linux-gnu/libstdc++.so.6+0xeae71)
    #4 0x7f91fb053ec5 in std::basic_ostream<char, std::char_traits<char> >& std::__ostream_insert<char, std::char_traits<char> >(std::basic_ostream<char, std::char_traits<char> >&, char const*, long) (/usr/lib/x86_64-linux-gnu/libstdc++.so.6+0x10eec5)
    #5 0x7f91fb054236 in std::basic_ostream<char, std::char_traits<char> >& std::operator<< <std::char_traits<char> >(std::basic_ostream<char, std::char_traits<char> >&, char const*) (/usr/lib/x86_64-linux-gnu/libstdc++.so.6+0x10f236)
    #6 0x21e8029 in ast_manager::mk_app_core(func_decl*, unsigned int, expr* const*) ../src/ast/ast.cpp:2283
    #7 0x21e8dd8 in ast_manager::mk_app(func_decl*, unsigned int, expr* const*) ../src/ast/ast.cpp:2362
    #8 0x21e57c3 in ast_manager::mk_app(int, int, unsigned int, parameter const*, unsigned int, expr* const*, sort*) ../src/ast/ast.cpp:2039
    #9 0x226b4ca in format_ns::mk_indent(ast_manager&, unsigned int, app*) ../src/ast/format.cpp:168
    #10 0x2152032 in smt2_printer::process_app(app*, smt2_printer::frame&) ../src/ast/ast_smt2_pp.cpp:775
    #11 0x2155b5e in smt2_printer::process(expr*, obj_ref<app, ast_manager>&) ../src/ast/ast_smt2_pp.cpp:1060
    #12 0x21567c5 in smt2_printer::operator()(expr*, unsigned int, char const*, obj_ref<app, ast_manager>&, old_sbuffer<symbol, 16u>&) ../src/ast/ast_smt2_pp.cpp:1125
    #13 0x214a831 in mk_smt2_format(expr*, smt2_pp_environment&, params_ref const&, unsigned int, char const*, obj_ref<app, ast_manager>&, old_sbuffer<symbol, 16u>&) ../src/ast/ast_smt2_pp.cpp:1201
    #14 0x214b516 in ast_smt2_pp(std::ostream&, expr*, smt2_pp_environment&, params_ref const&, unsigned int, unsigned int, char const*) ../src/ast/ast_smt2_pp.cpp:1240
    #15 0x214cee0 in operator<<(std::ostream&, mk_ismt2_pp const&) ../src/ast/ast_smt2_pp.cpp:1341
    #16 0x116809a in smt::context::display_literal_smt2(std::ostream&, smt::literal) const ../src/smt/smt_context_pp.cpp:108
    #17 0x1168158 in smt::context::display_literals_smt2(std::ostream&, unsigned int, smt::literal const*) const ../src/smt/smt_context_pp.cpp:114
    #18 0x116d768 in smt::context::display(std::ostream&, smt::b_justification) const ../src/smt/smt_context_pp.cpp:604
    #19 0x116da9c in smt::context::trace_assign(smt::literal, smt::b_justification, bool) const ../src/smt/smt_context_pp.cpp:629
    #20 0x118bb45 in smt::context::assign_core(smt::literal, smt::b_justification, bool) ../src/smt/smt_context.cpp:345
    #21 0x118cac3 in smt::context::bcp() ../src/smt/smt_context.cpp:445
    #22 0x1199cca in smt::context::propagate() ../src/smt/smt_context.cpp:1726
    #23 0x11b03f6 in smt::context::bounded_search() ../src/smt/smt_context.cpp:3775
    #24 0x11ae620 in smt::context::search() ../src/smt/smt_context.cpp:3659
    #25 0x11acb99 in smt::context::check(unsigned int, expr* const*, bool) ../src/smt/smt_context.cpp:3542
    #26 0x125dc2d in smt::parallel::operator()(ref_vector<expr, ast_manager> const&)::{lambda(int)#3}::operator()(int) const (/home/heqing/dependence/z3/build/z3+0x125dc2d)
    #27 0x125e72f in smt::parallel::operator()(ref_vector<expr, ast_manager> const&)::{lambda()#4}::operator()() const (/home/heqing/dependence/z3/build/z3+0x125e72f)
    #28 0x12618af in _M_invoke<> /usr/include/c++/5/functional:1531
    #29 0x12617c3 in operator() /usr/include/c++/5/functional:1520
    #30 0x1261753 in _M_run /usr/include/c++/5/thread:115
    #31 0x7f91faffdc7f  (/usr/lib/x86_64-linux-gnu/libstdc++.so.6+0xb8c7f)
    #32 0x7f91fb2ce6b9 in start_thread (/lib/x86_64-linux-gnu/libpthread.so.0+0x76b9)
    #33 0x7f91fa76341c in clone (/lib/x86_64-linux-gnu/libc.so.6+0x10741c)

0x625000007100 is located 0 bytes to the right of 8192-byte region [0x625000005100,0x625000007100)
allocated by thread T0 here:
    #0 0x7f91fb57d6b2 in operator new[](unsigned long) (/usr/lib/x86_64-linux-gnu/libasan.so.2+0x996b2)
    #1 0x7f91fb031467 in std::basic_filebuf<char, std::char_traits<char> >::_M_allocate_internal_buffer() (/usr/lib/x86_64-linux-gnu/libstdc++.so.6+0xec467)

Thread T4 created by T0 here:
    #0 0x7f91fb51a253 in pthread_create (/usr/lib/x86_64-linux-gnu/libasan.so.2+0x36253)
    #1 0x7f91faffddc2 in std::thread::_M_start_thread(std::shared_ptr<std::thread::_Impl_base>, void (*)()) (/usr/lib/x86_64-linux-gnu/libstdc++.so.6+0xb8dc2)

SUMMARY: AddressSanitizer: heap-buffer-overflow ??:0 ??
Shadow bytes around the buggy address:
  0x0c4a7fff8dd0: 00 00 00 00 00 00 00 00 00 00 00 00 00 00 00 00
  0x0c4a7fff8de0: 00 00 00 00 00 00 00 00 00 00 00 00 00 00 00 00
  0x0c4a7fff8df0: 00 00 00 00 00 00 00 00 00 00 00 00 00 00 00 00
  0x0c4a7fff8e00: 00 00 00 00 00 00 00 00 00 00 00 00 00 00 00 00
  0x0c4a7fff8e10: 00 00 00 00 00 00 00 00 00 00 00 00 00 00 00 00
=>0x0c4a7fff8e20:[fa]fa fa fa fa fa fa fa fa fa fa fa fa fa fa fa
  0x0c4a7fff8e30: fa fa fa fa fa fa fa fa fa fa fa fa fa fa fa fa
  0x0c4a7fff8e40: fa fa fa fa fa fa fa fa fa fa fa fa fa fa fa fa
  0x0c4a7fff8e50: fa fa fa fa fa fa fa fa fa fa fa fa fa fa fa fa
  0x0c4a7fff8e60: fa fa fa fa fa fa fa fa fa fa fa fa fa fa fa fa
  0x0c4a7fff8e70: fa fa fa fa fa fa fa fa fa fa fa fa fa fa fa fa
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
==55623==ABORTING

commit 65b2037

[NikolajBjorner]

threads + trace = don't do it