search

Z3Prover / z3

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

heap-use-after-free at ast.h:505 (z3str3) #3756

Closed rainoftime closed 4 years ago

rainoftime commented 4 years ago

Hi, for the following formula

(set-option :smt.phase_selection 5)
(set-option :smt.random_seed 7)
(set-option :smt.string_solver z3str3)
(declare-const Str9 String)
(assert (>= (str.len Str9) 363))
(push 1)
(check-sat)
(check-sat)

asan detecs a uaf in z3 5516e420a138

==130354==ERROR: AddressSanitizer: heap-use-after-free on address 0x60600002cd94 at pc 0x000000467ce9 bp 0x7ffe82a5eed0 sp 0x7ffe82a5eec0
READ of size 4 at 0x60600002cd94 thread T0
    #0 0x467ce8 in ast::hash() const ../src/ast/ast.h:505
    #1 0x5d0863 in obj_hash_entry<expr>::get_hash() const ../src/util/obj_hashtable.h:37
    #2 0x5cf157 in core_hashtable<obj_hash_entry<expr>, obj_ptr_hash<expr>, ptr_eq<expr> >::find_core(expr* const&) const ../src/util/hashtable.h:507
    #3 0x5ce64c in core_hashtable<obj_hash_entry<expr>, obj_ptr_hash<expr>, ptr_eq<expr> >::contains(expr* const&) const ../src/util/hashtable.h:522
    #4 0x13ec490 in smt::theory_str::assign_eh(int, bool) ../src/smt/theory_str.cpp:7692
    #5 0xf86082 in smt::context::propagate_atoms() ../src/smt/smt_context.cpp:1332
    #6 0xf89c02 in smt::context::propagate() ../src/smt/smt_context.cpp:1672
    #7 0xfa0378 in smt::context::bounded_search() ../src/smt/smt_context.cpp:3715
    #8 0xf9e5a2 in smt::context::search() ../src/smt/smt_context.cpp:3599
    #9 0xf9cb1b in smt::context::check(unsigned int, expr* const*, bool) ../src/smt/smt_context.cpp:3482
    #10 0xd13f6e in smt::kernel::imp::check(unsigned int, expr* const*) ../src/smt/smt_kernel.cpp:116
    #11 0xd12b8f in smt::kernel::check(unsigned int, expr* const*) ../src/smt/smt_kernel.cpp:296
    #12 0x10b1688 in check_sat_core2 ../src/smt/smt_solver.cpp:190
    #13 0x197f5c1 in solver_na2as::check_sat_core(unsigned int, expr* const*) ../src/solver/solver_na2as.cpp:67
    #14 0x19860f4 in combined_solver::check_sat_core(unsigned int, expr* const*) ../src/solver/combined_solver.cpp:219
    #15 0x198362b in solver::check_sat(unsigned int, expr* const*) ../src/solver/solver.cpp:330
    #16 0x193c1be in cmd_context::check_sat(unsigned int, expr* const*) ../src/cmd_context/cmd_context.cpp:1581
    #17 0x18cc1ed in smt2::parser::parse_check_sat() ../src/parsers/smt2/smt2parser.cpp:2596
    #18 0x18d0189 in smt2::parser::parse_cmd() ../src/parsers/smt2/smt2parser.cpp:2938
    #19 0x18d189b in smt2::parser::operator()() ../src/parsers/smt2/smt2parser.cpp:3130
    #20 0x18b0880 in parse_smt2_commands(cmd_context&, std::istream&, bool, params_ref const&, char const*) ../src/parsers/smt2/smt2parser.cpp:3179
    #21 0x43c250 in read_smtlib2_commands(char const*) ../src/shell/smtlib_frontend.cpp:89
NikolajBjorner commented 4 years ago

@mtrberzi - see comments in the code regarding lifetime of expressions. A more systematic solution is to tie the lifetime of expressions with the scope. So you remove elements from the set on backtracking the scope where they were created.