Z3Prover / z3

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

Heap-use-after-free about sat.ddfw.threads #7375

Closed Heaven2024 closed 2 months ago

Heaven2024 commented 2 months ago
(set-option :sat.ddfw.threads 1)
(set-logic QF_BV)
(declare-fun x () (_ BitVec 32))
(declare-fun y () (_ BitVec 32))
(assert (bvult (bvmul x y) (bvadd x y)))
(check-sat)

z3 test.smt2
=================================================================
==2887688==ERROR: AddressSanitizer: heap-use-after-free on address 0x61900001feb0 at pc 0x564c05ec0ed8 bp 0x7ffe37280080 sp 0x7ffe37280078
READ of size 8 at 0x61900001feb0 thread T0
    #0 0x564c05ec0ed7 in reslimit::pop_child() /yuhao/z3/build/../src/util/rlimit.cpp:90:35
    #1 0x564c050139cb in scoped_limits::reset() /yuhao/z3/build/../src/util/rlimit.h:97:64
    #2 0x564c050139cb in scoped_limits::~scoped_limits() /yuhao/z3/build/../src/util/rlimit.h:96:24
    #3 0x564c050139cb in sat::parallel::~parallel() /yuhao/z3/build/../src/sat/sat_parallel.cpp:93:5
    #4 0x564c04f6ac5a in sat::solver::check_par(unsigned int, sat::literal const*) /yuhao/z3/build/../src/sat/sat_solver.cpp:1607:5
    #5 0x564c01e444b4 in sat_tactic::imp::operator()(ref<goal> const&, sref_buffer<goal, 16u>&) /yuhao/z3/build/../src/sat/tactic/sat_tactic.cpp:73:33
    #6 0x564c01e4230b in sat_tactic::operator()(ref<goal> const&, sref_buffer<goal, 16u>&) /yuhao/z3/build/../src/sat/tactic/sat_tactic.cpp:221:13
    #7 0x564c0406cd8f in cleanup_tactical::operator()(ref<goal> const&, sref_buffer<goal, 16u>&) /yuhao/z3/build/../src/tactic/tactical.cpp:1032:14
    #8 0x564c0405fbfe in and_then_tactical::operator()(ref<goal> const&, sref_buffer<goal, 16u>&) /yuhao/z3/build/../src/tactic/tactical.cpp:122:19
    #9 0x564c0405fbfe in and_then_tactical::operator()(ref<goal> const&, sref_buffer<goal, 16u>&) /yuhao/z3/build/../src/tactic/tactical.cpp:122:19
    #10 0x564c0405fbfe in and_then_tactical::operator()(ref<goal> const&, sref_buffer<goal, 16u>&) /yuhao/z3/build/../src/tactic/tactical.cpp:122:19
    #11 0x564c0403b7ca in exec(tactic&, ref<goal> const&, sref_buffer<goal, 16u>&) /yuhao/z3/build/../src/tactic/tactic.cpp:165:9
    #12 0x564c0403bf07 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>>&) /yuhao/z3/build/../src/tactic/tactic.cpp:185:9
    #13 0x564c03f04d30 in (anonymous namespace)::tactic2solver::check_sat_core2(unsigned int, expr* const*) /yuhao/z3/build/../src/solver/tactic2solver.cpp:241:17
    #14 0x564c03f0e4b2 in solver_na2as::check_sat_core(unsigned int, expr* const*) /yuhao/z3/build/../src/solver/solver_na2as.cpp:67:12
    #15 0x564c03f1e671 in combined_solver::check_sat_core(unsigned int, expr* const*) /yuhao/z3/build/../src/solver/combined_solver.cpp
    #16 0x564c03f2fdce in solver::check_sat(unsigned int, expr* const*) /yuhao/z3/build/../src/solver/solver.cpp:318:13
    #17 0x564c03e7f1f5 in cmd_context::check_sat(unsigned int, expr* const*) /yuhao/z3/build/../src/cmd_context/cmd_context.cpp:1778:27
    #18 0x564c03d6ccf2 in smt2::parser::parse_check_sat() /yuhao/z3/build/../src/parsers/smt2/smt2parser.cpp:2633:19
    #19 0x564c03d5d950 in smt2::parser::operator()() /yuhao/z3/build/../src/parsers/smt2/smt2parser.cpp:3191:29
    #20 0x564c03d5c4c6 in parse_smt2_commands(cmd_context&, std::istream&, bool, params_ref const&, char const*) /yuhao/z3/build/../src/parsers/smt2/smt2parser.cpp:3242:12
    #21 0x564c0086a7b1 in read_smtlib2_commands(char const*) /yuhao/z3/build/../src/shell/smtlib_frontend.cpp:182:18
    #22 0x564c008cb5aa in main /yuhao/z3/build/../src/shell/main.cpp:384:28
    #23 0x7f00262bcd8f  (/lib/x86_64-linux-gnu/libc.so.6+0x29d8f) (BuildId: 962015aa9d133c6cbcfb31ec300596d7f44d3348)
    #24 0x7f00262bce3f in __libc_start_main (/lib/x86_64-linux-gnu/libc.so.6+0x29e3f) (BuildId: 962015aa9d133c6cbcfb31ec300596d7f44d3348)
    #25 0x564c00784544 in _start (/yuhao/z3/build/z3+0x1ea544) (BuildId: 5c00c5286df32e49d27f99f213a657243f3d2f76)

