Bor-Yuh Evan Chang
Xavier Rival
George C. NeculaXisa is an automatic program analysis and verification tool for reasoning about recursive data structures, such as pointer-based lists and trees. The Xisa approach is unique in that it utilizes high-level, program developer-oriented specifications to focus the analysis to properties of interest to the developer.
Shape analyses, like Xisa, are particularly important in that they can capture detailed aliasing and structural information that is typically beyond the ability of other static program analyses. To be precise and scalable, they need to use program-specific abstractions. Unlike other approaches that are typically either insufficiently customizable or require low-level, expert interaction, Xisa builds program-specific abstractions using high-level, inductive predicates analogous to data structure validation code (e.g., a pretty-printer of a data structure written by developers for testing or dynamic analysis). In the end, Xisa presents program invariants about the memory state in the form of graphical diagrams roughly comparable to those that would appear on a whiteboard or in a textbook.
For more details and examples, please see the demonstration page.
Papers
-
Calling Context Abstraction with Shapes [pdf, ps]
Xavier Rival and Bor-Yuh Evan Chang.
Thirty-Eighth Symposium on Principles of Programming Languages (POPL'11), ©ACM.abstractInterprocedural program analysis is often performed by computing procedure summaries. While possible, computing adequate summaries is difficult, particularly in the presence of recursive procedures. In this paper, we propose a complementary framework for interprocedural analysis based on a direct abstraction of the calling context. Specifically, our approach exploits the inductive structure of a calling context by treating it directly as a stack of activation records. We then build an abstraction based on separation logic with inductive definitions. A key element of this abstract domain is the use of parameters to refine the meaning of such call stack summaries and thus express relations across activation records and with the heap. In essence, we define an abstract interpretation-based analysis framework for recursive programs that permits a fluid per call site abstraction of the call stack—much like how shape analyzers enable a fluid per program point abstraction of the heap.Separating Shape Graphs [pdf]
Vincent Laviron, Bor-Yuh Evan Chang, and Xavier Rival.
Nineteenth European Symposium on Programming (ESOP'10), ©Springer-Verlag.abstractDetailed 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).Relational Inductive Shape Analysis [pdf, ps] [acm] [dblp]
Bor-Yuh Evan Chang and Xavier Rival.
Thirty-Fifth Symposium on Principles of Programming Languages (POPL'08), ©ACM.abstractShape analyses are concerned with precise abstractions of the heap to capture detailed structural properties. To do so, they need to build and decompose summaries ofdisjoint memory regions. Unfortunately, many data structure invariants require relations be tracked across disjoint regions, such as intricate numerical data invariants or structural invariants concerning back and cross pointers. In this paper, we identify issues inherent to analyzing relational structures and design an abstract domain that is parameterized both by an abstract domain for pure data properties and by user-supplied specifications of the data structure invariants to check. Particularly, it supports hybrid invariants about shape and data and features a generic mechanism for materializing summaries at the beginning, middle, or end of inductive structures. Around this domain, we build a shape analysis whose interesting components include a pre-analysis on the user-supplied specifications that guides the abstract interpretation and a widening operator over the combined shape and data domain. We then demonstrate our techniques on the proof of preservation of the red-black tree invariants during insertion. -
Shape Analysis with Structural Invariant Checkers [pdf, ps] [lncs] [dblp]
Bor-Yuh Evan Chang, Xavier Rival, and George C. Necula.
Fourteenth International Static Analysis Symposium (SAS'07), ©Springer-Verlag.Extended version available as Technical Report UCB/EECS-2007-80 [pdf].abstractDeveloper-supplied data structure specifications are important to shape analyses, as they tell the analysis what information should be tracked in order to obtain the desired shape invariants. We observe that data structure checking code (e.g., used in testing or dynamic analysis) provides shape information that can also be used in static analysis. In this paper, we propose a lightweight, automatic shape analysis based on these developer-supplied structural invariant checkers. In particular, we set up a parametric abstract domain, which is instantiated with such checker specifications to summarize memory regions using both notions of complete and partial checker evaluations. The analysis then automatically derives a strategy for canonicalizing or weakening shape invariants.
Talks
-
July 24, 2009 Reduction in End-User Shape Analysis [pptx, ppt, flash]
Bor-Yuh Evan Chang.
Dagstuhl Seminar 09301: Typing, Analysis, and Verification of Heap-Manipulating Programs.
Wadern, Germany. -
July 23, 2009 Shape Analysis Applied to C Code [pdf]
Xavier Rival.
Dagstuhl Seminar 09301: Typing, Analysis, and Verification of Heap-Manipulating Programs.
Wadern, Germany. -
August 28, 2008 End-User Program Analysis [pptx, ppt]
Bor-Yuh Evan Chang.
Dissertation Talk. University of California, Berkeley.
Berkeley, California, USA.May 16, 2008 Extensible Shape Analysis by Designing with the User in Mind [pptx, ppt]
Bor-Yuh Evan Chang.
Open Source Quality Project Retreat.
Santa Cruz, California, USA. -
August 27, 2007 Materialization in Shape Analysis with Structural Invariant Checkers [ppt, pdf]
Bor-Yuh Evan Chang.
IT University of Copenhagen.
Copenhagen, Denmark.abstractShape analyses are unique in that they can capture detailed aliasing and structural information that is typically beyond the ability of other static program analyses. To do so, they rely on specialized data structure descriptions to build precise heap abstractions. A key component of shape analyses that enable such precision is a partial concretization operation on abstract memories (i.e., materialization).In many respects, inductively-defined data structure specifications are a natural fit for shape analysis. First, we observe that they often resemble data structure invariant checkers used by program developers for testing or dynamic analysis. Second, they yield a straightforward materialization operation, that is, the unfolding of inductive definitions.
In this talk, we discuss an automated shape analysis parameterized by such developer-supplied inductive checkers. We focus on the challenges in designing such a parametric memory abstraction, which centers on abstractions for local invariants at intermediate program points (i.e., when the global data structure invariant holds only partially). In particular, we propose a generic unfolding (i.e., materialization) operation built on a type pre-analysis on the developer-supplied checkers. Such a mechanism is particularly important for data structures with back pointers, such a doubly-linked lists and trees with parent pointers.
Related Projects
- Tel Aviv University (IL)
- Carnegie Mellon University (US)
- MSR Cambridge (UK)
- Queen Mary, East London Massive (UK)
- MSR Redmond (US)
- EPFL (CH)
- Queen Mary, East London Massive (UK)
- MSR Redmond (US)