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

Expand use of max-uninteresting-iterations #222

Merged
merged 6 commits into from
Nov 9, 2023
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
10 changes: 6 additions & 4 deletions crosshair/condition_parser.py
Original file line number Diff line number Diff line change
Expand Up @@ -1173,10 +1173,12 @@ def get_fn_conditions(self, ctxfn: FunctionInfo) -> Optional[Conditions]:
return None

# Mess with the settings to wrap whatever database we're using for CrossHair
db = fn._hypothesis_internal_use_settings.database # type: ignore
fn._hypothesis_internal_use_settings = hypothesis.settings( # type: ignore
database=CrossHairDatabaseWrapper(db), phases=[hypothesis.Phase.generate]
)
if hasattr(fn, "_hypothesis_internal_use_settings"):
db = fn._hypothesis_internal_use_settings.database # type: ignore
fn._hypothesis_internal_use_settings = hypothesis.settings( # type: ignore
database=CrossHairDatabaseWrapper(db),
phases=[hypothesis.Phase.generate],
)
fuzz_one = getattr(handle, "fuzz_one_input", None)
if fuzz_one is None:
return None
Expand Down
9 changes: 3 additions & 6 deletions crosshair/core_test.py
Original file line number Diff line number Diff line change
Expand Up @@ -465,21 +465,21 @@ def test_methods_directly(self) -> None:
# don't explode:
messages = analyze_any(
walk_qualname(Person, "a_regular_method"),
AnalysisOptionSet(per_condition_timeout=5),
AnalysisOptionSet(),
)
self.assertEqual(*check_messages(messages, state=MessageType.CONFIRMED))

def test_class_method(self) -> None:
messages = analyze_any(
walk_qualname(Person, "a_class_method"),
AnalysisOptionSet(per_condition_timeout=5),
AnalysisOptionSet(),
)
self.assertEqual(*check_messages(messages, state=MessageType.CONFIRMED))

def test_static_method(self) -> None:
messages = analyze_any(
walk_qualname(Person, "a_static_method"),
AnalysisOptionSet(per_condition_timeout=5),
AnalysisOptionSet(),
)
self.assertEqual(*check_messages(messages, state=MessageType.CONFIRMED))

Expand Down Expand Up @@ -1135,7 +1135,6 @@ def test_hypothesis_counterexample_text():
DEFAULT_OPTIONS.overlay(
analysis_kind=[AnalysisKind.hypothesis],
max_iterations=10,
per_condition_timeout=20,
),
)
actual, expected = check_messages(
Expand Down Expand Up @@ -1172,7 +1171,6 @@ def test_hypothesis_database_interaction():
DEFAULT_OPTIONS.overlay(
analysis_kind=[AnalysisKind.hypothesis],
max_iterations=10,
per_condition_timeout=20,
),
)
actual, expected = check_messages(
Expand All @@ -1196,7 +1194,6 @@ def test_asserts(self):
DEFAULT_OPTIONS.overlay(
analysis_kind=[AnalysisKind.asserts],
max_iterations=10,
per_condition_timeout=5,
),
)
line = remove_smallest_with_asserts.__code__.co_firstlineno + 4
Expand Down
4 changes: 2 additions & 2 deletions crosshair/diff_behavior_test.py
Original file line number Diff line number Diff line change
Expand Up @@ -92,7 +92,7 @@ def cut_out_item2(a: List[int], i: int):
a[:] = a[:i] + a[i + 1 :]

