Compositional shape analysis by means of bi-abduction

ABSTRACT

This paper describes a compositional shape analysis, where each procedure is analyzed independently of its callers. The analysis uses an abstract domain based on a restricted fragment of separation logic, and assigns a collection of Hoare triples to each procedure; the triples provide an over-approximation of data structure usage. Compositionality brings its usual benefits -- increased potential to scale, ability to deal with unknown calling contexts, graceful way to deal with imprecision -- to shape analysis, for the first time.

The analysis rests on a generalized form of abduction (inference of explanatory hypotheses) which we call bi-abduction. Bi-abduction displays abduction as a kind of inverse to the frame problem: it jointly infers anti-frames (missing portions of state) and frames (portions of state not touched by an operation), and is the basis of a new interprocedural analysis algorithm. We have implemented our analysis algorithm and we report case studies on smaller programs to evaluate the quality of discovered specifications, and larger programs (e.g., an entire Linux distribution) to test scalability and graceful imprecision.

REFERENCES

• 1: Parosh Aziz Abdulla , Ahmed Bouajjani , Jonathan Cederberg , Frédéric Haziza , Ahmed Rezine, Monotonic Abstraction for Programs with Dynamic Memory Heaps, Proceedings of the 20th international conference on Computer Aided Verification, July 07-14, 2008, Princeton, NJ, USA [doi>10.1007/978-3-540-70545-1_33]
• 2: Andreas Podelski , Andrey Rybalchenko , Thomas Wies, Heap Assumptions on Demand, Proceedings of the 20th international conference on Computer Aided Verification, July 07-14, 2008, Princeton, NJ, USA [doi>10.1007/978-3-540-70545-1_31]
• 3: I. Balaban, A. Pnueli, and L. D. Zuck. Shape analysis by predicate abstraction. In VMCAI'05, pp. 164--180.
• 4: J. Berdine, C. Calcagno, B. Cook, D. Distefano, P. O'Hearn, T. Wies, and H. Yang. Shape analysis of composite data structures. In CAV'07.
• 5: J. Berdine, C. Calcagno, and P. O'Hearn. Symbolic execution with separation logic. In APLAS'05, pp. 52--68.
• 6: A. Bouajjani, P. Habermehl, A. Rogalewicz, and T. Vojnar. Abstract tree regular model checking of complex dynamic data structures. In SAS'06, pp. 52--70.
• 7: C. Calcagno, D. Distefano, P. O'Hearn, and H. Yang. Footprint analysis: A shape analysis that discovers preconditions. In SAS'07.
• 8: Bor-Yuh Evan Chang , Xavier Rival, Relational inductive shape analysis, Proceedings of the 35th annual ACM SIGPLAN-SIGACT symposium on Principles of programming languages, January 07-12, 2008, San Francisco, California, USA
• 9: B. Chang, X. Rival, and G. Necula. Shape analysis with structural invariant checkers. In SAS'07, pp. 384--401.
• 10: P. Cousot and R. Cousot. Compositional separate modular static analysis of programs by abstract interpretation. In SSGRR'01.% In Proceedings of SSGRR, Compact disk, L'Aquila, Italy, 2001.
• 11: D. Distefano, P. O'Hearn, and H. Yang. A local shape analysis based on separation logic. In TACAS'06, pp. 287--302.
• 12: Dino Distefano , Matthew J. Parkinson J, jStar: towards practical verification for java, Proceedings of the 23rd ACM SIGPLAN conference on Object-oriented programming systems languages and applications, October 19-23, 2008, Nashville, TN, USA
• 13: Nurit Dor , Michael Rodeh , Mooly Sagiv, CSSV: towards a realistic tool for statically detecting all buffer overflows in C, Proceedings of the ACM SIGPLAN 2003 conference on Programming language design and implementation, June 09-11, 2003, San Diego, California, USA
• 14: Rakesh Ghiya , Laurie J. Hendren, Is it a tree, a DAG, or a cyclic graph? A shape analysis for heap-directed pointers in C, Proceedings of the 23rd ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.1-15, January 21-24, 1996, St. Petersburg Beach, Florida, United States [doi>10.1145/237721.237724]
• 15: Roberto Giacobazzi, Abductive analysis of modular logic programs, Proceedings of the 1994 International Symposium on Logic programming, p.377-391, November 1994, Symposia, Melbourne
• 16: D. Gopan and T. Reps. Low-level library analysis and summarization. In CAV'07, pp. 68--81.
• 17: A. Gotsman, J. Berdine, and B. Cook. Interprocedural shape analysis with separated heap abstractions. In SAS'06, pp. 240--260.
• 18: Alexey Gotsman , Josh Berdine , Byron Cook , Mooly Sagiv, Thread-modular shape analysis, Proceedings of the 2007 ACM SIGPLAN conference on Programming language design and implementation, June 10-13, 2007, San Diego, California, USA
• 19: Sumit Gulwani , Bill McCloskey , Ashish Tiwari, Lifting abstract interpreters to quantified logical domains, Proceedings of the 35th annual ACM SIGPLAN-SIGACT symposium on Principles of programming languages, January 07-12, 2008, San Francisco, California, USA
• 20: S. Gulwani and A. Tiwari. Computing procedure summaries for interprocedural analysis. In ESOP'07, pp. 253--267.
• 21: Bolei Guo , Neil Vachharajani , David I. August, Shape analysis with inductive recursion synthesis, Proceedings of the 2007 ACM SIGPLAN conference on Programming language design and implementation, June 10-13, 2007, San Diego, California, USA
• 22: Brian Hackett , Radu Rugina, Region-based shape analysis with tracked locations, Proceedings of the 32nd ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.310-323, January 12-14, 2005, Long Beach, California, USA
• 23: Hongseok Yang , Oukseh Lee , Josh Berdine , Cristiano Calcagno , Byron Cook , Dino Distefano , Peter O'Hearn, Scalable Shape Analysis for Systems Code, Proceedings of the 20th international conference on Computer Aided Verification, July 07-14, 2008, Princeton, NJ, USA [doi>10.1007/978-3-540-70545-1_36]
• 24: A. C. Kakas, R. A. Kowalski, and F. Toni. Abductive logic programming. J. of Logic and Computation, 2(6):719--770, 1992.
• 25: Viktor Kuncak , Patrick Lam , Martin Rinard, Role analysis, Proceedings of the 29th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.17-32, January 16-18, 2002, Portland, Oregon
• 26: T. Lev--Ami, N. Immerman, and M. Sagiv. Abstraction for shape analysis with fast and precise transfomers. In CAV'06, pp. 547--561.
• 27: T. Lev--Ami, M. Sagiv, T. Reps, and S. Gulwani:. Backward analysis for inferring quantified preconditions. Tel Aviv University Tech Report TR-2007-12-01, 2007.
• 28: S. Magill, J. Berdine, E. Clarke, and B. Cook. Arithmetic Strengthening for Shape Analysis. In SAS'07, pp. 419--436.
• 29: R. Manevich, J. Berdine, B. Cook, G. Ramalingam, and M. Sagiv. Shape analysis by graph decomposition. In TACAS'07, pp. 3--18.
• 30: M. Marron, M. Hermenegildo, D. Kapur, and D. Stefanovic. Efficient context-sensitive shape analysis with graph based heap models. In CC'08, pp. 245--259.
• 31: Y. Moy. Sufficient preconditions for modular assertion checking. In VMCAI'08, pp. 188--202.
• 32: H. Nguyen, C. David, S. Qin, and W.-N. Chin. Automated verification of shape and size propertiesvia separation logic. In VMCAI'07.
• 33: E. Nystrom, H. Kim, and W. Hwu. Bottom-up and top-down context-sensitive summary-based pointer analysis. SAS'04, pp. 165--180.
• 34: Peter W. O'Hearn , John C. Reynolds , Hongseok Yang, Local Reasoning about Programs that Alter Data Structures, Proceedings of the 15th International Workshop on Computer Science Logic, p.1-19, September 10-13, 2001
• 35: Peter W. O'Hearn , Hongseok Yang , John C. Reynolds, Separation and information hiding, Proceedings of the 31st ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.268-280, January 14-16, 2004, Venice, Italy
• 36: C. Peirce. Collected papers of Charles Sanders Peirce. Harvard University Press., 1958.
• 37: A. Podelski and T. Wies. Boolean heaps. In SAS'05, pp. 268--283.
• 38: Andreas Podelski , Andrey Rybalchenko , Thomas Wies, Heap Assumptions on Demand, Proceedings of the 20th international conference on Computer Aided Verification, July 07-14, 2008, Princeton, NJ, USA [doi>10.1007/978-3-540-70545-1_31]
• 39: Thomas Reps , Susan Horwitz , Mooly Sagiv, Precise interprocedural dataflow analysis via graph reachability, Proceedings of the 22nd ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.49-61, January 23-25, 1995, San Francisco, California, United States [doi>10.1145/199448.199462]
• 40: John C. Reynolds, Separation Logic: A Logic for Shared Mutable Data Structures, Proceedings of the 17th Annual IEEE Symposium on Logic in Computer Science, p.55-74, July 22-25, 2002
• 41: Noam Rinetzky , Jörg Bauer , Thomas Reps , Mooly Sagiv , Reinhard Wilhelm, A semantics for procedure local heaps and its abstractions, Proceedings of the 32nd ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.296-309, January 12-14, 2005, Long Beach, California, USA
• 42: N. Rinetzky, M. Sagiv, and E. Yahav. Interprocedural shape analysis for cutpoint-free programs. In SAS'05, pp. 284--302.
• 43: Mooly Sagiv , Thomas Reps , Reinhard Wilhelm, Solving shape-analysis problems in languages with destructive updating, ACM Transactions on Programming Languages and Systems (TOPLAS), v.20 n.1, p.1-50, Jan. 1998 [doi>10.1145/271510.271517]
• 44: Steven S. Muchnick , Neil D. Jones, Program Flow Analysis: Theory and Application, Prentice Hall Professional Technical Reference, 1981
• 45: John Whaley , Martin Rinard, Compositional pointer and escape analysis for Java programs, Proceedings of the 14th ACM SIGPLAN conference on Object-oriented programming, systems, languages, and applications, p.187-206, November 01-05, 1999, Denver, Colorado, United States

INDEX TERMS

Primary Classification:
  D. Software
  D.2 SOFTWARE ENGINEERING
      D.2.4 Software/Program Verification

Additional Classification:
  D. Software
  D.3 PROGRAMMING LANGUAGES
      D.3.4 Processors

General Terms:
Languages, Reliability, Theory, Verification

Keywords:
abduction, program analysis, proof theory