CVE-2020-19725: use after free in ../src/math/grobner/pdd_simplifier.cpp:131 · Issue #3363 · Z3Prover/z3

Hi, there.

There is a use after free issue that causes segmentation fault using z3.

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

OS: Ubuntu 16.06
commit 6ad261e

Here is the trace reported by ASAN.

==42916==ERROR: AddressSanitizer: heap-use-after-free on address 0x603000057aa8 at pc 0x000002126476 bp 0x7ffce1825cf0 sp 0x7ffce1825ce0
READ of size 8 at 0x603000057aa8 thread T0
    #0 0x2126475 in dd::simplifier::simplify_linear_step(old_ptr_vector<dd::solver::equation>&) ../src/math/grobner/pdd_simplifier.cpp:131
    #1 0x2125e9c in dd::simplifier::simplify_linear_step(bool) ../src/math/grobner/pdd_simplifier.cpp:103
    #2 0x2125862 in dd::simplifier::operator()() ../src/math/grobner/pdd_simplifier.cpp:69
    #3 0x211ffda in dd::solver::simplify() ../src/math/grobner/pdd_solver.cpp:135
    #4 0x211f6af in dd::solver::saturate() ../src/math/grobner/pdd_solver.cpp:93
    #5 0x1e14c8b in nla::core::run_grobner() ../src/math/lp/nla_core.cpp:1403
    #6 0x1e136dd in nla::core::inner_check(bool) ../src/math/lp/nla_core.cpp:1288
    #7 0x1e13ed2 in nla::core::check(old_vector<nla::lemma, true, unsigned int>&) ../src/math/lp/nla_core.cpp:1341
    #8 0x1d4dbbd in nla::solver::check(old_vector<nla::lemma, true, unsigned int>&) ../src/math/lp/nla_solver.cpp:40
    #9 0xdc9029 in smt::theory_lra::imp::check_nra() (/home/heqing/dependence/z3/build/z3+0xdc9029)
    #10 0xdc1d03 in smt::theory_lra::imp::final_check_eh() ../src/smt/theory_lra.cpp:1753
    #11 0xda83e4 in smt::theory_lra::final_check_eh() ../src/smt/theory_lra.cpp:3976
    #12 0x11bac65 in smt::context::final_check() ../src/smt/smt_context.cpp:3904
    #13 0x11b9c6e in smt::context::bounded_search() ../src/smt/smt_context.cpp:3819
    #14 0x11b73a9 in smt::context::search() ../src/smt/smt_context.cpp:3646
    #15 0x11b4da4 in smt::context::setup_and_check(bool) ../src/smt/smt_context.cpp:3471
    #16 0x112257a in smt::kernel::imp::setup_and_check() ../src/smt/smt_kernel.cpp:108
    #17 0x1121255 in smt::kernel::setup_and_check() ../src/smt/smt_kernel.cpp:292
    #18 0xc496e6 in smt_tactic::operator()(ref<goal> const&, sref_buffer<goal, 16u>&) ../src/smt/tactic/smt_tactic.cpp:200
    #19 0x19d7aa3 in and_then_tactical::operator()(ref<goal> const&, sref_buffer<goal, 16u>&) ../src/tactic/tactical.cpp:120
    #20 0x19def27 in try_for_tactical::operator()(ref<goal> const&, sref_buffer<goal, 16u>&) ../src/tactic/tactical.cpp:933
    #21 0x19d8ea5 in or_else_tactical::operator()(ref<goal> const&, sref_buffer<goal, 16u>&) ../src/tactic/tactical.cpp:296
    #22 0x19d7aa3 in and_then_tactical::operator()(ref<goal> const&, sref_buffer<goal, 16u>&) ../src/tactic/tactical.cpp:120
    #23 0x19d7aa3 in and_then_tactical::operator()(ref<goal> const&, sref_buffer<goal, 16u>&) ../src/tactic/tactical.cpp:120
    #24 0x19dff24 in cond_tactical::operator()(ref<goal> const&, sref_buffer<goal, 16u>&) ../src/tactic/tactical.cpp:1023
    #25 0x19dff8e in cond_tactical::operator()(ref<goal> const&, sref_buffer<goal, 16u>&) ../src/tactic/tactical.cpp:1025
    #26 0x19dff8e in cond_tactical::operator()(ref<goal> const&, sref_buffer<goal, 16u>&) ../src/tactic/tactical.cpp:1025
    #27 0x19dff8e in cond_tactical::operator()(ref<goal> const&, sref_buffer<goal, 16u>&) ../src/tactic/tactical.cpp:1025
    #28 0x19dff8e in cond_tactical::operator()(ref<goal> const&, sref_buffer<goal, 16u>&) ../src/tactic/tactical.cpp:1025
    #29 0x19dff8e in cond_tactical::operator()(ref<goal> const&, sref_buffer<goal, 16u>&) ../src/tactic/tactical.cpp:1025
    #30 0x19dff8e in cond_tactical::operator()(ref<goal> const&, sref_buffer<goal, 16u>&) ../src/tactic/tactical.cpp:1025
    #31 0x19dff8e in cond_tactical::operator()(ref<goal> const&, sref_buffer<goal, 16u>&) ../src/tactic/tactical.cpp:1025
    #32 0x19d7aa3 in and_then_tactical::operator()(ref<goal> const&, sref_buffer<goal, 16u>&) ../src/tactic/tactical.cpp:120
    #33 0x19dd595 in unary_tactical::operator()(ref<goal> const&, sref_buffer<goal, 16u>&) ../src/tactic/tactical.cpp:763
    #34 0x1a0cc80 in exec(tactic&, ref<goal> const&, sref_buffer<goal, 16u>&) ../src/tactic/tactic.cpp:148
    #35 0x1a0d11b 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:168
    #36 0x19830fb in check_sat_core2 ../src/solver/tactic2solver.cpp:176
    #37 0x196bcb1 in solver_na2as::check_sat_core(unsigned int, expr* const*) ../src/solver/solver_na2as.cpp:67
    #38 0x19807b0 in combined_solver::check_sat_core(unsigned int, expr* const*) ../src/solver/combined_solver.cpp:246
    #39 0x196a68b in solver::check_sat(unsigned int, expr* const*) ../src/solver/solver.cpp:330
    #40 0x19306d2 in cmd_context::check_sat(unsigned int, expr* const*) ../src/cmd_context/cmd_context.cpp:1581
    #41 0x18bcc6b in smt2::parser::parse_check_sat() ../src/parsers/smt2/smt2parser.cpp:2596
    #42 0x18c0c07 in smt2::parser::parse_cmd() ../src/parsers/smt2/smt2parser.cpp:2938
    #43 0x18c2319 in smt2::parser::operator()() ../src/parsers/smt2/smt2parser.cpp:3130
    #44 0x18a12fe in parse_smt2_commands(cmd_context&, std::istream&, bool, params_ref const&, char const*) ../src/parsers/smt2/smt2parser.cpp:3179
    #45 0x41efab in read_smtlib2_commands(char const*) ../src/shell/smtlib_frontend.cpp:89
    #46 0x415a9e in main ../src/shell/main.cpp:352
    #47 0x7f65a714482f in __libc_start_main (/lib/x86_64-linux-gnu/libc.so.6+0x2082f)
    #48 0x414808 in _start (/home/heqing/dependence/z3/build/z3+0x414808)

