Multi-level Static Analysis for Finding Error Patterns and Defects in Source Code

This paper presents the formalism for multiple level static analysis for defect detection in source code. The first level has the program and memory model that are suitable for AST-level checks. The following levels address detection of critical errors: on the second level interprocedural partially context-sensitive analysis is performed via dataflow analysis and symbolic execution with state merging, whereas the third level adds path-sensitivity via predicate tracking for the dataflow information computed on the second. The analysis designer can freely choose the appropriate analysis level or their combination to check the desired program property. The presented methods are implemented in the Svace static analysis toolset. The first analysis levels for C/C++ and Java are implemented as extensions of corresponding production compilers (Clang and javac) and Find-Bugs tool plugins, while the second and third levels make the core of Svace analyzer together with 100+ implemented checkers for critical defects. The evaluation on extra large codebases of millions lines of code such as full-blown Android and Tizen OSes has shown the approach scalability and the acceptable false positives ratio (less than 40%).