第一节课是概论，主要是告诉你程序静态分析是什么（也讲了点 Programming Language 相关的东西），对入门来说还是比较重要的。对我来说，看这一节最大的收获就是发现我感兴趣的几个方向看似相似但实际上大相径庭 hhh
（擦泪）真是学无止境。在看这节课之前我读过一篇年代久远的论文综述：程序静态分析技术与工具，起到的作用差不多，它把程序静态分析的方法和理论总结得比较清晰。我把读这篇论文（以及其他一些零零散散的论文综述）时写的论文笔记也杂糅到了这篇课程笔记里。
另：课中李樾老师谈到的有关 CS 学习与发展的心得让人听了真的很感动……虽然那些道理我早就想明白了，但能听到一位老师在课堂上对学生真诚地说出来，还是很感动……不要浮躁，走自己的路就好，就像课程中讲的那样，“稳健比精确更重要”。
程序设计语言与静态分析
语言 → 支撑语言运行的环境系统 → 语言这一复杂系统的具体应用及其应用中需要的保证（可靠性、安全性等）
引入静态分析的动机是计算机科学界对程序正确性的追求，也即与程序验证有关的研究。显然，程序验证要求涵盖所有情况，因此一般通过推理或者穷举的手段来判定程序的行为是否符合规约。但程序设计语言的复杂性使得程序的复杂性程序尺寸的增大呈指数级增长（主要源自于程序规模的增大，语言本身的核心依旧是 命令式语言 / 函数式语言 / 逻辑式语言 没有变），同时 Rice’s Theorem 又证明了任一程序正确与否本身是一个不可判定问题。而在现实的软件开发中，大量的时间被用于发现和消除软件中的错误，也就是软件测试。因此，才衍生出了上图中 Application 这个研究分支，并且它的重要性在程序复杂性日益增大的今天也越来越大。
一般来说，从软工角度讨论的程序分析是指动态分析，放在 PL 的尺度下讲就指静态分析。动态分析就是执行程序，再观察其行为是否满足要求；静态则不编译运行程序，而是在编译前通过对程序源代码进行分析以发现其中的错误。
静态分析的定义
静态分析的具体定义是：通过分析程序 P 来推理其行为，在运行 P 之前确定其是否满足某些属性。
For Example：
P 是否包括任何的私人信息泄漏问题？
P 有没有解引用过空指针？（这个好像还挺经常在大型系统中被找出来的……）
所有的强转操作在 P 中都是安全的吗？
P 中会有断言失败吗？（这个也比较典……）
……
静态分析的目标不是证明程序完全正确，而是作为动态测试的补充，在程序运行前尽可能多地发现其中隐含的错误，提高程序的可靠性和健壮性。有很多错误只凭测试人员手工测试很难找出来，而通过静态测试则已经发现了很多相当成熟的系统中的错误（可以看一下这篇，很有意思：拧龙头法测试并发程序）。
Rice Theorem
莱斯定理的内容是：不存在一个方法能够准确地判断一个程序的正确与否。（当然，是否正确本身也是由人给的规约规定的）
如果一个程序是由递归可枚举（图灵机可识别）的语言写成，则不存在一个方法能够 准确（Sound && Complete） 判断那些我们感兴趣的、跟程序运行时相关的行为是否正确。
（不仅给不出 Sound && Complete 的方法，甚至也给不出准确的 Truth / False 的集合）
因此我们研究的不是 Perfect 的静态分析，而是 Useful 的静态分析，即追求 Compromise soundness OR Compromise completeness。
妥协 Soundness 会带来漏报（False Negatives），妥协 Completeness 会带来误报（False Positives）。
绝大部分的程序分析都选择了妥协 Completeness，即保证 Soundness 而牺牲 Completeness 的，“Sound but not fully-precise” 的静态分析——做到这一步，就已经诞生了很多非常 Useful 的分析方法了。也就是说，稳健比精确更重要。
Soundness 的重要性
分析的 Soundness 对于一系列的重要分析应用都是非常关键的，比如编译优化和程序验证，它们都要求分析过程保证绝对的 Soundness，否则会得到错误的分析结论。这是符合直觉的，毕竟漏报的后果比误报严重多了。
对于那些不要求绝对 Soundness 的应用（比如 bug detection），Soundness 自然也是越完备越好，这样能够帮助找到更多的 bug。
因此，对静态分析给出尽可能保证 soundness 的要求：
为什么要学习静态分析
- 程序可靠性 / 安全性：帮助找到影响程序可靠性的 bug
- 编译优化：大部分编译优化使用的是静态分析技术
- 程序理解
静态分析功能和实例介绍
Static Analysis is Abstraction + Over-approximation。
- Abstraction Example
- Over-approximation Example
- Transfer functions：根据每个 stmt 的语义决定符号抽象的转换规则
（编译优化就做过这个 hhh）在这里已经有机会造成误报了。
- Control flows：分析程序的控制流
静态分析的方法和理论
主要摘自论文综述。这些方法并不完全相互独立，一个静态分析工具常需要使用多种方法以取得最佳效果。
- 符号执行（好像就是上文的 Abstraction）
- 用抽象的符号表示程序中变量的值，来模拟程序的执行
- 由于它跟踪了变量的所有可能取值，因此能够发现程序中细微的逻辑错误。但是在处理大程序时，程序执行的可能路径数随着程序尺寸的增大而呈指数级增长。在这种情况下需要对路径进行选择，选取一定数量的路径进行分析。
- 克服了在静态测试时不能确定程序中变量的值的问题
- 常在对路径敏感的程序分析中使用
- 用抽象的符号表示程序中变量的值，来模拟程序的执行
- 定理证明
- 自动定理证明是基于语义的程序分析，特别是程序验证中常用到的技术
- 类型推导
- 由机器自动地推导出程序中变量和函数的类型
- 在函数式语言中应用广泛
- 适用于控制流无关分析
- 基本思想
- 程序中的数据可以依照一定的规则划分为不同的集合，如果把每个集合作为一种类型，就可以利用类型理论中的一些算法进行分析
- 例如：可以将程序看作一个图，各结点通过加有控制流和数据流信息的边相连。图中的每个结点包含了计算出的变量的值。若将结点依据一定的规则分组，每一组就是一个类型，由此就可以对程序中指针变量的别名等问题进行考察。
- 程序中的数据可以依照一定的规则划分为不同的集合，如果把每个集合作为一种类型，就可以利用类型理论中的一些算法进行分析
- 抽象解释
- 没太看懂，似乎是指使用抽象解释函数作用于一个特定的抽象域，只考察程序的某一特定属性，在抽象域上找程序的最小不动点
- 基于规则的检查
- 根据规则描述分析特定类型的错误
- 模型检测
- 验证有限状态的并发系统
- 基本思想
- 对于有限状态的系统构造状态机或者有向图等抽象模型，再对模型进行遍历以验证系统的某一性质
- 状态空间可能会很大（爆炸）
- ……（我还没了解到的方向）
静态分析方法往往基于程序的一定的抽象表示。抽象语法树、有限自动机以及有向图是常用的方法。
……我们认为，静态分析需要更加有效的算法。在程序模型的构造、路径选择等方面，需要有更好的策略。将分析的路径限制在一定的范围，将动态测试和静态分析有机结合，这也许是一个值得探索的方向。