0x603000057aa8 is located 24 bytes inside of 32-byte region [0x603000057a90,0x603000057ab0)
freed by thread T0 here:
    #0 0x7f65a8044961 in realloc (/usr/lib/x86_64-linux-gnu/libasan.so.2+0x98961)
    #1 0x253bf9c in memory::reallocate(void*, unsigned long) ../src/util/memory_manager.cpp:295
    #2 0x212548d in old_vector<dd::solver::equation*, false, unsigned int>::expand_vector() ../src/util/old_vector.h:87
    #3 0x2124abe in old_vector<dd::solver::equation*, false, unsigned int>::push_back(dd::solver::equation* const&) ../src/util/old_vector.h:419
    #4 0x2129020 in dd::simplifier::add_to_use(dd::solver::equation*, old_vector<old_ptr_vector<dd::solver::equation>, true, unsigned int>&) ../src/math/grobner/pdd_simplifier.cpp:350
    #5 0x2126789 in dd::simplifier::simplify_linear_step(old_ptr_vector<dd::solver::equation>&) ../src/math/grobner/pdd_simplifier.cpp:156
    #6 0x2125e9c in dd::simplifier::simplify_linear_step(bool) ../src/math/grobner/pdd_simplifier.cpp:103
    #7 0x2125862 in dd::simplifier::operator()() ../src/math/grobner/pdd_simplifier.cpp:69
    #8 0x211ffda in dd::solver::simplify() ../src/math/grobner/pdd_solver.cpp:135
    #9 0x211f6af in dd::solver::saturate() ../src/math/grobner/pdd_solver.cpp:93
    #10 0x1e14c8b in nla::core::run_grobner() ../src/math/lp/nla_core.cpp:1403
    #11 0x1e136dd in nla::core::inner_check(bool) ../src/math/lp/nla_core.cpp:1288
    #12 0x1e13ed2 in nla::core::check(old_vector<nla::lemma, true, unsigned int>&) ../src/math/lp/nla_core.cpp:1341
    #13 0x1d4dbbd in nla::solver::check(old_vector<nla::lemma, true, unsigned int>&) ../src/math/lp/nla_solver.cpp:40
    #14 0xdc9029 in smt::theory_lra::imp::check_nra() (/home/heqing/dependence/z3/build/z3+0xdc9029)
    #15 0xdc1d03 in smt::theory_lra::imp::final_check_eh() ../src/smt/theory_lra.cpp:1753
    #16 0xda83e4 in smt::theory_lra::final_check_eh() ../src/smt/theory_lra.cpp:3976
    #17 0x11bac65 in smt::context::final_check() ../src/smt/smt_context.cpp:3904
    #18 0x11b9c6e in smt::context::bounded_search() ../src/smt/smt_context.cpp:3819
    #19 0x11b73a9 in smt::context::search() ../src/smt/smt_context.cpp:3646
    #20 0x11b4da4 in smt::context::setup_and_check(bool) ../src/smt/smt_context.cpp:3471
    #21 0x112257a in smt::kernel::imp::setup_and_check() ../src/smt/smt_kernel.cpp:108
    #22 0x1121255 in smt::kernel::setup_and_check() ../src/smt/smt_kernel.cpp:292
    #23 0xc496e6 in smt_tactic::operator()(ref<goal> const&, sref_buffer<goal, 16u>&) ../src/smt/tactic/smt_tactic.cpp:200
    #24 0x19d7aa3 in and_then_tactical::operator()(ref<goal> const&, sref_buffer<goal, 16u>&) ../src/tactic/tactical.cpp:120
    #25 0x19def27 in try_for_tactical::operator()(ref<goal> const&, sref_buffer<goal, 16u>&) ../src/tactic/tactical.cpp:933
    #26 0x19d8ea5 in or_else_tactical::operator()(ref<goal> const&, sref_buffer<goal, 16u>&) ../src/tactic/tactical.cpp:296
    #27 0x19d7aa3 in and_then_tactical::operator()(ref<goal> const&, sref_buffer<goal, 16u>&) ../src/tactic/tactical.cpp:120
    #28 0x19d7aa3 in and_then_tactical::operator()(ref<goal> const&, sref_buffer<goal, 16u>&) ../src/tactic/tactical.cpp:120
    #29 0x19dff24 in cond_tactical::operator()(ref<goal> const&, sref_buffer<goal, 16u>&) ../src/tactic/tactical.cpp:1023

