Logical characterizations of heap abstractions

ABSTRACT

Shape analysis concerns the problem of determining “shape invariants” for programs that perform destructive updating on dynamically allocated storage. In recent work, we have shown how shape analysis can be performed using an abstract interpretation based on three-valued first-order logic. In that work, concrete stores are finite two-valued logical structures, and the sets of stores that can possibly arise during execution are represented (conservatively) using a certain family of finite three-valued logical structures. In this article, we show how three-valued structures that arise in shape analysis can be characterized using formulas in first-order logic with transitive closure. We also define a nonstandard (“supervaluational”) semantics for three-valued first-order logic that is more precise than a conventional three-valued semantics, and demonstrate that the supervaluational semantics can be implemented using existing theorem provers.

REFERENCES

• 1: Lars Ole Andersen, Binding-time analysis and the taming of C pointers, Proceedings of the 1993 ACM SIGPLAN symposium on Partial evaluation and semantics-based program manipulation, p.47-58, June 14-16, 1993, Copenhagen, Denmark [doi>10.1145/154630.154636]
• 2: Michael Benedikt , Thomas W. Reps , Shmuel Sagiv, A Decidable Logic for Describing Linked Data Structures, Proceedings of the 8th European Symposium on Programming Languages and Systems, p.2-19, March 22-28, 1999
• 3: Blamey, S. 2002. Partial logic. In Handbook of Philosophical Logic, 2nd. ed., vol. 5, D. Gabbay and F. Guenthner, Eds. Kluwer Academic. 261--353.
• 4: Glenn Bruns , Patrice Godefroid, Generalized Model Checking: Reasoning about Partial State Spaces, Proceedings of the 11th International Conference on Concurrency Theory, p.168-182, August 22-25, 2000
• 5: David R. Chase , Mark Wegman , F. Kenneth Zadeck, Analysis of pointers and structures, Proceedings of the ACM SIGPLAN 1990 conference on Programming language design and implementation, p.296-310, June 1990, White Plains, New York, United States
• 6: Edmund M. Clarke , Orna Grumberg , Somesh Jha , Yuan Lu , Helmut Veith, Counterexample-Guided Abstraction Refinement, Proceedings of the 12th International Conference on Computer Aided Verification, p.154-169, July 15-19, 2000
• 7: Edmund M. Clarke , Orna Grumberg , David E. Long, Model checking and abstraction, ACM Transactions on Programming Languages and Systems (TOPLAS), v.16 n.5, p.1512-1542, Sept. 1994 [doi>10.1145/186025.186051]
• 8: Courcelle, B. 1996. On the expression of graph properties in some fragments of monadic second-order logic. In Descriptive Complexity and Finite Models: Proceedings of a DIAMCS Workshop, N. Immerman and P. Kolaitis, Eds. American Mathematical Society. 33--57.
• 9: Patrick Cousot , Radhia Cousot, Abstract interpretation: a unified lattice model for static analysis of programs by construction or approximation of fixpoints, Proceedings of the 4th ACM SIGACT-SIGPLAN symposium on Principles of programming languages, p.238-252, January 17-19, 1977, Los Angeles, California [doi>10.1145/512950.512973]
• 10: Dams, D. 1996. Abstract interpretation and partial refinement for model checking. Ph.D. thesis, Technical University of Eindhoven, Eindhoven, The Netherlands.
• 11: Manuvir Das, Unification-based pointer analysis with directional assignments, Proceedings of the ACM SIGPLAN 2000 conference on Programming language design and implementation, p.35-46, June 18-21, 2000, Vancouver, British Columbia, Canada
• 12: Erez, G. 2004. Generating concrete counter examples for arbitrary abstract domains. M.S. thesis, Tel-Aviv University, Tel-Aviv, Israel. In preparation.
• 13: Erez, G., Sagiv, M., and Yahav, E. 2003. Generating concrete counter examples for arbitrary abstract domains. Unpublished manuscript.
• 14: Fagin, R. 1975. Monadic generalized spectra. Z. Math. Logik 21, 89--96.
• 15: Manuel Fähndrich , Jeffrey S. Foster , Zhendong Su , Alexander Aiken, Partial online cycle elimination in inclusion constraint graphs, Proceedings of the ACM SIGPLAN 1998 conference on Programming language design and implementation, p.85-96, June 17-19, 1998, Montreal, Quebec, Canada
• 16: Pascal Fradet , Daniel Le Métayer, Shape types, Proceedings of the 24th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.27-39, January 15-17, 1997, Paris, France [doi>10.1145/263699.263706]
• 17: Patrice Godefroid , Radha Jagadeesan, On the Expressiveness of 3-Valued Models, Proceedings of the 4th International Conference on Verification, Model Checking, and Abstract Interpretation, p.206-222, January 09-11, 2002
• 18: Nevin Heintze , Olivier Tardieu, Ultra-fast aliasing analysis using CLA: a million lines of C code in a second, Proceedings of the ACM SIGPLAN 2001 conference on Programming language design and implementation, p.254-263, June 2001, Snowbird, Utah, United States
• 19: Hell, P. and Nesetril, J. 2004. Graphs and Homomorphisms. Oxford University Press.
• 20: Laurie Jane Hendren, Parallelizing programs with recursive data structures, Cornell University, Ithaca, NY, 1990
• 21: Laurie J. Hendren , Joseph Hummell , Alexandru Nicolau, Abstractions for recursive pointer data structures: improving the analysis and transformation of imperative programs, Proceedings of the ACM SIGPLAN 1992 conference on Programming language design and implementation, p.249-260, June 15-19, 1992, San Francisco, California, United States
• 22: L. J. Hendren , A. Nicolau, Parallelizing Programs with Recursive Data Structures, IEEE Transactions on Parallel and Distributed Systems, v.1 n.1, p.35-47, January 1990 [doi>10.1109/71.80123]
• 23: Jesper G. Henriksen , Jakob L. Jensen , Michael E. Jørgensen , Nils Klarlund , Robert Paige , Theis Rauhe , Anders Sandholm, Mona: Monadic Second-Order Logic in Practice, Proceedings of the First International Workshop on Tools and Algorithms for Construction and Analysis of Systems, p.89-110, May 19-20, 1995
• 24: Michael Huth , Radha Jagadeesan , David A. Schmidt, Modal Transition Systems: A Foundation for Three-Valued Program Analysis, Proceedings of the 10th European Symposium on Programming Languages and Systems, p.155-169, April 02-06, 2001
• 25: Immerman, N. 1999. Descriptive Complexity. Springer Verlag.
• 26: Immerman, N., Rabinovich, A., Reps, T., Sagiv, M., and Yorsh, G. 2004a. The boundary between decidability and undecidability for transitive-closure logics. In Computer Science Logic. Lecture Notes in Computer Science, vol. 3210. Springer Verlag.
• 27: Immerman, N., Rabinovich, A., Reps, T., Sagiv, M., and Yorsh, G. 2004b. Verification via structure simulation. In Computer Aided Verification. Lecture Notes in Computer Science, vol. 3114. Springer Verlag.
• 28: Jones, N. and Muchnick, S. 1981. Flow analysis and optimization of Lisp-like structures. In Program Flow Analysis: Theory and Applications, S. Muchnick and N. Jones, Eds. Prentice-Hall, Englewood Cliffs, NJ, 102--131.
• 29: Neil D. Jones , Steven S. Muchnick, A flexible approach to interprocedural data flow analysis and programs with recursive data structures, Proceedings of the 9th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.66-74, January 25-27, 1982, Albuquerque, Mexico [doi>10.1145/582153.582161]
• 30: Nils Klarlund , Michael I. Schwartzbach, Graph types, Proceedings of the 20th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.196-205, March 1993, Charleston, South Carolina, United States [doi>10.1145/158511.158628]
• 31: Viktor Kuncak , Patrick Lam , Martin Rinard, Role analysis, Proceedings of the 29th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.17-32, January 16-18, 2002, Portland, Oregon
• 32: Kuncak, V. and Rinard, M. 2003a. Boolean algebra of shape analysis constraints. In Proceedings of the Verification Model Checking and Abstract Interpretation. Lecture Notes in Computer Science, vol. 2937. Springer Verlag. 59--72.
• 33: Kuncak, V. and Rinard, M. 2003b. On Boolean algebra of shape analysis constraints. Tech. Rep., MIT, CSAIL. http://www.mit.edu/~vkuncak/papers/index.html.
• 34: Lam, P., Kuncak, V., and Rinard, M. 2005. Hob: A tool for verifying data structure consistency. In Conference on Compiler Construction (Tool Demo).
• 35: Lev-Ami, T. 2000. TVLA: A framework for Kleene based static analysis. M.S. thesis, Tel-Aviv University, Tel-Aviv, Israel.
• 36: Lev-Ami, T., Immerman, N., Reps, T., Sagiv, M., Srivastava, S., and Yorsh, G. 2005. Simulating reachability using first-order logic with applications to verifciation of linked data structures. Submitted for publication.
• 37: Tal Lev-Ami , Thomas Reps , Mooly Sagiv , Reinhard Wilhelm, Putting static analysis to work for verification: A case study, Proceedings of the 2000 ACM SIGSOFT international symposium on Software testing and analysis, p.26-38, August 21-24, 2000, Portland, Oregon, United States
• 38: Tal Lev-Ami , Shmuel Sagiv, TVLA: A System for Implementing Static Analyses, Proceedings of the 7th International Symposium on Static Analysis, p.280-301, June 29-July 01, 2000
• 39: McCune, W. 2001. Mace 2.0 reference manual and guide. http://www-unix.mcs.anl.gov/AR/mace/.
• 40: Kenneth L. McMillan, Verification of Infinite State Systems by Compositional Model Checking, Proceedings of the 10th IFIP WG 10.5 Advanced Research Working Conference on Correct Hardware Design and Verification Methods, p.219-234, September 27-29, 1999
• 41: Meyer, A. R. 1975. Weak monadic second-order theory of successor is not elementary recursive. In Logic Colloquium, Proceedings of the Symposium on Logic. 132--154.
• 42: Anders Møller , Michael I. Schwartzbach, The pointer assertion logic engine, Proceedings of the ACM SIGPLAN 2001 conference on Programming language design and implementation, p.221-231, June 2001, Snowbird, Utah, United States
• 43: Mortimer, M. 1975. On languages with two variables. Zeitschrift fur Math. Logik uematischend Grundlagen der Math 21, 135--140.
• 44: Flemming Nielson , Hanne R. Nielson , Chris Hankin, Principles of Program Analysis, Springer-Verlag New York, Inc., Secaucus, NJ, 1999
• 45: Flemming Nielson , Hanne Riis Nielson , Shmuel Sagiv, A Kleene Analysis of Mobile Ambients, Proceedings of the 9th European Symposium on Programming Languages and Systems, p.305-319, April 02, 2000
• 46: Rabin, M. 1969. Decidability of second-order theories and automata on infinite trees. Trans. Amer. Math. Soc. 141, 1--35.
• 47: G. Ramalingam , Alex Warshavsky , John Field , Deepak Goyal , Mooly Sagiv, Deriving specialized program analyses for certifying component-client conformance, Proceedings of the ACM SIGPLAN 2002 Conference on Programming language design and implementation, June 17-19, 2002, Berlin, Germany
• 48: Reps, T., Sagiv, M., and Yorsh, G. 2004. Symbolic implementation of the best transformer. In Verification, Model Checking, and Abstract Interpretation. Lecture Notes in Computer Science, vol. 2937. Springer Verlag. 252--266.
• 49: Mooly Sagiv , Thomas Reps , Reinhard Wilhelm, Solving shape-analysis problems in languages with destructive updating, ACM Transactions on Programming Languages and Systems (TOPLAS), v.20 n.1, p.1-50, Jan. 1998 [doi>10.1145/271510.271517]
• 50: Mooly Sagiv , Thomas Reps , Reinhard Wilhelm, Parametric shape analysis via 3-valued logic, Proceedings of the 26th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.105-118, January 20-22, 1999, San Antonio, Texas, United States [doi>10.1145/292540.292552]
• 51: Mooly Sagiv , Thomas Reps , Reinhard Wilhelm, Parametric shape analysis via 3-valued logic, ACM Transactions on Programming Languages and Systems (TOPLAS), v.24 n.3, p.217-298, May 2002 [doi>10.1145/514188.514190]
• 52: Shaham, R., Yahav, E., Kolodner, E., and Sagiv, M. 2003. Establishing local temporal heap safety properties with applications to compile-time memory management. In Proceedings of the Static Analysis Symposium (SAS). Lecture Notes in Computer Science, vol. 2694. Springer Verlag, 483--503.
• 53: Marc Shapiro , Susan Horwitz, Fast and accurate flow-insensitive points-to analysis, Proceedings of the 24th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.1-14, January 15-17, 1997, Paris, France [doi>10.1145/263699.263703]
• 54: Bjarne Steensgaard, Points-to analysis in almost linear time, Proceedings of the 23rd ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.32-41, January 21-24, 1996, St. Petersburg Beach, Florida, United States [doi>10.1145/237721.237727]
• 55: Zhendong Su , Manuel Fähndrich , Alexander Aiken, Projection merging: reducing redundancies in inclusion constraint graphs, Proceedings of the 27th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.81-95, January 19-21, 2000, Boston, MA, USA [doi>10.1145/325694.325706]
• 56: van Fraassen, B. 1966. Singular terms, truth-value gaps, and free logic. J. Phil 63, 17, 481--495.
• 57: Weidenbach, C. 2006. SPASS: An automated theorem prover for first-order logic with equality. http://spass.mpi-sb.mpg.de/index.html.
• 58: Eran Yahav, Verifying safety properties of concurrent Java programs using 3-valued logic, Proceedings of the 28th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.27-40, January 2001, London, United Kingdom
• 59: Eran Yahav , G. Ramalingam, Verifying safety properties using separation and heterogeneous abstractions, Proceedings of the ACM SIGPLAN 2004 conference on Programming language design and implementation, June 09-11, 2004, Washington DC, USA
• 60: Yahav, E. and Sagiv, M. 2003. Automatically verifying concurrent queue algorithms. In Electronic Notes in Theoretical Computer Science, vol. 89. B. Cook et al. Eds. Elsevier.
• 61: Yorsh, G. 2003. Logical characterizations of heap abstractions. M.S. thesis, Tel-Aviv University, Tel-Aviv, Israel. http://www.math.tau.ac.il/~gretay.
• 62: Yorsh, G., Reps, T. W., and Sagiv, M. 2004. Symbolically computing most precise abstract operations for shape analysis. In Tools and Algorithms for the Construction and Analysis of Systems. Lecture Notes in Computer Science, vol. 2988. Springer Verlag. 530--545.

INDEX TERMS

Primary Classification:
  D. Software
  D.2 SOFTWARE ENGINEERING
      D.2.4 Software/Program Verification

General Terms:
Verification

Keywords:
Logic, canonical abstraction, characterization, shape analysis