Improve CFG's termination condition

[acuarica]

Instead of always follow jump destinations (and loop unrolling) determine when to stop symbolic execution. The main issue is when jump destinations are in different basic blocks. That is, when a jump destination is pushed in one basic block, but it's jumped to in a different one.

Some papers that might solve this issue

• https://dl.acm.org/doi/pdf/10.1145/3527321
• https://arxiv.org/pdf/1809.03981.pdf
• https://arxiv.org/pdf/2004.14437.pdf

The main problem that arises when deduplicating basic blocks is the introduction of phi-nodes or equivalent. The introduction of Local expressions represent SSA nodes. For a quick intro to SSA see https://www.cs.cornell.edu/courses/cs6120/2022sp/lesson/6/. When introducing phi-nodes it might require to re-execute already executed states.

As an alternative one can use Basic Block Arguments https://2pi.dk/2022/05/bb-arguments, but I'm not sure how to convert from a stack based execution to BB arguments. Discussion about phi-nodes vs BB arguments might be helpful https://news.ycombinator.com/item?id=22432344 and https://mlir.llvm.org/docs/Rationale/Rationale/#block-arguments-vs-phi-nodes.

For reference, how a similar library handles jumpi and jump instructions

jumpi https://github.com/a16z/halmos/blob/main/src/halmos/sevm.py#L1878
jump https://github.com/a16z/halmos/blob/main/src/halmos/sevm.py#L1949