previously allocated by thread T0 here:
    #0 0x7f65a8044602 in malloc (/usr/lib/x86_64-linux-gnu/libasan.so.2+0x98602)
    #1 0x253bdd5 in memory::allocate(unsigned long) ../src/util/memory_manager.cpp:268
    #2 0x21251bc in old_vector<dd::solver::equation*, false, unsigned int>::expand_vector() ../src/util/old_vector.h:65
    #3 0x2124abe in old_vector<dd::solver::equation*, false, unsigned int>::push_back(dd::solver::equation* const&) ../src/util/old_vector.h:419
    #4 0x2129020 in dd::simplifier::add_to_use(dd::solver::equation*, old_vector<old_ptr_vector<dd::solver::equation>, true, unsigned int>&) ../src/math/grobner/pdd_simplifier.cpp:350
    #5 0x21292d0 in dd::simplifier::get_use_list() ../src/math/grobner/pdd_simplifier.cpp:375
    #6 0x21260c2 in dd::simplifier::simplify_linear_step(old_ptr_vector<dd::solver::equation>&) ../src/math/grobner/pdd_simplifier.cpp:112
    #7 0x2125e9c in dd::simplifier::simplify_linear_step(bool) ../src/math/grobner/pdd_simplifier.cpp:103
    #8 0x2125862 in dd::simplifier::operator()() ../src/math/grobner/pdd_simplifier.cpp:69
    #9 0x211ffda in dd::solver::simplify() ../src/math/grobner/pdd_solver.cpp:135
    #10 0x211f6af in dd::solver::saturate() ../src/math/grobner/pdd_solver.cpp:93
    #11 0x1e14c8b in nla::core::run_grobner() ../src/math/lp/nla_core.cpp:1403
    #12 0x1e136dd in nla::core::inner_check(bool) ../src/math/lp/nla_core.cpp:1288
    #13 0x1e13ed2 in nla::core::check(old_vector<nla::lemma, true, unsigned int>&) ../src/math/lp/nla_core.cpp:1341
    #14 0x1d4dbbd in nla::solver::check(old_vector<nla::lemma, true, unsigned int>&) ../src/math/lp/nla_solver.cpp:40
    #15 0xdc9029 in smt::theory_lra::imp::check_nra() (/home/heqing/dependence/z3/build/z3+0xdc9029)
    #16 0xdc1d03 in smt::theory_lra::imp::final_check_eh() ../src/smt/theory_lra.cpp:1753
    #17 0xda83e4 in smt::theory_lra::final_check_eh() ../src/smt/theory_lra.cpp:3976
    #18 0x11bac65 in smt::context::final_check() ../src/smt/smt_context.cpp:3904
    #19 0x11b9c6e in smt::context::bounded_search() ../src/smt/smt_context.cpp:3819
    #20 0x11b73a9 in smt::context::search() ../src/smt/smt_context.cpp:3646
    #21 0x11b4da4 in smt::context::setup_and_check(bool) ../src/smt/smt_context.cpp:3471
    #22 0x112257a in smt::kernel::imp::setup_and_check() ../src/smt/smt_kernel.cpp:108
    #23 0x1121255 in smt::kernel::setup_and_check() ../src/smt/smt_kernel.cpp:292
    #24 0xc496e6 in smt_tactic::operator()(ref<goal> const&, sref_buffer<goal, 16u>&) ../src/smt/tactic/smt_tactic.cpp:200
    #25 0x19d7aa3 in and_then_tactical::operator()(ref<goal> const&, sref_buffer<goal, 16u>&) ../src/tactic/tactical.cpp:120
    #26 0x19def27 in try_for_tactical::operator()(ref<goal> const&, sref_buffer<goal, 16u>&) ../src/tactic/tactical.cpp:933
    #27 0x19d8ea5 in or_else_tactical::operator()(ref<goal> const&, sref_buffer<goal, 16u>&) ../src/tactic/tactical.cpp:296
    #28 0x19d7aa3 in and_then_tactical::operator()(ref<goal> const&, sref_buffer<goal, 16u>&) ../src/tactic/tactical.cpp:120
    #29 0x19d7aa3 in and_then_tactical::operator()(ref<goal> const&, sref_buffer<goal, 16u>&) ../src/tactic/tactical.cpp:120

