search

Z3Prover / z3

The Z3 Theorem Prover
Other
10.17k stars 1.47k forks source link

heap-use-after-free for CHC(BV) formula at ast.h:505 (proof, parallel, fp.xform.fix_unbound_vars) #3908

Closed rainoftime closed 4 years ago

rainoftime commented 4 years ago

Hi, for the following instance,

(set-logic HORN)
(set-option :proof true)
(set-option :parallel.enable true)
(set-option :smt.threads 6)
(set-option :fp.xform.fix_unbound_vars true)
(assert (forall ((q0 (_ BitVec 9)) (q1 (_ BitVec 9)) (q2 (_ BitVec 9)) (q3 (_ BitVec 9)) (q4 (_ BitVec 8))) (=> (bvuge q1 q1) (distinct (bvashr q4 q4) q4))))
(assert (forall ((q5 (_ BitVec 9)) (q6 (_ BitVec 9)) (q7 Bool)) (=> (= q5 (bvsdiv q6 q5)) (or q7 q7 q7 q7 q7 q7 q7 q7))))
(assert (forall ((q8 (_ BitVec 9)) (q9 (_ BitVec 9)) (q10 (_ BitVec 8))) (=> (= q10 q10) (= q9 (bvashr q8 (bvxor q9 q9 q9 q9))))))
(assert (forall ((q11 (_ BitVec 9)) (q12 (_ BitVec 9)) (q13 (_ BitVec 8))) (=> (= q13 q13) (bvsle (bvor q12 q11) (bvsdiv q12 q12)))))
(assert (forall ((q14 (_ BitVec 9)) (q15 (_ BitVec 9)) (q16 (_ BitVec 12))) (=> (bvuge (bvor q16 q16) (bvand (bvnot q16) (bvnot q16))) (bvsgt q15 q14))))
(assert (forall ((q17 (_ BitVec 9)) (q18 (_ BitVec 9)) (q19 (_ BitVec 9)) (q20 (_ BitVec 9)) (q21 Bool)) (=> (xor q21 q21 q21 q21 q21 q21 q21 q21) (distinct (bvnand q17 q18) (bvnand q17 q18)))))
(assert (forall ((q22 (_ BitVec 9)) (q23 (_ BitVec 9)) (q24 (_ BitVec 9)) (q25 (_ BitVec 12))) (=> (distinct (bvudiv q25 q25) (bvudiv q25 q25)) (bvslt q22 q22))))
(assert (forall ((q26 (_ BitVec 9)) (q27 Bool)) (=> (= q26 q26) (xor q27 q27 q27 q27 q27))))
(assert (forall ((q28 (_ BitVec 9)) (q29 (_ BitVec 9)) (q30 (_ BitVec 9)) (q31 (_ BitVec 10))) (=> (= q30 q30) (bvsgt q31 (bvsmod q31 q31)))))
(assert (forall ((q39 (_ BitVec 9)) (q40 (_ BitVec 9)) (q41 (_ BitVec 9)) (q42 (_ BitVec 9)) (q43 (_ BitVec 8))) (=> (distinct q39 (bvadd q39 q42)) (= (bvnot (bvurem ((_ extract 7 0) q43) q43)) q43))))
(check-sat)

z3 (commit ae5a713e815eb884) throws a uaf 

==124758==ERROR: AddressSanitizer: heap-use-after-free on address 0x60700063dbc4 at pc 0x000000467d09 bp 0x7ffe697ab370 sp 0x7ffe697ab360                                                         [116/1938]
READ of size 4 at 0x60700063dbc4 thread T0
    #0 0x467d08 in ast::hash() const ../src/ast/ast.h:505
    #1 0x5a4341 in obj_map<func_decl, unsigned int>::key_data::hash() const ../src/util/obj_hashtable.h:78
    #2 0x5a24a1 in obj_map<func_decl, unsigned int>::obj_map_entry::get_hash() const ../src/util/obj_hashtable.h:87
    #3 0x59fec3 in core_hashtable<obj_map<func_decl, unsigned int>::obj_map_entry, obj_hash<obj_map<func_decl, unsigned int>::key_data>, default_eq<obj_map<func_decl, unsigned int>::key_data> >::find_core
