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.