Cristiano Calcagno
Skip Abstract Section
Abstract
The accurate and efficient treatment of mutable data structures is one of the outstanding problem areas in automatic program verification and analysis. Shape analysis is a form of program analysis that attempts to infer descriptions of the data structures in a program, and to prove that these structures are not misused or corrupted. It is one of the more challenging and expensive forms of program analysis, due to the complexity of aliasing and the need to look arbitrarily deeply into the program heap. This article describes a method of boosting shape analyses by defining a compositional method, where each procedure is analyzed independently of its callers. The analysis algorithm uses 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. Our method brings the usual benefits of compositionality---increased potential to scale, ability to deal with incomplete programs, 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 analysis algorithm. We have implemented our analysis and we report case studies on smaller programs to evaluate the quality of discovered specifications, and larger code bases (e.g., sendmail, an imap server, a Linux distribution) to illustrate the level of automation and scalability that we obtain from our compositional method.
This article makes number of specific technical contributions on proof procedures and analysis algorithms, but in a sense its more important contribution is holistic: the explanation and demonstration of how a massive increase in automation is possible using abductive inference.
- Abdulla, P. A., Bouajjani, A., Cederberg, J., Haziza, F., and Rezine, A. 2008. Monotonic abstraction for programs with dynamic memory heaps. In Proceedings of the 20th International Conference on Computer Aided Verification, 20th International Conference (CAV). 341--354. Google Scholar
Digital Library
- Balaban, I., Pnueli, A., and Zuck, L. D. 2005. Shape analysis by predicate abstraction. In Proceedings of the 6th International Conference on Verification, Model Checking, and Abstract Interpretation (VMCAI). Lecture Notes in Computer Science, , vol. 3385. Springer, 164--180. Google ScholarDigital Library
- Ball, T., Bounimova, E., Cook, B., Levin, V., Lichtenberg, J., McGarvey, C., Ondrusek, B., Rajamani, S. K., and Ustuner, A. 2006. Thorough static analysis of device drivers. In Proceedings of the EuroSys Conference. 73--85. Google ScholarDigital Library
- Berdine, J., Calcagno, C., and O’Hearn, P. W. 2004. A decidable fragment of separation logic. In Proceedings of the 24th International Conference on Foundations of Software Technology and Theoretical Computer Science. Vol. 3328. 97--109. Google ScholarDigital Library
- Berdine, J., Calcagno, C., Cook, B., Distefano, D., O’Hearn, P., Wies, T., and Yang, H. 2007. Shape analysis of composite data structures. In Proceedings of the 19th International Conference on Computer Aided Verification (CAV). 178--192. Google ScholarDigital Library
- Berdine, J., Calcagno, C., and O’Hearn, P. W. 2005a. Smallfoot: Automatic modular assertion checking with separation logic. In Proceedings of the 4th International Symposium on Formal Methods for Components and Objects. Lecture Notes in Computer Science, vol. 4111. 115--137. Google ScholarDigital Library
- Berdine, J., Calcagno, C., and O’Hearn, P. W. 2005b. Symbolic execution with separation logic. In Proceedings of the 3rd Asian Symposium on Programming Languages and Systems (APLAS). 52--68. Google ScholarDigital Library
- Bierhoff, K. and Aldrich, J. 2005. Lightweight object specification with typestates. In Proceedings of the 13th ACM SIGSOFT Symposium on Foundations of Software Engineering (FSE). 217--226. Google ScholarDigital Library
- Bouajjani, A., Habermehl, P., Moro, P., and Vojnar, T. 2005. Verifying programs with dynamic 1-selector-linked structures in regular model checking. In Proceedings of the 11th Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS). 13--29. Google ScholarDigital Library
- Bouajjani, A., Habermehl, P., Rogalewicz, A., and Vojnar, T. 2006. Abstract tree regular model checking of complex dynamic data structures. In Proceedings of the 13th International Symposium on Static Analysis (SAS). Lecture Notes in Computer Science, vol. 4134. 52--70. Google ScholarDigital Library
- Calcagno, C., Distefano, D., O’Hearn, P. W., and Yang, H. 2006. Beyond reachability: Shape abstraction in the presence of pointer arithmetic. In Proceedings of the 13th International Symposium on Static Analysis (SAS). Lecture Notes in Computer Science, vol. 4134. 182--203. Google ScholarDigital Library
- Calcagno, C., Distefano, D., O’Hearn, P., and Yang, H. 2007a. Footprint analysis: A shape analysis that discovers preconditions. In Proceedings of the 14th International Symposium on Static Analysis (SAS). Lecture Notes in Computer Science, vol. 4634. 402--418. Google ScholarDigital Library
- Calcagno, C., O’Hearn, P., and Yang, H. 2007b. Local action and abstract separation logic. In Proceedings of the 22nd IEEE Symposium on Logic in Computer Science (LICS). 366--378. Google ScholarDigital Library
- Calcagno, C., Distefano, D., O’Hearn, P., and Yang, H. 2009a. Compositional shape analysis by means of bi-abduction. In Proceedings of the 36th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL). 289--300. Google ScholarDigital Library
- Calcagno, C., Distefano, D., and Vafeiadis, V. 2009b. Bi-abductive resource invariant synthesis. In Proceedings of the 7th Asian Symposium on Programming Languages and Systems (APLAS). 259--274. Google ScholarDigital Library
- Chang, B. and Rival, X. 2008. Relational inductive shape analysis. In Proceedings of the 36th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL). 247--260. Google ScholarDigital Library
- Chang, B., Rival, X., and Necula, G. 2007. Shape analysis with structural invariant checkers. In Proceedings of the 14th International Symposium on Static Analysis (SAS). Lecture Notes in Computer Science, Springer. 384--401. Google ScholarDigital Library
- Cook, S. A. 1978. Soundness and completeness of an axiomatic system for program verification. SIAM J. Comput. 7, 70--90.Google ScholarCross Ref
- Cousot, P. and Cousot, R. 1977. Abstract interpretation: A unified lattice model for static analysis of programs by construction or approximation of fixpoints. In Proceedings of the 4th ACM Symposium on Principles of Programming Languages (POPL). 238--252. Google ScholarDigital Library
- Cousot, P. and Cousot, R. 2001. Compositional separate modular static analysis of programs by abstract interpretation. In Proceedings of SSGRR.Google Scholar
- Cousot, P. and Cousot, R. 2002. Modular static program analysis. In Proceedings of the 11th International Conference on Compiler Construction (CC). Lecture Notes in Computer Science, vol. 2304. 159--178. Google ScholarDigital Library
- Cousot, P., Cousot, R., Feret, J., Mauborgne, L., Miné, A., Monniaux, D., and Rival, X. 2005. The ASTRÉE analyzer. In Proceedings of the 14th European Symposium on Programming (ESOP). Lecture Notes in Computer Science, vol. 3444. 21--30. Google ScholarDigital Library
- Creignou, N. and Zanuttini, B. 2006. A complete classification of the complexity of propositional abduction. SIAM J. Comput. 36, 1, 207--229. Google ScholarDigital Library
- DeLine, R. and Fähndrich, M. 2004. Typestates for objects. In Proceedings of the 18th European Conference on Object-Oriented Programming (ECOOP). 465--490.Google Scholar
- Distefano, D. and Filipovic, I. 2010. Memory leaks detection in java by bi-abductive inference. In Proceedings of the 13th International Conference on Fundamental Approaches to Software Engineering (FASE). Lecture Notes in Computer Science, vol. 6013. 278--292. Google ScholarDigital Library
- Distefano, D. and Parkinson, M. 2008. jStar: Towards Practical Verification for Java. In Proceedings of the 23rd Annual ACM SIGPLAN Conference on Object-Oriented Programming, Systems, Languages and Applications (OOPSLA). 213--226. Google ScholarDigital Library
- Distefano, D., O’Hearn, P., and Yang, H. 2006. A local shape analysis based on separation logic. In Proceedings of the 12th Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS). 287--302. Google ScholarDigital Library
- Dor, N., Rodeh, M., and Sagiv, M. 2003. CSSV: Towards a realistic tool for statically detecting all buffer overflows in C. In Proceedings of the ACM SIGPLAN 2003 Conference on Programming Language Design and Implementation (PLDI). 155--167. Google ScholarDigital Library
- Eiter, T. and Gottlob, G. 1995. The complexity of logic-based abduction. J. ACM 42, 1, 3--42. Google ScholarDigital Library
- Eiter, T. and Makino, K. 2002. On computing all abductive explanations. In Proceedings of the 18th National Conference on Artificial Intelligence and 14th Conference on Innovative Applications of Artificial Intelligence (AAAI/IAAI). 62--67. Google ScholarDigital Library
- Ghiya, R. and Hendren, L. 1996. Is it a tree, a DAG, or a cyclic graph? A shape analysis for heap-directed pointers in C. In Proceedings of the 23rd ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL). 1--15. Google ScholarDigital Library
- Giacobazzi, R. 1994. Abductive analysis of modular logic programs. In Proceedings of the International Logic Programming Symposium. The MIT Press, 377--392. Google ScholarDigital Library
- Gopan, D. and Reps, T. 2007. Low-level library analysis and summarization. In Proceedings of the 9th International Conference on Computer Aided Verification (CAV). 68--81. Google ScholarDigital Library
- Gotsman, A., Berdine, J., and Cook, B. 2006. Interprocedural shape analysis with separated heap abstractions. In Proceedings of the 13th International Symposium on Static Analysis (SAS). Lecture Notes in Computer Science, vol. 4134. 240--260. Google ScholarDigital Library
- Gulavani, B. S., Chakraborty, S., Ramalingam, G., and Nori, A. V. 2009. Bottom-up shape analysis. In Proceedings of the 16th International Symposium on Static Analysis (SAS). 188--204. Google ScholarDigital Library
- Gulwani, S. and Tiwari, A. 2007. Computing procedure summaries for interprocedural analysis. In Proceedings of the 16th European Symposium on Programming (ESOP). Lecture Notes in Computer Science, vol. 4421. Springer, 253--267. Google ScholarDigital Library
- Gulwani, S., McCloskey, B., and Tiwari, A. 2008. Lifting abstract interpreters to quantified logical domains. In Proceedings of the 35th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL). 235--246. Google ScholarDigital Library
- Guo, B., Vachharajani, N., and August, D. 2007. Shape analysis with inductive recursion synthesis. In Proceedings of the ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI). ACM. Google ScholarDigital Library
- Hackett, B. and Rugina, R. 2005. Region-based shape analysis with tracked locations. In Proceedings of the 32nd ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languagesc (POPL). ACM, 310--323. Google ScholarDigital Library
- Henzinger, T., Jhala, R., Majumdar, R., and Sutre, G. 2002. Lazy abstraction. In Proceedings of the 29th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL). ACM, 58--70. Google ScholarDigital Library
- Hoare, C. A. R. 1971. Procedures and parameters: An axiomatic approach. In Proceedings of the Symposium on the Semantics of Algebraic Languages. Lecture Notes in Math, vol. 188. 102--116.Google ScholarCross Ref
- Ishtiaq, S. and O’Hearn, P. W. 2001. BI as an assertion language for mutable data structures. In Proceedings of the 28th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL). ACM, 14--26. Google ScholarDigital Library
- Jhala, R. and Majumdar, R. 2009. Software model checking. ACM Comput. Surv. 41, 4. Google ScholarDigital Library
- Jung, Y. and Yi, K. 2008. Practical memory leak detector based on parameterized procedural summaries. In Proceedings of the 7th International Symposium on Memory Management. 131--140. Google ScholarDigital Library
- Kakas, A. C., Kowalski, R. A., and Toni, F. 1992. Abductive logic programming. J. Logic Comput. 2, 6, 719--770.Google ScholarCross Ref
- Kleymann, T. 1999. Hoare logic and auxiliary variables. Form. Asp. Comput. 11, 5, 541--566.Google ScholarCross Ref
- Lev-Ami, T., Immerman, N., and Sagiv, M. 2006. Abstraction for shape analysis with fast and precise transfomers. In Proceedings of the 18th International Conference on Computer Aided Verification (CAV). Google ScholarDigital Library
- Lev-Ami, T., Sagiv, M., Reps, T., and Gulwani, S. 2007. Backward analysis for inferring quantified preconditions. Tech rep. TR-2007-12-01, Tel-Aviv University.Google Scholar
- Luo, C., Craciun, F., Qin, S., He, G., and Chin, W.-N. 2010. Verifying pointer safety for programs with unknown calls. J. Symb. Comput. 45, 11, 1163--1183. Google ScholarDigital Library
- Magill, S., Berdine, J., Clarke, E., and Cook, B. 2007. Arithmetic strengthening for shape analysis. In Proceedings of the 14th International Symposium on Static Analysis (SAS). 419--436. Google ScholarDigital Library
- Manevich, R., Yahav, E., Ramalingam, G., and Sagiv, M. 2005. Predicate abstraction and canonical abstraction for singly-linked lists. In Proceedings of the 6th International Conference on Verification, Model Checking, and Abstract Interpretation (VMCA). Lecture Notes in Computer Science, vol. 3385. 181--198. Google ScholarDigital Library
- Manevich, R., Berdine, J., Cook, B., Ramalingam, G., and Sagiv, M. 2007. Shape analysis by graph decomposition. In Proceedings of the 13th Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS). Lecture Notes in Computer Science, vol. 4424. Springer, 3--18. Google ScholarDigital Library
- Marron, M., Hermenegildo, M., Kapur, D., and Stefanovic, D. 2008. Efficient context-sensitive shape analysis with graph based heap models. In Proceedings of the 17th International Conference on Compiler Construction (CC). Lecture Notes in Computer Science, vol 4959. 245--259. Google ScholarDigital Library
- Moy, Y. 2008. Sufficient preconditions for modular assertion checking. In Proceedings of the 9th International Conference on Verification, Model Checking, and Abstract Interpretation (VMCAI). 188--202. Google ScholarDigital Library
- Naumann, D. A. 2001. Calculating sharp adaptation rules. Inf. Process. Lett. 77, 2-4, 201--208. Google ScholarDigital Library
- Nguyen, H. H. and Chin, W.-N. 2008. Enhancing program verification with lemmas. In Proceedings of the 20th International Conference on Computer Aided Verification (CAV). Google ScholarDigital Library
- Nystrom, E., Kim, H., and Hwu, W. 2004. Bottom-up and top-down context-sensitive summary-based pointer analysis. In Proceedings of the 11th International Symposium on Static Analysis (SAS). 165--180.Google Scholar
- O’Hearn, P. W. 2007. Resources, concurrency and local reasoning. Theoret. Comput. Sci. 75, 1-3, 271--307. Google ScholarDigital Library
- O’Hearn, P. W., Reynolds, J. C., and Yang, H. 2001. Local reasoning about programs that alter data structures. In Proceedings of the 15th International Workshop on Computer Science Logic (CSL). 1--19. Google ScholarDigital Library
- O’Hearn, P. W., Yang, H., and Reynolds, J. C. 2009. Separation and information hiding. ACM Trans. Program. Lang. Syst. 31, 3. Google ScholarDigital Library
- Paul, G. 1993. Approaches to abductive reasoning: an overview. Artif. Intell. Rev. 7, 2, 109--152.Google ScholarCross Ref
- Peirce, C. 1958. Collected Papers of Charles Sanders Peirce. Harvard University Press.Google Scholar
- Podelski, A. and Wies, T. 2005. Boolean heaps. In Proceedings of the 12th International Symposium on Static Analysis (SAS). Lecture Notes in Computer Science, vol. 3672. Springer, 268--283. Google ScholarDigital Library
- Podelski, A., Rybalchenko, A., and Wies, T. 2008. Heap assumptions on demand. In Proceedings of the 18th International Conference on Computer Aided Verification (CAV). Google ScholarDigital Library
- Pym, D., O’Hearn, P., and Yang, H. 2004. Possible worlds and resources: the semantics of BI. Theoret. Comput. Sci. 315, 1, 257--305. Google ScholarDigital Library
- Reps, T., Horwitz, S., and Sagiv, M. 1995. Precise interprocedural dataflow analysis via graph reachability. In Proceedings of the 22nd ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL). Google ScholarDigital Library
- Reynolds, J. C. 2002. Separation logic: A logic for shared mutable data structures. In Proceedings of the 17th Annual IEEE Symposium on Logic in Computer Science (LICS). 55--74. Google ScholarDigital Library
- Rinetzky, N., Bauer, J., Reps, T., Sagiv, M., and Wilhelm, R. 2005a. A semantics for procedure local heaps and its abstractions. In Proceedings of the 32nd ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL). Google ScholarDigital Library
- Rinetzky, N., Sagiv, M., and Yahav, E. 2005b. Interprocedural shape analysis for cutpoint-free programs. In Proceedings of the 12th International Symposium on Static Analysis (SAS). Lecture Notes in Computer Science, vol. 3672. 284--302. Google ScholarDigital Library
- Sagiv, M., Reps, T., and Wilhelm, R. 1998. Solving shape-analysis problems in languages with destructive updating. ACM Trans. Prog. Lang. Syst. 20, 1, 1--50. Google ScholarDigital Library
- Sagiv, M., Reps, T., and Wilhelm, R. 2002. Parametric shape analysis via 3-valued logic. ACM Trans. Prog. Lang. Syst. 24, 3, 217--298. Google ScholarDigital Library
- Whaley, J. and Rinard, M. 2006. Compositional pointer and escape analysis for Java. In Proceedings of the 21st Annual ACM SIGPLAN Conference on Object-Oriented Programming, Systems, Languages and Applications (OOPSLA). 187--206. Google ScholarDigital Library
- Yang, H. 2001. Local reasoning for stateful programs. Ph.D. thesis, University of Illinois, Urbana-Champaign. Google ScholarDigital Library
- Yang, H., Lee, O., Berdine, J., Calcagno, C., Cook, B., Distefano, D., and O’Hearn, P. W. 2008. Scalable shape analysis for systems code. In Proceedings of the 20th International Conference on Computer Aided Verification (CAV). Google ScholarDigital Library
Index Terms
- Compositional Shape Analysis by Means of Bi-Abduction
Recommendations
Compositional shape analysis by means of bi-abduction
POPL '09: Proceedings of the 36th annual ACM SIGPLAN-SIGACT symposium on Principles of programming languagesThis 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 ...
Compositional shape analysis by means of bi-abduction
POPL '09This 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 ...
Pushdown control-flow analysis for free
POPL '16Traditional control-flow analysis (CFA) for higher-order languages introduces spurious connections between callers and callees, and different invocations of a function may pollute each other's return flows. Recently, three distinct approaches have been ...
Comments