Next steps for CSE

Following https://github.com/runtimeverification/kontrol/pull/284, we now have a very simple version of CSE merged into Kontrol. This allows us to take summaries of small functions and use them in executing larger functions. The next steps are to make this practical for real-world examples, which will include:

• Test on bigger examples. Take engagement codebases, generate summaries for sub-functions, store them, and use them for executing the larger tests. Upstream any examples that cause problems in the CSE process, to fix the bugs and make sure the summaries are useful (committing the output as part of test_foundry_dependency test-harness).
• Automated detection of call-graph structure. If the user passes the --cse flag, then we should walk the call-graph of the contracts and extract any functions that we can produce summaries for, and make sure the summaries exist before calling the current proof.
• Internal functions. The current support only works to generate the initial specifications of external functions, then re-using them. Many internal functions are used a lot though, and we would benefit from being able to have summaries of those. This will require extracting from the Solidity compiler the start/stop program counter of the internal function, as well as the wordstack structure associated with it, so that we can build the appropriate LHS of the given internal function.
• Node merging. Currently, when including a summary, we just include each basic block of execution, meaning we're retaining the branching structure of sub-functions. We should have a way that the user can minimize branching structure of the functions that are being called by doing node-merging. Specifically, the final nodes that are with the same status code EVMC_SUCCESS should all be merged together with the differences between the nodes guarded by #ite conditions. This can be done as two transformations, one which pulls branches up to the root of the CFG, and a second which merges the node with KCFGs behind it.

Start by reading PR #284 and the existing --cse path in Kontrol. Use the test_foundry_dependency test harness with larger engagement codebases to identify summary failures, then inspect Solidity compiler metadata for internal-function program counters and wordstack structure. Done means the remaining checklist items are implemented and covered by useful upstreamed examples.