Skip to main content
SpringerLink
Log in

Boolean Algebra of Shape Analysis Constraints

  • Conference paper
Verification, Model Checking, and Abstract Interpretation (VMCAI 2004)

Part of the book series: Lecture Notes in Computer Science ((LNCS,volume 2937))

Abstract

The parametric shape analysis framework of Sagiv, Reps, and Wilhelm [45,46] uses three-valued structures as dataflow lattice elements to represent sets of states at different program points. The recent work of Yorsh, Reps, Sagiv, Wilhelm [48,50] introduces a family of formulas in (classical, two-valued) logic that are isomorphic to three-valued structures [46] and represent the same sets of concrete states.

In this paper we introduce a larger syntactic class of formulas that has the same expressive power as the formulas in [48]. The formulas in [48] can be viewed as a normal form of the formulas in our syntactic class; we give an algorithm for transforming our formulas to this normal form. Our formulas make it obvious that the constraints are closed under all boolean operations and therefore form a boolean algebra. Our algorithm also gives a reduction of the entailment and the equivalence problems for these constraints to the satisfiability problem.

This research was supported in part by DARPA Contract F33615-00-C-1692, NSF Grant CCR00-86154, NSF Grant CCR00-63513, and the Singapore-MIT Alliance.

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. Back, R.-J., von Wright, J.: Refinement Calculus. Springer, Heidelberg (1998)

    MATH  Google Scholar 

  2. Ball, T., Majumdar, R., Millstein, T., Rajamani, S.K.: Automatic predicate abstraction of C programs. In: Proc. ACM PLDI (2001)

    Google Scholar 

  3. Ball, T., Podelski, A., Rajamani, S.K.: Relative completeness of abstraction refinement for software model checking. In: Katoen, J.-P., Stevens, P. (eds.) TACAS 2002. LNCS, vol. 2280, p. 158. Springer, Heidelberg (2002)

    Chapter  Google Scholar 

  4. Benedikt, M., Reps, T., Sagiv, M.: A decidable logic for linked data structures. In: Proc. 8th ESOP (1999)

    Google Scholar 

  5. Berndl, M., Lhoták, O., Qian, F., Hendren, L., Umanee, N.: Points-to analysis using BDDs. In: PLDI 2003 (2003)

    Google Scholar 

  6. Blanchet, B., Cousot, P., Cousot, R., Feret, J., Mauborgne, L., Miné, A., Monniaux, D., Rival, X.: A Static Analyzer for Large Safety-Critical Software. In: ACM PLDI, June 2003, ACM, New York (2003)

    Google Scholar 

  7. Bozga, M., Iosif, R., Laknech, Y.: Storeless semantics and alias logic. In: ACM PEPM 2003, pp. 55–65. ACM Press, New York (2003)

    Chapter  Google Scholar 

  8. Bush, W.R., Pincus, J.D., Sielaff, D.J.: A static analyzer for finding dynamic programming errors. Software—Practice & Experience 30(7), 775–802 (2000)

    Article  MATH  Google Scholar 

  9. Chase, D.R., Wegman, M., Kenneth Zadeck, F.: Analysis of pointers and structures. In: Proc. ACM PLDI (1990)

    Google Scholar 

  10. Clarke, L., Richardson, D.: Symbolic evaluation methods for program analysis. In: Program Flow Analysis: Theory and Applications, ch. 9, Prentice-Hall, Inc., Englewood Cliffs (1981)

    Google Scholar 

  11. Dams, D., Namjoshi, K.S.: Shape analysis through predicate abstraction and model checking. In: Zuck, L.D., Attie, P.C., Cortesi, A., Mukhopadhyay, S. (eds.) VMCAI 2003. LNCS, vol. 2575, pp. 310–323. Springer, Heidelberg (2002)

    Chapter  Google Scholar 

  12. Deutsch, A.: Interprocedural may-alias analysis for pointers: Beyond k-limiting. In: Proceedings of the ACM SIGPLAN 1994 conference on Programming language design and implementation, pp. 230–241. ACM Pres, New York (1994)

    Chapter  Google Scholar 

  13. Engler, D., Chelf, B., Chou, A., Hallem, S.: Checking system rules using system-specific, programmer-written compiler extensions. In: Proc. 4th USENIX OSDI (2000)

    Google Scholar 

  14. Flanagan, C., Rustan, K., Leino, M., Lilibridge, M., Nelson, G., Saxe, J.B., Stata, R.: Extended Static Checking for Java. In: Proc. ACM PLDI (2002)

    Google Scholar 

  15. Fradet, P., Le Métayer, D.: Shape types. In: Proc. 24th ACM POPL (1997)

    Google Scholar 

  16. Ghiya, R., Hendren, L.: Is it a tree, a DAG, or a cyclic graph? In: Proc. 23rd ACM POPL (1996)

    Google Scholar 

  17. Graf, S., Saidi, H.: Construction of abstract state graphs with pvs. In: Grumberg, O. (ed.) CAV 1997. LNCS, vol. 1254, pp. 72–83. Springer, Heidelberg (1997)

    Google Scholar 

  18. Hoare, C.A.R., Jifeng, H.: A trace model for pointers and objects. In: Guerraoui, R. (ed.) ECOOP 1999. LNCS, vol. 1628, p. 1. Springer, Heidelberg (1999)

    Chapter  Google Scholar 

  19. Holzmann, G.J.: Static source code checking for user-defined properties. In: Proc. IDPT 2002, Pasadena, CA (June 2002)

    Google Scholar 

  20. Hummel, J., Hendren, L.J., Nicolau, A.: A general data dependence test for dynamic, pointer-based data structures. In: Proc. ACM PLDI (1994)

    Google Scholar 

  21. Ishtiaq, S., O’Hearn, P.W.: BI as an assertion language for mutable data structures. In: Proc. 28th ACM POPL (2001)

    Google Scholar 

  22. Jones, N.D., Muchnick, S.S.: Flexible approach to interprocedural data flow analysis and programs with recursive data structures. In: Proc. 9th ACM POPL (1982)

    Google Scholar 

  23. Klarlund, N., Møller, A., Schwartzbach, M.I.: MONA implementation secrets. In: Yu, S., Păun, A. (eds.) CIAA 2000. LNCS, vol. 2088, p. 182. Springer, Heidelberg (2001)

    Chapter  Google Scholar 

  24. Kleene, S.C.: Introduction to Metamathematics. D. Van Nostrand Company, Inc., Princeton, New Jersey (1952); fifth reprint (1967)

    MATH  Google Scholar 

  25. Kuncak, V., Lam, P., Rinard, M.: A language for role specifications. In: Dietz, H.G. (ed.) LCPC 2001. LNCS, vol. 2624, Springer, Heidelberg (2003)

    Chapter  Google Scholar 

  26. Kuncak, V., Lam, P., Rinard, M.: Roles are really great! Technical Report 822, Laboratory for Computer Science, Massachusetts Institute of Technology (2001)

    Google Scholar 

  27. Kuncak, V., Lam, P., Rinard, M.: Role analysis. In: Proc. 29th POPL (2002)

    Google Scholar 

  28. Kuncak, V., Rinard, M.: Typestate checking and regular graph constraints. Technical Report 863, MIT Laboratory for Computer Science (2002)

    Google Scholar 

  29. Kuncak, V., Rinard, M.: Existential heap abstraction entailment is undecidable. In: Cousot, R. (ed.) SAS 2003. LNCS, vol. 2694, Springer, Heidelberg (2003)

    Chapter  Google Scholar 

  30. Kuncak, V., Rinard, M.: On role logic. Technical Report 925, MIT CSAIL (2003)

    Google Scholar 

  31. Kuncak, V., Rinard, M.: On the boolean algebra of shape analysis constraints. Technical report, MIT CSAIL (August 2003)

    Google Scholar 

  32. Larus, J.R., Hilfinger, P.N.: Detecting conflicts between structure accesses. In: Proc. ACM PLDI, Atlanta, GA (June 1988)

    Google Scholar 

  33. Lev-Ami, T.: TVLA: A framework for kleene based logic static analyses. Master’s thesis, Tel-Aviv University, Israel (2000)

    Google Scholar 

  34. Lev-Ami, T., Reps, T., Sagiv, M., Wilhelm, R.: Putting static analysis to work for verification: A case study. In: International Symposium on Software Testing and Analysis (2000)

    Google Scholar 

  35. Logozzo, F.: Class-level modular analysis for object oriented languages. In: Cousot, R. (ed.) SAS 2003. LNCS, vol. 2694, Springer, Heidelberg (2003)

    Chapter  Google Scholar 

  36. Manevich, R., Ramalingam, G., Field, J., Goyal, D., Sagiv, M.: Compactly representing first-order structures for static analysis. In: Proc. 9th International Static Analysis Symposium, pp. 196–212 (2002)

    Google Scholar 

  37. Møller, A., Schwartzbach, M.I.: The Pointer Assertion Logic Engine. In: Proc. ACM PLDI (2001)

    Google Scholar 

  38. Nielson, F., Nielson, H.R., Sagiv, M.: Kleene’s logic with equality. Information Processing Letters 80(3), 131–137 (2001)

    Article  MATH  MathSciNet  Google Scholar 

  39. Reps, T., Sagiv, M., Loginov, A.: Finite differencing of logical formulas for static analysis. In: Degano, P. (ed.) ESOP 2003. LNCS, vol. 2618, pp. 380–398. Springer, Heidelberg (2003)

    Chapter  Google Scholar 

  40. Reps, T., Sagiv, M., Yorsh, G.: Symbolic implementation of the best transformer. Technical Report TR-1468, University of Wisconsin (January 2003)

    Google Scholar 

  41. Reps, T., Sagiv, M., Yorsh, G.: Symbolic implementation of the best transformer. In: Steffen, B., Levi, G. (eds.) VMCAI 2004. LNCS, vol. 2937, pp. 252–266. Springer, Heidelberg (2004)

    Chapter  Google Scholar 

  42. Rinetzky, N.: Interprocedural shape analysis. Master’s thesis, Technion - Israel Institute of Technology (2000)

    Google Scholar 

  43. Rinetzky, N., Sagiv, M.: Interprocedual shape analysis for recursive programs. In: Proc. 10th International Conference on Compiler Construction (2001)

    Google Scholar 

  44. Sagiv, M., Reps, T., Wilhelm, R.: Solving shape-analysis problems in languages with destructive updating. ACM TOPLAS 20(1), 1–50 (1998)

    Article  Google Scholar 

  45. Sagiv, M., Reps, T., Wilhelm, R.: Parametric shape analysis via 3-valued logic. In: Proc. 26th ACM POPL (1999)

    Google Scholar 

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

    Article  Google Scholar 

  47. Smith, F., Walker, D., Morrisett, G.: Alias types. In: Smolka, G. (ed.) ESOP 2000. LNCS, vol. 1782, p. 366. Springer, Heidelberg (2000)

    Chapter  Google Scholar 

  48. Yorsh, G.: Logical characterizations of heap abstractions. Master’s thesis, Tel- Aviv University (March 2003)

    Google Scholar 

  49. Yorsh, G., Reps, T., Sagiv, M.: Symbolically computing mostprecise abstract operations for shape analysis. Technical report, Tel-Aviv University (September 2003) (forthcoming)

    Google Scholar 

  50. Yorsh, G., Reps, T., Sagiv, M., Wilhelm, R.: Logical characterizations of heap abstractions. Technical report, University of Wisconsin, Madison (January 2003)

    Google Scholar 

