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
-
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
-
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)
- MSR Cambridge (UK)
- Queen Mary, East London Massive (UK)
- MSR Redmond (US)
- EPFL (CH)
- Queen Mary, East London Massive (UK)
- MSR Redmond (US)