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

高凤娟 等:基于污点分析的数组越界缺陷的静态检测方法 2993

3. for each succ of BB
4. OutState[BB]+=InState[succ]
5. InState[BB]=∅
6. for each stmt in BB
7. checkStmt(stmt, &OutState[BB])
8. if OutState[BB]≠InState BB
9. InState[BB]=OutState[BB]
10. bbSet.add(all predecessors of BB)
11. ABCSet=OutState[BB]
12.return ABCSet
函数:checkStmt(stmt,OutState[BB]).
1.for each ABC in OutState[BB]
2. if imply(stmt, ArrStmt.idx,less,0)
3. Warnings.add(ABC)
4. OutState[BB].remove(ABC,low)
5. else if imply(stmt,ArrStmt.idx,notless,0)
6. OutState[BB].remove(ABC,low)
7. for each len in ArrStmt.LenSet
8. if imply(stmt,ArrStmt.idx,less,len)
9. cnt++
10. else if imply(stmt,ArrStmt.idx,notless,len)
11. Warnings.add(ABC)
12. OutState[BB].remove(ABC,up)
13. break
14. if cnt==ArrStmt.LenSet.size()
15. OutState[BB].remove(ABC,up)
函数:interABChecker(ABCSet,f,Depth).
1.if Depth<=0 or ABCSet==∅
2. return ABCSet
3.result=∅
4.for each caller off
5. bbSet=∅
6. bbSet.add(caller.callsite.BB)
7. OutState[callerBB]=update(ABCSet)
8. set=intraABChecker(bbSet,OutState)
9. set2=interABChecker(set,caller,Depth−1)
10. result+=set2
11.return result
如算法 1 中函数 checkStmt 所示,在数据流分析过程中,对于遇到的每一条语句 stmt,将根据表 1 和判定规则
3 进行处理.如果分析到一条语句可使公式(8)中的条件 A 或条件 E 满足,则后续数据流分析中不再关注 A、C、
E;如果分析到一条语句可使公式(8)中的条件 B 或条件 F 满足,则在后向数据流分析过程中不再关注 B、D、F.
在后向数据流分析过程中,主要关注与数组下标相关的语句,如表 1 的前两列所示,主要包括包含该数组下标的