trailofbits / manticore

Symbolic execution tool
https://blog.trailofbits.com/2017/04/27/manticore-symbolic-execution-for-humans/
GNU Affero General Public License v3.0
3.69k stars 472 forks source link

Limit Sanity Checks in SMTLib #1427

Closed ehennenfent closed 4 years ago

ehennenfent commented 5 years ago

core/smtlib/expression.py currently has 60 asserts, most of which are just sanity checks for typing. While they served a purpose when the library was relatively new and untested, these days they effectively do nothing but slow down every symbolic expression. We should strip out the asserts that we don't need and, where possible, replace them with type hints so that we can opt-in to type checks rather than having to opt-out of asserts.

(Note: the same will eventually be true of the asserts in the aarch64 module, but since that's still largely untested, we'll save that for another issue)

ehennenfent commented 4 years ago

1543 fixed this