Module linearize 

This module provides a function linearize() that converts IR from function bodies containing loops and other IR, into a linear sequence of instructions without any control flow.

The way this works is as follows:

    A    A: declare x; if b ...
   / \   B: then { x = f(x) }
  B   C  C: else { x = g(x) }
   \ /   D: return x
    D

This is then converted into SSA form, like:

    A    A: declare x/1; if b
   / \   B: then { x/2 = f(x/1) }
  B   C  C: else { x/3 = g(x/1) }
   \ /   D: x/4 = φ(x/2, x/3); return x/4
    D

Finally, we come out of SSA form by placing the control flow graph into topological order, and replacing the phi functions with ite functions that map directly to the ite construct in the SMT solver.

   A     A: declare x/1;
   |     B: declare x/2;
   B        x/2 = f(x/1);
   |     C: declare x/3;
   C        x/3 = g(x/1);
   |     D: declare x/4;
   D        x/4 = ite(b, x/2, x/3);
            return x/4

The obvious limitations of this are that the function in question needs to be pure (it can only read architectural state), and its control flow graph must be acyclic so it can be placed into a topological order.

Functions

linearize

self_test

Test that a rewritten function body is equivalent to the original body by constructing a symbolic execution problem that proves this. Note that this function should called with an uninitialized architecture.