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.
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
References
Bakewell, A.: Algorithms for checking the shape safety of graph transformation rules. Technical report, Available from [SPG] (2003)
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]
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]
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)
Drewes, F., Hoffmann, B., Minas, M.: Context-exploiting shapes for diagram transformation. Machine Graphics and Vision 12(1), 117–132 (2003)
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)
Fradet, P., Le Métayer, D.: Structured Gamma. Science of Computer Programming 31(2-3), 263–289 (1998)
Habel, A., Müller, J., Plump, D.: Double-pushout graph transformation revisited. Math. Struct. Comp. Science 11, 637–688 (2001)
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)
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)
Kuncak, V., Lam, P., Rinard, M.: Role analysis. In: Proc. Principles of Programming Languages (POPL 2002), pp. 17–32. ACM Press, New York (2002)
Klarlund, N., Schwartzbach, M.I.: Graph types. In: Proc. Principles of Programming Languages (POPL 1993), pp. 196–205. ACM Press, New York (1993)
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)
Safe Pointers by Graph Transformation, project webpage, http://www-users.cs.york.ac.uk/~ajb/spgt/
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)
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)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2004 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Bakewell, A., Plump, D., Runciman, C. (2004). Checking the Shape Safety of Pointer Manipulations. In: Berghammer, R., Möller, B., Struth, G. (eds) Relational and Kleene-Algebraic Methods in Computer Science. RelMiCS 2003. Lecture Notes in Computer Science, vol 3051. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-540-24771-5_5
Download citation
DOI: https://doi.org/10.1007/978-3-540-24771-5_5
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-22145-6
Online ISBN: 978-3-540-24771-5
eBook Packages: Springer Book Archive