Check out the Issue Explorer
Looking to fund some work? You can submit a new Funded Issue here.
Implement the most basic optimizations like the ones yo can find in a compiler: e.g., simple arithmetic simplifications (x + 0 = x), strength reduction (x * 2n = x << n), linear simplification (2*x - x = x), etc.
There is some optimizations already implemented here: https://github.com/trailofbits/manticore/blob/98190d891d87ac2f3ec3ba5927e6fd4b024cc7e2/manticore/core/smtlib/visitors.py#L351
To consider this issue fixed we need to:
1) Find a good and exhaustive list of common expression simplifications as the ones found in compilers.
2) Implement the rewriting visitors for all of the simplifications using the ones already implemented as inspirational guide.
3) Document each transformation.
4) Add tests for each. Ask the solver to demonstrate the simplified expression is equivalent to the original one.
5) Be sure the `taint` of expressions is maintained in the simplification if required.
6) This should be configurable using config.py
7) Overall symbolic execution performance gain should be measure/tested over a big test set (see https://github.com/trailofbits/manticore/issues/1204)