Extending Typestate Analysis to Multiple Interacting Objects

Extending Typestate Analysis to Multiple Interacting Objects
复制标题

将类型状态分析扩展到多个交互对象

DOI：
--
复制
发表时间：
2008
期刊：
影响因子：
--
通讯作者：
D. Cheriton
D. Cheriton
中科院分区：
--
文献类型：
--
作者：
Nomair A. Naeem;Ondřej Lhoták;D. Cheriton

文献摘要

被引文献

相似文献

本文扩展了静态typestate分析的时间规范组的相互作用的对象，这是使用tracematches表示。与typestate不同，跟踪匹配状态可能会因跟踪匹配绑定的一组对象中的任何一个上的操作而更改。本文提出了一个基于格的操作语义相当于原来的tracematch语义，但更适合于静态分析。本文定义了一个静态分析，计算精确的本地点集，并跟踪各个对象的流，从而使强大的状态更新的tracematch状态。分析已被证明在语义方面是合理的。一个上下文敏感的版本的分析已实施的IFDS和IDE算法的实例。在早期工作中使用的tracematches的分析进行了评估，发现是非常精确的。通过对来自堆的引用和异常控制流进行更精确的建模，可以消除剩余的不精确性。
This paper extends static typestate analysis to temporal specifications of groups of interacting objects, which are expressed using tracematches. Unlike typestate, a tracematch state may change due to operations on any of a set of objects bound by the tracematch. The paper proposes a lattice-based operational semantics equivalent to the original tracematch semantics but better suited to static analysis. The paper defines a static analysis that computes precise local points-to sets and tracks the flow of individual objects, thereby enabling strong state updates of the tracematch state. The analysis has been proved sound with respect to the semantics. A context-sensitive version of the analysis has been implemented as instances of the IFDS and IDE algorithms. The analysis was evaluated on tracematches used in earlier work and found to be very precise. Remaining imprecisions could be eliminated with more precise modeling of references from the heap and of exceptional control flow.