zhendongsu
commented
1 year ago [546] % z3release model_validate=true small.smt2
(error "line 9 column 46: invalid extract application")
Segmentation fault
[547] % z3san small.smt2
(error "line 9 column 46: invalid extract application")
=================================================================
==10339==ERROR: AddressSanitizer: heap-use-after-free on address 0x603000000013 at pc 0x55eeb5f3322c bp 0x7ffc2d30e5e0 sp 0x7ffc2d30e5d0
READ of size 2 at 0x603000000013 thread T0
#0 0x55eeb5f3322b in func_decl_info::is_right_associative() const ../src/ast/ast.h:407
#1 0x55eeb5f3322b in func_decl::is_right_associative() const ../src/ast/ast.h:647
#2 0x55eeb5f3322b in ast_manager::mk_app(func_decl*, unsigned int, expr* const*) ../src/ast/ast.cpp:2244
#3 0x55eeb514d3de in ast_manager::mk_app(func_decl*, expr*) ../src/ast/ast.h:1872
#4 0x55eeb514d3de in mk_extract_proc::operator()(unsigned int, unsigned int, expr*) ../src/ast/rewriter/mk_extract_proc.cpp:45
#5 0x55eeb503f440 in bv_rewriter::mk_sign_extend(unsigned int, expr*, obj_ref<expr, ast_manager>&) ../src/ast/rewriter/bv_rewriter.cpp:1612
#6 0x55eeb4fb6ea3 in reduce_app_core ../src/ast/rewriter/th_rewriter.cpp:235
#7 0x55eeb4fb6ea3 in reduce_app ../src/ast/rewriter/th_rewriter.cpp:648
#8 0x55eeb4fc925c in process_app<false> ../src/ast/rewriter/rewriter_def.h:316
#9 0x55eeb4fc925c in resume_core<false> ../src/ast/rewriter/rewriter_def.h:787
#10 0x55eeb4fc925c in main_loop<false> ../src/ast/rewriter/rewriter_def.h:746
#11 0x55eeb4fc925c in operator() ../src/ast/rewriter/rewriter_def.h:826
#12 0x55eeb3de113b in asserted_formulas::assert_expr(expr*, app*) ../src/solver/assertions/asserted_formulas.cpp:167
#13 0x55eeb3251a57 in smt::context::assert_expr_core(expr*, app*) ../src/smt/smt_context.cpp:3024
#14 0x55eeb3251a57 in smt::context::assert_expr(expr*, app*) ../src/smt/smt_context.cpp:3036
#15 0x55eeb3251a57 in smt::context::assert_expr(expr*) ../src/smt/smt_context.cpp:3031
#16 0x55eeb47289d3 in solver::assert_expr(expr*) ../src/solver/solver.cpp:205
#17 0x55eeb47289d3 in solver::assert_expr(expr*) ../src/solver/solver.cpp:205
#18 0x55eeb4688f94 in cmd_context::assert_expr(expr*) ../src/cmd_context/cmd_context.cpp:1474
#19 0x55eeb45ea131 in smt2::parser::parse_assert() ../src/parsers/smt2/smt2parser.cpp:2586
#20 0x55eeb45f50f7 in smt2::parser::parse_cmd() ../src/parsers/smt2/smt2parser.cpp:2941
#21 0x55eeb45f50f7 in smt2::parser::operator()() ../src/parsers/smt2/smt2parser.cpp:3166
#22 0x55eeb45aa1c5 in parse_smt2_commands(cmd_context&, std::istream&, bool, params_ref const&, char const*) ../src/parsers/smt2/smt2parser.cpp:3217
#23 0x55eeb16bec01 in read_smtlib2_commands(char const*) ../src/shell/smtlib_frontend.cpp:144
#24 0x55eeb1692861 in main ../src/shell/main.cpp:381
#25 0x7f788c86bc86 in __libc_start_main (/lib/x86_64-linux-gnu/libc.so.6+0x21c86)
#26 0x55eeb169f8d9 in _start (/local/suz-local/software/z3san/build-12042022095531-9b58135/z3+0x20a8d9)
0x603000000013 is located 3 bytes inside of 24-byte region [0x603000000010,0x603000000028)
freed by thread T0 here:
#0 0x7f788d877f30 in realloc (/usr/lib/x86_64-linux-gnu/libasan.so.4+0xdef30)
#1 0x55eeb64ecc41 in memory::reallocate(void*, unsigned long) ../src/util/memory_manager.cpp:334
#2 0x55eeb64afe41 in vector<unsigned long, false, unsigned int>::expand_vector() ../src/util/vector.h:202
#3 0x55eeb64afe41 in vector<unsigned long, false, unsigned int>::push_back(unsigned long const&) ../src/util/vector.h:523
#4 0x55eeb64afe41 in prime_generator::process_next_k_numbers(unsigned long) ../src/util/prime_generator.cpp:63
#5 0x55eeb64b1218 in prime_generator::initialize() ../src/util/prime_generator.cpp:80
#6 0x55eeb64b1218 in prime_iterator::initialize() ../src/util/prime_generator.cpp:133
#7 0x55eeb1723c58 in mem_initialize() ../src/shell/mem_initializer.cpp:11
#8 0x55eeb64ebd21 in memory::initialize(unsigned long) ../src/util/memory_manager.cpp:117
#9 0x55eeb1692091 in main ../src/shell/main.cpp:334
#10 0x7f788c86bc86 in __libc_start_main (/lib/x86_64-linux-gnu/libc.so.6+0x21c86)
previously allocated by thread T0 here:
#0 0x7f788d877b40 in __interceptor_malloc (/usr/lib/x86_64-linux-gnu/libasan.so.4+0xdeb40)
#1 0x55eeb64ecb7d in memory::allocate(unsigned long) ../src/util/memory_manager.cpp:301
#2 0x55eeb64b13d1 in vector<unsigned long, false, unsigned int>::expand_vector() ../src/util/vector.h:183
#3 0x55eeb64b13d1 in vector<unsigned long, false, unsigned int>::push_back(unsigned long&&) ../src/util/vector.h:539
#4 0x55eeb64b13d1 in prime_generator::initialize() ../src/util/prime_generator.cpp:78
#5 0x55eeb64b13d1 in prime_iterator::initialize() ../src/util/prime_generator.cpp:133
#6 0x55eeb1723c58 in mem_initialize() ../src/shell/mem_initializer.cpp:11
#7 0x55eeb64ebd21 in memory::initialize(unsigned long) ../src/util/memory_manager.cpp:117
#8 0x55eeb1692091 in main ../src/shell/main.cpp:334
#9 0x7f788c86bc86 in __libc_start_main (/lib/x86_64-linux-gnu/libc.so.6+0x21c86)
SUMMARY: AddressSanitizer: heap-use-after-free ../src/ast/ast.h:407 in func_decl_info::is_right_associative() const
Shadow bytes around the buggy address:
0x0c067fff7fb0: 00 00 00 00 00 00 00 00 00 00 00 00 00 00 00 00
0x0c067fff7fc0: 00 00 00 00 00 00 00 00 00 00 00 00 00 00 00 00
0x0c067fff7fd0: 00 00 00 00 00 00 00 00 00 00 00 00 00 00 00 00
0x0c067fff7fe0: 00 00 00 00 00 00 00 00 00 00 00 00 00 00 00 00
0x0c067fff7ff0: 00 00 00 00 00 00 00 00 00 00 00 00 00 00 00 00
=>0x0c067fff8000: fa fa[fd]fd fd fa fa fa fd fd fd fa fa fa fd fd
0x0c067fff8010: fd fd fa fa fd fd fd fd fa fa 00 00 00 00 fa fa
0x0c067fff8020: 00 00 00 00 fa fa 00 00 00 00 fa fa 00 00 00 fa
0x0c067fff8030: fa fa 00 00 00 fa fa fa 00 00 00 fa fa fa 00 00
0x0c067fff8040: 00 fa fa fa 00 00 00 fa fa fa 00 00 00 fa fa fa
0x0c067fff8050: 00 00 00 fa fa fa 00 00 00 fa fa fa 00 00 00 fa
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
Freed heap region: fd
Stack left redzone: f1
Stack mid redzone: f2
Stack right redzone: f3
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
Left alloca redzone: ca
Right alloca redzone: cb
==10339==ABORTING
[548] %
[548] % cat small.smt2
(declare-fun a () (Array (_ BitVec 32) (_ BitVec 8)))
(assert (let ((qb (concat (select a (_ bv2 32)) (concat (select a (_
bv1 32)) (select a (_ bv0 32)))))) (let ((qc (concat (select a (_
bv5 32)) (concat (select a (_ bv4 32)) (concat (select a (_ bv3 32))
qb))))) (let ((qd ((_ to_fp 11 53) (concat (select a (_ bv7 32))
(concat (select a (_ bv6 32)) qc))))) (let ((qg ((_ sign_extend 2)
((_ fp.to_sbv 32) roundTowardZero (fp.abs qd)))) (qe ((_ extract 31
0) (concat (_ bv0 32))))) (let ((qf (bvudiv ((_ extract 31 0) qg) (_
bv10 32)))) (= (_ bv0 32) (bvor qf qe))))))))
(assert (let ((qb (concat (select a (_ bv2 32)) (concat (select a (_
bv1 32)) (select a (_ bv0 32)))))) (let ((qc (concat (select a (_
bv5 32)) (concat (select a (_ bv4 32)) (concat (select a (_ bv3 32))
qb))))) (let ((qd ((_ to_fp 11 53) (concat (select a (_ bv7 32))
(concat (select a (_ bv6 32)) qc))))) (let ((qg ((_ sign_extend 32)
((_ fp.to_sbv 32) roundTowardZero (fp.neg qd))))) (let ((qe ((_
extract 1 0) (concat ((_ extract 63 32) qg))))) (distinct qe)))))))
(check-sat)
Spurious error, solution unsoundness, or invalid model: