期刊名称：Studia Universitatis Babes-Bolyai : Series Informatica
印刷版ISSN：1224-869X
出版年度：2018
卷号：63
期号：2
页码：1-14
DOI：10.24193/subbi.2018.2.06
出版社：Babes-Bolyai University, Cluj-Napoca
摘要：Static analysis is a widely used method for finding bugs in
large code bases. One of the most popular static analysis tools used for
software written in C/C++ languages is the Clang Static Analyzer [1].
During symbolic execution [2] of the source code, the analyzer models
path sensitivity by keeping track of constraints on symbolic variables. The
built-in constraint manager module, while granting excellent performance,
only handles constraints on certain types of integer expressions, which has
a detrimental effect on the quality of the analysis, as the infeasibility of
certain execution paths cannot be proved. This often leads to false positive
findings, i.e. error reports issued for code parts that are actually correct.
This paper records the first milestone in an effort to integrate the
state-of-the-art Z3 theorem prover [3] into the Clang Static Analyzer in
order to post-process bug reports. While full integration is hindered by
the burden Z3 places on the duration of the analysis, the refutation of
false positive reports using information collected by the default pass can
improve analysis quality substantially while introducing only a moderate
regression in performance. We present an initial prototype of the tiered
constraint solving solution that is already capable of filtering out some
bogus reports, evaluate it on real-world software projects, and explore
possible improvements we plan to accomplish in our future work.
