On the unusual effectiveness of type-aware operator mutations for testing SMT solvers
OPEN ACCESS
Author / Producer
Date
2020-11
Publication Type
Conference Paper
ETH Bibliography
yes
Citations
Altmetric
OPEN ACCESS
Data
Rights / License
Abstract
We propose type-aware operator mutation, a simple, but unusually effective approach for testing SMT solvers. The key idea is to mutate operators of conforming types within the seed formulas to generate well-typed mutant formulas. These mutant formulas are then used as the test cases for SMT solvers. We realized type-aware operator mutation within the OpFuzz tool and used it to stress-test Z3 and CVC4, two state-of-the-art SMT solvers. Type-aware operator mutations are unusually effective: During one year of extensive testing with OpFuzz, we reported 1092 bugs on Z3’s and CVC4’s respective GitHub issue trackers, out of which 819 unique bugs were confirmed and 685 of the confirmed bugs were fixed by the developers. The detected bugs are highly diverse — we found bugs of many different types (soundness bugs, invalid model bugs, crashes, etc.), logics and solver configurations. We have further conducted an in-depth study of the bugs found by OpFuzz. The study results show that the bugs found by OpFuzz are of high quality. Many of them affect core components of the SMT solvers’ codebases, and some required major changes for the developers to fix. Among the 819 confirmed bugs found by OpFuzz,184 were soundness bugs, the most critical bugs in SMT solvers,and 489 were in the default modes of the solvers. Notably, OpFuzz found 27 critical soundness bugs in CVC4, which has proved to be a very stable SMT solver.
Permanent link
Publication status
published
External links
Editor
Book title
Journal / series
Volume
4 (OOPSLA)
Pages / Article No.
193
Publisher
Association for Computing Machinery
Event
Object-oriented Programming, Systems, Languages, and Applications Conference (OOPSLA 2020)
Edition / version
Methods
Software
Geographic location
Date collected
Date created
Subject
SMT solvers; Fuzz testing; Type-aware operator mutation
Organisational unit
09628 - Su, Zhendong / Su, Zhendong