diff --git a/crosshair/libimpl/builtinslib.py b/crosshair/libimpl/builtinslib.py index f9460113..2b2a0ce0 100644 --- a/crosshair/libimpl/builtinslib.py +++ b/crosshair/libimpl/builtinslib.py @@ -3210,7 +3210,7 @@ def rpartition(self, substr): ) return ("", "", self) - def _find(self, partitioner, substr, start=None, end=None): + def _find(self, substr, start=None, end=None, from_right=False): if not isinstance(substr, str): raise TypeError mylen = len(self) @@ -3222,7 +3222,7 @@ def _find(self, partitioner, substr, start=None, end=None): end = mylen elif end < 0: end += mylen - matchstr = self[start:end] + matchstr = self[start:end] if start != 0 or end is not mylen else self if len(substr) == 0: # Add oddity of CPython. We can find the empty string when over-slicing # off the left side of the string, but not off the right: @@ -3231,18 +3231,24 @@ def _find(self, partitioner, substr, start=None, end=None): if matchstr == "" and start > min(mylen, max(end, 0)): return -1 else: - return max(start, 0) + if from_right: + return max(min(end, mylen), 0) + else: + return max(start, 0) else: - (prefix, match, _) = partitioner(matchstr, substr) + if from_right: + (prefix, match, _) = LazyIntSymbolicStr.rpartition(matchstr, substr) + else: + (prefix, match, _) = LazyIntSymbolicStr.partition(matchstr, substr) if match == "": return -1 return start + len(prefix) def find(self, substr, start=None, end=None): - return self._find(LazyIntSymbolicStr.partition, substr, start, end) + return self._find(substr, start, end, from_right=False) def rfind(self, substr, start=None, end=None): - return self._find(LazyIntSymbolicStr.rpartition, substr, start, end) + return self._find(substr, start, end, from_right=True) class SeqBasedSymbolicStr(AtomicSymbolicValue, SymbolicSequence, AnySymbolicStr): diff --git a/crosshair/libimpl/builtinslib_test.py b/crosshair/libimpl/builtinslib_test.py index e685ee4f..6bf85ea8 100644 --- a/crosshair/libimpl/builtinslib_test.py +++ b/crosshair/libimpl/builtinslib_test.py @@ -768,6 +768,15 @@ def f(a: str) -> str: check_states(f, POST_FAIL) +def test_str_find_does_not_realize_string_length() -> None: + def f(a: str) -> str: + """post: len(_) != 100""" + a.find("abc") + return a + + check_states(f, POST_FAIL) + + def test_str_find_with_limits_ok() -> None: def f(a: str) -> int: """post: _ == -1""" diff --git a/crosshair/path_cover.py b/crosshair/path_cover.py index 56dd7333..4d268f1c 100644 --- a/crosshair/path_cover.py +++ b/crosshair/path_cover.py @@ -168,7 +168,7 @@ def import_statements_for_references(references: Set[ReferencedIdentifier]) -> S if ref.modulename == "builtins": continue if "." in ref.qualname: - class_name, _ = ref.qualname.split(".", 2) + class_name, _ = ref.qualname.split(".", 1) imports.add(f"from {ref.modulename} import {class_name}") else: imports.add(f"from {ref.modulename} import {ref.qualname}") diff --git a/crosshair/path_cover_test.py b/crosshair/path_cover_test.py index a3ff957a..285cb113 100644 --- a/crosshair/path_cover_test.py +++ b/crosshair/path_cover_test.py @@ -46,16 +46,15 @@ def _has_no_successful_paths(x: int) -> None: context_statespace().defer_assumption("fail", lambda: False) -class Color(Enum): - RED = 0 - - @dataclass class Train: + class Color(Enum): + RED = 0 + color: Color -def _paint_train(train: Train, color: Color) -> Train: +def _paint_train(train: Train, color: Train.Color) -> Train: return Train(color=color) @@ -130,11 +129,10 @@ def test_path_cover_pytest_output() -> None: imports, lines = output_pytest_paths(_paint_train, paths) assert lines == [ "def test__paint_train():", - " assert _paint_train(Train(Color.RED), Color.RED) == Train(color=Color.RED)", + " assert _paint_train(Train(Train.Color.RED), Train.Color.RED) == Train(color=Train.Color.RED)", "", ] assert imports == { "from crosshair.path_cover_test import _paint_train", - "from crosshair.path_cover_test import Color", "from crosshair.path_cover_test import Train", }