›› 2013,Vol. 28 ›› Issue (6): 1063-1084.doi: 10.1007/s11390-013-1398-1

• Special Section on Selected Paper from NPC 2011 • 上一篇    下一篇

形状图逻辑和形状图系统

Zhao-Peng Li1, 2 (李兆鹏), Member, CCF, Yu Zhang1, 2, * (张昱), and Yi-Yun Chen1, 2 (陈意云), Member, CCF   

  • 收稿日期:2012-11-21 修回日期:2013-09-20 出版日期:2013-11-05 发布日期:2013-11-05
  • 作者简介:Zhao-Peng Li is a postdoctoral researcher in School of Computer Science and Technology, University of Science and Technology of China, Hefei. He received his Ph.D. degree in computer science from University of Science and Technology of China in 2008. His research interests include program verification, certifying compiler and theorem proving. He is a member of China Computer Federation.

A Shape Graph Logic and A Shape System

Zhao-Peng Li1, 2 (李兆鹏), Member, CCF, Yu Zhang1, 2, * (张昱), and Yi-Yun Chen1, 2 (陈意云), Member, CCF   

  1. 1 School of Computer Science and Technology, University of Science and Technology of China, Hefei 230027, China;
    2 Software Security Laboratory, Suzhou Institute for Advanced Study, University of Science and Technology of China Suzhou 215123, China
  • Received:2012-11-21 Revised:2013-09-20 Online:2013-11-05 Published:2013-11-05
  • Supported by:

    This research was supported by the National Natural Science Foundation of China under Grant Nos. 61003043, 61170018, the National High Technology Research and Development 863 Program of China under Grant No. 2012AA010901-2, and the Postdoctoral Science Foundation of China under Grant No. 2012M521250.

PDF (PC)

1316

指针程序的分析和验证一直是个难题,本文用形状图逻辑和形状系统来解决其中的困难,并采取先用形状分析构建各程序点的形状图,再借助形状图进行其它性质验证的两阶段方式完成指针程序的验证。所实现的系统原型可自动验证使用splay tree, treap, AVL tree 和 AA tree等数据结构的程序。本文提出一种直接把形状图作为程序中指针断言的形状图逻辑。它是Hoare逻辑的一种扩展,可用于对操作易变数据结构的指针程序的分析和验证。用形状图表示指针断言的好处是,便于程序验证阶段获取所需的指针信息。其次,提出形状系统概念。它要求程序员在声明递归结构体的类型时,指明其指针域参与构建的数据结构的形状,在形状分析阶段的形状检查据此排除所构建的形状偏离程序员期望的程序。其好处是可免去程序员为程序验证提供有关指针的函数前后条件和循环不变式。此外,还提出利用形状图来消除访问路径别名,让程序验证阶段对形状以外性质的验证仍用Hoare逻辑的规则进行推理的方法。该方法使得程序验证阶段生成的验证条件仍可以用通常的定理证明器来证明。

Abstract: Analysis and verification of pointer programs are still difficult problems so far. This paper uses a shape graph logic and a shape system to solve these problems in two stages. First, shape graphs at every program point are constructed using an analysis tool. Then, they are used to support the verification of other properties (e.g., orderedness). Our prototype supports automatic verification of programs manipulating complex data structures such as splay trees, treaps, AVL trees and AA trees, etc. The proposed shape graph logic, as an extension to Hoare logic, uses shape graphs directly as assertions. It can be used in the analysis and verification of programs manipulating mutable data structures. The benefit using shape graphs as assertions is that it is convenient for acquiring the relations between pointers in the verification stage. The proposed shape system requires programmers to provide lightweight shape declarations in recursive structure type declarations. It can help rule out programs that construct shapes deviating from what programmers expect (reflected in shape declarations) in the analysis stage. As a benefit, programmers need not provide specifications (e.g., pre-/post-conditions, loop invariants) about pointers. Moreover, we present a method doing verification in the second stage using traditional Hoare logic rules directly by eliminating aliasing with the aid of shape graphs. Thus, verification conditions could be discharged by general theorem provers.

[1] Paulson L C. Isabelle: A Generic Theorem Prover. SpringerVerlag Berlin, 1994.

