From 01cb87ea0ad219e6f65f3332bfd5a418e640b3c0 Mon Sep 17 00:00:00 2001 From: Phillip Schanely Date: Wed, 22 Jan 2025 10:21:16 -0500 Subject: [PATCH 1/4] Disable stack nondeterminism checks --- crosshair/statespace.py | 6 +++++- 1 file changed, 5 insertions(+), 1 deletion(-) diff --git a/crosshair/statespace.py b/crosshair/statespace.py index 3786a1f3..316fb7e7 100644 --- a/crosshair/statespace.py +++ b/crosshair/statespace.py @@ -892,7 +892,11 @@ def choose_possible( (not isinstance(node, WorstResultNode)) and "Wrong node type (expected WorstResultNode)" ) - or (node.stacktail != stacktail and "Stack trace changed") + # TODO: Not clear whether we want this stack trace check. + # A stack change usually indicates a serious problem, but not 100% of the time. + # Keeping it would mean that we fail earlier. + # But also see https://github.com/HypothesisWorks/hypothesis/pull/4034#issuecomment-2606415404 + # or (node.stacktail != stacktail and "Stack trace changed") or ((not z3.eq(node.expr, expr)) and "SMT expression changed") ) if not_deterministic_reason: From 338555e24a2a0dacc0372769677778e491ba01ff Mon Sep 17 00:00:00 2001 From: Phillip Schanely Date: Wed, 22 Jan 2025 12:14:47 -0500 Subject: [PATCH 2/4] Preserve symbolics in more math.copysign use cases --- crosshair/libimpl/builtinslib.py | 14 +++++++- crosshair/libimpl/builtinslib_ch_test.py | 5 +++ crosshair/libimpl/mathlib.py | 45 ++++++++++++------------ crosshair/libimpl/mathlib_ch_test.py | 17 +++++++-- crosshair/libimpl/mathlib_test.py | 18 ++++++---- 5 files changed, 68 insertions(+), 31 deletions(-) diff --git a/crosshair/libimpl/builtinslib.py b/crosshair/libimpl/builtinslib.py index d614e3f6..2e348bca 100644 --- a/crosshair/libimpl/builtinslib.py +++ b/crosshair/libimpl/builtinslib.py @@ -123,7 +123,7 @@ smtlib_typename, type_arg_of, ) -from crosshair.z3util import z3And, z3Eq, z3Ge, z3Gt, z3IntVal, z3Or +from crosshair.z3util import z3And, z3Eq, z3Ge, z3Gt, z3IntVal, z3Not, z3Or if sys.version_info >= (3, 12): from collections.abc import Buffer as BufferAbc @@ -165,6 +165,18 @@ def smt_or(a: bool, b: bool) -> bool: return a or b +def smt_xor(a: bool, b: bool) -> bool: + with NoTracing(): + if isinstance(a, SymbolicBool) or isinstance(b, SymbolicBool): + if isinstance(a, SymbolicBool) and isinstance(b, SymbolicBool): + return SymbolicBool(z3.Xor(a.var, b.var)) + elif isinstance(a, bool): + return SymbolicBool(z3Not(b.var)) if a else b + elif isinstance(b, bool): + return SymbolicBool(z3Not(a.var)) if b else a + return a ^ b + + def smt_not(x: object) -> Union[bool, "SymbolicBool"]: with NoTracing(): if isinstance(x, SymbolicBool): diff --git a/crosshair/libimpl/builtinslib_ch_test.py b/crosshair/libimpl/builtinslib_ch_test.py index a42de207..24f26697 100644 --- a/crosshair/libimpl/builtinslib_ch_test.py +++ b/crosshair/libimpl/builtinslib_ch_test.py @@ -1059,6 +1059,11 @@ def check_and(left: int): return compare_results(lambda lt: (lt & 3, 4 & lt), left) +def check_xor(left: Union[int, bool], right: Union[int, bool]): + """post: _""" + return compare_results(operator.xor, left, right) + + def check_truediv(left: Union[int, float], right: Union[int, float]): """post: _""" return compare_returns(operator.truediv, left, right) diff --git a/crosshair/libimpl/mathlib.py b/crosshair/libimpl/mathlib.py index d5ef62b2..cde7859c 100644 --- a/crosshair/libimpl/mathlib.py +++ b/crosshair/libimpl/mathlib.py @@ -12,42 +12,43 @@ SymbolicBool, SymbolicIntable, SymbolicValue, + smt_xor, ) from crosshair.tracers import ResumedTracing from crosshair.util import name_of_type from crosshair.z3util import z3Not, z3Or +def _is_positive(x): + if isinstance(x, SymbolicValue): + if isinstance(x, PreciseIeeeSymbolicFloat): + return SymbolicBool(z3Not(z3.fpIsNegative(x.var))) + elif isinstance(x, RealBasedSymbolicFloat): + return SymbolicBool(x.var >= 0) + else: + with ResumedTracing(): + return x >= 0 + else: + return math.copysign(1, x) == 1 + + def _copysign(x, y): if not isinstance(x, Real): raise TypeError(f"must be real number, not {name_of_type(type(x))}") if not isinstance(y, Real): raise TypeError(f"must be real number, not {name_of_type(type(y))}") with NoTracing(): - # Find the sign of y: - if isinstance(y, SymbolicValue): - if isinstance(y, PreciseIeeeSymbolicFloat): - y_is_positive = not SymbolicBool(z3.fpIsNegative(y.var)) - else: - with ResumedTracing(): - y_is_positive = y >= 0 - else: - y_is_positive = math.copysign(1, y) == 1 + x_is_positive = _is_positive(x) + y_is_positive = _is_positive(y) # then invert as needed: - if isinstance(x, PreciseIeeeSymbolicFloat): - if y_is_positive: - return PreciseIeeeSymbolicFloat( - z3.If(z3.fpIsNegative(x.var), -x.var, x.var) - ) - else: - return PreciseIeeeSymbolicFloat( - z3.If(z3.fpIsNegative(x.var), x.var, -x.var) - ) + invert = smt_xor(x_is_positive, y_is_positive) + with NoTracing(): + if isinstance(invert, SymbolicBool) and isinstance( + x, (PreciseIeeeSymbolicFloat, RealBasedSymbolicFloat) + ): + return type(x)(z3.If(invert.var, -x.var, x.var)) with ResumedTracing(): - if y_is_positive: - return x if x >= 0 else -x - else: - return -x if x >= 0 else x + return -x if invert else x if sys.version_info >= (3, 9): diff --git a/crosshair/libimpl/mathlib_ch_test.py b/crosshair/libimpl/mathlib_ch_test.py index cd22381e..c492a72b 100644 --- a/crosshair/libimpl/mathlib_ch_test.py +++ b/crosshair/libimpl/mathlib_ch_test.py @@ -4,12 +4,20 @@ import pytest # type: ignore +from crosshair.core import realize from crosshair.core_and_libs import MessageType, analyze_function, run_checkables +from crosshair.options import AnalysisOptionSet from crosshair.test_util import compare_results -def check_copysign(a: Union[int, float], b: Union[int, float]): +def check_copysign( + a: Union[int, float], b: Union[int, float], realize_a: bool, realize_b: bool +): """post: _""" + if realize_a: + a = realize(a) + if realize_b: + b = realize(b) return compare_results(math.copysign, a, b) @@ -26,6 +34,11 @@ def check_gcd(a: int, b: int): @pytest.mark.parametrize("fn_name", [fn for fn in dir() if fn.startswith("check_")]) def test_builtin(fn_name: str) -> None: this_module = sys.modules[__name__] - messages = run_checkables(analyze_function(getattr(this_module, fn_name))) + messages = run_checkables( + analyze_function( + getattr(this_module, fn_name), + AnalysisOptionSet(max_uninteresting_iterations=50), + ) + ) errors = [m for m in messages if m.state > MessageType.PRE_UNSAT] assert errors == [] diff --git a/crosshair/libimpl/mathlib_test.py b/crosshair/libimpl/mathlib_test.py index 990e0322..e800dba6 100644 --- a/crosshair/libimpl/mathlib_test.py +++ b/crosshair/libimpl/mathlib_test.py @@ -2,6 +2,8 @@ import sys import unittest +import pytest + from crosshair.core import proxy_for_type, standalone_statespace from crosshair.libimpl.builtinslib import ( ModelingDirector, @@ -14,7 +16,7 @@ from crosshair.util import set_debug -def test_copysign(): +def test_copysign_e2e(): def can_find_minus_zero(x: float): """post: math.copysign(1, _) == 1""" if x == 0: @@ -24,13 +26,17 @@ def can_find_minus_zero(x: float): check_states(can_find_minus_zero, POST_FAIL) -def test_copysign_with_precise_first_arg(space): - space.extra(ModelingDirector).global_representations[ - float - ] = PreciseIeeeSymbolicFloat - x = PreciseIeeeSymbolicFloat("x") +@pytest.mark.parametrize( + "FloatType", [PreciseIeeeSymbolicFloat, RealBasedSymbolicFloat] +) +def test_copysign_symbolics(FloatType, space): + space.extra(ModelingDirector).global_representations[float] = FloatType + x = FloatType("x") + y = FloatType("y") with ResumedTracing(): assert not space.is_possible(math.copysign(x, -0.0) > 0.0) + assert space.is_possible(math.copysign(x, y) > 0.0) + assert space.is_possible(math.copysign(x, y) < 0.0) def test_isfinite(): From 47201c0f243aafc301bb2e21fc90251b97d451eb Mon Sep 17 00:00:00 2001 From: Phillip Schanely Date: Thu, 23 Jan 2025 10:26:11 -0500 Subject: [PATCH 3/4] Update changelog --- doc/source/changelog.rst | 11 +++++++++++ 1 file changed, 11 insertions(+) diff --git a/doc/source/changelog.rst b/doc/source/changelog.rst index f6ad3dff..c8a1f2bb 100644 --- a/doc/source/changelog.rst +++ b/doc/source/changelog.rst @@ -9,6 +9,17 @@ Next Version * Nothing yet! +Version 0.0.82 +-------------- + + * Preserve symbolics in more math.copysign use cases. + * Disable stack-based nondeterminism checks. + In rare cases + (see `this thread `__), + the stack-based nondeterminism checks can be overly conservative. + CrossHair will still check and require that the solver is queried + deterministically. + Version 0.0.81 -------------- From ad48000cb63d81ced21e362759988f4a76e84e0d Mon Sep 17 00:00:00 2001 From: Phillip Schanely Date: Thu, 23 Jan 2025 10:31:30 -0500 Subject: [PATCH 4/4] Update tests for nondeterminism changes --- crosshair/core_test.py | 15 --------------- crosshair/main_test.py | 12 ++++++------ 2 files changed, 6 insertions(+), 21 deletions(-) diff --git a/crosshair/core_test.py b/crosshair/core_test.py index e058bd1e..91c1b7c7 100644 --- a/crosshair/core_test.py +++ b/crosshair/core_test.py @@ -1029,21 +1029,6 @@ 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] diff --git a/crosshair/main_test.py b/crosshair/main_test.py index 5813d9b6..a46f4e23 100644 --- a/crosshair/main_test.py +++ b/crosshair/main_test.py @@ -367,15 +367,15 @@ def test_check_circular_with_guard(root): def test_check_not_deterministic(root) -> None: NOT_DETERMINISTIC_FOO = { "foo.py": """ -_GLOBAL_THING = [True] +_GLOBAL_THING = [42] def wonky_foo(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 + _GLOBAL_THING[0] += 1 + if i > _GLOBAL_THING[0]: + pass + return True +_GLOBAL_THING = [True] def regular_foo(i: int) -> int: '''post: True'''