计算机科学 ›› 2015, Vol. 42 ›› Issue (7): 32-37.doi: 10.11896/j.issn.1002-137X.2015.07.008

• 2014’全国理论计算机科学年会 • 上一篇    下一篇

基于指向与数值抽象的带指针算术程序的分析方法

尹帮虎,陈立前,王 戟   

  1. 国防科学技术大学计算机学院并行与分布处理国防科技重点实验室 长沙410073,国防科学技术大学计算机学院并行与分布处理国防科技重点实验室 长沙410073,国防科学技术大学计算机学院并行与分布处理国防科技重点实验室 长沙410073
  • 出版日期:2018-11-14 发布日期:2018-11-14
  • 基金资助:
    本文受国家自然科学基金(61202120,7),教育部博士点基金(20124307120034)资助

Analysis of Programs with Pointer Arithmetic by Combining Points-to and Numerical Abstractions

YIN Banghu, CHEN Liqian and WANG Ji   

  • Online:2018-11-14 Published:2018-11-14

摘要: 带指针算术的程序往往包含数组越界、缓冲区溢出等运行时错误。单纯的指针分析技术和数值分析技术都无法有效处理指针算术。为了将指针分析与数值分析相结合,首先提出一种新的指针内存模型,然后基于该模型设计了一个刻画指针指向关系和指针偏移量的抽象域。最后在抽象解释框架下,设计并实现了一个面向带指针算术C程序的静态分析工具原型PAA。实验结果表明,PAA能够有效地分析指针程序的指向关系和数值性质,并能够在效率和精度间取得合理的权衡。

关键词: 静态分析,抽象解释,指向分析,数值抽象域

Abstract: ions YIN Bang-hu CHEN Li-qian WANG Ji (National Laboratory for Parallel and Distributed Processing,School of Computer Science, National University of Defense Technology,Changsha 410073,China) Abstract Programs with pointer arithmetic often involve runtime errors such as array out of bound,buffer overflow,etc.Pure pointer analysis and pure numerical analysis cannot deal with pointer arithmetic.To combine pointer analysis and numerical analysis,we proposed a new pointer memory model.On this basis,we presented an abstract domain to capture points-to and offset information of pointers.Finally,under the framework of abstract interpretation,we implemented a static analyzer prototype named PAA for analyzing C programs with pointer arithmetic.Experimental results show that PAA can analyze points-to and numerical properties of programs with pointer arithmetic effectively.More-over,PAA can achieve a reasonable trade-off between efficiency and accuracy.

Key words: Static analysis,Interpretation,Points-to analysis,Numerical abstract domain

[1] Dong W,Chen L Q.Recent advances on trusted computing in China[J].Chinese Science Bulletin,2012,57(35):4529-4532
[2] Steensgaard B.Points-to analysis in almost linear time[C]∥Proceedings of the 23rd ACM SIGPLAN-SIGACT symposium on Principles of programming languages.ACM,1996:32-41
[3] Andersen L O.Program analysis and specialization for the Cprogramming language[D].University of Cophenhagen,1994
[4] Cousot P,Cousot R.Interpretation:a unified lattice model forstatic analysis of programs by construction or approximation of fixpoints[C]∥Proceedings of the 4th ACM SIGACT-SIGPLAN Symposium on Principles of Programming Languages.ACM,1977:238-252
[5] 陈立前.基于区间线性抽象域的可靠浮点及非凸静态分析[D].长沙:国防科学技术大学,2010 Chen Li-qian.Sound floating-point and non-convex static analysis using interval linear abstract domains[D].Changsha:School of National University of Defense Technology,2010
[6] Cousot P,Cousot R,Feret J,et al.The ASTRéE analyzer[M]∥Programming Languages and Systems.Springer Berlin Heidelberg,2005:21-30
[7] Delmas D,Goubault E,Putot S,et al.Towards an industrial use of FLUCTUAT on safety-critical avionics software[M]∥Formal Methods for Industrial Critical Systems.Springer Berlin Heidelberg,2009:53-69
[8] Venet A,Brat G.Precise and efficient static array bound checking for large embedded C programs[J].ACM SIGPLAN Notices,2004,39(6):231-242
[9] Hasti R,Horwitz S.Using static single assignment form to improve flow-insensitive pointer analysis[J].ACM SIGPLAN Notices.ACM,1998,33(5):97-105
[10] Yu H,Xue J,Huo W,et al.Level by level:making flow-and context-sensitive pointer analysis scalable for millions of lines of code[C]∥Proceedings of the 8th annual IEEE/ACM international symposium on Code generation and optimization.ACM,2010:218-229
[11] Whaley J,Lam M S.Cloning-based context-sensitive pointeralias analysis using binary decision diagrams[J].ACM SIGPLAN Notices.ACM,2004,39(6):131-144
[12] King J C.Symbolic execution and program testing[J].Communications of the ACM,1976,19(7):385-394
[13] Hampapuram H,Yang Y,Das M.Symbolic path simulation in path-sensitive dataflow analysis[J].ACM SIGSOFT Software Engineering Notes.ACM,2005,31(1):52-58
[14] Xu Z,Kremenek T,Zhang J.A memory model for static analysis of C programs[M]∥Leveraging Applications of Formal Methods,Verification,and Validation.Springer Berlin Heidelberg,2010:535-548
[15] Canet G,Cuoq P,Monate B.A Value Analysis for C Programs[C]∥2013 IEEE 13th International Working Conference on Source Code Analysis and Manipulation(SCAM).IEEE,2009:123-124
[16] Miné A.Weakly relational numerical abstract domains[D].Paris:cole Normale Supérreure,2004
[17] Necula G C,McPeak S,Rahul S P,et al.CIL:Intermediate language and tools for analysis and transformation of C programs[C]∥Compiler Construction.Springer Berlin Heidelberg,2002:213-228
[18] Chen L,Li R,Wu X,et al.Static analysis of list-manipulating programs via bit-vectors and numerical abstractions[C]∥Proceedings of the 28th Annual ACM Symposium on Applied Computing.ACM,2013:1204-1210
[19] 李梦君,李舟军,陈火旺.基于抽象解释理论的程序验证技术[J].软件学报,2008,19(1):17-26 Li Meng-jun,Li Zhou-jun,Chen Huo-wang.Program verification techniques based on the abstract interpretation theory[J].Journal of Software,2008,19(1):17-26
[20] SNUReal-Time Benchmark Suite.http://archi.snu.ac.kr/realtime/benchmark
[21] von Hanxleden R,Holsti N,Lisper B,et al.WCET tool challenge 2011:report.http://hdl.handle.net/22909/10354

No related articles found!
Viewed
Full text


Abstract

Cited

  Shared   
  Discussed   
No Suggested Reading articles found!