Breccia: A Functional DSL Compiled to Egglog for Test Input Generation
摘要
Some prominent efforts within fuzz testing to automatically generate test inputs with complex invariants (e.g., well-typed programs for fuzzing compilers) have exploited logical satisfaction, such as using Prolog to describe constraints and generate satisfying instances. However, using Prolog has met with resistance from the community due to the difficulty of writing Prolog descriptions with acceptable performance. We propose an alternative logic programming-based approach: Datalog. While Datalog improves on the “effective programmability” of Prolog, it has its own issues: it is less expressive than Prolog, its bottom-up evaluation strategy requires keeping all generated terms in memory, and while it is easier to program effective generators in Datalog than Prolog, it still requires a specific style and has hidden pitfalls (such as bounding). We introduce Breccia, a functional DSL for generating objects with complex invariants that compiles to Egglog, a Datalog language extended with equality saturation. We show that Breccia is expressive enough to describe interesting objects such as well-typed programs with non-trivial type systems, and that equality saturation can greatly improve the performance of the resulting Egglog generator. We compare Breccia against Prolog implementations of similar generators in order to understand the tradeoffs involved.