[2] Nanevski A, Morrisett G, Shinnar A, Govereau P, Birkedal L. Ynot: Dependent types for imperative programs. In Proc. the 13th ACM SIGPLAN Int. Conf. Functional Programming, September 2008, pp.229-240.

[3] Barnett M, M. Leino K R, Schulte W. The spec# programming system: An overview. In Proc. Int. Conf. Construction and Analysis of Safe, Secure and Interoperable Smart Devices (CASSIS), March 2004, pp.49-69.

[4] Flanagan C, Rustan K, Lillibridge M et al. Extended static checking for Java. In Proc. the ACM SIGPLAN 2002 Conf. Programming Language Design and Implementation, June 2002, pp.234-245.

[5] Berdine J, Calcagno C, O'Hearn P W. Smallfoot: Modular automatic assertion checking with separation logic. In Proc. the 4th Int. Symp. Formal Methods for Components and Objects, Nov. 2005, pp.115-137.

[6] Distefano D, Parkinson M. jStar: Towards practical verification for Java. In Proc. the 23rd ACM SIGPLAN Int. Conf. Object-Oriented Programming, Systems, Languages, and Applications, Oct. 2008, pp.213-226.

[7] Li Z P, Zhang Y, Chen Y Y, Meng J C. Automated theorem proving for theory of shape graphs and its application in program verification. Technical Report, USTCYale Joint Research Center for High-Confidence Software, http://kyhcs.ustcsz.edu.cn/SGL, Nov. 2012.

