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. Andersen, L. O. 1993. Binding-Time analysis and the taming of C pointers. In Proceedings of the ACM Symposium on Partial Evaluation and Semantics-Based Program Manipulation (PEPM), D. Schmidt, Ed. 47--58.]]
2. Benedikt, M., Reps, T., and Sagiv, M. 1999. A decidable logic for describing linked data structures. In Proceedings of the European Symposium On Programming. 2--19.]]
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. Bruns, G. and Godefroid, P. 2000. Generalized model checking: Reasoning about partial state spaces. In Proceedings of the Concurrency Theory: 11th International Conference (CONCUR). Lecture Notes in Computer Science, vol. 1877. Springer Verlag, 168--182.]]
5. Chase, D., Wegman, M., and Zadeck, F. 1990. Analysis of pointers and structures. In SIGPLAN Conference on Programming Language Design and Implementation. 296--310.]]
6. Clarke, E., Grumberg, O., Jha, S., Lu, Y., and Veith, H. 2000. Counterexample-Guided abstraction refinement. In Proceedings of the Conference on Computer-Aided Verification. 154--169.]]
7. Clarke, E., Grumberg, O., and Long, D. 1994. Model checking and abstraction. Trans. Prog. Lang. Syst. 16, 5, 1512--1542.]]
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. Cousot, P. and Cousot, R. 1977. Abstract interpretation: A unified lattice model for static analysis of programs by construction of approximation of fixed points. In Symposium on Principles of Programming Languages. 238--252.]]
10. Dams, D. 1996. Abstract interpretation and partial refinement for model checking. Ph.D. thesis, Technical University of Eindhoven, Eindhoven, The Netherlands.]]
11. Das, M. 2000. Unification-Based pointer analysis with directional assignments. In Conference on Programming Language Design and Implementation. 35--46.]]
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. Fähndrich, M., Foster, J., Su, Z., and Aiken, A. 1998. Partial online cycle elimination in inclusion constraint graphs. In Proceedings of the SIGPLAN Conference on Programming Language Design and Implementation. 85--96.]]
16. Fradet, P. and Metayer, D. L. 1997. Shape types. In Proceedings of the Symposium on Principles of Programming Languages. 27--39.]]
17. Godefroid, P. and Jagadeesan, R. 2003. On the expressiveness of 3-valued models. In Proceedings of the 4th Conference on Verfication, Model Checking and Abstract Interpretation (VMCAI). 206--222.]]
18. Heintze, N. and Tardieu, O. 2001. Ultra-Fast aliasing analysis using CLA: A million lines of C code in a second. In Proceedings of the SIGPLAN Conference on Programming Language Design and Implementation.]]
19. Hell, P. and Nesetril, J. 2004. Graphs and Homomorphisms. Oxford University Press.]]
20. Hendren, L. 1990. Parallelizing programs with recursive data structures. Ph.D. thesis, Cornell University, Ithaca, NY.]]
21. Hendren, L., Hummel, J., and Nicolau, A. 1992. Abstractions for recursive pointer data structures: Improving the analysis and the transformation of imperative programs. In Proceedings of the SIGPLAN Conference on Programming Language Design and Implementation. 249--260.]]
22. Hendren, L. and Nicolau, A. 1990. Parallelizing programs with recursive data structures. IEEE Trans. Parallel Distrib Syst. 1, 1 (Jan.), 35--47.]]
23. Henriksen, J., Jensen, J., Jørgensen, M., Klarlund, N., Paige, B., Rauhe, T., and Sandholm, A. 1996. Mona: Monadic second-order logic in practice. In Proceedings of the Tools and Algorithms for the Construction and Analysis of Systems (TACAS'95). 89--110.]]
24. Huth, M., Jagadeesan, R., and Schmidt, D. A. 2001. Modal transition systems: A foundation for three-valued program analysis. In Proceedings of the Programming Languages and Systems: 10th European Symposium on Programming (ESOP). Lecture Notes in Computer Science, vol. 2028. Springer Verlag. 155--169.]]
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. Jones, N. and Muchnick, S. 1982. A flexible approach to interprocedural data flow analysis and programs with recursive data structures. In Symposium on Principles of Programming Languages. 66--74.]]
30. Klarlund, N. and Schwartzbach, M. 1993. Graph types. In Symposium on Principles of Programming Languages. New York, NY, 196--205.]]
31. Kuncak, V., Lam, P., and Rinard, M. C. 2002. Role analysis. In Proceedings of the Conference POPL. 17--32.]]
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. Lev-Ami, T., Reps, T., Sagiv, M., and Wilhelm, R. 2000. Putting static analysis to work for verification: A case study. In Proceedings of the International Symposium on Software Testing and Analysis. 26--38.]]
38. Lev-Ami, T. and Sagiv, M. 2000. TVLA: A system for implementing static analyses. In Proceedings of the Static Analysis Symposium. 280--301.]]
39. McCune, W. 2001. Mace 2.0 reference manual and guide. http://www-unix.mcs.anl.gov/AR/mace/.]]
40. McMillan, K. L. 1999. Verification of infinite state systems by compositional model checking. In Proceedings of the Correct Hardware Design and Venfication Methods: 110th IFIP WG 10.5 Advanced Research Working Conference (CHARME). Lecture Notes in Computer Science, vol. 1703. Springer Verlag. 219--234.]]
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. Møller, A. and Schwartzbach, M. 2001. The pointer assertion logic engine. In SIGPLAN Conference on Programming Language Design and Implementation. 221--231.]]
43. Mortimer, M. 1975. On languages with two variables. Zeitschrift fur Math. Logik uematischend Grundlagen der Math 21, 135--140.]]
44. Nielson, F., Nielson, H., and Hankin, C. 1999. Principles of Program Analysis. Springer Verlag.]]
45. Nielson, F., Nielson, H., and Sagiv, M. 2000. A Kleene analysis of mobile ambients. In Proceedings of the Programming Languages and Systems: 19th European Symposium on Programming (ESOP). Lecture Notes in Computer Science, vol. 1782. Springer Verlag. 305--319.]]
46. Rabin, M. 1969. Decidability of second-order theories and automata on infinite trees. Trans. Amer. Math. Soc. 141, 1--35.]]
47. Ramalingam, G., Varshavsky, A., Field, J., Goyal, D., and Sagiv, M. 2002. Deriving specialized program analyses for certifying component-client conformance. In Proceedings of the PLDI Conferance. 83--94.]]
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. Sagiv, M., Reps, T., and Wilhelm, R. 1998. Solving shape-analysis problems in languages with destructive updating. Trans. Program. Lang. Syst. 20, 1 (Jan.), 1--50.]]
50. Sagiv, M., Reps, T., and Wilhelm, R. 1999. Parametric shape analysis via 3-valued logic. In Symposium on Principles of Programming Language. 105--118.]]
51. Sagiv, M., Reps, T., and Wilhelm, R. 2002. Parametric shape analysis via 3-valued logic. Trans. Program. Lang. Syst.]]
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. Shapiro, M. and Horwitz, S. 1997. Fast and accurate flow-insensitive points-to analysis. In Symposium on Principles of Programming Languages. 1--14.]]
54. Steensgaard, B. 1996. Points-to analysis in almost-linear time. In Proceedings of the Symposium on Principles of Programming Languages. 32--41.]]
55. Su, Z., Fähndrich, M., and Aiken, A. 2000. Projection merging: Reducing redundancies in inclusion constraint graphs. In Proceedings of the Symposium on Principles of Programming Languages, T. Reps, Ed. 81--95.]]
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. Yahav, E. 2001. Verifying safety properties of concurrent Java programs using 3-valued logic. In Proceedings of the Symposium on Principles of Programming Languages 36, 3, 27--40.]]
59. Yahav, E. and Ramalingam, G. 2004. Verifying safety properties using separation and heterogeneous abstractions. In Proceedings of the ACM SIGPLAN Conference on Programming Language Design and Implementation. 25--34.]]
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

• General and reference

  • Cross-computing tools and techniques

    • Verification

• Software and its engineering

  • Software creation and management

    • Software development process management

    • Software verification and validation

      • Formal software verification

  • Software organization and properties

    • Software functional properties

      • Formal methods

        • Software verification

• Theory of computation

  • Semantics and reasoning

    • Program reasoning

      • Program verification