目錄
前言
第1章 源代碼分析概要 1
1.1 基本概念 1
1.1.1 源代碼 1
1.1.2 源代碼分析 1
1.1.3 分析過(guò)程 2
1.1.4 源代碼建模 2
1.2 語(yǔ)法與語(yǔ)義分析 4
1.2.1 語(yǔ)法分析 4
1.2.2 抽象語(yǔ)法樹(shù) 4
1.2.3 符號(hào)表 5
1.2.4 語(yǔ)義分析 7
1.3 控制流分析 8
1.3.1 控制流圖 9
1.3.2 支配圖 11
1.3.3 依賴(lài)圖 12
1.4 數(shù)據(jù)流分析 13
1.5 源代碼分析常用方法 15
1.6 常用源代碼分析技術(shù) 17
1.6.1 程序的抽象 17
1.6.2 區(qū)間運(yùn)算 18
1.6.3 程序切片計(jì)算 19
1.6.4 路徑計(jì)算 20
1.6.5 約束求解 21
參考文獻(xiàn) 22
第2章 抽象解釋 24
2.1 引言 24
2.2 基本概念 26
2.2.1 格與不動(dòng)點(diǎn)理論 26
2.2.2 伽羅瓦連接 34
2.2.3 Widening/Narrowing算子 38
2.3 程序分析與抽象解釋 40
2.3.1 程序分析的不可判定性 40
2.3.2 程序語(yǔ)義及其不動(dòng)點(diǎn)形 41
2.3.3 抽象解釋中的語(yǔ)義層次體系 43
2.4 抽象解釋?xiě)?yīng)用實(shí)例 45
參考文獻(xiàn) 48
第3章 符號(hào)計(jì)算 50
3.1 簡(jiǎn)介 50
3.2 符號(hào)執(zhí)行技術(shù)的基本原理 50
3.3 符號(hào)執(zhí)行技術(shù)的形式化表達(dá) 52
3.4 符號(hào)執(zhí)行實(shí)現(xiàn)方法 55
3.4.1 靜態(tài)符號(hào)執(zhí)行 55
3.4.2 動(dòng)態(tài)符號(hào)執(zhí)行 56
3.4.3 符號(hào)執(zhí)行技術(shù)總結(jié) 57
3.5 符號(hào)執(zhí)行工具簡(jiǎn)介 58
3.5.1 SPF 58
3.5.2 KLEE 59
3.5.3 SAGE 59
3.5.4 PEX 60
參考文獻(xiàn) 60
第4章 區(qū)間運(yùn)算技術(shù) 63
4.1 經(jīng)典的區(qū)間代數(shù) 63
4.1.1 區(qū)間及區(qū)間運(yùn)算 63
4.1.2 區(qū)間向量和區(qū)間函數(shù) 64
4.2 擴(kuò)展的區(qū)間運(yùn)算 64
4.2.1 數(shù)值型區(qū)間集代數(shù) 64
4.2.2 非數(shù)值型區(qū)間代數(shù) 67
4.2.3 條件表達(dá)式中的區(qū)間計(jì)算 68
4.2.4 基于區(qū)間運(yùn)算的變量值范圍分析 74
4.3 變量的相關(guān)性分析 80
4.3.1 變量間關(guān)聯(lián)關(guān)系的分類(lèi) 80
4.3.2 符號(hào)分析 82
4.4 區(qū)間運(yùn)算在程序分析中的應(yīng)用 90
4.4.1 檢測(cè)矛盾節(jié)點(diǎn) 90
4.4.2 檢測(cè)不可達(dá)路徑 93
4.4.3 提高缺陷檢測(cè)效率 93
參考文獻(xiàn) 95
第5章 路徑敏感分析 97
5.1 概述 97
5.2 路徑不敏感分析方法 97
5.2.1 數(shù)據(jù)流分析 97
5.2.2 四種典型數(shù)據(jù)流問(wèn)題 99
5.2.3 數(shù)據(jù)流分析的理論依據(jù) 109
5.2.4 數(shù)據(jù)流解的含義 109
5.3 路徑敏感分析方法 113
5.3.1 缺陷模式狀態(tài)機(jī) 113
5.3.2 不可達(dá)路徑引入誤報(bào) 116
5.3.3 路徑信息抽象 117
5.3.4 檢測(cè)算法 118
參考文獻(xiàn) 120
第6章 抽象內(nèi)存建模 122
6.1 傳統(tǒng)的程序分析模型 122
6.1.1 二元模型 122
6.1.2 數(shù)組模型 123
6.2 抽象內(nèi)存模型 124
6.2.1 模型定義 125
6.2.2 模型的基本操作 128
6.3 語(yǔ)義模擬算法 129
6.3.1 通用操作符 130
6.3.2 指針 130
6.3.3 數(shù)組 137
6.3.4 結(jié)構(gòu)體 138
6.3.5 字符串 138
6.4 基于抽象內(nèi)存模型的測(cè)試用例生成 142
參考文獻(xiàn) 144
第7章 上下文分析 146
7.1 問(wèn)題分析 146
7.1.1 函數(shù)調(diào)用后影響上下文 146
7.1.2 函數(shù)調(diào)用前約束上下文 148
7.1.3 函數(shù)特征影響上下文 149
7.2 函數(shù)影響 150
7.2.1 函數(shù)影響描述 150
7.2.2 函數(shù)影響生成 150
7.2.3 函數(shù)影響應(yīng)用 152
7.2.4 函數(shù)影響實(shí)驗(yàn) 153
7.3 函數(shù)約束 154
7.3.1 函數(shù)約束描述 154
7.3.2 函數(shù)約束生成 157
7.3.3 函數(shù)約束應(yīng)用 162
7.3.4 函數(shù)約束實(shí)驗(yàn) 163
7.4 函數(shù)特征 164
7.4.1 函數(shù)特征描述 164
7.4.2 函數(shù)特征生成 165
7.4.3 函數(shù)特征實(shí)驗(yàn) 166
參考文獻(xiàn) 168
第8章 程序切片 169
8.1 基本概念 169
8.1.1 程序切片的定義 169
8.1.2 程序切片標(biāo)準(zhǔn) 171
8.2 常見(jiàn)程序切片種類(lèi) 171
8.2.1 靜態(tài)切片 172
8.2.2 動(dòng)態(tài)切片 173
8.2.3 后向切片 174
8.2.4 前向切片 174
8.2.5 準(zhǔn)靜態(tài)切片 175
8.2.6 同步切片 176
8.2.7 條件切片 177
8.2.8 無(wú)定型切片 178
8.2.9 混合切片 179
8.2.10 程序砍片 179
8.3 程序切片計(jì)算方法 180
8.3.1 過(guò)程內(nèi)切片計(jì)算方法 180
8.3.2 過(guò)程間切片計(jì)算方法 183
8.3.3 面向?qū)ο蟮某绦蚯衅��?jì)算方法 185
8.4 程序切片的應(yīng)用 187
8.4.1 軟件質(zhì)量保證 187
8.4.2 軟件維護(hù) 187
8.4.3 軟件度量 188
參考文獻(xiàn) 188
第9章 路徑計(jì)算 192
9.1 路徑生成 192
9.1.1 不包含循環(huán)結(jié)構(gòu)的路徑生成 192
9.1.2 循環(huán)結(jié)構(gòu)路徑生成 194
9.2 路徑可達(dá)性計(jì)算 199
9.2.1 基于矛盾片段模式的路徑可達(dá)性計(jì)算 199
9.2.2 基于優(yōu)化區(qū)間運(yùn)算的路徑可達(dá)性計(jì)算 200
9.2.3 基于等式系數(shù)矩陣的路徑可達(dá)性計(jì)算 208
9.2.4 基于仿射運(yùn)算的路徑可達(dá)性計(jì)算 210
參考文獻(xiàn) 210
第10章 約束求解 212
10.1 求解布爾約束滿(mǎn)足問(wèn)題 212
10.1.1 布爾約束滿(mǎn)足問(wèn)題 212
10.1.2 基礎(chǔ)知識(shí) 213
10.1.3 算法 214
10.1.4 典型的SAT求解器和SMT求解器 216
10.2 求解有限約束滿(mǎn)足問(wèn)題 219
10.2.1 有限約束滿(mǎn)足問(wèn)題 219
10.2.2 回溯法 220
10.2.3 不完備算法-局部搜索法 221
10.3 求解混合約束滿(mǎn)足問(wèn)題 225
10.3.1 混合布爾約束滿(mǎn)足問(wèn)題 225
10.3.2 數(shù)值約束求解算法 225
10.4 基于約束求解的測(cè)試用例自動(dòng)生成 228
10.4.1 常見(jiàn)的測(cè)試用例生成方法 228
10.4.2 基于抽象內(nèi)存模型的分支限界法 237
參考文獻(xiàn) 241
第11章 源代碼分析應(yīng)用 244
11.1 缺陷檢測(cè)系統(tǒng)DTS 244
11.1.1 產(chǎn)品功能 244
11.1.2 產(chǎn)品特色 245
11.1.3 缺陷模式 246
11.1.4 技術(shù)架構(gòu) 247
11.1.5 技術(shù)指標(biāo) 248
11.1.6 使用步驟 248
11.2 代碼測(cè)試系統(tǒng)CTS 255
11.2.1 系統(tǒng)功能 255
11.2.2 操作步驟 257
11.3 其他代碼分析工具 261
11.3.1 Emma 262
11.3.2 C++test 268
11.3.3 Testbed 272