一种基于抽象解释和模型验证的运行时错误分析方法

摘要

一种基于抽象解释和模型验证的运行时错误分析方法，本发明包括以下步骤：基于抽象解释理论，采用前向迭代方法分析程序数值变量值范围，获得程序点达到稳定时的变量值范围信息，对于循环节点的迭代计算采用循环展开和延迟拓宽相结合的方法实现；根据待分析的运行时错误类型，在相关需要检测的程序点处将变量值范围信息转化为断言或假设形式插入程序中；将带有断言和假设的程序转化为布尔公式，其中布尔公式包括限制条件和属性；使用SAT验证器判断布尔公式中属性的正确性。若正确，说明不存在相关运行时错误；若不正确，说明存在相关运行时错误，并输出相关的反例路径。本发明实现了在运行时错误分析精度和效率之间取得一个平衡点。

主权项

一种基于抽象解释和模型验证的运行时错误分析方法，其特征在于包括以下步骤：（1）构造待分析程序的控制流图；（2）从该控制流图的入口点开始，根据控制流图的迁移方向利用区间域基本操作计算程序中各节点处的变量值范围；（3）当程序中各节点的变量值范围稳定时，变量值范围计算终止，所述变量值范围计算过程采用迭代计算的方法计算程序中出现的循环节点；（4）根据待分析的运行时错误类型，在待分析程序中需要检测的节点处将变量值范围信息转化为断言或假设并插入程序中；所述的运行时错误类型包括除零操作、数组越界、负数开偶次方和数值溢出；（5）将步骤（4）中带有断言和假设的程序转化为布尔公式，所述的布尔公式包括限制条件和属性，其中限制条件为程序的各赋值语句和假设，属性为断言；（6）利用SAT验证器判断步骤（5）中布尔公式中属性的正确性，若验证正确，则进入步骤（7），否则说明存在该类运行时错误并提供相关的反例路径；（7）说明不存在该类运行时错误，结束分析过程。