[8] Chen Y Y, Li Z P, Wang Z F, Hua B J. A pointer logic for pointer program verification. Chinese Journal of Software, 2010, 21(3): 124-137. (Chinese, English Version at http://kyhcs.ustcsz.edu.cn/?zpli/pl.pdf)

[9] Fradet P, Metayer D L. Shape types. In Proc. the ACM SIGPLAN-SIGACT Symp. Principles of Programming Languages, Jan. 1997, pp.27-39.

[10] de Moura L D, Bjørner N. Z3: An efficient SMT solver. In Proc. the 14th Int. Conf. Tools and Algorithms for the Construction and Analysis of Systems, Mar. 29-Apr. 6, 2008, pp.337-340.

[11] Lahiri S, Qadeer S. Verifying properties of well-founded linked lists. In Proc. the 33rd ACM SIGPLAN-SIGACT Symp. Principles of Programming Languages, Jan. 2006, pp.115126.

[12] Chin W N, David C, Nguyen H H, Qin S. Automated verification of shape, size and bag properties. In Proc. the 12th Int. Conf. Engineering of Complex Computer Systems, July 2007, pp.307-320.

[13] Lahiri S, Qadeer S. Back to the future: Revisiting precise program verification using SMT solvers. In Proc. the 35th ACM SIGPLAN-SIGACT Symp. Principles of Programming Languages, Jan. 2008, pp.171-182.

[14] Bouajjani A, Dragoi C, Enea C, Sighireanu M. A logic-based framework for reasoning about composite data structures. In Proc. the 20th Int. Conf. Concurrency Theory, Sept. 2009, pp.178-195.

[15] Madhusudan P, Parlato G, Qiu X K. Decidable logics combining heap structures and data. In Proc. the 38th ACM SIGPLAN-SIGACT Symp. Principles of Programming Languages, Jan. 2011, pp.611-622.

[16] Reynolds J C. Separation logic: A logic for shared mutable data structures. In Proc. the 17th IEEE Symp. Logic in Computer Science, July 2002, pp.55-74.

[17] O'Hearn P W, Yang H, Reynolds J C. Separation and information hiding. In Proc. the 31st ACM SIGPLAN-SIGACT Symp. Principles of Programming Languages, Jan. 2004, pp.268-280.

[18] Pérez J A N, Rybalchenko A. Separation logic + superposition calculus = Heap theorem prover. In Proc. ACM SIGPLAn Conf. Programming Language Design and Implementation, Jun. 2011, pp.556-566.

[19] Berdine J, Calcagno C, O'Hearn P W. A decidable fragment of separation logic. In Proc. the 24th Int. Conf. Foundations of Software Technology and Theoretical Computer Science, Dec. 2004, pp.97-109.

[20] Sagiv M, Reps T, Wilhelm R. Solving shape-analysis problems in languages with destructive updating. ACM Transactions on Programming Languages and Systems, 1998, 20(1): 1-50.

[21] Sagiv M, Reps T, Wilhelm R. Parametric shape analysis via 3valued logic. ACM Transactions on Programming Languages and Systems, 2002, 24(3): 217-298.

[22] Lee O, Yang H, Yi K. Automatic verification of pointer programs using grammar-based shape analysis. In Proc. the 19th European Conf. Programming Languages and Systems, Apr. 2005, pp.124-140.

[23] Chang B E, Rival X, Necula G C. Shape analysis with structural invariant checkers. In Proc. the 14th Int. Static Analysis Symp., Aug. 2007, pp.384-401.

[24] Chang B E, Rival X. Relational inductive shape analysis. In Proc. the 35th ACM SIGPLAN-SIGACT Symp. Principles of Programming Languages, Jan. 2008, pp.247-260.

[25] Laviron V, Chang B E, Rival X. Separating shape graphs. In Proc. the 19th European Conf. Programming Languages and Systems, Mar. 2010, pp.387-406.

[26] Lev-Ami T, Reps T, Sagiv M, Wilhelm R. Putting static analysis to work for verification: A case study. In Proc. the Int. Symp. Software Testing and Analysis, Aug. 2000, pp.26-38.

[27] Clarke E M, Grumberg O, Jha S, Lu Y, Veith H. Counterexample-guided abstraction refinement. In Proc. the 12th Int. Conf. Computer Aided Verification, July 2000, pp.154-169.

[28] Podelski A, Wies T. Counterexample-guided focus. In Proc. the 27th ACM SIGPLAN-SIGACT Symp. Principles of Programming Languages, Jan. 2010, pp.249-260.

[29] Madhusudan P, Qiu X K, Stefanescu A. Recursive proofs for inductive tree data-structures. In Proc. the 39th ACM SIGPLAN-SIGACT Symp. Principles of Programming Languages, Jan. 2012, pp.123-135.

[30] Calcagno C, Distefano D, O'Hearn P W, Yang H. Compositional shape analysis by means of bi-abduction. In Proc. the 36th ACM SIGPLAN-SIGACT Symp. Principles of Programming Languages, Jan. 2009, pp.289-300.
No related articles found!
Viewed
Full text


Abstract

Cited
  Shared   
  Discussed   
[1] 刘明业; 洪恩宇;. Some Covering Problems and Their Solutions in Automatic Logic Synthesis Systems[J]. , 1986, 1(2): 83 -92 .
[2] 陈世华;. On the Structure of (Weak) Inverses of an (Weakly) Invertible Finite Automaton[J]. , 1986, 1(3): 92 -100 .
[3] 高庆狮; 张祥; 杨树范; 陈树清;. Vector Computer 757[J]. , 1986, 1(3): 1 -14 .
[4] 陈肇雄; 高庆狮;. A Substitution Based Model for the Implementation of PROLOG——The Design and Implementation of LPROLOG[J]. , 1986, 1(4): 17 -26 .
[5] 黄河燕;. A Parallel Implementation Model of HPARLOG[J]. , 1986, 1(4): 27 -38 .
[6] 闵应骅; 韩智德;. A Built-in Test Pattern Generator[J]. , 1986, 1(4): 62 -74 .
[7] 唐同诰; 招兆铿;. Stack Method in Program Semantics[J]. , 1987, 2(1): 51 -63 .
[8] 闵应骅;. Easy Test Generation PLAs[J]. , 1987, 2(1): 72 -80 .
[9] 朱鸿;. Some Mathematical Properties of the Functional Programming Language FP[J]. , 1987, 2(3): 202 -216 .
[10] 李明慧;. CAD System of Microprogrammed Digital Systems[J]. , 1987, 2(3): 226 -235 .
版权所有 © 《计算机科学技术学报》编辑部
本系统由北京玛格泰克科技发展有限公司设计开发 技术支持：support@magtech.com.cn
总访问量：