Better expression shrinker

[j-hui]

There are a lot of expressions which should be easily, statically shrunk into constants. I'm not really sure what is gonig on with the shrinker right now but all the massive expressions really clutter up what could be smaller test cases.

[Rewbert]

There's no shrinking of expressions going on at all right now. I focused on shrinking statements, as that makes a program 'more' small ;) But expressions should be shrunk, absolutely. It's not something I will prioritize until after the paper deadline, I think. There are some other small things that I need to fix with the expression shrinker as well. Some programs are shrunk a lot, but could still be shrunk even more.

Just as a quick intro to something that confused me a bit now when I learned this myself recently:

QuickCheck shrinking is not of the form that e.g it turns 5 + 7 into the subexpression 12, but rather it turns 5 + 7 into the subexpressions 5 & 7. You could pattern match on this specific case of integer constants arithmetic, of course, and produce the subexpressions 5, 7 & 12, but it won't be the general case that expressions are normalized. It's a syntactical division of the tree into its immediate subtrees.

If you have (5 + 7) * (7 - 2) you turn that into the subexpressions 5 + 7 & 7 - 2. You don't recursively shrink them further yourself, as QuickCheck automatically does that for you if it needs to. Nothing will go wrong if you do it yourself, but it might slow down shrinking as you might test more mutations than you have to.

[j-hui]

I suppose chopping expressions into bits and pieces works too, but is there no way to essentially pipe the example programs through a constant-folder sort of pass?

[Rewbert]

You could, yes. The shrink interface as seen by QuickCheck is the function shrink :: a -> [a], which in our case is shrink :: Program -> [Program]. The result could be the singleton list containing the folded program. What you are describing is not necessarily the way shrinking is usually done though. It's supposed to be a

E.g an expression such as 5 + 7 would presumable have been evaluated while being subjected to a test, so shrinking and then testing 12 would test the semantically equivalent program, even if it is syntactically smaller. If you perform this constant folding and the new program also fails, you can not shrink it further as it is now a single leaf node rather than a tree. Maybe the bug only appears if the number is odd? The arbitrary & shrink functions are supposed to be quite 'simple' in their operation.

[j-hui]

We can include constant folding as one of the shrinking strategies involved, and even constant perturbation (replacing larger constant numbers with smaller ones), etc. We can include all of these as part of the various expression shrinking used in shrinking expressions, in addition to purely syntactic reduction (where we just drop entire terms from expressions).

On Fri, Jun 25, 2021 at 4:20 PM Robert Krook @.***> wrote:

You could, yes. The shrink interface as seen by QuickCheck is the function shrink :: a -> [a], which in our case is shrink :: Program -> [Program]. The result could be the singleton list containing the folded program. What you are describing is not necessarily the way shrinking is usually done though. It's supposed to be a

E.g an expression such as 5 + 7 would presumable have been evaluated while being subjected to a test, so shrinking and then testing 12 would test the semantically equivalent program, even if it is syntactically smaller. If you perform this constant folding and the new program also fails, you can not shrink it further as it is now a single leaf node rather than a tree. Maybe the bug only appears if the number is odd? The arbitrary & shrink functions are supposed to be quite 'simple' in their operation.

— You are receiving this because you authored the thread. Reply to this email directly, view it on GitHub https://github.com/Rewbert/ssm-edsl/issues/31#issuecomment-868812883, or unsubscribe https://github.com/notifications/unsubscribe-auth/AC2A5DDN4ULW546U4MFCYYLTUTQJZANCNFSM47KOHIZA .

[j-hui]

Fixed by #39