Skip to main content
SpringerLink
Log in

Automatic Analysis of Open Objects in Dynamic Language Programs

  • Conference paper
Static Analysis (SAS 2014)

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

Included in the following conference series:

Abstract

In dynamic languages, objects are open–they support iteration over and dynamic addition/deletion of their attributes. Open objects, because they have an unbounded number of attributes, are difficult to abstract without a priori knowledge of all or nearly all of the attributes and thus pose a significant challenge for precise static analysis. To address this challenge, we present the HOO (Heap with Open Objects) abstraction that can precisely represent and infer properties about open-object-manipulating programs without any knowledge of specific attributes. It achieves this by building upon a relational abstract domain for sets that is used to reason about partitions of object attributes. An implementation of the resulting static analysis is used to verify specifications for dynamic language framework code that makes extensive use of open objects, thus demonstrating the effectiveness of this approach.

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

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. 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)

    Chapter  Google Scholar 

  2. Bouajjani, A., Drăgoi, C., Enea, C., Sighireanu, M.: Abstract domains for automated reasoning about list-manipulating programs with infinite data. In: Kuncak, V., Rybalchenko, A. (eds.) VMCAI 2012. LNCS, vol. 7148, pp. 1–22. Springer, Heidelberg (2012)

    Chapter  Google Scholar 

  3. Bradley, A.R., Manna, Z., Sipma, H.B.: What’s decidable about arrays? In: Emerson, E.A., Namjoshi, K.S. (eds.) VMCAI 2006. LNCS, vol. 3855, pp. 427–442. Springer, Heidelberg (2006)

    Chapter  Google Scholar 

  4. Chang, B.-Y.E., Rival, X.: Relational inductive shape analysis. In: POPL, pp. 247–260 (2008)

    Google Scholar 

  5. Chugh, R., Herman, D., Jhala, R.: Dependent types for JavaScript. In: OOPSLA, pp. 587–606 (2012)

    Google Scholar 

  6. Chugh, R., Rondon, P.M., Jhala, R.: Nested refinements: A logic for duck typing. In: POPL, pp. 231–244 (2012)

    Google Scholar 

  7. 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 (1977)

    Google Scholar 

  8. Cousot, P., Cousot, R.: Systematic design of program analysis frameworks. In: POPL, pp. 269–282 (1979)

    Google Scholar 

  9. Cousot, P., Cousot, R., Logozzo, F.: A parametric segmentation functor for fully automatic and scalable array content analysis. In: POPL, pp. 105–118 (2011)

    Google Scholar 

  10. Cox, A., Chang, B.-Y.E., Sankaranarayanan, S.: QUIC graphs: Relational invariant generation for containers. In: Castagna, G. (ed.) ECOOP 2013. LNCS, vol. 7920, pp. 401–425. Springer, Heidelberg (2013)

    Chapter  Google Scholar 

  11. Cox, A., Chang, B.-Y.E., Rival, X.: Automatic analysis of open objects in dynamic language programs (extended). Technical report, University of Colorado Boulder (2014)

    Google Scholar 

  12. de Moura, L.M., Bjørner, N.: Generalized, efficient array decision procedures. In: FMCAD, pp. 45–52 (2009)

    Google Scholar 

  13. 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)

    Chapter  Google Scholar 

  14. Dillig, I., Dillig, T., Aiken, A.: Precise reasoning for programs using containers. In: POPL, pp. 187–200 (2011)

    Google Scholar 

  15. Gardner, P., Maffeis, S., Smith, G.D.: Towards a program logic for JavaScript. In: POPL, pp. 31–44 (2012)

    Google Scholar 

  16. Gopan, D., Reps, T.W., Sagiv, S.: A framework for numeric analysis of array operations. In: POPL, pp. 338–350 (2005)

    Google Scholar 

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

    Google Scholar 

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

    Google Scholar 

  19. Hardekopf, B., Wiedermann, B., Churchill, B., Kashyap, V.: Widening for control-flow. In: McMillan, K.L., Rival, X. (eds.) VMCAI 2014. LNCS, vol. 8318, pp. 472–491. Springer, Heidelberg (2014)

    Chapter  Google Scholar 

  20. Hoare, C.A.R.: An axiomatic basis for computer programming. Commun. ACM 12(10), 576–580 (1969)

    Article  MATH  Google Scholar 

  21. Jensen, S.H., Møller, A., Thiemann, P.: Type analysis for JavaScript. In: Palsberg, J., Su, Z. (eds.) SAS 2009. LNCS, vol. 5673, pp. 238–255. Springer, Heidelberg (2009)

    Chapter  Google Scholar 

  22. Jensen, S.H., Møller, A., Thiemann, P.: Interprocedural analysis with lazy propagation. In: Cousot, R., Martel, M. (eds.) SAS 2010. LNCS, vol. 6337, pp. 320–339. Springer, Heidelberg (2010)

    Chapter  Google Scholar 

  23. Jhala, R., McMillan, K.L.: Array abstractions from proofs. In: Damm, W., Hermanns, H. (eds.) CAV 2007. LNCS, vol. 4590, pp. 193–206. Springer, Heidelberg (2007)

    Chapter  Google Scholar 

  24. Kashyap, V., Sarracino, J., Wagner, J., Wiedermann, B., Hardekopf, B.: Type refinement for static analysis of JavaScript. In: DLS, pp. 17–26 (2013)

    Google Scholar 

  25. 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)

    Chapter  Google Scholar 

  26. Kuncak, V.: Modular Data Structure Verification. PhD thesis, EECS Department, Massachusetts Institute of Technology (February 2007)

    Google Scholar 

  27. Parkinson, M.J.: Local reasoning for Java. PhD thesis, University of Cambridge (2005)

    Google Scholar 

  28. Pham, T.-H., Trinh, M.-T., Truong, A.-H., Chin, W.-N.: Fixbag: A fixpoint calculator for quantified bag constraints. In: Gopalakrishnan, G., Qadeer, S. (eds.) CAV 2011. LNCS, vol. 6806, pp. 656–662. Springer, Heidelberg (2011)

    Chapter  Google Scholar 

  29. Reynolds, J.C.: Separation logic: A logic for shared mutable data structures. In: LICS, pp. 55–74 (2002)

    Google Scholar 

  30. Richards, G., Lebresne, S., Burg, B., Vitek, J.: An analysis of the dynamic behavior of JavaScript programs. In: PLDI, pp. 1–12 (2010)

    Google Scholar 

  31. Sridharan, M., Dolby, J., Chandra, S., Schäfer, M., Tip, F.: Correlation tracking for points-to analysis of JavaScript. In: Noble, J. (ed.) ECOOP 2012. LNCS, vol. 7313, pp. 435–458. Springer, Heidelberg (2012)

    Chapter  Google Scholar 

