Improve SSI representation

[agle]

SSI form is difficult for transforms to preserve due to lacking specific syntax constructs; we just generate a copy before the assert/assume which is not distinguishable from any other copy. To support it properly we can follow the approach of https://link.springer.com/content/pdf/10.1007/978-3-030-80515-9.pdf to split live ranges of variables.

1. Introduce sigma functions before branches, the dual of a phi; to join the information associated with split ranges in a backwards analysis.
2. Make the copy associated with an assert or assume happen in parallel to the assertion.

• Ocamlgraph provides dominance frontiers so it may be simple to improve the placement of phi nodes.