目前,源代碼分析是軟件工程領域的必備方法之一,有著強烈的工程需求和實用價值,已成為國際學術界和工業(yè)界的一個熱點。本書從源代碼分析的基本概念開始,將其中所涉及的重要的技術和應用——抽象解釋、符號計算、區(qū)間運算、路徑敏感分析、抽象內存建模、上下文分析、程序切片、路徑計算和約束求解等,結合大量的實例進行由淺入深的介紹和講解;同時,在本書的*后專門介紹應用源代碼分析技術所研發(fā)的一些常用測試工具,并重點介紹兩款靜態(tài)分析工具——DTS、CTS。
更多科學出版社服務,請掃碼獲取。
目錄
前言
第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ù)據流分析 13
1.5 源代碼分析常用方法 15
1.6 常用源代碼分析技術 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 抽象解釋應用實例 45
參考文獻 48
第3章 符號計算 50
3.1 簡介 50
3.2 符號執(zhí)行技術的基本原理 50
3.3 符號執(zhí)行技術的形式化表達 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í)行技術總結 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ū)間運算技術 63
4.1 經典的區(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 變量的相關性分析 80
4.3.1 變量間關聯(lián)關系的分類 80
4.3.2 符號分析 82
4.4 區(qū)間運算在程序分析中的應用 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ù)據流分析 97
5.2.2 四種典型數(shù)據流問題 99
5.2.3 數(shù)據流分析的理論依據 109
5.2.4 數(shù)據流解的含義 109
5.3 路徑敏感分析方法 113
5.3.1 缺陷模式狀態(tài)機 113
5.3.2 不可達路徑引入誤報 116
5.3.3 路徑信息抽象 117
5.3.4 檢測算法 118
參考文獻 120
第6章 抽象內存建模 122
6.1 傳統(tǒng)的程序分析模型 122
6.1.1 二元模型 122
6.1.2 數(shù)組模型 123
6.2 抽象內存模型 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 結構體 138
6.3.5 字符串 138
6.4 基于抽象內存模型的測試用例生成 142
參考文獻 144
第7章 上下文分析 146
7.1 問題分析 146
7.1.1 函數(shù)調用后影響上下文 146
7.1.2 函數(shù)調用前約束上下文 148
7.1.3 函數(shù)特征影響上下文 149
7.2 函數(shù)影響 150
7.2.1 函數(shù)影響描述 150
7.2.2 函數(shù)影響生成 150
7.2.3 函數(shù)影響應用 152
7.2.4 函數(shù)影響實驗 153
7.3 函數(shù)約束 154
7.3.1 函數(shù)約束描述 154
7.3.2 函數(shù)約束生成 157
7.3.3 函數(shù)約束應用 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 過程內切片計算方法 180
8.3.2 過程間切片計算方法 183
8.3.3 面向對象的程序切片計算方法 185
8.4 程序切片的應用 187
8.4.1 軟件質量保證 187
8.4.2 軟件維護 187
8.4.3 軟件度量 188
參考文獻 188
第9章 路徑計算 192
9.1 路徑生成 192
9.1.1 不包含循環(huán)結構的路徑生成 192
9.1.2 循環(huán)結構路徑生成 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 基礎知識 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 基于抽象內存模型的分支限界法 237
參考文獻 241
第11章 源代碼分析應用 244
11.1 缺陷檢測系統(tǒng)DTS 244
11.1.1 產品功能 244
11.1.2 產品特色 245
11.1.3 缺陷模式 246
11.1.4 技術架構 247
11.1.5 技術指標 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