Tracking MX project performance fixes

[Baltoli]

@jberthold and @virgil-serbanuta are working on optimizing symbolic execution of the MX- family of projects. Part of this work will entail making changes at the K level to improve performance. We'd ideally like to learn from this process and perhaps write up some guides on writing K code that performs well from the get-go.

Please log any MX PRs that are in aid of improved performance here:

[jberthold]

https://github.com/runtimeverification/mx-backend/pull/108 addresses a problem with variable subsorting: When a rule with variable A:SortA is matched against a configuration that has a variable B:SortB and SortA < SortB, the match will be conditional/indeterminate (causing an abort in booster, and matching with further rules/branching in kore-rpc). This is the correct behaviour, but in this particular case, the variable B was only introduced temporarily (programmatically in the python client code) to temporarily abstract unnecessary payload. It is easy to make this mistake of picking too general a sort when abstracting. pyk will insert the required injections SortA -> SortB automatically so the fix was easy.

[jberthold]

Some book-keeping of past PRs related to mx-backend performance:

• https://github.com/runtimeverification/wasm-semantics/pull/631: Refactoring to make a function on the RHS of a rewrite rule total (booster aborts if a RHS contains partial functions unless the rule is marked as preserves-definedness)
• https://github.com/runtimeverification/mx-semantics/pull/262: Execution is interrupted at the newWasmInstance rule to compute this new WASM instance externally (using LLVM from the python client). However, when marking a rule as a cut-point-rule, the following next state (RHS of the rule) will still be computed and returned. The PR introduced an intermediate execution state that requires no computation to avoid the duplicate computation.
• https://github.com/runtimeverification/wasm-semantics/pull/632 and https://github.com/runtimeverification/mx-semantics/pull/263: Run-off-the-mill PRs to mark rules as preserving definedness (avoiding fallbacks) and a fully-symbolic function as no-evaluators to avoid LLVM errors (which may also cause fallbacks but mainly warning messages).

[jberthold]

Recent PRs

• https://github.com/runtimeverification/mx-semantics/pull/289 Refactors a rule that included a two-stage match in Map fields (paraphrased: <a> K |-> K2 ...</a> <b> K2 |-> V ... </b>) to avoid a natch abort.
• https://github.com/runtimeverification/wasm-semantics/pull/651 and https://github.com/runtimeverification/wasm-semantics/pull/654 Mark a few rules as preserves-definedness (including justification for the added attributes in comments)
• https://github.com/runtimeverification/wasm-semantics/pull/655 Avoid pushing an unevaluated #if B #then exp1 #else exp2 #fi into a configuration cell, by forcing the decision depending on B (Caveat: This modifies the branching structure and may duplicate work so it might not always be better!)