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

(rewriter.flat=false) heap-use-after-free at ../src/util/old_vector.h:371 #3978

Closed
muchang opened this issue Apr 15, 2020 · 1 comment
Closed

(rewriter.flat=false) heap-use-after-free at ../src/util/old_vector.h:371 #3978

muchang opened this issue Apr 15, 2020 · 1 comment

Comments

@muchang
Copy link

muchang commented Apr 15, 2020

Hi,
For this formula, Z3 built with ASAN throws out a heap-use-after-free:

[609] % z3san small.smt2
=================================================================
==15079==ERROR: AddressSanitizer: heap-use-after-free on address 0x6270000d6b30 at pc 0x55d07ee282fe bp 0x7ffcac018070 sp 0x7ffcac018060
READ of size 8 at 0x6270000d6b30 thread T0
  #0 0x55d07ee282fd in old_vector<unsigned int, false, unsigned int>::operator[](unsigned int) ../src/util/old_vector.h:371
  #1 0x55d07ee282fd in nla::emonics::remove_cg_mon(nla::monic const&) ../src/math/lp/emonics.cpp:205
  #2 0x55d07ee35e90 in nla::emonics::remove_cg(unsigned int) ../src/math/lp/emonics.cpp:187
  #3 0x55d07ee35e90 in nla::emonics::rehash_cg(unsigned int) ../src/math/lp/emonics.h:110
  #4 0x55d07ee35e90 in nla::emonics::after_merge_eh(nla::signed_var, nla::signed_var, nla::signed_var, nla::signed_var) ../src/math/lp/emonics.cpp:442
  #5 0x55d07ecdb6ff in nla::var_eqs<nla::emonics>::after_merge_eh(unsigned int, unsigned int, unsigned int, unsigned int) ../src/math/lp/var_eqs.h:347
  #6 0x55d07ecdb6ff in union_find<nla::var_eqs<nla::emonics> >::merge(unsigned int, unsigned int) ../src/util/union_find.h:134
  #7 0x55d07ecdc0e6 in nla::var_eqs<nla::emonics>::merge(nla::signed_var, nla::signed_var, nla::eq_justification const&) ../src/math/lp/var_eqs.h:121
  #8 0x55d07ecc213c in nla::var_eqs<nla::emonics>::merge_minus(unsigned int, unsigned int, nla::eq_justification const&) ../src/math/lp/var_eqs.h:129
  #9 0x55d07ecc213c in nla::core::add_equivalence_maybe(lp::lar_term const*, unsigned int, unsigned int) ../src/math/lp/nla_core.cpp:880
  #10 0x55d07ecc2d2e in nla::core::collect_equivs() ../src/math/lp/nla_core.cpp:840
  #11 0x55d07ecc3717 in nla::core::check(old_vector<nla::lemma, true, unsigned int>&) ../src/math/lp/nla_core.cpp:1497
  #12 0x55d07cf0bb32 in smt::theory_lra::imp::check_nra() ../src/smt/theory_lra.cpp:2237
  #13 0x55d07cf0bb32 in smt::theory_lra::imp::final_check_eh() ../src/smt/theory_lra.cpp:1741
  #14 0x55d07cf0bb32 in smt::theory_lra::final_check_eh() ../src/smt/theory_lra.cpp:3977
  #15 0x55d07ca6f8f4 in smt::context::final_check() ../src/smt/smt_context.cpp:3851
  #16 0x55d07ca7fd16 in smt::context::bounded_search() ../src/smt/smt_context.cpp:3767
  #17 0x55d07ca80617 in smt::context::search() ../src/smt/smt_context.cpp:3594
  #18 0x55d07ca8330d in smt::context::setup_and_check(bool) ../src/smt/smt_context.cpp:3417
  #19 0x55d07c90491f in smt_tactic::operator()(ref<goal> const&, sref_buffer<goal, 16u>&) ../src/smt/tactic/smt_tactic.cpp:201
  #20 0x55d07e36a057 in and_then_tactical::operator()(ref<goal> const&, sref_buffer<goal, 16u>&) ../src/tactic/tactical.cpp:120
  #21 0x55d07e35c9b1 in cond_tactical::operator()(ref<goal> const&, sref_buffer<goal, 16u>&) ../src/tactic/tactical.cpp:1034
  #22 0x55d07e35c9b1 in cond_tactical::operator()(ref<goal> const&, sref_buffer<goal, 16u>&) ../src/tactic/tactical.cpp:1034
  #23 0x55d07e35c9b1 in cond_tactical::operator()(ref<goal> const&, sref_buffer<goal, 16u>&) ../src/tactic/tactical.cpp:1034
  #24 0x55d07e35c9b1 in cond_tactical::operator()(ref<goal> const&, sref_buffer<goal, 16u>&) ../src/tactic/tactical.cpp:1034
  #25 0x55d07e35c9b1 in cond_tactical::operator()(ref<goal> const&, sref_buffer<goal, 16u>&) ../src/tactic/tactical.cpp:1034
  #26 0x55d07e35c9b1 in cond_tactical::operator()(ref<goal> const&, sref_buffer<goal, 16u>&) ../src/tactic/tactical.cpp:1034
  #27 0x55d07e35c9b1 in cond_tactical::operator()(ref<goal> const&, sref_buffer<goal, 16u>&) ../src/tactic/tactical.cpp:1034
  #28 0x55d07e35c9b1 in cond_tactical::operator()(ref<goal> const&, sref_buffer<goal, 16u>&) ../src/tactic/tactical.cpp:1034
  #29 0x55d07e35c9b1 in cond_tactical::operator()(ref<goal> const&, sref_buffer<goal, 16u>&) ../src/tactic/tactical.cpp:1034
  #30 0x55d07e35c9b1 in cond_tactical::operator()(ref<goal> const&, sref_buffer<goal, 16u>&) ../src/tactic/tactical.cpp:1034
  #31 0x55d07e35c9b1 in cond_tactical::operator()(ref<goal> const&, sref_buffer<goal, 16u>&) ../src/tactic/tactical.cpp:1034
  #32 0x55d07e35c9b1 in cond_tactical::operator()(ref<goal> const&, sref_buffer<goal, 16u>&) ../src/tactic/tactical.cpp:1034
  #33 0x55d07e36a057 in and_then_tactical::operator()(ref<goal> const&, sref_buffer<goal, 16u>&) ../src/tactic/tactical.cpp:120
  #34 0x55d07e2cba4a in exec(tactic&, ref<goal> const&, sref_buffer<goal, 16u>&) ../src/tactic/tactic.cpp:148
  #35 0x55d07e2cdd4d 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 0x55d07e1cc6a8 in check_sat_core2 ../src/solver/tactic2solver.cpp:185
  #37 0x55d07e1d3a67 in solver_na2as::check_sat_core(unsigned int, expr* const*) ../src/solver/solver_na2as.cpp:67
  #38 0x55d07e191474 in combined_solver::check_sat_core(unsigned int, expr* const*) ../src/solver/combined_solver.cpp:246
  #39 0x55d07e172561 in solver::check_sat(unsigned int, expr* const*) ../src/solver/solver.cpp:330
  #40 0x55d07e0cd3b0 in cmd_context::check_sat(unsigned int, expr* const*) ../src/cmd_context/cmd_context.cpp:1551
  #41 0x55d07e014023 in smt2::parser::parse_check_sat() ../src/parsers/smt2/smt2parser.cpp:2596
  #42 0x55d07e014023 in smt2::parser::parse_cmd() ../src/parsers/smt2/smt2parser.cpp:2938
  #43 0x55d07e014023 in smt2::parser::operator()() ../src/parsers/smt2/smt2parser.cpp:3130
  #44 0x55d07dfcb545 in parse_smt2_commands(cmd_context&, std::istream&, bool, params_ref const&, char const*) ../src/parsers/smt2/smt2parser.cpp:3179
  #45 0x55d07b68a946 in read_smtlib2_commands(char const*) ../src/shell/smtlib_frontend.cpp:89
  #46 0x55d07b66341e in main ../src/shell/main.cpp:352
  #47 0x7f757421eb96 in __libc_start_main (/lib/x86_64-linux-gnu/libc.so.6+0x21b96)
  #48 0x55d07b676fb9 in _start (/home/suz/software/z3san/build-04142020192323-164a73f/z3+0x1f6fb9)
