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

2992 Journal of Software 软件学报 Vol.31, No.10, October 2020

函数中继续进行过程内的后向数据流分析.过程间后向数据流分析过程将一直执行,直到待检查语句集合为空
或达到配置的检查深度.
Table 1 Types of statements related to array out-of-bound checking
表 1 数组越界检测相关的语句类型
语句类型 语句模式 简单匹配法 约束求解法
声明语句 Type idx=expr idx=const !(idx==expr→idx<len)
!(idx==expr→idx>=len)
idx=expr%const !(idx==expr→idx<0)
!(idx==expr→idx>=0)
赋值语句 idx=expr ditto ditto
复合赋值语句 idx op=expr idx%=const !(idx 1==idx 0 op expr→idx 1<len)
条件语句 if(expr) idx<const !(expr→idx<len)
idx<=const
idx>const !(expr→idx>0)
idx>=const
for 循环语句 for(…;expr;…) ditto ditto
while 循环语句 while(expr) ditto ditto
算法 1. 数组越界检测算法.
函数:ABChecker(CallGraph,CFG,Depth).
输入:CallGraph,CFG,Depth;
输出:Warnings.
1.for each f in CallGraph
/*in backwards topological order*/
2. bbSet=∅
3. for each BB in CFG off
/*in backwards topological order */
4. for each ArrStmt in BB
5. if T(ArrStmt.idx)==untainted
6. if T(ArrStmt.LenSet)==tainted
7. Warnings.add(ArrStmt)
8. else
9. for each Len in ArrStmt.LenSet
10. if ArrStmt.idx>=Len
11. Warnings.add(ArrStmt)
12. break
13. else
14. OutState[BB].add(ArrStmt)
15. if OutState[BB]≠∅
16. bbSet.add(all predecessors of BB)
17. ABCSet=intraABChecker(bbSet,OutState)
18. if ABCSet≠∅
19. result=interABChecker(ABCSet,f,Depth−1)
20. Warnings.add(all ArrStmt in result)
函数:intraABChecker(bbSet,OutState).
1.while bbSet≠∅
2. BB=bbSet.pop()