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

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 current heuristics for removing spurious bug reports. We encode the path constraints produced by...

Full description

Saved in:
Bibliographic Details
Main Authors: R. Gadelha, Mikhail, Steffinlongo, Enrico, C. Cordeiro, Lucas, Fischer, Bernd, Nicole, Denis
Format: Conference Proceeding
Language:English
Subjects:
clang
Computer bugs
Libraries
Open source software
Reactive power
Runtime
SMT Solvers
Static analysis
Online Access:Request full text
Tags: Add Tag
No Tags, Be the first to tag this record!
Description
Summary: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 current heuristics for removing 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 https://www.youtube.com/watch?v=ylW5iRYNsGA.
ISSN:2574-1934
DOI:10.1109/ICSE-Companion.2019.00026