Skip to main content
SpringerLink
Log in

Hierarchical Shape Abstraction for Analysis of Free List Memory Allocators

  • Conference paper
  • First Online:
Logic-Based Program Synthesis and Transformation (LOPSTR 2016)

Part of the book series: Lecture Notes in Computer Science ((LNTCS,volume 10184))

Abstract

We propose a hierarchical abstract domain for the analysis of free list memory allocators that tracks shape and numerical properties about both the heap and the free lists. Our domain is based on Separation Logic extended with predicates that capture the pointer arithmetics constraints for the heap list and the shape of the free list. These predicates are combined using a hierarchical composition operator to specify the overlapping of the heap list by the free list. In addition to expressiveness, this operator leads to a compositional and compact representation of abstract values and simplifies the implementation of the abstract domain. The shape constraints are combined with numerical constraints over integer arrays to track properties about the allocation policies (best-fit, first-fit, etc.). Such properties are out of the scope of the existing analyzers. We implemented this domain and we show its effectiveness on several implementations of free list allocators.

This is a preview of subscription content, log in via an institution to check access.

Access this chapter

Log in via an institution
Chapter
USD 29.95
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
eBook
USD 39.99
Price excludes VAT (USA)
  • Available as EPUB and PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
USD 54.99
Price excludes VAT (USA)
  • Compact, lightweight edition
  • Dispatched in 3 to 5 business days
  • Free shipping worldwide - see info

Tax calculation will be finalised at checkout

Purchases are for personal use only

Institutional subscriptions

References

  1. Aldridge, L.: Memory allocation in C. In: Embedded Systems Programming, pp. 35–42, August 2008

    Google Scholar 

  2. Balakrishnan, G., Reps, T.: Recency-abstraction for heap-allocated storage. In: Yi, K. (ed.) SAS 2006. LNCS, vol. 4134, pp. 221–239. Springer, Heidelberg (2006). doi:10.1007/11823230_15

    Chapter  Google Scholar 

  3. Bouajjani, A., Dragoi, C., Enea, C., Sighireanu, M.: On inter-procedural analysis of programs with lists and data. In: PLDI, pp. 578–589. ACM (2011)

    Google Scholar 

  4. Bouajjani, A., Drăgoi, C., Enea, C., Sighireanu, M.: Accurate invariant checking for programs manipulating lists and arrays with infinite data. In: Chakraborty, S., Mukund, M. (eds.) ATVA 2012. LNCS, pp. 167–182. Springer, Heidelberg (2012). doi:10.1007/978-3-642-33386-6_14

    Chapter  Google Scholar 

  5. Calcagno, C., Distefano, D., O’Hearn, P.W., Yang, H.: Beyond reachability: shape abstraction in the presence of pointer arithmetic. In: Yi, K. (ed.) SAS 2006. LNCS, vol. 4134, pp. 182–203. Springer, Heidelberg (2006). doi:10.1007/11823230_13

    Chapter  Google Scholar 

  6. Chang, B.E., Rival, X.: Modular construction of shape-numeric analyzers. In: Semantics, Abstract Interpretation, and Reasoning about Programs, EPTCS, vol. 129, pp. 161–185 (2013)

    Google Scholar 

  7. Chang, B.-Y.E., Rival, X., Necula, G.C.: Shape analysis with structural invariant checkers. In: Nielson, H.R., Filé, G. (eds.) SAS 2007. LNCS, vol. 4634, pp. 384–401. Springer, Heidelberg (2007). doi:10.1007/978-3-540-74061-2_24

    Chapter  Google Scholar 

  8. Cousot, P., Cousot, R.: Abstract interpretation: a unified lattice model for static analysis of programs by construction or approximation of fixpoints. In: POPL, pp. 238–252. ACM (1977)

    Google Scholar 

  9. Distefano, D., O’Hearn, P.W., Yang, H.: A local shape analysis based on separation logic. In: Hermanns, H., Palsberg, J. (eds.) TACAS 2006. LNCS, vol. 3920, pp. 287–302. Springer, Heidelberg (2006). doi:10.1007/11691372_19

    Chapter  Google Scholar 

  10. Dragoi, C.: Automated verification of heap-manipulating programs with infinite data. PhD thesis, University Paris Diderot (2011)

    Google Scholar 

  11. Drăgoi, C., Enea, C., Sighireanu, M.: Local shape analysis for overlaid data structures. In: Logozzo, F., Fähndrich, M. (eds.) SAS 2013. LNCS, vol. 7935, pp. 150–171. Springer, Heidelberg (2013). doi:10.1007/978-3-642-38856-9_10

    Chapter  Google Scholar 

  12. Enea, C., Sighireanu, M., Wu, Z.: On automated lemma generation for separation logic with inductive definitions. In: Finkbeiner, B., Pu, G., Zhang, L. (eds.) ATVA 2015. LNCS, vol. 9364, pp. 80–96. Springer, Cham (2015). doi:10.1007/978-3-319-24953-7_7

    Chapter  Google Scholar 

  13. Gulwani, S., Lev-Ami, T., Sagiv, S.: A combination framework for tracking partition sizes. In: POPL, pp. 239–251. ACM (2009)

    Google Scholar 

  14. Gulwani, S., McCloskey, B., Tiwari, A.: Lifting abstract interpreters to quantified logical domains. In: POPL, pp. 235–246. ACM (2008)

    Google Scholar 

  15. Halbwachs, N., Péron, M.: Discovering properties about arrays in simple programs. In: PLDI, pp. 339–348. ACM (2008)

    Google Scholar 

  16. Jeannet, B., Miné, A.: Apron: a library of numerical abstract domains for static analysis. In: Bouajjani, A., Maler, O. (eds.) CAV 2009. LNCS, vol. 5643, pp. 661–667. Springer, Heidelberg (2009). doi:10.1007/978-3-642-02658-4_52

    Chapter  Google Scholar 

  17. Kernighan, B.W., Ritchie, D.: The C Programming Language, 2nd edn. Prentice-Hall, Englewood Cliffs (1988)

    MATH  Google Scholar 

  18. Kirchner, F., Kosmatov, N., Prevosto, V., Signoles, J., Yakobowski, B.: Frama-C: a software analysis perspective. FAC 27(3), 573–609 (2015)

    MathSciNet  Google Scholar 

  19. Knuth, D.E.: The Art of Computer Programming, Volume I: Fundamental Algorithms, 2nd edn. Addison-Wesley, Reading (1973)

    Google Scholar 

  20. Lea, D.: dlmalloc (2012). ftp://gee.cs.oswego.edu/pub/misc/malloc.c

  21. Lee, O., Yang, H., Petersen, R.: Program analysis for overlaid data structures. In: Gopalakrishnan, G., Qadeer, S. (eds.) CAV 2011. LNCS, vol. 6806, pp. 592–608. Springer, Heidelberg (2011). doi:10.1007/978-3-642-22110-1_48

    Chapter  Google Scholar 

  22. Liu, J., Rival, X.: Abstraction of arrays based on non contiguous partitions. In: D’Souza, D., Lal, A., Larsen, K.G. (eds.) VMCAI 2015. LNCS, vol. 8931, pp. 282–299. Springer, Heidelberg (2015). doi:10.1007/978-3-662-46081-8_16

    Google Scholar 

  23. Albert, E., Arenas, P., Genaim, S., Puebla, G.: Field-sensitive value analysis by field-insensitive analysis. In: Cavalcanti, A., Dams, D.R. (eds.) FM 2009. LNCS, vol. 5850, pp. 370–386. Springer, Heidelberg (2009). doi:10.1007/978-3-642-05089-3_24

    Chapter  Google Scholar 

  24. O’Hearn, P., Reynolds, J., Yang, H.: Local reasoning about programs that alter data structures. In: Fribourg, L. (ed.) CSL 2001. LNCS, vol. 2142, pp. 1–19. Springer, Heidelberg (2001). doi:10.1007/3-540-44802-0_1

    Chapter  Google Scholar 

  25. Sotin, P., Rival, X.: Hierarchical shape abstraction of dynamic structures in static blocks. In: Jhala, R., Igarashi, A. (eds.) APLAS 2012. LNCS, vol. 7705, pp. 131–147. Springer, Heidelberg (2012). doi:10.1007/978-3-642-35182-2_10

    Chapter  Google Scholar 

  26. Celia extensions. http://www.irif.fr/~sighirea/celia/plus.html

  27. Wilson, P.R., Johnstone, M.S., Neely, M., Boles, D.: Dynamic storage allocation: a survey and critical review. In: Baler, H.G. (ed.) IWMM 1995. LNCS, vol. 986, pp. 1–116. Springer, Heidelberg (1995). doi:10.1007/3-540-60368-9_19

    Chapter  Google Scholar 

