CSR----SMA Modular Pluggable Program Analyses

程序分析的开发人员今天面临着一个令人不安的选择：产生一个精确的分析，可以提取或验证相当复杂的属性（但无法扩展到大型程序）或产生一个有效的分析，可伸缩性好（但提取或验证只有非常基本的属性）。不幸的是，精确程序分析的潜在好处（检测编程错误，验证程序保持其数据结构一致性属性，增强提取有意义的设计信息的能力等）该项目将寻求一种新的方法，使多个分析集中应用于同一程序中的不同实例化模块，每个分析应用于最适合的模块。每个模块封装一个或多个数据结构，并使用抽象集合中的成员资格来指定每个模块的操作如何影响对象在其数据结构中的参与。每个分析验证所分析的模块的实现1）保留重要的内部数据结构表示不变量，以及2）符合使用集合代数中的公式来表征操作对数据结构的影响的规范。 每个分析都将使用一个抽象函数来建立具体数据结构实现和抽象集合成员之间的联系。这个抽象函数使分析能够将跨越模块边界的对象的集合成员属性转换回模块内的具体数据结构属性。这些属性对于验证数据结构保持一致以及每个模块正确实现其抽象集接口至关重要。系统通常具有涉及多个模块的一致性属性。例如，系统可能要求参与两个给定模块的对象集是不相交的。因为这些属性涉及多个模块共享的对象，所以如果要成功验证属性，不同的分析必须以某种方式互操作。在这里追求的方法中，这些类型的不变量使用抽象集合包含属性的布尔代数表示，并在适当的程序点通过每次分析进行局部验证。因此，这种方法消除了在程序的大区域中应用复杂（并且可能不可扩展）分析的需要。

Developers of program analyses today face an uncomfortable choice: produce a precise analysis that can extract or verify quite sophisticated properties (but fails to scale to large programs) or produce an efficient analysis that scales well (but extracts or verifies only very basic properties). The unfortunate consequence is that the potential benefits of precise program analysis (detecting programming errors, verifying that the program preserves its data structure consistency properties, enhanced ability to extract meaningful design information, etc.) are currently denied to the large programs that need them the most.The project will pursue a new approach that enables the focused application of multiple analyses to different instantiable modules in the same program, with each analysis applied to the modules for which it is most appropriate. Each module encapsulates one or more data structures and uses membership in abstract sets to specify how the actions of each module affect the participation of objects in its data structures. Each analysis verifies that the implementation of the analyzed module 1) preserves important internal data structure representation invariants and 2) conforms to a specification that uses formulas in a set algebra to characterize the effects of operations on the data structure. Each analysis will use an abstraction function to establish the connection between the concrete data structure implementation and abstract set membership. This abstraction function enables the analysis to translate the set membership properties of objects that cross module boundaries back into concrete data structure properties within the module. These properties are crucial to verifying that the data structures remain consistent and that each module correctly implements its abstract set interface.Systems often have consistency properties that involve multiple modules. For example, a system may require the sets of objects that participate in two given modules to be disjoint. Because these properties involve objects shared across multiple modules, different analyses must somehow interoperate if they are to successfully verify the property. In the approaches pursued here , these kinds of invariants are expressed using a boolean algebra of abstract set inclusion properties and locally verified at the appropriate program points by each analysis. This approach therefore eliminates the need to apply complex (and potentially unscalable) analyses across large regions of the program.