PL and Static Analysis
背景：在过去十年中，语言核心几乎没有变化，但是程序变得更大，更复杂。
挑战：如何确保大型复杂程序的可靠性，安全性和其他承诺？
编程语言
理论
Language design//语言设计
Type system//类型系统
Semantics and logics//语义学和逻辑学
环境
Compilers//编译器
Runtime system//运行系统
应用
Program analysis//程序分析
Program verification//程序验证
Program synthesis//程序综合
Why We Learn Static Analysis?
程序可靠性//Program Reliability
空指针取消引用，内存泄漏等
程序安全性//Program Security
私人信息泄漏，注入攻击等
编译器优化//Compiler Optimization
消除无效代码，代码移动等
程序理解//Program Understanding
IDE调用层次结构，类型指示等
静态分析的市场
Static analysis people are urgently needed !
What is Static Analysis?
静态分析对程序P进行分析以推断其行为，并在运行P之前确定其是否满足某些属性。
•P是否包含任何私人信息泄漏？<br>•P是否取消引用任何空指针？<br>•P中的所有投射操作是否安全？<br>•P中的v1和v2可以指向相同的存储位置吗？<br>•P中的某些断言语句会失败吗？<br>•这部分代码是否处于P状态（因此可以消除）？<br>•…
不幸的是，根据赖斯定理，没有一种方法可以确定P是否满足这种非平凡的性质，即给出确切的答案：是或否。
Rice's Theorem
“r.e. 语言中程序行为的任何非平凡属性都是不可判定的。”
r.e. (recursively enumerable)（递归可枚举）=可被图灵机识别
如果某一种属性不受任何 r.e. 语言的欢迎，那么它就是微不足道的，<br>或所有 r.e. 语言都满意；否则，它是不平凡的（ non-trivial）。
也就是说，这种属性既不是所有语言都没有，也不是所有语言都有，而是部分语言有。
不平凡的性质<br>〜=有趣的属性<br>〜=与程序的运行时行为相关的属性
前面提到的一些属性都是不平凡的。
<b>Perfect</b> static analysis
可以确定P是否满足这样的非平凡性质，即给出确切答案：是或否
Sound <br>AND <br>Complete
<b>Useful</b> static analysis
• Compromise soundness (false negatives)//妥协（损害）于soundness（漏报）<br>OR<br>• Compromise completeness (false positives)//妥协（损害）于completeness（误报）
主要妥协（损害）于completeness：<br>可靠但不够精确的静态分析。
Soundness的必要性
Soundness对于重要的（静态分析）应用程序集合至关重要，例如编译器优化和程序验证。
Soundness也比不需要Soundness的其他（静态分析）应用程序（例如错误检测）更可取，因为更好的Soundness意味着可以找到更多的错误。
Static Analysis — Bird's Eye View
静态分析：确保（或接近）Soundness，同时在分析精度和分析速度之间进行良好的权衡。
Static Analysis Features and Examples
总结静态分析的两个词//对于大多数静态分析（may analysis）
Abstraction + Over-approximation
一个例子
确定给定程序的所有变量的符号（+，-或0）。
Abstraction
Over-approximation
Transfer functions//传递函数
在静态分析中，传递函数定义了如何根据抽象值评估不同的程序语句。
传递函数是根据“分析问题”和不同程序语句的“语义”定义的。
Control flows
由于实际上不可能列举所有路径，因此大多数静态分析都将流量合并（作为一种过度逼近的方式）视为理所当然。
