ci: add ruff to pre-commit and replace black action with pre-commit (a…

…16z#354)

.github/workflows/black.yml

@@ -1,10 +1,11 @@
-name: Lint
+# Deprecated: use pre-commit instead
+# name: Lint
 
-on: [push, pull_request]
+# on: [push, pull_request]
 
-jobs:
-  lint:
-    runs-on: ubuntu-latest
-    steps:
-      - uses: actions/checkout@v4
-      - uses: psf/black@stable
+# jobs:
+#   lint:
+#     runs-on: ubuntu-latest
+#     steps:
+#       - uses: actions/checkout@v4
+#       - uses: psf/black@stable

.github/workflows/pre-commit.yml

@@ -0,0 +1,11 @@
+name: pre-commit
+
+on: [push, pull_request]
+
+jobs:
+  pre-commit:
+    runs-on: ubuntu-latest
+    steps:
+    - uses: actions/checkout@v4
+    - uses: actions/setup-python@v3
+    - uses: pre-commit/[email protected]

.pre-commit-config.yaml

@@ -1,10 +1,22 @@
 repos:
-  - repo: https://github.com/psf/black
-    rev: 23.7.0
-    hooks:
-      - id: black
-        # It is recommended to specify the latest version of Python
-        # supported by your project here, or alternatively use
-        # pre-commit's default_language_version, see
-        # https://pre-commit.com/#top_level-default_language_version
-        language_version: python3.12
+  # - repo: https://github.com/psf/black
+  #   rev: 23.7.0
+  #   hooks:
+  #     - id: black
+  #       # It is recommended to specify the latest version of Python
+  #       # supported by your project here, or alternatively use
+  #       # pre-commit's default_language_version, see
+  #       # https://pre-commit.com/#top_level-default_language_version
+  #       language_version: python3.12
+
+- repo: https://github.com/astral-sh/ruff-pre-commit
+  # Ruff version.
+  rev: v0.6.2
+  hooks:
+    # Run the linter.
+    - id: ruff
+      # don't autofix by default, this runs in CI
+      # to run fix locally, use `ruff check src/ --fix`
+      # args: [ --fix ]
+    # Run the formatter.
+    - id: ruff-format

pyproject.toml

@@ -54,3 +54,6 @@ select = [
 ignore = [
     "E501",  # line too long
 ]
+exclude = [
+    "tests/lib/**"
+]

src/halmos/__main__.py

@@ -76,7 +76,6 @@
     green,
     hexify,
     indent_text,
-    info,
     red,
     stringify,
     unbox_int,

src/halmos/sevm.py

@@ -65,6 +65,7 @@
     OutOfGasError,
     PathEndingException,
     Revert,
+    StackUnderflowError,
     WriteInStaticContext,
 )
 from .utils import (
@@ -414,6 +415,8 @@ def push(self, v: Word) -> None:
             self.stack.append(simplify(v))
 
     def pop(self) -> Word:
+        if not self.stack:
+            raise StackUnderflowError()
         return self.stack.pop()
 
     def peek(self, n: int = 1) -> Word:

tests/conftest.py

@@ -1,3 +1,8 @@
+# workaround for ruff removing fixture imports
+# they look unused because of dependency injection by pytest
+from test_fixtures import *  # noqa
+
+
 def pytest_addoption(parser):
     parser.addoption(
         "--halmos-options",

tests/regression/halmos.toml

@@ -135,12 +135,6 @@ solver-parallel = false
 #                             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
 

tests/test_bytevec.py

@@ -1,9 +1,8 @@
 import pytest
+from z3 import BitVec, BitVecVal, Concat, Extract, eq
 
-from z3 import BitVec, BitVecVal, Concat, Extract
-
-from halmos.bytevec import *
-from halmos.utils import concat
+from halmos.bytevec import ByteVec, Chunk, defrag
+from halmos.utils import concat, extract_bytes
 
 
 @pytest.fixture

tests/test_cli.py

@@ -1,13 +1,15 @@
-import pytest
 import json
 
-from z3 import *
+import pytest
+from z3 import (
+    BitVec,
+    BitVecVal,
+    Concat,
+)
 
+from halmos.__main__ import str_abi
+from halmos.sevm import Contract, Instruction, con
 from halmos.utils import EVM, hexify
-from halmos.sevm import con, Contract, Instruction
-from halmos.__main__ import str_abi, FunctionInfo
-
-from test_fixtures import args
 
 
 @pytest.fixture
@@ -76,16 +78,17 @@ def test_decode_mixed_bytecode():
     assert contract[0] == EVM.PUSH20
     assert contract[27] == EVM.RETURN
     assert contract[28] == EVM.STOP  # past the end
-
-    contract.valid_jump_destinations() == set()
+    assert contract.valid_jump_destinations() == set()
 
     # force decoding
     pc = 0
     while pc < len(contract):
         contract.decode_instruction(pc)
         pc = contract.next_pc(pc)
 
-    pcs, insns = zip(*((pc, insn) for (pc, insn) in contract._insn.items()))
+    pcs, insns = zip(
+        *((pc, insn) for (pc, insn) in contract._insn.items()), strict=False
+    )
     opcodes = tuple(insn.opcode for insn in insns)
 
     assert opcodes == (

tests/test_config.py

@@ -1,14 +1,18 @@
+import dataclasses
 import os
 import pickle
+
 import pytest
 
 from halmos.config import (
     Config,
-    default_config,
     arg_parser,
-    toml_parser as get_toml_parser,
+    default_config,
     resolve_config_files,
 )
+from halmos.config import (
+    toml_parser as get_toml_parser,
+)
 
 
 @pytest.fixture
@@ -35,7 +39,7 @@ def test_fresh_config_has_only_None_values():
 
 
 def test_default_config_immutable(config):
-    with pytest.raises(Exception):
+    with pytest.raises(dataclasses.FrozenInstanceError):
         config.solver_threads = 42
 
 
@@ -47,7 +51,7 @@ def test_unknown_keys_config_constructor_raise():
 def test_unknown_keys_config_object_raise():
     config = Config(_parent=None, _source="bogus")
     with pytest.raises(AttributeError):
-        config.unknown_key
+        config.unknown_key  # noqa: B018 (not a useless expression)
 
 
 def test_count_arg(config, parser):
@@ -165,7 +169,7 @@ def test_config_e2e(config, parser, toml_parser):
 
     # then the config object should have the expected values
     assert config.verbose == 3
-    assert config.symbolic_storage == True
+    assert config.symbolic_storage is True
     assert config.loop == 2
 
     # and each value should have the expected source

tests/test_fixtures.py

@@ -1,8 +1,8 @@
 import pytest
 
+from halmos.__main__ import mk_solver
 from halmos.config import default_config
 from halmos.sevm import SEVM
-from halmos.__main__ import mk_solver
 
 
 @pytest.fixture

tests/test_halmos.py

@@ -1,15 +1,12 @@
-import pytest
+import dataclasses
 import json
 
-from typing import Dict
-from dataclasses import asdict
+import pytest
 
 from halmos.__main__ import _main, rendered_calldata
 from halmos.bytevec import ByteVec
 from halmos.sevm import con
 
-from test_fixtures import halmos_options
-
 
 @pytest.mark.parametrize(
     "cmd, expected_path",
@@ -49,7 +46,7 @@
     ),
 )
 def test_main(cmd, expected_path, halmos_options):
-    actual = asdict(_main(cmd + halmos_options.split()))
+    actual = dataclasses.asdict(_main(cmd + halmos_options.split()))
     with open(expected_path, encoding="utf8") as f:
         expected = json.load(f)
     assert expected["exitcode"] == actual["exitcode"]
@@ -64,17 +61,17 @@ def test_main(cmd, expected_path, halmos_options):
     ids=("SetupFailTest",),
 )
 def test_main_fail(cmd, halmos_options):
-    actual = asdict(_main(cmd + halmos_options.split()))
+    actual = dataclasses.asdict(_main(cmd + halmos_options.split()))
     assert actual["exitcode"] != 0
 
 
-def assert_eq(m1: Dict, m2: Dict) -> int:
+def assert_eq(m1: dict, m2: dict) -> int:
     assert list(m1.keys()) == list(m2.keys())
     for c in m1:
         l1 = sorted(m1[c], key=lambda x: x["name"])
         l2 = sorted(m2[c], key=lambda x: x["name"])
         assert len(l1) == len(l2), c
-        for r1, r2 in zip(l1, l2):
+        for r1, r2 in zip(l1, l2, strict=False):
             assert r1["name"] == r2["name"]
             assert r1["exitcode"] == r2["exitcode"], f"{c} {r1['name']}"
             assert r1["num_models"] == r2["num_models"], f"{c} {r1['name']}"

tests/test_mapper.py

@@ -1,7 +1,6 @@
-from typing import List
-
 import json
 import os
+
 import pytest
 
 from halmos.mapper import AstNode, ContractMappingInfo, Mapper, SingletonMeta
@@ -15,14 +14,14 @@ def _read_file(filename):
         # Get the directory of the current test file
         test_dir = request.fspath.dirname
         file_path = os.path.join(test_dir, "data", filename)
-        with open(file_path, "r") as file:
+        with open(file_path) as file:
             return json.load(file)
 
     return _read_file
 
 
 @pytest.fixture
-def ast_nodes() -> List[AstNode]:
+def ast_nodes() -> list[AstNode]:
     return [
         AstNode(
             node_type="type1",

tests/test_prank.py

@@ -1,16 +1,14 @@
 import pytest
-
 from z3 import BitVec
 
 from halmos.cheatcodes import (
+    NO_PRANK,
     Prank,
     PrankResult,
-    NO_PRANK,
-    hevm_cheat_code,
     halmos_cheat_code,
+    hevm_cheat_code,
 )
-
-from halmos.sevm import Message, CallContext
+from halmos.sevm import CallContext, Message
 
 
 @pytest.fixture