程序分析原理

本书的写作目的
我们写这本书有两个目的：一是很长时间以来我们缺乏用于教授程序分析课程的教材，这迫使我们使用会议论文、期刊和已绝版的教科书的章节来替代；二是我们越来越感觉到研究人员在该领域的不同分支研究类似的问题时，没有充分意识到其他分支已有的领悟和发展。这促使我们撰写一本不但对程序分析的高级课程有用，而且能提高对该领域不同技术路线相似性的认识的教材。
我们可以用计算复杂性理论做个比喻。假设研究人员或学生想通过查阅文献寻找解决图问题的巧妙算法或启发式方法。他们可能会碰到描述解决布尔公式问题的巧妙算法或启发式方法的文献。或许他们会忽略这些文献，认为图和布尔公式显然是完全不同的东西。然而复杂性理论告诉我们这是一个错误的观点。不同问题之间的log空间规约关系和NP完全问题的概念让我们意识到表面上不相关的问题实际上可能密切相关，以至于某个问题的巧妙算法或启发式方法可能引向另一个问题的算法或启发式方法。我们认为，学习程序语言的学生，特别是学习程序分析的学生经常被允许做出类似的幼稚决定，这是一个令人悲哀的事实。程序分析理论还远远不能将不同技术路线的想法准确而密切地联系在一起，但我们希望这本书可以是一个开始。事实上，我们希望令一些读者感到震惊，让他们发现自己在工作中使用的方法与看似不相关的方法之间有重要的相似性。
本书的重点是（我们认为的）程序分析的四个主要方法：数据流分析、基于约束的分析、抽象解释、类型和作用系统。对于每种方法，我们的目标是鉴别和描述主要技术原理，而不是提供一个分析方法和程序语言构造的“宝典”。我们希望告诉读者如何把基本原理用于更复杂的程序语言和分析。
因此，我们特意决定不涵盖一些很有意思的方法，包括作者非常喜爱的方法，以保留篇幅来对这四种主要方法做比较深入的阐述。本书没有介绍的方法包括基于指称的程序分析、投影分析、基于Stone对偶性的逻辑表述。由于篇幅有限，我们也不得不省略一些本应在本书中有一席之地的方法，包括基于集合的约束、基于类型的分析的高效实现技术、静态单赋值形式（SSA）、更广的指针分析，以及程序分析与程序变换之间的相互影响和如何高效地重算因程序变换而失效的分析。
如何阅读本书
本书相对来说是自成一体的，但具有离散数学和编译原理方面的背景会对阅读本书有帮助。在本书的主要部分（第2～5章），每章的前半部分以严谨的形式介绍基本技术，后半部分以不那么严谨的方式介绍高级技术。
第1章是为了快速阅读。目的是概述程序分析的主要技术，强调程序分析把近似作为本质目的，并展示表面上不同的技术具有内在的相似性。我们推荐所有读者都阅读第1章，即使终目的是专注于本书某一章的内容。
第2章介绍数据流分析。21～24节覆盖过程内分析的基本技术，包括单调框架作为位向量框架的推广，以及高效计算的工作列表算法。22节覆盖更理论的性质（语义正确性），次阅读时可以跳过该节。该节使用了格理论，可参考附录A1和附录A2，以及附录A3的一部分。 25节包含高级内容，给出了过程间分析，包括基于调用字符串和基于假设集的方法。25节是学习第3章的基础，建议至少阅读到252节。26节也包含高级内容，展示如何结合简单的技术来设计一个非常复杂的形状分析。这些内容与本书的其余章节没有太大关系。
第3章讲述基于约束的分析。这里明确区分了分析结果的安全性和如何计算好的分析结果，同时强调了分析开放系统的必要性。31节、33节和34节介绍基本技术，包括余归纳概念，建议参考附录B（建立在附录A4的Tarski定理的基础上）。32节介绍较理论的性质（语义正确性和解的存在性），次阅读时可以跳过该节。35节和36节扩展这些技术，将其与数据流分析联系起来。35节介绍如何结合单调框架（见23节），36节介绍如何基于调用字符串和假设集（见25节）添加上下文。
第4章以独立于程序语言的方式介绍抽象解释理论，强调它能与数据流分析和基于约束的分析结合使用。41节介绍一些关键考虑因素，并为后几节的技术性定义做铺垫。42节介绍加宽算子和变窄算子，用于不动点的近似。43节介绍Galois连接。按这个顺序编排内容的目的是强调加宽算子的根本重要性，但这两节是相互独立的。44节和45节研究如何以系统的方式构造Galois连接，以及如何使用它们衍生近似分析，这些内容与本书的其余章节没有太大关系。
第5章介绍类型和作用系统，这通常被认为是一种和前面介绍的技术十分不同的程序分析方法。51节介绍主要方法（涵盖与第3章的基于约束的分析的联系），来帮助读者初步了解该方法。52节研究更理论的性质（语义正确性）。53节讨论算法问题（算法W的一个变体的可靠性和完备性），次阅读时可以跳过该节。54节和55节将逐步介绍类型和作用系统的更高级的内容。
第6章介绍数据流分析和基于约束的分析的算法，主要涉及不等式系统求解的通用技术。我们强调相同的算法在很大程度上可用于程序分析领域的很多不同情况。61节介绍一个通用的工作列表算法，将工作列表上的操作看作一个抽象数据类型，并证明该算法的正确性和复杂度。62节介绍如何组织工作列表使迭代根据逆后序进行，其中循环算法是一个特例。63节的算法进一步识别强分量，并在每个强分量完成逆后序迭代之后才考虑下一个强分量。
附录A和附录C介绍偏序集合、图和正则表达式的概念，本书有多处涉及了这些概念。附录B类似于教程，因为余归纳对于大多数读者来说可能是一个新概念。
我们使用的符号大多数是标准的，当使用时再解释。一些常用的符号解释如下：
 “iff”为“if and only if”（当且仅当）的缩写。
 …\[……\]代表语法替换和环境或存储的修改。
 …→fin…表示有限函数（具有有限定义域的部分函数）的集合。
