Refining CrossHair's Internal Testing Strategy

[pschanely]

A collection of notes about testing CrossHair:

• Most tests exercise logic by checking a contract on a function. In many cases, this exercises more code than we'd like. There is now a standalone_statespace context manager that correctly sets up a full symbolic environment. This can be used directly in tests, along with the statespace's is_possible() method to verify symbolic execution more directly. However, this only works if you know how your code under test is going to branch - otherwise, ambiguous branches will be selected arbitrarily.
• The test suite takes a while to run. If we ever complete symbolic handling of the entire standard library, we'd be looking at hours of runtime, with our current approaches.
• Since our symbolics try to emulate regular Python, we have an "oracle" to compare to. This opens the door for a lot of automatic tests that could exist.
• The potential for flaky tests is high when using something like z3. CrossHair now has a max_iterations config option, and I'm hoping we can turn up the timeouts and rely on max_iterations to get improved determinism. One challenge here: sometimes we need one path to timeout so that we can move on to another, more fruitful path.
• builtinslib_ch_test.py is one of the most efficient bug-finders we have right now. It essentially runs CrossHair on our own functions; this will repeatedly choose paths, realize the inputs, and compare to the native Python implementation of the same code. Because of the way CrossHair works, each iteration is effectively trying to gain code coverage. An important added benefit is that because CrossHair may pre-maturely realize inputs, it will check cases where some arguments are symbolic and some are native - bugs due to mixed arguments are common.
• fuzz_core_test.py is an older attempt at a fuzz test - in some ways, it's the opposite of builtinslib_ch_test.py - it starts with native values, and compares the same code applied to symbolics that have been constrained to be equal to the native values. Right now it mostly just finds errors where the arguments are of the wrong types; such bugs are lower priority - most people will also use a type checker which will usually prevent TypeErrors more effectively. It also doesn't use pytest's parametrize, and so it's annoying to go digging through the log when there's a failure. This is ripe for a rewrite.

[Rik-de-Kort]

Continuing on from #98 (it feels like going backwards):

• With regards to shrinking logic for counterexamples, one thing we could do: given the counterexample, we can generate a constructor and bytestream that leads to that example, and then use the Hypothesis shrinker. To prevent coupling to Hypothesis internals we could keep our own library of constructors. The shrinker is of course optimized for the Hypothesis values, but it should also work decently well for "similar" things. How often does this happen though, and how often is there a "straightforward" minimization (like using smaller lists)?

Also in regards to testing stmbolic behaviour is equivalent, this exists: https://github.com/python/cpython/tree/master/Lib/test ;)

[pschanely]

Re reversing hypothesis strategies, you might be interested in this early experiment and these notes. Another option for minimization is to investigate Z3 optimization and try to optimize for small lists, numbers etc, but I have a feeling the optimization algorithems may not work well for our kinds of cross-theory constraints.

Re equivalent behavior: yeah, the CPython tests could be handy at least for testing our library patches. (though I'm not sure how we'd make those tests use our symbolic values?). Another idea is to just generate arbitrary code and try to run it. The existing fuzz test sort of does this - it essentially tries to generate a single expression or method call and compares the behavior.