Loading...
Please wait, while we are loading the content...
Similar Documents
Fissile Type Analysis: Modular Checking of Almost Everywhere Invariants
| Content Provider | CiteSeerX |
|---|---|
| Author | Coughlin, Devin Chang, Bor-Yuh Evan |
| Abstract | We present a generic analysis approach to the imperative relation-ship update problem, in which destructive updates temporarily vio-late a global invariant of interest. Such invariants can be conveniently and concisely specified with dependent refinement types, which are efficient to check flow-insensitively. Unfortunately, while traditional flow-insensitive type checking is fast, it is inapplicable when the desired invariants can be temporarily broken. To overcome this lim-itation, past works have directly ratcheted up the complexity of the type analysis and associated type invariants, leading to ineffi-cient analysis and verbose specifications. In contrast, we propose a generic lifting of modular refinement type analyses with a symbolic analysis to efficiently and effectively check concise invariants that hold almost everywhere. The result is an efficient, highly modular flow-insensitive type analysis to optimistically check the preserva-tion of global relationship invariants that can fall back to a precise, disjunctive symbolic analysis when the optimistic assumption is vio-lated. This technique permits programmers to temporarily break and then re-establish relationship invariants—a flexibility that is crucial for checking relationships in real-world, imperative languages. A significant challenge is selectively violating the global type consis-tency invariant over heap locations, which we achieve via almost type-consistent heaps. To evaluate our approach, we have encoded the problem of verifying the safety of reflective method calls in dynamic languages as a refinement type checking problem. Our analysis is capable of validating reflective call safety at interactive speeds on commonly-used Objective-C libraries and applications. Categories and Subject Descriptors F.3.1 [Logics and Meanings |
| File Format | |
| Access Restriction | Open |
| Content Type | Text |
