From 9d6dbd303a3617a8b7df7ddea4ca6aac5712fdf0 Mon Sep 17 00:00:00 2001 From: Everett Hildenbrandt Date: Tue, 26 Sep 2023 02:03:13 -0600 Subject: [PATCH] Pull in changes to KEVM since project creation (#43) * src/{kontrol,tests}: import changes in KEVM since last import * Set Version: 0.1.4 * src/tests/integratiion/test_foundry_prove: bring back upped recursion limit * src/tests/unit/test_solc_to_k: add unit test harness * .github/test-pr: disable failing if any in matrix fails * .github/test-pr: build haskell backend too * Set Version: 0.1.5 * kontrol/cli: update to latest KEVM foundry_test_args * Set Version: 0.1.7 --------- Co-authored-by: devops --- .github/workflows/test-pr.yml | 4 +- package/version | 2 +- pyproject.toml | 2 +- src/kontrol/__main__.py | 57 +- src/kontrol/cli.py | 2 +- src/kontrol/foundry.py | 314 +++--- src/kontrol/solc_to_k.py | 6 +- .../integration/test-data/examples/ERC20.sol | 94 ++ .../integration/test-data/examples/ERC721.sol | 982 ++++++++++++++++++ .../integration/test-data/examples/Empty.sol | 4 + .../test-data/examples/Storage.sol | 98 ++ src/tests/integration/test_foundry_prove.py | 6 +- src/tests/unit/test_solc_to_k.py | 65 ++ 13 files changed, 1424 insertions(+), 212 deletions(-) create mode 100644 src/tests/integration/test-data/examples/ERC20.sol create mode 100644 src/tests/integration/test-data/examples/ERC721.sol create mode 100644 src/tests/integration/test-data/examples/Empty.sol create mode 100644 src/tests/integration/test-data/examples/Storage.sol create mode 100644 src/tests/unit/test_solc_to_k.py diff --git a/.github/workflows/test-pr.yml b/.github/workflows/test-pr.yml index 17c0645e6..814793e5d 100644 --- a/.github/workflows/test-pr.yml +++ b/.github/workflows/test-pr.yml @@ -63,6 +63,7 @@ jobs: name: 'Profiling' runs-on: [self-hosted, linux, normal] strategy: + fail-fast: false matrix: backend: ['legacy', 'booster'] timeout-minutes: 30 @@ -94,6 +95,7 @@ jobs: name: 'Integration Tests' runs-on: [self-hosted, linux, normal] strategy: + fail-fast: false matrix: backend: ['legacy', 'booster'] timeout-minutes: 240 @@ -109,7 +111,7 @@ jobs: - name: 'Build KEVM' run: | docker exec -u github-user kontrol-ci-integration-${GITHUB_SHA} /bin/bash -c 'poetry install' - docker exec -u github-user kontrol-ci-integration-${GITHUB_SHA} /bin/bash -c 'CXX=clang++-14 poetry run kevm-dist --verbose build -j`nproc` plugin foundry' + docker exec -u github-user kontrol-ci-integration-${GITHUB_SHA} /bin/bash -c 'CXX=clang++-14 poetry run kevm-dist --verbose build -j`nproc` plugin haskell foundry' - name: 'Run integration tests' run: | TEST_ARGS= diff --git a/package/version b/package/version index c946ee616..11808190d 100644 --- a/package/version +++ b/package/version @@ -1 +1 @@ -0.1.6 +0.1.7 diff --git a/pyproject.toml b/pyproject.toml index 7f58eb3a9..658e89565 100644 --- a/pyproject.toml +++ b/pyproject.toml @@ -4,7 +4,7 @@ build-backend = "poetry.core.masonry.api" [tool.poetry] name = "kontrol" -version = "0.1.6" +version = "0.1.7" description = "Foundry integration for KEVM" authors = [ "Runtime Verification, Inc. ", diff --git a/src/kontrol/__main__.py b/src/kontrol/__main__.py index baec8db25..416d422b8 100644 --- a/src/kontrol/__main__.py +++ b/src/kontrol/__main__.py @@ -1,9 +1,7 @@ from __future__ import annotations -import argparse import json import logging -import re import sys from argparse import ArgumentParser from typing import TYPE_CHECKING @@ -145,7 +143,7 @@ def exec_prove( max_depth: int = 1000, max_iterations: int | None = None, reinit: bool = False, - tests: Iterable[tuple[str, str | None]] = (), + tests: Iterable[tuple[str, int | None]] = (), exclude_tests: Iterable[str] = (), workers: int = 1, simplify_init: bool = True, @@ -218,7 +216,7 @@ def exec_prove( def exec_show( foundry_root: Path, test: str, - id: str | None, + version: int | None, nodes: Iterable[NodeIdLike] = (), node_deltas: Iterable[tuple[NodeIdLike, NodeIdLike]] = (), to_module: bool = False, @@ -234,7 +232,7 @@ def exec_show( output = foundry_show( foundry_root=foundry_root, test=test, - id=id, + version=version, nodes=nodes, node_deltas=node_deltas, to_module=to_module, @@ -249,8 +247,8 @@ def exec_show( print(output) -def exec_to_dot(foundry_root: Path, test: str, id: str | None, **kwargs: Any) -> None: - foundry_to_dot(foundry_root=foundry_root, test=test, id=id) +def exec_to_dot(foundry_root: Path, test: str, version: int | None, **kwargs: Any) -> None: + foundry_to_dot(foundry_root=foundry_root, test=test, version=version) def exec_list(foundry_root: Path, **kwargs: Any) -> None: @@ -258,9 +256,9 @@ def exec_list(foundry_root: Path, **kwargs: Any) -> None: print('\n'.join(stats)) -def exec_view_kcfg(foundry_root: Path, test: str, id: str | None, **kwargs: Any) -> None: +def exec_view_kcfg(foundry_root: Path, test: str, version: int | None, **kwargs: Any) -> None: foundry = Foundry(foundry_root) - test_id = foundry.get_test_id(test, id) + test_id = foundry.get_test_id(test, version) contract_name, _ = test_id.split('.') proof = foundry.get_apr_proof(test_id) @@ -275,14 +273,14 @@ def _custom_view(elem: KCFGElem) -> Iterable[str]: viewer.run() -def exec_remove_node(foundry_root: Path, test: str, node: NodeIdLike, id: str | None, **kwargs: Any) -> None: - foundry_remove_node(foundry_root=foundry_root, test=test, id=id, node=node) +def exec_remove_node(foundry_root: Path, test: str, node: NodeIdLike, version: int | None, **kwargs: Any) -> None: + foundry_remove_node(foundry_root=foundry_root, test=test, version=version, node=node) def exec_simplify_node( foundry_root: Path, test: str, - id: str | None, + version: int | None, node: NodeIdLike, replace: bool = False, minimize: bool = True, @@ -301,7 +299,7 @@ def exec_simplify_node( pretty_term = foundry_simplify_node( foundry_root=foundry_root, test=test, - id=id, + version=version, node=node, replace=replace, minimize=minimize, @@ -317,7 +315,7 @@ def exec_simplify_node( def exec_step_node( foundry_root: Path, test: str, - id: str | None, + version: int | None, node: NodeIdLike, repeat: int = 1, depth: int = 1, @@ -335,7 +333,7 @@ def exec_step_node( foundry_step_node( foundry_root=foundry_root, test=test, - id=id, + version=version, node=node, repeat=repeat, depth=depth, @@ -349,17 +347,17 @@ def exec_step_node( def exec_merge_nodes( foundry_root: Path, test: str, - id: str | None, + version: int | None, nodes: Iterable[NodeIdLike], **kwargs: Any, ) -> None: - foundry_merge_nodes(foundry_root=foundry_root, node_ids=nodes, test=test, id=id) + foundry_merge_nodes(foundry_root=foundry_root, node_ids=nodes, test=test, version=version) def exec_section_edge( foundry_root: Path, test: str, - id: str | None, + version: int | None, edge: tuple[str, str], sections: int = 2, replace: bool = False, @@ -377,7 +375,7 @@ def exec_section_edge( foundry_section_edge( foundry_root=foundry_root, test=test, - id=id, + version=version, edge=edge, sections=sections, replace=replace, @@ -391,7 +389,7 @@ def exec_section_edge( def exec_get_model( foundry_root: Path, test: str, - id: str | None, + version: int | None, nodes: Iterable[NodeIdLike] = (), pending: bool = False, failing: bool = False, @@ -400,7 +398,7 @@ def exec_get_model( output = foundry_get_model( foundry_root=foundry_root, test=test, - id=id, + version=version, nodes=nodes, pending=pending, failing=failing, @@ -441,15 +439,12 @@ def parse(s: str) -> list[T]: solc_to_k_args.add_argument('contract_file', type=file_path, help='Path to contract file.') solc_to_k_args.add_argument('contract_name', type=str, help='Name of contract to generate K helpers for.') - def _parse_test_id_tuple(value: str) -> tuple[str, str | None]: - pattern = r'^([^,]+)(?:,\s*(\S+))?$' - match = re.match(pattern, value) - - if match: - groups = match.groups() - return groups[0], groups[1] if groups[1] is not None else None + def _parse_test_version_tuple(value: str) -> tuple[str, int | None]: + if ':' in value: + test, version = value.split(':') + return (test, int(version)) else: - raise argparse.ArgumentTypeError("Invalid tuple format. Expected 'test, id' or 'test'") + return (value, None) build = command_parser.add_parser( 'build', @@ -494,7 +489,7 @@ def _parse_test_id_tuple(value: str) -> tuple[str, str | None]: ) prove_args.add_argument( '--test', - type=_parse_test_id_tuple, + type=_parse_test_version_tuple, dest='tests', default=[], action='append', @@ -502,7 +497,7 @@ def _parse_test_id_tuple(value: str) -> tuple[str, str | None]: ) prove_args.add_argument( '--exclude-test', - type=_parse_test_id_tuple, + type=_parse_test_version_tuple, dest='exclude_tests', default=[], action='append', diff --git a/src/kontrol/cli.py b/src/kontrol/cli.py index a39fc6aeb..4bd5f07c1 100644 --- a/src/kontrol/cli.py +++ b/src/kontrol/cli.py @@ -31,7 +31,7 @@ def foundry_args(self) -> ArgumentParser: def foundry_test_args(self) -> ArgumentParser: args = ArgumentParser(add_help=False) args.add_argument('test', type=str, help='Test to run') - args.add_argument('--id', type=str, default=None, required=False, help='ID of the test') + args.add_argument('--version', type=int, default=None, required=False, help='Version of the test to use') return args @cached_property diff --git a/src/kontrol/foundry.py b/src/kontrol/foundry.py index 7ff710203..7a8277edb 100644 --- a/src/kontrol/foundry.py +++ b/src/kontrol/foundry.py @@ -28,7 +28,7 @@ from pathos.pools import ProcessPool # type: ignore from pyk.cterm import CTerm from pyk.kast.inner import KApply, KSequence, KSort, KToken, KVariable, Subst -from pyk.kast.manip import free_vars, minimize_term +from pyk.kast.manip import flatten_label, free_vars, minimize_term, set_cell from pyk.kast.outer import KDefinition, KFlatModule, KImport, KRequire from pyk.kcfg import KCFG from pyk.prelude.bytes import bytesToken @@ -88,10 +88,6 @@ def out(self) -> Path: def proofs_dir(self) -> Path: return self.out / 'proofs' - @property - def proofs_index(self) -> Path: - return self.proofs_dir / 'index.json' - @property def digest_file(self) -> Path: return self.out / 'digest' @@ -141,10 +137,6 @@ def contracts(self) -> dict[str, Contract]: def mk_proofs_dir(self) -> None: self.proofs_dir.mkdir(exist_ok=True) - try: - self.proofs_index.open('x') - except FileExistsError: - pass def method_digest(self, contract_name: str, method_sig: str) -> str: return self.contracts[contract_name].method_by_sig[method_sig].digest @@ -154,35 +146,6 @@ def digest(self) -> str: contract_digests = [self.contracts[c].digest for c in sorted(self.contracts)] return hash_str('\n'.join(contract_digests)) - def proof_digest(self, test_id: str) -> str: - with open(self.proofs_index) as f: - content = f.read() - if content != '': - try: - return json.loads(content)[test_id]['digest'] - except KeyError: - pass - return '' - - def write_proof_digest(self, test_id: str) -> None: - contract_name, test = test_id.split('.') - if test == 'setUp()': - method_sig = test - else: - method_sig, _ = test.split(':') - if not self.proofs_index.exists(): - self.proofs_index.open('r+') - content = self.proofs_index.read_text() - if content != '': - obj = json.loads(content) - else: - obj = {} - if test_id not in content: - obj[test_id] = {} - foundry_digest = self.method_digest(contract_name, method_sig) - obj[test_id]['digest'] = foundry_digest - self.proofs_index.write_text(json.dumps(obj)) - @cached_property def llvm_dylib(self) -> Path | None: match sys.platform: @@ -204,7 +167,7 @@ def up_to_date(self) -> bool: digest_dict = json.loads(self.digest_file.read_text()) if 'foundry' not in digest_dict: digest_dict['foundry'] = '' - self.digest_file.write_text(json.dumps(digest_dict)) + self.digest_file.write_text(json.dumps(digest_dict, indent=4)) return digest_dict['foundry'] == self.digest def update_digest(self) -> None: @@ -212,7 +175,7 @@ def update_digest(self) -> None: if self.digest_file.exists(): digest_dict = json.loads(self.digest_file.read_text()) digest_dict['foundry'] = self.digest - self.digest_file.write_text(json.dumps(digest_dict)) + self.digest_file.write_text(json.dumps(digest_dict, indent=4)) _LOGGER.info(f'Updated Foundry digest file: {self.digest_file}') @@ -335,20 +298,20 @@ def unique_sig(self, test: str) -> tuple[str, str]: test_sig = self.matching_sig(test).split('.')[1] return (contract_name, test_sig) - def get_test_id(self, test: str, id: str | None) -> str: + def get_test_id(self, test: str, id: int | None) -> str: matching_proofs = self.proofs_with_test(test) if not matching_proofs: raise ValueError(f'Found no matching proofs for {test}.') if id is None: if len(matching_proofs) > 1: raise ValueError( - f'Found {len(matching_proofs)} matching proofs for {test}. Use the --id flag to choose one.' + f'Found {len(matching_proofs)} matching proofs for {test}. Use the --version flag to choose one.' ) test_id = single(matching_proofs).id return test_id else: for proof in matching_proofs: - if proof.id.endswith(id): + if proof.id.endswith(str(id)): return proof.id raise ValueError('No proof matching this predicate.') @@ -419,15 +382,6 @@ def proofs_with_test(self, test: str) -> list[Proof]: ] return [proof for proof in proofs if proof is not None] - def up_to_date_proofs(self, test: str) -> list[Proof]: - contract_name, method_sig = test.split('.') - matching_proofs = self.proofs_with_test(test) - return [ - proof - for proof in matching_proofs - if self.proof_digest(proof.id) == self.method_digest(contract_name, method_sig) - ] - def get_apr_proof(self, test_id: str) -> APRProof: proof = Proof.read_proof_data(self.proofs_dir, test_id) if not isinstance(proof, APRProof): @@ -448,38 +402,76 @@ def get_optional_proof(self, test_id: str) -> Proof | None: return Proof.read_proof_data(self.proofs_dir, test_id) return None - def free_proof_id( + def get_method(self, test: str) -> Contract.Method: + contract_name, method_name = test.split('.') + contract = self.contracts[contract_name] + return contract.method_by_sig[method_name] + + def resolve_proof_version( + self, + test: str, + reinit: bool, + user_specified_version: int | None, + ) -> int: + method = self.get_method(test) + + if reinit and user_specified_version is not None: + raise ValueError('--reinit is not compatible with specifying proof versions.') + + if reinit: + _LOGGER.info(f'Creating a new version of test {test} because --reinit was specified.') + return self.free_proof_version(test) + + if user_specified_version: + _LOGGER.info(f'Using user-specified version {user_specified_version} for test {test}') + if not Proof.proof_data_exists(f'{test}:{user_specified_version}', self.proofs_dir): + raise ValueError(f'The specified version {user_specified_version} of proof {test} does not exist.') + if not method.up_to_date(self.digest_file): + _LOGGER.warn( + f'Using specified version {user_specified_version} of proof {test}, but it is out of date.' + ) + return user_specified_version + + if not method.up_to_date(self.digest_file): + _LOGGER.info(f'Creating a new version of test {test} because it is out of date.') + return self.free_proof_version(test) + + latest_version = self.latest_proof_version(test) + if latest_version is not None: + _LOGGER.info( + f'Using the the latest version {latest_version} of test {test} because it is up to date and no version was specified.' + ) + if not method.contract_up_to_date(self.digest_file): + _LOGGER.warning( + f'Test {test} was not reinitialized because it is up to date, but the contract it is a part of has changed.' + ) + return latest_version + + _LOGGER.info( + f'Test {test} is up to date in {self.digest_file}, but does not exist on disk. Assigning version 0' + ) + return 0 + + def latest_proof_version( self, test: str, - ) -> str: + ) -> int | None: + """ + find the highest used proof ID, to be used as a default. Returns None if no version of this proof exists. + """ + proof_ids = listdir(self.proofs_dir) + versions = {int(pid.split(':')[1]) for pid in proof_ids if pid.split(':')[0] == test} + return max(versions, default=None) + + def free_proof_version( + self, + test: str, + ) -> int: """ find the lowest proof id that is not used yet """ - test_ids: dict[str, set[int]] = {} - for pid in listdir(self.proofs_dir): - if pid.find(':') >= 0: - test_name, tid = pid.split(':') - if test_ids.get(test_name) is None: - ids = set() - else: - ids = test_ids[test_name] - try: - id_num = int(tid) - except ValueError: - # falls back to hex string if it fails - id_num = int(tid.encode('utf-8').hex()) - ids.add(id_num) - test_ids[test_name] = ids - if test_ids.get(test) is None: - return '0' - else: - ids = test_ids[test] - # find the first free id - i = 0 - while True: - if i not in ids: - return str(i) - i += 1 + latest_version = self.latest_proof_version(test) + return latest_version + 1 if latest_version is not None else 0 def foundry_kompile( @@ -577,7 +569,7 @@ def kompilation_up_to_date() -> bool: digest_dict = json.loads(foundry.digest_file.read_text()) if 'kompilation' not in digest_dict: digest_dict['kompilation'] = '' - foundry.digest_file.write_text(json.dumps(digest_dict)) + foundry.digest_file.write_text(json.dumps(digest_dict, indent=4)) return digest_dict['kompilation'] == kompilation_digest() def update_kompilation_digest() -> None: @@ -585,7 +577,7 @@ def update_kompilation_digest() -> None: if foundry.digest_file.exists(): digest_dict = json.loads(foundry.digest_file.read_text()) digest_dict['kompilation'] = kompilation_digest() - foundry.digest_file.write_text(json.dumps(digest_dict)) + foundry.digest_file.write_text(json.dumps(digest_dict, indent=4)) _LOGGER.info('Updated Kompilation digest') @@ -613,7 +605,7 @@ def foundry_prove( max_depth: int = 1000, max_iterations: int | None = None, reinit: bool = False, - tests: Iterable[tuple[str, str | None]] = (), + tests: Iterable[tuple[str, int | None]] = (), exclude_tests: Iterable[str] = (), workers: int = 1, simplify_init: bool = True, @@ -631,7 +623,7 @@ def foundry_prove( trace_rewrites: bool = False, auto_abstract_gas: bool = False, port: int | None = None, -) -> dict[tuple[str, str | None], tuple[bool, list[str] | None]]: +) -> dict[tuple[str, int], tuple[bool, list[str] | None]]: if workers <= 0: raise ValueError(f'Must have at least one worker, found: --workers {workers}') if max_iterations is not None and max_iterations < 0: @@ -654,72 +646,26 @@ def foundry_prove( if not tests: tests = [(test, None) for test in foundry.all_tests] - tests = list({(foundry.matching_sig(test), id) for test, id in tests}) + tests = list({(foundry.matching_sig(test), version) for test, version in tests}) test_names = [test[0] for test in tests] _LOGGER.info(f'Running tests: {test_names}') - setup_methods: dict[str, str] = {} contracts = set(unique({test.split('.')[0] for test in test_names})) - for contract_name in contracts: - if 'setUp' in foundry.contracts[contract_name].method_by_name: - setup_methods[contract_name] = f'{contract_name}.setUp()' - - test_methods = [ - method - for contract in foundry.contracts.values() - for method in contract.methods - if ( - f'{method.contract_name}.{method.signature}' in test_names - or (method.is_setup and method.contract_name in contracts) + + setup_methods = set( + unique( + f'{contract_name}.setUp()' + for contract_name in contracts + if 'setUp' in foundry.contracts[contract_name].method_by_name ) - ] + ) - out_of_date_methods: set[str] = set() - for method in test_methods: - if not method.up_to_date(foundry.out / 'digest') or reinit: - out_of_date_methods.add(method.signature) - _LOGGER.info(f'Method {method.signature} is out of date, so it was reinitialized') - else: - _LOGGER.info(f'Method {method.signature} not reinitialized because it is up to date') - if not method.contract_up_to_date(foundry.out / 'digest'): - _LOGGER.warning( - f'Method {method.signature} not reinitialized because digest was up to date, but the contract it is a part of has changed.' - ) - method.update_digest(foundry.out / 'digest') - - for i, (test, id) in enumerate(tests): - contract_name, method_sig = test.split('.') - foundry_digest = foundry.method_digest(contract_name, method_sig) - up_to_date_proofs = foundry.up_to_date_proofs(test) - if id is None and not reinit and len(up_to_date_proofs) > 0: - matching_proofs = foundry.proofs_with_test(test) - up_to_date_proofs = [proof for proof in matching_proofs if foundry.proof_digest(proof.id) == foundry_digest] - if len(up_to_date_proofs) > 1: - raise ValueError( - f'Found {len(up_to_date_proofs)} up to date proofs for {test}. Specify an id with "--test {test},`id`" flag to choose one.' - ) - elif len(up_to_date_proofs) == 1: - id = single(up_to_date_proofs).id.split(':')[1] - elif reinit or test in out_of_date_methods or len(up_to_date_proofs) == 0: - if id is not None: - _LOGGER.warn( - 'an id was specified but the proof has to be reinitialized so a new id will be attributed.' - ) - id = foundry.free_proof_id(test) - else: - test_id = f'{test}:{id}' - if foundry.proof_digest(test_id) != foundry_digest: - raise ValueError(f'Proof with id `{test_id}` is not up to date.') - assert id is not None - tests[i] = (test, id) - - def _init_and_run_proof(_init_problem: tuple[str, str, str | None]) -> tuple[bool, list[str] | None]: - contract_name, method_sig, id = _init_problem + def _init_and_run_proof(_init_problem: tuple[str, str, int]) -> tuple[bool, list[str] | None]: + contract_name, method_sig, version = _init_problem contract = foundry.contracts[contract_name] method = contract.method_by_sig[method_sig] - id = ':' + id if id is not None else '' - test_id = f'{contract_name}.{method_sig}{id}' + test_id = f'{contract_name}.{method_sig}:{version}' llvm_definition_dir = foundry.llvm_library if use_booster else None start_server = port is None @@ -763,13 +709,11 @@ def _init_and_run_proof(_init_problem: tuple[str, str, str | None]) -> tuple[boo failure_log = print_failure_info(proof, kcfg_explore, counterexample_info) return passed, failure_log - def run_cfg_group( - tests: list[tuple[str, str | None]] - ) -> dict[tuple[str, str | None], tuple[bool, list[str] | None]]: - def _split_test(test: tuple[str, str | None]) -> tuple[str, str, str | None]: - test_name, id = test + def run_cfg_group(tests: list[tuple[str, int]]) -> dict[tuple[str, int], tuple[bool, list[str] | None]]: + def _split_test(test: tuple[str, int]) -> tuple[str, str, int]: + test_name, version = test contract, method = test_name.split('.') - return contract, method, id + return contract, method, version init_problems = [_split_test(test) for test in tests] @@ -785,14 +729,29 @@ def _split_test(test: tuple[str, str | None]) -> tuple[str, str, str | None]: apr_proofs = dict(zip(tests, _apr_proofs, strict=True)) return apr_proofs - _LOGGER.info(f'Running setup functions in parallel: {list(setup_methods.values())}') - results = run_cfg_group([(method, None) for method in setup_methods.values()]) + tests_with_versions = [ + (test_name, foundry.resolve_proof_version(test_name, reinit, version)) for (test_name, version) in tests + ] + setup_methods_with_versions = [ + (setup_method_name, foundry.resolve_proof_version(setup_method_name, reinit, None)) + for setup_method_name in setup_methods + ] + + _LOGGER.info(f'Updating digests: {[test_name for test_name, _ in tests]}') + for test_name, _ in tests: + foundry.get_method(test_name).update_digest(foundry.digest_file) + _LOGGER.info(f'Updating digests: {setup_methods}') + for test_name in setup_methods: + foundry.get_method(test_name).update_digest(foundry.digest_file) + + _LOGGER.info(f'Running setup functions in parallel: {list(setup_methods)}') + results = run_cfg_group(setup_methods_with_versions) failed = [setup_cfg for setup_cfg, passed in results.items() if not passed] if failed: raise ValueError(f'Running setUp method failed for {len(failed)} contracts: {failed}') _LOGGER.info(f'Running test functions in parallel: {test_names}') - results = run_cfg_group(tests) + results = run_cfg_group(tests_with_versions) return results @@ -800,7 +759,7 @@ def _split_test(test: tuple[str, str | None]) -> tuple[str, str, str | None]: def foundry_show( foundry_root: Path, test: str, - id: str | None = None, + version: int | None = None, nodes: Iterable[NodeIdLike] = (), node_deltas: Iterable[tuple[NodeIdLike, NodeIdLike]] = (), to_module: bool = False, @@ -817,7 +776,7 @@ def foundry_show( ) -> str: contract_name, _ = test.split('.') foundry = Foundry(foundry_root) - test_id = foundry.get_test_id(test, id) + test_id = foundry.get_test_id(test, version) proof = foundry.get_apr_proof(test_id) if pending: @@ -865,10 +824,10 @@ def foundry_show( return '\n'.join(res_lines) -def foundry_to_dot(foundry_root: Path, test: str, id: str | None = None) -> None: +def foundry_to_dot(foundry_root: Path, test: str, version: int | None = None) -> None: foundry = Foundry(foundry_root) dump_dir = foundry.proofs_dir / 'dump' - test_id = foundry.get_test_id(test, id) + test_id = foundry.get_test_id(test, version) contract_name, _ = test.split('.') proof = foundry.get_apr_proof(test_id) @@ -900,9 +859,9 @@ def foundry_list(foundry_root: Path) -> list[str]: return lines -def foundry_remove_node(foundry_root: Path, test: str, node: NodeIdLike, id: str | None = None) -> None: +def foundry_remove_node(foundry_root: Path, test: str, node: NodeIdLike, version: int | None = None) -> None: foundry = Foundry(foundry_root) - test_id = foundry.get_test_id(test, id) + test_id = foundry.get_test_id(test, version) apr_proof = foundry.get_apr_proof(test_id) node_ids = apr_proof.prune(node) _LOGGER.info(f'Pruned nodes: {node_ids}') @@ -913,7 +872,7 @@ def foundry_simplify_node( foundry_root: Path, test: str, node: NodeIdLike, - id: str | None = None, + version: int | None = None, replace: bool = False, minimize: bool = True, sort_collections: bool = False, @@ -924,7 +883,7 @@ def foundry_simplify_node( port: int | None = None, ) -> str: foundry = Foundry(foundry_root, bug_report=bug_report) - test_id = foundry.get_test_id(test, id) + test_id = foundry.get_test_id(test, version) apr_proof = foundry.get_apr_proof(test_id) cterm = apr_proof.kcfg.node(node).cterm start_server = port is None @@ -952,7 +911,7 @@ def foundry_merge_nodes( foundry_root: Path, test: str, node_ids: Iterable[NodeIdLike], - id: str | None = None, + version: int | None = None, bug_report: BugReport | None = None, include_disjunct: bool = False, ) -> None: @@ -969,7 +928,7 @@ def check_cells_equal(cell: str, nodes: Iterable[KCFG.Node]) -> bool: return True foundry = Foundry(foundry_root, bug_report=bug_report) - test_id = foundry.get_test_id(test, id) + test_id = foundry.get_test_id(test, version) apr_proof = foundry.get_apr_proof(test_id) if len(list(node_ids)) < 2: @@ -998,7 +957,7 @@ def foundry_step_node( foundry_root: Path, test: str, node: NodeIdLike, - id: str | None = None, + version: int | None = None, repeat: int = 1, depth: int = 1, bug_report: BugReport | None = None, @@ -1013,7 +972,7 @@ def foundry_step_node( raise ValueError(f'Expected positive value for --depth, got: {depth}') foundry = Foundry(foundry_root, bug_report=bug_report) - test_id = foundry.get_test_id(test, id) + test_id = foundry.get_test_id(test, version) apr_proof = foundry.get_apr_proof(test_id) start_server = port is None @@ -1037,7 +996,7 @@ def foundry_section_edge( foundry_root: Path, test: str, edge: tuple[str, str], - id: str | None = None, + version: int | None = None, sections: int = 2, replace: bool = False, bug_report: BugReport | None = None, @@ -1047,7 +1006,7 @@ def foundry_section_edge( port: int | None = None, ) -> None: foundry = Foundry(foundry_root, bug_report=bug_report) - test_id = foundry.get_test_id(test, id) + test_id = foundry.get_test_id(test, version) apr_proof = foundry.get_apr_proof(test_id) source_id, target_id = edge start_server = port is None @@ -1072,14 +1031,14 @@ def foundry_section_edge( def foundry_get_model( foundry_root: Path, test: str, - id: str | None = None, + version: int | None = None, nodes: Iterable[NodeIdLike] = (), pending: bool = False, failing: bool = False, port: int | None = None, ) -> str: foundry = Foundry(foundry_root) - test_id = foundry.get_test_id(test, id) + test_id = foundry.get_test_id(test, version) proof = foundry.get_apr_proof(test_id) if not nodes: @@ -1176,7 +1135,8 @@ def _method_to_apr_proof( setup_digest = None if method_sig != 'setUp()' and 'setUp' in contract.method_by_name: - setup_digest = f'{contract_name}.setUp()' + latest_version = foundry.latest_proof_version(f'{contract.name}.setUp()') + setup_digest = f'{contract_name}.setUp():{latest_version}' _LOGGER.info(f'Using setUp method for test: {test_id}') empty_config = foundry.kevm.definition.empty_config(GENERATED_TOP_CELL) @@ -1198,8 +1158,6 @@ def _method_to_apr_proof( target_cterm = CTerm.from_kast(target_term) kcfg.replace_node(target_node_id, target_cterm) - foundry.write_proof_digest(test_id) - if simplify_init: _LOGGER.info(f'Simplifying KCFG for test: {test_id}') kcfg_explore.simplify(kcfg, {}) @@ -1249,8 +1207,9 @@ def _method_to_cfg( return cfg, init_node.id, target_node.id -def get_final_accounts_cell(proof_id: str, proof_dir: Path) -> tuple[KInner, Iterable[KInner]]: - print(proof_id, proof_dir) +def get_final_accounts_cell( + proof_id: str, proof_dir: Path, overwrite_code_cell: KInner | None = None +) -> tuple[KInner, Iterable[KInner]]: apr_proof = APRProof.read_proof_data(proof_dir, proof_id) target = apr_proof.kcfg.node(apr_proof.target) target_states = apr_proof.kcfg.covers(target_id=target.id) @@ -1262,6 +1221,19 @@ def get_final_accounts_cell(proof_id: str, proof_dir: Path) -> tuple[KInner, Ite raise ValueError(f'setUp() function for {apr_proof.id} branched and has {len(target_states)} target states.') cterm = single(target_states).source.cterm acct_cell = cterm.cell('ACCOUNTS_CELL') + + if overwrite_code_cell is not None: + new_accounts = [CTerm(account, []) for account in flatten_label('_AccountCellMap_', acct_cell)] + new_accounts_map = {account.cell('ACCTID_CELL'): account for account in new_accounts} + test_contract_account = new_accounts_map[Foundry.address_TEST_CONTRACT()] + + new_accounts_map[Foundry.address_TEST_CONTRACT()] = CTerm( + set_cell(test_contract_account.config, 'CODE_CELL', overwrite_code_cell), + [], + ) + + acct_cell = KEVM.accounts([account.config for account in new_accounts_map.values()]) + fvars = free_vars(acct_cell) acct_cons = constraints_for(fvars, cterm.constraints) return (acct_cell, acct_cons) @@ -1335,7 +1307,7 @@ def _init_cterm( constraints = None if init_state: - accts, constraints = get_final_accounts_cell(init_state, kcfgs_dir) + accts, constraints = get_final_accounts_cell(init_state, kcfgs_dir, overwrite_code_cell=program) init_subst['ACCOUNTS_CELL'] = accts if calldata is not None: diff --git a/src/kontrol/solc_to_k.py b/src/kontrol/solc_to_k.py index cdc8ed18e..0903067a9 100644 --- a/src/kontrol/solc_to_k.py +++ b/src/kontrol/solc_to_k.py @@ -136,7 +136,7 @@ def up_to_date(self, digest_file: Path) -> bool: digest_dict = json.loads(digest_file.read_text()) if 'methods' not in digest_dict: digest_dict['methods'] = {} - digest_file.write_text(json.dumps(digest_dict)) + digest_file.write_text(json.dumps(digest_dict, indent=4)) if self.qualified_name not in digest_dict['methods']: return False return digest_dict['methods'][self.qualified_name]['method'] == self.digest @@ -147,7 +147,7 @@ def contract_up_to_date(self, digest_file: Path) -> bool: digest_dict = json.loads(digest_file.read_text()) if 'methods' not in digest_dict: digest_dict['methods'] = {} - digest_file.write_text(json.dumps(digest_dict)) + digest_file.write_text(json.dumps(digest_dict, indent=4)) if self.qualified_name not in digest_dict['methods']: return False return digest_dict['methods'][self.qualified_name]['contract'] == self.contract_digest @@ -159,7 +159,7 @@ def update_digest(self, digest_file: Path) -> None: if 'methods' not in digest_dict: digest_dict['methods'] = {} digest_dict['methods'][self.qualified_name] = {'method': self.digest, 'contract': self.contract_digest} - digest_file.write_text(json.dumps(digest_dict)) + digest_file.write_text(json.dumps(digest_dict, indent=4)) _LOGGER.info(f'Updated method {self.qualified_name} in digest file: {digest_file}') diff --git a/src/tests/integration/test-data/examples/ERC20.sol b/src/tests/integration/test-data/examples/ERC20.sol new file mode 100644 index 000000000..f62add45a --- /dev/null +++ b/src/tests/integration/test-data/examples/ERC20.sol @@ -0,0 +1,94 @@ +// THIS IS A BUGGY ERC20 +// DO NOT USE FOR ANYTHING + +pragma solidity >=0.6.0; + +contract ERC20 { + + mapping(address => uint256) private _balances; + mapping(address => mapping(address => uint256)) private _allowances; + + uint256 private _totalSupply; + uint8 private _decimals; + string private _name; + string private _symbol; + + constructor ( + string memory name + , string memory symbol + , address initAccount + , uint256 initSupply + , uint8 decimals + ) public { + _name = name; + _symbol = symbol; + _decimals = decimals; + _mint(initAccount, initSupply); + } + + function name() public view returns (string memory) { return _name; } + function symbol() public view returns (string memory) { return _symbol; } + function decimals() public view returns (uint256) { return _decimals; } + function totalSupply() public view returns (uint256) { return _totalSupply; } + + function balanceOf(address account) external view returns (uint256) { + return _balances[account]; + } + + function transfer(address to, uint256 amount) external returns (bool) { + _transfer(msg.sender, to, amount); + return true; + } + + function allowance(address owner, address spender) external view returns (uint256) { + return _allowances[owner][spender]; + } + + function approve(address spender, uint256 amount) external returns (bool) { + _approve(msg.sender, spender, amount); + return true; + } + + function transferFrom(address from, address to, uint256 amount) external returns (bool) { + _transfer(from, to, amount); + + uint256 currentAllowance = _allowances[from][msg.sender]; + require(currentAllowance >= amount, "ERC20: transfer amount exceeds allowance"); + _approve(from, msg.sender, currentAllowance - amount); + + return true; + } + + function _transfer(address from, address to, uint256 amount) internal { + require(from != address(0), "ERC20: transfer from the zero address"); + require(to != address(0), "ERC20: transfer to the zero address"); + uint256 toBalance = _balances[to]; + uint256 fromBalance = _balances[from]; + require(fromBalance >= amount, "ERC20: transfer amount exceeds balance"); + uint256 fromBalanceUpdated = fromBalance - amount; + uint256 toBalanceUpdated = toBalance + amount; + _balances[from] = fromBalanceUpdated; + _balances[to] = toBalanceUpdated; + } + + function _approve(address owner, address spender, uint256 amount) internal { + require(owner != address(0), "ERC20: approve from the zero address"); + require(spender != address(0), "ERC20: approve to the zero address"); + + _allowances[owner][spender] = amount; + } + + function _mint(address account, uint256 amount) internal { + require(account != address(0), "ERC20: mint to the zero address"); + require(_totalSupply <= _totalSupply + amount);//check overflow on totalSupply + _totalSupply = _totalSupply + amount; + _balances[account] = _balances[account] + amount; + } + + function _burn(address account, uint256 amount) internal { + require(account != address(0), "ERC20: burn from the zero address"); + require(_balances[account] >= _balances[account] - amount);//check underflow on balances + _totalSupply = _totalSupply - amount; + _balances[account] = _balances[account] - amount; + } +} diff --git a/src/tests/integration/test-data/examples/ERC721.sol b/src/tests/integration/test-data/examples/ERC721.sol new file mode 100644 index 000000000..d3ec55f9d --- /dev/null +++ b/src/tests/integration/test-data/examples/ERC721.sol @@ -0,0 +1,982 @@ +// SPDX-License-Identifier: MIT + +pragma solidity ^0.8.0; + +// OpenZeppelin Contracts v4.4.1 (utils/Address.sol) + +/** + * @dev Collection of functions related to the address type + */ +library Address { + /** + * @dev Returns true if `account` is a contract. + * + * [IMPORTANT] + * ==== + * It is unsafe to assume that an address for which this function returns + * false is an externally-owned account (EOA) and not a contract. + * + * Among others, `isContract` will return false for the following + * types of addresses: + * + * - an externally-owned account + * - a contract in construction + * - an address where a contract will be created + * - an address where a contract lived, but was destroyed + * ==== + * + * [IMPORTANT] + * ==== + * You shouldn't rely on `isContract` to protect against flash loan attacks! + * + * Preventing calls from contracts is highly discouraged. It breaks composability, breaks support for smart wallets + * like Gnosis Safe, and does not provide security since it can be circumvented by calling from a contract + * constructor. + * ==== + */ + function isContract(address account) internal view returns (bool) { + // This method relies on extcodesize/address.code.length, which returns 0 + // for contracts in construction, since the code is only stored at the end + // of the constructor execution. + + return account.code.length > 0; + } + + /** + * @dev Replacement for Solidity's `transfer`: sends `amount` wei to + * `recipient`, forwarding all available gas and reverting on errors. + * + * https://eips.ethereum.org/EIPS/eip-1884[EIP1884] increases the gas cost + * of certain opcodes, possibly making contracts go over the 2300 gas limit + * imposed by `transfer`, making them unable to receive funds via + * `transfer`. {sendValue} removes this limitation. + * + * https://diligence.consensys.net/posts/2019/09/stop-using-soliditys-transfer-now/[Learn more]. + * + * IMPORTANT: because control is transferred to `recipient`, care must be + * taken to not create reentrancy vulnerabilities. Consider using + * {ReentrancyGuard} or the + * https://solidity.readthedocs.io/en/v0.5.11/security-considerations.html#use-the-checks-effects-interactions-pattern[checks-effects-interactions pattern]. + */ + function sendValue(address payable recipient, uint256 amount) internal { + require(address(this).balance >= amount, "Address: insufficient balance"); + + (bool success, ) = recipient.call{value: amount}(""); + require(success, "Address: unable to send value, recipient may have reverted"); + } + + /** + * @dev Performs a Solidity function call using a low level `call`. A + * plain `call` is an unsafe replacement for a function call: use this + * function instead. + * + * If `target` reverts with a revert reason, it is bubbled up by this + * function (like regular Solidity function calls). + * + * Returns the raw returned data. To convert to the expected return value, + * use https://solidity.readthedocs.io/en/latest/units-and-global-variables.html?highlight=abi.decode#abi-encoding-and-decoding-functions[`abi.decode`]. + * + * Requirements: + * + * - `target` must be a contract. + * - calling `target` with `data` must not revert. + * + * _Available since v3.1._ + */ + function functionCall(address target, bytes memory data) internal returns (bytes memory) { + return functionCall(target, data, "Address: low-level call failed"); + } + + /** + * @dev Same as {xref-Address-functionCall-address-bytes-}[`functionCall`], but with + * `errorMessage` as a fallback revert reason when `target` reverts. + * + * _Available since v3.1._ + */ + function functionCall( + address target, + bytes memory data, + string memory errorMessage + ) internal returns (bytes memory) { + return functionCallWithValue(target, data, 0, errorMessage); + } + + /** + * @dev Same as {xref-Address-functionCall-address-bytes-}[`functionCall`], + * but also transferring `value` wei to `target`. + * + * Requirements: + * + * - the calling contract must have an ETH balance of at least `value`. + * - the called Solidity function must be `payable`. + * + * _Available since v3.1._ + */ + function functionCallWithValue( + address target, + bytes memory data, + uint256 value + ) internal returns (bytes memory) { + return functionCallWithValue(target, data, value, "Address: low-level call with value failed"); + } + + /** + * @dev Same as {xref-Address-functionCallWithValue-address-bytes-uint256-}[`functionCallWithValue`], but + * with `errorMessage` as a fallback revert reason when `target` reverts. + * + * _Available since v3.1._ + */ + function functionCallWithValue( + address target, + bytes memory data, + uint256 value, + string memory errorMessage + ) internal returns (bytes memory) { + require(address(this).balance >= value, "Address: insufficient balance for call"); + require(isContract(target), "Address: call to non-contract"); + + (bool success, bytes memory returndata) = target.call{value: value}(data); + return verifyCallResult(success, returndata, errorMessage); + } + + /** + * @dev Same as {xref-Address-functionCall-address-bytes-}[`functionCall`], + * but performing a static call. + * + * _Available since v3.3._ + */ + function functionStaticCall(address target, bytes memory data) internal view returns (bytes memory) { + return functionStaticCall(target, data, "Address: low-level static call failed"); + } + + /** + * @dev Same as {xref-Address-functionCall-address-bytes-string-}[`functionCall`], + * but performing a static call. + * + * _Available since v3.3._ + */ + function functionStaticCall( + address target, + bytes memory data, + string memory errorMessage + ) internal view returns (bytes memory) { + require(isContract(target), "Address: static call to non-contract"); + + (bool success, bytes memory returndata) = target.staticcall(data); + return verifyCallResult(success, returndata, errorMessage); + } + + /** + * @dev Same as {xref-Address-functionCall-address-bytes-}[`functionCall`], + * but performing a delegate call. + * + * _Available since v3.4._ + */ + function functionDelegateCall(address target, bytes memory data) internal returns (bytes memory) { + return functionDelegateCall(target, data, "Address: low-level delegate call failed"); + } + + /** + * @dev Same as {xref-Address-functionCall-address-bytes-string-}[`functionCall`], + * but performing a delegate call. + * + * _Available since v3.4._ + */ + function functionDelegateCall( + address target, + bytes memory data, + string memory errorMessage + ) internal returns (bytes memory) { + require(isContract(target), "Address: delegate call to non-contract"); + + (bool success, bytes memory returndata) = target.delegatecall(data); + return verifyCallResult(success, returndata, errorMessage); + } + + /** + * @dev Tool to verifies that a low level call was successful, and revert if it wasn't, either by bubbling the + * revert reason using the provided one. + * + * _Available since v4.3._ + */ + function verifyCallResult( + bool success, + bytes memory returndata, + string memory errorMessage + ) internal pure returns (bytes memory) { + if (success) { + return returndata; + } else { + // Look for revert reason and bubble it up if present + if (returndata.length > 0) { + // The easiest way to bubble the revert reason is using memory via assembly + + assembly { + let returndata_size := mload(returndata) + revert(add(32, returndata), returndata_size) + } + } else { + revert(errorMessage); + } + } + } +} + +// OpenZeppelin Contracts v4.4.1 (utils/Context.sol) + +/** + * @dev Provides information about the current execution context, including the + * sender of the transaction and its data. While these are generally available + * via msg.sender and msg.data, they should not be accessed in such a direct + * manner, since when dealing with meta-transactions the account sending and + * paying for execution may not be the actual sender (as far as an application + * is concerned). + * + * This contract is only required for intermediate, library-like contracts. + */ +abstract contract Context { + function _msgSender() internal view virtual returns (address) { + return msg.sender; + } + + function _msgData() internal view virtual returns (bytes calldata) { + return msg.data; + } +} + +// OpenZeppelin Contracts v4.4.1 (utils/Strings.sol) + +/** + * @dev String operations. + */ +library Strings { + bytes16 private constant _HEX_SYMBOLS = "0123456789abcdef"; + + /** + * @dev Converts a `uint256` to its ASCII `string` decimal representation. + */ + function toString(uint256 value) internal pure returns (string memory) { + // Inspired by OraclizeAPI's implementation - MIT licence + // https://github.com/oraclize/ethereum-api/blob/b42146b063c7d6ee1358846c198246239e9360e8/oraclizeAPI_0.4.25.sol + + if (value == 0) { + return "0"; + } + uint256 temp = value; + uint256 digits; + while (temp != 0) { + digits++; + temp /= 10; + } + bytes memory buffer = new bytes(digits); + while (value != 0) { + digits -= 1; + buffer[digits] = bytes1(uint8(48 + uint256(value % 10))); + value /= 10; + } + return string(buffer); + } + + /** + * @dev Converts a `uint256` to its ASCII `string` hexadecimal representation. + */ + function toHexString(uint256 value) internal pure returns (string memory) { + if (value == 0) { + return "0x00"; + } + uint256 temp = value; + uint256 length = 0; + while (temp != 0) { + length++; + temp >>= 8; + } + return toHexString(value, length); + } + + /** + * @dev Converts a `uint256` to its ASCII `string` hexadecimal representation with fixed length. + */ + function toHexString(uint256 value, uint256 length) internal pure returns (string memory) { + bytes memory buffer = new bytes(2 * length + 2); + buffer[0] = "0"; + buffer[1] = "x"; + for (uint256 i = 2 * length + 1; i > 1; --i) { + buffer[i] = _HEX_SYMBOLS[value & 0xf]; + value >>= 4; + } + require(value == 0, "Strings: hex length insufficient"); + return string(buffer); + } +} + +// OpenZeppelin Contracts v4.4.1 (utils/introspection/IERC165.sol) + +/** + * @dev Interface of the ERC165 standard, as defined in the + * https://eips.ethereum.org/EIPS/eip-165[EIP]. + * + * Implementers can declare support of contract interfaces, which can then be + * queried by others ({ERC165Checker}). + * + * For an implementation, see {ERC165}. + */ +interface IERC165 { + /** + * @dev Returns true if this contract implements the interface defined by + * `interfaceId`. See the corresponding + * https://eips.ethereum.org/EIPS/eip-165#how-interfaces-are-identified[EIP section] + * to learn more about how these ids are created. + * + * This function call must use less than 30 000 gas. + */ + function supportsInterface(bytes4 interfaceId) external view returns (bool); +} + +// OpenZeppelin Contracts v4.4.1 (utils/introspection/ERC165.sol) + +/** + * @dev Implementation of the {IERC165} interface. + * + * Contracts that want to implement ERC165 should inherit from this contract and override {supportsInterface} to check + * for the additional interface id that will be supported. For example: + * + * ```solidity + * function supportsInterface(bytes4 interfaceId) public view virtual override returns (bool) { + * return interfaceId == type(MyInterface).interfaceId || super.supportsInterface(interfaceId); + * } + * ``` + * + * Alternatively, {ERC165Storage} provides an easier to use but more expensive implementation. + */ +abstract contract ERC165 is IERC165 { + /** + * @dev See {IERC165-supportsInterface}. + */ + function supportsInterface(bytes4 interfaceId) public view virtual override returns (bool) { + return interfaceId == type(IERC165).interfaceId; + } +} + +// OpenZeppelin Contracts v4.4.1 (token/ERC721/IERC721.sol) + +/** + * @dev Required interface of an ERC721 compliant contract. + */ +interface IERC721 is IERC165 { + /** + * @dev Emitted when `tokenId` token is transferred from `from` to `to`. + */ + event Transfer(address indexed from, address indexed to, uint256 indexed tokenId); + + /** + * @dev Emitted when `owner` enables `approved` to manage the `tokenId` token. + */ + event Approval(address indexed owner, address indexed approved, uint256 indexed tokenId); + + /** + * @dev Emitted when `owner` enables or disables (`approved`) `operator` to manage all of its assets. + */ + event ApprovalForAll(address indexed owner, address indexed operator, bool approved); + + /** + * @dev Returns the number of tokens in ``owner``'s account. + */ + function balanceOf(address owner) external view returns (uint256 balance); + + /** + * @dev Returns the owner of the `tokenId` token. + * + * Requirements: + * + * - `tokenId` must exist. + */ + function ownerOf(uint256 tokenId) external view returns (address owner); + + /** + * @dev Safely transfers `tokenId` token from `from` to `to`, checking first that contract recipients + * are aware of the ERC721 protocol to prevent tokens from being forever locked. + * + * Requirements: + * + * - `from` cannot be the zero address. + * - `to` cannot be the zero address. + * - `tokenId` token must exist and be owned by `from`. + * - If the caller is not `from`, it must be have been allowed to move this token by either {approve} or {setApprovalForAll}. + * - If `to` refers to a smart contract, it must implement {IERC721Receiver-onERC721Received}, which is called upon a safe transfer. + * + * Emits a {Transfer} event. + */ + function safeTransferFrom( + address from, + address to, + uint256 tokenId + ) external; + + /** + * @dev Transfers `tokenId` token from `from` to `to`. + * + * WARNING: Usage of this method is discouraged, use {safeTransferFrom} whenever possible. + * + * Requirements: + * + * - `from` cannot be the zero address. + * - `to` cannot be the zero address. + * - `tokenId` token must be owned by `from`. + * - If the caller is not `from`, it must be approved to move this token by either {approve} or {setApprovalForAll}. + * + * Emits a {Transfer} event. + */ + function transferFrom( + address from, + address to, + uint256 tokenId + ) external; + + /** + * @dev Gives permission to `to` to transfer `tokenId` token to another account. + * The approval is cleared when the token is transferred. + * + * Only a single account can be approved at a time, so approving the zero address clears previous approvals. + * + * Requirements: + * + * - The caller must own the token or be an approved operator. + * - `tokenId` must exist. + * + * Emits an {Approval} event. + */ + function approve(address to, uint256 tokenId) external; + + /** + * @dev Returns the account approved for `tokenId` token. + * + * Requirements: + * + * - `tokenId` must exist. + */ + function getApproved(uint256 tokenId) external view returns (address operator); + + /** + * @dev Approve or remove `operator` as an operator for the caller. + * Operators can call {transferFrom} or {safeTransferFrom} for any token owned by the caller. + * + * Requirements: + * + * - The `operator` cannot be the caller. + * + * Emits an {ApprovalForAll} event. + */ + function setApprovalForAll(address operator, bool _approved) external; + + /** + * @dev Returns if the `operator` is allowed to manage all of the assets of `owner`. + * + * See {setApprovalForAll} + */ + function isApprovedForAll(address owner, address operator) external view returns (bool); + + /** + * @dev Safely transfers `tokenId` token from `from` to `to`. + * + * Requirements: + * + * - `from` cannot be the zero address. + * - `to` cannot be the zero address. + * - `tokenId` token must exist and be owned by `from`. + * - If the caller is not `from`, it must be approved to move this token by either {approve} or {setApprovalForAll}. + * - If `to` refers to a smart contract, it must implement {IERC721Receiver-onERC721Received}, which is called upon a safe transfer. + * + * Emits a {Transfer} event. + */ + function safeTransferFrom( + address from, + address to, + uint256 tokenId, + bytes calldata data + ) external; +} + +// OpenZeppelin Contracts v4.4.1 (token/ERC721/IERC721Receiver.sol) + +/** + * @title ERC721 token receiver interface + * @dev Interface for any contract that wants to support safeTransfers + * from ERC721 asset contracts. + */ +interface IERC721Receiver { + /** + * @dev Whenever an {IERC721} `tokenId` token is transferred to this contract via {IERC721-safeTransferFrom} + * by `operator` from `from`, this function is called. + * + * It must return its Solidity selector to confirm the token transfer. + * If any other value is returned or the interface is not implemented by the recipient, the transfer will be reverted. + * + * The selector can be obtained in Solidity with `IERC721.onERC721Received.selector`. + */ + function onERC721Received( + address operator, + address from, + uint256 tokenId, + bytes calldata data + ) external returns (bytes4); +} + +// OpenZeppelin Contracts v4.4.1 (token/ERC721/extensions/IERC721Metadata.sol) + +/** + * @title ERC-721 Non-Fungible Token Standard, optional metadata extension + * @dev See https://eips.ethereum.org/EIPS/eip-721 + */ +interface IERC721Metadata is IERC721 { + /** + * @dev Returns the token collection name. + */ + function name() external view returns (string memory); + + /** + * @dev Returns the token collection symbol. + */ + function symbol() external view returns (string memory); + + /** + * @dev Returns the Uniform Resource Identifier (URI) for `tokenId` token. + */ + function tokenURI(uint256 tokenId) external view returns (string memory); +} + +// OpenZeppelin Contracts v4.4.1 (token/ERC721/ERC721.sol) + +/** + * @dev Implementation of https://eips.ethereum.org/EIPS/eip-721[ERC721] Non-Fungible Token Standard, including + * the Metadata extension, but not including the Enumerable extension, which is available separately as + * {ERC721Enumerable}. + */ +contract ERC721 is Context, ERC165, IERC721, IERC721Metadata { + using Address for address; + using Strings for uint256; + + // Token name + string private _name; + + // Token symbol + string private _symbol; + + // Mapping from token ID to owner address + mapping(uint256 => address) private _owners; + + // Mapping owner address to token count + mapping(address => uint256) private _balances; + + // Mapping from token ID to approved address + mapping(uint256 => address) private _tokenApprovals; + + // Mapping from owner to operator approvals + mapping(address => mapping(address => bool)) private _operatorApprovals; + + /** + * @dev Initializes the contract by setting a `name` and a `symbol` to the token collection. + */ + constructor(string memory name_, string memory symbol_) { + _name = name_; + _symbol = symbol_; + } + + /** + * @dev See {IERC165-supportsInterface}. + */ + function supportsInterface(bytes4 interfaceId) public view virtual override(ERC165, IERC165) returns (bool) { + return + interfaceId == type(IERC721).interfaceId || + interfaceId == type(IERC721Metadata).interfaceId || + super.supportsInterface(interfaceId); + } + + /** + * @dev See {IERC721-balanceOf}. + */ + function balanceOf(address owner) public view virtual override returns (uint256) { + require(owner != address(0), "ERC721: balance query for the zero address"); + return _balances[owner]; + } + + /** + * @dev See {IERC721-ownerOf}. + */ + function ownerOf(uint256 tokenId) public view virtual override returns (address) { + address owner = _owners[tokenId]; + require(owner != address(0), "ERC721: owner query for nonexistent token"); + return owner; + } + + /** + * @dev See {IERC721Metadata-name}. + */ + function name() public view virtual override returns (string memory) { + return _name; + } + + /** + * @dev See {IERC721Metadata-symbol}. + */ + function symbol() public view virtual override returns (string memory) { + return _symbol; + } + + /** + * @dev See {IERC721Metadata-tokenURI}. + */ + function tokenURI(uint256 tokenId) public view virtual override returns (string memory) { + require(_exists(tokenId), "ERC721Metadata: URI query for nonexistent token"); + + string memory baseURI = _baseURI(); + return bytes(baseURI).length > 0 ? string(abi.encodePacked(baseURI, tokenId.toString())) : ""; + } + + /** + * @dev Base URI for computing {tokenURI}. If set, the resulting URI for each + * token will be the concatenation of the `baseURI` and the `tokenId`. Empty + * by default, can be overriden in child contracts. + */ + function _baseURI() internal view virtual returns (string memory) { + return ""; + } + + /** + * @dev See {IERC721-approve}. + */ + function approve(address to, uint256 tokenId) public virtual override { + address owner = ERC721.ownerOf(tokenId); + require(to != owner, "ERC721: approval to current owner"); + + require( + _msgSender() == owner || isApprovedForAll(owner, _msgSender()), + "ERC721: approve caller is not owner nor approved for all" + ); + + _approve(to, tokenId); + } + + /** + * @dev See {IERC721-getApproved}. + */ + function getApproved(uint256 tokenId) public view virtual override returns (address) { + require(_exists(tokenId), "ERC721: approved query for nonexistent token"); + + return _tokenApprovals[tokenId]; + } + + /** + * @dev See {IERC721-setApprovalForAll}. + */ + function setApprovalForAll(address operator, bool approved) public virtual override { + _setApprovalForAll(_msgSender(), operator, approved); + } + + /** + * @dev See {IERC721-isApprovedForAll}. + */ + function isApprovedForAll(address owner, address operator) public view virtual override returns (bool) { + return _operatorApprovals[owner][operator]; + } + + /** + * @dev See {IERC721-transferFrom}. + */ + function transferFrom( + address from, + address to, + uint256 tokenId + ) public virtual override { + //solhint-disable-next-line max-line-length + require(_isApprovedOrOwner(_msgSender(), tokenId), "ERC721: transfer caller is not owner nor approved"); + + _transfer(from, to, tokenId); + } + + /** + * @dev See {IERC721-safeTransferFrom}. + */ + function safeTransferFrom( + address from, + address to, + uint256 tokenId + ) public virtual override { + safeTransferFrom(from, to, tokenId, ""); + } + + /** + * @dev See {IERC721-safeTransferFrom}. + */ + function safeTransferFrom( + address from, + address to, + uint256 tokenId, + bytes memory _data + ) public virtual override { + require(_isApprovedOrOwner(_msgSender(), tokenId), "ERC721: transfer caller is not owner nor approved"); + _safeTransfer(from, to, tokenId, _data); + } + + /** + * @dev Safely transfers `tokenId` token from `from` to `to`, checking first that contract recipients + * are aware of the ERC721 protocol to prevent tokens from being forever locked. + * + * `_data` is additional data, it has no specified format and it is sent in call to `to`. + * + * This internal function is equivalent to {safeTransferFrom}, and can be used to e.g. + * implement alternative mechanisms to perform token transfer, such as signature-based. + * + * Requirements: + * + * - `from` cannot be the zero address. + * - `to` cannot be the zero address. + * - `tokenId` token must exist and be owned by `from`. + * - If `to` refers to a smart contract, it must implement {IERC721Receiver-onERC721Received}, which is called upon a safe transfer. + * + * Emits a {Transfer} event. + */ + function _safeTransfer( + address from, + address to, + uint256 tokenId, + bytes memory _data + ) internal virtual { + _transfer(from, to, tokenId); + require(_checkOnERC721Received(from, to, tokenId, _data), "ERC721: transfer to non ERC721Receiver implementer"); + } + + /** + * @dev Returns whether `tokenId` exists. + * + * Tokens can be managed by their owner or approved accounts via {approve} or {setApprovalForAll}. + * + * Tokens start existing when they are minted (`_mint`), + * and stop existing when they are burned (`_burn`). + */ + function _exists(uint256 tokenId) internal view virtual returns (bool) { + return _owners[tokenId] != address(0); + } + + /** + * @dev Returns whether `spender` is allowed to manage `tokenId`. + * + * Requirements: + * + * - `tokenId` must exist. + */ + function _isApprovedOrOwner(address spender, uint256 tokenId) internal view virtual returns (bool) { + require(_exists(tokenId), "ERC721: operator query for nonexistent token"); + address owner = ERC721.ownerOf(tokenId); + return (spender == owner || getApproved(tokenId) == spender || isApprovedForAll(owner, spender)); + } + + /** + * @dev Safely mints `tokenId` and transfers it to `to`. + * + * Requirements: + * + * - `tokenId` must not exist. + * - If `to` refers to a smart contract, it must implement {IERC721Receiver-onERC721Received}, which is called upon a safe transfer. + * + * Emits a {Transfer} event. + */ + function _safeMint(address to, uint256 tokenId) internal virtual { + _safeMint(to, tokenId, ""); + } + + /** + * @dev Same as {xref-ERC721-_safeMint-address-uint256-}[`_safeMint`], with an additional `data` parameter which is + * forwarded in {IERC721Receiver-onERC721Received} to contract recipients. + */ + function _safeMint( + address to, + uint256 tokenId, + bytes memory _data + ) internal virtual { + _mint(to, tokenId); + require( + _checkOnERC721Received(address(0), to, tokenId, _data), + "ERC721: transfer to non ERC721Receiver implementer" + ); + } + + /** + * @dev Mints `tokenId` and transfers it to `to`. + * + * WARNING: Usage of this method is discouraged, use {_safeMint} whenever possible + * + * Requirements: + * + * - `tokenId` must not exist. + * - `to` cannot be the zero address. + * + * Emits a {Transfer} event. + */ + function _mint(address to, uint256 tokenId) internal virtual { + require(to != address(0), "ERC721: mint to the zero address"); + require(!_exists(tokenId), "ERC721: token already minted"); + + _beforeTokenTransfer(address(0), to, tokenId); + + _balances[to] += 1; + _owners[tokenId] = to; + + emit Transfer(address(0), to, tokenId); + + _afterTokenTransfer(address(0), to, tokenId); + } + + /** + * @dev Destroys `tokenId`. + * The approval is cleared when the token is burned. + * + * Requirements: + * + * - `tokenId` must exist. + * + * Emits a {Transfer} event. + */ + function _burn(uint256 tokenId) internal virtual { + address owner = ERC721.ownerOf(tokenId); + + _beforeTokenTransfer(owner, address(0), tokenId); + + // Clear approvals + _approve(address(0), tokenId); + + _balances[owner] -= 1; + delete _owners[tokenId]; + + emit Transfer(owner, address(0), tokenId); + + _afterTokenTransfer(owner, address(0), tokenId); + } + + /** + * @dev Transfers `tokenId` from `from` to `to`. + * As opposed to {transferFrom}, this imposes no restrictions on msg.sender. + * + * Requirements: + * + * - `to` cannot be the zero address. + * - `tokenId` token must be owned by `from`. + * + * Emits a {Transfer} event. + */ + function _transfer( + address from, + address to, + uint256 tokenId + ) internal virtual { + require(ERC721.ownerOf(tokenId) == from, "ERC721: transfer from incorrect owner"); + require(to != address(0), "ERC721: transfer to the zero address"); + + _beforeTokenTransfer(from, to, tokenId); + + // Clear approvals from the previous owner + _approve(address(0), tokenId); + + _balances[from] -= 1; + _balances[to] += 1; + _owners[tokenId] = to; + + emit Transfer(from, to, tokenId); + + _afterTokenTransfer(from, to, tokenId); + } + + /** + * @dev Approve `to` to operate on `tokenId` + * + * Emits a {Approval} event. + */ + function _approve(address to, uint256 tokenId) internal virtual { + _tokenApprovals[tokenId] = to; + emit Approval(ERC721.ownerOf(tokenId), to, tokenId); + } + + /** + * @dev Approve `operator` to operate on all of `owner` tokens + * + * Emits a {ApprovalForAll} event. + */ + function _setApprovalForAll( + address owner, + address operator, + bool approved + ) internal virtual { + require(owner != operator, "ERC721: approve to caller"); + _operatorApprovals[owner][operator] = approved; + emit ApprovalForAll(owner, operator, approved); + } + + /** + * @dev Internal function to invoke {IERC721Receiver-onERC721Received} on a target address. + * The call is not executed if the target address is not a contract. + * + * @param from address representing the previous owner of the given token ID + * @param to target address that will receive the tokens + * @param tokenId uint256 ID of the token to be transferred + * @param _data bytes optional data to send along with the call + * @return bool whether the call correctly returned the expected magic value + */ + function _checkOnERC721Received( + address from, + address to, + uint256 tokenId, + bytes memory _data + ) private returns (bool) { + if (to.isContract()) { + try IERC721Receiver(to).onERC721Received(_msgSender(), from, tokenId, _data) returns (bytes4 retval) { + return retval == IERC721Receiver.onERC721Received.selector; + } catch (bytes memory reason) { + if (reason.length == 0) { + revert("ERC721: transfer to non ERC721Receiver implementer"); + } else { + assembly { + revert(add(32, reason), mload(reason)) + } + } + } + } else { + return true; + } + } + + /** + * @dev Hook that is called before any token transfer. This includes minting + * and burning. + * + * Calling conditions: + * + * - When `from` and `to` are both non-zero, ``from``'s `tokenId` will be + * transferred to `to`. + * - When `from` is zero, `tokenId` will be minted for `to`. + * - When `to` is zero, ``from``'s `tokenId` will be burned. + * - `from` and `to` are never both zero. + * + * To learn more about hooks, head to xref:ROOT:extending-contracts.adoc#using-hooks[Using Hooks]. + */ + function _beforeTokenTransfer( + address from, + address to, + uint256 tokenId + ) internal virtual {} + + /** + * @dev Hook that is called after any transfer of tokens. This includes + * minting and burning. + * + * Calling conditions: + * + * - when `from` and `to` are both non-zero. + * - `from` and `to` are never both zero. + * + * To learn more about hooks, head to xref:ROOT:extending-contracts.adoc#using-hooks[Using Hooks]. + */ + function _afterTokenTransfer( + address from, + address to, + uint256 tokenId + ) internal virtual {} +} diff --git a/src/tests/integration/test-data/examples/Empty.sol b/src/tests/integration/test-data/examples/Empty.sol new file mode 100644 index 000000000..21a769222 --- /dev/null +++ b/src/tests/integration/test-data/examples/Empty.sol @@ -0,0 +1,4 @@ +pragma solidity >=0.6.0; + +contract Empty { +} diff --git a/src/tests/integration/test-data/examples/Storage.sol b/src/tests/integration/test-data/examples/Storage.sol new file mode 100644 index 000000000..5a795bb18 --- /dev/null +++ b/src/tests/integration/test-data/examples/Storage.sol @@ -0,0 +1,98 @@ +// SPDX-License-Identifier: UNLICENSED +pragma solidity ^0.8.13; + +contract Storage { + bool public myBool; + + uint8 public myUint8; + uint16 public myUint16; + uint24 public myUint24; + uint32 public myUint32; + uint40 public myUint40; + uint48 public myUint48; + uint56 public myUint56; + uint64 public myUint64; + uint72 public myUint72; + uint80 public myUint80; + uint88 public myUint88; + uint96 public myUint96; + uint104 public myUint104; + uint112 public myUint112; + uint120 public myUint120; + uint128 public myUint128; + uint136 public myUint136; + uint144 public myUint144; + uint152 public myUint152; + uint160 public myUint160; + uint168 public myUint168; + uint176 public myUint176; + uint184 public myUint184; + uint192 public myUint192; + uint200 public myUint200; + uint208 public myUint208; + uint216 public myUint216; + uint224 public myUint224; + uint232 public myUint232; + uint240 public myUint240; + uint248 public myUint248; + uint256 public myUint256; + + int8 public myInt8; + int16 public myInt16; + int24 public myInt24; + int32 public myInt32; + int40 public myInt40; + int48 public myInt48; + int56 public myInt56; + int64 public myInt64; + int72 public myInt72; + int80 public myInt80; + int88 public myInt88; + int96 public myInt96; + int104 public myInt104; + int112 public myInt112; + int120 public myInt120; + int128 public myInt128; + int136 public myInt136; + int144 public myInt144; + int152 public myInt152; + int160 public myInt160; + int168 public myInt168; + int176 public myInt176; + int184 public myInt184; + int192 public myInt192; + int200 public myInt200; + int208 public myInt208; + int216 public myInt216; + int224 public myInt224; + int232 public myInt232; + int240 public myInt240; + int248 public myInt248; + int256 public myInt256; + + string public myString; + bytes public myBytes; + + uint128[] myUint128s; + uint64[5] myUint64s; + + struct Foo { + uint128 myUint128; + uint8[] myUint8Array; + } + + Foo myFoo; + Foo[] myFoos; + + constructor () { + myBool = true; + myUint128 = 100; + myUint256 = 200; + myString = "foo"; + } + + function setMyBool(bool newBool) public { + myBool = newBool; + } + +} diff --git a/src/tests/integration/test_foundry_prove.py b/src/tests/integration/test_foundry_prove.py index 58ef81ace..e7d2f1995 100644 --- a/src/tests/integration/test_foundry_prove.py +++ b/src/tests/integration/test_foundry_prove.py @@ -336,7 +336,7 @@ def test_foundry_remove_node( assert_pass(test, prove_res) -def assert_pass(test: str, prove_res: dict[tuple[str, str | None], tuple[bool, list[str] | None]]) -> None: +def assert_pass(test: str, prove_res: dict[tuple[str, int], tuple[bool, list[str] | None]]) -> None: id = id_for_test(test, prove_res) passed, log = prove_res[(test, id)] if not passed: @@ -344,14 +344,14 @@ def assert_pass(test: str, prove_res: dict[tuple[str, str | None], tuple[bool, l pytest.fail('\n'.join(log)) -def assert_fail(test: str, prove_res: dict[tuple[str, str | None], tuple[bool, list[str] | None]]) -> None: +def assert_fail(test: str, prove_res: dict[tuple[str, int], tuple[bool, list[str] | None]]) -> None: id = id_for_test(test, prove_res) passed, log = prove_res[test, id] assert not passed assert log -def id_for_test(test: str, prove_res: dict[tuple[str, str | None], tuple[bool, list[str] | None]]) -> str: +def id_for_test(test: str, prove_res: dict[tuple[str, int], tuple[bool, list[str] | None]]) -> int: return single(_id for _test, _id in prove_res.keys() if _test == test and _id is not None) diff --git a/src/tests/unit/test_solc_to_k.py b/src/tests/unit/test_solc_to_k.py new file mode 100644 index 000000000..1666eece8 --- /dev/null +++ b/src/tests/unit/test_solc_to_k.py @@ -0,0 +1,65 @@ +from __future__ import annotations + +from typing import TYPE_CHECKING + +import pytest +from kevm_pyk.kevm import KEVM +from pyk.kast.inner import KToken, KVariable + +from kontrol.solc_to_k import Contract, _range_predicate + +from .utils import TEST_DATA_DIR + +if TYPE_CHECKING: + from typing import Final + + from pyk.kast.inner import KInner + + +EXAMPLES_DIR: Final = TEST_DATA_DIR / 'examples' + +PREDICATE_DATA: list[tuple[str, KInner, str, KInner | None]] = [ + ('bytes4', KVariable('V0_x'), 'bytes4', KEVM.range_bytes(KToken('4', 'Int'), KVariable('V0_x'))), + ('int128', KVariable('V0_x'), 'int128', KEVM.range_sint(128, KVariable('V0_x'))), + ('int24', KVariable('V0_x'), 'int24', KEVM.range_sint(24, KVariable('V0_x'))), + ('uint24', KVariable('V0_x'), 'uint24', KEVM.range_uint(24, KVariable('V0_x'))), +] + + +@pytest.mark.parametrize( + 'test_id,term,type,expected', + PREDICATE_DATA, + ids=[test_id for test_id, *_ in PREDICATE_DATA], +) +def test_range_predicate(test_id: str, term: KInner, type: str, expected: KInner | None) -> None: + # When + ret = _range_predicate(term, type) + + # Then + assert ret == expected + + +ESCAPE_DATA: list[tuple[str, str, str, str]] = [ + ('has_underscore', 'S2K', 'My_contract', 'S2KMyZUndcontract'), + ('no_change', '', 'mycontract', 'mycontract'), + ('starts_underscore', 'S2K', '_method', 'S2KZUndmethod'), + ('with_escape', '', 'Z_', 'ZZZUnd'), + ('lower_z', '', 'z_', 'zZUnd'), + ('with_escape_no_prefix', 'S2K', 'zS2K_', 'S2KzS2KZUnd'), + ('doll', 'S2K', '$name', 'S2KZDlrname'), +] + + +@pytest.mark.parametrize('test_id,prefix,input,output', ESCAPE_DATA, ids=[test_id for test_id, *_ in ESCAPE_DATA]) +def test_escaping(test_id: str, prefix: str, input: str, output: str) -> None: + # When + escaped = Contract.escaped(input, prefix) + + # Then + assert escaped == output + + # And When + unescaped = Contract.unescaped(output, prefix) + + # Then + assert unescaped == input