Closed pnevyk closed 1 year ago
Of course, first attempts to use fuzzing on currently implemented storages revealed bugs even in very simple cases.
For example, undirected AdjList
panics for
After adding check for consistency, for directed AdjList
we get even shorter sequence:
Other storages ended up very similarly.
No doubt that this effort will help tremendously.
This PR establishes an infrastructure for correctness testing using fuzzing and property-based testing. There are two main areas:
Graph storages
For graph storages, we will mainly employ fuzzing with stateful modeling of a graph behavior. For that, we have a
MutOp
enum which represents common graph manipulating operations. The test input is a sequence of such operations, either completely random or guided viaMutOpsSeq
. The operations are then applied on a graph under test. There are three levels of such testing:check_consistency
utility function.Model
type andcheck_potential_isomorphism
function.The
Model
type is an implementation of graph with the goal of being simple so it is easier to reason about its correctness. Moreover, it provides ways how to adjust the operations sequence according to specific needs using theModelParams
type andcheck
method. The model itself can be tested on levels 1 and 2.I believe it will be better to check consistency and model-conformance after every operation applied to reveal problems as soon as they occur.
The main reason for using stateful testing with sequence of operations is that it allows to assert validity of the graph also after removing operations, which are usually the hardest to implement correctly.
Algorithms
For algorithms, we will mainly employ property-based testing with fast and customizable generation of the input graphs. For that, we will utilize proptest crate with custom
GraphStrategy
. The strategy is able to generate a graph into provided type if it implements standard graph manipulation traits. It is customizable viaStrategyParams
and thus is able to generate constrained graphs to reduce the number of cases when an algorithm would unnecessarily fail on a graph structure it does not support.The graph algorithms outputs are relatively good for property-based testing. One can think of a few rules that apply to an output and often lemmas from the literature come handy. At the very least, we will usually have more than one algorithm for a problem, so that "oracle" test can be used to compare the results from different algorithms.