SMT-Based Refutation of Spurious Bug Reports in the Clang Static Analyzer

TL;DR

This paper introduces an SMT-based extension for the Clang Static Analyzer that effectively refutes spurious bug reports with minimal performance impact, improving accuracy in open-source software analysis.

Contribution

We develop an SMT-based bug refutation extension that enhances Clang Static Analyzer's ability to eliminate false positives more accurately.

Findings

Refutes 8 out of 12 open-source applications' spurious bugs

On average refutes 7% of all bug reports

Adds only 1.2% overhead to the Clang/LLVM toolchain

Abstract

We describe and evaluate a bug refutation extension for the Clang Static Analyzer (CSA) that addresses the limitations of the existing built-in constraint solver. In particular, we complement CSA's existing heuristics that remove spurious bug reports. We encode the path constraints produced by CSA as Satisfiability Modulo Theories (SMT) problems, use SMT solvers to precisely check them for satisfiability, and remove bug reports whose associated path constraints are unsatisfiable. Our refutation extension refutes spurious bug reports in 8 out of 12 widely used open-source applications; on average, it refutes ca. 7% of all bug reports, and never refutes any true bug report. It incurs only negligible performance overheads, and on average adds 1.2% to the runtime of the full Clang/LLVM toolchain. A demonstration is available at {\tt https://www.youtube.com/watch?v=ylW5iRYNsGA}.