Accumulation Analysis
Accumulation Analysis
复制标题
DOI：
10.4230/lipics.ecoop.2022.10
复制
发表时间：
2022
期刊：
影响因子：
--
通讯作者：
Martin Kellogg;Narges Shadab;Manu Sridharan;Michael D. Ernst
中科院分区：
文献类型：
--
作者：
Martin Kellogg;Narges Shadab;Manu Sridharan;Michael D. Ernst
10一个typestate specification指明了对象的哪些行为在11个对象的状态中被允许。在一般情况下，正确地检查类型状态规范需要关于别名的精确信息（即，别名或指针分析），这在计算上是昂贵的。[13]这一要求妨碍了在实践中采用健全的类型状态分析。[14]这篇论文识别了累积类型状态规范，它是类型状态规范的子集，可以在没有任何关于别名的信息的情况下进行可靠的检查。一个累加16的类型状态规范可以通过累加分析来检查：一个简单的，快速的数据流17分析，保守地近似于对一个对象执行的操作。[18]本文形式化了积累分析和积累类型状态规范的概念。它证明了累积类型状态规范正是那些可以在没有混叠信息的情况下进行可靠检查的类型状态规范。此外，研究文献中出现的41%的类型状态规范21是累积类型状态规范。22、国家科学
10 A typestate specification indicates which behaviors of an object are permitted in each of the 11 object’s states. In the general case, soundly checking a typestate specification requires precise 12 information about aliasing (i.e., an alias or pointer analysis), which is computationally expensive. 13 This requirement has hindered the adoption of sound typestate analyses in practice. 14 This paper identifies accumulation typestate specifications , which are the subset of typestate 15 specifications that can be soundly checked without any information about aliasing. An accumulation 16 typestate specification can be checked instead by an accumulation analysis: a simple, fast dataflow 17 analysis that conservatively approximates the operations that have been performed on an object. 18 This paper formalizes the notions of accumulation analysis and accumulation typestate specifica- 19 tion. It proves that accumulation typestate specifications are exactly those typestate specifications 20 that can be checked soundly without aliasing information. Further, 41% of the typestate specifications 21 that appear in the research literature are accumulation typestate specifications. 22 in National Science