Summary-based method of implementing arbitrary context-sensitive checks for source-based analysis via symbolic execution

A specific approach to summary-based interprocedural symbolic execution is described. The approach is suitable for analysis of program source code developed with high-level programming languages and allows executing arbitrarily complex checks during symbolic execution, including throwing reports in the callee function about defects that only become certain within the caller context. The structure of the function summary, procedure of applying the summary in a particular context, composition of symbolic values for particular contexts, effect of summary-based analysis on complexity of implementing specific checker modules, procedure for constructing path-sensitive bug reports, and other aspects of the implementation are discussed in detail. A particular implementation of the approach, based on Clang Static Analyzer, is described. The implementation is scalable enough to allow analysis of large-scale software projects in reasonable time, finding bugs faster than the existing implementation of the inlining-based interprocedural analysis, without sacrificing correctness and soundness of the analysis. Particular checker modules, which find various defects, such as integer overflows, modifications of constant-qualified memory, multithreading issues, array bound checks, exception safety checks, and file stream errors, were updated to use the summary-based approach, demonstrating flexibility of the technique proposed. The implementation was tested by running full intra-unit inter-procedural analysis of the Android Open Source Project codebase.