Use finite times and intercept time.sleep

Author: pschanely

crosshair/libimpl/timelib.py

@@ -1,27 +1,45 @@
 import time as real_time
 from inspect import Signature
 from math import isfinite
-from typing import Any, Callable
+from typing import Any, Literal
 
-from crosshair.core import FunctionInterps
+from crosshair.core import register_patch
 from crosshair.register_contract import register_contract
 from crosshair.statespace import context_statespace
 from crosshair.tracers import NoTracing
 
 
-def _gte_last(fn: Callable, value: Any) -> bool:
+class EarliestPossibleTime:
+    monotonic: float = 0.0
+    process_time: float = 0.0
+
+    def __init__(self, *a):
+        pass
+
+
+# Imprecision at high values becomes a sort of artificial problem
+_UNREALISTICALLY_LARGE_TIME_FLOAT = float(60 * 60 * 24 * 365 * 100_000)
+
+
+def _gte_last(kind: Literal["monotonic", "process_time"], value: Any) -> bool:
+    with NoTracing():
+        earliest_times = context_statespace().extra(EarliestPossibleTime)
+        threshold = getattr(earliest_times, kind)
+        setattr(earliest_times, kind, value)
+    return all([threshold <= value, value < _UNREALISTICALLY_LARGE_TIME_FLOAT])
+
+
+def _sleep(value: float) -> None:
     with NoTracing():
-        interps = context_statespace().extra(FunctionInterps)
-        previous = interps._interpretations[fn]
-        if len(previous) < 2:
-            return True
-    return value >= previous[-2]
+        earliest_times = context_statespace().extra(EarliestPossibleTime)
+    earliest_times.monotonic += value
+    return None
 
 
 def make_registrations():
     register_contract(
         real_time.time,
-        post=lambda __return__: __return__ > 0.0,
+        post=lambda __return__: __return__ > 0.0 and isfinite(__return__),
         sig=Signature(parameters=[], return_annotation=float),
     )
     register_contract(
@@ -31,23 +49,24 @@ def make_registrations():
     )
     register_contract(
         real_time.monotonic,
-        post=lambda __return__: isfinite(__return__)
-        and _gte_last(real_time.monotonic, __return__),
+        post=lambda __return__: _gte_last("monotonic", __return__)
+        and isfinite(__return__),
         sig=Signature(parameters=[], return_annotation=float),
     )
     register_contract(
         real_time.monotonic_ns,
-        post=lambda __return__: isfinite(__return__)
-        and _gte_last(real_time.monotonic_ns, __return__),
+        post=lambda __return__: _gte_last("monotonic", __return__ / 1_000_000_000),
         sig=Signature(parameters=[], return_annotation=int),
     )
     register_contract(
         real_time.process_time,
-        post=lambda __return__: _gte_last(real_time.process_time, __return__),
+        post=lambda __return__: _gte_last("process_time", __return__)
+        and isfinite(__return__),
         sig=Signature(parameters=[], return_annotation=float),
     )
     register_contract(
         real_time.process_time_ns,
-        post=lambda __return__: _gte_last(real_time.process_time_ns, __return__),
+        post=lambda __return__: _gte_last("process_time", __return__ / 1_000_000_000),
         sig=Signature(parameters=[], return_annotation=int),
     )
+    register_patch(real_time.sleep, _sleep)

crosshair/libimpl/timelib_test.py

@@ -2,7 +2,7 @@
 
 import pytest
 
-from crosshair.statespace import CONFIRMED, POST_FAIL
+from crosshair.statespace import CANNOT_CONFIRM, CONFIRMED, POST_FAIL
 from crosshair.test_util import check_states
 
 
@@ -69,4 +69,14 @@ def f():
         start = time.monotonic_ns()
         return time.monotonic_ns() - start
 
-    check_states(f, CONFIRMED)
+    check_states(f, CANNOT_CONFIRM)
+
+
+def test_sleep():
+    def f():
+        """post: _ >= 60.0"""
+        start = time.monotonic()
+        time.sleep(60.01)
+        return time.monotonic() - start
+
+    check_states(f, CANNOT_CONFIRM)

doc/source/changelog.rst

@@ -14,6 +14,10 @@ Version 0.0.85
 
   * Do not always realize symbolic booleans on identity comparisons.
   * Start making preparations for Python 3.14 (as of alpha 6)
+  * Do not let time functions return ``float("inf")``
+    (fixes `#345 <https://github.com/pschanely/CrossHair/issues/345>`__)
+  * Do not actually sleep when encountering ``time.sleep()``!
+    (fixes `#346 <https://github.com/pschanely/CrossHair/issues/346>`__)
 
 
 Version 0.0.84