diff --git a/certora_autosetup/setup/sanity.py b/certora_autosetup/setup/sanity.py index 4bac9804..5433cd85 100644 --- a/certora_autosetup/setup/sanity.py +++ b/certora_autosetup/setup/sanity.py @@ -9,6 +9,7 @@ import asyncio import json +import os import re import time import uuid @@ -191,7 +192,23 @@ class SanityResult(Enum): # Per-job prover timeout (seconds) applied to the exploratory sanity runs. -SANITY_GLOBAL_TIMEOUT = 1200 +SANITY_TIMEOUT_ENV = "AUTOPROVER_SANITY_TIMEOUT" +DEFAULT_SANITY_TIMEOUT = 1200 + + +def sanity_global_timeout() -> int: + """The per-job prover timeout (seconds) for the exploratory sanity runs: ``DEFAULT_SANITY_TIMEOUT``, + or the integer value of ``AUTOPROVER_SANITY_TIMEOUT`` when set (a non-integer or <1 value is ignored + with a warning). Mirrors ``AUTOPROVER_GLOBAL_PROVER_TIMEOUT`` for the sanity phase.""" + raw = os.environ.get(SANITY_TIMEOUT_ENV) + if raw is None: + return DEFAULT_SANITY_TIMEOUT + try: + n = int(raw) + except ValueError: + logger.warning(f"Ignoring non-integer {SANITY_TIMEOUT_ENV}={raw!r}") + return DEFAULT_SANITY_TIMEOUT + return n if n >= 1 else DEFAULT_SANITY_TIMEOUT @dataclass @@ -213,7 +230,7 @@ def get_config_properties(self) -> Dict[str, Any]: # excluded from the analysis), so the rule_sanity sub-checks are pure wasted runtime here. "rule_sanity": "none", # Cap the exploratory sanity runs; only applied to these transient conf copies. - "global_timeout": str(SANITY_GLOBAL_TIMEOUT), + "global_timeout": str(sanity_global_timeout()), } if self.hashing_bound is not None: properties["hashing_length_bound"] = self.hashing_bound @@ -579,7 +596,7 @@ async def _run_sanity_coverage_rerun(self, failing_methods: List[str], completio "coverage_info": "advanced", "method": [method], "rule_sanity": "none", - "global_timeout": str(SANITY_GLOBAL_TIMEOUT), + "global_timeout": str(sanity_global_timeout()), }, f"_coverage_rerun_{i}", target_dir=self._internal_confs_dir, @@ -709,7 +726,7 @@ async def _detect_optimal_hashing_bounds(self) -> Optional[int]: # Cap the detection run; global_timeout is a top-level property, not a prover arg. self.config_manager.update_config_with_properties( - bound_detection_config.path, {"global_timeout": str(SANITY_GLOBAL_TIMEOUT)} + bound_detection_config.path, {"global_timeout": str(sanity_global_timeout())} ) # Submit bound detection job diff --git a/tests/test_sanity_timeout.py b/tests/test_sanity_timeout.py new file mode 100644 index 00000000..f8ea75d9 --- /dev/null +++ b/tests/test_sanity_timeout.py @@ -0,0 +1,25 @@ +"""Unit tests for the AUTOPROVER_SANITY_TIMEOUT override on the sanity phase's per-job timeout.""" + +from certora_autosetup.setup.sanity import ( + DEFAULT_SANITY_TIMEOUT, + SANITY_TIMEOUT_ENV, + sanity_global_timeout, +) + + +class TestSanityGlobalTimeout: + def test_unset_returns_default(self, monkeypatch): + monkeypatch.delenv(SANITY_TIMEOUT_ENV, raising=False) + assert sanity_global_timeout() == DEFAULT_SANITY_TIMEOUT == 1200 + + def test_integer_env_value_used(self, monkeypatch): + monkeypatch.setenv(SANITY_TIMEOUT_ENV, "300") + assert sanity_global_timeout() == 300 + + def test_non_integer_falls_back_to_default(self, monkeypatch): + monkeypatch.setenv(SANITY_TIMEOUT_ENV, "five-minutes") + assert sanity_global_timeout() == DEFAULT_SANITY_TIMEOUT + + def test_non_positive_falls_back_to_default(self, monkeypatch): + monkeypatch.setenv(SANITY_TIMEOUT_ENV, "0") + assert sanity_global_timeout() == DEFAULT_SANITY_TIMEOUT