Add foundry-merge-nodes option #1934

nwatson22 · 2023-06-30T00:43:32Z

Adds an option foundry-merge-nodes used with:

kevm foundry-merge-nodes [Contract.test_name] --node [node id] --node [node id]

which creates a new node which is the anti_unify_with_constraints of all the listed nodes and makes this node a cover of all the listed nodes.
Optionally, include the --include-disjunct flag to keep the abstracted nodes as an orBool disjunction, e.g.

<k> 1 </k>

merged with

<k> 2 </k>

would yield:

<k> N:Int </k>
#And (N ==K 1 orBool N ==K 2)

Additionally, the PR changes foundry-remove-node so that it no longer prunes the target node if it is a child of the removed node, and fixes foundry-step-node, foundry-section-edge, foundry-remove-node, foundry-list and foundry-to-dot, which were assuming that the proof being operated on was an APRProof and not an APRBMCProof, so they converted the proof back to an APRProof.

…ication/evm-semantics into noah/merge-branches

kevm-pyk/src/kevm_pyk/foundry.py

ehildenb · 2023-06-30T14:50:41Z

Let's reduce whitespace a bit, no need to define some of the intermediates (eg. intermeditae for new_cterm, can just directly create it an insert it as a node). Also, instead of naming the variables apr_proof, I've been trying to switch to just the more compact proof name everywhere.

ehildenb · 2023-06-30T14:57:14Z

We should also be putting a sanity check on the nodes the user has asked to merge. Specifically, they all must:

Have the exact same content in the following cells: <k>, <program>, <pc>, <callDepth>. Otherwise, throw an error.

Co-authored-by: Everett Hildenbrandt <everett.hildenbrandt@gmail.com>

…or <callDepth>

kevm-pyk/src/kevm_pyk/foundry.py

…ication/evm-semantics into noah/merge-branches

kevm-pyk/src/kontrol/foundry.py

* Add foundry-merge-nodes option * Set Version: 1.0.225 * Anti-unify without disjunct * Update kevm-pyk/src/kevm_pyk/foundry.py Co-authored-by: Everett Hildenbrandt <everett.hildenbrandt@gmail.com> * Update kevm-pyk/src/kevm_pyk/foundry.py Co-authored-by: Everett Hildenbrandt <everett.hildenbrandt@gmail.com> * Fix formatting * Rename apr_proof to proof, reduce whitespace * Disallow merging nodes if they do not match on <k>, <program>, <pc>, or <callDepth> * Improve variable naming * Add test for branch merging * Update expected contracts.k * Set Version: 1.0.226 * Set Version: 1.0.226 * Update expected output * Set Version: 1.0.227 * Update test_foundry_fail expected files * Keep disjunction of concrete values * Switch to using associated pyk branch * Set Version: 1.0.228 * Fix foundry_get_apr_proof and foundry_step_node to be compatible with APR and APRBMC proofs * Fix various commands to work with APRBMCProof * Update kevm-pyk/src/kevm_pyk/__main__.py * Update kevm-pyk/src/kevm_pyk/foundry.py * Update foundry_merge_nodes test * Fix formatting * Update expected files * Set Version: 1.0.229 * Set Version: 1.0.231 * Set Version: 1.0.232 * Set Version: 1.0.235 * Set Version: 1.0.236 * Revert poetry.lock * Fix setUp method execution being limited by max_iterations * Set Version: 1.0.239 * Set Version: 1.0.244 * Set Version: 1.0.249 * Set Version: 1.0.250 * Revert foundry_get_proof and foundry_get_apr_proof changes as they have been moved to another branch * Fix foundry_list proof_data_exists call * Use digest, not just method name for looking up setUp method * Revert change to proof loading path * Use foundry.get_apr_proof in foundry_merge_nodes * Set Version: 1.0.251 * Use foundry.get_apr_proof in test * Set Version: 1.0.252 * Set Version: 1.0.262 * Use new anti_unification function * Set Version: 1.0.263 * Set Version: 1.0.264 * Include kdefinition in anti_unify call and fix test * Re-add foundry-merge-nodes command * Set Version: 1.0.265 * Set Version: 1.0.265 * Set Version: 1.0.266 * Set Version: 1.0.267 --------- Co-authored-by: devops <devops@runtimeverification.com> Co-authored-by: Everett Hildenbrandt <everett.hildenbrandt@gmail.com>

Needed for runtimeverification/evm-semantics#1934. Adds an additional option to `anti_unify_with_constraints` which adds an additional constraint which is an `_orBool_` of the two anti-unifying substitutions. Adds a test for the method with this option which tests a new variable is created to abstract and the `orBool` constraint is added as described. --------- Co-authored-by: devops <devops@runtimeverification.com>

- Changed `anti_unify` and `anti_unify_with_constraints` to require a `KDefinition` which they use to grab the tightest sort for the terms they are abstracting - Since these actions are now associated with a specific K definition, moved them into `KDefinition` as methods. - Adds `KDefinition.least_common_supersort` which returns the most specific sort that will cover two terms (as long as one sort is a subsort of the other). - Uses this function in `KDefinition.sort` to determine the sort of a `KRewrite`. - Rewrote the tests for `anti_unify` and `anti_unify_with_constraints` to use `KDefinition` and test that the abstracted variables are now more tightly typed based on the original terms. This is an attempt to fix an issue in runtimeverification/evm-semantics#1934 where the looser sort bound is preventing simplification after the merging (anti-unification) of two nodes. --------- Co-authored-by: devops <devops@runtimeverification.com>