0x61900001feb0 is located 48 bytes inside of 920-byte region [0x61900001fe80,0x619000020218)
freed by thread T0 here:
    #0 0x564c0081e0c6 in free (/yuhao/z3/build/z3+0x2840c6) (BuildId: 5c00c5286df32e49d27f99f213a657243f3d2f76)
    #1 0x564c05d4172a in memory::deallocate(void*) /yuhao/z3/build/../src/util/memory_manager.cpp:286:5

previously allocated by thread T0 here:
    #0 0x564c0081e36e in malloc (/yuhao/z3/build/z3+0x28436e) (BuildId: 5c00c5286df32e49d27f99f213a657243f3d2f76)
    #1 0x564c05d41c95 in memory::allocate(unsigned long) /yuhao/z3/build/../src/util/memory_manager.cpp:301:16

SUMMARY: AddressSanitizer: heap-use-after-free /yuhao/z3/build/../src/util/rlimit.cpp:90:35 in reslimit::pop_child()
Shadow bytes around the buggy address:
  0x61900001fc00: fd fd fd fd fd fd fd fd fd fd fd fd fd fd fd fd
  0x61900001fc80: fd fd fd fd fd fd fd fd fd fd fd fd fd fd fd fd
  0x61900001fd00: fd fd fd fd fd fd fd fd fd fd fd fd fd fd fd fd
  0x61900001fd80: fd fd fd fd fd fd fd fd fd fd fd fd fd fa fa fa
  0x61900001fe00: fa fa fa fa fa fa fa fa fa fa fa fa fa fa fa fa
=>0x61900001fe80: fd fd fd fd fd fd[fd]fd fd fd fd fd fd fd fd fd
  0x61900001ff00: fd fd fd fd fd fd fd fd fd fd fd fd fd fd fd fd
  0x61900001ff80: fd fd fd fd fd fd fd fd fd fd fd fd fd fd fd fd
  0x619000020000: fd fd fd fd fd fd fd fd fd fd fd fd fd fd fd fd
  0x619000020080: fd fd fd fd fd fd fd fd fd fd fd fd fd fd fd fd
  0x619000020100: fd fd fd fd fd fd fd fd fd fd fd fd fd fd fd fd
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
==2887688==ABORTING
NikolajBjorner commented 2 months ago

this is fuzzspam and mainly distracting. You can submit pull requests fixing issues.