Download references

Author information

Authors and Affiliations

  1. IRIF, University Paris Diderot and CNRS, Paris, France

    Bin Fang & Mihaela Sighireanu

  2. Shanghai Key Laboratory of Trustworthy Computing, ECNU, Shanghai, China

    Bin Fang

Authors
  1. Bin Fang
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Mihaela Sighireanu
    View author publications

    You can also search for this author in PubMed Google Scholar

Corresponding author

Correspondence to Mihaela Sighireanu .

Editor information

Editors and Affiliations

  1. IMDEA Software Institute and Universidad Politécnica de Madrid, Madrid, Spain

    Manuel V Hermenegildo

  2. IMDEA Software Institute and CSIC, Madrid, Spain

    Pedro Lopez-Garcia

Rights and permissions

Reprints and permissions

Copyright information

© 2017 Springer International Publishing AG

About this paper

Cite this paper

Fang, B., Sighireanu, M. (2017). Hierarchical Shape Abstraction for Analysis of Free List Memory Allocators. In: Hermenegildo, M., Lopez-Garcia, P. (eds) Logic-Based Program Synthesis and Transformation. LOPSTR 2016. Lecture Notes in Computer Science(), vol 10184. Springer, Cham. https://doi.org/10.1007/978-3-319-63139-4_9

Download citation

  • DOI: https://doi.org/10.1007/978-3-319-63139-4_9

  • Published:

  • Publisher Name: Springer, Cham

  • Print ISBN: 978-3-319-63138-7

  • Online ISBN: 978-3-319-63139-4

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Search

Navigation