Checking the shape safety of pointer manipulations

Detlef Plump; Adam Bakewell; Colin Runciman

doi:10.1007/978-3-540-24771-5_5

Checking the shape safety of pointer manipulations

Detlef Plump, Adam Bakewell, Colin Runciman

Computer Science

Research output: Chapter in Book/Report/Conference proceeding › Conference contribution

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.

Original language	English
Title of host publication	Relational Methods in Computer Science (RelMiCS 7), Revised Selected Papers
Editors	R Berghammer, B Moller, G Struth
Place of Publication	Berlin
Publisher	Springer
Pages	48-61
Number of pages	14
ISBN (Print)	3-540-22145-X
DOIs	https://doi.org/10.1007/978-3-540-24771-5_5
Publication status	Published - 2004
Event	7th International Seminar on Relational Methods in Computer Science/2nd International Workshop on Applications of Kleene Algebra - Bad Malente Duration: 12 May 2003 → 17 May 2003

Publication series

Name	Lecture Notes in Computer Science
Publisher	Springer
Volume	3051

Conference

Conference	7th International Seminar on Relational Methods in Computer Science/2nd International Workshop on Applications of Kleene Algebra
City	Bad Malente
Period	12/05/03 → 17/05/03

Access to Document

10.1007/978-3-540-24771-5_5

http://www.cs.york.ac.uk/plasma/publications/pdf/BakewellPlumpRunciman.04a.pdfLicence: Unspecified

Cite this

@inproceedings{52741235a52e41b98c79dad177e0ebe3,

title = "Checking the shape safety of pointer manipulations",

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.",

author = "Detlef Plump and Adam Bakewell and Colin Runciman",

year = "2004",

doi = "10.1007/978-3-540-24771-5_5",

language = "English",

isbn = "3-540-22145-X",

series = "Lecture Notes in Computer Science",

publisher = "Springer",

pages = "48--61",

editor = "R Berghammer and B Moller and G Struth",

booktitle = "Relational Methods in Computer Science (RelMiCS 7), Revised Selected Papers",

address = "Germany",

note = "7th International Seminar on Relational Methods in Computer Science/2nd International Workshop on Applications of Kleene Algebra ; Conference date: 12-05-2003 Through 17-05-2003",

}

Plump, D, Bakewell, A & Runciman, C 2004, Checking the shape safety of pointer manipulations. in R Berghammer, B Moller & G Struth (eds), Relational Methods in Computer Science (RelMiCS 7), Revised Selected Papers. Lecture Notes in Computer Science, vol. 3051, Springer, Berlin, pp. 48-61, 7th International Seminar on Relational Methods in Computer Science/2nd International Workshop on Applications of Kleene Algebra, Bad Malente, 12/05/03. https://doi.org/10.1007/978-3-540-24771-5_5

Checking the shape safety of pointer manipulations. / Plump, Detlef; Bakewell, Adam; Runciman, Colin.
Relational Methods in Computer Science (RelMiCS 7), Revised Selected Papers. ed. / R Berghammer; B Moller; G Struth. Berlin: Springer, 2004. p. 48-61 (Lecture Notes in Computer Science; Vol. 3051).

Research output: Chapter in Book/Report/Conference proceeding › Conference contribution

TY - GEN

T1 - Checking the shape safety of pointer manipulations

AU - Plump, Detlef

AU - Bakewell, Adam

AU - Runciman, Colin

PY - 2004

Y1 - 2004

N2 - 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.

AB - 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.

U2 - 10.1007/978-3-540-24771-5_5

DO - 10.1007/978-3-540-24771-5_5

M3 - Conference contribution

SN - 3-540-22145-X

T3 - Lecture Notes in Computer Science

SP - 48

EP - 61

BT - Relational Methods in Computer Science (RelMiCS 7), Revised Selected Papers

A2 - Berghammer, R

A2 - Moller, B

A2 - Struth, G

PB - Springer

CY - Berlin

T2 - 7th International Seminar on Relational Methods in Computer Science/2nd International Workshop on Applications of Kleene Algebra

Y2 - 12 May 2003 through 17 May 2003

ER -