Fix config precedence: command line options now have highest precedence (#544)

Author: Copilot

.github/workflows/test.yml

@@ -58,5 +58,16 @@ jobs:
         run: |
           uv sync --extra dev
 
+      - name: Write halmos.toml
+        shell: bash
+        run: |
+          uv run python -m halmos.config \
+            --storage-layout ${{ matrix.storage-layout }} \
+            ${{ matrix.cache-solver }} \
+            | tee tests/regression/halmos.toml
+
       - name: Run pytest
-        run: uv run pytest -v -k "not long and not ffi" --ignore=tests/lib --halmos-options="-st --disable-gc --solver-threads 1 --storage-layout ${{ matrix.storage-layout }} ${{ matrix.cache-solver }} --solver-timeout-assertion 0 ${{ inputs.halmos-options }}" ${{ inputs.pytest-options }}
+        shell: bash
+        run: |
+          uv run pytest -v -k "not long and not ffi" --ignore=tests/lib \
+            --halmos-options="-st --disable-gc --solver-threads 1 ${{ inputs.halmos-options }}" ${{ inputs.pytest-options }}

src/halmos/config.py

@@ -10,7 +10,7 @@
 from dataclasses import MISSING, dataclass, fields
 from dataclasses import field as dataclass_field
 from enum import Enum, IntEnum
-from functools import cached_property
+from functools import cached_property, lru_cache
 from typing import Any
 
 import toml
@@ -48,14 +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 = 4
+    contract_annotation = 3
 
     # function-level annotation (e.g. @custom:halmos --some-option)
-    function_annotation = 5
+    function_annotation = 4
+
+    # from command line, highest precedence
+    command_line = 5
 
 
 # helper to define config fields
@@ -639,25 +639,33 @@ class Config:
 
     ### Methods
 
-    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.
+    def __hash__(self):
+        return id(self)
 
-        Because of this, printing a Config object will show a "flattened/resolved" view of the configuration.
+    # cachable because each layer is immutable
+    @lru_cache(maxsize=64)  # noqa: B019
+    def __getattribute__(self, name):
+        """
+        Look up values based on precedence, where higher ConfigSource values override lower ones.
         """
+        # Handle internal attributes normally
+        if name[0] == "_" or name in (
+            "value_with_source",
+            "values",
+            "values_by_layer",
+            "formatted_layers",
+            "resolved_solver_command",
+            "with_overrides",
+        ):
+            return object.__getattribute__(self, name)
 
-        # look up value in current object
-        value = object.__getattribute__(self, name)
-        if value is not None:
+        # For config fields, use precedence-based lookup
+        try:
+            value, _ = self.value_with_source(name)
             return value
-
-        # look up value in parent object
-        parent = object.__getattribute__(self, "_parent")
-        if parent is not None:
-            return getattr(parent, name)
-
-        return value
+        except AttributeError:
+            # Fall back to normal attribute lookup for non-config fields
+            return object.__getattribute__(self, name)
 
     def with_overrides(self, source: ConfigSource, **overrides):
         """Create a new configuration object with some fields overridden.
@@ -673,26 +681,16 @@ def with_overrides(self, source: ConfigSource, **overrides):
             sys.exit(2)
 
     def value_with_source(self, name: str) -> tuple[Any, ConfigSource]:
-        # look up value in current object
-        value = object.__getattribute__(self, name)
-        if value is not None:
-            return (value, self._source)
+        best_value, best_source = None, ConfigSource.void
 
-        # look up value in parent object
-        parent = self._parent
-        if parent is not None:
-            return parent.value_with_source(name)
+        current = self
+        while current is not None:
+            value = object.__getattribute__(current, name)
+            if value is not None and (current_source := current._source) > best_source:
+                best_value, best_source = value, current_source
+            current = current._parent
 
-        return (value, self._source)
-
-    def values_with_sources(self) -> dict[str, tuple[Any, ConfigSource]]:
-        # 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
+        return (best_value, best_source)
 
     def values(self):
         skip_empty = self._parent is not None

tests/regression/test/StdAssertTest.t.sol

@@ -42,11 +42,15 @@ contract StdAssertPassTest is Test {
         assertEq(x, y);
     }
 
+    // times out after 1min with yices and --cache-solver
+    /// @custom:halmos --solver z3
     function check_assertEq(string memory x, string memory y) public {
         vm.assume(keccak256(bytes(x)) == keccak256(bytes(y)));
         assertEq(x, y);
     }
 
+    // times out after 1min with yices and --cache-solver
+    /// @custom:halmos --solver z3
     function check_assertEq(bytes memory x, bytes memory y) public {
         vm.assume(keccak256(x) == keccak256(y));
         assertEq(x, y);
@@ -512,11 +516,15 @@ contract StdAssertFailLogTest is Test {
         assertNotEq(x, y, "");
     }
 
+    // times out after 1min with yices and --cache-solver
+    /// @custom:halmos --solver z3
     function check_assertNotEq(string memory x, string memory y) public {
         vm.assume(!(keccak256(bytes(x)) != keccak256(bytes(y))));
         assertNotEq(x, y, "");
     }
 
+    // times out after 1min with yices and --cache-solver
+    /// @custom:halmos --solver z3
     function check_assertNotEq(bytes memory x, bytes memory y) public {
         vm.assume(!(keccak256(x) != keccak256(y)));
         assertNotEq(x, y, "");

tests/test_config.py

@@ -67,7 +67,9 @@ 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))
+    config_from_args = config.with_overrides(
+        source=ConfigSource.command_line, **vars(args)
+    )
     assert config_from_args.verbose == 6
 
 
@@ -78,7 +80,7 @@ def test_choice_arg(config, parser):
 
     # valid choice works
     args = parser.parse_args(["--storage-layout", "generic"])
-    overrides = config.with_overrides(source="command-line", **vars(args))
+    overrides = config.with_overrides(source=ConfigSource.command_line, **vars(args))
     assert overrides.storage_layout == "generic"
 
 
@@ -380,8 +382,50 @@ def test_solver_resolution_precedence(config):
     # 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",
-    ]
+    # the resolved solver command is derived from the solver option (command line)
+    # because command line has higher precedence than contract annotation
+    assert "cvc5" in " ".join(contract_config.resolved_solver_command)
+
+
+def test_command_line_precedence_over_annotations(config):
+    """Test that command line options have highest precedence, overriding annotations."""
+
+    # Start with default config
+    assert config.solver == "yices"
+
+    # Apply config file override
+    config_file_config = config.with_overrides(ConfigSource.config_file, solver="z3")
+    assert config_file_config.solver == "z3"
+    assert config_file_config.value_with_source("solver") == (
+        "z3",
+        ConfigSource.config_file,
+    )
+
+    # Apply command line override (should have highest precedence)
+    cli_config = config_file_config.with_overrides(
+        ConfigSource.command_line, solver="cvc5"
+    )
+    assert cli_config.solver == "cvc5"
+    assert cli_config.value_with_source("solver") == ("cvc5", ConfigSource.command_line)
+
+    # Apply contract annotation override (should NOT override command line)
+    contract_config = cli_config.with_overrides(
+        ConfigSource.contract_annotation, solver="bitwuzla"
+    )
+    # Command line should still win
+    assert contract_config.solver == "cvc5"
+    assert contract_config.value_with_source("solver") == (
+        "cvc5",
+        ConfigSource.command_line,
+    )
+
+    # Apply function annotation override (should NOT override command line)
+    function_config = contract_config.with_overrides(
+        ConfigSource.function_annotation, solver="yices"
+    )
+    # Command line should still win
+    assert function_config.solver == "cvc5"
+    assert function_config.value_with_source("solver") == (
+        "cvc5",
+        ConfigSource.command_line,
+    )