如果能让表达更为清晰，我们将使用λ符号表示函数：λx…x…表示由f(x)=…x…定义的一元函数f。
如何教授本书
本书包含的内容超过一个学期的课程内容。课程的进度自然取决于学生的背景，我们为大四学生和拥有不同背景的博士生都开设过这门课。下面我们总结教授本书不同部分需要多少课时，以作为以上关于如何阅读本书的内容的补充。
 用两到三节课足以讲完第1章以及附录A1和附录A2中较简单的概念。
 21节、23节和24节应该是任何数据流分析课程的核心内容。用三到四节课可以讲完21～24节，但如果学生缺乏操作语义或格理论（附录A1～A3的一部分）的背景知识，则需要增加一节课。25节和26节是高级内容。用一到两节课可以讲完25节，而在两节课内讲完26节比较困难。
 用四到五节课应该能讲完第3章和附录B；但是，需要一段时间来熟悉余归纳的概念，因此好解释不止一次。
 用四到五节课应该能讲完第4章和附录A4。
 用四节课应该能讲完第5章。
 用两节课应该能讲完第6章，但如果需要复习附录C的大部分内容，则需要三节课。
我们把附录作为其他章节的一部分。实际上，第1章也介绍了一些基础的偏序概念，而且大多数学生对偏序、图和正则表达式已经有了一些了解。
本书包括很多练习和一些迷你项目，涉及本书内容的实践或理论方面的问题，以及不同章节之间的联系和类比。较难的练习标注了星号。
致谢
感谢Reinhard Wilhelm对本书的长期关注，他给了我们许多鼓励和建设性的意见。我们也从与Alan Mycroft、Mooly Sagiv、Helmut Seidl关于本书部分章节的讨论中受益匪浅。同事Alex Aiken、Torben Amtoft、Patrick Cousot、Laurie Hendren、Suresh Jagannathan、Florian Martin、Barbara Ryder、Bernhard Steffen也影响了这本书的写作，在此我们表示感谢。我们也感谢Schloss Dagstuhl主持了两次关键会议：1997年3月作者间的一周会议和1998年11月的高级讨论班。非常感谢参加在Dagstuhl举办的高级讨论班的学生，以及帮助测试本书的来自Aarhus、London、Saarbrücken和Tel Aviv的学生。后我们感谢Springer出版社的Alfred Hofmann提供的非常令人满意的合同。René Rydhof Hansen帮助我们调整了LATEX命令。
Flemming Nielson
Hanne Riis Nielson
Chris Hankin
1999年8月于奥胡斯和伦敦
第二次印刷的前言
在第二次印刷中，我们纠正了次印刷的错误和缺陷，感谢Torben Amtoft、John Tang Boyland、 Jurriaan Hage和Mirko Luedde，以及我们的学生的敏锐观察。

该书共分为6章，其中第1章为介绍，第2~5章依次为数据流分析、基于约束的分析、抽象解释、类型和作用系统，第6章为分析算法介绍。该书内容基本囊括了程序分析领域中的经典方法和技术，配以严谨的形式化系统，全书思路清晰、逻辑性强，是不可多得的经典书籍。

该书共分为6章，其中第1章为介绍，第2~5章依次为数据流分析、基于约束的分析、抽象解释、类型和作用系统，第6章为分析算法介绍。该书内容基本囊括了程序分析领域中的经典方法和技术，配以严谨的形式化系统，全书思路清晰、逻辑性强，是不可多得的经典书籍。

前言
第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

该书共分为6章，其中第1章为介绍，第2~5章依次为数据流分析、基于约束的分析、抽象解释、类型和作用系统，第6章为分析算法介绍。该书内容基本囊括了程序分析领域中的经典方法和技术，配以严谨的形式化系统，全书思路清晰、逻辑性强，是不可多得的经典书籍。