程序分析原理

前言

第1章 概述1
1.1什麼是程式分析1
1.2設置場景2
1.3資料流程分析3
1.3.1等式方法3
1.3.2基於約束的方法5
1.4基於約束的分析6
1.5抽象解釋8
1.6類型和作用系統11
1.6.1注釋類型系統12
1.6.2作用系統14
1.7演算法16
1.8程式轉換17
結束語18
迷你項目18
練習20

第2章資料流程分析22
2.1過程內資料流程分析22
2.1.1可用運算式分析24
2.1.2到達定值分析26
2.1.3很忙的運算式分析29
2.1.4活躍變數分析31
2.1.5派生資料流程資訊33
2.2理論性質34
2.2.1結構操作語義34
2.2.2活躍變數分析的正確性38
2.3單調框架41
2.3.1基本定義43
2.3.2案例回顧44
2.3.3一個不可分配的例子46
2.4等式系統的求解47
2.4.1MFP解47
2.4.2MOP解50
2.5過程間分析53
2.5.1結構操作語義55
2.5.2過程內分析與過程間分析56
2.5.3顯式使用上下文58
2.5.4調用字串作為上下文61
2.5.5假設集作為上下文63
2.5.6流敏感與流不敏感64
2.6形狀分析66
2.6.1結構操作語義67
2.6.2形狀圖70
2.6.3分析的描述73
結束語82
迷你項目84
練習86

第3章基於約束的分析90
3.1抽象0CFA分析90
3.1.1分析的描述91
3.1.2分析的明確定義96
3.2理論性質97
3.2.1結構操作語義98
3.2.2語義正確性101
3.2.3解的存在性104
3.2.4餘歸納和歸納的比較106
3.3語法引導的0CFA分析108
3.3.1語法引導的規範108
3.3.2解的保持110
3.4基於約束的0CFA分析111
3.4.1解的保持113
3.4.2約束的求解113
3.5添加資料流程分析117
3.5.1抽象值為冪集117
3.5.2抽象值為完全格119
3.6添加上下文信息122
3.6.1均勻kCFA分析123
3.6.2笛卡兒積演算法127
結束語128
迷你項目130
練習132

第4章抽象解釋135
4.1一種普通的正確性定義135
4.1.1正確性關係136
4.1.2表示函數138
4.1.3一個較小的擴展139
4.2不動點的近似141
4.2.1加寬運算元143
4.2.2變窄運算元146
4.3Galois連接149
4.3.1Galois連接的性質152
4.3.2Galois插入155
4.4Galois連接的系統的設計方法157
4.4.1元件上的組合159
4.4.2其他組合方式162
4.5衍生的操作165
4.5.1沿著抽象化函數衍生165
4.5.2資料流程分析中的應用168
4.5.3沿著具體化函數衍生171
結束語174
迷你項目176
練習177

第5章類型和作用系統182
5.1控制流分析182
5.1.1底層類型系統183
5.1.2基於類型的分析184
5.2理論性質187
5.2.1自然語義187
5.2.2語義正確性189
5.2.3解的存在性191
5.3類型推導演算法193
5.3.1一個底層類型系統的演算法193
5.3.2一個控制流分析的演算法196
5.3.3語法可靠性和完備性200
5.3.4解的存在性204
5.4作用205
5.4.1副作用分析206
5.4.2異常分析210
5.4.3區域推導213
5.5行為219
5.5.1通信分析219
結束語225
迷你項目228
練習231

第6章演算法234
6.1工作清單演算法234
6.1.1工作清單演算法的結構235
6.1.2LIFO和FIFO反覆運算238
6.2逆後序反覆運算239
6.2.1迴圈演算法242
6.3在強分量裡反覆運算243
結束語245
迷你項目247
練習248

附錄A偏序集合250
附錄B歸納和餘歸納258
附錄C圖和規則運算式265
參考文獻272
符號索引283
術語索引287