From 46cf95e937a10d973392401e56cbcd36287396ff Mon Sep 17 00:00:00 2001 From: Rik Date: Wed, 13 Mar 2024 20:42:13 +0100 Subject: [PATCH] Retry extract a shrinking pass in a functional style --- minithesis.py | 96 ++++++++++++++++++++++++++++++++------------------- 1 file changed, 60 insertions(+), 36 deletions(-) diff --git a/minithesis.py b/minithesis.py index 8d57541..8ab3d1a 100644 --- a/minithesis.py +++ b/minithesis.py @@ -82,6 +82,8 @@ S = TypeVar("S", covariant=True) U = TypeVar("U") # Invariant +InterestTest = Callable[[array], bool] # Really array[int] -> bool + class Database(Protocol): def __setitem__(self, key: str, value: bytes) -> None: @@ -676,43 +678,12 @@ def consider(choices: array[int]) -> bool: # First try deleting each choice we made in chunks. self.shrink_remove(consider) - def replace(values: Mapping[int, int]) -> bool: - """Attempts to replace some indices in the current - result with new values. Useful for some purely lexicographic - reductions that we are about to perform.""" - assert self.result is not None - attempt = array("Q", self.result) - for i, v in values.items(): - # The size of self.result can change during shrinking. - # If that happens, stop attempting to make use of these - # replacements because some other shrink pass is better - # to run now. - if i >= len(attempt): - return False - attempt[i] = v - return consider(attempt) - # Now we try replacing blocks of choices with zeroes. # Note that unlike the above we skip k = 1 because we # handle that in the next step. Often (but not always) # a block of all zeroes is the shortlex smallest value # that a region can be. - k = 8 - - while k > 1: - i = len(self.result) - k - while i >= 0: - if replace({j: 0 for j in range(i, i + k)}): - # If we've succeeded then all of [i, i + k] - # is zero so we adjust i so that the next region - # does not overlap with this at all. - i -= k - else: - # Otherwise we might still be able to zero some - # of these values but not the last one, so we - # just go back one. - i -= 1 - k //= 2 + self.result = shrink_zeroes(self.result, consider) # Now try replacing each choice with a smaller value # by doing a binary search. This will replace n with 0 or n - 1 @@ -721,7 +692,13 @@ def replace(values: Mapping[int, int]) -> bool: i = len(self.result) - 1 while i >= 0: # Attempt to replace - bin_search_down(0, self.result[i], lambda v: replace({i: v})) + bin_search_down( + 0, + self.result[i], + lambda v: is_interesting_with_replacement( + self.result, {i: v}, consider + ), + ) i -= 1 # NB from here on this is just showing off cool shrinker tricks and @@ -753,7 +730,11 @@ def replace(values: Mapping[int, int]) -> bool: if j < len(self.result): # pragma: no cover # Try swapping out of order pairs if self.result[i] > self.result[j]: - replace({j: self.result[i], i: self.result[j]}) + is_interesting_with_replacement( + self.result, + {j: self.result[i], i: self.result[j]}, + consider, + ) # j could be out of range if the previous swap succeeded. if j < len(self.result) and self.result[i] > 0: previous_i = self.result[i] @@ -761,8 +742,10 @@ def replace(values: Mapping[int, int]) -> bool: bin_search_down( 0, previous_i, - lambda v: replace( - {i: v, j: previous_j + (previous_i - v)} + lambda v: is_interesting_with_replacement( + self.result, + {i: v, j: previous_j + (previous_i - v)}, + consider, ), ) @@ -817,6 +800,47 @@ def shrink_remove(self, consider): removal_index -= 1 +def shrink_zeroes(current: array[int], test: InterestTest) -> array[int]: + sizes_to_try = [8, 4, 2, 1] + for size in sizes_to_try: + i = len(current) - size + while i >= 0: + # Zero out section starting at i + attempt = current[:i] + array("Q", (0 for _ in range(size))) + current[i + size:] + + if test(attempt): + current = attempt + # If we've succeeded then all of [i, i + size] + # is zero so we adjust i so that the next region + # does not overlap with this at all. + i -= size + else: + # Otherwise we might still be able to zero some + # of these values but not the last one, so we + # just go back one. + i -= 1 + return current + + +def is_interesting_with_replacement( + current: array[int], values: Mapping[int, int], test: InterestTest +) -> bool: + """Attempts to replace some indices in the current + result with new values. Useful for some purely lexicographic + reductions that we are about to perform.""" + assert current is not None + + # If replacement map is out-of-range, abort. + # Some other shrinking pass is probably better. + if any(i >= len(current) for i in values.keys()): + return False + + attempt = array("Q", current) + for i, v in values.items(): + attempt[i] = v + return test(attempt) + + def bin_search_down(lo: int, hi: int, f: Callable[[int], bool]) -> int: """Returns n in [lo, hi] such that f(n) is True, where it is assumed and will not be checked that