# TODO: this takes longer than I'd like:
opts = DEFAULT_OPTIONS.overlay(max_iterations=40, per_condition_timeout=30)
opts = DEFAULT_OPTIONS.overlay(max_iterations=40)
diffs = diff_behavior(
FunctionInfo.from_fn(cut_out_item1),
FunctionInfo.from_fn(cut_out_item2),
Expand Down Expand Up @@ -123,7 +123,7 @@ def isack2(s: str) -> Optional[bool]:
diffs = diff_behavior(
FunctionInfo.from_fn(isack1),
FunctionInfo.from_fn(isack2),
DEFAULT_OPTIONS.overlay(max_iterations=20, per_condition_timeout=5),
DEFAULT_OPTIONS.overlay(max_iterations=20),
)
debug("diffs=", diffs)
assert not isinstance(diffs, str)
Expand Down
1 change: 0 additions & 1 deletion crosshair/examples/PEP316/__init__.py
Original file line number Diff line number Diff line change
@@ -1,2 +1 @@
# crosshair: analysis_kind=PEP316
# crosshair: per_condition_timeout=0.75
2 changes: 1 addition & 1 deletion crosshair/examples/PEP316/bugs_detected/getattr_magic.out
Original file line number Diff line number Diff line change
@@ -1 +1 @@
getattr_magic.py:14: error: false when calling visit_animals(animal = 'cows') (which returns 'moo')
getattr_magic.py:11: error: false when calling visit_animals('cows') (which returns 'moo')
3 changes: 0 additions & 3 deletions crosshair/examples/PEP316/bugs_detected/getattr_magic.py
Original file line number Diff line number Diff line change
@@ -1,6 +1,3 @@
# crosshair: per_condition_timeout=2


class Farm:
def visit_chickens(self) -> str:
return "cluck"
Expand Down
1 change: 0 additions & 1 deletion crosshair/examples/deal/__init__.py
Original file line number Diff line number Diff line change
@@ -1,2 +1 @@
# crosshair: analysis_kind=deal
# crosshair: per_condition_timeout=1.0
1 change: 0 additions & 1 deletion crosshair/examples/hypothesis/__init__.py
Original file line number Diff line number Diff line change
@@ -1,3 +1,2 @@
# crosshair: analysis_kind=hypothesis
# crosshair: per_condition_timeout=30
# crosshair: per_path_timeout=7
1 change: 0 additions & 1 deletion crosshair/examples/icontract/__init__.py
Original file line number Diff line number Diff line change
@@ -1,2 +1 @@
# crosshair: analysis_kind=icontract
# crosshair: per_condition_timeout=1.0
25 changes: 22 additions & 3 deletions crosshair/libimpl/builtinslib.py
Original file line number Diff line number Diff line change
Expand Up @@ -2539,7 +2539,7 @@ def capitalize(self):
firstchar = self[0].title()
else:
firstchar = self[0].upper()
return firstchar + self[1:]
return firstchar + self[1:].lower()

def casefold(self):
if len(self) != 1:
Expand Down Expand Up @@ -4310,8 +4310,27 @@ def _int_from_bytes(
return val


def _list_index(self, value, start=0, stop=9223372036854775807):
return list.index(self, value, realize(start), realize(stop))
_LIST_INDEX_START_DEFAULT = 0
_LIST_INDEX_STOP_DEFAULT = 9223372036854775807


def _list_index(
self, value, start=_LIST_INDEX_START_DEFAULT, stop=_LIST_INDEX_STOP_DEFAULT
):
with NoTracing():
if not isinstance(self, list):
raise TypeError
if (
start is not _LIST_INDEX_START_DEFAULT
or stop is not _LIST_INDEX_STOP_DEFAULT
):
self = self[start:stop]
for idx, self_value in enumerate(self):
with ResumedTracing():
isequal = value == self_value
if isequal:
return idx
raise ValueError


def _dict_get(self: dict, key, default=None):
Expand Down
5 changes: 1 addition & 4 deletions crosshair/libimpl/builtinslib_ch_test.py
Original file line number Diff line number Diff line change
Expand Up @@ -22,14 +22,13 @@
from crosshair.test_util import ResultComparison, compare_results

_TRICKY_UNICODE = (
"A\u01f2", # upper followed by title cased character
"\ua770", # Lm, lower (superscript "9")
"\u01f2", # Lt, title-cased but not upper (compound "Dz" like char)
"\u2165", # Nl (roman numeral "VI")
"A\u01f2", # upper followed by title cased character
)

# crosshair: max_iterations=20
# crosshair: per_condition_timeout=14


def check_abs(x: float) -> ResultComparison:
Expand Down Expand Up @@ -770,15 +769,13 @@ def check_str_strip(string: str, chars: str) -> ResultComparison:

def check_str_swapcase(string: str):
"""post: _"""
# crosshair: per_condition_timeout=60
if string not in ("Ab", "\u01f2"):
return True
return compare_results(lambda s: s.swapcase(), string)


def check_str_title(string: str):
"""post: _"""
# crosshair: per_condition_timeout=60
if string not in ("A\u01f2", "aA"):
return True
return compare_results(lambda s: s.title(), string)
Expand Down
13 changes: 5 additions & 8 deletions crosshair/libimpl/builtinslib_test.py
Original file line number Diff line number Diff line change
Expand Up @@ -600,7 +600,7 @@ def f(a: str) -> float:
check_states(
f,
MessageType.POST_FAIL,
AnalysisOptionSet(max_iterations=100, per_condition_timeout=10),
AnalysisOptionSet(max_iterations=100),
)


Expand Down Expand Up @@ -1084,7 +1084,7 @@ def f(s: str) -> str:
return s.upper()

# TODO: make this use case more efficient.
options = AnalysisOptionSet(per_condition_timeout=60.0, per_path_timeout=20.0)
options = AnalysisOptionSet(per_path_timeout=20.0)
check_states(f, POST_FAIL, options)


Expand All @@ -1096,8 +1096,7 @@ def f(lines: List[str]) -> List[str]:
"""
return [line[: line.index(",")] for line in lines]

options = AnalysisOptionSet(per_condition_timeout=5)
check_states(f, CANNOT_CONFIRM, options)
check_states(f, CANNOT_CONFIRM)


@pytest.mark.demo
Expand Down Expand Up @@ -2224,7 +2223,7 @@ def f(d: Dict[Tuple[int, bool], Tuple[float, int]]) -> int:
else:
return 42

check_states(f, MessageType.POST_FAIL, AnalysisOptionSet(per_condition_timeout=5))
check_states(f, MessageType.POST_FAIL)


def test_dict_isinstance_check() -> None:
Expand Down Expand Up @@ -2406,7 +2405,6 @@ def f(d: dict, k: int) -> dict:
check_states(
f,
MessageType.POST_FAIL,
AnalysisOptionSet(per_condition_timeout=90),
)


Expand Down Expand Up @@ -2488,7 +2486,7 @@ def f(s: Set[Union[int, str]]) -> Set[Union[int, str]]:
"""post: not ((42 in s) and ('42' in s))"""
return s

check_states(f, MessageType.POST_FAIL, AnalysisOptionSet(per_condition_timeout=7.0))
check_states(f, MessageType.POST_FAIL)


def test_set_subset_compare_ok() -> None:
Expand Down Expand Up @@ -2722,7 +2720,6 @@ def f(typ1: Type, typ2: Type[bool], typ3: Type):
check_states(
f,
POST_FAIL,
AnalysisOptionSet(max_iterations=60, per_condition_timeout=10),
)


Expand Down
2 changes: 1 addition & 1 deletion crosshair/libimpl/codecslib_test.py
Original file line number Diff line number Diff line change
Expand Up @@ -51,4 +51,4 @@ def f(byts: bytes) -> str:
"""
return byts.decode("utf-8", errors="strict")

check_states(f, POST_FAIL, AnalysisOptionSet(per_condition_timeout=20))
check_states(f, POST_FAIL)
2 changes: 1 addition & 1 deletion crosshair/libimpl/collectionslib_ch_test.py
Original file line number Diff line number Diff line change
Expand Up @@ -244,7 +244,7 @@ def check_defaultdict_values(dictionary: DefaultDict[int, int]) -> ResultCompari
# It runs crosshair on each of the "check" functions defined above.
@pytest.mark.parametrize("fn_name", [fn for fn in dir() if fn.startswith("check_")])
def test_builtin(fn_name: str) -> None:
opts = AnalysisOptionSet(max_iterations=7, per_condition_timeout=20)
opts = AnalysisOptionSet(max_iterations=7)
this_module = sys.modules[__name__]
fn = getattr(this_module, fn_name)
messages = run_checkables(analyze_function(fn, opts))
Expand Down
4 changes: 1 addition & 3 deletions crosshair/libimpl/datetimelib_test.py
Original file line number Diff line number Diff line change
Expand Up @@ -6,8 +6,6 @@
from crosshair.statespace import CANNOT_CONFIRM, EXEC_ERR, POST_FAIL
from crosshair.test_util import check_states

_SLOW_TEST = AnalysisOptionSet(per_condition_timeout=20, per_path_timeout=4)


def test_timedelta_symbolic_months_fail() -> None:
def f(num_months: int) -> datetime.date:
Expand All @@ -18,7 +16,7 @@ def f(num_months: int) -> datetime.date:
dt = datetime.date(2000, 1, 1)
return dt + datetime.timedelta(days=30 * num_months)

check_states(f, POST_FAIL, _SLOW_TEST)
check_states(f, POST_FAIL)


@pytest.mark.demo
Expand Down
1 change: 0 additions & 1 deletion crosshair/libimpl/encodings_ch_test.py
Original file line number Diff line number Diff line change
Expand Up @@ -11,7 +11,6 @@
_ERROR_HANDLERS = ["strict", "replace", "ignore"]

# crosshair: max_iterations=20
# crosshair: per_condition_timeout=60


def check_encode_ascii(string: str, errors: str) -> ResultComparison:
Expand Down
4 changes: 1 addition & 3 deletions crosshair/libimpl/heapqlib_test.py
Original file line number Diff line number Diff line change
Expand Up @@ -5,8 +5,6 @@
from crosshair.statespace import CONFIRMED, MessageType
from crosshair.test_util import check_states

_SLOW_TEST = AnalysisOptionSet(per_condition_timeout=10)


def test_heapify():
def f(items: List[int]):
Expand All @@ -17,4 +15,4 @@ def f(items: List[int]):
heapq.heapify(items)
return items

check_states(f, CONFIRMED, _SLOW_TEST)
check_states(f, CONFIRMED)
1 change: 0 additions & 1 deletion crosshair/libimpl/iolib_ch_test.py
Original file line number Diff line number Diff line change
Expand Up @@ -11,7 +11,6 @@
from crosshair.tracers import is_tracing

# crosshair: max_iterations=40
# crosshair: per_condition_timeout=100


def _maybe_stringio(s: BackedStringIO) -> Union[StringIO, BackedStringIO]:
Expand Down
3 changes: 1 addition & 2 deletions crosshair/libimpl/jsonlib_ch_test.py
Original file line number Diff line number Diff line change
Expand Up @@ -36,8 +36,7 @@ def check_encode_decode_roundtrip(obj: Union[bool, int, str]):
# It runs crosshair on each of the "check" functions defined above.
@pytest.mark.parametrize("fn_name", [fn for fn in dir() if fn.startswith("check_")])
def test_builtin(fn_name: str) -> None:
opts = AnalysisOptionSet(max_iterations=40, per_condition_timeout=60)
fn = getattr(sys.modules[__name__], fn_name)
messages = run_checkables(analyze_function(fn, opts))
messages = run_checkables(analyze_function(fn))
errors = [m for m in messages if m.state > MessageType.PRE_UNSAT]
assert errors == []
3 changes: 1 addition & 2 deletions crosshair/libimpl/relib_ch_test.py
Original file line number Diff line number Diff line change
Expand Up @@ -138,9 +138,8 @@ def check_negative_lookbehind(text: str) -> ResultComparison:
# It runs crosshair on each of the "check" functions defined above.
@pytest.mark.parametrize("fn_name", [fn for fn in dir() if fn.startswith("check_")])
def test_builtin(fn_name: str) -> None:
opts = AnalysisOptionSet(max_iterations=20, per_condition_timeout=30)
this_module = sys.modules[__name__]
fn = getattr(this_module, fn_name)
messages = run_checkables(analyze_function(fn, opts))
messages = run_checkables(analyze_function(fn))
errors = [m for m in messages if m.state > MessageType.PRE_UNSAT]
assert errors == []
2 changes: 1 addition & 1 deletion crosshair/libimpl/relib_test.py
Original file line number Diff line number Diff line change
Expand Up @@ -357,7 +357,7 @@ def f(s: str):
check_states(
f,
POST_FAIL,
AnalysisOptionSet(max_iterations=20, per_condition_timeout=20),
AnalysisOptionSet(max_iterations=20),
)


Expand Down
12 changes: 7 additions & 5 deletions crosshair/lsp_server.py
Original file line number Diff line number Diff line change
Expand Up @@ -28,7 +28,7 @@
from pygls.server import LanguageServer

from crosshair import __version__, env_info
from crosshair.options import AnalysisOptionSet
from crosshair.options import DEFAULT_OPTIONS, AnalysisOptionSet
from crosshair.statespace import AnalysisMessage, MessageType
from crosshair.watcher import Watcher

Expand Down Expand Up @@ -132,19 +132,21 @@ def log(*a):
server.show_message_log(
f"Scanning {numfiles} file(s) for properties to check."
)
max_condition_timeout = 0.5
max_uninteresting_iterations = (
DEFAULT_OPTIONS.max_uninteresting_iterations
)
restart = False
stats = Counter()
for k, v in list(active_messages.items()):
active_messages[k] = None if v is None else {}
else:
time.sleep(0.25)
max_condition_timeout = min(
sys.float_info.max, 2 * max_condition_timeout
max_uninteresting_iterations = min(
sys.maxsize, 2 * max_uninteresting_iterations
)
log(f"iteration starting" + str(_i))
for curstats, messages in watcher.run_iteration(
1.0 + max_condition_timeout
max_uninteresting_iterations
):
log(f"iteration yielded {curstats, messages}")
stats.update(curstats)
Expand Down
Loading