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 |
| Subject Keyword | Modular Checking Almost Everywhere Invariant Fissile Type Analysis Optimistic Assumption Past Work Interactive Speed Refinement Type Checking Problem Modular Flow-insensitive Type Analysis Reflective Method Subject Descriptor Dynamic Language Imperative Relation-ship Update Problem Global Relationship Invariant Significant Challenge Type Analysis Global Invariant Destructive Update Ineffi-cient Analysis Reflective Call Safety Verbose Specification Concise Invariant Commonly-used Objective-c Library Dependent Refinement Type Global Type Consis-tency Invariant Symbolic Analysis Heap Location Re-establish Relationship Desired Invariant Modular Refinement Type Disjunctive Symbolic Analysis Type-consistent Heap Type Invariant Traditional Flow-insensitive Type Checking Imperative Language Generic Analysis Approach Generic Lifting |
| Content Type | Text |