Download references

Author information

Authors and Affiliations

  1. University of Colorado Boulder, Boulder, Colorado, USA

    Arlen Cox & Bor-Yuh Evan Chang

  2. INRIA, CNRS, ENS Paris, Paris, France

    Xavier Rival

Authors
  1. Arlen Cox
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Bor-Yuh Evan Chang
    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

Editor information

Editors and Affiliations

  1. Institut für Informatik, Westfälische Wilhelms-Universität Münster, FB 10, Einsteinstraße 62, 48149, Münster, Germany

    Markus Müller-Olm

  2. Institut für Informatik, Technische Universität München, 12, Boltzmannstr. 3, 85748, Garching, Germany

    Helmut Seidl

Rights and permissions

Reprints and permissions

Copyright information

© 2014 Springer International Publishing Switzerland

About this paper

Cite this paper

Cox, A., Chang, BY.E., Rival, X. (2014). Automatic Analysis of Open Objects in Dynamic Language Programs. In: Müller-Olm, M., Seidl, H. (eds) Static Analysis. SAS 2014. Lecture Notes in Computer Science, vol 8723. Springer, Cham. https://doi.org/10.1007/978-3-319-10936-7_9

Download citation

  • DOI: https://doi.org/10.1007/978-3-319-10936-7_9

  • Publisher Name: Springer, Cham

  • Print ISBN: 978-3-319-10935-0

  • Online ISBN: 978-3-319-10936-7

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Search

Navigation