Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Preserve symbolics in more math.copysign use cases #333

Merged
merged 4 commits into from
Jan 23, 2025
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
15 changes: 0 additions & 15 deletions crosshair/core_test.py
Original file line number Diff line number Diff line change
Expand Up @@ -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]

Expand Down
14 changes: 13 additions & 1 deletion crosshair/libimpl/builtinslib.py
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand Down Expand Up @@ -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):
Expand Down
5 changes: 5 additions & 0 deletions crosshair/libimpl/builtinslib_ch_test.py
Original file line number Diff line number Diff line change
Expand Up @@ -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)
Expand Down
45 changes: 23 additions & 22 deletions crosshair/libimpl/mathlib.py
Original file line number Diff line number Diff line change
Expand Up @@ -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):
Expand Down
17 changes: 15 additions & 2 deletions crosshair/libimpl/mathlib_ch_test.py
Original file line number Diff line number Diff line change
Expand Up @@ -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)


Expand All @@ -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 == []
18 changes: 12 additions & 6 deletions crosshair/libimpl/mathlib_test.py
Original file line number Diff line number Diff line change
Expand Up @@ -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,
Expand All @@ -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:
Expand All @@ -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():
Expand Down
12 changes: 6 additions & 6 deletions crosshair/main_test.py
Original file line number Diff line number Diff line change
Expand Up @@ -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'''
Expand Down
6 changes: 5 additions & 1 deletion crosshair/statespace.py
Original file line number Diff line number Diff line change
Expand Up @@ -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:
Expand Down
11 changes: 11 additions & 0 deletions doc/source/changelog.rst
Original file line number Diff line number Diff line change
Expand Up @@ -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 <https://github.com/HypothesisWorks/hypothesis/pull/4034#issuecomment-2606415404>`__),
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
--------------

Expand Down
Loading