Reference

Abstract

Detailed memory models that expose individual fields are necessary to precisely analyze code that makes use of low-level aspects such as, pointers to fields and untagged unions. Yet, higher-level representations that collect fields into records are often used because they are typically more convenient and efficient in modeling the program heap. In this paper, we present a shape graph representation of memory that exposes individual fields while largely retaining the convenience of an object-level model. This representation has a close connection to particular kinds of formulas in separation logic. Then, with this representation, we show how to extend the Xisa shape analyzer for low-level aspects, including pointers to fields, C-style nested structures and unions, malloc and free, and array values, with minimal changes to the core algorithms (e.g., materialization and summarization).

BibTeX

@string{ESOP = "European Symposium on Programming (ESOP)"}
@inproceedings{ssg-esop10,
  author = {Vincent Laviron and Bor-Yuh Evan Chang and Xavier Rival},
  title = {Separating Shape Graphs},
  booktitle = ESOP,
  year = {2010},
  pages = {387-406},
  
}