[TASK] Computed JUMPDEST Improvements

[iamrecursion]

Description

The CpuFrilessVerifier contract has some situations where a non-conditional JUMP instruction jumps to different destinations based on the offset (of a JUMPDEST) that gets pushed onto the stack at some point prior to reaching the JUMP instruction.

The smlXL control flow generator (an internal tool) shows that these independent paths are able to be discovered statically (as it also does symbolic execution), which implies that the SLA should be able to reach all of these paths during its execution.

However, it currently does reach all of these paths (as evidenced by us never seeing the SLOAD opcodes and not finding a layout). Based on analysis of the full CFG, it looks like these things are certainly reachable from the initial function dispatch table, so we should be able to improve the analyzer to reach these.

It does not appear that the JUMPDEST is ever non-constant as far as the analyzer is concerned, so we are not bailing in that respect. This makes it all the more probable that we should be able to deal with this situation properly.

Spec

• Work out a strategy—potentially using a mechanism like the one described in [FEAT] Extensible Execution Strategies #48—that allows us to see these JUMPDESTs correctly.
• Alternatively, work out a strategy that blindly visits all un-visited JUMPDESTs while retaining type coherence.
• Implement whichever sounds best.

[iamrecursion]

Upon a bit more investigation, it seems that the SLA never hits the code paths that generate jump targets other than 0x1d20 on the top of the stack at 0x3176. This implies that we are likely saturating some conditional jump target during the course of execution, and thereby never hitting any of the other potential jump targets from 0x3176 (these are 0x21c5, 0x2187 and 0x2138).

A smarter execution strategy in this case is likely to be the solution here. 0x3176 is visited in a loop, and we are clearly continuing the same path through the loop until it saturates. This means that we never see the alternative, no matter how high we set the jump target fork limit.

[iamrecursion]

My current thoughts on how to improve this situation is to change the default execution strategy a little.

• Currently, JUMPDEST instructions saturate based on the number of incoming JUMPI instructions.
• In this situation, we saturate the JUMPDEST from a single JUMPI and hence never see the other code paths.
• My suggestion is to change the saturation logic so that you have a saturation counter per-JUMPI that is set to something lower.
• That way, the initial loop would saturate and then allow a different code path to be tried.
• This would continue until all JUMPI with destination JUMPDEST have saturated.

Doing this would likely increase runtime, so using a lower per-jump saturation threshold will be necessary. Take care to profile this approach and see if it is generally feasible.

I should also note that this may not 100% solve this problem, as we may be running into strange path saturation behavior due to the complexity here.