没有合适的资源?快使用搜索试试~ 我知道了~
资源推荐
资源详情
资源评论
Static Program Analysis
Anders Møller and Michael I. Schwartzbach
February 10, 2022
Copyright © 2008–2021 Anders Møller and Michael I. Schwartzbach
Department of Computer Science
Aarhus University, Denmark
This work is licensed under the Creative Commons Attribution-NonCommercial-
NoDerivatives 4.0 International License. To view a copy of this license, visit
http://creativecommons.org/licenses/by-nc-nd/4.0/.
Contents
Preface v
1 Introduction 1
1.1 Applications of Static Program Analysis . . . . . . . . . . . . . . 1
1.2 Approximative Answers . . . . . . . . . . . . . . . . . . . . . . . 3
1.3 Undecidability of Program Correctness . . . . . . . . . . . . . . 6
2 A Tiny Imperative Programming Language 9
2.1 The Syntax of TIP . . . . . . . . . . . . . . . . . . . . . . . . . . . 9
2.2 Example Programs . . . . . . . . . . . . . . . . . . . . . . . . . . 13
2.3 Normalization . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 14
2.4 Abstract Syntax Trees . . . . . . . . . . . . . . . . . . . . . . . . . 15
2.5 Control Flow Graphs . . . . . . . . . . . . . . . . . . . . . . . . . 16
3 Type Analysis 19
3.1 Types . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 20
3.2 Type Constraints . . . . . . . . . . . . . . . . . . . . . . . . . . . 22
3.3 Solving Constraints with Unification . . . . . . . . . . . . . . . . 25
3.4 Record Types . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
3.5 Limitations of the Type Analysis . . . . . . . . . . . . . . . . . . 33
4 Lattice Theory 37
4.1 Motivating Example: Sign Analysis . . . . . . . . . . . . . . . . . 37
4.2 Lattices . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38
4.3 Constructing Lattices . . . . . . . . . . . . . . . . . . . . . . . . . 41
4.4 Equations, Monotonicity, and Fixed Points . . . . . . . . . . . . . 43
5 Dataflow Analysis with Monotone Frameworks 51
5.1 Sign Analysis, Revisited . . . . . . . . . . . . . . . . . . . . . . . 52
5.2 Constant Propagation Analysis . . . . . . . . . . . . . . . . . . . 57
5.3 Fixed-Point Algorithms . . . . . . . . . . . . . . . . . . . . . . . . 58
i
ii CONTENTS
5.4 Live Variables Analysis . . . . . . . . . . . . . . . . . . . . . . . . 62
5.5 Available Expressions Analysis . . . . . . . . . . . . . . . . . . . 66
5.6 Very Busy Expressions Analysis . . . . . . . . . . . . . . . . . . . 70
5.7 Reaching Definitions Analysis . . . . . . . . . . . . . . . . . . . . 71
5.8 Forward, Backward, May, and Must . . . . . . . . . . . . . . . . 72
5.9 Initialized Variables Analysis . . . . . . . . . . . . . . . . . . . . 75
5.10 Transfer Functions . . . . . . . . . . . . . . . . . . . . . . . . . . 76
6 Widening 79
6.1 Interval Analysis . . . . . . . . . . . . . . . . . . . . . . . . . . . 79
6.2 Widening and Narrowing . . . . . . . . . . . . . . . . . . . . . . 82
7 Path Sensitivity and Relational Analysis 89
7.1 Control Sensitivity using Assertions . . . . . . . . . . . . . . . . 90
7.2 Paths and Relations . . . . . . . . . . . . . . . . . . . . . . . . . . 91
8 Interprocedural Analysis 99
8.1 Interprocedural Control Flow Graphs . . . . . . . . . . . . . . . 99
8.2 Context Sensitivity . . . . . . . . . . . . . . . . . . . . . . . . . . 103
8.3 Context Sensitivity with Call Strings . . . . . . . . . . . . . . . . 104
8.4 Context Sensitivity with the Functional Approach . . . . . . . . . 107
9 Control Flow Analysis 111
9.1 Closure Analysis for the λ-calculus . . . . . . . . . . . . . . . . . 111
9.2 The Cubic Algorithm . . . . . . . . . . . . . . . . . . . . . . . . . 114
9.3 TIP with First-Class Function . . . . . . . . . . . . . . . . . . . . 116
9.4 Control Flow in Object Oriented Languages . . . . . . . . . . . . 120
10 Pointer Analysis 123
10.1 Allocation-Site Abstraction . . . . . . . . . . . . . . . . . . . . . . 123
10.2 Andersen’s Algorithm . . . . . . . . . . . . . . . . . . . . . . . . 124
10.3 Steensgaard’s Algorithm . . . . . . . . . . . . . . . . . . . . . . . 129
10.4 Interprocedural Pointer Analysis . . . . . . . . . . . . . . . . . . 131
10.5 Null Pointer Analysis . . . . . . . . . . . . . . . . . . . . . . . . . 132
10.6 Flow-Sensitive Pointer Analysis . . . . . . . . . . . . . . . . . . . 135
10.7 Escape Analysis . . . . . . . . . . . . . . . . . . . . . . . . . . . . 137
11 Abstract Interpretation 139
11.1 A Collecting Semantics for TIP . . . . . . . . . . . . . . . . . . . 139
11.2 Abstraction and Concretization . . . . . . . . . . . . . . . . . . . 145
11.3 Soundness . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 152
11.4 Optimality . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 158
11.5 Completeness . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 160
11.6 Trace Semantics . . . . . . . . . . . . . . . . . . . . . . . . . . . . 166
Index of Notation 171
剩余184页未读,继续阅读
资源评论
- 刘林旭2023-08-01感谢资源主的分享,这个资源对我来说很有用,内容描述详尽,值得借鉴。
manok
- 粉丝: 2386
- 资源: 20
下载权益
C知道特权
VIP文章
课程特权
开通VIP
上传资源 快速赚钱
- 我的内容管理 展开
- 我的资源 快来上传第一个资源
- 我的收益 登录查看自己的收益
- 我的积分 登录查看自己的积分
- 我的C币 登录后查看C币余额
- 我的收藏
- 我的下载
- 下载帮助
安全验证
文档复制为VIP权益,开通VIP直接复制
信息提交成功