(obj_map<func_decl, unsigned int>::key_data const&) const ../src/util/hashtable.h:504
    #4 0x5991d2 in obj_map<func_decl, unsigned int>::find_core(func_decl*) const ../src/util/obj_hashtable.h:158
    #5 0x5939cc in obj_map<func_decl, unsigned int>::find(func_decl*, unsigned int&) const ../src/util/obj_hashtable.h:162
    #6 0x1a7e197 in model::top_sort::occur_count(func_decl*) const ../src/model/model.cpp:209
    #7 0x1a7a7e6 in model::compress() ../src/model/model.cpp:241
    #8 0x750dcf in spacer::ground_sat_answer_op::mk_children(spacer::ground_sat_answer_op::frame&, old_vector<spacer::ground_sat_answer_op::frame, true, unsigned int>&) ../src/muz/spacer/spacer_sat_answer
.cpp:143
    #9 0x7502bb in spacer::ground_sat_answer_op::operator()(spacer::pred_transformer&) ../src/muz/spacer/spacer_sat_answer.cpp:95
    #10 0x6d9710 in spacer::context::get_ground_refutation() const ../src/muz/spacer/spacer_context.cpp:2906
    #11 0x6b2a7d in spacer::context::get_proof() const (/home/peisen/test/tofuzz/z3-debug/build/z3+0x6b2a7d)
    #12 0x6b24ed in spacer::dl_interface::get_proof() ../src/muz/spacer/spacer_dl_interface.cpp:347
    #13 0xa5bf0b in datalog::context::get_proof() ../src/muz/base/dl_context.cpp:920
    #14 0x637c05 in horn_tactic::imp::verify(expr*, ref<goal> const&, sref_buffer<goal, 16u>&, ref<model_converter>&, ref<proof_converter>&) ../src/muz/fp/horn_tactic.cpp:274
    #15 0x637683 in horn_tactic::imp::operator()(ref<goal> const&, sref_buffer<goal, 16u>&) ../src/muz/fp/horn_tactic.cpp:241
    #16 0x63927b in horn_tactic::operator()(ref<goal> const&, sref_buffer<goal, 16u>&) ../src/muz/fp/horn_tactic.cpp:405
    #17 0x1a43f85 in cleanup_tactical::operator()(ref<goal> const&, sref_buffer<goal, 16u>&) ../src/tactic/tactical.cpp:915
    #18 0x1a372de in exec(tactic&, ref<goal> const&, sref_buffer<goal, 16u>&) ../src/tactic/tactic.cpp:148
    #19 0x1a37779 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
    #20 0x19bd812 in check_sat_core2 ../src/solver/tactic2solver.cpp:185
    #21 0x19c29af in solver_na2as::check_sat_core(unsigned int, expr* const*) ../src/solver/solver_na2as.cpp:67
    #22 0x19c98ab in combined_solver::check_sat_core(unsigned int, expr* const*) ../src/solver/combined_solver.cpp:246
    #23 0x19c6a19 in solver::check_sat(unsigned int, expr* const*) ../src/solver/solver.cpp:330
    #24 0x197f374 in cmd_context::check_sat(unsigned int, expr* const*) ../src/cmd_context/cmd_context.cpp:1581
    #25 0x190f3a3 in smt2::parser::parse_check_sat() ../src/parsers/smt2/smt2parser.cpp:2596
    #26 0x191333f in smt2::parser::parse_cmd() ../src/parsers/smt2/smt2parser.cpp:2938
    #27 0x1914a51 in smt2::parser::operator()() ../src/parsers/smt2/smt2parser.cpp:3130
    #28 0x18f3a36 in parse_smt2_commands(cmd_context&, std::istream&, bool, params_ref const&, char const*) ../src/parsers/smt2/smt2parser.cpp:3179
    #29 0x43c270 in read_smtlib2_commands(char const*) ../src/shell/smtlib_frontend.cpp:89
    #30 0x454104 in main ../src/shell/main.cpp:352
    #31 0x7f511646282f in __libc_start_main (/lib/x86_64-linux-gnu/libc.so.6+0x2082f)
agurfinkel commented 4 years ago

@NikolajBjorner please review my fix: 2b27aa1