SMT-Based Refutation of Spurious Bug Reports in the Clang Static Analyzer
- Track: LLVM devroom
- Room: K.4.201
- Day: Sunday
- Start: 14:15
- End: 14:55
I will present a new option added to the clang static analyzer (CSA) to refute false bug reports, using satisfiability modulo theory (SMT) solvers. In this talk, I will:
(1) give a general overview of the CSA, how it works and its limitations;
(2) show how we extended the existing heuristics to remove spurious bug reports: path constraints produced by CSA are encoded as SMT problems, SMT solvers precisely check them for satisfiability, and bug reports (whose associated path constraints are unsatisfiable) are removed;
(3) show the evaluation of our refutation algorithm when analyzing twelve widely used open-source projects;
(4) show how to set up an automated testing environment using scripts provided by the CSA infrastructure. As an example, I will show how to set up the twelve projects used to evaluate our refutation algorithm: https://github.com/mikhailramalho/analyzer-projects.
The target audience of this talk is anyone interested in learning more about the clang static analyzer and in analyzing their C/C++/ObjectiveC projects.
The clang static analyzer works by symbolically executing a program, collecting the symbols and constraints for every path in the program, and reasoning about bug feasibility using a built-in solver called RangedConstraintManager. It was designed to be fast so that it can provide results for common mistakes (e.g., division by zero or use of uninitialized variables) even in complex programs. However, the speed comes at the expense of precision; it cannot handle some arithmetic operations (e.g, remainders) or bitwise expressions. In these cases, the analyzer discards the constraints and might report false bugs.
The new option works by adding an extra step in the program analysis after the bug is found by the built-in solver but before reporting it to the user; the path and the constraints that trigger the bug are encoded in SMT and checked for satisfiability.
I will present an evaluation of the crosscheck when analyzing twelve C/C++ open-source projects of various size (tmux, redis, openssl, twin, git, postgresql, sqlite3, curl, libWebM, memcached, xerces-c, and XNU). When analyzing these projects with bug validation enabled, the slowdown is negligible in cases where no bug is refuted (average 1.2% slowdown) and, when it finds false bugs, the bug validation gives a small speedup (average 6.2% speedup). On average, 12.2 bugs per program were refuted by the SMT solver, ranging from 1 bug refuted in redis to 51 being refuted in XNU.
Finally, I will present a set of scripts provided by the CSA that can be used to set up an automated testing environment. The scripts are freely available and their presentation will follow the process described in https://github.com/mikhailramalho/analyzer-projects.
Speakers
| Mikhail Gadelha |