From 399cb5991aff02586607e53cafcb48eccb96a349 Mon Sep 17 00:00:00 2001 From: karmacoma Date: Fri, 24 May 2024 18:09:29 -0700 Subject: [PATCH 01/19] use configargparse to process halmos.toml --- halmos.toml | 13 ++-- pyproject.toml | 1 + src/halmos/__main__.py | 39 ++++------ src/halmos/parser.py | 160 +++++++++++++++++++++++++++-------------- src/halmos/sevm.py | 1 + tests/test_fixtures.py | 6 +- tests/test_parser.py | 160 ++++++++++++++++++++++++++--------------- 7 files changed, 236 insertions(+), 144 deletions(-) diff --git a/halmos.toml b/halmos.toml index 9a923647..a55baa5c 100644 --- a/halmos.toml +++ b/halmos.toml @@ -1,9 +1,12 @@ # This is an example file for configuring the Halmos settings. # For configuration values, refer to the options listed under the 'halmos --help' command. -# You may freely use sections to categorize the settings as needed. -[settings] -depth = 4 +# for now, every setting must be under the 'global' section +[global] -[compile-settings] -array-lengths = 2 \ No newline at end of file +verbose = 3 +debug = true +statistics = true + +depth = 1_000_000 +storage-layout = 'generic' diff --git a/pyproject.toml b/pyproject.toml index 32698ce6..1d2af16e 100644 --- a/pyproject.toml +++ b/pyproject.toml @@ -22,6 +22,7 @@ classifiers = [ ] requires-python = ">=3.9" dependencies = [ + "ConfigArgParse>=1.7", "sortedcontainers>=2.4.0", "toml", "z3-solver==4.12.6.0", diff --git a/src/halmos/__main__.py b/src/halmos/__main__.py index a5d09b04..0b81607f 100644 --- a/src/halmos/__main__.py +++ b/src/halmos/__main__.py @@ -18,7 +18,7 @@ from .bytevec import Chunk, ByteVec from .calldata import Calldata -from .parser import mk_arg_parser, load_config_file, parse_config +from .parser import ConfigParser from .sevm import * from .utils import ( NamedTimer, @@ -42,8 +42,6 @@ StrModel = Dict[str, str] AnyModel = UnionType[Model, StrModel] -arg_parser = mk_arg_parser() - # Python version >=3.8.14, >=3.9.14, >=3.10.7, or >=3.11 if hasattr(sys, "set_int_max_str_digits"): sys.set_int_max_str_digits(0) @@ -929,8 +927,8 @@ def run_parallel(run_args: RunArgs) -> List[TestResult]: abi, setup_info, fun_info, - extend_args(args, parse_devdoc(setup_info.sig, run_args.contract_json)), - extend_args(args, parse_devdoc(fun_info.sig, run_args.contract_json)), + args.extend(parse_devdoc(setup_info.sig, run_args.contract_json)), + args.extend(parse_devdoc(fun_info.sig, run_args.contract_json)), libs, ) for fun_info in fun_infos @@ -949,9 +947,7 @@ def run_sequential(run_args: RunArgs) -> List[TestResult]: setup_info = extract_setup(run_args.methodIdentifiers) try: - setup_args = extend_args( - args, parse_devdoc(setup_info.sig, run_args.contract_json) - ) + setup_args = args.extend(parse_devdoc(setup_info.sig, run_args.contract_json)) setup_ex = setup( run_args.creation_hexcode, run_args.deployed_hexcode, @@ -974,9 +970,8 @@ def run_sequential(run_args: RunArgs) -> List[TestResult]: funsig.split("(")[0], funsig, run_args.methodIdentifiers[funsig] ) try: - extended_args = extend_args( - args, parse_devdoc(funsig, run_args.contract_json) - ) + extended_args = args.extend(parse_devdoc(funsig, run_args.contract_json)) + debug(extended_args.format_values()) test_result = run(setup_ex, run_args.abi, fun_info, extended_args) except Exception as err: print(f"{color_warn('[ERROR]')} {funsig}") @@ -991,15 +986,6 @@ def run_sequential(run_args: RunArgs) -> List[TestResult]: return test_results -def extend_args(args: Namespace, more_opts: str) -> Namespace: - if more_opts: - new_args = deepcopy(args) - arg_parser.parse_args(more_opts.split(), new_args) - return new_args - else: - return args - - @dataclass(frozen=True) class GenModelArgs: args: Namespace @@ -1398,14 +1384,13 @@ def _main(_args=None) -> MainResult: # command line arguments # - args = arg_parser.parse_args(_args) - - if args.config: - config = load_config_file(args.config) - args = parse_config(config, arg_parser, args, sys.argv[1:]) + config_parser = ConfigParser() + args = config_parser.parse_config(_args) + if args.debug: + debug(args.format_values()) if args.version: - print(f"Halmos {metadata.version('halmos')}") + print(f"halmos {metadata.version('halmos')}") return MainResult(0) # quick bytecode execution mode @@ -1507,7 +1492,7 @@ def on_signal(signum, frame): print(f"\nRunning {num_found} tests for {contract_path}") # support for `/// @custom:halmos` annotations - contract_args = extend_args(args, parse_natspec(natspec)) if natspec else args + contract_args = args.extend(parse_natspec(natspec)) if natspec else args run_args = RunArgs( funsigs, diff --git a/src/halmos/parser.py b/src/halmos/parser.py index 71b2cb75..09c22b60 100644 --- a/src/halmos/parser.py +++ b/src/halmos/parser.py @@ -1,17 +1,38 @@ # SPDX-License-Identifier: AGPL-3.0 -import argparse +from copy import deepcopy + +import configargparse import os -import toml -from typing import Dict, Optional +from typing import List, Optional + +# type hint for the argument parser +ArgParser = configargparse.ArgParser + +# type hint for the arguments +Args = configargparse.Namespace + + +def _mk_root_parser() -> ArgParser: + root_parser = configargparse.ArgumentParser() + root_parser.add_argument( + "--root", + metavar="DIRECTORY", + default=os.getcwd(), + ) -from .utils import warn + return root_parser -def mk_arg_parser() -> argparse.ArgumentParser: - parser = argparse.ArgumentParser( - prog="halmos", epilog="For more information, see https://github.com/a16z/halmos" +def _mk_arg_parser(config_file_provider: "ConfigFileProvider") -> ArgParser: + parser = configargparse.ArgParser( + prog="halmos", + epilog="For more information, see https://github.com/a16z/halmos", + default_config_files=config_file_provider.provide(), + config_file_parser_class=configargparse.TomlConfigParser(sections=["global"]), + add_config_file_help=True, + args_for_setting_config_path=["--config"], ) parser.add_argument( @@ -20,6 +41,7 @@ def mk_arg_parser() -> argparse.ArgumentParser: default=os.getcwd(), help="source root directory (default: current directory)", ) + parser.add_argument( "--contract", metavar="CONTRACT_NAME", @@ -115,14 +137,6 @@ def mk_arg_parser() -> argparse.ArgumentParser: "--version", action="store_true", help="print the version number" ) - parser.add_argument( - "-f", - "--config", - metavar="CONFIGURE_FILE_PATH", - type=str, - help="load the configuration from the given TOML file", - ) - # debugging options group_debug = parser.add_argument_group("Debugging options") @@ -271,51 +285,91 @@ def mk_arg_parser() -> argparse.ArgumentParser: return parser -def load_config_file(path: str) -> Optional[Dict]: - if not os.path.exists(path): - print(f"Configuration file not found: {path}") - return None +class ConfigFileProvider: + def __init__(self, config_files: Optional[List[str]] = None): + self.root_parser = _mk_root_parser() + self.config_files = config_files + + # for testing purposes + self.config_file_contents = None + + def resolve_config_files(self, args: str) -> List[str]: + if self.config_files: + return self.config_files + + # first, parse find the project root directory (containing foundry.toml) + root_args = self.root_parser.parse_known_args(args, ignore_help_args=True)[0] + + # we expect to find halmos.toml in the project root directory + self.config_files = [os.path.join(root_args.root, "halmos.toml")] + return self.config_files + + def provide(self) -> Optional[List[str]]: + return self.config_files + + +class ConfigParser: + def __init__(self, config_file_provider: ConfigFileProvider = None): + self.config_file_provider = config_file_provider or ConfigFileProvider() + + # initialized in parse_config + self.arg_parser = None + + def parse_config(self, args: str) -> "Config": + """ + Parse the configuration file and command line arguments. + + Resolves the configuration file path based on the --root argument. + """ + self.config_file_provider.resolve_config_files(args) + + # construct an argument parser that can parse the configuration file + self.arg_parser = _mk_arg_parser(self.config_file_provider) + + # parse the configuration file + command line arguments + config_file_contents = self.config_file_provider.config_file_contents + + namespace = self.arg_parser.parse_args( + args, config_file_contents=config_file_contents + ) + return Config(parser=self, args=namespace) + + def parse_args(self, args: str, base_config: Optional["Config"] = None) -> "Config": + """ + Parse command line arguments, potentially extending an existing configuration. + """ + base_namespace = deepcopy(base_config.args) if base_config else None + new_namespace = self.arg_parser.parse_args(args, namespace=base_namespace) - with open(path, "r") as f: - return toml.load(f) + if base_config.debug: + self.format_values() + return Config(parser=self, args=new_namespace) -def parse_config( - config_from_file: Dict, - parser: argparse.ArgumentParser, - args: argparse.Namespace, - commands: list[str], -) -> argparse.Namespace: - if not config_from_file: - return args + def format_values(self): + return self.arg_parser.format_values() - actions = { - action.dest: (action.type, action.option_strings) for action in parser._actions - } - for _, config_group in config_from_file.items(): - for key, value in config_group.items(): - # convert to snake_case because argparse converts hyphens to underscores - key = key.replace("-", "_") +class Config: + def __init__(self, parser: ConfigParser = None, args: Args = None): + self.parser: ConfigParser = parser if parser else ConfigParser() + self.args: Args = args if args else self.parser.parse_config - if key not in actions: - warn(f"Unknown config key: {key}") - continue + def extend(self, more_opts: str) -> "Config": + if more_opts: + new_config = self.parser.parse_args(more_opts, base_config=self) + return new_config + else: + return self - value_type, options_strings = actions[key] + def format_values(self): + return self.parser.format_values() - if any(option in commands for option in options_strings): - warn(f"Skipping config key: {key} (command line argument)") - continue + def __getattr__(self, name): + return getattr(self.args, name) - if value_type is None or isinstance(value, value_type): - # Set the value if the type is None or the type is correct - setattr(args, key, value) - else: - expected_type_name = value_type.__name__ if value_type else "Any" - warn( - f"Invalid type for {key}: {type(value).__name__}" - f" (expected {expected_type_name})" - ) + def __repr__(self) -> str: + return repr(self.args) - return args + def __str__(self) -> str: + return str(self.args) diff --git a/src/halmos/sevm.py b/src/halmos/sevm.py index 012327dd..248cfd72 100644 --- a/src/halmos/sevm.py +++ b/src/halmos/sevm.py @@ -1053,6 +1053,7 @@ def empty(cls, addr: BitVecRef, loc: BitVecRef) -> ArrayRef: @classmethod def init(cls, ex: Exec, addr: Any, loc: BitVecRef) -> None: assert_address(addr) + print(f"{addr = }") if loc.size() not in ex.storage[addr]: ex.storage[addr][loc.size()] = cls.empty(addr, loc) diff --git a/tests/test_fixtures.py b/tests/test_fixtures.py index c2c745f4..23172e40 100644 --- a/tests/test_fixtures.py +++ b/tests/test_fixtures.py @@ -1,14 +1,14 @@ import pytest +from halmos.parser import ConfigParser from halmos.sevm import SEVM - -from halmos.__main__ import arg_parser, mk_options, mk_solver +from halmos.__main__ import mk_options, mk_solver import halmos.__main__ @pytest.fixture def args(): - args = arg_parser.parse_args([]) + args = ConfigParser().parse_config("") # set the global args for the main module halmos.__main__.args = args diff --git a/tests/test_parser.py b/tests/test_parser.py index b2c3f91e..15c5b03d 100644 --- a/tests/test_parser.py +++ b/tests/test_parser.py @@ -1,75 +1,123 @@ -import argparse -from unittest.mock import mock_open, patch - +import os import pytest -from halmos.parser import load_config_file, parse_config +from halmos.parser import ConfigFileProvider, ConfigParser, Config + + +def mock_config_file_provider(config_file_contents): + # use a real object but with a non-existent file and mocked contents + provider = ConfigFileProvider(config_files=["mock_halmos.toml"]) + provider.config_file_contents = config_file_contents + return provider + + +def test_config_file_default_location_is_cwd(): + cfp = ConfigFileProvider() + + # when we don't pass the project root as an argument + cfp.resolve_config_files(args=[]) + + # then the config file should be in the default location + assert cfp.provide() == [os.path.join(os.getcwd(), "halmos.toml")] + + +def test_config_file_in_project_root(): + cfp = ConfigFileProvider() + + # when we pass the project root as an argument + args = ["--root", "/path/to/project", "--extra-args", "ignored", "--help"] + cfp.resolve_config_files(args) + + # then the config file should be in the project root + assert cfp.provide() == ["/path/to/project/halmos.toml"] + + +def test_load_config_file_not_found(): + # when we try to load a non-existent config file + cfp = ConfigFileProvider(config_files=["nonexistent.toml"]) + config_parser = ConfigParser(config_file_provider=cfp) + config = config_parser.parse_config(args="") + + # then we should get a config object with default values + assert "Config File" not in config.format_values() + + +def test_load_config_file_missing_section(): + # mock a valid config file with a missing section + cfp = mock_config_file_provider("depth = 42") + config_parser = ConfigParser(config_file_provider=cfp) + + # when we parse the config with the missing section + config = config_parser.parse_config(args="") + + # then the malformed config file does not contribute to the config object + assert "Config File" not in config.format_values() + assert config.depth != 42 + + +def test_parse_config_invalid_key(): + # mock a valid config file with an invalid key + cfp = mock_config_file_provider("[global]\ninvalid_key = 42") + config_parser = ConfigParser(config_file_provider=cfp) + + # invalid keys result in an error and exit + with pytest.raises(SystemExit) as exc_info: + config_parser.parse_config(args="") + assert exc_info.value.code == 2 + +def test_parse_config_invalid_type(): + cfp = mock_config_file_provider("[global]\ndepth = 'invalid'") + config_parser = ConfigParser(config_file_provider=cfp) -@pytest.fixture -def mock_config(): - return { - "settings": { - "depth": 4, - "array-lengths": 2, - } - } + # invalid types result in an error and exit + with pytest.raises(SystemExit) as exc_info: + config_parser.parse_config(args="") + assert exc_info.value.code == 2 -@pytest.fixture -def mock_parser(): - parser = argparse.ArgumentParser() - parser.add_argument("--depth", type=int) - parser.add_argument("--array-lengths") - return parser +def test_parse_config_success(): + # mock a valid config file + cfp = mock_config_file_provider("[global]\ndepth = 42") + config_parser = ConfigParser(config_file_provider=cfp) + # when we parse the config + config = config_parser.parse_config(args="") -@pytest.fixture -def mock_args(): - args = argparse.Namespace() - args.root = "/fake/path" - args.config = "halmos.toml" - args.depth = None - args.array_lengths = None - return args + # then we should get a config object with the correct values + assert config.depth == 42 -def test_load_config_file_not_found(monkeypatch): - monkeypatch.setattr("os.path.exists", lambda x: False) - assert load_config_file("not_exist.toml") is None +def test_parse_config_override(): + # mock a valid config file + cfp = mock_config_file_provider("[global]\ndepth = 42\nverbose = 1234") + config_parser = ConfigParser(config_file_provider=cfp) + # when we parse the config with an override + config = config_parser.parse_config(args="--depth 123456") -def test_parse_config_success(mock_config, mock_parser, mock_args): - updated_args = parse_config(mock_config, mock_parser, mock_args, []) - assert updated_args.depth == 4 - assert updated_args.array_lengths == 2 + # then we should get a config object with the overridden value + assert config.depth == 123456 + # from config file + assert config.verbose == 1234 -def test_parse_config_invalid_key(mock_parser, mock_args): - invalid_key_config = { - "settings": { - "invalid_key": "invalid", - } - } - updated_args = parse_config(invalid_key_config, mock_parser, mock_args, []) - assert not hasattr(updated_args, "invalid_key") + # from command line defaults + assert config.loop == 2 -def test_parse_config_invalid_type(mock_parser, mock_args): - invalid_type_config = { - "settings": { - "depth": "invalid", - "array-lengths": 2, - } - } - updated_args = parse_config(invalid_type_config, mock_parser, mock_args, []) - assert updated_args.depth is None - assert updated_args.array_lengths == 2 +def test_config_extend_does_not_modify_original(): + # mock a valid config file + cfp = mock_config_file_provider("[global]\ndepth = 42\nverbose = 1234") + config_parser = ConfigParser(config_file_provider=cfp) + config = config_parser.parse_config(args="") + assert config.depth == 42 + # when we extend the config + new_config = config.extend("--depth=123456") -def test_parse_config_skip_in_commands(mock_config, mock_parser, mock_args): - mock_args.depth = 5 - updated_args = parse_config(mock_config, mock_parser, mock_args, ["--depth", "5"]) + # then the new config should have the overridden value + assert new_config.depth == 123456 - assert updated_args.depth == 5 - assert updated_args.array_lengths == 2 + # and the original config should not be modified + assert config.depth == 42 From 099e9a0a4e733536741504bfcb3cc5279977d015 Mon Sep 17 00:00:00 2001 From: karmacoma Date: Fri, 24 May 2024 18:21:51 -0700 Subject: [PATCH 02/19] avoid copies of Config objects --- pyproject.toml | 2 +- src/halmos/parser.py | 31 ++++++++++++++++++++++++------- 2 files changed, 25 insertions(+), 8 deletions(-) diff --git a/pyproject.toml b/pyproject.toml index 1d2af16e..1427cc5c 100644 --- a/pyproject.toml +++ b/pyproject.toml @@ -24,7 +24,7 @@ requires-python = ">=3.9" dependencies = [ "ConfigArgParse>=1.7", "sortedcontainers>=2.4.0", - "toml", + "toml>=0.10.2", "z3-solver==4.12.6.0", ] dynamic = ["version"] diff --git a/src/halmos/parser.py b/src/halmos/parser.py index 09c22b60..16904f8a 100644 --- a/src/halmos/parser.py +++ b/src/halmos/parser.py @@ -1,7 +1,5 @@ # SPDX-License-Identifier: AGPL-3.0 -from copy import deepcopy - import configargparse import os @@ -338,22 +336,37 @@ def parse_args(self, args: str, base_config: Optional["Config"] = None) -> "Conf """ Parse command line arguments, potentially extending an existing configuration. """ - base_namespace = deepcopy(base_config.args) if base_config else None + base_namespace = configargparse.Namespace() new_namespace = self.arg_parser.parse_args(args, namespace=base_namespace) if base_config.debug: self.format_values() - return Config(parser=self, args=new_namespace) + return Config(parser=self, args=new_namespace, parent=base_config) def format_values(self): return self.arg_parser.format_values() class Config: - def __init__(self, parser: ConfigParser = None, args: Args = None): - self.parser: ConfigParser = parser if parser else ConfigParser() - self.args: Args = args if args else self.parser.parse_config + """ + A wrapper around the parsed configuration with some extras: + + - keeps a reference to its parser + - can extend itself with more options + - can format the values for debugging (shows provenance of each value) + - can access the values of the underlying namespace as attributes + - keeps track of its parent configuration, avoiding copies + + Not to be instantiated directly, use ConfigParser.parse_config instead. + """ + + def __init__( + self, parser: ConfigParser = None, args: Args = None, parent: "Config" = None + ): + self.parser = parser + self.args = args + self.parent = parent def extend(self, more_opts: str) -> "Config": if more_opts: @@ -366,6 +379,10 @@ def format_values(self): return self.parser.format_values() def __getattr__(self, name): + if not hasattr(self.args, name): + if self.parent: + return getattr(self.parent, name) + return getattr(self.args, name) def __repr__(self) -> str: From b10d5362160cb88a84220d9bde70006f2b3cff37 Mon Sep 17 00:00:00 2001 From: karmacoma Date: Fri, 24 May 2024 21:05:41 -0700 Subject: [PATCH 03/19] fix pickling issue and args.extend issue --- src/halmos/__main__.py | 9 +++++---- src/halmos/parser.py | 36 ++++++++++++++++++------------------ src/halmos/sevm.py | 1 - tests/test_parser.py | 35 +++++++++++++++++++++++++---------- 4 files changed, 48 insertions(+), 33 deletions(-) diff --git a/src/halmos/__main__.py b/src/halmos/__main__.py index 0b81607f..c2017b12 100644 --- a/src/halmos/__main__.py +++ b/src/halmos/__main__.py @@ -18,7 +18,7 @@ from .bytevec import Chunk, ByteVec from .calldata import Calldata -from .parser import ConfigParser +from .parser import get_config_parser from .sevm import * from .utils import ( NamedTimer, @@ -915,11 +915,13 @@ def run_parallel(run_args: RunArgs) -> List[TestResult]: ) setup_info = extract_setup(methodIdentifiers) + setup_config = args.extend(parse_devdoc(setup_info.sig, run_args.contract_json)) fun_infos = [ FunctionInfo(funsig.split("(")[0], funsig, methodIdentifiers[funsig]) for funsig in run_args.funsigs ] + single_run_args = [ SetupAndRunSingleArgs( creation_hexcode, @@ -927,7 +929,7 @@ def run_parallel(run_args: RunArgs) -> List[TestResult]: abi, setup_info, fun_info, - args.extend(parse_devdoc(setup_info.sig, run_args.contract_json)), + setup_config, args.extend(parse_devdoc(fun_info.sig, run_args.contract_json)), libs, ) @@ -971,7 +973,6 @@ def run_sequential(run_args: RunArgs) -> List[TestResult]: ) try: extended_args = args.extend(parse_devdoc(funsig, run_args.contract_json)) - debug(extended_args.format_values()) test_result = run(setup_ex, run_args.abi, fun_info, extended_args) except Exception as err: print(f"{color_warn('[ERROR]')} {funsig}") @@ -1384,7 +1385,7 @@ def _main(_args=None) -> MainResult: # command line arguments # - config_parser = ConfigParser() + config_parser = get_config_parser() args = config_parser.parse_config(_args) if args.debug: debug(args.format_values()) diff --git a/src/halmos/parser.py b/src/halmos/parser.py index 16904f8a..17d471f5 100644 --- a/src/halmos/parser.py +++ b/src/halmos/parser.py @@ -1,6 +1,7 @@ # SPDX-License-Identifier: AGPL-3.0 import configargparse +import copy import os from typing import List, Optional @@ -330,19 +331,19 @@ def parse_config(self, args: str) -> "Config": namespace = self.arg_parser.parse_args( args, config_file_contents=config_file_contents ) - return Config(parser=self, args=namespace) + return Config(args=namespace) def parse_args(self, args: str, base_config: Optional["Config"] = None) -> "Config": """ Parse command line arguments, potentially extending an existing configuration. """ - base_namespace = configargparse.Namespace() + base_namespace = copy.copy(base_config.args) if base_config else None new_namespace = self.arg_parser.parse_args(args, namespace=base_namespace) if base_config.debug: self.format_values() - return Config(parser=self, args=new_namespace, parent=base_config) + return Config(args=new_namespace) def format_values(self): return self.arg_parser.format_values() @@ -352,41 +353,40 @@ class Config: """ A wrapper around the parsed configuration with some extras: - - keeps a reference to its parser - can extend itself with more options - - can format the values for debugging (shows provenance of each value) - can access the values of the underlying namespace as attributes - keeps track of its parent configuration, avoiding copies Not to be instantiated directly, use ConfigParser.parse_config instead. """ - def __init__( - self, parser: ConfigParser = None, args: Args = None, parent: "Config" = None - ): - self.parser = parser + def __init__(self, args: Args = None): self.args = args - self.parent = parent def extend(self, more_opts: str) -> "Config": if more_opts: - new_config = self.parser.parse_args(more_opts, base_config=self) + new_config = config_parser.parse_args(more_opts, base_config=self) return new_config else: return self - def format_values(self): - return self.parser.format_values() - def __getattr__(self, name): - if not hasattr(self.args, name): - if self.parent: - return getattr(self.parent, name) + args = self.__dict__.get("args", None) + if name == "args": + return args - return getattr(self.args, name) + return getattr(args, name) def __repr__(self) -> str: return repr(self.args) def __str__(self) -> str: return str(self.args) + + +# global parser instance +config_parser = ConfigParser() + + +def get_config_parser() -> ConfigParser: + return config_parser diff --git a/src/halmos/sevm.py b/src/halmos/sevm.py index 248cfd72..012327dd 100644 --- a/src/halmos/sevm.py +++ b/src/halmos/sevm.py @@ -1053,7 +1053,6 @@ def empty(cls, addr: BitVecRef, loc: BitVecRef) -> ArrayRef: @classmethod def init(cls, ex: Exec, addr: Any, loc: BitVecRef) -> None: assert_address(addr) - print(f"{addr = }") if loc.size() not in ex.storage[addr]: ex.storage[addr][loc.size()] = cls.empty(addr, loc) diff --git a/tests/test_parser.py b/tests/test_parser.py index 15c5b03d..42794662 100644 --- a/tests/test_parser.py +++ b/tests/test_parser.py @@ -1,7 +1,8 @@ import os import pytest -from halmos.parser import ConfigFileProvider, ConfigParser, Config +import halmos.parser +from halmos.parser import ConfigFileProvider, ConfigParser def mock_config_file_provider(config_file_contents): @@ -11,6 +12,13 @@ def mock_config_file_provider(config_file_contents): return provider +def mock_config_parser(config_file_provider): + halmos.parser.config_parser = ConfigParser( + config_file_provider=config_file_provider + ) + return halmos.parser.get_config_parser() + + def test_config_file_default_location_is_cwd(): cfp = ConfigFileProvider() @@ -35,30 +43,30 @@ def test_config_file_in_project_root(): def test_load_config_file_not_found(): # when we try to load a non-existent config file cfp = ConfigFileProvider(config_files=["nonexistent.toml"]) - config_parser = ConfigParser(config_file_provider=cfp) + config_parser = mock_config_parser(cfp) config = config_parser.parse_config(args="") # then we should get a config object with default values - assert "Config File" not in config.format_values() + assert "Config File" not in config_parser.format_values() def test_load_config_file_missing_section(): # mock a valid config file with a missing section cfp = mock_config_file_provider("depth = 42") - config_parser = ConfigParser(config_file_provider=cfp) + config_parser = mock_config_parser(cfp) # when we parse the config with the missing section config = config_parser.parse_config(args="") # then the malformed config file does not contribute to the config object - assert "Config File" not in config.format_values() + assert "Config File" not in config_parser.format_values() assert config.depth != 42 def test_parse_config_invalid_key(): # mock a valid config file with an invalid key cfp = mock_config_file_provider("[global]\ninvalid_key = 42") - config_parser = ConfigParser(config_file_provider=cfp) + config_parser = mock_config_parser(cfp) # invalid keys result in an error and exit with pytest.raises(SystemExit) as exc_info: @@ -68,7 +76,7 @@ def test_parse_config_invalid_key(): def test_parse_config_invalid_type(): cfp = mock_config_file_provider("[global]\ndepth = 'invalid'") - config_parser = ConfigParser(config_file_provider=cfp) + config_parser = mock_config_parser(cfp) # invalid types result in an error and exit with pytest.raises(SystemExit) as exc_info: @@ -79,7 +87,7 @@ def test_parse_config_invalid_type(): def test_parse_config_success(): # mock a valid config file cfp = mock_config_file_provider("[global]\ndepth = 42") - config_parser = ConfigParser(config_file_provider=cfp) + config_parser = mock_config_parser(cfp) # when we parse the config config = config_parser.parse_config(args="") @@ -91,7 +99,7 @@ def test_parse_config_success(): def test_parse_config_override(): # mock a valid config file cfp = mock_config_file_provider("[global]\ndepth = 42\nverbose = 1234") - config_parser = ConfigParser(config_file_provider=cfp) + config_parser = mock_config_parser(cfp) # when we parse the config with an override config = config_parser.parse_config(args="--depth 123456") @@ -109,7 +117,7 @@ def test_parse_config_override(): def test_config_extend_does_not_modify_original(): # mock a valid config file cfp = mock_config_file_provider("[global]\ndepth = 42\nverbose = 1234") - config_parser = ConfigParser(config_file_provider=cfp) + config_parser = mock_config_parser(cfp) config = config_parser.parse_config(args="") assert config.depth == 42 @@ -121,3 +129,10 @@ def test_config_extend_does_not_modify_original(): # and the original config should not be modified assert config.depth == 42 + + # the base value can be accessed from the new config + assert new_config.verbose == 1234 + + # missing values raise + with pytest.raises(AttributeError): + new_config.missing From fdd74ae2567bf73588fe0abe4f965e078535f6ab Mon Sep 17 00:00:00 2001 From: karmacoma Date: Fri, 24 May 2024 21:14:03 -0700 Subject: [PATCH 04/19] fix windows ci --- tests/test_parser.py | 3 ++- 1 file changed, 2 insertions(+), 1 deletion(-) diff --git a/tests/test_parser.py b/tests/test_parser.py index 42794662..53e3112e 100644 --- a/tests/test_parser.py +++ b/tests/test_parser.py @@ -33,11 +33,12 @@ def test_config_file_in_project_root(): cfp = ConfigFileProvider() # when we pass the project root as an argument + base_path = "/path/to/project" args = ["--root", "/path/to/project", "--extra-args", "ignored", "--help"] cfp.resolve_config_files(args) # then the config file should be in the project root - assert cfp.provide() == ["/path/to/project/halmos.toml"] + assert cfp.provide() == [os.path.join(base_path, "halmos.toml")] def test_load_config_file_not_found(): From 96a15560d5e6c1215bf62b34bd729d37c42aeafe Mon Sep 17 00:00:00 2001 From: karmacoma Date: Tue, 28 May 2024 18:31:00 -0700 Subject: [PATCH 05/19] WIP --- src/halmos/__main__.py | 2 +- src/halmos/pools.py | 5 ----- 2 files changed, 1 insertion(+), 6 deletions(-) delete mode 100644 src/halmos/pools.py diff --git a/src/halmos/__main__.py b/src/halmos/__main__.py index c2017b12..8b0e92e0 100644 --- a/src/halmos/__main__.py +++ b/src/halmos/__main__.py @@ -1388,7 +1388,7 @@ def _main(_args=None) -> MainResult: config_parser = get_config_parser() args = config_parser.parse_config(_args) if args.debug: - debug(args.format_values()) + debug(config_parser.format_values()) if args.version: print(f"halmos {metadata.version('halmos')}") diff --git a/src/halmos/pools.py b/src/halmos/pools.py deleted file mode 100644 index 12d1f44f..00000000 --- a/src/halmos/pools.py +++ /dev/null @@ -1,5 +0,0 @@ -from concurrent.futures import ProcessPoolExecutor, ThreadPoolExecutor - -# defined as globals so that they can be imported from anywhere but instantiated only once -# process_pool = ProcessPoolExecutor() -# thread_pool = ThreadPoolExecutor() From 3b6b0b34d0c5b7b4bebfb3853bde15e3a9071d61 Mon Sep 17 00:00:00 2001 From: karmacoma Date: Tue, 28 May 2024 18:31:56 -0700 Subject: [PATCH 06/19] WIP --- src/halmos/config.py | 267 +++++++++++++++++++++++++++++++++++++++++++ tests/test_config.py | 72 ++++++++++++ 2 files changed, 339 insertions(+) create mode 100644 src/halmos/config.py create mode 100644 tests/test_config.py diff --git a/src/halmos/config.py b/src/halmos/config.py new file mode 100644 index 00000000..1aaa16f4 --- /dev/null +++ b/src/halmos/config.py @@ -0,0 +1,267 @@ +import argparse +import os +import toml + +from dataclasses import dataclass, field, fields, MISSING +from typing import Optional + +# common strings +help, metavar, group, choices, internal, global_default, short, countable = ( + "help", + "metavar", + "group", + "choices", + "internal", + "global_default", + "short", + "countable", +) + +# groups +debug, solver = "Debugging options", "Solver options" + +# singleton default config, access with `default_config()` +_default_config: "Config" = None + +# singleton arg parser, access with `arg_parser()` +_arg_parser: argparse.ArgumentParser = None + +# singleton toml parser, access with `toml_parser()` +_toml_parser: "TomlParser" = None + + +@dataclass(kw_only=True, frozen=True) +class Config: + """Configuration object for halmos. + + Don't instantiate this directly, since all fields have default value None. Instead, use: + + - `default_config()` to get the default configuration with the actual default values + - `with_overrides()` to create a new configuration object with some fields overridden + """ + + def __getattribute__(self, name): + """Look up values in parent object if they are not set in the current object. + + This is because we consider the current object to override its parent. + + Because of this, printing a Config object will show a "flattened/resolved" view of the configuration. + """ + + # look up value in current object + value = object.__getattribute__(self, name) + if value is not None: + return value + + # look up value in parent object + parent = object.__getattribute__(self, "config_parent") + if value is None and parent is not None: + return getattr(parent, name) + + return value + + def with_overrides(self, source: str, **overrides): + """Create a new configuration object with some fields overridden. + + Use vars(namespace) to pass in the arguments from an argparse parser or + just a dictionary with the overrides (e.g. from a toml or json file).""" + + return Config(config_parent=self, config_source=source, **overrides) + + ### Internal fields (not used to generate arg parsers) + + config_parent: "Config" = field( + repr=False, + metadata={ + internal: True, + }, + ) + + config_source: str = field( + metadata={ + internal: True, + }, + ) + + ### General options + + root: str = field( + default=None, + metadata={ + help: "Project root directory", + metavar: "PATH", + global_default: os.getcwd(), + }, + ) + + loop: int = field( + default=None, + metadata={ + help: "set loop unrolling bounds", + metavar: "MAX_BOUND", + global_default: 2, + }, + ) + + symbolic_storage: bool = field( + default=None, + metadata={ + help: "set default storage values to symbolic", + global_default: False, + }, + ) + + storage_layout: str = field( + default=None, + metadata={ + help: "storage layout file", + metavar: "FILE", + choices: ["solidity", "generic"], + global_default: "solidity", + }, + ) + + ### Debugging options + + verbose: int = field( + default=None, + metadata={ + help: "increase verbosity levels: -v, -vv, -vvv, ...", + metavar: "LEVEL", + group: debug, + global_default: 0, + short: "v", + countable: True, + }, + ) + + statistics: bool = field( + default=None, + metadata={ + help: "print statistics", + group: debug, + global_default: False, + }, + ) + + json_output: str = field( + default=None, + metadata={ + help: "output test results in JSON", + metavar: "JSON_FILE_PATH", + group: debug, + global_default: None, + }, + ) + + ### Solver options + + solver_timeout_assertion: int = field( + default=None, + metadata={ + help: "set timeout (in milliseconds) for solving assertion violation conditions; 0 means no timeout (default: 1000)", + metavar: "MILLISECONDS", + group: solver, + global_default: 1000, + }, + ) + + solver_parallel: bool = field( + default=None, + metadata={ + help: "run assertion solvers in parallel", + group: solver, + global_default: False, + }, + ) + + solver_threads: int = field( + default=None, + metadata={ + help: f"number of threads to use for assertion solving", + metavar: "N", + group: solver, + global_default: os.cpu_count() or 1, + }, + ) + + +def default_config() -> "Config": + global _default_config + if _default_config is None: + values = {} + + for field in fields(Config): + # let's skip the actual default values + # if field.default is not MISSING: + # values[field.name] = field.default + + default_value = field.metadata.get(global_default, MISSING) + if default_value != MISSING: + values[field.name] = default_value + + _default_config = Config(config_parent=None, config_source="default", **values) + + return _default_config + + +def _create_arg_parser() -> argparse.ArgumentParser: + parser = argparse.ArgumentParser( + prog="halmos", + epilog="For more information, see https://github.com/a16z/halmos", + ) + + groups = { + None: parser, + } + + # add arguments from the Config dataclass + for field_info in fields(Config): + # skip internal fields + if field_info.metadata.get(internal, False): + continue + + long_name = f"--{field_info.name.replace('_', '-')}" + names = [long_name] + + short_name = field_info.metadata.get(short, None) + if short_name: + names.append(f"-{short_name}") + + arg_help = field_info.metadata.get("help", "") + metavar = field_info.metadata.get("metavar", None) + group_name = field_info.metadata.get("group", None) + + if group_name not in groups: + groups[group_name] = parser.add_argument_group(group_name) + + group = groups[group_name] + + if field_info.type == bool: + group.add_argument(*names, help=arg_help, action="store_true", default=None) + elif field_info.metadata.get(countable, False): + group.add_argument(*names, help=arg_help, action="count") + else: + kwargs = { + "help": arg_help, + "metavar": metavar, + "type": field_info.type, + } + if choices := field_info.metadata.get("choices", None): + kwargs["choices"] = choices + group.add_argument(*names, **kwargs) + + return parser + + +def arg_parser() -> argparse.ArgumentParser: + global _arg_parser + if _arg_parser is None: + _arg_parser = _create_arg_parser() + return _arg_parser + + +if __name__ == "__main__": + parser = arg_parser() + args = parser.parse_args() + print(args) diff --git a/tests/test_config.py b/tests/test_config.py new file mode 100644 index 00000000..8e7a0101 --- /dev/null +++ b/tests/test_config.py @@ -0,0 +1,72 @@ +import argparse +import pytest + +from halmos.config import Config, default_config, arg_parser + + +@pytest.fixture +def config(): + return default_config() + + +@pytest.fixture +def parser(): + return arg_parser() + + +def test_fresh_config_has_only_None_values(): + config = Config(config_parent=None, config_source="bogus") + for field in config.__dataclass_fields__.values(): + if field.metadata.get("internal"): + continue + assert getattr(config, field.name) is None + + +def test_default_config_immutable(config): + with pytest.raises(Exception): + config.solver_threads = 42 + + +def test_unknown_keys_config_constructor_raise(): + with pytest.raises(TypeError): + Config(config_parent=None, config_source="bogus", unknown_key=42) + + +def test_unknown_keys_config_object_raise(): + config = Config(config_parent=None, config_source="bogus") + with pytest.raises(AttributeError): + config.unknown_key + + +def test_count_arg(config, parser): + args = parser.parse_args(["-vvvvvv"]) + assert args.verbose == 6 + + config_from_args = config.with_overrides(source="command-line", **vars(args)) + assert config_from_args.verbose == 6 + + +def test_choice_arg(config, parser): + # wrong choice raises + with pytest.raises(SystemExit): + parser.parse_args(["--storage-layout", "beepboop"]) + + # valid choice works + args = parser.parse_args(["--storage-layout", "generic"]) + overrides = config.with_overrides(source="command-line", **vars(args)) + assert overrides.storage_layout == "generic" + + +def test_override(config): + verbose_before = config.verbose + + override = Config(config_parent=config, config_source="override", verbose=42) + + # # the override is reflected in the new config + assert override.verbose == 42 + + # # the default config is unchanged + assert config.verbose == verbose_before + + # default values are still available in the override config + assert override.solver_threads == config.solver_threads From 9826f605e12246c8a59ba821d412ae1fe93b664f Mon Sep 17 00:00:00 2001 From: karmacoma Date: Wed, 29 May 2024 14:50:14 -0700 Subject: [PATCH 07/19] WIP --- src/halmos/config.py | 250 +++++++++++++++++++++++++++++++++---------- tests/test_config.py | 108 ++++++++++++++++++- 2 files changed, 302 insertions(+), 56 deletions(-) diff --git a/src/halmos/config.py b/src/halmos/config.py index 1aaa16f4..b469442b 100644 --- a/src/halmos/config.py +++ b/src/halmos/config.py @@ -1,9 +1,13 @@ import argparse import os +import sys import toml +from collections import OrderedDict from dataclasses import dataclass, field, fields, MISSING -from typing import Optional +from typing import Any, Dict, List, Optional, Tuple, Union as UnionType + +from .utils import warn # common strings help, metavar, group, choices, internal, global_default, short, countable = ( @@ -20,15 +24,6 @@ # groups debug, solver = "Debugging options", "Solver options" -# singleton default config, access with `default_config()` -_default_config: "Config" = None - -# singleton arg parser, access with `arg_parser()` -_arg_parser: argparse.ArgumentParser = None - -# singleton toml parser, access with `toml_parser()` -_toml_parser: "TomlParser" = None - @dataclass(kw_only=True, frozen=True) class Config: @@ -40,34 +35,6 @@ class Config: - `with_overrides()` to create a new configuration object with some fields overridden """ - def __getattribute__(self, name): - """Look up values in parent object if they are not set in the current object. - - This is because we consider the current object to override its parent. - - Because of this, printing a Config object will show a "flattened/resolved" view of the configuration. - """ - - # look up value in current object - value = object.__getattribute__(self, name) - if value is not None: - return value - - # look up value in parent object - parent = object.__getattribute__(self, "config_parent") - if value is None and parent is not None: - return getattr(parent, name) - - return value - - def with_overrides(self, source: str, **overrides): - """Create a new configuration object with some fields overridden. - - Use vars(namespace) to pass in the arguments from an argparse parser or - just a dictionary with the overrides (e.g. from a toml or json file).""" - - return Config(config_parent=self, config_source=source, **overrides) - ### Internal fields (not used to generate arg parsers) config_parent: "Config" = field( @@ -84,6 +51,19 @@ def with_overrides(self, source: str, **overrides): ) ### General options + # + # These are the fields that will be used to generate arg parsers + # We don't want them to have an actual default value, new Config() objects + # should only have None values for these fields. + # + # Constructing a Config object with the actual default values is the responsibility + # of the `default_config()` function, and it uses the `global_default` metadata field + # for that. + # + # The reason for this is that when you construct a Config object from some external + # arguments, we only want the external arguments to be set, and not the default values. + # + # We can then layer these Config objects on top of the `default_config()` root: str = field( default=None, @@ -94,6 +74,15 @@ def with_overrides(self, source: str, **overrides): }, ) + depth: int = field( + default=None, + metadata={ + help: "set the max path length", + metavar: "MAX_DEPTH", + global_default: None, + }, + ) + loop: int = field( default=None, metadata={ @@ -159,7 +148,7 @@ def with_overrides(self, source: str, **overrides): solver_timeout_assertion: int = field( default=None, metadata={ - help: "set timeout (in milliseconds) for solving assertion violation conditions; 0 means no timeout (default: 1000)", + help: "set timeout (in milliseconds) for solving assertion violation conditions; 0 means no timeout", metavar: "MILLISECONDS", group: solver, global_default: 1000, @@ -185,24 +174,155 @@ def with_overrides(self, source: str, **overrides): }, ) + ### Methods -def default_config() -> "Config": - global _default_config - if _default_config is None: + def __getattribute__(self, name): + """Look up values in parent object if they are not set in the current object. + + This is because we consider the current object to override its parent. + + Because of this, printing a Config object will show a "flattened/resolved" view of the configuration. + """ + + # look up value in current object + value = object.__getattribute__(self, name) + if value is not None: + return value + + # look up value in parent object + parent = object.__getattribute__(self, "config_parent") + if value is None and parent is not None: + return getattr(parent, name) + + return value + + def with_overrides(self, source: str, **overrides): + """Create a new configuration object with some fields overridden. + + Use vars(namespace) to pass in the arguments from an argparse parser or + just a dictionary with the overrides (e.g. from a toml or json file).""" + + return Config(config_parent=self, config_source=source, **overrides) + + def value_with_source(self, name: str) -> Tuple[Any, str]: + # look up value in current object + value = object.__getattribute__(self, name) + if value is not None: + return (value, self.config_source) + + # look up value in parent object + parent = object.__getattribute__(self, "config_parent") + if value is None and self.config_parent is not None: + return parent.value_with_source(name) + + return (value, self.config_source) + + def values_with_sources(self) -> Dict[str, Tuple[Any, str]]: + # field -> (value, source) values = {} + for field in fields(self): + if field.metadata.get(internal): + continue + values[field.name] = self.value_with_source(field.name) + return values + + def values(self): + skip_empty = self.config_parent is not None + + for field in fields(self): + if field.metadata.get(internal): + continue + + field_value = object.__getattribute__(self, field.name) + if skip_empty and field_value is None: + continue + + yield field.name, field_value + + def values_by_layer(self) -> Dict[str, Tuple[str, Any]]: + # source -> {field, value} + if self.config_parent is None: + return OrderedDict([(self.config_source, dict(self.values()))]) + + values = self.config_parent.values_by_layer() + values[self.config_source] = dict(self.values()) + return values + + def formatted_layers(self) -> str: + lines = [] + for layer, values in self.values_by_layer().items(): + lines.append(f"{layer}:") + for field, value in values.items(): + lines.append(f" {field}: {value}") + return "\n".join(lines) + + +def _mk_root_parser() -> argparse.ArgumentParser: + root_parser = argparse.ArgumentParser() + root_parser.add_argument( + "--root", + metavar="DIRECTORY", + default=os.getcwd(), + ) - for field in fields(Config): - # let's skip the actual default values - # if field.default is not MISSING: - # values[field.name] = field.default + return root_parser - default_value = field.metadata.get(global_default, MISSING) - if default_value != MISSING: - values[field.name] = default_value - _default_config = Config(config_parent=None, config_source="default", **values) +def resolve_config_files(args: UnionType[str, List[str]]) -> List[str]: + root_parser = _mk_root_parser() - return _default_config + # first, parse find the project root directory (containing foundry.toml) + # beware: errors and help flags will cause a system exit + root_args = root_parser.parse_known_args(args)[0] + + # we expect to find halmos.toml in the project root directory + config_files = [os.path.join(root_args.root, "halmos.toml")] + return config_files + + +class TomlParser: + def __init__(self): + pass + + def parse_file(self, toml_file_path: str) -> Dict: + with open(toml_file_path) as f: + return self.parse_str(f.read(), source=toml_file_path) + + # exposed for easier testing + def parse_str(self, file_contents: str, source: str = "halmos.toml") -> Dict: + parsed = toml.loads(file_contents) + return self.parse_dict(parsed, source=source) + + # exposed for easier testing + def parse_dict(self, parsed: dict, source: str = "halmos.toml") -> Dict: + if len(parsed) != 1: + warn( + f"error: expected a single `[global]` section in the toml file, " + f"got {len(parsed)}: {', '.join(parsed.keys())}" + ) + sys.exit(2) + + data = parsed.get("global", None) + if data is None: + for key in parsed.keys(): + warn( + f"error: expected a `[global]` section in the toml file, got '{key}'" + ) + sys.exit(2) + + return {k.replace("-", "_"): v for k, v in data.items()} + + +def _create_default_config() -> "Config": + values = {} + + for field in fields(Config): + # we build the default config by looking at the global_default metadata field + default_value = field.metadata.get(global_default, MISSING) + if default_value != MISSING: + values[field.name] = default_value + + return Config(config_parent=None, config_source="default", **values) def _create_arg_parser() -> argparse.ArgumentParser: @@ -254,14 +374,34 @@ def _create_arg_parser() -> argparse.ArgumentParser: return parser +def _create_toml_parser() -> TomlParser: + return TomlParser() + + +# public singleton accessors + + +def default_config() -> "Config": + return _default_config + + def arg_parser() -> argparse.ArgumentParser: - global _arg_parser - if _arg_parser is None: - _arg_parser = _create_arg_parser() return _arg_parser +def toml_parser(): + return _toml_parser + + +# init module-level singletons + +_arg_parser = _create_arg_parser() +_default_config = _create_default_config() +_toml_parser = _create_toml_parser() + + if __name__ == "__main__": parser = arg_parser() args = parser.parse_args() - print(args) + config = default_config().with_overrides(source="command-line", **vars(args)) + print(config.formatted_layers()) diff --git a/tests/test_config.py b/tests/test_config.py index 8e7a0101..c19663bd 100644 --- a/tests/test_config.py +++ b/tests/test_config.py @@ -1,7 +1,15 @@ import argparse +import os +import pickle import pytest -from halmos.config import Config, default_config, arg_parser +from halmos.config import ( + Config, + default_config, + arg_parser, + toml_parser as get_toml_parser, + resolve_config_files, +) @pytest.fixture @@ -14,6 +22,11 @@ def parser(): return arg_parser() +@pytest.fixture +def toml_parser(): + return get_toml_parser() + + def test_fresh_config_has_only_None_values(): config = Config(config_parent=None, config_source="bogus") for field in config.__dataclass_fields__.values(): @@ -70,3 +83,96 @@ def test_override(config): # default values are still available in the override config assert override.solver_threads == config.solver_threads + + +def test_toml_parser_expects_single_section(toml_parser): + # extra section + with pytest.raises(SystemExit): + toml_parser.parse_str("[global]\na = 1\n[extra]\nb = 2") + + # missing global + with pytest.raises(SystemExit): + toml_parser.parse_str("a = 1\nb = 2") + + # single section is not expected one + with pytest.raises(SystemExit): + toml_parser.parse_str("[weird]\na = 1\nb = 2") + + # works + toml_parser.parse_str("[global]") + + +def test_config_file_default_location_is_cwd(): + # when we don't pass the project root as an argument + config_files = resolve_config_files(args=[]) + + # then the config file should be in the default location + assert config_files == [os.path.join(os.getcwd(), "halmos.toml")] + + +def test_config_file_in_project_root(): + # when we pass the project root as an argument + base_path = "/path/to/project" + args = ["--root", base_path, "--extra-args", "ignored"] + config_files = resolve_config_files(args) + + # then the config file should be in the project root + assert config_files == [os.path.join(base_path, "halmos.toml")] + + +def test_config_file_invalid_key(toml_parser): + # invalid keys result in an error and exit + with pytest.raises(SystemExit) as exc_info: + toml_parser.parse_str("[global]\ninvalid_key = 42") + assert exc_info.value.code == 2 + + +# TODO: uncomment when type checking is implemented +# def test_config_file_invalid_type(toml_parser): +# # invalid types result in an error and exit +# with pytest.raises(SystemExit) as exc_info: +# config = toml_parser.parse_str("[global]\ndepth = 'invalid'") +# print(config) +# assert exc_info.value.code == 2 + + +def test_config_file_snake_case(config, toml_parser): + config_file_data = toml_parser.parse_str("[global]\nsolver-threads = 42") + assert config_file_data["solver_threads"] == 42 + + config = config.with_overrides(source="halmos.toml", **config_file_data) + assert config.solver_threads == 42 + + +def test_config_e2e(config, parser, toml_parser): + # when we apply overrides to the default config + config_file_data = toml_parser.parse_str( + "[global]\nverbose = 42\nsymbolic_storage = true" + ) + config = config.with_overrides(source="halmos.toml", **config_file_data) + + args = parser.parse_args(["-vvv"]) + config = config.with_overrides(source="command-line", **vars(args)) + + # then the config object should have the expected values + assert config.verbose == 3 + assert config.symbolic_storage == True + assert config.loop == 2 + + # and each value should have the expected source + assert config.value_with_source("verbose") == (3, "command-line") + assert config.value_with_source("symbolic_storage") == (True, "halmos.toml") + assert config.value_with_source("loop") == (2, "default") + + +def test_config_pickle(config, parser): + args = parser.parse_args(["-vvv"]) + config = config.with_overrides(source="command-line", **vars(args)) + + # pickle and unpickle the config + pickled = pickle.dumps(config) + unpickled = pickle.loads(pickled) + + # then the config object should be the same + assert config == unpickled + assert unpickled.value_with_source("verbose") == (3, "command-line") From 404b6726f4d34342b516b4152f5f75ac37d0dfe6 Mon Sep 17 00:00:00 2001 From: karmacoma Date: Wed, 29 May 2024 14:53:17 -0700 Subject: [PATCH 08/19] fix test_config_file_invalid_key --- src/halmos/config.py | 7 ++++++- tests/test_config.py | 5 +++-- 2 files changed, 9 insertions(+), 3 deletions(-) diff --git a/src/halmos/config.py b/src/halmos/config.py index b469442b..ad2949c6 100644 --- a/src/halmos/config.py +++ b/src/halmos/config.py @@ -202,7 +202,12 @@ def with_overrides(self, source: str, **overrides): Use vars(namespace) to pass in the arguments from an argparse parser or just a dictionary with the overrides (e.g. from a toml or json file).""" - return Config(config_parent=self, config_source=source, **overrides) + try: + return Config(config_parent=self, config_source=source, **overrides) + except TypeError as e: + # follow argparse error message format and behavior + warn(f"error: unrecognized argument: {str(e).split()[-1]}") + sys.exit(2) def value_with_source(self, name: str) -> Tuple[Any, str]: # look up value in current object diff --git a/tests/test_config.py b/tests/test_config.py index c19663bd..9f161185 100644 --- a/tests/test_config.py +++ b/tests/test_config.py @@ -120,10 +120,11 @@ def test_config_file_in_project_root(): assert config_files == [os.path.join(base_path, "halmos.toml")] -def test_config_file_invalid_key(toml_parser): +def test_config_file_invalid_key(config, toml_parser): # invalid keys result in an error and exit with pytest.raises(SystemExit) as exc_info: - toml_parser.parse_str("[global]\ninvalid_key = 42") + data = toml_parser.parse_str("[global]\ninvalid_key = 42") + config = config.with_overrides(source="halmos.toml", **data) assert exc_info.value.code == 2 From 58ef9e90a97a2d16dacc8039169696f28c2db187 Mon Sep 17 00:00:00 2001 From: karmacoma Date: Wed, 29 May 2024 17:02:05 -0700 Subject: [PATCH 09/19] integrate in main module --- src/halmos/__main__.py | 115 +++++++++--- src/halmos/config.py | 415 +++++++++++++++++++++++++++++------------ src/halmos/parser.py | 392 -------------------------------------- tests/test_cli.py | 3 +- tests/test_config.py | 8 +- tests/test_fixtures.py | 9 +- tests/test_parser.py | 139 -------------- 7 files changed, 382 insertions(+), 699 deletions(-) delete mode 100644 src/halmos/parser.py delete mode 100644 tests/test_parser.py diff --git a/src/halmos/__main__.py b/src/halmos/__main__.py index 8b0e92e0..933933ff 100644 --- a/src/halmos/__main__.py +++ b/src/halmos/__main__.py @@ -9,7 +9,7 @@ import time import traceback import uuid -from argparse import Namespace + from collections import Counter from concurrent.futures import ProcessPoolExecutor, ThreadPoolExecutor from dataclasses import asdict, dataclass @@ -18,7 +18,13 @@ from .bytevec import Chunk, ByteVec from .calldata import Calldata -from .parser import get_config_parser +from .config import ( + arg_parser, + default_config, + resolve_config_files, + toml_parser, + Config as HalmosConfig, +) from .sevm import * from .utils import ( NamedTimer, @@ -63,6 +69,53 @@ VERBOSITY_TRACE_CONSTRUCTOR = 5 +def with_devdoc(args: HalmosConfig, fn_sig: str, contract_json: Dict) -> HalmosConfig: + devdoc = parse_devdoc(fn_sig, contract_json) + if not devdoc: + return args + + overrides = arg_parser().parse_args(devdoc.split()) + return args.with_overrides(source=fn_sig, **vars(overrides)) + + +def with_natspec( + args: HalmosConfig, contract_name: str, contract_natspec: str +) -> HalmosConfig: + if not contract_natspec: + return args + + parsed = parse_natspec(contract_natspec) + if not parsed: + return args + + overrides = arg_parser().parse_args(parsed.split()) + return args.with_overrides(source=contract_name, **vars(overrides)) + + +def load_config(_args) -> HalmosConfig: + config = default_config() + + # parse CLI args first, so that can get `--help` out of the way and resolve `--debug` + # but don't apply the CLI overrides yet + cli_overrides = arg_parser().parse_args(_args) + + # then for each config file, parse it and override the args + config_files = resolve_config_files(_args) + for config_file in config_files: + if not os.path.exists(config_file): + if cli_overrides.debug: + debug(f"Skipping config file {config_file}") + continue + + overrides = toml_parser().parse_file(config_file) + config = config.with_overrides(source=config_file, **overrides) + + # finally apply the CLI overrides + config = config.with_overrides(source="command line args", **vars(cli_overrides)) + + return config + + @dataclass(frozen=True) class FunctionInfo: name: Optional[str] = None @@ -104,7 +157,7 @@ def mk_calldata( fun_info: FunctionInfo, cd: ByteVec, dyn_param_size: List[str], - args: Namespace, + args: Config, ) -> None: # find function abi fun_abi = find_abi(abi, fun_info) @@ -144,7 +197,7 @@ def mk_addr(name: str) -> Address: return BitVec(name, 160) -def mk_caller(args: Namespace) -> Address: +def mk_caller(args: Config) -> Address: if args.symbolic_msg_sender: return mk_addr("msg_sender") else: @@ -155,7 +208,7 @@ def mk_this() -> Address: return magic_address + 1 -def mk_solver(args: Namespace, logic="QF_AUFBV", ctx=None, assertion=False): +def mk_solver(args: Config, logic="QF_AUFBV", ctx=None, assertion=False): timeout = ( args.solver_timeout_assertion if assertion else args.solver_timeout_branching ) @@ -282,7 +335,7 @@ def render_trace(context: CallContext, file=sys.stdout) -> None: print(file=file) -def run_bytecode(hexcode: str, args: Namespace) -> List[Exec]: +def run_bytecode(hexcode: str, args: Config) -> List[Exec]: solver = mk_solver(args) contract = Contract.from_hexcode(hexcode) balance = mk_balance() @@ -345,7 +398,7 @@ def deploy_test( creation_hexcode: str, deployed_hexcode: str, sevm: SEVM, - args: Namespace, + args: Config, libs: Dict, ) -> Exec: this = mk_this() @@ -422,7 +475,7 @@ def setup( deployed_hexcode: str, abi: List, setup_info: FunctionInfo, - args: Namespace, + args: Config, libs: Dict, ) -> Exec: setup_timer = NamedTimer("setup") @@ -569,7 +622,7 @@ def run( setup_ex: Exec, abi: List, fun_info: FunctionInfo, - args: Namespace, + args: Config, ) -> TestResult: funname, funsig, funselector = fun_info.name, fun_info.sig, fun_info.selector if args.verbose >= 1: @@ -830,8 +883,8 @@ class SetupAndRunSingleArgs: abi: List setup_info: FunctionInfo fun_info: FunctionInfo - setup_args: Namespace - args: Namespace + setup_args: Config + args: Config libs: Dict @@ -899,7 +952,7 @@ class RunArgs: abi: List methodIdentifiers: Dict[str, str] - args: Namespace + args: Config contract_json: Dict libs: Dict @@ -915,8 +968,7 @@ def run_parallel(run_args: RunArgs) -> List[TestResult]: ) setup_info = extract_setup(methodIdentifiers) - setup_config = args.extend(parse_devdoc(setup_info.sig, run_args.contract_json)) - + setup_config = with_devdoc(args, setup_info.sig, run_args.contract_json) fun_infos = [ FunctionInfo(funsig.split("(")[0], funsig, methodIdentifiers[funsig]) for funsig in run_args.funsigs @@ -930,7 +982,7 @@ def run_parallel(run_args: RunArgs) -> List[TestResult]: setup_info, fun_info, setup_config, - args.extend(parse_devdoc(fun_info.sig, run_args.contract_json)), + with_devdoc(args, fun_info.sig, run_args.contract_json), libs, ) for fun_info in fun_infos @@ -949,13 +1001,13 @@ def run_sequential(run_args: RunArgs) -> List[TestResult]: setup_info = extract_setup(run_args.methodIdentifiers) try: - setup_args = args.extend(parse_devdoc(setup_info.sig, run_args.contract_json)) + setup_config = with_devdoc(args, setup_info.sig, run_args.contract_json) setup_ex = setup( run_args.creation_hexcode, run_args.deployed_hexcode, run_args.abi, setup_info, - setup_args, + setup_config, run_args.libs, ) except Exception as err: @@ -972,8 +1024,10 @@ def run_sequential(run_args: RunArgs) -> List[TestResult]: funsig.split("(")[0], funsig, run_args.methodIdentifiers[funsig] ) try: - extended_args = args.extend(parse_devdoc(funsig, run_args.contract_json)) - test_result = run(setup_ex, run_args.abi, fun_info, extended_args) + test_config = with_devdoc(args, funsig, run_args.contract_json) + if test_config.debug: + debug(f"{test_config.formatted_layers()}") + test_result = run(setup_ex, run_args.abi, fun_info, test_config) except Exception as err: print(f"{color_warn('[ERROR]')} {funsig}") print(color_warn(f"{type(err).__name__}: {err}")) @@ -989,7 +1043,7 @@ def run_sequential(run_args: RunArgs) -> List[TestResult]: @dataclass(frozen=True) class GenModelArgs: - args: Namespace + args: Config idx: int sexpr: str dump_dirname: Optional[str] = None @@ -1000,7 +1054,7 @@ def copy_model(model: Model) -> Dict: def solve( - query: str, args: Namespace, dump_filename: Optional[str] = None + query: str, args: Config, dump_filename: Optional[str] = None ) -> Tuple[CheckSatResult, Model]: if args.dump_smt_queries or args.solver_command: if not dump_filename: @@ -1101,7 +1155,7 @@ def package_result( model: Optional[UnionType[Model, str]], idx: int, result: CheckSatResult, - args: Namespace, + args: Config, ) -> ModelWithContext: if result == unsat: if args.verbose >= 1: @@ -1167,7 +1221,7 @@ def render_model(model: UnionType[str, StrModel]) -> str: return "".join(sorted(formatted)) if formatted else "∅" -def mk_options(args: Namespace) -> Dict: +def mk_options(args: Config) -> Dict: options = { "target": args.root, "verbose": args.verbose, @@ -1200,7 +1254,7 @@ def mk_options(args: Namespace) -> Dict: return options -def mk_arrlen(args: Namespace) -> Dict[str, int]: +def mk_arrlen(args: Config) -> Dict[str, int]: arrlen = {} if args.array_lengths: for assign in [x.split("=") for x in args.array_lengths.split(",")]: @@ -1210,7 +1264,7 @@ def mk_arrlen(args: Namespace) -> Dict[str, int]: return arrlen -def parse_build_out(args: Namespace) -> Dict: +def parse_build_out(args: Config) -> Dict: result = {} # compiler version -> source filename -> contract name -> (json, type) out_path = os.path.join(args.root, args.forge_build_out) @@ -1385,10 +1439,7 @@ def _main(_args=None) -> MainResult: # command line arguments # - config_parser = get_config_parser() - args = config_parser.parse_config(_args) - if args.debug: - debug(config_parser.format_values()) + args = load_config(_args) if args.version: print(f"halmos {metadata.version('halmos')}") @@ -1415,6 +1466,9 @@ def _main(_args=None) -> MainResult: ] # run forge without capturing stdout/stderr + if args.debug: + debug(f"Running {' '.join(build_cmd)}") + build_exitcode = subprocess.run(build_cmd).returncode if build_exitcode: @@ -1493,8 +1547,7 @@ def on_signal(signum, frame): print(f"\nRunning {num_found} tests for {contract_path}") # support for `/// @custom:halmos` annotations - contract_args = args.extend(parse_natspec(natspec)) if natspec else args - + contract_args = with_natspec(args, contract_name, natspec) run_args = RunArgs( funsigs, creation_hexcode, diff --git a/src/halmos/config.py b/src/halmos/config.py index ad2949c6..d24864ae 100644 --- a/src/halmos/config.py +++ b/src/halmos/config.py @@ -9,20 +9,37 @@ from .utils import warn -# common strings -help, metavar, group, choices, internal, global_default, short, countable = ( - "help", - "metavar", - "group", - "choices", - "internal", - "global_default", - "short", - "countable", +# groups +debug, solver, build, experimental = ( + "Debugging options", + "Solver options", + "Build options", + "Experimental options", ) -# groups -debug, solver = "Debugging options", "Solver options" + +# helper to define config fields +def arg( + help: str, + global_default: Any, + metavar: Optional[str] = None, + group: Optional[str] = None, + choices: Optional[str] = None, + short: Optional[str] = None, + countable: bool = False, +): + return field( + default=None, + metadata={ + "help": help, + "global_default": global_default, + "metavar": metavar, + "group": group, + "choices": choices, + "short": short, + "countable": countable, + }, + ) @dataclass(kw_only=True, frozen=True) @@ -37,16 +54,16 @@ class Config: ### Internal fields (not used to generate arg parsers) - config_parent: "Config" = field( + _parent: "Config" = field( repr=False, metadata={ - internal: True, + "internal": True, }, ) - config_source: str = field( + _source: str = field( metadata={ - internal: True, + "internal": True, }, ) @@ -65,113 +82,272 @@ class Config: # # We can then layer these Config objects on top of the `default_config()` - root: str = field( - default=None, - metadata={ - help: "Project root directory", - metavar: "PATH", - global_default: os.getcwd(), - }, + root: str = arg( + help="Project root directory", global_default=os.getcwd(), metavar="PATH" ) - depth: int = field( - default=None, - metadata={ - help: "set the max path length", - metavar: "MAX_DEPTH", - global_default: None, - }, + contract: str = arg( + help="run tests in the given contract. Shortcut for `--match-contract '^{NAME}$'`.", + global_default=None, + metavar="CONTRACT_NAME", ) - loop: int = field( - default=None, - metadata={ - help: "set loop unrolling bounds", - metavar: "MAX_BOUND", - global_default: 2, - }, + match_contract: str = arg( + help="run tests in contracts matching the given regex. Ignored if the --contract name is given. (default: '%(default)s')", + global_default="", + metavar="CONTRACT_NAME_REGEX", ) - symbolic_storage: bool = field( - default=None, - metadata={ - help: "set default storage values to symbolic", - global_default: False, - }, + function: str = arg( + help="run tests matching the given prefix. Shortcut for `--match-test '^{PREFIX}'`. (default: '%(default)s')", + global_default="check_", + metavar="FUNCTION_NAME_PREFIX", ) - storage_layout: str = field( - default=None, - metadata={ - help: "storage layout file", - metavar: "FILE", - choices: ["solidity", "generic"], - global_default: "solidity", - }, + match_test: str = arg( + help="run tests matching the given regex. The --function prefix is automatically added, unless the regex starts with '^'. (default: '%(default)s')", + global_default="", + metavar="FUNCTION_NAME_REGEX", + short="mt", + ) + + loop: int = arg( + help="set loop unrolling bounds (default: %(default)s)", + global_default=2, + metavar="MAX_BOUND", + ) + + width: int = arg( + help="set the max number of paths (default: %(default)s)", + global_default=2**64, + metavar="MAX_WIDTH", + ) + + depth: int = arg( + help="set the max path length", global_default=None, metavar="MAX_DEPTH" + ) + + array_lengths: str = arg( + help="set the length of dynamic-sized arrays including bytes and string (default: loop unrolling bound)", + global_default=None, + metavar="NAME1=LENGTH1,NAME2=LENGTH2,...", + ) + + uninterpreted_unknown_calls: str = arg( + help="use uninterpreted abstractions for unknown external calls with the given function signatures (default: '%(default)s')", + global_default="0x150b7a02,0x1626ba7e,0xf23a6e61,0xbc197c81", + metavar="SELECTOR1,SELECTOR2,...", + ) + + return_size_of_unknown_calls: int = arg( + help="set the byte size of return data from uninterpreted unknown external calls (default: %(default)s)", + global_default=32, + metavar="BYTE_SIZE", + ) + + storage_layout: str = arg( + help="Select one of the available storage layout models. The generic model should only be necessary for vyper, huff, or unconventional storage patterns in yul.", + global_default="solidity", + choices=["solidity", "generic"], + ) + + symbolic_storage: bool = arg( + help="set default storage values to symbolic", + global_default=False, + ) + + symbolic_msg_sender: bool = arg( + help="set msg.sender symbolic", + global_default=False, + ) + + no_test_constructor: bool = arg( + help="do not run the constructor of test contracts", + global_default=False, + ) + + ffi: bool = arg( + help="allow the usage of FFI to call external functions", + global_default=False, + ) + + version: bool = arg( + help="print the version number", + global_default=False, ) ### Debugging options - verbose: int = field( - default=None, - metadata={ - help: "increase verbosity levels: -v, -vv, -vvv, ...", - metavar: "LEVEL", - group: debug, - global_default: 0, - short: "v", - countable: True, - }, + verbose: int = arg( + help="increase verbosity levels: -v, -vv, -vvv, ...", + global_default=0, + group=debug, + short="v", + countable=True, ) - statistics: bool = field( - default=None, - metadata={ - help: "print statistics", - group: debug, - global_default: False, - }, + statistics: bool = arg( + help="print statistics", + global_default=False, + group=debug, + short="st", ) - json_output: str = field( - default=None, - metadata={ - help: "output test results in JSON", - metavar: "JSON_FILE_PATH", - group: debug, - global_default: None, - }, + debug: bool = arg( + help="run in debug mode", + global_default=False, + group=debug, + ) + + log: str = arg( + help="log every execution steps in JSON", + global_default=None, + metavar="LOG_FILE_PATH", + group=debug, + ) + + json_output: str = arg( + help="output test results in JSON", + global_default=None, + metavar="JSON_FILE_PATH", + group=debug, + ) + + minimal_json_output: bool = arg( + help="include minimal information in the JSON output", + global_default=False, + group=debug, + ) + + print_steps: bool = arg( + help="print every execution steps", + global_default=False, + group=debug, + ) + + print_states: bool = arg( + help="print all final execution states", + global_default=False, + group=debug, + ) + + print_failed_states: bool = arg( + help="print failed execution states", + global_default=False, + group=debug, + ) + + print_blocked_states: bool = arg( + help="print blocked execution states", + global_default=False, + group=debug, + ) + + print_setup_states: bool = arg( + help="print setup execution states", + global_default=False, + group=debug, + ) + + print_full_model: bool = arg( + help="print full counterexample model", + global_default=False, + group=debug, + ) + + early_exit: bool = arg( + help="stop after a counterexample is found", + global_default=False, + group=debug, + ) + + dump_smt_queries: bool = arg( + help="dump SMT queries for assertion violations", + global_default=False, + group=debug, + ) + + ### Build options + + forge_build_out: str = arg( + help="forge build artifacts directory name (default: 'out/')", + metavar="DIRECTORY_NAME", + global_default="out", + group=build, ) ### Solver options - solver_timeout_assertion: int = field( - default=None, - metadata={ - help: "set timeout (in milliseconds) for solving assertion violation conditions; 0 means no timeout", - metavar: "MILLISECONDS", - group: solver, - global_default: 1000, - }, + smt_exp_by_const: int = arg( + help="interpret constant power up to N (default: %(default)s)", + global_default=2, + metavar="N", + group=solver, ) - solver_parallel: bool = field( - default=None, - metadata={ - help: "run assertion solvers in parallel", - group: solver, - global_default: False, - }, + solver_timeout_branching: int = arg( + help="set timeout (in milliseconds) for solving branching conditions; 0 means no timeout (default: %(default)s)", + global_default=1, + metavar="TIMEOUT", + group=solver, ) - solver_threads: int = field( - default=None, - metadata={ - help: f"number of threads to use for assertion solving", - metavar: "N", - group: solver, - global_default: os.cpu_count() or 1, - }, + solver_timeout_assertion: int = arg( + help="set timeout (in milliseconds) for solving assertion violation conditions; 0 means no timeout (default: %(default)s)", + global_default=1000, + metavar="TIMEOUT", + group=solver, + ) + + solver_max_memory: int = arg( + help="set memory limit (in megabytes) for the solver; 0 means no limit (default: %(default)s)", + global_default=0, + metavar="SIZE", + group=solver, + ) + + solver_command: str = arg( + help="use the given command when invoking the solver, e.g. `z3 -model`", + global_default=None, + metavar="COMMAND", + group=solver, + ) + + solver_parallel: bool = arg( + help="run assertion solvers in parallel", global_default=False, group=solver + ) + + solver_threads: int = arg( + help="set the number of threads for parallel solvers (default: %(default)s)", + global_default=os.cpu_count() or 1, + metavar="N", + group=solver, + ) + + ### Experimental options + + bytecode: str = arg( + help="execute the given bytecode", + global_default=None, + metavar="HEX_STRING", + group=experimental, + ) + + reset_bytecode: str = arg( + help="reset the bytecode of given addresses after setUp()", + global_default=None, + metavar="ADDR1=CODE1,ADDR2=CODE2,...", + group=experimental, + ) + + test_parallel: bool = arg( + help="run tests in parallel", global_default=False, group=experimental + ) + + symbolic_jump: bool = arg( + help="support symbolic jump destination", + global_default=False, + group=experimental, ) ### Methods @@ -190,7 +366,7 @@ def __getattribute__(self, name): return value # look up value in parent object - parent = object.__getattribute__(self, "config_parent") + parent = object.__getattribute__(self, "_parent") if value is None and parent is not None: return getattr(parent, name) @@ -203,7 +379,7 @@ def with_overrides(self, source: str, **overrides): just a dictionary with the overrides (e.g. from a toml or json file).""" try: - return Config(config_parent=self, config_source=source, **overrides) + return Config(_parent=self, _source=source, **overrides) except TypeError as e: # follow argparse error message format and behavior warn(f"error: unrecognized argument: {str(e).split()[-1]}") @@ -213,14 +389,14 @@ def value_with_source(self, name: str) -> Tuple[Any, str]: # look up value in current object value = object.__getattribute__(self, name) if value is not None: - return (value, self.config_source) + return (value, self._source) # look up value in parent object - parent = object.__getattribute__(self, "config_parent") - if value is None and self.config_parent is not None: + parent = object.__getattribute__(self, "_parent") + if value is None and self._parent is not None: return parent.value_with_source(name) - return (value, self.config_source) + return (value, self._source) def values_with_sources(self) -> Dict[str, Tuple[Any, str]]: # field -> (value, source) @@ -232,7 +408,7 @@ def values_with_sources(self) -> Dict[str, Tuple[Any, str]]: return values def values(self): - skip_empty = self.config_parent is not None + skip_empty = self._parent is not None for field in fields(self): if field.metadata.get(internal): @@ -246,11 +422,11 @@ def values(self): def values_by_layer(self) -> Dict[str, Tuple[str, Any]]: # source -> {field, value} - if self.config_parent is None: - return OrderedDict([(self.config_source, dict(self.values()))]) + if self._parent is None: + return OrderedDict([(self._source, dict(self.values()))]) - values = self.config_parent.values_by_layer() - values[self.config_source] = dict(self.values()) + values = self._parent.values_by_layer() + values[self._source] = dict(self.values()) return values def formatted_layers(self) -> str: @@ -262,7 +438,7 @@ def formatted_layers(self) -> str: return "\n".join(lines) -def _mk_root_parser() -> argparse.ArgumentParser: +def resolve_config_files(args: UnionType[str, List[str]]) -> List[str]: root_parser = argparse.ArgumentParser() root_parser.add_argument( "--root", @@ -270,12 +446,6 @@ def _mk_root_parser() -> argparse.ArgumentParser: default=os.getcwd(), ) - return root_parser - - -def resolve_config_files(args: UnionType[str, List[str]]) -> List[str]: - root_parser = _mk_root_parser() - # first, parse find the project root directory (containing foundry.toml) # beware: errors and help flags will cause a system exit root_args = root_parser.parse_known_args(args)[0] @@ -323,11 +493,11 @@ def _create_default_config() -> "Config": for field in fields(Config): # we build the default config by looking at the global_default metadata field - default_value = field.metadata.get(global_default, MISSING) + default_value = field.metadata.get("global_default", MISSING) if default_value != MISSING: values[field.name] = default_value - return Config(config_parent=None, config_source="default", **values) + return Config(_parent=None, _source="default", **values) def _create_arg_parser() -> argparse.ArgumentParser: @@ -349,7 +519,7 @@ def _create_arg_parser() -> argparse.ArgumentParser: long_name = f"--{field_info.name.replace('_', '-')}" names = [long_name] - short_name = field_info.metadata.get(short, None) + short_name = field_info.metadata.get("short", None) if short_name: names.append(f"-{short_name}") @@ -364,7 +534,7 @@ def _create_arg_parser() -> argparse.ArgumentParser: if field_info.type == bool: group.add_argument(*names, help=arg_help, action="store_true", default=None) - elif field_info.metadata.get(countable, False): + elif field_info.metadata.get("countable", False): group.add_argument(*names, help=arg_help, action="count") else: kwargs = { @@ -384,8 +554,6 @@ def _create_toml_parser() -> TomlParser: # public singleton accessors - - def default_config() -> "Config": return _default_config @@ -399,7 +567,6 @@ def toml_parser(): # init module-level singletons - _arg_parser = _create_arg_parser() _default_config = _create_default_config() _toml_parser = _create_toml_parser() diff --git a/src/halmos/parser.py b/src/halmos/parser.py deleted file mode 100644 index 17d471f5..00000000 --- a/src/halmos/parser.py +++ /dev/null @@ -1,392 +0,0 @@ -# SPDX-License-Identifier: AGPL-3.0 - -import configargparse -import copy -import os - -from typing import List, Optional - -# type hint for the argument parser -ArgParser = configargparse.ArgParser - -# type hint for the arguments -Args = configargparse.Namespace - - -def _mk_root_parser() -> ArgParser: - root_parser = configargparse.ArgumentParser() - root_parser.add_argument( - "--root", - metavar="DIRECTORY", - default=os.getcwd(), - ) - - return root_parser - - -def _mk_arg_parser(config_file_provider: "ConfigFileProvider") -> ArgParser: - parser = configargparse.ArgParser( - prog="halmos", - epilog="For more information, see https://github.com/a16z/halmos", - default_config_files=config_file_provider.provide(), - config_file_parser_class=configargparse.TomlConfigParser(sections=["global"]), - add_config_file_help=True, - args_for_setting_config_path=["--config"], - ) - - parser.add_argument( - "--root", - metavar="DIRECTORY", - default=os.getcwd(), - help="source root directory (default: current directory)", - ) - - parser.add_argument( - "--contract", - metavar="CONTRACT_NAME", - help="run tests in the given contract. Shortcut for `--match-contract '^{NAME}$'`.", - ) - parser.add_argument( - "--match-contract", - "--mc", - metavar="CONTRACT_NAME_REGEX", - default="", - help="run tests in contracts matching the given regex. Ignored if the --contract name is given. (default: '%(default)s')", - ) - parser.add_argument( - "--function", - metavar="FUNCTION_NAME_PREFIX", - default="check_", - help="run tests matching the given prefix. Shortcut for `--match-test '^{PREFIX}'`. (default: '%(default)s')", - ) - parser.add_argument( - "--match-test", - "--mt", - metavar="FUNCTION_NAME_REGEX", - default="", - help="run tests matching the given regex. The --function prefix is automatically added, unless the regex starts with '^'. (default: '%(default)s')", - ) - - parser.add_argument( - "--loop", - metavar="MAX_BOUND", - type=int, - default=2, - help="set loop unrolling bounds (default: %(default)s)", - ) - parser.add_argument( - "--width", - metavar="MAX_WIDTH", - type=int, - default=2**64, - help="set the max number of paths (default: %(default)s)", - ) - parser.add_argument( - "--depth", metavar="MAX_DEPTH", type=int, help="set the max path length" - ) - parser.add_argument( - "--array-lengths", - metavar="NAME1=LENGTH1,NAME2=LENGTH2,...", - help="set the length of dynamic-sized arrays including bytes and string (default: loop unrolling bound)", - ) - - parser.add_argument( - "--uninterpreted-unknown-calls", - metavar="SELECTOR1,SELECTOR2,...", - # IERC721.onERC721Received, IERC1271.isValidSignature, IERC1155.onERC1155Received, IERC1155.onERC1155BatchReceived - default="0x150b7a02,0x1626ba7e,0xf23a6e61,0xbc197c81", - help="use uninterpreted abstractions for unknown external calls with the given function signatures (default: '%(default)s')", - ) - parser.add_argument( - "--return-size-of-unknown-calls", - metavar="BYTE_SIZE", - type=int, - default=32, - help="set the byte size of return data from uninterpreted unknown external calls (default: %(default)s)", - ) - - parser.add_argument( - "--storage-layout", - choices=["solidity", "generic"], - default="solidity", - help="Select one of the available storage layout models. The generic model should only be necessary for vyper, huff, or unconventional storage patterns in yul.", - ) - - parser.add_argument( - "--symbolic-storage", - action="store_true", - help="set default storage values to symbolic", - ) - parser.add_argument( - "--symbolic-msg-sender", action="store_true", help="set msg.sender symbolic" - ) - parser.add_argument( - "--no-test-constructor", - action="store_true", - help="do not run the constructor of test contracts", - ) - - parser.add_argument( - "--ffi", - action="store_true", - help="allow the usage of FFI to call external functions", - ) - - parser.add_argument( - "--version", action="store_true", help="print the version number" - ) - - # debugging options - group_debug = parser.add_argument_group("Debugging options") - - group_debug.add_argument( - "-v", - "--verbose", - action="count", - default=0, - help="increase verbosity levels: -v, -vv, -vvv, ...", - ) - group_debug.add_argument( - "-st", "--statistics", action="store_true", help="print statistics" - ) - group_debug.add_argument("--debug", action="store_true", help="run in debug mode") - group_debug.add_argument( - "--log", metavar="LOG_FILE_PATH", help="log every execution steps in JSON" - ) - group_debug.add_argument( - "--json-output", metavar="JSON_FILE_PATH", help="output test results in JSON" - ) - group_debug.add_argument( - "--minimal-json-output", - action="store_true", - help="include minimal information in the JSON output", - ) - group_debug.add_argument( - "--print-steps", action="store_true", help="print every execution steps" - ) - group_debug.add_argument( - "--print-states", action="store_true", help="print all final execution states" - ) - group_debug.add_argument( - "--print-failed-states", - action="store_true", - help="print failed execution states", - ) - group_debug.add_argument( - "--print-blocked-states", - action="store_true", - help="print blocked execution states", - ) - group_debug.add_argument( - "--print-setup-states", action="store_true", help="print setup execution states" - ) - group_debug.add_argument( - "--print-full-model", - action="store_true", - help="print full counterexample model", - ) - group_debug.add_argument( - "--early-exit", - action="store_true", - help="stop after a counterexample is found", - ) - - group_debug.add_argument( - "--dump-smt-queries", - action="store_true", - help="dump SMT queries for assertion violations", - ) - - # build options - group_build = parser.add_argument_group("Build options") - - group_build.add_argument( - "--forge-build-out", - metavar="DIRECTORY_NAME", - default="out", - help="forge build artifacts directory name (default: '%(default)s')", - ) - - # smt solver options - group_solver = parser.add_argument_group("Solver options") - - group_solver.add_argument( - "--smt-exp-by-const", - metavar="N", - type=int, - default=2, - help="interpret constant power up to N (default: %(default)s)", - ) - - group_solver.add_argument( - "--solver-timeout-branching", - metavar="TIMEOUT", - type=int, - default=1, - help="set timeout (in milliseconds) for solving branching conditions; 0 means no timeout (default: %(default)s)", - ) - group_solver.add_argument( - "--solver-timeout-assertion", - metavar="TIMEOUT", - type=int, - default=1000, - help="set timeout (in milliseconds) for solving assertion violation conditions; 0 means no timeout (default: %(default)s)", - ) - group_solver.add_argument( - "--solver-max-memory", - metavar="SIZE", - type=int, - default=0, - help="set memory limit (in megabytes) for the solver; 0 means no limit (default: %(default)s)", - ) - group_solver.add_argument( - "--solver-command", - metavar="COMMAND", - help="use the given command when invoking the solver, e.g. `z3 -model`", - ) - group_solver.add_argument( - "--solver-parallel", - action="store_true", - help="run assertion solvers in parallel", - ) - group_solver.add_argument( - "--solver-threads", - metavar="N", - type=int, - # the default value of max_workers for ThreadPoolExecutor - # TODO: set default value := total physical memory size / average z3 memory footprint - default=min(32, os.cpu_count() + 4), - help=f"set the number of threads for parallel solvers (default: %(default)s)", - ) - - # internal options - group_internal = parser.add_argument_group("Internal options") - - group_internal.add_argument( - "--bytecode", metavar="HEX_STRING", help="execute the given bytecode" - ) - group_internal.add_argument( - "--reset-bytecode", - metavar="ADDR1=CODE1,ADDR2=CODE2,...", - help="reset the bytecode of given addresses after setUp()", - ) - group_internal.add_argument( - "--test-parallel", action="store_true", help="run tests in parallel" - ) - - # experimental options - group_experimental = parser.add_argument_group("Experimental options") - - group_experimental.add_argument( - "--symbolic-jump", action="store_true", help="support symbolic jump destination" - ) - - return parser - - -class ConfigFileProvider: - def __init__(self, config_files: Optional[List[str]] = None): - self.root_parser = _mk_root_parser() - self.config_files = config_files - - # for testing purposes - self.config_file_contents = None - - def resolve_config_files(self, args: str) -> List[str]: - if self.config_files: - return self.config_files - - # first, parse find the project root directory (containing foundry.toml) - root_args = self.root_parser.parse_known_args(args, ignore_help_args=True)[0] - - # we expect to find halmos.toml in the project root directory - self.config_files = [os.path.join(root_args.root, "halmos.toml")] - return self.config_files - - def provide(self) -> Optional[List[str]]: - return self.config_files - - -class ConfigParser: - def __init__(self, config_file_provider: ConfigFileProvider = None): - self.config_file_provider = config_file_provider or ConfigFileProvider() - - # initialized in parse_config - self.arg_parser = None - - def parse_config(self, args: str) -> "Config": - """ - Parse the configuration file and command line arguments. - - Resolves the configuration file path based on the --root argument. - """ - self.config_file_provider.resolve_config_files(args) - - # construct an argument parser that can parse the configuration file - self.arg_parser = _mk_arg_parser(self.config_file_provider) - - # parse the configuration file + command line arguments - config_file_contents = self.config_file_provider.config_file_contents - - namespace = self.arg_parser.parse_args( - args, config_file_contents=config_file_contents - ) - return Config(args=namespace) - - def parse_args(self, args: str, base_config: Optional["Config"] = None) -> "Config": - """ - Parse command line arguments, potentially extending an existing configuration. - """ - base_namespace = copy.copy(base_config.args) if base_config else None - new_namespace = self.arg_parser.parse_args(args, namespace=base_namespace) - - if base_config.debug: - self.format_values() - - return Config(args=new_namespace) - - def format_values(self): - return self.arg_parser.format_values() - - -class Config: - """ - A wrapper around the parsed configuration with some extras: - - - can extend itself with more options - - can access the values of the underlying namespace as attributes - - keeps track of its parent configuration, avoiding copies - - Not to be instantiated directly, use ConfigParser.parse_config instead. - """ - - def __init__(self, args: Args = None): - self.args = args - - def extend(self, more_opts: str) -> "Config": - if more_opts: - new_config = config_parser.parse_args(more_opts, base_config=self) - return new_config - else: - return self - - def __getattr__(self, name): - args = self.__dict__.get("args", None) - if name == "args": - return args - - return getattr(args, name) - - def __repr__(self) -> str: - return repr(self.args) - - def __str__(self) -> str: - return str(self.args) - - -# global parser instance -config_parser = ConfigParser() - - -def get_config_parser() -> ConfigParser: - return config_parser diff --git a/tests/test_cli.py b/tests/test_cli.py index 21f5ab70..30550674 100644 --- a/tests/test_cli.py +++ b/tests/test_cli.py @@ -103,8 +103,7 @@ def test_decode_mixed_bytecode(): def test_run_bytecode(args): - # sets the flag in the global args for the main module - args.symbolic_jump = True + args = args.with_overrides(source="test_run_bytecode", symbolic_jump=True) hexcode = "34381856FDFDFDFDFDFD5B00" exs = run_bytecode(hexcode, args) diff --git a/tests/test_config.py b/tests/test_config.py index 9f161185..4f0b31d9 100644 --- a/tests/test_config.py +++ b/tests/test_config.py @@ -28,7 +28,7 @@ def toml_parser(): def test_fresh_config_has_only_None_values(): - config = Config(config_parent=None, config_source="bogus") + config = Config(_parent=None, _source="bogus") for field in config.__dataclass_fields__.values(): if field.metadata.get("internal"): continue @@ -42,11 +42,11 @@ def test_default_config_immutable(config): def test_unknown_keys_config_constructor_raise(): with pytest.raises(TypeError): - Config(config_parent=None, config_source="bogus", unknown_key=42) + Config(_parent=None, _source="bogus", unknown_key=42) def test_unknown_keys_config_object_raise(): - config = Config(config_parent=None, config_source="bogus") + config = Config(_parent=None, _source="bogus") with pytest.raises(AttributeError): config.unknown_key @@ -73,7 +73,7 @@ def test_choice_arg(config, parser): def test_override(config): verbose_before = config.verbose - override = Config(config_parent=config, config_source="override", verbose=42) + override = Config(_parent=config, _source="override", verbose=42) # # the override is reflected in the new config assert override.verbose == 42 diff --git a/tests/test_fixtures.py b/tests/test_fixtures.py index 23172e40..b5875a29 100644 --- a/tests/test_fixtures.py +++ b/tests/test_fixtures.py @@ -1,6 +1,6 @@ import pytest -from halmos.parser import ConfigParser +from halmos.config import default_config from halmos.sevm import SEVM from halmos.__main__ import mk_options, mk_solver import halmos.__main__ @@ -8,12 +8,7 @@ @pytest.fixture def args(): - args = ConfigParser().parse_config("") - - # set the global args for the main module - halmos.__main__.args = args - - return args + return default_config() @pytest.fixture diff --git a/tests/test_parser.py b/tests/test_parser.py deleted file mode 100644 index 53e3112e..00000000 --- a/tests/test_parser.py +++ /dev/null @@ -1,139 +0,0 @@ -import os -import pytest - -import halmos.parser -from halmos.parser import ConfigFileProvider, ConfigParser - - -def mock_config_file_provider(config_file_contents): - # use a real object but with a non-existent file and mocked contents - provider = ConfigFileProvider(config_files=["mock_halmos.toml"]) - provider.config_file_contents = config_file_contents - return provider - - -def mock_config_parser(config_file_provider): - halmos.parser.config_parser = ConfigParser( - config_file_provider=config_file_provider - ) - return halmos.parser.get_config_parser() - - -def test_config_file_default_location_is_cwd(): - cfp = ConfigFileProvider() - - # when we don't pass the project root as an argument - cfp.resolve_config_files(args=[]) - - # then the config file should be in the default location - assert cfp.provide() == [os.path.join(os.getcwd(), "halmos.toml")] - - -def test_config_file_in_project_root(): - cfp = ConfigFileProvider() - - # when we pass the project root as an argument - base_path = "/path/to/project" - args = ["--root", "/path/to/project", "--extra-args", "ignored", "--help"] - cfp.resolve_config_files(args) - - # then the config file should be in the project root - assert cfp.provide() == [os.path.join(base_path, "halmos.toml")] - - -def test_load_config_file_not_found(): - # when we try to load a non-existent config file - cfp = ConfigFileProvider(config_files=["nonexistent.toml"]) - config_parser = mock_config_parser(cfp) - config = config_parser.parse_config(args="") - - # then we should get a config object with default values - assert "Config File" not in config_parser.format_values() - - -def test_load_config_file_missing_section(): - # mock a valid config file with a missing section - cfp = mock_config_file_provider("depth = 42") - config_parser = mock_config_parser(cfp) - - # when we parse the config with the missing section - config = config_parser.parse_config(args="") - - # then the malformed config file does not contribute to the config object - assert "Config File" not in config_parser.format_values() - assert config.depth != 42 - - -def test_parse_config_invalid_key(): - # mock a valid config file with an invalid key - cfp = mock_config_file_provider("[global]\ninvalid_key = 42") - config_parser = mock_config_parser(cfp) - - # invalid keys result in an error and exit - with pytest.raises(SystemExit) as exc_info: - config_parser.parse_config(args="") - assert exc_info.value.code == 2 - - -def test_parse_config_invalid_type(): - cfp = mock_config_file_provider("[global]\ndepth = 'invalid'") - config_parser = mock_config_parser(cfp) - - # invalid types result in an error and exit - with pytest.raises(SystemExit) as exc_info: - config_parser.parse_config(args="") - assert exc_info.value.code == 2 - - -def test_parse_config_success(): - # mock a valid config file - cfp = mock_config_file_provider("[global]\ndepth = 42") - config_parser = mock_config_parser(cfp) - - # when we parse the config - config = config_parser.parse_config(args="") - - # then we should get a config object with the correct values - assert config.depth == 42 - - -def test_parse_config_override(): - # mock a valid config file - cfp = mock_config_file_provider("[global]\ndepth = 42\nverbose = 1234") - config_parser = mock_config_parser(cfp) - - # when we parse the config with an override - config = config_parser.parse_config(args="--depth 123456") - - # then we should get a config object with the overridden value - assert config.depth == 123456 - - # from config file - assert config.verbose == 1234 - - # from command line defaults - assert config.loop == 2 - - -def test_config_extend_does_not_modify_original(): - # mock a valid config file - cfp = mock_config_file_provider("[global]\ndepth = 42\nverbose = 1234") - config_parser = mock_config_parser(cfp) - config = config_parser.parse_config(args="") - assert config.depth == 42 - - # when we extend the config - new_config = config.extend("--depth=123456") - - # then the new config should have the overridden value - assert new_config.depth == 123456 - - # and the original config should not be modified - assert config.depth == 42 - - # the base value can be accessed from the new config - assert new_config.verbose == 1234 - - # missing values raise - with pytest.raises(AttributeError): - new_config.missing From 16409b984ba2f4b41cf8a2d5972f511276986eef Mon Sep 17 00:00:00 2001 From: karmacoma Date: Wed, 29 May 2024 17:11:41 -0700 Subject: [PATCH 10/19] remove `(default: None)` --- src/halmos/calldata.py | 6 ++--- src/halmos/config.py | 61 ++++++++++++++++++++++-------------------- 2 files changed, 35 insertions(+), 32 deletions(-) diff --git a/src/halmos/calldata.py b/src/halmos/calldata.py index df34af19..5378417f 100644 --- a/src/halmos/calldata.py +++ b/src/halmos/calldata.py @@ -4,13 +4,13 @@ from dataclasses import dataclass from typing import List, Dict -from argparse import Namespace from functools import reduce from z3 import * from .sevm import con, concat from .bytevec import ByteVec +from .config import Config as HalmosConfig @dataclass(frozen=True) @@ -83,12 +83,12 @@ class EncodingResult: class Calldata: - args: Namespace + args: HalmosConfig arrlen: Dict[str, int] dyn_param_size: List[str] # to be updated def __init__( - self, args: Namespace, arrlen: Dict[str, int], dyn_param_size: List[str] + self, args: HalmosConfig, arrlen: Dict[str, int], dyn_param_size: List[str] ) -> None: self.args = args self.arrlen = arrlen diff --git a/src/halmos/config.py b/src/halmos/config.py index d24864ae..a86f97d3 100644 --- a/src/halmos/config.py +++ b/src/halmos/config.py @@ -9,8 +9,11 @@ from .utils import warn +# common strings +internal = "internal" + # groups -debug, solver, build, experimental = ( +debugging, solver, build, experimental = ( "Debugging options", "Solver options", "Build options", @@ -57,13 +60,13 @@ class Config: _parent: "Config" = field( repr=False, metadata={ - "internal": True, + internal: True, }, ) _source: str = field( metadata={ - "internal": True, + internal: True, }, ) @@ -93,32 +96,32 @@ class Config: ) match_contract: str = arg( - help="run tests in contracts matching the given regex. Ignored if the --contract name is given. (default: '%(default)s')", + help="run tests in contracts matching the given regex. Ignored if the --contract name is given.", global_default="", metavar="CONTRACT_NAME_REGEX", ) function: str = arg( - help="run tests matching the given prefix. Shortcut for `--match-test '^{PREFIX}'`. (default: '%(default)s')", + help="run tests matching the given prefix. Shortcut for `--match-test '^{PREFIX}'`.", global_default="check_", metavar="FUNCTION_NAME_PREFIX", ) match_test: str = arg( - help="run tests matching the given regex. The --function prefix is automatically added, unless the regex starts with '^'. (default: '%(default)s')", + help="run tests matching the given regex. The --function prefix is automatically added, unless the regex starts with '^'.", global_default="", metavar="FUNCTION_NAME_REGEX", short="mt", ) loop: int = arg( - help="set loop unrolling bounds (default: %(default)s)", + help="set loop unrolling bounds", global_default=2, metavar="MAX_BOUND", ) width: int = arg( - help="set the max number of paths (default: %(default)s)", + help="set the max number of paths", global_default=2**64, metavar="MAX_WIDTH", ) @@ -134,13 +137,13 @@ class Config: ) uninterpreted_unknown_calls: str = arg( - help="use uninterpreted abstractions for unknown external calls with the given function signatures (default: '%(default)s')", + help="use uninterpreted abstractions for unknown external calls with the given function signatures", global_default="0x150b7a02,0x1626ba7e,0xf23a6e61,0xbc197c81", metavar="SELECTOR1,SELECTOR2,...", ) return_size_of_unknown_calls: int = arg( - help="set the byte size of return data from uninterpreted unknown external calls (default: %(default)s)", + help="set the byte size of return data from uninterpreted unknown external calls", global_default=32, metavar="BYTE_SIZE", ) @@ -181,7 +184,7 @@ class Config: verbose: int = arg( help="increase verbosity levels: -v, -vv, -vvv, ...", global_default=0, - group=debug, + group=debugging, short="v", countable=True, ) @@ -189,82 +192,82 @@ class Config: statistics: bool = arg( help="print statistics", global_default=False, - group=debug, + group=debugging, short="st", ) debug: bool = arg( help="run in debug mode", global_default=False, - group=debug, + group=debugging, ) log: str = arg( help="log every execution steps in JSON", global_default=None, metavar="LOG_FILE_PATH", - group=debug, + group=debugging, ) json_output: str = arg( help="output test results in JSON", global_default=None, metavar="JSON_FILE_PATH", - group=debug, + group=debugging, ) minimal_json_output: bool = arg( help="include minimal information in the JSON output", global_default=False, - group=debug, + group=debugging, ) print_steps: bool = arg( help="print every execution steps", global_default=False, - group=debug, + group=debugging, ) print_states: bool = arg( help="print all final execution states", global_default=False, - group=debug, + group=debugging, ) print_failed_states: bool = arg( help="print failed execution states", global_default=False, - group=debug, + group=debugging, ) print_blocked_states: bool = arg( help="print blocked execution states", global_default=False, - group=debug, + group=debugging, ) print_setup_states: bool = arg( help="print setup execution states", global_default=False, - group=debug, + group=debugging, ) print_full_model: bool = arg( help="print full counterexample model", global_default=False, - group=debug, + group=debugging, ) early_exit: bool = arg( help="stop after a counterexample is found", global_default=False, - group=debug, + group=debugging, ) dump_smt_queries: bool = arg( help="dump SMT queries for assertion violations", global_default=False, - group=debug, + group=debugging, ) ### Build options @@ -279,28 +282,28 @@ class Config: ### Solver options smt_exp_by_const: int = arg( - help="interpret constant power up to N (default: %(default)s)", + help="interpret constant power up to N", global_default=2, metavar="N", group=solver, ) solver_timeout_branching: int = arg( - help="set timeout (in milliseconds) for solving branching conditions; 0 means no timeout (default: %(default)s)", + help="set timeout (in milliseconds) for solving branching conditions; 0 means no timeout", global_default=1, metavar="TIMEOUT", group=solver, ) solver_timeout_assertion: int = arg( - help="set timeout (in milliseconds) for solving assertion violation conditions; 0 means no timeout (default: %(default)s)", + help="set timeout (in milliseconds) for solving assertion violation conditions; 0 means no timeout", global_default=1000, metavar="TIMEOUT", group=solver, ) solver_max_memory: int = arg( - help="set memory limit (in megabytes) for the solver; 0 means no limit (default: %(default)s)", + help="set memory limit (in megabytes) for the solver; 0 means no limit", global_default=0, metavar="SIZE", group=solver, @@ -318,7 +321,7 @@ class Config: ) solver_threads: int = arg( - help="set the number of threads for parallel solvers (default: %(default)s)", + help="set the number of threads for parallel solvers", global_default=os.cpu_count() or 1, metavar="N", group=solver, From d620dc2e8daef84fa76ec12ea4a0dc47106e374f Mon Sep 17 00:00:00 2001 From: karmacoma Date: Wed, 29 May 2024 17:16:19 -0700 Subject: [PATCH 11/19] add default value to the help string --- src/halmos/config.py | 8 ++++++-- 1 file changed, 6 insertions(+), 2 deletions(-) diff --git a/src/halmos/config.py b/src/halmos/config.py index a86f97d3..3acc6914 100644 --- a/src/halmos/config.py +++ b/src/halmos/config.py @@ -122,7 +122,7 @@ class Config: width: int = arg( help="set the max number of paths", - global_default=2**64, + global_default=2**16, metavar="MAX_WIDTH", ) @@ -529,7 +529,6 @@ def _create_arg_parser() -> argparse.ArgumentParser: arg_help = field_info.metadata.get("help", "") metavar = field_info.metadata.get("metavar", None) group_name = field_info.metadata.get("group", None) - if group_name not in groups: groups[group_name] = parser.add_argument_group(group_name) @@ -540,6 +539,11 @@ def _create_arg_parser() -> argparse.ArgumentParser: elif field_info.metadata.get("countable", False): group.add_argument(*names, help=arg_help, action="count") else: + # add the default value to the help text + default = field_info.metadata.get("global_default", None) + if default is not None: + arg_help += f" (default: {default!r})" + kwargs = { "help": arg_help, "metavar": metavar, From 317c2068519fe8a902b8d0a3585f9c28e68cbda6 Mon Sep 17 00:00:00 2001 From: karmacoma Date: Wed, 29 May 2024 17:41:53 -0700 Subject: [PATCH 12/19] add --config option --- halmos.toml | 12 ------------ src/halmos/__main__.py | 5 ++--- src/halmos/config.py | 29 +++++++++++++++++++++++------ tests/test_config.py | 13 ++++++++++--- 4 files changed, 35 insertions(+), 24 deletions(-) delete mode 100644 halmos.toml diff --git a/halmos.toml b/halmos.toml deleted file mode 100644 index a55baa5c..00000000 --- a/halmos.toml +++ /dev/null @@ -1,12 +0,0 @@ -# This is an example file for configuring the Halmos settings. -# For configuration values, refer to the options listed under the 'halmos --help' command. - -# for now, every setting must be under the 'global' section -[global] - -verbose = 3 -debug = true -statistics = true - -depth = 1_000_000 -storage-layout = 'generic' diff --git a/src/halmos/__main__.py b/src/halmos/__main__.py index 933933ff..aef9e2e2 100644 --- a/src/halmos/__main__.py +++ b/src/halmos/__main__.py @@ -103,9 +103,8 @@ def load_config(_args) -> HalmosConfig: config_files = resolve_config_files(_args) for config_file in config_files: if not os.path.exists(config_file): - if cli_overrides.debug: - debug(f"Skipping config file {config_file}") - continue + error(f"Config file not found: {config_file}") + sys.exit(2) overrides = toml_parser().parse_file(config_file) config = config.with_overrides(source=config_file, **overrides) diff --git a/src/halmos/config.py b/src/halmos/config.py index 3acc6914..f6a3da10 100644 --- a/src/halmos/config.py +++ b/src/halmos/config.py @@ -85,6 +85,12 @@ class Config: # # We can then layer these Config objects on top of the `default_config()` + config: str = arg( + help="path to the configuration file", + global_default=None, + metavar="FILE", + ) + root: str = arg( help="Project root directory", global_default=os.getcwd(), metavar="PATH" ) @@ -441,21 +447,32 @@ def formatted_layers(self) -> str: return "\n".join(lines) -def resolve_config_files(args: UnionType[str, List[str]]) -> List[str]: - root_parser = argparse.ArgumentParser() - root_parser.add_argument( +def resolve_config_files(args: List[str], include_missing: bool = False) -> List[str]: + config_parser = argparse.ArgumentParser() + config_parser.add_argument( "--root", metavar="DIRECTORY", default=os.getcwd(), ) + config_parser.add_argument("--config", metavar="FILE") + # first, parse find the project root directory (containing foundry.toml) # beware: errors and help flags will cause a system exit - root_args = root_parser.parse_known_args(args)[0] + args = config_parser.parse_known_args(args)[0] + + # if --config is passed explicitly, use that + # no check for existence is done here, we don't want to silently ignore + # missing config files when they are requested explicitly + if args.config: + return [args.config] # we expect to find halmos.toml in the project root directory - config_files = [os.path.join(root_args.root, "halmos.toml")] - return config_files + default_config_path = os.path.join(args.root, "halmos.toml") + if not include_missing and not os.path.exists(default_config_path): + return [] + + return [default_config_path] class TomlParser: diff --git a/tests/test_config.py b/tests/test_config.py index 4f0b31d9..164ba8d4 100644 --- a/tests/test_config.py +++ b/tests/test_config.py @@ -106,15 +106,22 @@ def test_config_file_default_location_is_cwd(): # when we don't pass the project root as an argument config_files = resolve_config_files(args=[]) - # then the config file should be in the default location - assert config_files == [os.path.join(os.getcwd(), "halmos.toml")] + # then we don't expect a config file since the default doesn't exist + assert config_files == [] + + # when we pass a --config argument explicitly + args = ["--config", "fake.toml", "--extra-args", "ignored"] + config_files = resolve_config_files(args) + + # then we expect the config file to be the one we passed + assert config_files == ["fake.toml"] def test_config_file_in_project_root(): # when we pass the project root as an argument base_path = "/path/to/project" args = ["--root", base_path, "--extra-args", "ignored"] - config_files = resolve_config_files(args) + config_files = resolve_config_files(args, include_missing=True) # then the config file should be in the project root assert config_files == [os.path.join(base_path, "halmos.toml")] From 6a9a5c78cf438936b3cf12bda595d2a6f3f8810f Mon Sep 17 00:00:00 2001 From: karmacoma Date: Wed, 29 May 2024 17:44:55 -0700 Subject: [PATCH 13/19] remove ConfigArgParse dependency --- pyproject.toml | 1 - tests/test_config.py | 16 +++++++++------- 2 files changed, 9 insertions(+), 8 deletions(-) diff --git a/pyproject.toml b/pyproject.toml index 1427cc5c..df346d68 100644 --- a/pyproject.toml +++ b/pyproject.toml @@ -22,7 +22,6 @@ classifiers = [ ] requires-python = ">=3.9" dependencies = [ - "ConfigArgParse>=1.7", "sortedcontainers>=2.4.0", "toml>=0.10.2", "z3-solver==4.12.6.0", diff --git a/tests/test_config.py b/tests/test_config.py index 164ba8d4..decc9ed6 100644 --- a/tests/test_config.py +++ b/tests/test_config.py @@ -109,13 +109,6 @@ def test_config_file_default_location_is_cwd(): # then we don't expect a config file since the default doesn't exist assert config_files == [] - # when we pass a --config argument explicitly - args = ["--config", "fake.toml", "--extra-args", "ignored"] - config_files = resolve_config_files(args) - - # then we expect the config file to be the one we passed - assert config_files == ["fake.toml"] - def test_config_file_in_project_root(): # when we pass the project root as an argument @@ -127,6 +120,15 @@ def test_config_file_in_project_root(): assert config_files == [os.path.join(base_path, "halmos.toml")] +def test_config_file_explicit(): + # when we pass a --config argument explicitly + args = ["--config", "path/to/fake.toml", "--extra-args", "ignored"] + config_files = resolve_config_files(args) + + # then we expect the config file to be the one we passed + assert config_files == ["path/to/fake.toml"] + + def test_config_file_invalid_key(config, toml_parser): # invalid keys result in an error and exit with pytest.raises(SystemExit) as exc_info: From d089cb736f4c07694757bd9a608c97856a54096c Mon Sep 17 00:00:00 2001 From: karmacoma Date: Wed, 29 May 2024 17:46:31 -0700 Subject: [PATCH 14/19] unused import --- tests/test_config.py | 1 - 1 file changed, 1 deletion(-) diff --git a/tests/test_config.py b/tests/test_config.py index decc9ed6..8dcbe40e 100644 --- a/tests/test_config.py +++ b/tests/test_config.py @@ -1,4 +1,3 @@ -import argparse import os import pickle import pytest From 3bcf0b8d963f27cf943c6cfdedd18455a0ddef15 Mon Sep 17 00:00:00 2001 From: karmacoma Date: Wed, 29 May 2024 17:58:07 -0700 Subject: [PATCH 15/19] remove kw_only for python 3.9 support --- src/halmos/config.py | 3 ++- 1 file changed, 2 insertions(+), 1 deletion(-) diff --git a/src/halmos/config.py b/src/halmos/config.py index f6a3da10..8db031d9 100644 --- a/src/halmos/config.py +++ b/src/halmos/config.py @@ -45,7 +45,8 @@ def arg( ) -@dataclass(kw_only=True, frozen=True) +# TODO: add kw_only=True when we support Python>=3.10 +@dataclass(frozen=True) class Config: """Configuration object for halmos. From 407cbeffa5c508beed3ce939aeb0e37d5489b106 Mon Sep 17 00:00:00 2001 From: karmacoma Date: Thu, 30 May 2024 09:47:20 -0700 Subject: [PATCH 16/19] replace SEVM.options dict with a Config object --- src/halmos/__main__.py | 78 +++++++++++----------------------------- src/halmos/cheatcodes.py | 8 ++--- src/halmos/config.py | 8 ++++- src/halmos/sevm.py | 54 ++++++++++++++-------------- tests/test_cli.py | 2 +- tests/test_fixtures.py | 12 ++----- tests/test_sevm.py | 2 +- tests/test_traces.py | 5 ++- 8 files changed, 64 insertions(+), 105 deletions(-) diff --git a/src/halmos/__main__.py b/src/halmos/__main__.py index aef9e2e2..3bb3ce84 100644 --- a/src/halmos/__main__.py +++ b/src/halmos/__main__.py @@ -156,7 +156,7 @@ def mk_calldata( fun_info: FunctionInfo, cd: ByteVec, dyn_param_size: List[str], - args: Config, + args: HalmosConfig, ) -> None: # find function abi fun_abi = find_abi(abi, fun_info) @@ -196,7 +196,7 @@ def mk_addr(name: str) -> Address: return BitVec(name, 160) -def mk_caller(args: Config) -> Address: +def mk_caller(args: HalmosConfig) -> Address: if args.symbolic_msg_sender: return mk_addr("msg_sender") else: @@ -207,7 +207,7 @@ def mk_this() -> Address: return magic_address + 1 -def mk_solver(args: Config, logic="QF_AUFBV", ctx=None, assertion=False): +def mk_solver(args: HalmosConfig, logic="QF_AUFBV", ctx=None, assertion=False): timeout = ( args.solver_timeout_assertion if assertion else args.solver_timeout_branching ) @@ -334,12 +334,11 @@ def render_trace(context: CallContext, file=sys.stdout) -> None: print(file=file) -def run_bytecode(hexcode: str, args: Config) -> List[Exec]: +def run_bytecode(hexcode: str, args: HalmosConfig) -> List[Exec]: solver = mk_solver(args) contract = Contract.from_hexcode(hexcode) balance = mk_balance() block = mk_block() - options = mk_options(args) this = mk_this() message = Message( @@ -350,7 +349,7 @@ def run_bytecode(hexcode: str, args: Config) -> List[Exec]: call_scheme=EVM.CALL, ) - sevm = SEVM(options) + sevm = SEVM(args) ex = sevm.mk_exec( code={this: contract}, storage={this: {}}, @@ -397,7 +396,7 @@ def deploy_test( creation_hexcode: str, deployed_hexcode: str, sevm: SEVM, - args: Config, + args: HalmosConfig, libs: Dict, ) -> Exec: this = mk_this() @@ -474,13 +473,13 @@ def setup( deployed_hexcode: str, abi: List, setup_info: FunctionInfo, - args: Config, + args: HalmosConfig, libs: Dict, ) -> Exec: setup_timer = NamedTimer("setup") setup_timer.create_subtimer("decode") - sevm = SEVM(mk_options(args)) + sevm = SEVM(args) setup_ex = deploy_test(creation_hexcode, deployed_hexcode, sevm, args, libs) setup_timer.create_subtimer("run") @@ -621,7 +620,7 @@ def run( setup_ex: Exec, abi: List, fun_info: FunctionInfo, - args: Config, + args: HalmosConfig, ) -> TestResult: funname, funsig, funselector = fun_info.name, fun_info.sig, fun_info.selector if args.verbose >= 1: @@ -654,9 +653,7 @@ def run( timer = NamedTimer("time") timer.create_subtimer("paths") - options = mk_options(args) - sevm = SEVM(options) - + sevm = SEVM(args) solver = mk_solver(args) path = Path(solver) path.extend_path(setup_ex.path) @@ -882,8 +879,8 @@ class SetupAndRunSingleArgs: abi: List setup_info: FunctionInfo fun_info: FunctionInfo - setup_args: Config - args: Config + setup_args: HalmosConfig + args: HalmosConfig libs: Dict @@ -951,7 +948,7 @@ class RunArgs: abi: List methodIdentifiers: Dict[str, str] - args: Config + args: HalmosConfig contract_json: Dict libs: Dict @@ -1042,7 +1039,7 @@ def run_sequential(run_args: RunArgs) -> List[TestResult]: @dataclass(frozen=True) class GenModelArgs: - args: Config + args: HalmosConfig idx: int sexpr: str dump_dirname: Optional[str] = None @@ -1053,7 +1050,7 @@ def copy_model(model: Model) -> Dict: def solve( - query: str, args: Config, dump_filename: Optional[str] = None + query: str, args: HalmosConfig, dump_filename: Optional[str] = None ) -> Tuple[CheckSatResult, Model]: if args.dump_smt_queries or args.solver_command: if not dump_filename: @@ -1154,7 +1151,7 @@ def package_result( model: Optional[UnionType[Model, str]], idx: int, result: CheckSatResult, - args: Config, + args: HalmosConfig, ) -> ModelWithContext: if result == unsat: if args.verbose >= 1: @@ -1220,40 +1217,7 @@ def render_model(model: UnionType[str, StrModel]) -> str: return "".join(sorted(formatted)) if formatted else "∅" -def mk_options(args: Config) -> Dict: - options = { - "target": args.root, - "verbose": args.verbose, - "debug": args.debug, - "log": args.log, - "expByConst": args.smt_exp_by_const, - "timeout": args.solver_timeout_branching, - "max_memory": args.solver_max_memory, - "sym_jump": args.symbolic_jump, - "print_steps": args.print_steps, - "unknown_calls_return_size": args.return_size_of_unknown_calls, - "ffi": args.ffi, - "storage_layout": args.storage_layout, - } - - if args.width is not None: - options["max_width"] = args.width - - if args.depth is not None: - options["max_depth"] = args.depth - - if args.loop is not None: - options["max_loop"] = args.loop - - options["unknown_calls"] = [] - if args.uninterpreted_unknown_calls.strip(): - for x in args.uninterpreted_unknown_calls.split(","): - options["unknown_calls"].append(int(x, 0)) - - return options - - -def mk_arrlen(args: Config) -> Dict[str, int]: +def mk_arrlen(args: HalmosConfig) -> Dict[str, int]: arrlen = {} if args.array_lengths: for assign in [x.split("=") for x in args.array_lengths.split(",")]: @@ -1263,7 +1227,7 @@ def mk_arrlen(args: Config) -> Dict[str, int]: return arrlen -def parse_build_out(args: Config) -> Dict: +def parse_build_out(args: HalmosConfig) -> Dict: result = {} # compiler version -> source filename -> contract name -> (json, type) out_path = os.path.join(args.root, args.forge_build_out) @@ -1322,10 +1286,8 @@ def parse_build_out(args: Config) -> Dict: ) contract_map[contract_name] = (json_out, contract_type, natspec) except Exception as err: - print( - color_warn( - f"Skipped {json_filename} due to parsing failure: {type(err).__name__}: {err}" - ) + warn( + f"Skipped {json_filename} due to parsing failure: {type(err).__name__}: {err}" ) if args.debug: traceback.print_exc() diff --git a/src/halmos/cheatcodes.py b/src/halmos/cheatcodes.py index a47e427b..df967c7e 100644 --- a/src/halmos/cheatcodes.py +++ b/src/halmos/cheatcodes.py @@ -349,7 +349,7 @@ def handle(sevm, ex, arg: ByteVec) -> Optional[ByteVec]: [filename, contract_name] = path.split(":") path = "out/" + filename + "/" + contract_name + ".json" - target = sevm.options["target"].rstrip("/") + target = sevm.options.root.rstrip("/") path = target + "/" + path with open(path) as f: @@ -470,14 +470,14 @@ def handle(sevm, ex, arg: ByteVec) -> Optional[ByteVec]: # ffi(string[]) returns (bytes) elif funsig == hevm_cheat_code.ffi_sig: - if not sevm.options.get("ffi"): + if not sevm.options.ffi: error_msg = "ffi cheatcode is disabled. Run again with `--ffi` if you want to enable it" raise HalmosException(error_msg) cmd = extract_string_array_argument(arg, 0) - debug = sevm.options.get("debug", False) - verbose = sevm.options.get("verbose", 0) + debug = sevm.options.debug + verbose = sevm.options.verbose if debug or verbose: print(f"[vm.ffi] {cmd}") diff --git a/src/halmos/config.py b/src/halmos/config.py index 8db031d9..f574ea65 100644 --- a/src/halmos/config.py +++ b/src/halmos/config.py @@ -230,7 +230,13 @@ class Config: ) print_steps: bool = arg( - help="print every execution steps", + help="print every execution step", + global_default=False, + group=debugging, + ) + + print_mem: bool = arg( + help="when --print-steps is enabled, also print memory contents", global_default=False, group=debugging, ) diff --git a/src/halmos/sevm.py b/src/halmos/sevm.py index 012327dd..c1795cc0 100644 --- a/src/halmos/sevm.py +++ b/src/halmos/sevm.py @@ -6,7 +6,7 @@ from copy import deepcopy from collections import defaultdict from dataclasses import dataclass, field -from functools import reduce, lru_cache +from functools import reduce from typing import ( Any, Callable, @@ -24,13 +24,13 @@ from .bytevec import Chunk, ByteVec from .cheatcodes import halmos_cheat_code, hevm_cheat_code, Prank +from .config import Config as HalmosConfig from .console import console from .exceptions import * from .utils import * from .warnings import ( warn, LIBRARY_PLACEHOLDER, - INTERNAL_ERROR, ) Steps = Dict[int, Dict[str, Any]] # execution tree @@ -1228,17 +1228,22 @@ def __len__(self) -> int: class SEVM: - options: Dict + options: HalmosConfig storage_model: Type[SomeStorage] logs: HalmosLogs steps: Steps - def __init__(self, options: Dict) -> None: + def __init__(self, options: HalmosConfig) -> None: self.options = options self.logs = HalmosLogs() self.steps: Steps = {} - is_generic = self.options["storage_layout"] == "generic" + # init unknown calls + hex_string = options.uninterpreted_unknown_calls.strip() + self.unknown_calls: List[int] = [int(x, 16) for x in hex_string.split(",") if x] + + # init storage model + is_generic = self.options.storage_layout == "generic" self.storage_model = GenericStorage if is_generic else SolidityStorage def div_xy_y(self, w1: Word, w2: Word) -> Word: @@ -1378,7 +1383,7 @@ def arith(self, ex: Exec, op: int, w1: Word, w2: Word) -> Word: if i2 == 1: return w1 - if i2 <= self.options.get("expByConst"): + if i2 <= self.options.smt_exp_by_const: exp = w1 for _ in range(i2 - 1): exp = exp * w1 @@ -1434,21 +1439,19 @@ def resolve_address_alias(self, ex: Exec, target: Address) -> Address: return target # set new timeout temporarily for this task - ex.path.solver.set(timeout=max(1000, self.options["timeout"])) + ex.path.solver.set(timeout=max(1000, self.options.solver_timeout_branching)) if target not in ex.alias: for addr in ex.code: if ex.check(target != addr) == unsat: # target == addr - if self.options.get("debug"): - print( - f"[DEBUG] Address alias: {hexify(addr)} for {hexify(target)}" - ) + if self.options.debug: + debug(f"Address alias: {hexify(addr)} for {hexify(target)}") ex.alias[target] = addr ex.path.append(target == addr) break # reset timeout - ex.path.solver.set(timeout=self.options["timeout"]) + ex.path.solver.set(timeout=self.options.solver_timeout_branching) return ex.alias.get(target) @@ -1643,7 +1646,7 @@ def call_unknown() -> None: # FIX: this doesn't capture the case of returndatasize != ret_size actual_ret_size = ret_size else: - actual_ret_size = self.options["unknown_calls_return_size"] + actual_ret_size = self.options.return_size_of_unknown_calls ret = ByteVec() if actual_ret_size > 0: @@ -1761,7 +1764,7 @@ def call_unknown() -> None: # uninterpreted unknown calls funsig = extract_funsig(arg) - if funsig in self.options["unknown_calls"]: + if funsig in self.unknown_calls: self.logs.add_uninterpreted_unknown_call(funsig, to, arg) call_unknown() return @@ -1955,8 +1958,8 @@ def jumpi( if potential_true and potential_false: # for loop unrolling - follow_true = visited[True] < self.options["max_loop"] - follow_false = visited[False] < self.options["max_loop"] + follow_true = visited[True] < self.options.loop + follow_false = visited[False] < self.options.loop if not (follow_true and follow_false): self.logs.bounded_loops.append(jid) else: @@ -2005,14 +2008,10 @@ def jump(self, ex: Exec, stack: List[Tuple[Exec, int]], step_id: int) -> None: stack.push(ex, step_id) # otherwise, create a new execution for feasible targets - elif self.options["sym_jump"]: + elif self.options.symbolic_jump: for target in ex.pgm.valid_jump_destinations(): target_reachable = simplify(dst == target) if ex.check(target_reachable) != unsat: # jump - if self.options.get("debug"): - print( - f"We can jump to {target} with model {ex.path.solver.model()}" - ) new_ex = self.create_branch(ex, target_reachable, target) stack.push(new_ex, step_id) else: @@ -2098,12 +2097,11 @@ def finalize(ex: Exec): insn = ex.current_instruction() opcode = insn.opcode - max_depth = self.options.get("max_depth", 0) - if max_depth and step_id > max_depth: + if (max_depth := self.options.depth) and step_id > max_depth: continue # TODO: clean up - if self.options.get("log"): + if self.options.log: if opcode == EVM.JUMPI: self.steps[step_id] = {"parent": prev_step_id, "exec": str(ex)} # elif opcode == EVM.CALL: @@ -2112,8 +2110,8 @@ def finalize(ex: Exec): # self.steps[step_id] = {'parent': prev_step_id, 'exec': ex.summary()} self.steps[step_id] = {"parent": prev_step_id, "exec": str(ex)} - if self.options.get("print_steps"): - print(ex.dump(print_mem=self.options.get("print_mem", False))) + if self.options.print_steps: + print(ex.dump(print_mem=self.options.print_mem)) if opcode in [EVM.STOP, EVM.INVALID, EVM.REVERT, EVM.RETURN]: if opcode == EVM.STOP: @@ -2430,7 +2428,7 @@ def finalize(ex: Exec): ) ) else: - if self.options["debug"]: + if self.options.debug: print( f"Warning: the use of symbolic BYTE indexing may potentially impact the performance of symbolic reasoning: BYTE {idx} {w}" ) @@ -2482,7 +2480,7 @@ def finalize(ex: Exec): continue except HalmosException as err: - if self.options["debug"]: + if self.options.debug: print(err) ex.halt(data=None, error=err) diff --git a/tests/test_cli.py b/tests/test_cli.py index 30550674..e1a8cbf6 100644 --- a/tests/test_cli.py +++ b/tests/test_cli.py @@ -9,7 +9,7 @@ from halmos.__main__ import str_abi, run_bytecode, FunctionInfo -from test_fixtures import args, options +from test_fixtures import args @pytest.fixture diff --git a/tests/test_fixtures.py b/tests/test_fixtures.py index b5875a29..312349c0 100644 --- a/tests/test_fixtures.py +++ b/tests/test_fixtures.py @@ -2,8 +2,7 @@ from halmos.config import default_config from halmos.sevm import SEVM -from halmos.__main__ import mk_options, mk_solver -import halmos.__main__ +from halmos.__main__ import mk_solver @pytest.fixture @@ -12,13 +11,8 @@ def args(): @pytest.fixture -def options(args): - return mk_options(args) - - -@pytest.fixture -def sevm(options): - return SEVM(options) +def sevm(args): + return SEVM(args) @pytest.fixture diff --git a/tests/test_sevm.py b/tests/test_sevm.py index 3c45b7e2..2aa17dac 100644 --- a/tests/test_sevm.py +++ b/tests/test_sevm.py @@ -27,7 +27,7 @@ from halmos.__main__ import mk_block -from test_fixtures import args, options, sevm, solver +from test_fixtures import args, sevm, solver caller = BitVec("msg_sender", 160) diff --git a/tests/test_traces.py b/tests/test_traces.py index 9861cc22..a626f10e 100644 --- a/tests/test_traces.py +++ b/tests/test_traces.py @@ -3,7 +3,7 @@ import subprocess from dataclasses import dataclass -from typing import Dict, List, Any, Optional +from typing import Dict, Any, Optional from z3 import * @@ -12,7 +12,6 @@ from halmos.exceptions import * from halmos.sevm import ( CallContext, - CallOutput, Contract, EventLog, Exec, @@ -25,7 +24,7 @@ int_of, ) from halmos.utils import EVM -from test_fixtures import args, options, sevm +from test_fixtures import args, sevm import halmos.sevm From a0ea38df4390fa275ee206b35db1bb0bcf9ccbe0 Mon Sep 17 00:00:00 2001 From: karmacoma Date: Fri, 31 May 2024 09:26:48 -0700 Subject: [PATCH 17/19] remove spurious checks --- src/halmos/config.py | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) diff --git a/src/halmos/config.py b/src/halmos/config.py index f574ea65..f2d77652 100644 --- a/src/halmos/config.py +++ b/src/halmos/config.py @@ -383,7 +383,7 @@ def __getattribute__(self, name): # look up value in parent object parent = object.__getattribute__(self, "_parent") - if value is None and parent is not None: + if parent is not None: return getattr(parent, name) return value @@ -408,8 +408,8 @@ def value_with_source(self, name: str) -> Tuple[Any, str]: return (value, self._source) # look up value in parent object - parent = object.__getattribute__(self, "_parent") - if value is None and self._parent is not None: + parent = self._parent + if parent is not None: return parent.value_with_source(name) return (value, self._source) From 7ebc21332257edb46e945041d0ea0a4d37b42592 Mon Sep 17 00:00:00 2001 From: karmacoma Date: Fri, 31 May 2024 09:33:51 -0700 Subject: [PATCH 18/19] config tweaks --- src/halmos/config.py | 14 +++++++++++--- 1 file changed, 11 insertions(+), 3 deletions(-) diff --git a/src/halmos/config.py b/src/halmos/config.py index f2d77652..eb0f615a 100644 --- a/src/halmos/config.py +++ b/src/halmos/config.py @@ -106,6 +106,7 @@ class Config: help="run tests in contracts matching the given regex. Ignored if the --contract name is given.", global_default="", metavar="CONTRACT_NAME_REGEX", + short="mc", ) function: str = arg( @@ -128,13 +129,15 @@ class Config: ) width: int = arg( - help="set the max number of paths", - global_default=2**16, + help="set the max number of paths, 0 for unlimited", + global_default=0, metavar="MAX_WIDTH", ) depth: int = arg( - help="set the max path length", global_default=None, metavar="MAX_DEPTH" + help="set the maximum length in steps of a single path, 0 for unlimited", + global_default=0, + metavar="MAX_DEPTH", ) array_lengths: str = arg( @@ -143,6 +146,11 @@ class Config: metavar="NAME1=LENGTH1,NAME2=LENGTH2,...", ) + # default set of selectors: + # - IERC721.onERC721Received + # - IERC1271.isValidSignature + # - IERC1155.onERC1155Received + # - IERC1155.onERC1155BatchReceived uninterpreted_unknown_calls: str = arg( help="use uninterpreted abstractions for unknown external calls with the given function signatures", global_default="0x150b7a02,0x1626ba7e,0xf23a6e61,0xbc197c81", From 2db8e294d7de636d2abc0e196d33204889ea702a Mon Sep 17 00:00:00 2001 From: karmacoma Date: Fri, 31 May 2024 11:41:07 -0700 Subject: [PATCH 19/19] fix width check --- src/halmos/__main__.py | 3 ++- 1 file changed, 2 insertions(+), 1 deletion(-) diff --git a/src/halmos/__main__.py b/src/halmos/__main__.py index 3bb3ce84..e67b5f69 100644 --- a/src/halmos/__main__.py +++ b/src/halmos/__main__.py @@ -774,7 +774,8 @@ def future_callback(future_model): elif not error: normal += 1 - if len(result_exs) >= args.width: + # 0 width is unlimited + if args.width and len(result_exs) >= args.width: break timer.create_subtimer("models")