Abstract

SMT sampling involves finding numerous satisfying assignments (samples), for an SMT formula, and is increasingly finding applications in software testing. An effective SMT sampler should achieve high throughput, yielding a large number of samples in a given time budget, and high diversity, yielding samples that cover disparate parts of the solution space.

Most SMT samplers rely on off-the-shelf SMT solvers and thus inherit those solvers’ scalability issues. Because SMT solvers tend to scale poorly when applied to floating-point constraints, the scalability and diversity of SMT sampling is correspondingly limited in the floating-point domain.

We propose JFSampler, the first SMT sampling technique built on top of coverage-guided fuzzing. JFSampler extends Just Fuzz-it Solver (JFS), a scalable but incomplete SMT solver that is effective at finding solutions to floating-point formulas by encoding satisfiability as a reachability problem that is then offloaded to a fuzzer. By building on JFS, JFSampler has an advantage over other SMT samplers in the floating-point domain. Further, we propose two novel strategies that increase both throughput and diversity of sampled solutions. First, JFSampler enhances the fuzzer’s code coverage feedback signal by measuring coverage of the formula’s solution space. Second, JFSampler incorporates a custom mutator tailored for SMT sampling. By design, these two novel techniques can be combined, having a positive synergy on throughput and diversity.

We present a large evaluation over QF_FP and QF_BVFP formulas from the SMT-LIB benchmark. Our results show that JFSampler achieves substantial improvements over SMTSampler, a state-of-the-art SMT sampling technique, when applied to floating-point formulas.