...
SUMMARY: AddressSanitizer: heap-use-after-free ../src/util/old_vector.h:371 in old_vector<unsigned int, false, unsigned int>::operator[](unsigned int)
...
==15079==ABORTING
[610] % 
[610] % 
[610] % cat small.smt2
(set-option :rewriter.flat false)
(declare-fun a () Real)
(declare-fun b () Real)
(declare-fun c () Real)
(declare-fun d () Real)
(declare-fun aa () Real)
(declare-fun e () Real)
(declare-fun f () Real)
(declare-fun ab () Real)
(declare-fun ac () Real)
(declare-fun ad () 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)
(declare-fun v () Real)
(declare-fun ep () Real)
(declare-fun p () Real)
(declare-fun ae () Real)
(declare-fun q () Real)
(declare-fun r () Real)
(assert (forall ((af Real)) (=> (and (or (or (or (and (and (or (and
 (and (and (and (and (= o 0.0 (- aa)) (= (+ aa q) 2.0) ) (= (- e) 2.0)
 ) (>= 0 ac)) (= (/ 14 f ae) 2.0)) (<= o 0)) (< 0.0 (/ 14 b q))) (>
 0.0 a)) (< (* n) v(/ 5 d j))) (<= (* c (- 5 d)) v)) (<= 0.0 h)) (<
 0.0 v)) (>= 0.0 ep)) (or (= 0 ad) (<= 0.0 g) (<= af g) (or (or (or
 (<= 0.0 (/ 8 ab p)) (< p v)) (< 0.0 (/ (* h af) j))) (> (+ (+ h af)
 j) v)) (<= (- af) ep)) (= m 2.0))))
