Skip to main content
SpringerLink
Log in

A Relational Shape Abstract Domain

  • Conference paper
  • First Online:
NASA Formal Methods (NFM 2017)

Part of the book series: Lecture Notes in Computer Science ((LNPSE,volume 10227))

Included in the following conference series:

Abstract

Static analyses aim at inferring semantic properties of programs. While many analyses compute an over-approximation of reachable states, some analyses compute a description of the input-output relations of programs. In the case of numeric programs, several analyses have been proposed that utilize relational numerical abstract domains to describe relations. On the other hand, designing abstractions for relations over memory states and taking shapes into account is challenging. In this paper, we propose a set of novel logical connectives to describe such relations, which are inspired by separation logic. This logic can express that certain memory areas are unchanged, freshly allocated, or freed, or that only part of the memory was modified. Using these connectives, we build an abstract domain and design a static analysis that over-approximates relations over memory states containing inductive structures. We implement this analysis and report on the analysis of a basic library of list manipulating functions.

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. Baudin, P., Filliâtre, J.-C., Marché, C., Monate, B., Moy, Y., Prevosto, V.: ACSL: ANSI C specification language (2008)

    Google Scholar 

  2. Calcagno, C., Distefano, D., O’Hearn, P.W., Yang, H.: Footprint analysis: a shape analysis that discovers preconditions. In: Nielson, H.R., Filé, G. (eds.) SAS 2007. LNCS, vol. 4634, pp. 402–418. Springer, Heidelberg (2007). doi:10.1007/978-3-540-74061-2_25

    Chapter  Google Scholar 

  3. Calcagno, C., Distefano, D., O’Hearn, P., Yang, H.: Compositional shape analysis by means of bi-abduction. In: Symposium on Principles of Programming Languages (POPL), pp. 289–300. ACM (2009)

    Google Scholar 

  4. Castelnuovo, G., Naik, M., Rinetzky, N., Sagiv, M., Yang, H.: Modularity in lattices: a case study on the correspondence between top-down and bottom-up analysis. In: Blazy, S., Jensen, T. (eds.) SAS 2015. LNCS, vol. 9291, pp. 252–274. Springer, Heidelberg (2015). doi:10.1007/978-3-662-48288-9_15

    Chapter  Google Scholar 

  5. Chang, B.-Y.E., Rival, X.: Relational inductive shape analysis. In: Symposium on Principles of Programming Languages (POPL), pp. 247–260. ACM (2008)

    Google Scholar 

  6. Chatterjee, R., Ryder, B.G., Landi, W.A.: Relevant context inference. In: Symposium on Principles of Programming Languages (POPL), pp. 133–146. ACM (1999)

    Google Scholar 

  7. Cousot, P., Halbwachs, N.: Automatic discovery of linear restraints among variables of a program. In: Symposium on Principles of Programming Languages (POPL), pp. 84–97. ACM (1978)

    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: Symposium on Principles of Programming Languages (POPL) (1977)

    Google Scholar 

  9. Cousot, P., Cousot, R.: Systematic design of program analysis frameworks. In: Symposium on Principles of Programming Languages (POPL). ACM (1979)

    Google Scholar 

  10. Cousot, P., Cousot, R.: Modular static program analysis. In: Horspool, R.N. (ed.) CC 2002. LNCS, vol. 2304, pp. 159–179. Springer, Heidelberg (2002). doi:10.1007/3-540-45937-5_13

    Chapter  Google Scholar 

  11. Cox, A., Chang, B.-Y.E., Rival, X.: Desynchronized multi-state abstractions for open programs in dynamic languages. In: Vitek, J. (ed.) ESOP 2015. LNCS, vol. 9032, pp. 483–509. Springer, Heidelberg (2015). doi:10.1007/978-3-662-46669-8_20

    Chapter  Google Scholar 

  12. Dillig, I., Dillig, T., Aiken, A., Sagiv, M.: Precise and compact modular procedure summaries for heap manipulating programs. In: Conference on Programming Language Design and Implementation (PLDI), pp. 567–577. ACM (2011)

    Google Scholar 

  13. Distefano, D., Katoen, J.-P., Rensink, A.: Who is pointing when to whom? In: Lodaya, K., Mahajan, M. (eds.) FSTTCS 2004. LNCS, vol. 3328, pp. 250–262. Springer, Heidelberg (2004). doi:10.1007/978-3-540-30538-5_21

    Chapter  Google Scholar 

  14. Distefano, D., Katoen, J.-P., Rensink, A.: Safety and liveness in concurrent pointer programs. In: Boer, F.S., Bonsangue, M.M., Graf, S., Roever, W.-P. (eds.) FMCO 2005. LNCS, vol. 4111, pp. 280–312. Springer, Heidelberg (2006). doi:10.1007/11804192_14

    Chapter  Google Scholar 

  15. 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 

  16. Gulavani, B.S., Chakraborty, S., Ramalingam, G., Nori, A.V.: Bottom-up shape analysis. In: Palsberg, J., Su, Z. (eds.) SAS 2009. LNCS, vol. 5673, pp. 188–204. Springer, Heidelberg (2009). doi:10.1007/978-3-642-03237-0_14

    Chapter  Google Scholar 

  17. Jeannet, B., Loginov, A., Reps, T., Sagiv, M.: A relational approach to interprocedural shape analysis. ACM Trans. Program. Lang. Syst. (TOPLAS) 32(2), 5 (2010)

    Article  MATH  Google Scholar 

  18. Kaki, G., Jagannathan, S.: A relational framework for higher-order shape analysis. In: International Colloquium on Function Programming, pp. 311–324. ACM (2014)

    Google Scholar 

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

    Article  MathSciNet  Google Scholar 

  20. Le, Q.L., Gherghina, C., Qin, S., Chin, W.-N.: Shape analysis via second-order bi-abduction. In: Biere, A., Bloem, R. (eds.) CAV 2014. LNCS, vol. 8559, pp. 52–68. Springer, Cham (2014). doi:10.1007/978-3-319-08867-9_4

    Google Scholar 

  21. Leavens, G.T., Baker, A.L., Ruby, C.: JML: a java modeling language. In: Formal Underpinnings of Java Workshop (at OOPSLA 1998), pp. 404–420 (1998)

    Google Scholar 

  22. Popeea, C., Chin, W.-N.: Inferring disjunctive postconditions. In: Okada, M., Satoh, I. (eds.) ASIAN 2006. LNCS, vol. 4435, pp. 331–345. Springer, Heidelberg (2007). doi:10.1007/978-3-540-77505-8_26

    Chapter  Google Scholar 

  23. Reynolds, J.: Separation logic: a logic for shared mutable data structures. In: Symposium on Logics in Computer Science (LICS), pp. 55–74. IEEE (2002)

    Google Scholar 

  24. Sagiv, M., Reps, T., Wilhelm, R.: Parametric shape analysis via 3-valued logic. ACM Trans. Program. Lang. Syst. (TOPLAS) 24(3), 217–298 (2002)

    Article  Google Scholar 

  25. Zhu, H., Petri, G., Jagannathan, S.: Automatically learning shape specifications. In: Conference on Programming Language Design and Implementation (PLDI), pp. 491–507. ACM (2016)

    Google Scholar 

