Parametric shape analysis via 3-valued logic

ABSTRACT

Shape analysis concerns the problem of determining "shape invariants" for programs that perform destructive updating on dynamically allocated storage. This article presents a parametric framework for shape analysis that can be instantiated in different ways to create different shape-analysis algorithms that provide varying degrees of efficiency and precision. A key innovation of the work is that the stores that can possibly arise during execution are represented (conservatively) using 3-valued logical structures. The framework is instantiated in different ways by varying the predicates used in the 3-valued logic. The class of programs to which a given instantiation of the framework can be applied is not limited a priori (i.e., as in some work on shape analysis, to programs that manipulate only lists, trees, DAGS, etc.); each instantiation of the framework can be applied to any program, but may produce imprecise results (albeit conservative ones) due to the set of predicates employed.

REFERENCES

• 1: Aiken, A. 1996. Position statement. Prepared for the Programming Languages Working Group of the ACM Workshop on Strategic Directions in Computing Research (Cambridge, Mass, June 14--15, 1996).
• 2: Assmann, U. and Weinhardt, M. 1993. Interprocedural heap analysis for parallelizing imperative programs. In Programming Models For Massively Parallel Computers, W. K. Giloi, S. Jähnichen, and B. D. Shriver, Eds., IEEE Press, Washington, DC, 74--82.
• 3: Bell, J. and Machover, M. 1977. A Course in Mathematical Logic. North-Holland, Amsterdam.
• 4: 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
• 5: Luca Cardelli , Andrew D. Gordon, Mobile Ambients, Proceedings of the First International Conference on Foundations of Software Science and Computation Structure, p.140-155, March 28-April 04, 1998
• 6: 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
• 7: Clarke, E. and Jha, S. 1995. Symmetry and induction in model checking. In Computer Science Today: Recent Trends and Developments, J. V. Leeuwen, Ed., Lecture Notes in Computer Science, vol. 1000, Springer-Verlag, New York, 455--470.
• 8: 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
• 9: R. L. Constable , S. D. Johnson , C. D. Eichenlaub, An Introduction to the PL/CV2 Programming Logic, Springer-Verlag New York, Inc., Secaucus, NJ, 1982
• 10: 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]
• 11: Patrick Cousot , Radhia Cousot, Systematic design of program analysis frameworks, Proceedings of the 6th ACM SIGACT-SIGPLAN symposium on Principles of programming languages, p.269-282, January 29-31, 1979, San Antonio, Texas [doi>10.1145/567752.567778]
• 12: Satyaki Das , David L. Dill , Seungjoon Park, Experience with Predicate Abstraction, Proceedings of the 11th International Conference on Computer Aided Verification, p.160-171, July 06-10, 1999
• 13: Deutsch, L. 1973. An interactive program verifier. Ph.D. Thesis, University of California, Berkeley, Calif.
• 14: Edsger Wybe Dijkstra, A Discipline of Programming, Prentice Hall PTR, Upper Saddle River, NJ, 1997
• 15: Jacob Elgaard , Anders Møller , Michael I. Schwartzbach, Compile-Time Debugging of C Programs Working on Trees, Proceedings of the 9th European Symposium on Programming Languages and Systems, p.119-134, April 02, 2000
• 16: E. Allen Emerson , A. Prasad Sistla, Symmetry and Model Checking, Proceedings of the 5th International Conference on Computer Aided Verification, p.463-478, June 28-July 01, 1993
• 17: Ginsberg, M. 1988. Multivalued logics: A uniform approach to inference in artificial intelligence. Comp. Intell. 4, 265--316.
• 18: Susanne Graf , Hassen Saïdi, Construction of Abstract State Graphs with PVS, Proceedings of the 9th International Conference on Computer Aided Verification, p.72-83, June 22-25, 1997
• 19: David Gries, The Science of Programming, Springer-Verlag New York, Inc., Secaucus, NJ, 1987
• 20: Laurie Jane Hendren, Parallelizing programs with recursive data structures, Cornell University, Ithaca, NY, 1990
• 21: 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]
• 22: 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
• 23: Hoare, C. 1975. Recursive data structures. Int. J. Comput. Inf. Sci. 4, 2, 105--132.
• 24: S. Horwitz , P. Pfeiffer , T. Reps, Dependence analysis for pointer variables, Proceedings of the ACM SIGPLAN 1989 Conference on Programming language design and implementation, p.28-40, June 19-23, 1989, Portland, Oregon, United States
• 25: Jakob L. Jensen , Michael E. Jørgensen , Michael I. Schwartzbach , Nils Klarlund, Automatic verification of pointer programs using monadic second-order logic, Proceedings of the ACM SIGPLAN 1997 conference on Programming language design and implementation, p.226-234, June 16-18, 1997, Las Vegas, Nevada, United States
• 26: 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, N.J., Chapter 4, 102--131.
• 27: 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]
• 28: James Cornelius King, A program verifier, 1970
• 29: Kleene, S. 1987. Introduction to Metamathematics, Second Ed. North-Holland, Amsterdam.
• 30: Kunen, K. 1998. Personal communication.
• 31: J. R. Larus , P. N. Hilfinger, Detecting conflicts between structure accesses, Proceedings of the ACM SIGPLAN 1988 conference on Programming Language design and Implementation, p.24-31, June 20-24, 1988, Atlanta, Georgia, United States
• 32: Lev-Ami, T. 2000. TVLA: A framework for Kleene based static analysis. M.S. Thesis, Tel-Aviv University, Tel-Aviv, Israel.
• 33: 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
• 34: 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
• 35: Lifschitz, V. 1998. Personal communication.
• 36: Morris, J. 1982. Assignment and linked data structures. In Theoretical Foundations of Programming Methodology, M. Broy and G. Schmidt, Eds., D. Reidel, Boston, 35--41.
• 37: 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
• 38: John Plevyak , Andrew A. Chien , Vijay Karamcheti, Analysis of Dynamic Structures for Efficient Parallel Execution, Proceedings of the 6th International Workshop on Languages and Compilers for Parallel Computing, p.37-56, August 12-14, 1993
• 39: Noam Rinetzky , Shmuel Sagiv, Interprocedural Shape Analysis for Recursive Programs, Proceedings of the 10th International Conference on Compiler Construction, p.133-149, April 02-06, 2001
• 40: 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]
• 41: 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]
• 42: Jan Stransky, A lattice for abstract interpretation of dynamic (LISP-like) structures, Information and Computation, v.101 n.1, p.70-102, Nov. 1992 [doi>10.1016/0890-5401(92)90076-R]
• 43: Edward Yan-Bing Wang , Paul N. Hilfinger, Analysis of recursive types in an imperative language, 1994
• 44: 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
• 45: Yahav, E., Reps, T., and Sagiv, M. 2001. LTL model checking for systems with unbounded number of dynamically created threads and objects. Tech. Rep. TR-1424, Comp. Sci. Dept., Univ. of Wisconsin, Madison, Wisc. March.

INDEX TERMS

Primary Classification:
  D. Software
  D.2 SOFTWARE ENGINEERING
      D.2.5 Testing and Debugging
          Subjects: Symbolic execution

Additional Classification:
  D. Software
  D.3 PROGRAMMING LANGUAGES
      D.3.3 Language Constructs and Features
          Subjects: Data types and structures; Dynamic storage management

  E. Data
  E.1 DATA STRUCTURES
      Subjects: Graphs and networks; Lists, stacks, and queues; Trees
  E.2 DATA STORAGE REPRESENTATIONS
      Subjects: Linked representations

  F. Theory of Computation
  F.3 LOGICS AND MEANINGS OF PROGRAMS
      F.3.1 Specifying and Verifying and Reasoning about Programs
          Subjects: Invariants; Assertions

General Terms:
Algorithms, Languages, Theory, Verification

Keywords:
3-valued logic, Abstract interpretation, alias analysis, constraint solving, destructive updating, pointer analysis, shape analysis, static analysis