论现代命令式语言的通用静态分析器设计

为现代命令式语言（如 C、C++、Java 和 Python）的重要片段设计和实现精确的静态分析器是一个具有挑战性的问题。在本文中，我们考虑一种核心命令式语言，它具有主流语言中的若干特性，例如递归函数、运行时系统和用户自定义异常，以及现实的数据和内存模型。对于这种语言，我们提供了具体语义——表征有限和无限计算——以及一个通用的抽象语义，并证明了其相对于具体语义的可靠性。我们说抽象语义是通用的，因为它的设计在分析域上是完全参数化的：特别是，它提供了对关系域（即可以捕获不同数据对象之间关系的抽象域）的支持。我们还概述了如何扩展所提出的方法以适应包含指针、复合数据对象和非结构化控制流机制的更大语言。该方法基于结构化的大步 $\mathrm{G}^\infty\mathrm{SOS}$ 操作语义和抽象解释，具有模块化特性，因为整个静态分析器自然地被划分为具有明确职责和接口的组件，这极大地简化了正确性证明和实现。