[Code Generator] Simplify Expressions

[ebehner]

Proposal

During the restructuring, we simplify conditions using their old SSA name. Furthermore, we never simplify any expression that is not part of a condition.

More precisely, we would like to be able to simplify expression as

• a+a to 2a or 1+ a + 3 to a + 4
• arg2 = arg1 + -1L to arg2 = arg1 - 1L
• a + 1 < 5 to a < 4 or a < 5 & a < 3 to a < 3

Approach

In the code generator, translate every pseudo-condition into a logic condition (either z3 or custom logic) and simplify it. Do the same with the logic conditions, which are saved using symbols and a condition map.

The benefit of doing it in the code generator is that we do not have to translate it back to our pseudo-language.

Attention: When simplifying unsigned comparison, like ULE(BitVec('x', 32), BitVecVal(5, 32)), with z3, the result is And(Extract(31, 3, x) == 0, ULE(Extract(2, 0, x), 5)) which is less readable. So one has to be careful how to simplify.