heap-use-after-free at src/ast/ast.h:502

[rainoftime]

Hi, for the following formula,

(declare-sort Type)
(declare-fun subtype (Type Type) Bool)
(declare-fun root-type () Type)
(declare-fun l1 () Bool)
(assert (and (forall ((x Type)) (subtype x x)) (forall ((x Type) (y Type)) (or (= x y) (not (subtype x y)) (not (subtype y x)))) (forall ((x Type) (y Type) (z Type)) (or (subtype x z) (not (subtype x y)) (not (subtype y z))))))
(assert (= l1 (forall ((x Type)) (subtype x root-type))))
(check-sat-using (then aig special-relations))

z3 4f6fcf8

=================================================================
==186460==ERROR: AddressSanitizer: heap-use-after-free on address 0x607000025db4 at pc 0x0000005be097 bp 0x7ffd834a3670 sp 0x7ff
d834a3668
READ of size 4 at 0x607000025db4 thread T0
    #0 0x5be096 in ast::hash() const /home/z3-debug/build/../src/ast/ast.h:502:36
    #1 0x81c0cf in obj_map<expr, expr*>::key_data::hash() const /home/z3-debug/build/../src/util/obj_hashtabl
e.h:76:47
    #2 0x81bc94 in obj_map<expr, expr*>::obj_map_entry::get_hash() const /home/z3-debug/build/../src/util/obj
_hashtable.h:84:51
    #3 0x81f3ad in core_hashtable<obj_map<expr, expr*>::obj_map_entry, obj_hash<obj_map<expr, expr*>::key_data>, default_eq<obj_
map<expr, expr*>::key_data> >::find_core(obj_map<expr, expr*>::key_data const&) const /home/z3-debug/build/..
/src/util/hashtable.h:513:13
    #4 0x81f1bf in obj_map<expr, expr*>::find_core(expr*) const /home/z3-debug/build/../src/util/obj_hashtabl
e.h:155:24

[NikolajBjorner]

Given that I haven't set up ASAN properly in my environment, something that would help for these reports is a deeper stack trace.

[rainoftime]

The full trace is

=================================================================
==86343==ERROR: AddressSanitizer: heap-use-after-free on address 0x607000025db4 at pc 0x0000005be097 bp 0x7ffcba1b4310 sp 0x7ffcba1b4308
READ of size 4 at 0x607000025db4 thread T0
    #0 0x5be096 in ast::hash() const /home/z3/build/../src/ast/ast.h:502:36
    #1 0x81c0cf in obj_map<expr, expr*>::key_data::hash() const /home/z3/build/../src/util/obj_hashtable.h:76:47
    #2 0x81bc94 in obj_map<expr, expr*>::obj_map_entry::get_hash() const /home/z3/build/../src/util/obj_hashtable.h:84:51
    #3 0x81f3ad in core_hashtable<obj_map<expr, expr*>::obj_map_entry, obj_hash<obj_map<expr, expr*>::key_data>, default_eq<obj_map<expr, expr*>::key_data> >::find_core(obj_map<expr, expr*>
::key_data const&) const /home/z3/build/../src/util/hashtable.h:513:13
    #4 0x81f1bf in obj_map<expr, expr*>::find_core(expr*) const /home/z3/build/../src/util/obj_hashtable.h:155:24
    #5 0xfff0dc in obj_map<expr, expr*>::contains(expr*) const /home/z3/build/../src/util/obj_hashtable.h:191:16
    #6 0x340d2c2 in func_decl_replace::operator()(expr*) /home/z3/build/../src/ast/rewriter/func_decl_replace.cpp:29:21
    #7 0x2d079bf in special_relations_tactic::operator()(ref<goal> const&, sref_buffer<goal, 16u>&) /home/z3/build/../src/tactic/core/special_relations_tactic.cpp:1
67:34
    #8 0x31f443f in and_then_tactical::operator()(ref<goal> const&, sref_buffer<goal, 16u>&) /home/z3/build/../src/tactic/tactical.cpp:121:19
    #9 0x320629e in unary_tactical::operator()(ref<goal> const&, sref_buffer<goal, 16u>&) /home/z3/build/../src/tactic/tactical.cpp:840:14
    #10 0x31ea10c in exec(tactic&, ref<goal> const&, sref_buffer<goal, 16u>&) /home/z3/build/../src/tactic/tactic.cpp:152:9
    #11 0x31ea9b2 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_ma
nager>&, std::__cxx11::basic_string<char, std::char_traits<char>, std::allocator<char> >&) /home/z3/build/../src/tactic/tactic.cpp:172:9
    #12 0x305a248 in check_sat_using_tactic_cmd::execute(cmd_context&) /home/z3/build/../src/cmd_context/tactic_cmds.cpp:216:25
    #13 0x300844b in smt2::parser::parse_ext_cmd(int, int) /home/z3/build/../src/parsers/smt2/smt2parser.cpp:2910:33
    #14 0x2fffa6f in smt2::parser::parse_cmd() /home/z3/build/../src/parsers/smt2/smt2parser.cpp:3016:13
    #15 0x2ff9865 in smt2::parser::operator()() /home/z3/build/../src/parsers/smt2/smt2parser.cpp:3162:29
    #16 0x2ff7e9e in parse_smt2_commands(cmd_context&, std::istream&, bool, params_ref const&, char const*) /home/z3/build/../src/parsers/smt2/smt2parser.cpp:3211:1
