Summary-based interprocedural analysis method for implementation in multi-purpose static C/C++ code analyzer

The paper gives a detailed description of the summary-based interprocedural analysis method developed for the symbolic execution method. This method is implemented in the analyzer model of Clang Static Analyzer, using its framework. This allows using the summary-based method for developing a multi-purpose analyzer with the ability to search for various defects in programs with C and C++ software codes. The author describe summary collecting methods and their application in symbolic execution, as well as in translating symbolic meanings from a callee context to a caller one and vice versa. The method of the defect report building with the help of the summary-based interprocedural analysis method is also developed and presented in the paper. The research aims at developing an analyzer suitable for doing an interprocedural analysis of large software projects, such as Android, in reasonable time. The results of measuring the analysis time are given. The summary-based and inlining methods are compared.

References

[1] James C. King. Symbolic execution and program testing. Communications of the ACM, 1976, vol. 19, no. 7, pp. 385-394.

[2] Aho A., Lam M., Sethi R., Ullman D. Compilers: Principles, Techniques, and Tools. Addison-Wesley, 1986.

[3] Cadar C., Dunbar D., Engler D. KLEE: Unassisted and automatic generation of high-coverage tests for complex systems programs. In Proc. of the USENIX Symposium on Operating System Design and Implementation, 2008.

[4] Cha Sang Kil, Avgerinos Th., Rebert A., Brumley D. Unleashing Mayhem on Binary Code. In Proc. of the 33rd IEEE Symposium on Security and Privacy, 2012.

[5] Reisner E., Song Ch., Ma Kin-Keung, Foster Jeffrey S., Porter A. Using Symbolic Evaluation to Understand Behavior in Configurable Software Systems. In Proc. of the 32nd International Conference on Software Engineering (ICSE), Cape Town, South Africa, 2010, pp. 445-454.

[6] Xu Zh., Zhang J., Xu Zh. Melton: a practical and precise memory leak detection tool for C programs. Frontiers of Computer Science in China, 2015, vol. 9, no. 1, pp. 34-54.

[7] Qadeer S., Rajamani S., Rehof J. Summarizing procedures in concurrent programs. 31st Annual ACM SIGPLAN-SIGACT Symp. on Principles of Programming Languages, 2004, vol. 39, pp. 245-255.

[8] Braberman V., Garbervetsky D., Hym S., Yovine S. Summary-based inference of quantitative bounds of live heap objects. Science of Computer Programming, 2013, vol. 92, pp. 56-84.

[9] Clang Static Analyzer. URL: http://clang-analyzer.llvm.org (accessed: 15.04.2015).

[10] Clang: a C Language Family Frontend for LLVM. URL: http://clang.llvm.org (accessed: 15.04.2015).

[11] The LLVM Compiler Infrastructure. URL: http://llvm.org (accessed: 14.04.2015).

[12] Ignat’ev V.N. Usage of the lightweight static analysis for checking adaptive semantic constraints of the software programming language. Tr. Instituta sistemnogo programmirovaniya RAN [Proc. of The Institute for Systems Programming, Russian Academy of Sciences], 2012, vol. 22, pp. 169-188 (in Russ.).

[13] Sargsyan S., Kurmangaleev Sh. Belevantsev, A., Aslanyan A., Baloyan A. Zoomed searching tool of code clones based on program semantics analysis. Tr. Instituta sistemnogo programmirovaniya RAN [Proc. of The Institute for Systems Programming, Russian Academy of Sciences], 2015, vol. 27, pp. 39-50 (in Russ.).

[14] Reps T., Horwitz S., Sagiv M. Precise interprocedural dataflow analysis via graph reachability. In POPL ’95 Proc. of the 22nd ACM SIGPLAN-SIGACT symp. on Principles of programming languages, 1995, pp. 49-61.

[15] Xu Z., Kremenek T., Zhang J. A memory model for static analysis of C programs. In ISoLA’10 Proc. of the 4th international conf. on Leveraging applications offormal methods, verification, and validation, 2010, pp. 535-548.