Fix solver resolution precedence to preserve original config source priority (#539)

Author: Copilot

src/halmos/__main__.py

@@ -6,6 +6,7 @@
 import logging
 import os
 import re
+import shlex
 import shutil
 import signal
 import subprocess
@@ -109,7 +110,6 @@
     solve_end_to_end,
     solve_low_level,
 )
-from halmos.solvers import get_solver_command
 from halmos.traces import (
     render_trace,
     rendered_address,
@@ -187,7 +187,7 @@ def with_devdoc(args: HalmosConfig, fn_sig: str, contract_json: dict) -> HalmosC
     if not devdoc:
         return args
 
-    overrides = arg_parser().parse_args(devdoc.split())
+    overrides = arg_parser().parse_args(shlex.split(devdoc))
     source = ConfigSource.function_annotation
     return args.with_overrides(source, **vars(overrides))
 
@@ -202,35 +202,11 @@ def with_natspec(
     if not parsed:
         return args
 
-    overrides = arg_parser().parse_args(parsed.split())
+    overrides = arg_parser().parse_args(shlex.split(parsed))
     source = ConfigSource.contract_annotation
     return args.with_overrides(source, **vars(overrides))
 
 
-def with_resolved_solver(args: HalmosConfig) -> HalmosConfig:
-    solver, solver_source = args.value_with_source("solver")
-    solver_command, solver_command_source = args.value_with_source("solver_command")
-
-    # `--solver-command` overrides `--solver` if it is at least as high precedence
-    if solver_command and solver_command_source >= solver_source:
-        if solver_command_source == solver_source:
-            warn(
-                f"--solver-command and --solver are both provided at the same "
-                f"precedence level ({solver_source.name}), "
-                f"--solver-command will be used and --solver will be ignored",
-                allow_duplicate=False,
-            )
-        return args
-
-    # if no `--solver-command` is provided, or `--solver` has higher precedence,
-    # we need to resolve `--solver <name>` to an actual command
-    command = get_solver_command(solver)
-    if not command:
-        raise RuntimeError(f"Solver '{solver}' could not be found or installed.")
-    source = ConfigSource.dynamic_resolution
-    return args.with_overrides(source, solver_command=command)
-
-
 def load_config(_args) -> HalmosConfig:
     config = default_config()
 
@@ -641,8 +617,7 @@ def _compute_frontier(ctx: ContractContext, depth: int) -> Iterator[Exec]:
 
     visited = ctx.visited
 
-    args = with_resolved_solver(ctx.args)
-
+    args = ctx.args
     panic_error_codes = args.panic_error_codes
     flamegraph_enabled = args.flamegraph
 
@@ -1523,10 +1498,9 @@ def run_contract(ctx: ContractContext) -> list[TestResult]:
 
     try:
         setup_config = with_devdoc(args, setup_info.sig, ctx.contract_json)
-        setup_config = with_resolved_solver(setup_config)
 
         if setup_config.debug_config:
-            debug(f"{setup_config.formatted_layers()}")
+            debug(f"config for setUp():\n{setup_config.formatted_layers()}")
 
         setup_solver = mk_solver(setup_config)
         setup_ctx = FunctionContext(
@@ -1634,11 +1608,8 @@ def run_tests(
         try:
             test_config = with_devdoc(args, funsig, ctx.contract_json)
 
-            # resolve the solver command at the function level
-            test_config = with_resolved_solver(test_config)
-
             if debug_config:
-                debug(f"{test_config.formatted_layers()}")
+                debug(f"config for {funsig}:\n{test_config.formatted_layers()}")
 
             max_call_depth = (
                 test_config.invariant_depth if funsig.startswith("invariant_") else 0
@@ -1733,10 +1704,10 @@ def _main(_args=None) -> MainResult:
                 f" and {call_flamegraph.out_filepath}"
             )
         else:
-            error("flamegraph.pl not found in PATH")
-            error("(see https://github.com/brendangregg/FlameGraph)")
-            dynamic_resolution = ConfigSource.dynamic_resolution
-            args = args.with_overrides(dynamic_resolution, flamegraph=False)
+            error(
+                "flamegraph.pl not found in PATH (see https://github.com/brendangregg/FlameGraph)"
+            )
+            return MainResult(1)
 
     #
     # compile

src/halmos/config.py

@@ -3,18 +3,20 @@
 import argparse
 import os
 import re
+import shlex
 import sys
 from collections import OrderedDict
 from collections.abc import Callable, Generator
 from dataclasses import MISSING, dataclass, fields
 from dataclasses import field as dataclass_field
 from enum import Enum, IntEnum
+from functools import cached_property
 from typing import Any
 
 import toml
 
 from halmos.logs import warn
-from halmos.solvers import SOLVERS
+from halmos.solvers import SOLVERS, get_solver_command
 from halmos.utils import parse_time
 
 # common strings
@@ -46,17 +48,14 @@ class ConfigSource(IntEnum):
     # e.g. halmos.toml
     config_file = 2
 
+    # from command line
+    command_line = 3
+
     # contract-level annotation (e.g. @custom:halmos --some-option)
-    contract_annotation = 3
+    contract_annotation = 4
 
     # function-level annotation (e.g. @custom:halmos --some-option)
-    function_annotation = 4
-
-    # from command line
-    command_line = 5
-
-    # dynamic resolution (e.g. after solver resolution)
-    dynamic_resolution = 6
+    function_annotation = 5
 
 
 # helper to define config fields
@@ -561,9 +560,11 @@ class Config:
         group=solver_group,
     )
 
+    # this is the low-level option that overrides the `--solver` option
+    # use `resolved_solver_command` to get the actual command as a list of strings
     solver_command: str = arg(
         help="use the given exact command when invoking the solver (overrides automatic solver detection/download triggered by --solver)",
-        global_default=None,
+        global_default="",
         metavar="COMMAND",
         group=solver_group,
     )
@@ -723,6 +724,38 @@ def formatted_layers(self) -> str:
                 lines.append(f"  {field}: {value}")
         return "\n".join(lines)
 
+    @cached_property
+    def resolved_solver_command(self) -> list[str]:
+        """
+        Dynamically resolve the solver command from the `--solver` and `--solver-command` options.
+        """
+
+        solver, solver_source = self.value_with_source("solver")
+        solver_command, solver_command_source = self.value_with_source("solver_command")
+
+        # `--solver-command` overrides `--solver` if it is at least as high precedence
+        if (
+            solver_command
+            and solver_command_source
+            and solver_command_source >= solver_source
+        ):
+            if solver_command_source == solver_source:
+                warn(
+                    f"--solver-command and --solver are both provided at the same "
+                    f"precedence level ({solver_source.name}), "
+                    f"--solver-command will be used and --solver will be ignored",
+                    allow_duplicate=False,
+                )
+            return shlex.split(solver_command)
+
+        # if no `--solver-command` is provided, or `--solver` has higher precedence,
+        # we need to resolve `--solver <name>` to an actual command
+        command = get_solver_command(solver)
+        if not command:
+            raise RuntimeError(f"Solver '{solver}' could not be found or installed.")
+
+        return command
+
 
 def resolve_config_files(args: list[str], include_missing: bool = False) -> list[str]:
     config_parser = argparse.ArgumentParser()

src/halmos/solve.py

@@ -1,6 +1,7 @@
 # SPDX-License-Identifier: AGPL-3.0
 
 import re
+import shlex
 import subprocess
 from concurrent.futures import ThreadPoolExecutor
 from dataclasses import dataclass, field
@@ -485,21 +486,15 @@ def solve_low_level(path_ctx: PathContext) -> SolverOutput:
     # make sure the smt2 file has been written
     dump(path_ctx)
 
+    solver_command = args.resolved_solver_command + [smt2_filename]
     if args.verbose >= 1:
         print("  Checking with external solver process")
-        print(f"    {args.solver_command} {smt2_filename} > {smt2_filename}.out")
+        print(f"    {shlex.join(solver_command)} > {smt2_filename}.out")
 
     # solver_timeout_assertion == 0 means no timeout,
     # which translates to timeout_seconds=None for subprocess.run
     timeout_seconds = t if (t := args.solver_timeout_assertion) else None
-
-    cmd_list = (
-        args.solver_command.split()
-        if isinstance(args.solver_command, str)
-        else args.solver_command
-    )
-    cmd_with_file = cmd_list + [smt2_filename]
-    future = PopenFuture(cmd_with_file, timeout=timeout_seconds)
+    future = PopenFuture(solver_command, timeout=timeout_seconds)
 
     # starts the subprocess asynchronously
     path_ctx.solving_ctx.executor.submit(future)

tests/test_config.py

@@ -340,3 +340,48 @@ def test_value_with_source(config):
 
     # overrides have higher precedence than defaults
     assert source > ConfigSource.default
+
+
+def test_solver_resolution_precedence(config):
+    # default config
+    assert config.solver == "yices"
+    assert config.solver_command == ""
+
+    # the resolved solver command is derived from the default solver
+    assert "yices" in " ".join(config.resolved_solver_command)
+
+    #########################################################
+    # command line overrides
+    #########################################################
+
+    cli_config = config.with_overrides(ConfigSource.command_line, solver="cvc5")
+    assert cli_config.solver == "cvc5"
+
+    # the solver command is inherited from the default config
+    assert cli_config.solver_command == config.solver_command
+
+    # but the actual command is derived from the solver option (at a higher precedence)
+    assert "cvc5" in " ".join(cli_config.resolved_solver_command)
+
+    #########################################################
+    # contract annotation overrides
+    #########################################################
+
+    contract_config = cli_config.with_overrides(
+        ConfigSource.contract_annotation,
+        solver_command="path/to/bitwuzla --produce-models",
+    )
+    # the solver option is inherited from the command line config
+    assert contract_config.value_with_source("solver") == (
+        "cvc5",
+        ConfigSource.command_line,
+    )
+
+    # the solver command comes from the contract annotation
+    assert contract_config.solver_command == "path/to/bitwuzla --produce-models"
+
+    # the resolved solver command is derived from the contract annotation
+    assert contract_config.resolved_solver_command == [
+        "path/to/bitwuzla",
+        "--produce-models",
+    ]