diff --git a/crosshair/condition_parser.py b/crosshair/condition_parser.py index de580bcf..5e10da8d 100644 --- a/crosshair/condition_parser.py +++ b/crosshair/condition_parser.py @@ -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 diff --git a/crosshair/core_test.py b/crosshair/core_test.py index 59f7362e..3fcae65d 100644 --- a/crosshair/core_test.py +++ b/crosshair/core_test.py @@ -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)) @@ -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( @@ -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( @@ -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 diff --git a/crosshair/diff_behavior_test.py b/crosshair/diff_behavior_test.py index 33cdba3e..3e965d68 100644 --- a/crosshair/diff_behavior_test.py +++ b/crosshair/diff_behavior_test.py @@ -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), @@ -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) diff --git a/crosshair/examples/PEP316/__init__.py b/crosshair/examples/PEP316/__init__.py index b6af8273..53674d31 100644 --- a/crosshair/examples/PEP316/__init__.py +++ b/crosshair/examples/PEP316/__init__.py @@ -1,2 +1 @@ # crosshair: analysis_kind=PEP316 -# crosshair: per_condition_timeout=0.75 diff --git a/crosshair/examples/PEP316/bugs_detected/getattr_magic.out b/crosshair/examples/PEP316/bugs_detected/getattr_magic.out index 301f0b14..00deef6a 100644 --- a/crosshair/examples/PEP316/bugs_detected/getattr_magic.out +++ b/crosshair/examples/PEP316/bugs_detected/getattr_magic.out @@ -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') diff --git a/crosshair/examples/PEP316/bugs_detected/getattr_magic.py b/crosshair/examples/PEP316/bugs_detected/getattr_magic.py index 1ecb2621..082e0fec 100644 --- a/crosshair/examples/PEP316/bugs_detected/getattr_magic.py +++ b/crosshair/examples/PEP316/bugs_detected/getattr_magic.py @@ -1,6 +1,3 @@ -# crosshair: per_condition_timeout=2 - - class Farm: def visit_chickens(self) -> str: return "cluck" diff --git a/crosshair/examples/deal/__init__.py b/crosshair/examples/deal/__init__.py index 67162535..2142f298 100644 --- a/crosshair/examples/deal/__init__.py +++ b/crosshair/examples/deal/__init__.py @@ -1,2 +1 @@ # crosshair: analysis_kind=deal -# crosshair: per_condition_timeout=1.0 diff --git a/crosshair/examples/hypothesis/__init__.py b/crosshair/examples/hypothesis/__init__.py index 5d89e6c1..812dbbe9 100644 --- a/crosshair/examples/hypothesis/__init__.py +++ b/crosshair/examples/hypothesis/__init__.py @@ -1,3 +1,2 @@ # crosshair: analysis_kind=hypothesis -# crosshair: per_condition_timeout=30 # crosshair: per_path_timeout=7 diff --git a/crosshair/examples/icontract/__init__.py b/crosshair/examples/icontract/__init__.py index 953e26f0..fabb46fb 100644 --- a/crosshair/examples/icontract/__init__.py +++ b/crosshair/examples/icontract/__init__.py @@ -1,2 +1 @@ # crosshair: analysis_kind=icontract -# crosshair: per_condition_timeout=1.0 diff --git a/crosshair/libimpl/builtinslib.py b/crosshair/libimpl/builtinslib.py index 8d45f565..f9460113 100644 --- a/crosshair/libimpl/builtinslib.py +++ b/crosshair/libimpl/builtinslib.py @@ -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: @@ -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): diff --git a/crosshair/libimpl/builtinslib_ch_test.py b/crosshair/libimpl/builtinslib_ch_test.py index b356fcad..1fbad48e 100644 --- a/crosshair/libimpl/builtinslib_ch_test.py +++ b/crosshair/libimpl/builtinslib_ch_test.py @@ -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: @@ -770,7 +769,6 @@ 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) @@ -778,7 +776,6 @@ def check_str_swapcase(string: str): 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) diff --git a/crosshair/libimpl/builtinslib_test.py b/crosshair/libimpl/builtinslib_test.py index cdffd260..e685ee4f 100644 --- a/crosshair/libimpl/builtinslib_test.py +++ b/crosshair/libimpl/builtinslib_test.py @@ -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), ) @@ -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) @@ -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 @@ -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: @@ -2406,7 +2405,6 @@ def f(d: dict, k: int) -> dict: check_states( f, MessageType.POST_FAIL, - AnalysisOptionSet(per_condition_timeout=90), ) @@ -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: @@ -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), ) diff --git a/crosshair/libimpl/codecslib_test.py b/crosshair/libimpl/codecslib_test.py index ff191815..0e13744b 100644 --- a/crosshair/libimpl/codecslib_test.py +++ b/crosshair/libimpl/codecslib_test.py @@ -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) diff --git a/crosshair/libimpl/collectionslib_ch_test.py b/crosshair/libimpl/collectionslib_ch_test.py index ae43cfd3..4e6f2147 100644 --- a/crosshair/libimpl/collectionslib_ch_test.py +++ b/crosshair/libimpl/collectionslib_ch_test.py @@ -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)) diff --git a/crosshair/libimpl/datetimelib_test.py b/crosshair/libimpl/datetimelib_test.py index 2e730b6e..3f9c5d57 100644 --- a/crosshair/libimpl/datetimelib_test.py +++ b/crosshair/libimpl/datetimelib_test.py @@ -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: @@ -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 diff --git a/crosshair/libimpl/encodings_ch_test.py b/crosshair/libimpl/encodings_ch_test.py index ff7a99a8..b71df23d 100644 --- a/crosshair/libimpl/encodings_ch_test.py +++ b/crosshair/libimpl/encodings_ch_test.py @@ -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: diff --git a/crosshair/libimpl/heapqlib_test.py b/crosshair/libimpl/heapqlib_test.py index 7941e508..26c5c7a8 100644 --- a/crosshair/libimpl/heapqlib_test.py +++ b/crosshair/libimpl/heapqlib_test.py @@ -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]): @@ -17,4 +15,4 @@ def f(items: List[int]): heapq.heapify(items) return items - check_states(f, CONFIRMED, _SLOW_TEST) + check_states(f, CONFIRMED) diff --git a/crosshair/libimpl/iolib_ch_test.py b/crosshair/libimpl/iolib_ch_test.py index 9f4a081e..1c8266e6 100644 --- a/crosshair/libimpl/iolib_ch_test.py +++ b/crosshair/libimpl/iolib_ch_test.py @@ -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]: diff --git a/crosshair/libimpl/jsonlib_ch_test.py b/crosshair/libimpl/jsonlib_ch_test.py index a3a83f59..ad0ad35b 100644 --- a/crosshair/libimpl/jsonlib_ch_test.py +++ b/crosshair/libimpl/jsonlib_ch_test.py @@ -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 == [] diff --git a/crosshair/libimpl/relib_ch_test.py b/crosshair/libimpl/relib_ch_test.py index dfc541e8..2d51c02b 100644 --- a/crosshair/libimpl/relib_ch_test.py +++ b/crosshair/libimpl/relib_ch_test.py @@ -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 == [] diff --git a/crosshair/libimpl/relib_test.py b/crosshair/libimpl/relib_test.py index 07c92b2b..138f8dcc 100644 --- a/crosshair/libimpl/relib_test.py +++ b/crosshair/libimpl/relib_test.py @@ -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), ) diff --git a/crosshair/lsp_server.py b/crosshair/lsp_server.py index f121ce10..71b7ba7c 100644 --- a/crosshair/lsp_server.py +++ b/crosshair/lsp_server.py @@ -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 @@ -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) diff --git a/crosshair/main.py b/crosshair/main.py index e23d7999..f8fdf4d0 100644 --- a/crosshair/main.py +++ b/crosshair/main.py @@ -365,8 +365,10 @@ def command_line_parser() -> argparse.ArgumentParser: help=textwrap.dedent( """\ Maximum seconds to spend checking one execution path. - If unspecified, CrossHair will timeout each path at the square root of the - `per_condition_timeout`. + If unspecified, CrossHair will timeout each path: + 1. at the square root of `--per_condition_timeout`, if speficied + 2. else, at a number of seconds equal to `--max_uninteresting_iterations`, if specified + 3. else, there will be no per-path timeout. """ ), ) @@ -425,14 +427,14 @@ def run_watch_loop( print_divider("-") line = f" Analyzing {len(watcher._modtimes)} files." print(color(line, AnsiColor.OKBLUE), end="") - max_condition_timeout = 0.5 + max_uninteresting_iterations = DEFAULT_OPTIONS.max_uninteresting_iterations restart = False stats = Counter() active_messages = {} else: time.sleep(0.1) - max_condition_timeout *= 2 - for curstats, messages in watcher.run_iteration(max_condition_timeout): + max_uninteresting_iterations *= 2 + for curstats, messages in watcher.run_iteration(max_uninteresting_iterations): messages = [m for m in messages if m.state > MessageType.PRE_UNSAT] stats.update(curstats) if messages_merged(active_messages, messages): @@ -693,7 +695,7 @@ def diffbehavior( stdout.write("All paths exhausted, functions are likely the same!\n") else: stdout.write( - "Consider trying longer with: --per_condition_timeout=\n" + "Consider increasing the --max_uninteresting_iterations option.\n" ) return 0 else: @@ -815,7 +817,7 @@ def on_example(example: str) -> None: ) if final_example is None: stderr.write("No input found.\n") - stderr.write("Consider trying longer with: --per_condition_timeout=\n") + stderr.write("Consider increasing the --max_uninteresting_iterations option.\n") return 1 else: if not output_all_examples: @@ -886,7 +888,6 @@ def unwalled_main(cmd_args: Union[List[str], argparse.Namespace]) -> int: elif args.action == "diffbehavior": defaults = DEFAULT_OPTIONS.overlay( AnalysisOptionSet( - per_condition_timeout=3.0, per_path_timeout=30.0, # mostly, we don't want to time out paths ) ) @@ -894,7 +895,6 @@ def unwalled_main(cmd_args: Union[List[str], argparse.Namespace]) -> int: elif args.action == "cover": defaults = DEFAULT_OPTIONS.overlay( AnalysisOptionSet( - per_condition_timeout=3.0, per_path_timeout=30.0, # mostly, we don't want to time out paths ) ) diff --git a/crosshair/options.py b/crosshair/options.py index 65fa1117..9fa28ace 100644 --- a/crosshair/options.py +++ b/crosshair/options.py @@ -135,10 +135,15 @@ class AnalysisOptions: def get_per_path_timeout(self): if math.isnan(self.per_path_timeout): - if self.per_condition_timeout > 1.0: - return self.per_condition_timeout**0.5 + if math.isfinite(self.per_condition_timeout): + if self.per_condition_timeout > 1.0: + return self.per_condition_timeout**0.5 + else: + return self.per_condition_timeout + elif math.isfinite(self.max_uninteresting_iterations): + return max(self.max_uninteresting_iterations, 1.0) else: - return self.per_condition_timeout + return float("inf") else: return self.per_path_timeout @@ -193,11 +198,11 @@ def incr(self, key: str): ), enabled=True, specs_complete=False, - per_condition_timeout=3.0, + per_condition_timeout=float("inf"), max_iterations=sys.maxsize, report_all=False, report_verbose=True, timeout=float("inf"), per_path_timeout=float("NaN"), - max_uninteresting_iterations=sys.maxsize, + max_uninteresting_iterations=5, ) diff --git a/crosshair/path_cover_test.py b/crosshair/path_cover_test.py index b6aca57f..a3ff957a 100644 --- a/crosshair/path_cover_test.py +++ b/crosshair/path_cover_test.py @@ -59,7 +59,7 @@ def _paint_train(train: Train, color: Color) -> Train: return Train(color=color) -OPTS = DEFAULT_OPTIONS.overlay(max_iterations=10, per_condition_timeout=10.0) +OPTS = DEFAULT_OPTIONS.overlay(max_iterations=10) foo = FunctionInfo.from_fn(_foo) decorated_foo = FunctionInfo.from_fn(functools.lru_cache()(_foo)) regex = FunctionInfo.from_fn(_regex) diff --git a/crosshair/test_util.py b/crosshair/test_util.py index 34b9c8ea..783a3a28 100644 --- a/crosshair/test_util.py +++ b/crosshair/test_util.py @@ -1,4 +1,5 @@ import pathlib +import sys from copy import deepcopy from dataclasses import dataclass, replace from typing import Callable, Iterable, List, Mapping, Optional, Sequence, Set, Tuple @@ -47,15 +48,28 @@ def check_states( optionset: AnalysisOptionSet = AnalysisOptionSet(), ) -> None: if expected == MessageType.POST_FAIL: - local_opts = AnalysisOptionSet(per_condition_timeout=16) + local_opts = AnalysisOptionSet( + per_condition_timeout=16, + max_uninteresting_iterations=sys.maxsize, + ) elif expected == MessageType.CONFIRMED: - local_opts = AnalysisOptionSet(per_condition_timeout=10, per_path_timeout=5) + local_opts = AnalysisOptionSet( + per_condition_timeout=10, + per_path_timeout=5, + max_uninteresting_iterations=sys.maxsize, + ) elif expected == MessageType.POST_ERR: local_opts = AnalysisOptionSet(max_iterations=20) elif expected == MessageType.CANNOT_CONFIRM: - local_opts = AnalysisOptionSet(max_iterations=40, per_condition_timeout=3) + local_opts = AnalysisOptionSet( + max_uninteresting_iterations=40, + per_condition_timeout=3, + ) else: - local_opts = AnalysisOptionSet(max_iterations=40, per_condition_timeout=5) + local_opts = AnalysisOptionSet( + max_uninteresting_iterations=40, + per_condition_timeout=5, + ) options = local_opts.overlay(optionset) found = set([m.state for m in run_checkables(analyze_function(fn, options))]) assertmsg = f"Got {','.join(map(str, found))} instead of {expected}" @@ -67,9 +81,7 @@ def check_states( def check_exec_err( fn: Callable, message_prefix="", optionset: AnalysisOptionSet = AnalysisOptionSet() ) -> ComparableLists: - local_opts = AnalysisOptionSet( - max_iterations=20, per_condition_timeout=10, per_path_timeout=2 - ) + local_opts = AnalysisOptionSet(max_iterations=20) options = local_opts.overlay(optionset) messages = run_checkables(analyze_function(fn, options)) if all(m.message.startswith(message_prefix) for m in messages): diff --git a/crosshair/watcher.py b/crosshair/watcher.py index 151400bc..5565ae1b 100644 --- a/crosshair/watcher.py +++ b/crosshair/watcher.py @@ -235,17 +235,19 @@ def startpool(self) -> Pool: return Pool(multiprocessing.cpu_count() - 1) def run_iteration( - self, max_condition_timeout=0.5 + self, max_uninteresting_iterations=0.5 ) -> Iterator[Tuple[Counter[str], List[AnalysisMessage]]]: - debug(f"starting pass with a condition timeout of {max_condition_timeout}") + debug( + f"starting pass with max_uninteresting_iterations={max_uninteresting_iterations}" + ) debug("Files:", self._modtimes.keys()) pool = self._pool - for filename in self._modtimes.keys(): + for filename, _ in sorted(self._modtimes.items(), key=lambda pair: -pair[1]): worker_timeout = max( - 10.0, max_condition_timeout * 100.0 + 10.0, max_uninteresting_iterations * 100.0 ) # TODO: times 100? is that right? iter_options = AnalysisOptionSet( - per_condition_timeout=max_condition_timeout, + max_uninteresting_iterations=max_uninteresting_iterations, ) options = self._options.overlay(iter_options) pool.submit((filename, options, time.time() + worker_timeout)) diff --git a/doc/source/contracts.rst b/doc/source/contracts.rst index 464e9dfa..45bcd661 100644 --- a/doc/source/contracts.rst +++ b/doc/source/contracts.rst @@ -186,8 +186,10 @@ It is more customizable than ``watch`` and produces machine-readable output. CrossHair for hours. --per_path_timeout FLOAT Maximum seconds to spend checking one execution path. - If unspecified, CrossHair will timeout each path at the square root of the - `per_condition_timeout`. + If unspecified, CrossHair will timeout each path: + 1. at the square root of `--per_condition_timeout`, if speficied + 2. else, at a number of seconds equal to `--max_uninteresting_iterations`, if specified + 3. else, there will be no per-path timeout. --per_condition_timeout FLOAT Maximum seconds to spend checking execution paths for one condition --analysis_kind KIND Kind of contract to check. diff --git a/doc/source/cover.rst b/doc/source/cover.rst index 31f0ba39..b4689f6b 100644 --- a/doc/source/cover.rst +++ b/doc/source/cover.rst @@ -115,8 +115,10 @@ How do I try it? CrossHair for hours. --per_path_timeout FLOAT Maximum seconds to spend checking one execution path. - If unspecified, CrossHair will timeout each path at the square root of the - `per_condition_timeout`. + If unspecified, CrossHair will timeout each path: + 1. at the square root of `--per_condition_timeout`, if speficied + 2. else, at a number of seconds equal to `--max_uninteresting_iterations`, if specified + 3. else, there will be no per-path timeout. --per_condition_timeout FLOAT Maximum seconds to spend checking execution paths for one condition diff --git a/doc/source/diff_behavior.rst b/doc/source/diff_behavior.rst index ddcc6712..17c88217 100644 --- a/doc/source/diff_behavior.rst +++ b/doc/source/diff_behavior.rst @@ -64,8 +64,10 @@ How do I try it? Plugin file(s) you wish to use during the current execution --per_path_timeout FLOAT Maximum seconds to spend checking one execution path. - If unspecified, CrossHair will timeout each path at the square root of the - `per_condition_timeout`. + If unspecified, CrossHair will timeout each path: + 1. at the square root of `--per_condition_timeout`, if speficied + 2. else, at a number of seconds equal to `--max_uninteresting_iterations`, if specified + 3. else, there will be no per-path timeout. --per_condition_timeout FLOAT Maximum seconds to spend checking execution paths for one condition