链接：https://cs.au.dk/~amoeller/spa/
由于最近可能会用到静态分析，所以就打算系统的学一下。
最先找到的是 #熊英飞 老师的《软件分析技术》课程，
这本书就是 introduction 中介绍的一本参考书。
在读这本书之前，我对 “静态分析” 的理解非常有限，
控制流分析，数据流分析，我本来以为这是编译器优化相关的，
没想到却是静态分析的内容。
读了这本书之后，脑海中几个分散的知识点，似乎被串联起来了。
- 可计算性理论：不可判定性，停机问题
- 类型理论：unification algorithm，let-polymorphism，recursive type
- 形式语义学：Lambda calculus，偏序集，格，最小不动点定理
- 编译原理：AST，CFG（控制流图），编译器优化
- 数理逻辑：可靠性，完备性
让我感到以前花时间学的知识，多少还是有些用处的。
本书一开始，作者就把静态分析建立在了完善的数学基础之上。
由于程序的静态分析具有不可判定性，所有无法给出精确的结论，
所以，本书用代数中的 “格” 来表示程序的可能状态，
格上的序关系，表示状态的精确程度，值越小表示结论越精确越肯定。
程序状态的转变是受代码控制的，因此不同种类的代码定义了格上的不同运算，
这些运算可以看做是一种约束，限制了程序状态不可任意转变。
很显然，程序的最终状态，必须满足所有的约束条件。
所以，静态分析的本质，
就是在格上求解所有约束条件的最小不动点（最精确解）。
对代码进行不同的静态分析，
就是为程序确定不同的抽象状态，以及不同的约束条件，
这种做法，被作者纳入到了一个统一的框架中，称为 “Monotone Frameworks”。
以下分析方法，都可以看做是 “Monotone Frameworks” 的一个应用。
- type analysis
- sign analysis
- live variables analysis
- available expressions analysis
- very busy expressions analysis
- reaching definitions analysis
- initialized variables analysis
后文作者又讨论了一些比较现实的场景，
分支，函数调用，first-class function，面向对象，指针，应该如何分析。
- 格高无限时（通过 widening，进行 interval analysis），
- 含 if 条件时（通过穷举，在乘积格上进行 ralational analysis）
- 代码中包含函数调用时（过程间分析）
- 含有 function 作为 first-class value 时（控制流分析，closure analysis）
- 面向对象语言中的控制流分析
- 包含指针时（pointer analysis，null pointer analysis）
最后，作者做了一个总结，
引出了 “抽象解释”（Abstract Interpretation）的概念。
抽象解释（其实是一个函子），建立了具体语义与分析模型之间的联系。
对同一段代码进行不同的静态分析，相当于为具体语义指定不同的解释映射。
人们喜爱可靠的解释，是因为程序执行的实际结果，一定包含在分析结论中，不会误报。
但不可靠的抽象解释未必不能用，因为可能对某一段代码来说它是可靠的。
总之，这本书是一本有足够深度的书，更偏理论一些，
对于系统性的认识静态分析，还是有很大帮助的。
只是具体的分析算法，描述的不是特别详细，
实际项目用起来的话可能还要花费更多的努力才行。
若有收获，就点个赞吧
0 人点赞