SUMMARY: AddressSanitizer: heap-use-after-free ../src/math/grobner/pdd_simplifier.cpp:131 dd::simplifier::simplify_linear_step(old_ptr_vector<dd::solver::equation>&)
Shadow bytes around the buggy address:
  0x0c0680002f00: 00 fa fa fa 00 00 00 fa fa fa 00 00 00 fa fa fa
  0x0c0680002f10: 00 00 00 fa fa fa 00 00 00 fa fa fa 00 00 00 fa
  0x0c0680002f20: fa fa 00 00 00 fa fa fa 00 00 00 fa fa fa 00 00
  0x0c0680002f30: 00 fa fa fa 00 00 00 fa fa fa 00 00 00 fa fa fa
  0x0c0680002f40: 00 00 00 fa fa fa 00 00 00 00 fa fa 00 00 00 00
=>0x0c0680002f50: fa fa fd fd fd[fd]fa fa 00 00 00 00 fa fa 00 00
  0x0c0680002f60: 00 00 fa fa 00 00 00 00 fa fa 00 00 00 00 fa fa
  0x0c0680002f70: 00 00 00 00 fa fa 00 00 00 00 fa fa 00 00 00 00
  0x0c0680002f80: fa fa fd fd fd fd fa fa fd fd fd fd fa fa fd fd
  0x0c0680002f90: fd fd fa fa fd fd fd fd fa fa fd fd fd fd fa fa
  0x0c0680002fa0: fd fd fd fd fa fa fd fd fd fd fa fa 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
==42916==ABORTING