Publication detail

From Low-Level Pointers to High-Level Containers

DUDKA, K. HOLÍK, L. PERINGER, P. TRTÍK, M. VOJNAR, T.

Original Title

From Low-Level Pointers to High-Level Containers

English Title

From Low-Level Pointers to High-Level Containers

Type

conference paper

Language

en

Original Abstract

We propose a method that transforms a C program manipulating containers using low-level pointer statements into an equivalent program where the containers are manipulated via calls of standard high-level container operations like push_back or pop_front. The input of our method is a C program annotated by a special form of shape invariants which can be obtained from current automatic shape analysers after a slight modification. The resulting program where the low-level pointer statements are summarized into high-level container operations is more understandable and (among other possible benefits) better suitable for program analysis. We have implemented our approach and successfully tested it through a number of experiments with list-based containers, including experiments with simplification of program analysis by separating shape analysis from analysing data-related properties.

English abstract

We propose a method that transforms a C program manipulating containers using low-level pointer statements into an equivalent program where the containers are manipulated via calls of standard high-level container operations like push_back or pop_front. The input of our method is a C program annotated by a special form of shape invariants which can be obtained from current automatic shape analysers after a slight modification. The resulting program where the low-level pointer statements are summarized into high-level container operations is more understandable and (among other possible benefits) better suitable for program analysis. We have implemented our approach and successfully tested it through a number of experiments with list-based containers, including experiments with simplification of program analysis by separating shape analysis from analysing data-related properties.

Keywords

program analysis, static analysis, shape analysis, heap abstraction, symbolic memory graphs, program transformation, pointer programs, container programs

Released

17.01.2016

Publisher

Springer Verlag

Location

Berlin Heidelberg

ISBN

978-3-662-49121-8

Book

Verification, Model Checking, and Abstract Interpretation (VMCAI)

Edition

Lecture Notes in Computer Science

Edition number

NEUVEDEN

Pages from

431

Pages to

452

Pages count

22

URL

Documents

BibTex


@inproceedings{BUT130929,
  author="Kamil {Dudka} and Lukáš {Holík} and Petr {Peringer} and Marek {Trtík} and Tomáš {Vojnar}",
  title="From Low-Level Pointers to High-Level Containers",
  annote="We propose a method that transforms a C program manipulating containers using
low-level pointer statements into an equivalent program where the containers are
manipulated via calls of standard high-level container operations like push_back
or pop_front. The input of our method is a C program annotated by a special form
of shape invariants which can be obtained from current automatic shape analysers
after a slight modification. The resulting program where the low-level pointer
statements are summarized into high-level container operations is more
understandable and (among other possible benefits) better suitable for program
analysis. We have implemented our approach and successfully tested it through
a number of experiments with list-based containers, including experiments with
simplification of program analysis by separating shape analysis from analysing
data-related properties.",
  address="Springer Verlag",
  booktitle="Verification, Model Checking, and Abstract Interpretation (VMCAI)",
  chapter="130929",
  doi="10.1007/978-3-662-49122-5_21",
  edition="Lecture Notes in Computer Science",
  howpublished="print",
  institution="Springer Verlag",
  year="2016",
  month="january",
  pages="431--452",
  publisher="Springer Verlag",
  type="conference paper"
}