Advertisement

Shape Analysis with Connectors

  • Holger Siegel
  • Axel SimonEmail author
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 9058)

Abstract

We extend off-the-shelf shape analyses with the ability to infer numeric relations between directly or indirectly connected heap cells. Specifically, we introduce the concept of connectors, an instrumentation that retains relations between heap cells even if these cells are merged into summary nodes. Managing connectors is based on applying generic \(\textit{fold}\) and \(\textit{expand}\) operations on a numeric abstract domain. Connectors are thus a universal tool to enhance shape analyses with any numeric analysis. We show how connectors provide the ability to infer invariants of non-trivial heap structures such as sorted/skip lists and search trees.

Keywords

Shape Analysis Numeric State Numeric Relation Abstract Domain Numeric Domain 
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. 1.
    Bouajjani, A., Drăgoi, C., Enea, C., Rezine, A., Sighireanu, M.: Invariant synthesis for programs manipulating lists with unbounded data. In: Touili, T., Cook, B., Jackson, P. (eds.) CAV 2010. LNCS, vol. 6174, pp. 72–88. Springer, Heidelberg (2010) CrossRefGoogle Scholar
  2. 2.
    Cousot, P., Halbwachs, N.: Automatic discovery of linear constraints among variables of a program. In: Principles of Programming Languages, Tucson, Arizona, USA, pp. 84–97. ACM, January 1978Google Scholar
  3. 3.
    Ferrara, P., Fuchs, R., Juhasz, U.: TVAL+: TVLA and value analyses together. In: Eleftherakis, G., Hinchey, M., Holcombe, M. (eds.) SEFM 2012. LNCS, vol. 7504, pp. 63–77. Springer, Heidelberg (2012) CrossRefGoogle Scholar
  4. 4.
    Fu, Z.: Modularly combining numeric abstract domains with points-to analysis, and a scalable static numeric analyzer for java. In: McMillan, K.L., Rival, X. (eds.) VMCAI 2014. LNCS, vol. 8318, pp. 282–301. Springer, Heidelberg (2014) CrossRefGoogle Scholar
  5. 5.
    Gopan, D., DiMaio, F., Dor, N., Reps, T., Sagiv, M.: Numeric domains with summarized dimensions. In: Jensen, K., Podelski, A. (eds.) TACAS 2004. LNCS, vol. 2988, pp. 512–529. Springer, Heidelberg (2004) CrossRefGoogle Scholar
  6. 6.
    Gulwani, S., Lev-Ami, T., Sagiv, M.: A combination framework for tracking partition sizes. In: Principles of Programming Languages, Savannah, Georgia, USA. ACM, January 2009Google Scholar
  7. 7.
    Halbwachs, N., Péron, M.: Discovering properties about arrays in simple programs. In: Gupta, R., Amarasinghe, S.P. (eds.) Programming Language Design and Implementation, Tucson, Arizona, USA, pp. 339–348. ACM, June 2008Google Scholar
  8. 8.
    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) CrossRefGoogle Scholar
  9. 9.
    Magill, S., Berdine, J., Clarke, E., Cook, B.: Arithmetic strengthening for shape analysis. In: Nielson, H.R., Filé, G. (eds.) SAS 2007. LNCS, vol. 4634, pp. 419–436. Springer, Heidelberg (2007) CrossRefGoogle Scholar
  10. 10.
    McCloskey, B., Reps, T., Sagiv, M.: Statically inferring complex heap, array, and numeric invariants. In: Cousot, R., Martel, M. (eds.) SAS 2010. LNCS, vol. 6337, pp. 71–99. Springer, Heidelberg (2010) CrossRefGoogle Scholar
  11. 11.
    Miné, A.: The Octagon Abstract Domain. Higher-Order and Symbolic Computation 19, 31–100 (2006)CrossRefzbMATHGoogle Scholar
  12. 12.
    Nguyen, H.H., David, C., Qin, S.C., Chin, W.-N.: Automated verification of shape and size properties via separation logic. In: Cook, B., Podelski, A. (eds.) VMCAI 2007. LNCS, vol. 4349, pp. 251–266. Springer, Heidelberg (2007) CrossRefGoogle Scholar
  13. 13.
    Podelski, A., Wies, T.: Boolean heaps. In: Hankin, C., Siveroni, I. (eds.) SAS 2005. LNCS, vol. 3672, pp. 268–283. Springer, Heidelberg (2005) CrossRefGoogle Scholar
  14. 14.
    Reynolds, J.C.: Separation logic: a logic for shared mutable data structures. In: Logic in Computer Science, Copenhagen, Denmark, pp. 55–74. IEEE (2002)Google Scholar
  15. 15.
    Sagiv, M., Reps, T., Wilhelm, R.: Parametric Shape Analysis via 3-Valued Logic. Transactions on Programming Languages and Systems 24(3), 217–298 (2002)CrossRefGoogle Scholar
  16. 16.
    Siegel, H., Simon, A.: Summarized dimensions revisited. In: Mauborgne, L. (ed.) Workshop on Numeric and Symbolic Abstract Domains, ENTCS, Venice, Italy. Springer, September 2011Google Scholar
  17. 17.
    Siegel, H., Simon, A.: FESA: fold- and expand-based shape analysis. In: Jhala, R., De Bosschere, K. (eds.) Compiler Construction. LNCS, vol. 7791, pp. 82–101. Springer, Heidelberg (2013) CrossRefGoogle Scholar

Copyright information

© Springer International Publishing Switzerland 2015

Authors and Affiliations

  1. 1.Institut für Informatik IITechnische Universität MünchenGarchingGermany

Personalised recommendations