无需量词消去的传递函数合成

传统上，程序中的传递函数是逐条指令手动设计的。在此设定下，传递函数描述单条指令的语义，详述给定的抽象输入状态如何映射到抽象输出状态。随后，可通过组合构成指令的传递函数来计算指令序列（即基本块）的净效应。然而，若应用单个传递函数来捕捉整个块的语义，则可提高精度。由于基本块依赖于具体程序，这种方法需要自动化实现。因此，自动计算传递函数日益受到关注，其中最显著的是基于量词消去的技术。尽管概念上优雅，但量词消去不可避免地会导致计算瓶颈，从而将这些方法的适用范围限制在小型基本块上。本文提出了一种完全规避量词消去的传递函数计算方法，可视为对该问题的回应。该方法通过为线性模板约束（包括区间和八边形）描述的输入和输出状态生成传递函数，展示了其实用性。