数据流精化类型推断
Data Flow Refinement Type Inference
摘要：
精化类型支持函数程序的轻量级验证。用于静态推断细化类型的算法通常通过简化到求解从类型化派生中提取的受约束Horn子句的系统来工作。一个例子是Liquid类型推断，它使用谓词抽象来解决提取的约束。然而，约束求解本身的简化已经意味着影响整体静态分析精度的程序语义的抽象。为了更好地理解这个问题，我们通过抽象解释的视角来整体研究类型推断问题。我们提出了一个新的细化类型系统，是参数的类型细化的抽象域的选择，以及它跟踪上下文敏感的控制流信息的程度。然后，我们推导出一个伴随的参数推理算法作为一个抽象的解释一个新的数据流语义的功能程序。我们进一步表明，类型系统是健全的和完整的构造抽象语义。我们的理论发展揭示了细化类型推断算法中固有的关键抽象步骤。这些抽象步骤的精度和效率之间的权衡由类型系统的参数控制。现有的精化类型系统及其相应的推理算法，如Liquid类型，都是通过具体的参数实例化来捕获的。我们已经在一个原型工具中实现了我们的框架，并针对一系列新的参数实例（例如，使用八边形和多面体来表示类型细化）。该工具与其他现有工具相比毫不逊色。我们的评估表明，我们的方法可以用来系统地构建新的细化类型推断算法，是强大的和精确的。
英文摘要：
Refinement types enable lightweight verification of functional programs. Algorithms for statically inferring refinement types typically work by reduction to solving systems of constrained Horn clauses extracted from typing derivations. An example is Liquid type inference, which solves the extracted constraints using predicate abstraction. However, the reduction to constraint solving in itself already signifies an abstraction of the program semantics that affects the precision of the overall static analysis. To better understand this issue, we study the type inference problem in its entirety through the lens of abstract interpretation. We propose a new refinement type system that is parametric with the choice of the abstract domain of type refinements as well as the degree to which it tracks context-sensitive control flow information. We then derive an accompanying parametric inference algorithm as an abstract interpretation of a novel data flow semantics of functional programs. We further show that the type system is sound and complete with respect to the constructed abstract semantics. Our theoretical development reveals the key abstraction steps inherent in refinement type inference algorithms. The trade-off between precision and efficiency of these abstraction steps is controlled by the parameters of the type system. Existing refinement type systems and their respective inference algorithms, such as Liquid types, are captured by concrete parameter instantiations. We have implemented our framework in a prototype tool and evaluated it for a range of new parameter instantiations (e.g., using octagons and polyhedra for expressing type refinements). The tool compares favorably against other existing tools. Our evaluation indicates that our approach can be used to systematically construct new refinement type inference algorithms that are both robust and precise.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
