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