Advertisement

Analyzing Array Manipulating Programs by Program Transformation

  • J. Robert M. Cornish
  • Graeme Gange
  • Jorge A. Navas
  • Peter Schachte
  • Harald SøndergaardEmail author
  • Peter J. Stuckey
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 8981)

Abstract

We explore a transformational approach to the problem of verifying simple array-manipulating programs. Traditionally, verification of such programs requires intricate analysis machinery to reason with universally quantified statements about symbolic array segments, such as “every data item stored in the segment A[i] to A[j] is equal to the corresponding item stored in the segment B[i] to B[j].” We define a simple abstract machine which allows for set-valued variables and we show how to translate programs with array operations to array-free code for this machine. For the purpose of program analysis, the translated program remains faithful to the semantics of array manipulation. Based on our implementation in LLVM, we evaluate the approach with respect to its ability to extract useful invariants and the cost in terms of code size.

Keywords

Index Variable Basic Block Original Program Segment Bound Abstract Interpretation 
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.

Notes

Acknowledgements

This work was supported through ARC grant DP140102194.

Supplementary material

References

  1. 1.
    Alberti, F., Bruttomesso, R., Ghilardi, S., Ranise, S., Sharygina, N.: Lazy abstraction with interpolants for arrays. In: Bjørner, N., Voronkov, A. (eds.) LPAR-18 2012. LNCS, vol. 7180, pp. 46–61. Springer, Heidelberg (2012) CrossRefGoogle Scholar
  2. 2.
    Blanchet, B., Cousot, P., Cousot, R., Feret, J., Mauborgne, L., Miné, A., Monniaux, D., Rival, X.: Design and implementation of a special-purpose static program analyzer for safety-critical real-time embedded software. In: Mogensen, T.Æ., Schmidt, D.A., Sudborough, I. (eds.) The Essence of Computation. LNCS, vol. 2566, pp. 85–108. Springer, Heidelberg (2002)Google Scholar
  3. 3.
    Brat, G., Navas, J.A., Shi, N., Venet, A.: IKOS: a framework for static analysis based on abstract interpretation. In: Giannakopoulou, D., Salaün, G. (eds.) SEFM 2014. LNCS, vol. 8702, pp. 271–277. Springer, Heidelberg (2014) CrossRefGoogle Scholar
  4. 4.
    Cousot, P., Cousot, R.: Abstract interpretation: a unified lattice model for static analysis of programs by construction or approximation of fixpoints. In: POPL 1977, pp. 238–252. ACM Press (1977)Google Scholar
  5. 5.
    Cousot, P., Cousot, R., Logozzo, F.: A parametric segmentation functor for fully automatic and scalable array content analysis. In: POPL 2011, pp. 105–118. ACM Press (2011)Google Scholar
  6. 6.
    De Angelis, E., Fioravanti, F., Pettorossi, A., Proietti, M.: Verifying array programs by transforming verification conditions. In: McMillan, K.L., Rival, X. (eds.) VMCAI 2014. LNCS, vol. 8318, pp. 182–202. Springer, Heidelberg (2014)CrossRefGoogle Scholar
  7. 7.
    Dillig, I., Dillig, T., Aiken, A.: Fluid updates: beyond strong vs. weak updates. In: Gordon, A.D. (ed.) ESOP 2010. LNCS, vol. 6012, pp. 246–266. Springer, Heidelberg (2010) CrossRefGoogle Scholar
  8. 8.
    Ernst, M.D., Perkins, J.H., Guo, P.J., McCamant, S., Pacheco, C., Tschantz, M.S., Xiao, C.: The Daikon system for dynamic detection of likely invariants. Sci. Comput. Program. 69(1–3), 35–45 (2007)CrossRefzbMATHMathSciNetGoogle Scholar
  9. 9.
    Gopan, D., Reps, T., Sagiv, M.: A framework for numeric analysis of array operations. In: POPL 2005, pp. 338–350. ACM Press (2005)Google Scholar
  10. 10.
    Gulwani, S., McCloskey, B., Tiwari, A.: Lifting abstract interpreters to quantified logical domains. In: POPL 2008, pp. 235–246. ACM Press (2008)Google Scholar
  11. 11.
    Halbwachs, N., Péron, M.: Discovering properties about arrays in simple programs. In: PLDI 2008, pp. 339–348. ACM Press (2008)Google Scholar
  12. 12.
    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
  13. 13.
    Kovács, L., Voronkov, A.: Finding loop invariants for programs over arrays using a theorem prover. In: Chechik, M., Wirsing, M. (eds.) FASE 2009. LNCS, vol. 5503, pp. 470–485. Springer, Heidelberg (2009) CrossRefGoogle Scholar
  14. 14.
    Larraz, D., Rodríguez-Carbonell, E., Rubio, A.: SMT-based array invariant generation. In: Giacobazzi, R., Berdine, J., Mastroeni, I. (eds.) VMCAI 2013. LNCS, vol. 7737, pp. 169–188. Springer, Heidelberg (2013) CrossRefGoogle Scholar
  15. 15.
    Nguyen, T.V., Kapur, D., Weimer, W., Forrest, S.: Using dynamic analysis to discover polynomial and array invariants. In: Proceedings of the 34th International Conference on Software Engineering, pp. 760–770. IEEE (2012)Google Scholar
  16. 16.
    Péron, M.: Contributions à l’analyse statique de programmes manipulant des tableaux. Ph.D. thesis, Université de Grenoble (2010)Google Scholar
  17. 17.
    Regehr, J.: Uninitialized variables. Web blog, http://blog.regehr.org/archives/519, Accessed 18 June 2014

Copyright information

© Springer International Publishing Switzerland 2015

Authors and Affiliations

  • J. Robert M. Cornish
    • 1
  • Graeme Gange
    • 1
  • Jorge A. Navas
    • 2
  • Peter Schachte
    • 1
  • Harald Søndergaard
    • 1
    Email author
  • Peter J. Stuckey
    • 1
  1. 1.Department of Computing and Information SystemsThe University of Melbourne MelbourneAustralia
  2. 2.NASA Ames Research CenterMountain ViewUSA

Personalised recommendations