ddsexpr

Fuzzing and Delta-Debugging of S-Expressions

We provide a classical fuzzer and delta-debugger for S-Exprs, i.e., LISP and SMT terms. The fuzzer mutates existing files and both the fuzzer and the delta-debugger are only partially grammar aware. Initially we used these tools to make the SMT2 parser of Boolector more robust, e.g., to avoid segmentation faults on malformed input or during parse error messages etc.

The delta-debugger has three phases. First phase is line based, second phase tries to use the hierarchical structure of S-Expressions and third phase is character based. Thus it works reasonable well for many other formats as well. We successfully used it for instance on SMT, BTOR and SMV files. It also makes sense to interleave it with a grammar-based delta-debugger such as ddSMT for SMT.

There are a README, and LICENSE files. The actual code of the fuzzer and delta-debugger is bundled and available as ddsexpr1.tar.gz.