Page 10 - 《软件学报》2021年第10期

2982 Journal of Software 软件学报 Vol.32, No.10, October 2021

中断驱动
程序顺序化 航天嵌入式软件

语法解析& CFG 转换为静态
循环展开 单赋值形式

程序模型 约简 约简的
约简方法 程序模型

整数溢出性质 插入 逻辑公式

SMT
满足 求解器求解 不满足

存在反例 在界限k之内不存在
程序错误 整数溢出错误
Fig.6 Basic framework of the bounded model checking for integer overflow
图 6 整数溢出有界模型检测基本框架

2.2 基于整数溢出变量依赖的程序模型约简技术
在有界模型检测中,通过对源程序进行语法分析、循环和递归按 k 边界展开、控制流分析,最终产生一种中
间表示,称为静态单赋值形式 SSA.在 SSA 形式中,任何变量只在一个语句中被定义,且对变量的任何使用都只
有一个到达定值.在构建逻辑公式的过程中,会将 SSA 形式下的所有语句进行合取操作,得到程序的约束条件
C,将待验证的整数溢出断言语句转换为性质集合 P,用于 SMT 求解器求解.随着程序规模的扩大,约束条件 C 将
变得异常复杂,使得求解效率大幅降低.
本文根据整数溢出变量的特点对程序约束条件进行约简,使得最终得到的约束条件 C simp 中不包含与整数
溢出性质无关的语句.下面给出相应的程序模型约简算法.
1 算法. 程序模型约简算法.
2 输入:SSA 中间表示语句集合 S、整数溢出断言语句 assert、整数溢出断言语句位置 locs;
3 输出:程序约束条件 C simp .
4 Worklist:={}
5 C simp :=
6 foreach variable v used in assert do
7 Worklist:=Worklist{v}
8 line:=locs
9 repeat
10 line:=line1
11 if variable v defined in S[line]Worklist then
12 delete v from Worklist
13 C simp :=C simp {S[line]}
14 if v is defined by a constant then
15 continue
16 foreach variable u used in S[line] do
17 Worklist:=Worklist{u}