Static analysis of C programs via region-based memory model

被引：0
作者：
Dong, Yu-Kun [1 ,2 ]
Jin, Da-Hai [1 ]
Gong, Yun-Zhan [1 ]
Xing, Ying [1 ]
机构：
[1] State Key Laboratory of Networking and Switching Technology, Beijing University of Posts and Telecommunications
[2] College of Computer and Communication Engineering, China University of Petroleum
来源：
Ruan Jian Xue Bao/Journal of Software | 2014年 / 25卷 / 02期
关键词：
Addressable expression; Defect detection; Memory model; Static analysis; Symbolic function summary;
D O I：
10.13328/j.cnki.jos.004532
中图分类号：
学科分类号：
摘要：
In order to improve the precision of static analysis for C procedures, this paper introduces a static analysis method applying region-based symbolic three-valued logic (RSTVL). RSTVL can describe shape of data structures, all kinds of memory states and relations of addressable expressions including alias relations, hierarchical relations and logic relations. To improve precision, a RSTVL- based analysis method is proposed to analyze the shape, dataflow and point-to relationship at every procedure point. The method facilitates flow-sensitive and field-sensitive intra-procedure, and context-sensitive inter-procedure analysis based on symbolic function summary. Experimental results validate that the porposed static analysis method offers higher precision on the precondition with no efficiency loss. © Copyright 2014, Institute of Software, the Chinese Academy of Sciences. All rights reserved.
引用
收藏
页码：357 / 372
页数：15
相关论文
共 28 条
  • [1] Dong Y.K., Xing Y., Jin D.H., Gong Y.Z., An approach to fully recognizing addressable expression, Proc. of the 13th Int'l Conf. on Quality Software, pp. 149-152, (2013)
  • [2] Zhang J., Symbolic execution of program paths involving pointers and structure variables, Proc. of the 4th Int'l Conf. on Quality Software, pp. 87-92, (2004)
  • [3] Mooly S., Thomas R., Reinhard W., Solving shape-analysis problems in languages with destructive updating, ACM Trans. on Programming Languages and Systems, 20, 1, pp. 1-50, (1998)
  • [4] Lev-Ami T., Sagiv M., TVLA: A system for implementing static analyses, Proc. of the 7th Int'l Static Analysis Symp., pp. 280-301, (2000)
  • [5] Wilson R.P., Monica S., Lam. Efficient context-sensitive pointer analysis for C programs, Proc. of the ACM SIGPLAN 1995 Conf. on Programming Language Design and Implementation, pp. 1-12, (1995)
  • [6] Xu Z.X., Kremenek T., Zhang J., A memory model for static analysis of C programs, Proc. of the Leveraging Applications of Formal Methods, Verification, and Validation, pp. 535-548, (2010)
  • [7] Zhao Y.S., Wang Y.W., Gong Y.Z., Chen H.H., Xiao Q., Yang Z.H., STVL: Improve the precision of static defect detection with symbolic three-valued logic, Proc. of the 8th Asia-Pacific Software Engineering Conf., pp. 179-186, (2011)
  • [8] Blanchet B., Cousot P., Cousot R., Feret J., Mauborgne L., Mine A., Monniaux D., Rival X., A static analyzer for large safety-critical software, Proc. of the ACM SIGPLAN 2003 Conf. on Programming Language Design and Implementation, pp. 196-207, (2003)
  • [9] Choi J.D., Burke M., Carini P., Efficient flow-sensitive interprocedural computation of pointer-induced aliases and side effects, Proc. of the 20th ACM SIGPLAN-SIGACT Symp. on Principles of Programming Languages, pp. 232-245, (1993)
  • [10] Mine A., Field-Sensitive value analysis of embedded C programs with union types and pointer arithmetics, Proc. of the 2006 ACM SIGPLAN/SIGBED Conf. on Language, Compilers, and Tool Support for Embedded Systems, pp. 54-63, (2006)
123