Skip to content
Merged
Show file tree
Hide file tree
Changes from all commits
Commits
File filter

Filter by extension

Filter by extension

Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
14 changes: 9 additions & 5 deletions ethcheck/ethcheck.py
Original file line number Diff line number Diff line change
Expand Up @@ -12,17 +12,21 @@
from list_forks import list_forks
import subprocess
import ast
import pkg_resources
import importlib.util
import argparse
import generate_pytest

def get_file_path(module_name):
mainnet_file = 'mainnet.py'
spec_file = 'spec.py'
resource_path = pkg_resources.resource_filename(module_name, mainnet_file)
# Locate the fork's spec source inside the installed eth2spec package without
# importing the fork body. importlib.util.find_spec replaces the removed
# pkg_resources.resource_filename (dropped from setuptools >= 81); it only
# needs the package directory, so it avoids pulling in the fork's heavy deps.
spec = importlib.util.find_spec(module_name)
pkg_dir = spec.submodule_search_locations[0]
resource_path = os.path.join(pkg_dir, 'mainnet.py')
generate_pytest.module_name = 'mainnet'
if not os.path.exists(resource_path):
resource_path = pkg_resources.resource_filename(module_name, spec_file)
resource_path = os.path.join(pkg_dir, 'spec.py')
generate_pytest.module_name = 'spec'
return resource_path

Expand Down
38 changes: 23 additions & 15 deletions tests/test_verify_function.py
Original file line number Diff line number Diff line change
Expand Up @@ -22,12 +22,17 @@ def __init__(self, stdout="", stderr=""):
self.returncode = 0


def fake_subprocess_run(esbmc_stdout="", esbmc_stderr="",
esbmc_timeout=False, pytest_outcome="pass"):
def fake_subprocess_run(esbmc_stdout="", esbmc_stderr="", esbmc_timeout=False,
generates_testcase=False, pytest_outcome="pass"):
"""Build a stub for ``subprocess.run`` used inside ``verify_function``.

The ESBMC call and the pytest confirmation call are told apart by argv
(``pytest`` is always invoked as ``['pytest', <file>]``).
(``pytest`` is always invoked as ``['pytest', <file>]``). When
``generates_testcase`` is set, the ESBMC stub drops a ``testcase.xml`` in
the cwd, modelling ``--generate-testcase`` finding a trace. This mirrors
reality: ``verify_function`` removes any stale ``testcase.xml`` *before*
invoking ESBMC, so only the binary recreating it drives the confirmation
branch -- a pre-seeded file would be deleted on entry.
"""
def _run(cmd, *_args, **_kwargs):
if cmd and cmd[0] == "pytest":
Expand All @@ -37,6 +42,9 @@ def _run(cmd, *_args, **_kwargs):
# ESBMC invocation.
if esbmc_timeout:
raise subprocess.TimeoutExpired(cmd, 10)
if generates_testcase:
with open("testcase.xml", "w", encoding="utf-8") as fh:
fh.write("<testcase/>")
return FakeCompleted(stdout=esbmc_stdout, stderr=esbmc_stderr)

return _run
Expand Down Expand Up @@ -93,40 +101,40 @@ def test_failed_without_testcase_prints_counterexample(run_in_tmp, monkeypatch,
def test_failed_pytest_pass_prints_check_and_removes_testcase(run_in_tmp, monkeypatch, capsys):
# ESBMC found a trace and emitted testcase.xml, but pytest does not confirm
# the bug -> report ✓ and clean up testcase.xml so it can't mis-test later.
(run_in_tmp / "testcase.xml").write_text("<testcase/>")
monkeypatch.setattr(ec, "generate_python_script", lambda *a, **k: None)
esbmc = "[Counterexample]\nState 1\nVERIFICATION FAILED\n"
monkeypatch.setattr(ec.subprocess, "run",
fake_subprocess_run(esbmc_stdout=esbmc, pytest_outcome="pass"))
fake_subprocess_run(esbmc_stdout=esbmc, generates_testcase=True,
pytest_outcome="pass"))
ec.verify_function("notabug", COMMAND)
out = capsys.readouterr().out
assert "notabug ✓" in out
assert not (run_in_tmp / "testcase.xml").exists()


def test_failed_pytest_confirms_exits_3_and_removes_testcase(run_in_tmp, monkeypatch, capsys):
(run_in_tmp / "testcase.xml").write_text("<testcase/>")
def test_failed_pytest_confirms_returns_failed_and_removes_testcase(run_in_tmp, monkeypatch, capsys):
# ESBMC trace + pytest reproduces it -> confirmed counterexample. verify_function
# reports ✗ and returns 'failed'; the process exit code (3) is the caller's job
# via exit_code_for, so a confirmed bug does not abort the batch mid-run.
monkeypatch.setattr(ec, "generate_python_script", lambda *a, **k: None)
esbmc = "[Counterexample]\nState 1\nVERIFICATION FAILED\n"
monkeypatch.setattr(ec.subprocess, "run",
fake_subprocess_run(esbmc_stdout=esbmc, pytest_outcome="fail"))
with pytest.raises(SystemExit) as exc:
ec.verify_function("realbug", COMMAND)
assert exc.value.code == 3
fake_subprocess_run(esbmc_stdout=esbmc, generates_testcase=True,
pytest_outcome="fail"))
assert ec.verify_function("realbug", COMMAND) == "failed"
assert "realbug ✗" in capsys.readouterr().out
# Cleanup must still run on the exit path (finally).
# Cleanup must still run on the failure path (finally).
assert not (run_in_tmp / "testcase.xml").exists()


def test_failed_testcase_generation_valueerror_removes_testcase(run_in_tmp, monkeypatch, capsys):
(run_in_tmp / "testcase.xml").write_text("<testcase/>")

def _raise(*_a, **_k):
raise ValueError("cannot build testcase")

monkeypatch.setattr(ec, "generate_python_script", _raise)
esbmc = "[Counterexample]\nState 1\nVERIFICATION FAILED\n"
monkeypatch.setattr(ec.subprocess, "run", fake_subprocess_run(esbmc_stdout=esbmc))
monkeypatch.setattr(ec.subprocess, "run",
fake_subprocess_run(esbmc_stdout=esbmc, generates_testcase=True))
ec.verify_function("ungen", COMMAND)
out = capsys.readouterr().out
assert "ungen ✗" in out
Expand Down
Loading