NotDeterministic diagnostics and weakref support

crosshair/_tracers_test.py

@@ -125,4 +125,4 @@ def test_CTracer_does_not_leak_memory():
         if i == 100:
             usage = mem_usage_kb()
     usage_increase = mem_usage_kb() - usage
-    assert usage_increase < 35
+    assert usage_increase < 200

crosshair/copyext_test.py

@@ -61,5 +61,4 @@ def set(self, a):
 def test_deepcopyext_recursivetype(space):
     recursive_obj = RecursiveType()
     recursive_obj.set(recursive_obj)
-    with ResumedTracing():
-        deepcopyext(recursive_obj, CopyMode.REALIZE, {})
+    deepcopyext(recursive_obj, CopyMode.REALIZE, {})

crosshair/core.py

@@ -76,7 +76,6 @@
     AnalysisMessage,
     CallAnalysis,
     MessageType,
-    NotDeterministic,
     RootNode,
     SimpleStateSpace,
     StateSpace,
@@ -107,6 +106,7 @@
     EvalFriendlyReprContext,
     IdKeyedDict,
     IgnoreAttempt,
+    NotDeterministic,
     ReferencedIdentifier,
     UnexploredPath,
     ch_stack,
@@ -132,15 +132,11 @@
 _OPCODE_PATCHES: List[TracingModule] = []
 
 _PATCH_REGISTRATIONS: Dict[Callable, Callable] = {}
-_PATCH_FN_TYPE_REGISTRATIONS: Dict[type, Callable] = {}
 
 
 class Patched:
     def __enter__(self):
         COMPOSITE_TRACER.patching_module.add(_PATCH_REGISTRATIONS)
-        COMPOSITE_TRACER.patching_module.fn_type_overrides = (
-            _PATCH_FN_TYPE_REGISTRATIONS
-        )
         if len(_OPCODE_PATCHES) == 0:
             raise CrossHairInternal("Opcode patches haven't been loaded yet.")
         for module in _OPCODE_PATCHES:
@@ -152,7 +148,6 @@ def __exit__(self, exc_type, exc_val, exc_tb):
         for module in reversed(self.pushed):
             COMPOSITE_TRACER.pop_config(module)
         COMPOSITE_TRACER.patching_module.pop(_PATCH_REGISTRATIONS)
-        COMPOSITE_TRACER.patching_module.fn_type_overrides = {}
         return False
 
 
@@ -231,8 +226,14 @@ def __exit__(self, exc_type, exc_value, tb) -> bool:
                 debug("Proxy intolerace:", exc_value, "at", format_exc())
                 raise CrosshairUnsupported("Detected proxy intolerance")
             if isinstance(exc_value, (Exception, PreconditionFailed)):
-                if isinstance(exc_value, z3.Z3Exception):
-                    return False  # internal issue: re-raise
+                if isinstance(
+                    exc_value,
+                    (
+                        z3.Z3Exception,  # internal issue, re-raise
+                        NotDeterministic,  # cannot continue to use the solver, re-raise
+                    ),
+                ):
+                    return False
                 # Most other issues are assumed to be user-facing exceptions:
                 lower_frames = extract_tb(sys.exc_info()[2])
                 higher_frames = extract_stack()[:-2]
@@ -488,19 +489,11 @@ def _reset_all_registrations():
     _SIMPLE_PROXIES.clear()
     global _PATCH_REGISTRATIONS
     _PATCH_REGISTRATIONS.clear()
-    global _PATCH_FN_TYPE_REGISTRATIONS
-    _PATCH_FN_TYPE_REGISTRATIONS.clear()
     global _OPCODE_PATCHES
     _OPCODE_PATCHES.clear()
     clear_contract_registrations()
 
 
