compiler-construction - 约束求解器在编程语言和编译器中的使用

Question

任何或多或少实用的编程语言和编译器都必须处理约束。最常见的约束是类型。通常类型派生和统一是通过一个简单的算法(例如 Hindley-Milner )完成的，最终程序中的所有术语都被分配了唯一的类型。如果没有发生，则有错误指示。

编译器中可能存在更复杂的约束，其中不可能完全统一并且解决方案仅在某些限制下存在。可能的例子是

数据流分析。仿射等式约束的解可用于循环向量化。

内存管理。如果我们对引用和数据访问模式有一些限制，编译器可以从优化引用计数和垃圾收集中受益。

另一方面，约束求解器，如 Z3 或 Yices，在为不同类型的约束寻找可满足的模型方面非常强大。

我正在寻找关于编译器如何从 SMT 求解器的强大功能中受益以及它们正在解决什么样的任务的成功案例。我列出了一些领域，但我没有找到任何具体的例子。你能提出任何建议吗？

Answer 1

SMT 求解器通常用于实现需要大量静态验证的编程语言。例如，使用依赖类型、细化类型或静态强制合约的语言通常使用 SMT 求解器。

例如 Liquid Haskell以及微软的 Dafny和 Chalice都用Z3。其他语言，如 ATS或 Whiley ，实现了自己的求解器。