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

Mikhail Y.R. Gadelha; Enrico Steffinlongo; Lucas Cordeiro; Bernd Fischer; Denis A Nicole

doi:10.1109/ICSE-Companion.2019.00026

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

Mikhail Y.R. Gadelha
, Enrico Steffinlongo
, Lucas Cordeiro
, Bernd Fischer
, Denis A Nicole

Formal Methods

Research output: Chapter in Book/Conference proceeding › Conference contribution › peer-review

152 Downloads (Pure)

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 https://www.youtube.com/watch?v=ylW5iRYNsGA.

Original language	English
Title of host publication	41st ACM/IEEE International Conference on Software Engineering
DOIs	https://doi.org/10.1109/ICSE-Companion.2019.00026
Publication status	Published - 25 May 2019

Access to Document

10.1109/ICSE-Companion.2019.00026

bare_confAccepted author manuscript, 386 KB

Cite this

@inproceedings{6c9f9f5bffc8446b8cb798bce8dd9543,

title = "SMT-Based Refutation of Spurious Bug Reports in the Clang Static Analyzer",

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 https://www.youtube.com/watch?v=ylW5iRYNsGA.",

author = "Gadelha, \{Mikhail Y.R.\} and Enrico Steffinlongo and Lucas Cordeiro and Bernd Fischer and Nicole, \{Denis A\}",

year = "2019",

month = may,

day = "25",

doi = "10.1109/ICSE-Companion.2019.00026",

language = "English",

booktitle = "41st ACM/IEEE International Conference on Software Engineering",

}

TY - GEN

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

AU - Gadelha, Mikhail Y.R.

AU - Steffinlongo, Enrico

AU - Cordeiro, Lucas

AU - Fischer, Bernd

AU - Nicole, Denis A

PY - 2019/5/25

Y1 - 2019/5/25

N2 - 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 https://www.youtube.com/watch?v=ylW5iRYNsGA.

AB - 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 https://www.youtube.com/watch?v=ylW5iRYNsGA.

U2 - 10.1109/ICSE-Companion.2019.00026

DO - 10.1109/ICSE-Companion.2019.00026

M3 - Conference contribution

BT - 41st ACM/IEEE International Conference on Software Engineering

ER -

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

Abstract

Access to Document

Fingerprint

Cite this