【Static Program Analysis - Chapter 3】Type Analysis

类型分析，我的理解就是（经过静态分析技术）分析出代码中，哪些地方只能是某种或某几种数据类型，这是一种约束。

 

例如，给定一个程序:

其中，咱们能够很直接地获得一些约束：

最后，通过简化能够获得：

对于给定的变量类型，若是他们不符合这个约束，则说明，他们是不合法的。

那么，怎么去提取以及维护这些约束呢？

采用一种“并查集”的结构：一个有向图，每一个节点有一条边指向父节点（父节点则指向本身）。若是两个节点具备相同的父节点，那么，这个两节点就认为是等价的，即含有相同的数据类型。

如下是并查集的基本算法：

The unification algorithm uses union-find by associating a node with each term (including sub-terms) in the constraint system.

For each term τ we initially invoke MakeSet(τ ).

Note that each term at this point is either a type variable or a proper type (i.e. integer, heap pointer, or function); μ terms are only produced for presenting solutions to constraints, as explained below.

For each constraint τ1 = τ2 we invoke Unify(τ1, τ2), which unifies the two terms if possible and enforces the general term equality axiom by unifiying sub-terms recursively: 

Unification fails if attempting to unify two terms with different constructor (where function constructors are considered different if they have different arity). 

再来看个例子：

对于递归：

Limitations of the Type Analysis 

例子：

 

运行的时候没问题，可是，遵循以前的方法会报错，以前的方法并不考虑程序的顺序执行给数据类型转换的影响。即X=42在X=alloc以后，所以，最终返回的必定是int型。

另外一个例子：