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
335 stars 62 forks source link

SMT-LIB v1 parser crashes #90

Closed strongcourage closed 4 years ago

strongcourage commented 4 years ago

Hi,

I am aware that you will no longer support SMT-LIB v1 parser, but actually there is a null pointer dereferencing bug (the latest commit 3249ae0) in set_last_occurrence_of_symbols() in parser/btorsmt.c, that causes boolector to crash with PoC.

Valgrind says:

==18389== Invalid read of size 8
==18389==    at 0x4F05582: set_last_occurrence_of_symbols (btorsmt.c:2803)
==18389==    by 0x4F05582: parse (btorsmt.c:2914)
==18389==    by 0x4F05582: parse_smt_parser (btorsmt.c:2955)
==18389==    by 0x4EAE7FE: parse_aux (btorparse.c:68)
==18389==    by 0x4EAE7FE: btor_parse (btorparse.c:235)
==18389==    by 0x40563F: boolector_main (btormain.c:1464)
==18389==    by 0x540182F: (below main) (libc-start.c:291)
==18389==  Address 0x8 is not stack'd, malloc'd or (recently) free'd

Best, MD

mpreiner commented 4 years ago

The SMT-LIB v1 parser is outdated and not maintained anymore, and will be removed soon. Please do not submit any new issues on this parser.