Download references

Author information

Authors and Affiliations

  1. Computer Science and Artificial Intelligence Laboratory, Massachusetts Institute of Technology, Cambridge, MA, 02139, USA

    Viktor Kuncak & Martin Rinard

Authors
  1. Viktor Kuncak
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Martin Rinard
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

Editors and Affiliations

  1. Chair Programming Systems, Universität Dortmund, Otto-Hahn-Str. 14, 44227, Dortmund, Germany

    Bernhard Steffen

  2. Dipartimento di Informatica, Università di Pisa, Via Buonarroti, 2, 56100, Pisa, Italy

    Giorgio Levi

Rights and permissions

Reprints and permissions

Copyright information

© 2004 Springer-Verlag Berlin Heidelberg

About this paper

Cite this paper

Kuncak, V., Rinard, M. (2004). Boolean Algebra of Shape Analysis Constraints. In: Steffen, B., Levi, G. (eds) Verification, Model Checking, and Abstract Interpretation. VMCAI 2004. Lecture Notes in Computer Science, vol 2937. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-540-24622-0_7

Download citation

  • DOI: https://doi.org/10.1007/978-3-540-24622-0_7

  • Publisher Name: Springer, Berlin, Heidelberg

  • Print ISBN: 978-3-540-20803-7

  • Online ISBN: 978-3-540-24622-0

  • eBook Packages: Springer Book Archive

Publish with us

Policies and ethics

Search

Navigation