SMT: Add explicit terminators to SSA graph

Makes the graph slightly cleaner, and means we can represent
conditionals in a way that shoud allow computing path conditions much
easier.

Essentially rather than a basic block being a list of instructions
where the last instruction is a jump (or other terminator) it is now a
list of instructions combined with an explict terminator, i.e.

CF_block (instrs @ I_jump (cval, label) ==> CF_block (instrs, T_jump (n, label))

Rather than storing the cval in the T_jump it just has a number that
links to a mapping from numbers to cvals, and we represent the
negation of any cval in that table by negating its number. Therefore
at any join point in the CFG, we can efficiently check when the
joining path conditionals contain both n and minus n and remove both.

0 files changed, 0 insertions, 0 deletions