example halmos.toml (#299)

Co-authored-by: Daejun Park <[email protected]>

.gitignore

@@ -21,3 +21,6 @@ venv/
 # Foundry build files
 cache/
 out/
+
+# VS Code
+.vscode/

src/halmos/config.py

@@ -30,6 +30,7 @@ def arg(
     choices: Optional[str] = None,
     short: Optional[str] = None,
     countable: bool = False,
+    global_default_str: Optional[str] = None,
 ):
     return field(
         default=None,
@@ -41,6 +42,7 @@ def arg(
             "choices": choices,
             "short": short,
             "countable": countable,
+            "global_default_str": global_default_str,
         },
     )
 
@@ -86,19 +88,23 @@ 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",
+        metavar="ROOT",
+        global_default=os.getcwd,
+        global_default_str="current working directory",
     )
 
-    root: str = arg(
-        help="Project root directory", global_default=os.getcwd(), metavar="PATH"
+    config: str = arg(
+        help="path to the config file",
+        metavar="FILE",
+        global_default=lambda: os.path.join(os.getcwd(), "halmos.toml"),
+        global_default_str="ROOT/halmos.toml",
     )
 
     contract: str = arg(
         help="run tests in the given contract. Shortcut for `--match-contract '^{NAME}$'`.",
-        global_default=None,
+        global_default="",
         metavar="CONTRACT_NAME",
     )
 
@@ -129,13 +135,13 @@ class Config:
     )
 
     width: int = arg(
-        help="set the max number of paths, 0 for unlimited",
+        help="set the max number of paths; 0 means unlimited",
         global_default=0,
         metavar="MAX_WIDTH",
     )
 
     depth: int = arg(
-        help="set the maximum length in steps of a single path, 0 for unlimited",
+        help="set the maximum length in steps of a single path; 0 means unlimited",
         global_default=0,
         metavar="MAX_DEPTH",
     )
@@ -294,7 +300,7 @@ class Config:
     ### Build options
 
     forge_build_out: str = arg(
-        help="forge build artifacts directory name (default: 'out/')",
+        help="forge build artifacts directory name",
         metavar="DIRECTORY_NAME",
         global_default="out",
         group=build,
@@ -331,7 +337,7 @@ class Config:
     )
 
     solver_command: str = arg(
-        help="use the given command when invoking the solver, e.g. `z3 -model`",
+        help="use the given command when invoking the solver",
         global_default=None,
         metavar="COMMAND",
         group=solver,
@@ -343,9 +349,10 @@ class Config:
 
     solver_threads: int = arg(
         help="set the number of threads for parallel solvers",
-        global_default=os.cpu_count() or 1,
         metavar="N",
         group=solver,
+        global_default=(lambda: os.cpu_count() or 1),
+        global_default_str="number of CPUs",
     )
 
     ### Experimental options
@@ -528,9 +535,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)
-        if default_value != MISSING:
-            values[field.name] = default_value
+        default = field.metadata.get("global_default", MISSING)
+        if default == MISSING:
+            continue
+
+        values[field.name] = default() if callable(default) else default
 
     return Config(_parent=None, _source="default", **values)
 
@@ -574,7 +583,9 @@ def _create_arg_parser() -> argparse.ArgumentParser:
             # 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})"
