Expand path elimination of ecfg to consider multiple blocks
ecfg currently only considers each basic block in isolation when determining possible jump targets. It can handle constants, arithmetic, and cases where z3 can prove only certain addresses are possible (ex. pop() * 0 will always be zero.) In all other cases, ecfg is forced to assume that all jump targets are reachable.
For small handwritten programs, this naive approach is sufficient, but even the simplest solidity contract turns into an unreadable mess of paths.
The next step for ecfg is to consider the program flow as a whole, and trace execution paths starting from offset zero, building a more complete picture. In other words, to further improve the control flow graph, the inputs to each block have to come from the preceding blocks.