Download references

Acknowledgements

We thank Arlen Cox for fruitful discussions, and Francois Berenger, Huisong Li, Jiangchao Liu and the anonymous reviewers for their comments on an earlier version of this paper. This work has received funding from the European Research Council under the EU’s seventh framework programme (FP7/2007-2013), grant agreement 278673, Project MemCAD, and from Bpifrance, grant agreement P3423-189738, FUI Project P-RC2.

Author information

Authors and Affiliations

  1. CEA, LIST, Software Reliability and Security Laboratory, P.C. 174, 91191, Gif-sur-Yvette, France

    Hugo Illous & Matthieu Lemerre

  2. Inria Paris/CNRS/École Normale Supérieure/PSL Research University, Paris, France

    Hugo Illous & Xavier Rival

Authors
  1. Hugo Illous
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Matthieu Lemerre
    View author publications

    You can also search for this author in PubMed Google Scholar

  3. Xavier Rival
    View author publications

    You can also search for this author in PubMed Google Scholar

Corresponding author

Correspondence to Hugo Illous .

Editor information

Editors and Affiliations

  1. Stanford University, Palo Alto, California, USA

    Clark Barrett

  2. NASA Ames Research Center, Moffett Field, California, USA

    Misty Davies

  3. NASA Ames Research Center, Moffett Field, California, USA

    Temesghen Kahsai

Rights and permissions

Reprints and permissions

Copyright information

© 2017 Springer International Publishing AG

About this paper

Cite this paper

Illous, H., Lemerre, M., Rival, X. (2017). A Relational Shape Abstract Domain. In: Barrett, C., Davies, M., Kahsai, T. (eds) NASA Formal Methods. NFM 2017. Lecture Notes in Computer Science(), vol 10227. Springer, Cham. https://doi.org/10.1007/978-3-319-57288-8_15

Download citation

  • DOI: https://doi.org/10.1007/978-3-319-57288-8_15

  • Published:

  • Publisher Name: Springer, Cham

  • Print ISBN: 978-3-319-57287-1

  • Online ISBN: 978-3-319-57288-8

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Search

Navigation