(assert (distinct c (* i ae)))
(assert (= aa (/ 78 k q)))
(assert (= e (* l q)))
(assert (= ab (/ v r)))
(check-sat)
[611] %

OS: Ubuntu 18.04
Commit: 164a73f
@zhendongsu
Copy link

A much simpler repro that doesn't need the rewriter.flat=false option:

[579] % z3san small.smt2
=================================================================
==17534==ERROR: AddressSanitizer: heap-use-after-free on address 0x62700005a6c0 at pc 0x55ed8363904e bp 0x7ffe514f7cc0 sp 0x7ffe514f7cb0
READ of size 8 at 0x62700005a6c0 thread T0
    #0 0x55ed8363904d in vector<unsigned int, false, unsigned int>::operator[](unsigned int) ../src/util/vector.h:371
    #1 0x55ed8363904d in nla::emonics::remove_cg_mon(nla::monic const&) ../src/math/lp/emonics.cpp:205
    #2 0x55ed83646be0 in nla::emonics::remove_cg(unsigned int) ../src/math/lp/emonics.cpp:187
    #3 0x55ed83646be0 in nla::emonics::rehash_cg(unsigned int) ../src/math/lp/emonics.h:110
    #4 0x55ed83646be0 in nla::emonics::after_merge_eh(nla::signed_var, nla::signed_var, nla::signed_var, nla::signed_var) ../src/math/lp/emonics.cpp:442
    #5 0x55ed834ee9cf in nla::var_eqs<nla::emonics>::after_merge_eh(unsigned int, unsigned int, unsigned int, unsigned int) ../src/math/lp/var_eqs.h:347
    #6 0x55ed834ee9cf in union_find<nla::var_eqs<nla::emonics> >::merge(unsigned int, unsigned int) ../src/util/union_find.h:134
    #7 0x55ed834ef3b6 in nla::var_eqs<nla::emonics>::merge(nla::signed_var, nla::signed_var, nla::eq_justification const&) ../src/math/lp/var_eqs.h:121
    #8 0x55ed834d6b31 in nla::var_eqs<nla::emonics>::merge_plus(unsigned int, unsigned int, nla::eq_justification const&) ../src/math/lp/var_eqs.h:128
    #9 0x55ed834d6b31 in nla::core::add_equivalence_maybe(lp::lar_term const*, unsigned int, unsigned int) ../src/math/lp/nla_core.cpp:882
    #10 0x55ed834d74b7 in nla::core::collect_equivs() ../src/math/lp/nla_core.cpp:840
    #11 0x55ed834d8177 in nla::core::check(vector<nla::lemma, true, unsigned int>&) ../src/math/lp/nla_core.cpp:1497
    #12 0x55ed81703652 in smt::theory_lra::imp::check_nra() ../src/smt/theory_lra.cpp:2238
    #13 0x55ed81703652 in smt::theory_lra::imp::final_check_eh() ../src/smt/theory_lra.cpp:1742
    #14 0x55ed81703652 in smt::theory_lra::final_check_eh() ../src/smt/theory_lra.cpp:3976
    #15 0x55ed81266614 in smt::context::final_check() ../src/smt/smt_context.cpp:3857
    #16 0x55ed81276b96 in smt::context::bounded_search() ../src/smt/smt_context.cpp:3773
    #17 0x55ed81277497 in smt::context::search() ../src/smt/smt_context.cpp:3600
    #18 0x55ed8127a19d in smt::context::setup_and_check(bool) ../src/smt/smt_context.cpp:3423
    #19 0x55ed810fb78f in smt_tactic::operator()(ref<goal> const&, sref_buffer<goal, 16u>&) ../src/smt/tactic/smt_tactic.cpp:201
    #20 0x55ed82b81257 in and_then_tactical::operator()(ref<goal> const&, sref_buffer<goal, 16u>&) ../src/tactic/tactical.cpp:120
    #21 0x55ed82b73bb1 in cond_tactical::operator()(ref<goal> const&, sref_buffer<goal, 16u>&) ../src/tactic/tactical.cpp:1034
    #22 0x55ed82b73bb1 in cond_tactical::operator()(ref<goal> const&, sref_buffer<goal, 16u>&) ../src/tactic/tactical.cpp:1034
    #23 0x55ed82b73bb1 in cond_tactical::operator()(ref<goal> const&, sref_buffer<goal, 16u>&) ../src/tactic/tactical.cpp:1034
    #24 0x55ed82b73bb1 in cond_tactical::operator()(ref<goal> const&, sref_buffer<goal, 16u>&) ../src/tactic/tactical.cpp:1034
    #25 0x55ed82b73bb1 in cond_tactical::operator()(ref<goal> const&, sref_buffer<goal, 16u>&) ../src/tactic/tactical.cpp:1034
    #26 0x55ed82b73bb1 in cond_tactical::operator()(ref<goal> const&, sref_buffer<goal, 16u>&) ../src/tactic/tactical.cpp:1034
    #27 0x55ed82b73bb1 in cond_tactical::operator()(ref<goal> const&, sref_buffer<goal, 16u>&) ../src/tactic/tactical.cpp:1034
    #28 0x55ed82b73bb1 in cond_tactical::operator()(ref<goal> const&, sref_buffer<goal, 16u>&) ../src/tactic/tactical.cpp:1034
    #29 0x55ed82b73bb1 in cond_tactical::operator()(ref<goal> const&, sref_buffer<goal, 16u>&) ../src/tactic/tactical.cpp:1034
    #30 0x55ed82b73bb1 in cond_tactical::operator()(ref<goal> const&, sref_buffer<goal, 16u>&) ../src/tactic/tactical.cpp:1034
    #31 0x55ed82b73bb1 in cond_tactical::operator()(ref<goal> const&, sref_buffer<goal, 16u>&) ../src/tactic/tactical.cpp:1034
    #32 0x55ed82b73bb1 in cond_tactical::operator()(ref<goal> const&, sref_buffer<goal, 16u>&) ../src/tactic/tactical.cpp:1034
    #33 0x55ed82b81257 in and_then_tactical::operator()(ref<goal> const&, sref_buffer<goal, 16u>&) ../src/tactic/tactical.cpp:120
    #34 0x55ed82ae2c4a in exec(tactic&, ref<goal> const&, sref_buffer<goal, 16u>&) ../src/tactic/tactic.cpp:148
    #35 0x55ed82ae4f4d 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 0x55ed829e38a8 in check_sat_core2 ../src/solver/tactic2solver.cpp:185
    #37 0x55ed829eac67 in solver_na2as::check_sat_core(unsigned int, expr* const*) ../src/solver/solver_na2as.cpp:67
    #38 0x55ed829a8674 in combined_solver::check_sat_core(unsigned int, expr* const*) ../src/solver/combined_solver.cpp:246
    #39 0x55ed82989761 in solver::check_sat(unsigned int, expr* const*) ../src/solver/solver.cpp:330
    #40 0x55ed828e4820 in cmd_context::check_sat(unsigned int, expr* const*) ../src/cmd_context/cmd_context.cpp:1551
    #41 0x55ed8282b503 in smt2::parser::parse_check_sat() ../src/parsers/smt2/smt2parser.cpp:2596
    #42 0x55ed8282b503 in smt2::parser::parse_cmd() ../src/parsers/smt2/smt2parser.cpp:2938
    #43 0x55ed8282b503 in smt2::parser::operator()() ../src/parsers/smt2/smt2parser.cpp:3130
    #44 0x55ed827e2a25 in parse_smt2_commands(cmd_context&, std::istream&, bool, params_ref const&, char const*) ../src/parsers/smt2/smt2parser.cpp:3179
    #45 0x55ed7fe81466 in read_smtlib2_commands(char const*) ../src/shell/smtlib_frontend.cpp:89
    #46 0x55ed7fe59e3e in main ../src/shell/main.cpp:352
    #47 0x7f6318319b96 in __libc_start_main (/lib/x86_64-linux-gnu/libc.so.6+0x21b96)
    #48 0x55ed7fe6dad9 in _start (/home/suz/software/z3san/build-04172020182140-3e9479d/z3+0x1f7ad9)
...
==17534==ABORTING
[580] % 
[580] % cat small.smt2
(declare-fun a () Real)
(declare-fun b () Real)
(declare-fun c () Real)
(assert (forall ((d Real)) (distinct (> (+ b d) 0) (= (- a (* (/ 2 a (- c d)) d)) 1))))
(check-sat)
[581] %

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
3 participants
@NikolajBjorner @muchang @zhendongsu