+                default_str = field_info.metadata.get("global_default_str", None)
+                default_str = repr(default) if default_str is None else default_str
+                arg_help += f" (default: {default_str})"
 
             kwargs = {
                 "help": arg_help,
@@ -611,8 +622,72 @@ def toml_parser():
 _toml_parser = _create_toml_parser()
 
 
-if __name__ == "__main__":
-    parser = arg_parser()
-    args = parser.parse_args()
+# can generate a sample config file using:
+# python -m halmos.config ARGS > halmos.toml
+def main():
+    def _to_toml_str(value: Any, type) -> str:
+        assert value is not None
+        if type == str:
+            return f'"{value}"'
+        if type == bool:
+            return str(value).lower()
+        return str(value)
+
+    args = arg_parser().parse_args()
     config = default_config().with_overrides(source="command-line", **vars(args))
-    print(config.formatted_layers())
+
+    # devs can have a little easter egg
+    lines = [
+        "#     ___       ___       ___       ___       ___       ___",
+        "#    /\\__\\     /\\  \\     /\\__\\     /\\__\\     /\\  \\     /\\  \\",
+        "#   /:/__/_   /::\\  \\   /:/  /    /::L_L_   /::\\  \\   /::\\  \\",
+        "#  /::\\/\\__\\ /::\\:\\__\\ /:/__/    /:/L:\\__\\ /:/\\:\\__\\ /\\:\\:\\__\\",
+        "#  \\/\\::/  / \\/\\::/  / \\:\\  \\    \\/_/:/  / \\:\\/:/  / \\:\\:\\/__/",
+        "#    /:/  /    /:/  /   \\:\\__\\     /:/  /   \\::/  /   \\::/  /",
+        "#    \\/__/     \\/__/     \\/__/     \\/__/     \\/__/     \\/__/",
+    ]
+
+    lines.append("\n[global]")
+    current_group_name = None
+
+    for field_info in fields(config):
+        if field_info.metadata.get(internal, False):
+            # skip internal fields
+            continue
+
+        name = field_info.name.replace("_", "-")
+        if name in ["config", "root", "version"]:
+            # skip fields that don't make sense in a config file
+            continue
+
+        group_name = field_info.metadata.get("group", None)
+        if group_name != current_group_name:
+            separator = "#" * 80
+            lines.append(f"\n{separator}")
+            lines.append(f"# {group_name: ^76} #")
+            lines.append(separator)
+            current_group_name = group_name
+
+        arg_help = field_info.metadata.get("help", "")
+        arg_help_tokens = arg_help.split(". ")  # split on sentences
+        arg_help_str = "\n# ".join(arg_help_tokens)
+        lines.append(f"\n# {arg_help_str}")
+
+        (value, source) = config.value_with_source(field_info.name)
+        default = field_info.metadata.get("global_default", None)
+
+        # callable defaults mean that the default value is not a hardcoded constant
+        # it depends on the context, so don't emit it in the config file unless it
+        # is explicitly set by the user on the command line
+        if value is None or (callable(default) and source != "command-line"):
+            metavar = field_info.metadata.get("metavar", None)
+            lines.append(f"# {name} = {metavar}")
+        else:
+            value_str = _to_toml_str(value, field_info.type)
+            lines.append(f"{name} = {value_str}")
+
+    print("\n".join(lines))
+
+
+if __name__ == "__main__":
+    main()

tests/regression/halmos.toml

@@ -0,0 +1,148 @@
+[global]
+
+# run tests in the given contract
+# Shortcut for `--match-contract '^{NAME}$'`.
+contract = ""
+
+# run tests in contracts matching the given regex
+# Ignored if the --contract name is given.
+match-contract = ""
+
+# run tests matching the given prefix
+# Shortcut for `--match-test '^{PREFIX}'`.
+function = "check_"
+
+# run tests matching the given regex
+# The --function prefix is automatically added, unless the regex starts with '^'.
+match-test = ""
+
+# set loop unrolling bounds
+loop = 2
+
+# set the max number of paths; 0 means unlimited
+width = 0
+
+# set the maximum length in steps of a single path; 0 means unlimited
+depth = 0
+
+# set the length of dynamic-sized arrays including bytes and string (default: loop unrolling bound)
+# array-lengths = NAME1=LENGTH1,NAME2=LENGTH2,...
+
+# use uninterpreted abstractions for unknown external calls with the given function signatures
+uninterpreted-unknown-calls = "0x150b7a02,0x1626ba7e,0xf23a6e61,0xbc197c81"
+
+# set the byte size of return data from uninterpreted unknown external calls
+return-size-of-unknown-calls = 32
+
+# Select one of the available storage layout models
+# The generic model should only be necessary for vyper, huff, or unconventional storage patterns in yul.
+storage-layout = "solidity"
+
+# set default storage values to symbolic
+symbolic-storage = false
+
+# set msg.sender symbolic
+symbolic-msg-sender = false
+
+# do not run the constructor of test contracts
+no-test-constructor = false
+
+# allow the usage of FFI to call external functions
+ffi = false
+
+################################################################################
+#                              Debugging options                               #
+################################################################################
+
+# increase verbosity levels: -v, -vv, -vvv, ...
+verbose = 0
+
+# print statistics
+statistics = false
+
+# run in debug mode
+debug = false
+
+# log every execution steps in JSON
+# log = LOG_FILE_PATH
+
+# output test results in JSON
+# json-output = JSON_FILE_PATH
+
+# include minimal information in the JSON output
+minimal-json-output = false
+
+# print every execution step
+print-steps = false
+
+# when --print-steps is enabled, also print memory contents
+print-mem = false
+
+# print all final execution states
+print-states = false
+
+# print failed execution states
+print-failed-states = false
+
+# print blocked execution states
+print-blocked-states = false
+
+# print setup execution states
+print-setup-states = false
+
+# print full counterexample model
+print-full-model = false
+
+# stop after a counterexample is found
+early-exit = false
+
+# dump SMT queries for assertion violations
+dump-smt-queries = false
+
+################################################################################
+#                                Build options                                 #
+################################################################################
+
+# forge build artifacts directory name
+forge-build-out = "out"
+
+################################################################################
+#                                Solver options                                #
+################################################################################
+
+# interpret constant power up to N
+smt-exp-by-const = 2
+
+# set timeout (in milliseconds) for solving branching conditions; 0 means no timeout
+solver-timeout-branching = 1
+
+# set timeout (in milliseconds) for solving assertion violation conditions; 0 means no timeout
+solver-timeout-assertion = 1000
+
+# set memory limit (in megabytes) for the solver; 0 means no limit
+solver-max-memory = 0
+
+# use the given command when invoking the solver
+# solver-command = COMMAND
+
+# run assertion solvers in parallel
+solver-parallel = false
+
+# set the number of threads for parallel solvers
+# solver-threads = N
+
+################################################################################
+#                             Experimental options                             #
+################################################################################
+
+# execute the given bytecode
+# bytecode = HEX_STRING
+
+# reset the bytecode of given addresses after setUp()
+# reset-bytecode = ADDR1=CODE1,ADDR2=CODE2,...
+
+# run tests in parallel
+test-parallel = false
+
+# support symbolic jump destination
+symbolic-jump = false