Overhaul test-primops, improving C call testing
I started rewriting some code to add support for C calls within expressions and kept finding things that were badly in need of refactoring, in particular a lot of code that wouldn't work if we wanted to add support for vectors.
Non-comprehensive list of changes:
-
Update the .cabal file, adding version bounds, commoning up logic in the common stanza, and restructuring the project to more cleanly separate library code from testing code.
-
Rename
NumbertoValueto emphasise that it is about literal values, and also becauseNumberwould become very misleading once we add support for testing vectors. -
Introduce
Typefor Cmm types. This tidies up the code and paves the way for adding testing for vectors. ParametriseExprbyTypeinstead ofFormat/Width. -
The expression type now includes C calls, which allows testing C calls as part of the general expression correctness tests. As a result, we now test more complicated C calls which return arguments (instead of only returning constants). The separate C call tests have been removed.
-
Improved shrinking for floating point constants. The old shrinker did not meaningfully shrink the complexity of a floating point value.
-
Fix the interpreter for floating-point subtraction. The old implementation used the fall-back
x+y = x + negate y, which is wrong in general (e.g.0 - NaN /= 0 + -NaN). -
Improved the shrinking for expressions by shrinking to subexpressions (both of the same type and of a different type), and removing unnecessary guards that e.g. only allowed shrinking "a+b" to "a" when "b" evaluates to 0. I believe that logic was intended to avoid causing undefined behaviour when shrinking (e.g. introducing a division by zero), but that significantly impeded shrinking. The concern about UB is now handled separately and explicitly, including avoiding introducing UB of the form (-128::W8) / (-1::W8) when shrinking.
-
Add a "bulk shrinking" mode that shrinks to powers-of-2 sizes like QuickCheck's
shrinkList. This allows quickly narrowing down the appropriate size to trigger a bug for cases when it is only the size of the expression that matters to trigger a bug. -
Use proper singletons for
Type/Format/Widthso that most of the code that dispatches on those becomes total and has good pattern match warnings. This removes a huge amount of manualtestEqualitycalls and relatederrorcalls. -
Consistently handle all situations in which evaluation is undefined (division by zero, converting a NaN to an integral type, ...). This is achieved by having the reference interpreter return
Nothingwhenever evaluation is undefined, and using that to avoid testing any expressions that contain such undefined evaluation (avoiding them while shrinking too). -
Test with both
-O0and-O.