标签：sys with .com tor mit poi str 直接 red
类型分析，个人理解就是（通过静态分析技术）分析出代码中，哪些地方只能是某种或某几种数据类型，这是一种约束。
?
例如，给定一个程序:
其中，我们可以很直接地得到一些约束：
最后，经过简化可以得到：
对于给定的变量类型，如果他们不符合这个约束，则说明，他们是不合法的。
那么，怎么去提取以及维护这些约束呢？
采用一种“并查集”的结构：一个有向图，每个节点有一条边指向父节点（父节点则指向自己）。如果两个节点具有相同的父节点，那么，这个两节点就认为是等价的，即含有相同的数据类型。
以下是并查集的基本算法：
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型。
另一个例子：
【Static Program Analysis - Chapter 3】Type Analysis
标签：sys with .com tor mit poi str 直接 red
原文地址：http://www.cnblogs.com/XBWer/p/7966406.html
