Usability improvements to foundry-merge-node

[lucasmt]

With this PR, we can now use the foundry-merge-nodes command to merge two nodes in different branches into a single node that subsumes both. This lets us merge branches back after a split, for example after an if statement or a loop, continuing the execution as a single branch, which has the potential of greatly improving the scalability of the tool in code with many loops or if statements.

However, this command has a few limitations in terms of usability:

1. The corresponding nodes in each branch (same PC) need to be present in the KCFG in order to be merged. This is not necessarily easy to ensure.
2. Because it requires manual intervention, the result of the verification becomes harder to reproduce.

We should think about ways to address these limitations to make this functionality easier to use. For example, suppose there was a cheatcode kevm.mergePoint() that denotes the point where we want to merge branches:

if (condition) {
    // if branch
} else {
    // else branch
}

kevm.mergePoint();

If we could implement this cheatcode such that the point where it's called is always added as a node to the KCFG, this would take care of (1). Going one step further, if we had an option to automatically merge such nodes if they have the same PC, this would take care of (2) (but this heuristic might not always work, for example if the merge point itself is inside a loop or a function that is called multiple times). But I don't know if something like that could actually be implemented, because it is a cheatcode that would not be handled solely from inside kevm, instead needing to somehow communicate with pyk.

I'd like to hear people's thoughts on this and brainstorm possible options.

[lucasmt]

For now, the alternative that I'm using to mergePoint is to make an external call that does nothing (it can be implemented as a dummy cheatcode, for example) and turn on --break-on-calls. But this will break on every external call, which will slow down execution a bit.

[ehildenb]

I would call it a kevm.cut() instead, in the same notion of a cut-rule, and we can just make the rule which implements it a cut-rule. This is in line with the idea of cut-points from @daejunpark's thesis: https://www.semanticscholar.org/paper/Cut-Bisimulation-and-Program-Equivalence-Park-Kasampalis/be608a0dcfe23747c4146ed0f10a544ab015e059

[lucasmt]

One potential complication that just occurred to me based on the current engagement: the point where we ideally want to merge can be inside the client code, in which case calling a cheatcode is not really possible.

[palinatolmach]

Oh, right, thanks @lucasmt. @ehildenb said the same thing — his suggestion is to let the user specify PCs in the contract being verified that we can use to generate some dummy rule that can behave as a cut rule (creating and saving relevant nodes into KCFG) and facilitating the merge, and/or add these PC to the <cut opcodes> cell (or something like this) in the configuration. EDIT: here's another description of the proposal by Everett that I found: "We could store a set in the KEVM configuration called "cut-program-counts", and have a simple no-op rule that fires when we hit such a opcode pc, and then make that rule a cut-rule."

@lucasmt do you think it would work? @ehildenb could you please check if I got it right?

@nwatson22 please let me know if you have any suggestions or comments on this issue too.

[lucasmt]

@palinatolmach Yeah, I think that could work. We would need to update the PC if the code changed, but that would be a relatively minor inconvenience compared with manually editing the KCFG every time to find the node we want.

[palinatolmach]

Another suggestion from @lisandrasilva is to allows specifying the desired place of merging using natspec comments in the client code — that would not entail any modification of the code itself, but would improve the interface for using the node merging functionality.

[lisandrasilva]

I would also suggest to merge according to some condition, for instance:

kevm.merge(removeNode != 0)

At this point, all nodes that satisfy the condition removeNode != 0 (where removeNode is a code variable) would be merged.