2
    #17 0x55ec42 in read_smtlib2_commands(char const*) /home/z3/build/../src/shell/smtlib_frontend.cpp:142:18
    #18 0x59b12b in main /home/z3/build/../src/shell/main.cpp:371:28
    #19 0x7f88aa29a83f in __libc_start_main /build/glibc-S7Ft5T/glibc-2.23/csu/../csu/libc-start.c:291
    #20 0x4439f8 in _start (/home/z3/build/z3+0x4439f8)

0x607000025db4 is located 20 bytes inside of 76-byte region [0x607000025da0,0x607000025dec)
freed by thread T0 here:
    #0 0x4d6af8 in free /home/heqing/dependence/llvm-project/compiler-rt/lib/asan/asan_malloc_linux.cpp:123
    #1 0x47fa1b7 in memory::deallocate(void*) /home/z3/build/../src/util/memory_manager.cpp:265:5
    #2 0x484f43c in small_object_allocator::deallocate(unsigned long, void*) /home/z3/build/../src/util/small_object_allocator.cpp:77:5
    #3 0x41ce005 in ast_manager::deallocate_node(ast*, unsigned int) /home/z3/build/../src/ast/ast.h:1676:17
    #4 0x41a2f0f in ast_manager::delete_node(ast*) /home/z3/build/../src/ast/ast.cpp:1912:9
    #5 0x57985a in ast_manager::dec_ref(ast*) /home/z3/build/../src/ast/ast.h:1635:17
    #6 0x6654a7 in parray_manager<ast_manager::expr_array_config>::dec_ref(expr* const&) /home/z3/build/../src/util/parray.h:90:24
    #7 0x6656d6 in parray_manager<ast_manager::expr_array_config>::rset(expr**, unsigned int, expr* const&) /home/z3/build/../src/util/parray.h:163:9
    #8 0x31e681a in parray_manager<ast_manager::expr_array_config>::rset(parray_manager<ast_manager::expr_array_config>::cell*, unsigned int, expr* const&) /home/z3
/build/../src/util/parray.h:170:9
    #9 0x31e5e06 in parray_manager<ast_manager::expr_array_config>::set(parray_manager<ast_manager::expr_array_config>::ref&, unsigned int, expr* const&) /home/z3/b
uild/../src/util/parray.h:368:17
    #10 0x31e261b in ast_manager::set(parray_manager<ast_manager::expr_array_config>::ref&, unsigned int, expr*) /home/z3/build/../src/ast/ast.h:2019:75
    #11 0x31db2ad in goal::update(unsigned int, expr*, app*, dependency_manager<ast_manager::expr_dependency_config>::dependency*) /home/z3/build/../src/tactic/goal
.cpp:318:21
    #12 0x2d07a5d in special_relations_tactic::operator()(ref<goal> const&, sref_buffer<goal, 16u>&) /home/z3/build/../src/tactic/core/special_relations_tactic.cpp:
168:20
    #13 0x31f443f in and_then_tactical::operator()(ref<goal> const&, sref_buffer<goal, 16u>&) /home/z3/build/../src/tactic/tactical.cpp:121:19
    #14 0x320629e in unary_tactical::operator()(ref<goal> const&, sref_buffer<goal, 16u>&) /home/z3/build/../src/tactic/tactical.cpp:840:14
    #15 0x31ea10c in exec(tactic&, ref<goal> const&, sref_buffer<goal, 16u>&) /home/z3/build/../src/tactic/tactic.cpp:152:9
    #16 0x31f4203 in and_then_tactical::operator()(ref<goal> const&, sref_buffer<goal, 16u>&) /home/z3/build/../src/tactic/tactical.cpp:112:15
    #17 0x320629e in unary_tactical::operator()(ref<goal> const&, sref_buffer<goal, 16u>&) /home/z3/build/../src/tactic/tactical.cpp:840:14
    #18 0x31ea10c in exec(tactic&, ref<goal> const&, sref_buffer<goal, 16u>&) /home/z3/build/../src/tactic/tactic.cpp:152:9
    #19 0x31ea9b2 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_ma
nager>&, std::__cxx11::basic_string<char, std::char_traits<char>, std::allocator<char> >&) /home/z3/build/../src/tactic/tactic.cpp:172:9
    #20 0x305a248 in check_sat_using_tactic_cmd::execute(cmd_context&) /home/z3/build/../src/cmd_context/tactic_cmds.cpp:216:25
    #21 0x300844b in smt2::parser::parse_ext_cmd(int, int) /home/z3/build/../src/parsers/smt2/smt2parser.cpp:2910:33
    #22 0x2fffa6f in smt2::parser::parse_cmd() /home/z3/build/../src/parsers/smt2/smt2parser.cpp:3016:13
    #23 0x2ff9865 in smt2::parser::operator()() /home/z3/build/../src/parsers/smt2/smt2parser.cpp:3162:29
    #24 0x2ff7e9e in parse_smt2_commands(cmd_context&, std::istream&, bool, params_ref const&, char const*) /home/z3/build/../src/parsers/smt2/smt2parser.cpp:3211:1
2
    #25 0x55ec42 in read_smtlib2_commands(char const*) /home/z3/build/../src/shell/smtlib_frontend.cpp:142:18
    #26 0x59b12b in main /home/z3/build/../src/shell/main.cpp:371:28
    #27 0x7f88aa29a83f in __libc_start_main /build/glibc-S7Ft5T/glibc-2.23/csu/../csu/libc-start.c:291

SUMMARY: AddressSanitizer: heap-use-after-free /home/z3/build/../src/ast/ast.h:502:36 in ast::hash() const