[Feature/#125] Enhance configuration management by using toml configu…

…ration file (#296)

Co-authored-by: karmacoma <karma@coma.lol>

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

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

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)

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

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