-def register_fn_type_patch(typ: type, patch_value: Callable[[Callable], Callable]):
-    if typ in _PATCH_FN_TYPE_REGISTRATIONS:
-        raise CrossHairInternal(f"Doubly registered fn type patch: {typ}")
-    _PATCH_FN_TYPE_REGISTRATIONS[typ] = patch_value
-
-
 def register_opcode_patch(module: TracingModule) -> None:
     if type(module) in map(type, _OPCODE_PATCHES):
         raise CrossHairInternal(
@@ -1100,6 +1093,46 @@ class CallTreeAnalysis:
     num_confirmed_paths: int = 0
 
 
+class MessageGenerator:
+    def __init__(self, fn: Callable):
+        self.filename = ""
+        if hasattr(fn, "__code__"):
+            code_obj = fn.__code__
+            self.filename = code_obj.co_filename
+            self.start_lineno = code_obj.co_firstlineno
+            _, _, lines = sourcelines(fn)
+            self.end_lineno = self.start_lineno + len(lines)
+
+    def make(
+        self,
+        message_type: MessageType,
+        detail: str,
+        suggested_filename: Optional[str],
+        suggested_lineno: int,
+        tb: str,
+    ) -> AnalysisMessage:
+        if (
+            suggested_filename is not None
+            and (os.path.abspath(suggested_filename) == os.path.abspath(self.filename))
+            and (self.start_lineno <= suggested_lineno <= self.end_lineno)
+        ):
+            return AnalysisMessage(
+                message_type, detail, suggested_filename, suggested_lineno, 0, tb
+            )
+        else:
+            exprline = "<unknown>"
+            if suggested_filename is not None:
+                lines = linecache.getlines(suggested_filename)
+                try:
+                    exprline = lines[suggested_lineno - 1].strip()
+                except IndexError:
+                    pass
+            detail = f'"{exprline}" yields {detail}'
+            return AnalysisMessage(
+                message_type, detail, self.filename, self.start_lineno, 0, tb
+            )
+
+
 def analyze_calltree(
     options: AnalysisOptions, conditions: Conditions
 ) -> CallTreeAnalysis:
@@ -1162,6 +1195,25 @@ def analyze_calltree(
                             call_analysis.failing_precondition_reason
                         )
 
+            except NotDeterministic:
+                # TODO: Improve nondeterminism helpfulness
+                tb = extract_tb(sys.exc_info()[2])
+                frame_filename, frame_lineno = frame_summary_for_fn(
+                    conditions.src_fn, tb
+                )
+                msg_gen = MessageGenerator(conditions.src_fn)
+                call_analysis = CallAnalysis(
+                    VerificationStatus.REFUTED,
+                    [
+                        msg_gen.make(
+                            MessageType.EXEC_ERR,
+                            "NotDeterministic: Found a different execution paths after making the same decisions",
+                            frame_filename,
+                            frame_lineno,
+                            traceback.format_exc(),
+                        )
+                    ],
+                )
             except UnexploredPath:
                 call_analysis = CallAnalysis(VerificationStatus.UNKNOWN)
             except IgnoreAttempt:
@@ -1321,46 +1373,6 @@ def explore_paths(
                     break
 
 
-class MessageGenerator:
-    def __init__(self, fn: Callable):
-        self.filename = ""
-        if hasattr(fn, "__code__"):
-            code_obj = fn.__code__
-            self.filename = code_obj.co_filename
-            self.start_lineno = code_obj.co_firstlineno
-            _, _, lines = sourcelines(fn)
-            self.end_lineno = self.start_lineno + len(lines)
-
-    def make(
-        self,
-        message_type: MessageType,
-        detail: str,
-        suggested_filename: Optional[str],
-        suggested_lineno: int,
-        tb: str,
-    ) -> AnalysisMessage:
-        if (
-            suggested_filename is not None
-            and (os.path.abspath(suggested_filename) == os.path.abspath(self.filename))
-            and (self.start_lineno <= suggested_lineno <= self.end_lineno)
-        ):
-            return AnalysisMessage(
-                message_type, detail, suggested_filename, suggested_lineno, 0, tb
-            )
-        else:
-            exprline = "<unknown>"
-            if suggested_filename is not None:
-                lines = linecache.getlines(suggested_filename)
-                try:
-                    exprline = lines[suggested_lineno - 1].strip()
-                except IndexError:
-                    pass
-            detail = f'"{exprline}" yields {detail}'
-            return AnalysisMessage(
-                message_type, detail, self.filename, self.start_lineno, 0, tb
-            )
-
-
 def make_counterexample_message(
     conditions: Conditions, args: BoundArguments, return_val: object = None
 ) -> str:
@@ -1456,10 +1468,9 @@ def attempt_call(
         detail = name_of_type(type(e)) + ": " + str(e)
         tb_desc = tb.format()
         frame_filename, frame_lineno = frame_summary_for_fn(conditions.src_fn, tb)
-        if not isinstance(e, NotDeterministic):
-            with ResumedTracing():
-                space.detach_path()
-            detail += " " + make_counterexample_message(conditions, original_args)
+        with ResumedTracing():
+            space.detach_path(e)
+        detail += " " + make_counterexample_message(conditions, original_args)
         debug("exception while evaluating function body:", detail)
         debug("exception traceback:", ch_stack(tb))
         return CallAnalysis(
@@ -1509,12 +1520,11 @@ def attempt_call(
     elif efilter.user_exc is not None:
         (e, tb) = efilter.user_exc
         detail = name_of_type(type(e)) + ": " + str(e)
-        if not isinstance(e, NotDeterministic):
-            with ResumedTracing():
-                space.detach_path()
-            detail += " " + make_counterexample_message(
-                conditions, original_args, __return__
-            )
+        with ResumedTracing():
+            space.detach_path(e)
+        detail += " " + make_counterexample_message(
+            conditions, original_args, __return__
+        )
         debug("exception while calling postcondition:", detail)
         debug("exception traceback:", ch_stack(tb))
         failures = [

crosshair/core_and_libs.py

@@ -47,6 +47,7 @@
     typeslib,
     unicodedatalib,
     urlliblib,
+    weakreflib,
     zliblib,
 )
 from crosshair.options import AnalysisKind, AnalysisOptions
@@ -105,6 +106,7 @@ def _make_registrations():
     unicodedatalib.make_registrations()
     urlliblib.make_registrations()
     opcode_intercept.make_registrations()
+    weakreflib.make_registrations()
     zliblib.make_registrations()
 
     plugin_entries = entry_points(group="crosshair.plugin")

crosshair/core_test.py

@@ -976,19 +976,6 @@ def f(x: Dict[FrozenSet[float], int]) -> bool:
 
         check_states(f, POST_FAIL)
 
-    def test_nondeterminisim_detected(self) -> None:
-        _GLOBAL_THING = [True]
-
-        def f(i: int) -> int:
-            """post: True"""
-            _GLOBAL_THING[0] = not _GLOBAL_THING[0]
-            if _GLOBAL_THING[0]:
-                return -i if i < 0 else i
-            else:
-                return -i if i < 0 else i
-
-        self.assertEqual(*check_exec_err(f, "NotDeterministic"))
-
     def test_old_works_in_invariants(self) -> None:
         @dataclasses.dataclass
         class FrozenApples:
@@ -1046,6 +1033,50 @@ def f(ls: list[int]) -> List[int]:
         check_states(f, CONFIRMED)
 
 
+def test_nondeterministic_detected_via_stacktrace() -> None:
+    _GLOBAL_THING = [True]
+
+    def f(i: int) -> int:
+        """post: True"""
+        _GLOBAL_THING[0] = not _GLOBAL_THING[0]
+        if _GLOBAL_THING[0]:
+            return -i if i < 0 else i
+        else:
+            return -i if i < 0 else i
+
+    actual, expected = check_exec_err(f, "NotDeterministic")
+    assert actual == expected
+
+
+def test_nondeterministic_detected_via_condition() -> None:
+    _GLOBAL_THING = [42]
+
+    def f(i: int) -> int:
+        """post: True"""
+        _GLOBAL_THING[0] += 1
+        if i > _GLOBAL_THING[0]:
+            pass
+        return True
+
+    actual, expected = check_exec_err(f, "NotDeterministic")
+    assert actual == expected
+
+
+def test_nondeterministic_detected_in_detached_path() -> None:
+    _GLOBAL_THING = [True]
+
+    def f(i: int) -> int:
+        """post: True"""
+        _GLOBAL_THING[0] = not _GLOBAL_THING[0]
+        if _GLOBAL_THING[0]:
+            raise Exception
+        else:
+            return -i if i < 0 else i
+
+    actual, expected = check_exec_err(f, "NotDeterministic")
+    assert actual == expected
+
+
 if icontract:
 
     class TestIcontract(unittest.TestCase):

crosshair/libimpl/collectionslib_test.py

@@ -206,7 +206,7 @@ def f(symbolic: DefaultDict[int, int]) -> Tuple[dict, dict]:
     check_states(f, CANNOT_CONFIRM)
 
 
-def test_defaultdict_basic_fail(test_list) -> None:
+def test_defaultdict_basic_fail() -> None:
     def f(a: DefaultDict[int, int], k: int, v: int) -> None:
         """
         post[a]: a[42] != 42

crosshair/libimpl/functoolslib.py

@@ -1,22 +1,28 @@
-import functools as orig_functools
+from functools import _lru_cache_wrapper, partial, reduce
 
-from crosshair.core import register_fn_type_patch, register_patch
+from crosshair.core import register_patch
 
 # TODO: deal with lru_cache (note it needs to be intercepted at import-time)
 
 
 def _partial(func, *a1, **kw1):
     if callable(func):
-        return orig_functools.partial(lambda *a2, **kw2: func(*a2, **kw2), *a1, **kw1)
+        return partial(lambda *a2, **kw2: func(*a2, **kw2), *a1, **kw1)
     else:
         raise TypeError
 
 
 def _reduce(function, *a, **kw):
-    return orig_functools.reduce(lambda x, y: function(x, y), *a, **kw)
+    return reduce(lambda x, y: function(x, y), *a, **kw)
 
 
 def make_registrations():
-    register_patch(orig_functools.partial, _partial)
-    register_patch(orig_functools.reduce, _reduce)
-    register_fn_type_patch(orig_functools._lru_cache_wrapper, lambda w: w.__wrapped__)
+    register_patch(partial, _partial)
+    register_patch(reduce, _reduce)
+
+    def call_with_skipped_cache(self, *a, **kw):
+        if not isinstance(self, _lru_cache_wrapper):
+            raise TypeError
+        return self.__wrapped__(*a, **kw)
+
+    register_patch(_lru_cache_wrapper.__call__, call_with_skipped_cache)

crosshair/libimpl/timelib_test.py

@@ -2,7 +2,7 @@
 
 import pytest
 
-from crosshair.statespace import CANNOT_CONFIRM, CONFIRMED, POST_FAIL, MessageType
+from crosshair.statespace import CONFIRMED, POST_FAIL
 from crosshair.test_util import check_states
 
 

crosshair/libimpl/weakreflib.py

@@ -0,0 +1,13 @@
+from weakref import ref
+
+from crosshair.core import register_patch
+
+
+def _ref_call(r):
+    if not isinstance(r, ref):
+        raise TypeError
+    return None
+
+
+def make_registrations():
+    register_patch(ref.__call__, _ref_call)