Allow merging branches back after a split

[lucasmt]

We need a way to merge branches back after they have been split. For example, if we have code like

if (condition) {
    x = 10;
} else {
    x = 12;
}

// rest of the program

KEVM will split into two branches, one where x contains 10 and another where it contains 12, and the rest of the program will be executed twice, once in each branch. Instead, in some cases it would be better if we could merge these branches back into a single branch where the contents of x are replaced with a symbolic variable X with the constraint X ==Int 10 orBool X ==Int 12, and then execute the rest of the program only once.

This could be implemented by a command like (just a suggestion, feel free to use a different syntax) kevm foundry-merge-nodes ContractName.testName --node N1 --node N2 ... --node Nk, which would create a new node N subsuming nodes N1...Nk. According to @ehildenb, this node can be computed automatically as a convex anti-unifier of N1...Nk.

[lucasmt]

@ehildenb suggested @nwatson22, @palinatolmach or @iFrostizz for this

[ehildenb]

Here is an anti-unification routine that can be used: https://github.com/runtimeverification/pyk/blob/49d861944bad260be137f68f4adc37b360e25771/src/pyk/kast/manip.py#L585

And here is the variant that can also handle constraints, though it does not do a good job: https://github.com/runtimeverification/pyk/blob/49d861944bad260be137f68f4adc37b360e25771/src/pyk/kast/manip.py#L600

You may need to fix this issue at the same time: runtimeverification/k#4219

[nwatson22]

What is meant by convex here?

[ehildenb]

Convex here means that no disjuncts (orBool) should show up in the resulting term, or matching logic disjuncts (#Or).

[nwatson22]

So when we abstract a cell, we should not do the thing suggested where we include an orBool of the concrete values?

[ehildenb]

That's right, that would make the anti-unifier concave instead of convex.