From afeca6e5247194cf27be3d8c2dbc0d320b4fd48c Mon Sep 17 00:00:00 2001 From: Everett Hildenbrandt Date: Thu, 5 Sep 2024 21:25:40 +0000 Subject: [PATCH 1/3] test_foundry_prove: remove unused option --- src/tests/integration/test_foundry_prove.py | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/tests/integration/test_foundry_prove.py b/src/tests/integration/test_foundry_prove.py index 43aeb39c1..f29992f58 100644 --- a/src/tests/integration/test_foundry_prove.py +++ b/src/tests/integration/test_foundry_prove.py @@ -417,7 +417,7 @@ def test_foundry_merge_nodes( ) check_pending(foundry, test, [6, 7]) - foundry_merge_nodes(foundry, MergeNodesOptions({'test': test, 'nodes': [6, 7], 'include_disjunct': True})) + foundry_merge_nodes(foundry, MergeNodesOptions({'test': test, 'nodes': [6, 7]})) check_pending(foundry, test, [8]) From 028c8ffb41167982c17efaa2d7d34bf01589c7c2 Mon Sep 17 00:00:00 2001 From: Everett Hildenbrandt Date: Thu, 5 Sep 2024 21:51:56 +0000 Subject: [PATCH 2/3] kontrol/foundry: remove use of keep_values argument --- src/kontrol/foundry.py | 18 +++++++++++++++--- 1 file changed, 15 insertions(+), 3 deletions(-) diff --git a/src/kontrol/foundry.py b/src/kontrol/foundry.py index 3427cec38..fb5f077e9 100644 --- a/src/kontrol/foundry.py +++ b/src/kontrol/foundry.py @@ -21,14 +21,22 @@ from kevm_pyk.utils import byte_offset_to_lines, legacy_explore, print_failure_info, print_model from pyk.cterm import CTerm from pyk.kast.inner import KApply, KInner, KSort, KToken, KVariable -from pyk.kast.manip import cell_label_to_var_name, collect, extract_lhs, flatten_label, minimize_term, top_down +from pyk.kast.manip import ( + cell_label_to_var_name, + collect, + extract_lhs, + flatten_label, + minimize_term, + ml_pred_to_bool, + top_down, +) from pyk.kast.outer import KDefinition, KFlatModule, KImport, KRequire from pyk.kcfg import KCFG from pyk.kcfg.minimize import KCFGMinimizer from pyk.prelude.bytes import bytesToken from pyk.prelude.collections import map_empty from pyk.prelude.k import DOTS -from pyk.prelude.kbool import notBool +from pyk.prelude.kbool import andBool, notBool, orBool from pyk.prelude.kint import INT, intToken from pyk.prelude.ml import mlEqualsFalse, mlEqualsTrue from pyk.proof.proof import Proof @@ -1122,7 +1130,11 @@ def check_cells_equal(cell: str, nodes: Iterable[KCFG.Node]) -> bool: anti_unification = nodes[0].cterm for node in nodes[1:]: - anti_unification, _, _ = anti_unification.anti_unify(node.cterm, keep_values=True, kdef=foundry.kevm.definition) + anti_unification, csubst1, csubst2 = anti_unification.anti_unify(node.cterm, kdef=foundry.kevm.definition) + constraint1 = andBool([csubst1.subst.pred] + list(map(ml_pred_to_bool, csubst1.constraints))) + constraint2 = andBool([csubst2.subst.pred] + list(map(ml_pred_to_bool, csubst2.constraints))) + anti_unification.add_constraint(mlEqualsTrue(orBool([constraint1, constraint2]))) + new_node = apr_proof.kcfg.create_node(anti_unification) for node in nodes: succ = apr_proof.kcfg.successors(node.id) From 523ee6bb2426b8f7257e34a586fabacd91718609 Mon Sep 17 00:00:00 2001 From: Everett Hildenbrandt Date: Thu, 5 Sep 2024 21:54:20 +0000 Subject: [PATCH 3/3] kontrol/foundry: use new CSubst.pred instead of Subst.pred --- src/kontrol/foundry.py | 10 ++++++++-- 1 file changed, 8 insertions(+), 2 deletions(-) diff --git a/src/kontrol/foundry.py b/src/kontrol/foundry.py index fb5f077e9..57ec7356e 100644 --- a/src/kontrol/foundry.py +++ b/src/kontrol/foundry.py @@ -1131,8 +1131,14 @@ def check_cells_equal(cell: str, nodes: Iterable[KCFG.Node]) -> bool: anti_unification = nodes[0].cterm for node in nodes[1:]: anti_unification, csubst1, csubst2 = anti_unification.anti_unify(node.cterm, kdef=foundry.kevm.definition) - constraint1 = andBool([csubst1.subst.pred] + list(map(ml_pred_to_bool, csubst1.constraints))) - constraint2 = andBool([csubst2.subst.pred] + list(map(ml_pred_to_bool, csubst2.constraints))) + constraint1 = andBool( + [csubst1.pred(constraints=False, sort_with=foundry.kevm.definition)] + + list(map(ml_pred_to_bool, csubst1.constraints)) + ) + constraint2 = andBool( + [csubst2.pred(constraints=False, sort_with=foundry.kevm.definition)] + + list(map(ml_pred_to_bool, csubst2.constraints)) + ) anti_unification.add_constraint(mlEqualsTrue(orBool([constraint1, constraint2]))) new_node = apr_proof.kcfg.create_node(anti_unification)