利用SMT求解实现更强大的常量值检查

中文摘要 AI 辅助

可插拔类型系统通过引入额外的类型层次来指定变量之间更复杂的属性和依赖关系，从而扩展编程语言的基本类型系统。我们考虑常量值检查器（Constant Value Checker），这是一个使用Checker Framework实现的Java可插拔类型检查器，该框架提供了各种可插拔类型系统及相应的检查器。常量值检查器允许用户使用常量值的集合或范围来限制基本整数或布尔变量可以持有的值。然而，当前的值检查器（Value Checker）实现使用了一组有限的语法类型规则，在实践中，这些规则往往无法验证更复杂代码的类型正确性。在本文中，我们介绍了一种对Checker Framework的扩展，使用可满足性模理论（Satisfiability Modulo Theories，SMT）求解器来解决这些限制，方法是为那些在当前语法类型规则下类型检查失败的表达式创建相应的一阶逻辑公式，并根据这些公式的可满足性来确定其类型正确性。此外，我们引入了新的依赖类型，用于通过可以依赖于程序中其他变量的表达式来指定允许的值。

英文摘要

Pluggable type systems extend the basic type system of a programming language by introducing additional type hierarchies to specify more complex properties and dependencies between variables. We consider the Constant Value Checker, a pluggable type checker for Java implemented using the Checker Framework, which provides various pluggable type systems and corresponding checkers. The Constant Value Checker lets users specify restrictions on the values a primitive integer or boolean variable can hold using a set or range of constant values. However, the current implementation of the Value Checker makes use of a limited set of syntactic typing rules that, in practice, often fail to verify well-typedness of more complex code. In this paper, we introduce an extension to the Checker Framework using Satisfiability Modulo Theories (SMT) solvers to address these limitations by creating corresponding first-order logic formulas for expressions whose type checks fail with the current syntactic typing rules and determining their well-typedness based on the satisfiability of these formulas. Furthermore, we introduce new dependent types for specifying allowed values with expressions that can depend on other variables in the program.

发表机构

• Institute of Information Security and Dependability (KASTEL), Karlsruhe Institute of Technology（卡尔斯鲁厄理工学院信息安全与可靠性研究所（KASTEL））

机构由 AI 辅助整理，请以论文原文为准。