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

Improve integer shrinking #743

Open
wants to merge 8 commits into
base: main
Choose a base branch
from

Conversation

jonaskoelker
Copy link
Contributor

This is my implementation of #735.

I have included some extra tests of shrinking, which prevents regressions of #244 more thoroughly. I added them mainly so I could be sure my new shrinker works as desired.

I recommend you read my code changes before reading the following side notes:

I think the tests on the form property("shrink[Byte]") = forAll { (n: Byte) => !shrink(n).contains(n) } are superfluous (given my acyclic tests), and I'll happily write a commit which deletes them if you like. Otherwise, I think they should use forAllNoShrink, otherwise shrinking will go into an infinite loop when they fail. In general, I think tests of shrinkers should use forAllNoShrink in almost all circumstances: if the shrinker is buggy, how interested are you in the minimal gold-in-garbage-out counterexample it produces? I guess you could shrink with a different shrinker, but will you test the second shrinker, and the third, etc.?

The tests on the form property("shrink[Byte] != 0") = forAll { (n: Byte) => (n != 0) ==> shrinkClosure(n).contains(0) } also caught my attention: shrinkClosure looks dangerous to call on buggy infinite-regress shrinkers. A safer test which proves the same thing, for integral types, is this: forAllNoShrink { (n: T) => (n == 0) == shrink(n).isEmpty }. Assuming the shrink function is a strict partial order (i.e. the tests I've added cannot fail) and also assuming the above test succeeds, all values except zero shrink to something, and since shrinking is acyclic (and thus finite for finitely inhabited types), all shrinking processes transitively shrink to zero. But since we only do a single shrink in the test I'm suggesting, it will not hang if shrinking is cyclic. It might incorrectly succeed, or fail to prove what I think you want, but in that case the "x is acyclic" tests will fail, so you will know there is something to correct.

I'd like to hear your thoughts about why you prefer property("shrink[Byte] != 0") = forAll { (n: Byte) => (n != 0) ==> shrinkClosure(n).contains(0) } to forAllNoShrink { (n: T) => (n == 0) == shrink(n).isEmpty }, if that is indeed the case, or else whether you'd like me to make the change.

We all know that we shrink towards 0 and from negative to positive.
Formalizing this is simple and strengthens the typelevel#244 regression tests.
So long as the test case keeps succeeding, shrink to the next query
value of a binary search that searches for the smallest failing value.

That is, try the midpoint between the most recent test failure and the
previous shrunk value: x => x * (1 - 1/2^k) for natural numbers k.

For example, `shrink(32).toList == List(0, 16, 24, 28, 30, 31)`.
@jonaskoelker
Copy link
Contributor Author

MiMa helpfully caught a binary incompatibility. I told MiMa "thank you, that's okay". I can also add back the skipNegation even though we don't use it any longer (we address the same concern in a different way).

Base automatically changed from master to main March 26, 2021 18:56
@jonaskoelker
Copy link
Contributor Author

As an illustrating example of why this shrinker may be more useful, I stumbled upon this test.

The error is overflow. That's why the same property fails for Int but succeeds for BigInt. The products xz and yz tend to be close to Integer.MIN_VALUE or Integer.MAX_VALUE with the new and (IMO) improved shrinker; this is not the case for the old shrinker. That is, I find that the new shrinker provides better debugging clues in at least this one scenario. [In general, if the boundary between failure and succees lies between n/2 and n, where n is the initial failure value, then the new shrinker will find it and the old shrinker will not.

import org.scalacheck.{Arbitrary, Properties, Shrink}
import org.scalacheck.Prop.{forAll, forAllShrink, propBoolean}

object GcdProperties extends Properties("GCD") {
  def gcd[T: Integral](a: T, b: T): T = {
    val num = implicitly[Integral[T]]
    if (a == 0) num.abs(b) else gcd(num.rem(b, a), a)
  }

  property("scales and commutes (Int)") = forAll {
    (x: Int, y: Int, z: Int) =>
    s"${x * z} and ${y * z}" |: gcd(z*x, z*y) == z.abs * gcd(y, x)
  }

  property("scales and commutes (BigInt)") = forAll {
    (x: BigInt, y: BigInt, z: BigInt) => gcd(z*x, z*y) == z.abs * gcd(y, x)
  }

  val shrinkThreeInts = {
    implicit val intShrinkFunction = Shrink {
      (n: Int) => Stream
        .range(0, 31)
        .map(k => n - n / (1 << k))
        .filter(_.abs < n.abs)
    }
    implicitly[Shrink[(Int, Int, Int)]].shrink _
  }

  property("scales and commutes (Int) with explicit shrinker") =
    forAllShrink(Arbitrary.arbitrary[(Int, Int, Int)], shrinkThreeInts) {
      case (x, y, z) =>
        s"${x * z} and ${y * z}" |:
        gcd(z*x, z*y) == z.abs * gcd(y, x)
    }
}

@jonaskoelker
Copy link
Contributor Author

It occurred to me that I could write a test case which asserts that shrinking finds the exact success/failure boundary, so I did.

On the way I stumbled upon a few ways in which the earlier code could be improved.

Now the shrinker does the same algebra as the rust-quickcheck shrinking of fixed-size signed integer types, which does the right thing for the one unsigned Scala type I can think of (Char), as well as for arbitrary-precision integers (BigInt).

@jonaskoelker
Copy link
Contributor Author

I can also add back the skipNegation even though we don't use it any longer (we address the same concern in a different way).

I searched on GitHub for skipNegation. Almost all hits were in files named Shrink.scala in various repositories. Almost all remaining hits were in copies of the Shrink.scala I'm changing (in gists, etc.). One occurrence of skipNegation was inside a string literal which from context looked completely unrelated to ScalaCheck. I also did a generic web search for "skipNegation scalacheck", and all three hits were on scalacheck.org.

TL;DR: no one uses skipNegation except Shrink.scala itself. We are not inconveniencing anyone by removing it, as far as I can tell.

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
None yet
Projects
None yet
Development

Successfully merging this pull request may close these issues.

None yet

1 participant