search

Boolector / boolector

A Satisfiability Modulo Theories (SMT) solver for the theories of fixed-size bit-vectors, arrays and uninterpreted functions.
http://boolector.github.io
Other
325 stars 63 forks source link

heap-use-after-free at src/parser/btorsmt.c:383 #129

Closed rainoftime closed 4 years ago

rainoftime commented 4 years ago

Hi, for the following formula,

; COeck-proof --quiet
; EXPECT: unsat
(bet-logic QF_BV)
(declare-fun x () (_ BitVec 4))
(assert (and (= (bvudiv (_ bv2 4) x) (_ bv2 4)) (= (_ bv0 4) x) (= (_ bv1 4) x)))
(check-sat)
(exit)

boolector 59c9ade58 throws a uaf

==171704==ERROR: AddressSanitizer: heap-use-after-free on address 0x60300000e020 at pc 0x7f3fa04e1dc4 bp 0x7ffcf33fd3e0 sp 0x7ffcf33fd3d0
READ of size 8 at 0x60300000e020 thread T0
    #0 0x7f3fa04e1dc3 in recursively_delete_smt_node /home/boolector/src/parser/btorsmt.c:383
    #1 0x7f3fa04e224c in release_smt_nodes /home/boolector/src/parser/btorsmt.c:443
    #2 0x7f3fa04e224c in release_smt_internals /home/peisen/test/tofuzz/boolector/src/parser/btorsmt.c:449
    #3 0x7f3fa05099f3 in parse_smt_parser/home/boolector/src/parser/btorsmt.c:2956
    #4 0x7f3fa035a789 in parse_aux /boolector/src/btorparse.c:68
    #5 0x7f3fa035a789 in btor_parse /boolector/src/btorparse.c:235
    #6 0x41597d in boolector_main /boolector/src/btormain.c:1440
    #7 0x7f3f9fdd982f in __libc_start_main (/lib/x86_64-linux-gnu/libc.so.6+0x2082f)
    #8 0x402748 in _start (/home/boolector/build/bin/boolector+0x402748)
mpreiner commented 4 years ago

Crash is in btorsmt.c, which is the old and unmaintained SMT-LIB v1 parser. Please do not submit any more issues on btorsmt.c