A common problem in automated software testing is the need to generate many inputs with a well-defined structure in a black box fashion. For example, a library for manipulating red-black trees may require that inputs are themselves valid red-black trees, meaning anything invalid is not suitable for testing. As another example, in order to test code generation in a compiler, it is necessary to use input programs which are both syntactically valid and well-typed. Despite the importance of this problem, we observe that existing solutions are few in number and have severe drawbacks, including unreasonably slow performance and a lack of generality to testing different systems.
In this talk, I will present a solution to this problem of structured input generation. I observe that test inputs can be described as solutions to systems of logical constraints, and that a variety of search strategies can be used to solve these constraints. These two observations naturally end themselves to the use of constraint logic programming (CLP), which serves as an excellent foundation for building test input generators. Via a series of case studies, I have found that CLP (1) is applicable to testing a wide variety of systems; (2) can scale to more complex constraints than ever previously described; and (3) is often orders of magnitude faster than prior solutions. These case studies have exposed dozens of bugs in high-profile software, including the Rust compiler and the Z3 SMT solver. I will show highlights from these case studies, along with an in-depth look at some of them.