Advertisement

Checking the Shape Safety of Pointer Manipulations

  • Adam Bakewell
  • Detlef Plump
  • Colin Runciman
Part of the Lecture Notes in Computer Science book series (LNCS, volume 3051)

Abstract

We present a new algorithm for checking the shape-safety of pointer manipulation programs. In our model, an abstract, data-less pointer structure is a graph. A shape is a language of graphs. A pointer manipulation program is modelled abstractly as a set of graph rewrite rules over such graphs where each rule corresponds to a pointer manipulation step. Each rule is annotated with the intended shape of its domain and range and our algorithm checks these annotations.

We formally define the algorithm and apply it to a binary search tree insertion program. Shape-safety is undecidable in general, but our method is more widely applicable than previous checkers, in particular, it can check programs that temporarily violate a shape by the introduction of intermediate shape definitions.

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. [Bak03]
    Bakewell, A.: Algorithms for checking the shape safety of graph transformation rules. Technical report, Available from [SPG] (2003)Google Scholar
  2. [BPR03a]
    Bakewell, A., Plump, D., Runciman, C.: Checking the shape safety of pointer manipulations —extended abstract. In: Participant’s Proceedings of the 7th International Seminar on Relational Methods in Computer Science (RelMiCS 7), Malente, Germany, pp. 144–151. University of Kiel (2003), Available from [SPG]Google Scholar
  3. [BPR03b]
    Bakewell, A., Plump, D., Runciman, C.: Specifying pointer structures by graph reduction. Technical Report YCS-2003-367, Department of Computer Science, University of York (2003), Available from [SPG]Google Scholar
  4. [BRS99]
    Benedikt, M., Reps, T., Sagiv, M.: A decidable logic for describing linked data structures. In: Swierstra, S.D. (ed.) ESOP 1999. LNCS, vol. 1576, pp. 2–19. Springer, Heidelberg (1999)CrossRefGoogle Scholar
  5. [DHM03]
    Drewes, F., Hoffmann, B., Minas, M.: Context-exploiting shapes for diagram transformation. Machine Graphics and Vision 12(1), 117–132 (2003)Google Scholar
  6. [FM97]
    Fradet, P., Le Métayer, D.: Shape types. I. In: Proc. Principles of Programming Languages (POPL 1997), pp. 27–39. ACM Press, New York (1997)Google Scholar
  7. [FM98]
    Fradet, P., Le Métayer, D.: Structured Gamma. Science of Computer Programming 31(2-3), 263–289 (1998)zbMATHCrossRefMathSciNetGoogle Scholar
  8. [HMP01]
    Habel, A., Müller, J., Plump, D.: Double-pushout graph transformation revisited. Math. Struct. Comp. Science 11, 637–688 (2001)zbMATHGoogle Scholar
  9. [HP01]
    Habel, A., Plump, D.: Computational completeness of programming languages based on graph transformation. In: Honsell, F., Miculan, M. (eds.) FOSSACS 2001. LNCS, vol. 2030, pp. 230–245. Springer, Heidelberg (2001)CrossRefGoogle Scholar
  10. [IO01]
    Ishtiaq, S., O’Hearn, P.W.: BI as an assertion language for mutable data structures. In: Proc. Principles of Programming Languages (POPL 2001), pp. 14–26. ACM Press, New York (2001)Google Scholar
  11. [KLR02]
    Kuncak, V., Lam, P., Rinard, M.: Role analysis. In: Proc. Principles of Programming Languages (POPL 2002), pp. 17–32. ACM Press, New York (2002)Google Scholar
  12. [KS93]
    Klarlund, N., Schwartzbach, M.I.: Graph types. In: Proc. Principles of Programming Languages (POPL 1993), pp. 196–205. ACM Press, New York (1993)Google Scholar
  13. [MS01]
    Møller, A., Schwartzbach, M.I.: The pointer assertion logic engine. In: Proc. ACM SIGPLAN 2001 Conference on Programming Langauge Design and Implementation (PLDI 2001), ACM Press, New York (2001)Google Scholar
  14. [SPG]
    Safe Pointers by Graph Transformation, project webpage, http://www-users.cs.york.ac.uk/~ajb/spgt/
  15. [SRW02]
    Sagiv, M., Reps, T., Wilhelm, R.: Parametric shape analysis via 3- valued logic. ACM Transactions on Programming Languages and Systems 24(3), 217–298 (2002)CrossRefGoogle Scholar
  16. [WM01]
    Walker, D., Morrisett, G.: Alias types for recursive data structures. In: Harper, R. (ed.) TIC 2000. LNCS, vol. 2071, pp. 177–206. Springer, Heidelberg (2001)CrossRefGoogle Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 2004

Authors and Affiliations

  • Adam Bakewell
    • 1
  • Detlef Plump
    • 1
  • Colin Runciman
    • 1
  1. 1.Department of Computer ScienceUniversity of YorkUK

Personalised recommendations