From 90d913d504bc400a79690bdb15348d01614718a2 Mon Sep 17 00:00:00 2001 From: Everett Hildenbrandt Date: Mon, 15 Jan 2024 12:03:03 -0700 Subject: [PATCH] Enable generating KEVM claims from the basic blocks of Kontrol KCFGs (#262) * kontrol/{foundry,__main__}: add option to generate a list of KEVM claims from a given foundry proof * kontrol/{foundry,__main__}: add option for where to generate KEVM claim files at * kontrol/foundry: avoid duplicate hyphens in module name * kontrol/foundry: better filtering of claims that wont work in KEVM * kontrol/foundry: only include edge basic blocks, not ndbranches * kontrol/foundry: correction to how we exclude foundry claims * kontrol/foundry: do not duplicate source/target id in claim name * kontrol/foundry: also filter out rules with call_foundry helper * kontrol/foundry: filter out claims with terminal LHS too * kontrol/foundry: no commas in module names * kontrol/foundry: limit more foundry-specific klabels from being printed to kevm claims * kontrol/foundry: allow for empty claims by not generating the file * Set Version: 0.1.105 * poetry.lock: update * Set Version: 0.1.109 * Set Version: 0.1.112 * kontrol/foundry.py: simpler way to calculate new module name * kontrol/foundry: get list of productions to exclude from KEVM claims from definition directly * Set Version: 0.1.114 * kontrol/foundry: grab klabel of productions, not sentence label --------- Co-authored-by: devops --- package/version | 2 +- poetry.lock | 2 +- pyproject.toml | 2 +- src/kontrol/__init__.py | 2 +- src/kontrol/__main__.py | 18 +++++++++++ src/kontrol/foundry.py | 70 ++++++++++++++++++++++++++++++++++++++--- 6 files changed, 88 insertions(+), 8 deletions(-) diff --git a/package/version b/package/version index c21e67e65..c29f5f750 100644 --- a/package/version +++ b/package/version @@ -1 +1 @@ -0.1.113 +0.1.114 diff --git a/poetry.lock b/poetry.lock index 010fd0a63..6616c1d9a 100644 --- a/poetry.lock +++ b/poetry.lock @@ -1,4 +1,4 @@ -# This file is automatically @generated by Poetry 1.7.1 and should not be changed by hand. +# This file is automatically @generated by Poetry 1.6.1 and should not be changed by hand. [[package]] name = "attrs" diff --git a/pyproject.toml b/pyproject.toml index f8ee93c97..0116c9665 100644 --- a/pyproject.toml +++ b/pyproject.toml @@ -4,7 +4,7 @@ build-backend = "poetry.core.masonry.api" [tool.poetry] name = "kontrol" -version = "0.1.113" +version = "0.1.114" description = "Foundry integration for KEVM" authors = [ "Runtime Verification, Inc. ", diff --git a/src/kontrol/__init__.py b/src/kontrol/__init__.py index 83856c1dd..f373c1a93 100644 --- a/src/kontrol/__init__.py +++ b/src/kontrol/__init__.py @@ -5,4 +5,4 @@ if TYPE_CHECKING: from typing import Final -VERSION: Final = '0.1.113' +VERSION: Final = '0.1.114' diff --git a/src/kontrol/__main__.py b/src/kontrol/__main__.py index a83293f8e..4c6a9e95f 100644 --- a/src/kontrol/__main__.py +++ b/src/kontrol/__main__.py @@ -14,6 +14,7 @@ from pyk.kbuild.utils import KVersion, k_version from pyk.proof.reachability import APRProof from pyk.proof.tui import APRProofViewer +from pyk.utils import ensure_dir_path from . import VERSION from .cli import KontrolCLIArgs @@ -310,6 +311,8 @@ def exec_show( nodes: Iterable[NodeIdLike] = (), node_deltas: Iterable[tuple[NodeIdLike, NodeIdLike]] = (), to_module: bool = False, + to_kevm_claims: bool = False, + kevm_claim_dir: Path | None = None, minimize: bool = True, sort_collections: bool = False, omit_unstable_output: bool = False, @@ -328,6 +331,8 @@ def exec_show( nodes=nodes, node_deltas=node_deltas, to_module=to_module, + to_kevm_claims=to_kevm_claims, + kevm_claim_dir=kevm_claim_dir, minimize=minimize, omit_unstable_output=omit_unstable_output, sort_collections=sort_collections, @@ -762,6 +767,19 @@ def _parse_test_version_tuple(value: str) -> tuple[str, int | None]: action='store_true', help='Strip output that is likely to change without the contract logic changing', ) + show_args.add_argument( + '--to-kevm-claims', + dest='to_kevm_claims', + default=False, + action='store_true', + help='Generate a K module which can be run directly as KEVM claims for the given KCFG (best-effort).', + ) + show_args.add_argument( + '--kevm-claim-dir', + dest='kevm_claim_dir', + type=ensure_dir_path, + help='Path to write KEVM claim files at.', + ) command_parser.add_parser( 'to-dot', diff --git a/src/kontrol/foundry.py b/src/kontrol/foundry.py index 158d6fa19..16d2375aa 100644 --- a/src/kontrol/foundry.py +++ b/src/kontrol/foundry.py @@ -14,8 +14,10 @@ import tomlkit from kevm_pyk.kevm import KEVM, KEVMNodePrinter, KEVMSemantics from kevm_pyk.utils import byte_offset_to_lines, legacy_explore, print_failure_info, print_model -from pyk.kast.inner import KApply, KSort, KToken -from pyk.kast.manip import minimize_term +from pyk.cterm import CTerm +from pyk.kast.inner import KApply, KSort, KToken, KVariable +from pyk.kast.manip import collect, extract_lhs, minimize_term +from pyk.kast.outer import KDefinition, KFlatModule, KImport, KRequire from pyk.kcfg import KCFG from pyk.prelude.bytes import bytesToken from pyk.prelude.kbool import notBool @@ -32,7 +34,6 @@ from collections.abc import Iterable from typing import Any, Final - from pyk.cterm import CTerm from pyk.kast.inner import KInner from pyk.kcfg.kcfg import NodeIdLike from pyk.kcfg.tui import KCFGElem @@ -491,6 +492,8 @@ def foundry_show( nodes: Iterable[NodeIdLike] = (), node_deltas: Iterable[tuple[NodeIdLike, NodeIdLike]] = (), to_module: bool = False, + to_kevm_claims: bool = False, + kevm_claim_dir: Path | None = None, minimize: bool = True, sort_collections: bool = False, omit_unstable_output: bool = False, @@ -550,7 +553,66 @@ def foundry_show( res_lines += print_failure_info(proof, kcfg_explore, counterexample_info) res_lines += Foundry.help_info() - return '\n'.join(res_lines) + if to_kevm_claims: + _foundry_labels = [ + prod.klabel + for prod in foundry.kevm.definition.all_modules_dict['FOUNDRY-CHEAT-CODES'].productions + if prod.klabel is not None + ] + + def _remove_foundry_config(_cterm: CTerm) -> CTerm: + kevm_config_pattern = KApply( + '', + [ + KApply('', [KVariable('KEVM_CELL'), KVariable('CHEATCODES_CELL')]), + KVariable('GENERATEDCOUNTER_CELL'), + ], + ) + kevm_config_match = kevm_config_pattern.match(_cterm.config) + if kevm_config_match is None: + _LOGGER.warning('Unable to match on cell.') + return _cterm + return CTerm(kevm_config_match['KEVM_CELL'], _cterm.constraints) + + def _contains_foundry_klabel(_kast: KInner) -> bool: + _contains = False + + def _collect_klabel(_k: KInner) -> None: + nonlocal _contains + if type(_k) is KApply and _k.label.name in _foundry_labels: + _contains = True + + collect(_collect_klabel, _kast) + return _contains + + for node in proof.kcfg.nodes: + proof.kcfg.replace_node(node.id, _remove_foundry_config(node.cterm)) + + # Due to bug in KCFG.replace_node: https://github.com/runtimeverification/pyk/issues/686 + proof.kcfg = KCFG.from_dict(proof.kcfg.to_dict()) + + claims = [edge.to_rule('BASIC-BLOCK', claim=True) for edge in proof.kcfg.edges()] + claims = [claim for claim in claims if not _contains_foundry_klabel(claim.body)] + claims = [ + claim for claim in claims if not KEVMSemantics().is_terminal(CTerm.from_kast(extract_lhs(claim.body))) + ] + if len(claims) == 0: + _LOGGER.warning(f'No claims retained for proof {proof.id}') + + else: + module_name = re.sub(r'[%().:,]+', '-', proof.id.upper()) + '-SPEC' + module = KFlatModule(module_name, sentences=claims, imports=[KImport('VERIFICATION')]) + defn = KDefinition(module_name, [module], requires=[KRequire('verification.k')]) + + defn_lines = foundry.kevm.pretty_print(defn, in_module='EVM').split('\n') + + res_lines += defn_lines + + if kevm_claim_dir is not None: + kevm_claims_file = kevm_claim_dir / (module_name.lower() + '.k') + kevm_claims_file.write_text('\n'.join(line.rstrip() for line in defn_lines)) + + return '\n'.join([line.rstrip() for line in res_lines]) def foundry_to_dot(foundry: Foundry, test: str, version: int | None = None) -> None: