Static program analysis can improve programmer productivity and software reliability by definitively ruling out entire classes of programmer mistakes. For mainstream imperative languages such as C, C++, and Java, static analysis about the heap—memory that is dynamically allocated at run time—is particularly challenging because heap memory acts as global, mutable state.
This dissertation describes how to soundly combine two static analyses that each take vastly different approaches to reasoning about the heap: type systems and separation logic. Traditional type systems take an alias-agnostic, global view of the heap that affords both fast verification and light-weight annotation of invariants holding over the entire program. Separation logic, in contrast, provides an alias-aware, local view of the heap in which invariants can vary at each program point.
In this work, I show how type systems and separation logic can be safely and efficiently combined. The result is type-intertwined separation logic, an analysis that applies traditional type-based reasoning to some regions of the program and separation logic to others—converting between analysis representations at region boundaries—and summarizes some portions of the heap with coarse type invariants and others with precise separation logic invariants.
The key challenge that this dissertation addresses is the communication and preservation of heap invariants between analyses. I tackle this challenge with two core contributions. The first is type-consistent summarization and materialization, which enables type-intertwined separation logic to both leverage and selectively violate the global type invariant. This mechanism allows the analysis to efficiently and precisely verify invariants that hold almost everywhere. Second, I describe gated separating conjunction, a non-commutative strengthening of standard separating conjunction that expresses local dis-pointing relationships between sub-heaps. Gated separation enables local heap reasoning by permitting the separation logic to frame out portions of memory and prevent the type system from interfering with its contents—an operation that would be unsound in type-intertwined analysis with only standard separating conjunction. With these two contributions, type-intertwined separation logic combines the benefits of both type-like global reasoning and separation-logic-style local reasoning in a single analysis.
|Advisor:||Chang, Bor-Yuh Evan|
|Commitee:||Diwan, Amer, Jhala, Ranjit, Sankaranarayanan, Sriram, Siek, Jeremy G.|
|School:||University of Colorado at Boulder|
|School Location:||United States -- Colorado|
|Source:||DAI-B 76/10(E), Dissertation Abstracts International|
|Keywords:||Dependent types, Objective-c, Separation logic, Type systems|
Copyright in each Dissertation and Thesis is retained by the author. All Rights Reserved
The supplemental file or files you are about to download were provided to ProQuest by the author as part of a
dissertation or thesis. The supplemental files are provided "AS IS" without warranty. ProQuest is not responsible for the
content, format or impact on the supplemental file(s) on our system. in some cases, the file type may be unknown or
may be a .exe file. We recommend caution as you open such files.
Copyright of the original materials contained in the supplemental file is retained by the author and your access to the
supplemental files is subject to the ProQuest Terms and Conditions of use.
Depending on the size of the file(s) you are downloading, the system may take some time to download them. Please be