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

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

变式.
在进行中断驱动程序顺序化之前,基于抽象解释采用数值区间抽象域对函数 ISR i Proc 进行迭代分析,计算
出 ISR i 上各干扰变量值区间不变式后,生成中断函数摘要.当遇到中断函数触发时,用计算得到的中断函数摘要
替代原中断函数.这样不仅能降低分析复杂度,而且能避免对中断函数调用进行多次迭代分析,提高分析性能.
2.3.3 中断驱动程序顺序化方法
中断驱动程序顺序化 [12] 是指将中断驱动程序转换为可靠的非确定的顺序化程序,即保证转化后的程序行
为是原中断驱动程序在实际执行时的一个上近似.
本文基于中断函数摘要机制给出面向整数溢出检测的中断驱动程序顺序化方法,具体步骤如下.
 步骤 1:对程序 P 以及中断向量号为 i 的中断 ISR i (i<N)进行干扰变量分析,在分析过程中,记录干扰变量
st
st
st
st
st
信息v ,st,loc ,vec,简称 interf ,其中,v 为语句 st 上的干扰变量,st 为 P 上使用 v 的语句,loc 为 P 中的
语句 st 位置,vec 为 ISR i 对应的中断向量号;
 步骤 2:对中断 ISR i 分别进行抽象解释迭代分析,求解干扰变量值区间不变式,生成函数摘要.其中,函数
摘要中的中断向量号为 i,中断 ISR i 上的干扰变量集合已在步骤 1 中求得;
st
 步骤 3:将相应的干扰变量信息插入到程序的语句块中.本文引入函数 Trigger(st,interf )用于将中断函
数摘要插入到对应语句之前;同时,引入干扰位置变量 Loc i 和中断触发标志变量 Rand i .其中,变量 Loc i
和 Rand i 的个数等于程序中干扰中断的数量,下标 i 表示干扰中断对应的中断向量号.Loc i 表示受中断
st
st
st
影响的语句位置集合,取值范围为{interf .loc |interf .ver==i},用于保证同一中断在主程序一次循环过
程中只执行一次;Rand i 表示中断触发标志集合,取值范围为{0,1},用于表征中断在干扰位置前是否触
st
st
发.在中断驱动程序顺序化过程中,对 interf 中的每条语句 st 前显式地加入 Trigger(st,interf )函数,假
st
设程序 P 由语句 st 1 ,st 2 ,st i ,…,st n 组成,语句 st i 为 interf 中的一条语句,则顺序化后的程序为 st st st ,...,
,
,
1 2 i
st n ,其中, st 定义如下: st  Trigger (,st interf st ); .st
i i
下面给出 Trigger 函数执行框架,输入为待插入的语句 st 以及经步骤 1 干扰变量分析后得到的干扰变量信
st
息 interf .
st
Trigger(st,interf )
1 begin
2 flag vec :=true
st
st
st
3 for each v ,st,loc ,vec in interf do
st
st
4 if Loc i =interf .loc and Rand i =1 and flag vec =true then
5 flag vec :=false
6 insert summary(ISR vec ) before st
7 endif
8 endfor
9 end
st
上述执行框架首先对语句 st 中的干扰变量进行遍历,并根据干扰变量信息 interf 找到该干扰变量对应的
干扰中断 ISR vec ;然后,将干扰中断函数摘要插入到语句 st 之前,完成顺序化操作.在主程序一次循环执行过程中,
该执行框架考虑了同一干扰中断最多触发一次以及不同干扰中断可以同时触发的情况,能够确保转化后程序
行为的可靠性.
图 10 给出了一个中断驱动程序顺序化示例.图 10(a)中的中断驱动程序包含 1 个主程序和 1 个中断 ISR 0 ,
以及 1 个全局变量 interfval,主程序在第 7 行~第 11 行间禁止中断 ISR 0 的触发.若不考虑中断函数触发,则主程
序运行至第 9 行时,被减数 firstval 取值为 2,减数 interfval 取值为 1,因此,两个无符号整数相减后未引起整数溢
出;若考虑中断触发,即在主程序第 6 行、第 7 行之间发生中断 ISR 0 ,则减数 interfval 被重新赋值为 3,主程序运
行至第 9 行时发生无符号整数减溢出错误.综上,图 10(a)所示中断驱动程序存在整数溢出错误.