From 189cdb5ff282ec744f81a32f16a68874d4d3c8cb Mon Sep 17 00:00:00 2001 From: Noah Watson Date: Tue, 1 Aug 2023 14:47:37 -0500 Subject: [PATCH] Fix KCFGExplore.__init__() calls to pass in KoreClient --- kevm-pyk/src/kevm_pyk/__main__.py | 162 ++++++++++++------------- kevm-pyk/src/kevm_pyk/foundry.py | 188 +++++++++++++++--------------- 2 files changed, 179 insertions(+), 171 deletions(-) diff --git a/kevm-pyk/src/kevm_pyk/__main__.py b/kevm-pyk/src/kevm_pyk/__main__.py index 9d6ee86123..4936608015 100644 --- a/kevm-pyk/src/kevm_pyk/__main__.py +++ b/kevm-pyk/src/kevm_pyk/__main__.py @@ -13,6 +13,7 @@ from pyk.kast.outer import KApply, KRewrite from pyk.kcfg import KCFG, KCFGExplore from pyk.kore.prelude import int_dv +from pyk.kore.rpc import KoreClient, KoreServer from pyk.ktool.kompile import LLVMKompileType from pyk.ktool.krun import KRunOutput, _krun from pyk.prelude.ml import is_bottom, is_top @@ -281,85 +282,84 @@ def is_functional(claim: KClaim) -> bool: return not (type(claim_lhs) is KApply and claim_lhs.label.name == '') def _init_and_run_proof(claim: KClaim) -> tuple[bool, list[str] | None]: - with KCFGExplore( - kevm, - kcfg_semantics=KEVMSemantics(auto_abstract_gas=auto_abstract_gas), - id=claim.label, - bug_report=br, - kore_rpc_command=kore_rpc_command, - smt_timeout=smt_timeout, - smt_retry_limit=smt_retry_limit, - trace_rewrites=trace_rewrites, - ) as kcfg_explore: - proof_problem: Proof - if is_functional(claim): - if ( - save_directory is not None - and not reinit - and EqualityProof.proof_exists(claim.label, save_directory) - ): - proof_problem = EqualityProof.read_proof_data(save_directory, claim.label) + with KoreServer(kevm.definition_dir, kevm.main_module, bug_report=br) as server: + with KoreClient('localhost', server.port, bug_report=br) as client: + kcfg_explore = KCFGExplore( + kprint=kevm, + kore_client=client, + kcfg_semantics=KEVMSemantics(auto_abstract_gas=auto_abstract_gas), + id=claim.label, + trace_rewrites=trace_rewrites, + ) + proof_problem: Proof + if is_functional(claim): + if ( + save_directory is not None + and not reinit + and EqualityProof.proof_exists(claim.label, save_directory) + ): + proof_problem = EqualityProof.read_proof_data(save_directory, claim.label) + else: + proof_problem = EqualityProof.from_claim(claim, kevm.definition, proof_dir=save_directory) else: - proof_problem = EqualityProof.from_claim(claim, kevm.definition, proof_dir=save_directory) - else: - if save_directory is not None and not reinit and APRProof.proof_exists(claim.label, save_directory): - proof_problem = APRProof.read_proof_data(save_directory, claim.label) - - else: - _LOGGER.info(f'Converting claim to KCFG: {claim.label}') - kcfg, init_node_id, target_node_id = KCFG.from_claim(kevm.definition, claim) - - new_init = ensure_ksequence_on_k_cell(kcfg.node(init_node_id).cterm) - new_target = ensure_ksequence_on_k_cell(kcfg.node(target_node_id).cterm) - - _LOGGER.info(f'Computing definedness constraint for initial node: {claim.label}') - new_init = kcfg_explore.cterm_assume_defined(new_init) - - if simplify_init: - _LOGGER.info(f'Simplifying initial and target node: {claim.label}') - _new_init, _ = kcfg_explore.cterm_simplify(new_init) - _new_target, _ = kcfg_explore.cterm_simplify(new_target) - if is_bottom(_new_init): - raise ValueError( - 'Simplifying initial node led to #Bottom, are you sure your LHS is defined?' - ) - if is_bottom(_new_target): - raise ValueError( - 'Simplifying target node led to #Bottom, are you sure your RHS is defined?' - ) - new_init = CTerm.from_kast(_new_init) - new_target = CTerm.from_kast(_new_target) - - kcfg.replace_node(init_node_id, new_init) - kcfg.replace_node(target_node_id, new_target) - - proof_problem = APRProof( - claim.label, kcfg, init_node_id, target_node_id, {}, proof_dir=save_directory - ) - - passed = kevm_prove( - kevm, - proof_problem, - kcfg_explore, - save_directory=save_directory, - max_depth=max_depth, - max_iterations=max_iterations, - workers=workers, - break_every_step=break_every_step, - break_on_jumpi=break_on_jumpi, - break_on_calls=break_on_calls, - implication_every_block=implication_every_block, - bug_report=br, - kore_rpc_command=kore_rpc_command, - smt_timeout=smt_timeout, - smt_retry_limit=smt_retry_limit, - trace_rewrites=trace_rewrites, - ) - failure_log = None - if not passed: - failure_log = print_failure_info(proof_problem, kcfg_explore) - - return passed, failure_log + if save_directory is not None and not reinit and APRProof.proof_exists(claim.label, save_directory): + proof_problem = APRProof.read_proof_data(save_directory, claim.label) + + else: + _LOGGER.info(f'Converting claim to KCFG: {claim.label}') + kcfg, init_node_id, target_node_id = KCFG.from_claim(kevm.definition, claim) + + new_init = ensure_ksequence_on_k_cell(kcfg.node(init_node_id).cterm) + new_target = ensure_ksequence_on_k_cell(kcfg.node(target_node_id).cterm) + + _LOGGER.info(f'Computing definedness constraint for initial node: {claim.label}') + new_init = kcfg_explore.cterm_assume_defined(new_init) + + if simplify_init: + _LOGGER.info(f'Simplifying initial and target node: {claim.label}') + _new_init, _ = kcfg_explore.cterm_simplify(new_init) + _new_target, _ = kcfg_explore.cterm_simplify(new_target) + if is_bottom(_new_init): + raise ValueError( + 'Simplifying initial node led to #Bottom, are you sure your LHS is defined?' + ) + if is_bottom(_new_target): + raise ValueError( + 'Simplifying target node led to #Bottom, are you sure your RHS is defined?' + ) + new_init = CTerm.from_kast(_new_init) + new_target = CTerm.from_kast(_new_target) + + kcfg.replace_node(init_node_id, new_init) + kcfg.replace_node(target_node_id, new_target) + + proof_problem = APRProof( + claim.label, kcfg, init_node_id, target_node_id, {}, proof_dir=save_directory + ) + + passed = kevm_prove( + kevm, + proof_problem, + kcfg_explore, + save_directory=save_directory, + max_depth=max_depth, + max_iterations=max_iterations, + workers=workers, + break_every_step=break_every_step, + break_on_jumpi=break_on_jumpi, + break_on_calls=break_on_calls, + implication_every_block=implication_every_block, + bug_report=br, + kore_rpc_command=kore_rpc_command, + smt_timeout=smt_timeout, + smt_retry_limit=smt_retry_limit, + trace_rewrites=trace_rewrites, + ) + failure_log = None + if not passed: + failure_log = print_failure_info(proof_problem, kcfg_explore) + + return passed, failure_log results: list[tuple[bool, list[str] | None]] if workers > 1: @@ -473,8 +473,10 @@ def exec_show_kcfg( ) if failure_info: - with KCFGExplore(kevm, kcfg_semantics=KEVMSemantics(), id=proof.id) as kcfg_explore: - res_lines += print_failure_info(proof, kcfg_explore) + with KoreServer(kevm.definition_dir, kevm.main_module) as server: + with KoreClient('localhost', server.port) as client: + kcfg_explore = KCFGExplore(kprint=kevm, kore_client=client, kcfg_semantics=KEVMSemantics(), id=proof.id) + res_lines += print_failure_info(proof, kcfg_explore) print('\n'.join(res_lines)) diff --git a/kevm-pyk/src/kevm_pyk/foundry.py b/kevm-pyk/src/kevm_pyk/foundry.py index 974f2830ff..731a36974b 100644 --- a/kevm-pyk/src/kevm_pyk/foundry.py +++ b/kevm-pyk/src/kevm_pyk/foundry.py @@ -16,6 +16,7 @@ from pyk.kast.manip import free_vars, minimize_term from pyk.kast.outer import KDefinition, KFlatModule, KImport, KRequire from pyk.kcfg import KCFG, KCFGExplore +from pyk.kore.rpc import KoreClient, KoreServer from pyk.ktool.kompile import LLVMKompileType from pyk.prelude.bytes import bytesToken from pyk.prelude.k import GENERATED_TOP_CELL @@ -511,55 +512,52 @@ def foundry_prove( def _init_and_run_proof(_init_problem: tuple[str, str]) -> tuple[bool, list[str] | None]: proof_id = f'{_init_problem[0]}.{_init_problem[1]}' - llvm_definition_dir = foundry.out / 'kompiled-llvm' if use_booster else None - - with KCFGExplore( - foundry.kevm, - kcfg_semantics=KEVMSemantics(auto_abstract_gas=auto_abstract_gas), - id=proof_id, - bug_report=br, - kore_rpc_command=kore_rpc_command, - llvm_definition_dir=llvm_definition_dir, - smt_timeout=smt_timeout, - smt_retry_limit=smt_retry_limit, - trace_rewrites=trace_rewrites, - ) as kcfg_explore: - contract_name, method_name = _init_problem - contract = foundry.contracts[contract_name] - method = contract.method_by_name[method_name] - proof = _method_to_apr_proof( - foundry, - contract, - method, - save_directory, - kcfg_explore, - reinit=(method.qualified_name in out_of_date_methods), - simplify_init=simplify_init, - bmc_depth=bmc_depth, - ) - passed = kevm_prove( - foundry.kevm, - proof, - kcfg_explore, - save_directory=save_directory, - max_depth=max_depth, - max_iterations=max_iterations, - workers=workers, - break_every_step=break_every_step, - break_on_jumpi=break_on_jumpi, - break_on_calls=break_on_calls, - implication_every_block=implication_every_block, - bug_report=br, - kore_rpc_command=kore_rpc_command, - smt_timeout=smt_timeout, - smt_retry_limit=smt_retry_limit, - trace_rewrites=trace_rewrites, - ) - failure_log = None - if not passed: - failure_log = print_failure_info(proof, kcfg_explore, counterexample_info) - return passed, failure_log + with KoreServer(foundry.kevm.definition_dir, foundry.kevm.main_module, bug_report=br) as server: + with KoreClient('localhost', server.port, bug_report=br) as client: + kcfg_explore = KCFGExplore( + kprint=foundry.kevm, + kore_client=client, + kcfg_semantics=KEVMSemantics(auto_abstract_gas=auto_abstract_gas), + id=proof_id, + trace_rewrites=trace_rewrites, + ) + contract_name, method_name = _init_problem + contract = foundry.contracts[contract_name] + method = contract.method_by_name[method_name] + proof = _method_to_apr_proof( + foundry, + contract, + method, + save_directory, + kcfg_explore, + reinit=(method.qualified_name in out_of_date_methods), + simplify_init=simplify_init, + bmc_depth=bmc_depth, + ) + + passed = kevm_prove( + foundry.kevm, + proof, + kcfg_explore, + save_directory=save_directory, + max_depth=max_depth, + max_iterations=max_iterations, + workers=workers, + break_every_step=break_every_step, + break_on_jumpi=break_on_jumpi, + break_on_calls=break_on_calls, + implication_every_block=implication_every_block, + bug_report=br, + kore_rpc_command=kore_rpc_command, + smt_timeout=smt_timeout, + smt_retry_limit=smt_retry_limit, + trace_rewrites=trace_rewrites, + ) + failure_log = None + if not passed: + failure_log = print_failure_info(proof, kcfg_explore, counterexample_info) + return passed, failure_log def run_cfg_group(tests: list[str]) -> dict[str, tuple[bool, list[str] | None]]: init_problems = [tuple(test.split('.')) for test in tests] @@ -635,9 +633,13 @@ def _short_info(cterm: CTerm) -> Iterable[str]: ) if failure_info: - with KCFGExplore(foundry.kevm, kcfg_semantics=KEVMSemantics(), id=proof.id) as kcfg_explore: - res_lines += print_failure_info(proof, kcfg_explore, counterexample_info) - res_lines += Foundry.help_info() + with KoreServer(foundry.kevm.definition_dir, foundry.kevm.main_module) as server: + with KoreClient('localhost', server.port) as client: + kcfg_explore = KCFGExplore( + kprint=foundry.kevm, kore_client=client, kcfg_semantics=KEVMSemantics(), id=proof.id + ) + res_lines += print_failure_info(proof, kcfg_explore, counterexample_info) + res_lines += Foundry.help_info() return '\n'.join(res_lines) @@ -708,16 +710,16 @@ def foundry_simplify_node( proof_digest = foundry.proof_digest(contract_name, test_name) apr_proof = APRProof.read_proof_data(apr_proofs_dir, proof_digest) cterm = apr_proof.kcfg.node(node).cterm - with KCFGExplore( - foundry.kevm, - kcfg_semantics=KEVMSemantics(), - id=apr_proof.id, - bug_report=br, - smt_timeout=smt_timeout, - smt_retry_limit=smt_retry_limit, - trace_rewrites=trace_rewrites, - ) as kcfg_explore: - new_term, _ = kcfg_explore.cterm_simplify(cterm) + with KoreServer(foundry.kevm.definition_dir, foundry.kevm.main_module, bug_report=br) as server: + with KoreClient('localhost', server.port, bug_report=br) as client: + kcfg_explore = KCFGExplore( + kprint=foundry.kevm, + kore_client=client, + kcfg_semantics=KEVMSemantics(), + id=apr_proof.id, + trace_rewrites=trace_rewrites, + ) + new_term, _ = kcfg_explore.cterm_simplify(cterm) if replace: apr_proof.kcfg.replace_node(node, CTerm.from_kast(new_term)) apr_proof.write_proof_data() @@ -748,18 +750,18 @@ def foundry_step_node( contract_name, test_name = test.split('.') proof_digest = foundry.proof_digest(contract_name, test_name) apr_proof = APRProof.read_proof_data(apr_proofs_dir, proof_digest) - with KCFGExplore( - foundry.kevm, - kcfg_semantics=KEVMSemantics(), - id=apr_proof.id, - bug_report=br, - smt_timeout=smt_timeout, - smt_retry_limit=smt_retry_limit, - trace_rewrites=trace_rewrites, - ) as kcfg_explore: - for _i in range(repeat): - node = kcfg_explore.step(apr_proof.kcfg, node, apr_proof.logs, depth=depth) - apr_proof.write_proof_data() + with KoreServer(foundry.kevm.definition_dir, foundry.kevm.main_module, bug_report=br) as server: + with KoreClient('localhost', server.port, bug_report=br) as client: + kcfg_explore = KCFGExplore( + kprint=foundry.kevm, + kore_client=client, + kcfg_semantics=KEVMSemantics(), + id=apr_proof.id, + trace_rewrites=trace_rewrites, + ) + for _i in range(repeat): + node = kcfg_explore.step(apr_proof.kcfg, node, apr_proof.logs, depth=depth) + apr_proof.write_proof_data() def foundry_section_edge( @@ -780,18 +782,18 @@ def foundry_section_edge( proof_digest = foundry.proof_digest(contract_name, test_name) apr_proof = APRProof.read_proof_data(apr_proofs_dir, proof_digest) source_id, target_id = edge - with KCFGExplore( - foundry.kevm, - kcfg_semantics=KEVMSemantics(), - id=apr_proof.id, - bug_report=br, - smt_timeout=smt_timeout, - smt_retry_limit=smt_retry_limit, - trace_rewrites=trace_rewrites, - ) as kcfg_explore: - kcfg, _ = kcfg_explore.section_edge( - apr_proof.kcfg, source_id=source_id, target_id=target_id, logs=apr_proof.logs, sections=sections - ) + with KoreServer(foundry.kevm.definition_dir, foundry.kevm.main_module, bug_report=br) as server: + with KoreClient('localhost', server.port, bug_report=br) as client: + kcfg_explore = KCFGExplore( + kprint=foundry.kevm, + kore_client=client, + kcfg_semantics=KEVMSemantics(), + id=apr_proof.id, + trace_rewrites=trace_rewrites, + ) + kcfg, _ = kcfg_explore.section_edge( + apr_proof.kcfg, source_id=source_id, target_id=target_id, logs=apr_proof.logs, sections=sections + ) apr_proof.write_proof_data() @@ -823,12 +825,16 @@ def foundry_get_model( res_lines = [] - with KCFGExplore(foundry.kevm, kcfg_semantics=KEVMSemantics(), id=proof.id) as kcfg_explore: - for node_id in nodes: - res_lines.append('') - res_lines.append(f'Node id: {node_id}') - node = proof.kcfg.node(node_id) - res_lines.extend(print_model(node, kcfg_explore)) + with KoreServer(foundry.kevm.definition_dir, foundry.kevm.main_module) as server: + with KoreClient('localhost', server.port) as client: + kcfg_explore = KCFGExplore( + kprint=foundry.kevm, kore_client=client, kcfg_semantics=KEVMSemantics(), id=proof.id + ) + for node_id in nodes: + res_lines.append('') + res_lines.append(f'Node id: {node_id}') + node = proof.kcfg.node(node_id) + res_lines.extend(print_model(node, kcfg_explore)) return '\n'.join(res_lines)