# How to efficiently simplify obfuscated formula in QF_BV logic with Z3?

I would like to know if there are efficient ways to simplify arithmetic formula expression over bit-vectors with Microsoft Z3. But, first, I would like to explain a bit the problem. Lets start with an example:

``````x + y == (x ^ y) + 2 * (x & y)
``````

Both `x + y` and `(x ^ y) + 2 * (x & y)` are, in fact, coding the addition over bit-vectors. Of course, the right hand formula is used to confuse a reverser when found in the binary program. I try to find tools and techniques to simplify the obfuscated formula and find the simpler form of the formula (left-hand).

For this, I looked at the Python interface of Z3, trying to see what I can get out of it. So, defining the obfuscated formula is done like this:

``````>>> from z3 import *
>>> x = BitVec('x', 32)
>>> y = BitVec('y', 32)
>>> fun1 = (x ^ y) + 2 * (x & y)
``````

Now, lets try to simplify this function with the help of the built-in function `simplify`:

``````>>> simplify((x ^ y) + 2 * (x & y))
(x ^ y) + 2*~(~x | ~y)
``````

Not really convincing... But, lets try to prove the equivalence with `x + y`:

``````>>> prove((x ^ y) + 2 * (x & y) == x + y)
proved
>>> prove((x ^ y) + 2 * (x & y) == x - y)
counterexample
[y = 2164268032, x = 2139094080]
``````

I added a negative result to show that it is also possible to disqualify a formula.

So, if the `simplify` function is not really convincing, it is still possible to try, in a brute-force manner to compare the unknown formula with a list of simpler and usual formula one after one. But, this way seems extremely inefficient to me. I guess I am missing some smarter algorithms to simplify formula.

I would like to know if there are some already existing tools or well-known techniques to perform in a more efficient manner than the brute-force approach. So, if someone has some hints or comments about this, it would be more than welcome.

• Try `help_simplify()` - some of the options may do what you are looking for. Feb 2 '14 at 21:45
• I already tried several of these tactics (`simplify(fun1, som=True)`), but with no success either. Maybe I missed the right set of tactics to use. If you have such a list, I would be happy to know your suggestion ! Feb 2 '14 at 21:49
• The question isn't very clear. What does "efficiently" mean, and what makes `simplify` "inefficient"? Feb 2 '14 at 23:49
• You're right. I meant more efficiently than a brute-force approach where you check all formula against the one you are investigating. Feb 3 '14 at 6:31