StringFuzz: A Fuzzer for String SMT Solvers

Abstract

We introduce StringFuzz, a software tool for automatically testing string SMT solvers. String SMT solvers are specialised software tools for solving the Satisfiability Modulo Theories (SMT) problem with string contraints, which is a type of constraint satisfaction problem applicable in industry. Like all tools, string SMT solvers need testing. The developers of solvers commonly test them with published test suites: pre-generated sets of problem instances (i.e. example problems). As new features are added to string SMT solvers, they often are not exercised by existing suites. We introduce StringFuzz, a tool for solver developers to generate SMT instances to exercise and find defects in their solvers. We describe StringFuzz’s features for generating and transforming SMT instances with string and regex constraints. We also show StringFuzz’s many controls, and show how to use them to generate specially tuned scaling instances. For public use, we present our own suite of StringFuzz-generated SMT instances. We also introduce StringBreak, an automated exploratory tester for string SMT solvers, which uses a genetic algorithm to generate SMT instances that take a long time for solvers to solve. To demonstrate the usefulness of StringFuzz and StringBreak, we show experimental results from testing leading string SMT solvers (Z3str3, CVC4, Z3str2, and Norn) with them. We describe two defects and one potential future enhancement that we discovered in Z3str3 as a result of our experiments.