diff --git a/halmos.toml b/halmos.toml new file mode 100644 index 00000000..9a923647 --- /dev/null +++ b/halmos.toml @@ -0,0 +1,9 @@ +# 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 + +[compile-settings] +array-lengths = 2 \ No newline at end of file diff --git a/pyproject.toml b/pyproject.toml index ba307be3..32698ce6 100644 --- a/pyproject.toml +++ b/pyproject.toml @@ -23,6 +23,7 @@ classifiers = [ requires-python = ">=3.9" dependencies = [ "sortedcontainers>=2.4.0", + "toml", "z3-solver==4.12.6.0", ] dynamic = ["version"] @@ -34,7 +35,7 @@ halmos = "halmos.__main__:main" "Homepage" = "https://github.com/a16z/halmos" [tool.black] -target-versions = ["py39", "py310", "py311", "py312"] +target-version = ["py39", "py310", "py311", "py312"] [tool.pytest.ini_options] # TODO: re-add test_traces.py when we have a better way to support it in CI diff --git a/src/halmos/__main__.py b/src/halmos/__main__.py index 49e1e7e0..a5d09b04 100644 --- a/src/halmos/__main__.py +++ b/src/halmos/__main__.py @@ -1,45 +1,43 @@ # SPDX-License-Identifier: AGPL-3.0 -import os -import sys -import subprocess -import uuid import json +import os import re import signal -import traceback +import subprocess +import sys import time - +import traceback +import uuid from argparse import Namespace -from dataclasses import dataclass, asdict -from importlib import metadata -from enum import Enum from collections import Counter - from concurrent.futures import ProcessPoolExecutor, ThreadPoolExecutor +from dataclasses import asdict, dataclass +from enum import Enum +from importlib import metadata from .bytevec import Chunk, ByteVec +from .calldata import Calldata +from .parser import mk_arg_parser, load_config_file, parse_config from .sevm import * from .utils import ( - create_solver, - hexify, - stringify, - indent_text, NamedTimer, - yellow, + color_error, + color_good, + color_info, + color_warn, + create_solver, cyan, - green, - red, error, + green, + hexify, + indent_text, info, - color_good, - color_warn, - color_info, - color_error, + red, + stringify, + yellow, ) from .warnings import * -from .parser import mk_arg_parser -from .calldata import Calldata StrModel = Dict[str, str] AnyModel = UnionType[Model, StrModel] @@ -1402,6 +1400,10 @@ def _main(_args=None) -> MainResult: 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:]) + if args.version: print(f"Halmos {metadata.version('halmos')}") return MainResult(0) diff --git a/src/halmos/parser.py b/src/halmos/parser.py index d2e43090..71b2cb75 100644 --- a/src/halmos/parser.py +++ b/src/halmos/parser.py @@ -1,7 +1,12 @@ # SPDX-License-Identifier: AGPL-3.0 -import os import argparse +import os +import toml + +from typing import Dict, Optional + +from .utils import warn def mk_arg_parser() -> argparse.ArgumentParser: @@ -110,6 +115,14 @@ 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") @@ -256,3 +269,53 @@ 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 + + with open(path, "r") as f: + return toml.load(f) + + +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 + + 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("-", "_") + + if key not in actions: + warn(f"Unknown config key: {key}") + continue + + value_type, options_strings = actions[key] + + if any(option in commands for option in options_strings): + warn(f"Skipping config key: {key} (command line argument)") + continue + + 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})" + ) + + return args diff --git a/tests/test_parser.py b/tests/test_parser.py new file mode 100644 index 00000000..b2c3f91e --- /dev/null +++ b/tests/test_parser.py @@ -0,0 +1,75 @@ +import argparse +from unittest.mock import mock_open, patch + +import pytest + +from halmos.parser import load_config_file, parse_config + + +@pytest.fixture +def mock_config(): + return { + "settings": { + "depth": 4, + "array-lengths": 2, + } + } + + +@pytest.fixture +def mock_parser(): + parser = argparse.ArgumentParser() + parser.add_argument("--depth", type=int) + parser.add_argument("--array-lengths") + return parser + + +@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 + + +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_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 + + +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") + + +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_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"]) + + assert updated_args.depth == 5 + assert updated_args.array_lengths == 2