计算机科学 ›› 2015, Vol. 42 ›› Issue (7): 32-37.doi: 10.11896/j.issn.1002-137X.2015.07.008
尹帮虎,陈立前,王 戟
YIN Banghu, CHEN Liqian and WANG Ji
摘要: 带指针算术的程序往往包含数组越界、缓冲区溢出等运行时错误。单纯的指针分析技术和数值分析技术都无法有效处理指针算术。为了将指针分析与数值分析相结合,首先提出一种新的指针内存模型,然后基于该模型设计了一个刻画指针指向关系和指针偏移量的抽象域。最后在抽象解释框架下,设计并实现了一个面向带指针算术C程序的静态分析工具原型PAA。实验结果表明,PAA能够有效地分析指针程序的指向关系和数值性质,并能够在效率和精度间取得合理的权衡。
[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! |
|