AAM 与 Control Flow Anlaysis中的精度控制

0. 总览

这是一篇过度冗长的博客,如果你有心情读,大不必都看,算是对我之前workshop paper的一个背景补充介绍。

  • 什么是CFA
  • 什么是AAM式的CFA算法
  • 不同闭包的构造方式
  • k VS m,两种不同CFA精度
  • k与m的精度丢失与状态爆炸
  • 杂项

1 背景

控制流分析是很多现代程序分析算法的基础,几乎所有的静态程序分析算法首先都依赖与预先生成好的程序控制流图。在抽象解释(Abstract Interpretation)流派^1的静态分析中甚至认为只要在控制流分析中混入合适收集语义(collecting semantic), 就能实现绝大多数静态分析算法。不过现实中对于大多数过程间分析的算法(inter-procedure anlaysis), 函数之间的控制流边是很难生成的,其最主要的原因在于高阶函数的存在。 在函数式编程中我们可以从下面的例子看出

(let* ([a (lambda (x) x)]
       [b (lambda (y) (y y))
  (b a))

在这个例子中,如果我们不先去计算a和b的值那么我们只能看到 a\rightsquigarrow b的 函数调用, 但是如果我们进一步对a 和b进行带入计算,不难发现实际上在计算b的函数体的时候实际存在一条a\rightsquigarrow a的函数调用边。 大多数编译器中使用的控制流分析算法并不是很复杂,对于这种高阶函数调用的分析都是非常有限的。但是对于函数式编程编译器来说,大多数的用户程序都会大量使用高阶函数, 如果不分析高阶函数的控制流那么编译器优化的有效程度就变得大打折扣了。

如果编译器的对象不是函数式编程语言呢比如java,在这种高级的面向对象语言中往往存在类型系统, 类型系统的存在似乎让我们总能知道我们要调用的对象上有哪些方法,从而找出函数之间的调用关系。但是考虑下面的例子:

Cat kk = new BlackCat();
Cat ww =  new TabbyCat();

function foo(Cat c) {
    c.meow();
}
foo(kk);
foo(ww);

由于继承关系/函数指针/反射等机制的存在,如果想要知道meow函数执行的到底是什么我们需要知道c指针在程序所有运行时的指向。所以面向对象语言的高阶控制流分析也被称为指针分析。静态的生成比较精准的控制流图是非常困难的,而完全精确的知道运行的每一个时刻程序指针的指向更是直接可以让问题被reduce到停机问题。

虽说完全精准的CFA在理论上是不可能的,但是这不意味着我们不能使用他,我们可以通过Over Approximate的方式,通过某一些近似来得到相对精确的控制流。但是精度也是一把双刃剑,越高的精度往往意味着算法的潜在开销越大,所以在CFA算法被提出后大量的研究重心都放在了如何调节CFA的精度上。

2. AAM

由于控制流分析本质上来说是近似程序运行中会经过的轨迹, 所以相关的算法受到Abstract Interpretation流派分析的影响非常的深。主流的算法都倾向与设计一个针对目标语言解释器,在这个解释器上运行需要被分析的目标代码, 然后记录解释器运行过程中经过的程序状态。当然, 如果我们不对这个解释器做任何的修改,那么我们最终得到就是一个完全精确的程序控制流。由于停机问题的存在这样的解释器自然也不是decidable的,更无法去穷举程序的所有可能执行结果。 因此, 我们需要一种抽象语义,在这种语义下:

  1. 我们的解释器程序总能停机,
  2. 并且这种语义能够覆盖(over approximate) 程序在精确语义下的执行结果。

但是设计一种能满足上述两点要求的抽象语义不是一件容易的事情,所以在很长的一段时间内实现高级控制流分析都是比较复杂的一件事情。算法的设计者需要准确的描述他的抽象语义并且证明他的语义能够做到上面两点要求。 这种情况直到2010年才有所改善,David Van Horn 和 Matt Might提出了一种抽象语义设计的通用模板Abstracting Abstract Machine(AAM)^2

CESK* machine

在这篇文章中他们使用最简单的\lambda - calculus的带时间戳的CESK*型解释器作为例子,说明了对于任意的抽象语义模型,设计抽象语义中最核心的是三个要素

  1. 如何抽象存储(store),使得其中存放的值总是有限多的
  2. 如何分配程序的变量和Continuation在内存中的地址(设计alloc函数)
  3. 如何描述程序的运行时间戳,即一个程序状态他距离程序开始经过了多少时间(tick函数)

一个常见的误区是AAM只能试用与CESK*-timestamp machine。事实上这是不一定的,抽象解释中语言的模型是不固定的只要做到了上面说的几点,其他只是具体实现的问题。 而在实际的算法设计中我们不能对文章中举例的语义模型进行生搬硬套,还是要理解设计框架的核心思想和抽象位置。

4. 分歧点:不同的(闭包/对象)构造方式

这个章节算是一些题外话,但是我认为对实际中的CFA中设计非常重要。

大多数的控制流分析的算法都是针对函数式编程语言的,在AAM论文中, 你可以发现, 唯一一种提到的值就是函数闭包,之前也说了,抽象值必须是有限多的,所以不同的闭包的生成方式其实会对我们算法的设计产生巨大的影响。

但是从某种意义上来说,函数式编程中的闭包就是面向对象编程中的对象,他们本质上都是函数加数据的集合体。在这里我们不妨放下语言流派之间的分歧重新用从更高的视点来看待问题 在这个小节中我也将以c++式的语言为例子分析两种不同的闭包构造方式和他们对AAM式抽象解释模型产生的影响

4.1 链表式对象构造

class Foo  {
     int* x;
     Bar* bar;
     void  do(){};
}

在上面的这个例子中, 类Foo的所有成员都是指针类型的,也就是说在构造对象的时候并没有直接把值或者别的对象的数据放在对象当中。实际上在有些函数式语言中也是这样的,在构造闭包的时候闭包里并没有直接存放别的函数的值,而是只存放一个指向别的内部函数或者数据的指针。这种构造方式的好处是我们可以把每一个对象/闭包变得非常的小,从而避免stack overflow之类的问题, 但是坏处也很明显,我们如果需要访问bar所指向对象中值,我们需要从新计算bar的地址,如果他们不在同一个内存页/缓存行中,我们就会遇到cache以及页表替换的问题,这对编译器优化也提出了更加高的挑战。在许多语言,比如java/haskell中你几乎只能使用这种方式,这类语言往往拥有非常强大的垃圾回收机制。

4.2 扁平式的对象构造

class Foo  {
     int x;
     Bar bar;
     void  do(){};
}

在C系列的语言中我们可以写出下面的代码, 此时bar对象被直接存放在Foo的内部, 这种方式被称为扁平式对象。其实在函数式语言中我们也可以做类似的事情

((lambda (x) (lambda (z) x))
 1)

在我们对(lambda (z) x)进行求值让他从纯粹的字面表达式变成闭包的值的时候我们可以像之前说的那样,把外部词法空间中的变量x的地址放在(lambda (z) x)的值中变成\langle (\lambda z.x), \{ x \mapsto x_{addr} \} \rangle, 也可以扁平化,把x所对应的值直接复制进入闭包,得到\langle (\lambda z.x), \{ x \mapsto 1 \} \rangle.

4.3 影响

这两种闭包的构造方式可能从精确解释器求值的情况下一般来说是等价的,但是对我们的抽象语义的设计却会产生非常大的影响,特别在是时间复杂度和精度控制上。同样是在2010年,Yannis Smaragdaski,Matt Might和David Van Horn开始尝试对面向对象语言进行AAM式的分析^4.他们发现如果采用链表式的对象/闭包构造,算法的时间复杂度是指数级别的,比较难在大型的程序上运行这样的算法, 但是如果使用扁平化闭包进行抽象语义设计,就可以得到多项式级别的时间复杂度。在接下来的章节中我会分别介绍两种构造方式和针对其适应的CFA算法。

3. k last calling context CFA(k-CFA)

那么我们应该与如何定义CFA的精度呢? 回到1991年,Olin Shiver 在他的博士毕业论文中^3 对这个问题进行了深入的探讨,他设计了一种针对CPS变换后\lambda-calculus的抽象语义,并且详细描述了如何利用抽象语义的方法来实现CFA. 在他的分析中, CFA的精度取决距离函数被调用位置最近的k个调用上下文。k个上下文是一个比较抽象的概念,我们可以用AAM的方式来重新描述Olin Shiver的k精度算法。

首先, 正如AAM原本论文中的例子一样k-CFA算法可以用带时间戳的CESK*模型描述

  • store中的值只有\lambda闭包, 每一个闭包是一个\lambda表达式文本加上一个包含其中所有自由变量的变量名到变量地址的map映射。 因为一段代码中的\lambda表达式的个数是有限的, 自由变量也是有限的,那么在变量地址有限的情况下,store就是有限的。
  • store中的Continuation分为参数求值和函数作用两种, 其中, 每一个Continuation包含一个指向下一个Continuation的指针, 在地址有限的情况下,Continuation的数量也是有限的。
  • 抽象变量分配得到的地址是函数名加上当前变量被分配时程序的运行时间戳,得到.\langle x, t \rangle二元组的结构。
  • 程序时间戳是当前执行的表达式编号加上调用栈历史\langle l, \delta \rangle, 原文把调用栈称为程序轮廓(contour)。而每次如果遇到需要变量绑定,就往调用栈中添加当前的程序表达式编号,并且保持调用栈的长度总为k.
  • continuation的地址是 下一个要被运行的表达式的编号加上当前程序时间中的程序轮廓,构成的二元组\langle l, \delta \rangle
    k-CFA

在Olin Shiver的算法中,程序轮廓是一个非常抽象的概念,我个人觉得这个名字并不合适,其本质就是调用栈,或者可以理解为程序上下文context。 这个值的变化发生在每次函数求完参数的值,把函数中的参数变量绑定到对应值的时候, 这个时候本质就是移动EBP调用栈加一,而这里的长度k表示的就是我们最多能够追踪的调用栈数量(注意这里不是深度) 。注意这里的tick v那条, 这条发生在变量绑定的时候,他实际上会把之前被调用点的label推入调用栈当中。
看一个例子吧,最经典的id id
(^1(^2(^3\lambda x. ^6x) (^4\lambda y. ^7y)) (^5\lambda z .^8z))
求值顺序为
1 \rightsquigarrow 2 \rightsquigarrow 3 \rightsquigarrow 4 \rightsquigarrow 6 \rightsquigarrow 7 \rightsquigarrow halt
其运行过程中的如果我们令k= \infty,时间戳变化如下:

  1. \langle 1, [] \rangle,
  2. \langle 2, [] \rangle
  3. \langle 2, [] \rangle
  4. \langle \bullet ,[2] \rangle
  5. \langle \bullet ,[2] \rangle
  6. \langle \bullet ,[2] \rangle
  7. \langle \bullet ,[\bullet ,2] \rangle

如果是k= 1那么当\bullet被放入调用栈的时候 ,2就被顶出来了。这里有一点点不太合理的地方就是如果你认为 l\delta是一个整体作为程序contour的那么实际上1cfa中有的时候会有两个调用栈信息,因为AAM的论文中认为,k的值是\delta的长度。
一句话来总结k-CFA算法的敏感程度,这个算法实际上就是在时间戳中记录倒数k个调用栈信息,以此来区别对同一个函数的多次调用。在使用链表式闭包构造的语义中,大量的分析采用了这种调用敏感度。

4. m top calling context CFA(m-CFA)

实际上k-CFA并不唯一的调用敏感程度的描述方式。还是在Resolving and Exploiting the k-CFA Paradox^4这篇论文当中, 作者提出了另一种更新时间戳的方式。这种时间戳的更新方式是针对扁平化闭包来语义的。 这种CFA依然是使用AAM的方式进行描述的,但是由于扁平化闭包的加入,CESK*-timestamp模型并不再能完全适用了。

首先, 原本的E肯定是不再需要了,因为原本,如果是链表式的闭包,我们需要用一个map去记录之前变量的实际地址的,但是现在不同每次当我们的函数调用上下文发生变化的时候我们是直接把所有需要用到的自由变量从闭包外面复制到当前的调用栈当中。我们只需要知道程序现在的调用栈标记是什么,根据他就可以直接去查询变量的值, 而之前在介绍k-CFA的时候,我们已经说时间戳的本质是函数的调用栈,而在m-CFA的论文中, 他们直接不再使用timestamp或者contour之类奇怪的名字了,而直接用context上下文来称呼, 所以最终的模型被化简为了CSK* -context抽象机, 其实原文中甚至没有K*因为是针对CPS变换后的\lambda-Calculus的。并且,他们不再使用tick这一函数的称呼,而是采用了new.虽然这个语义中并没有显示的描述他们的alloc函数是怎么样的,但是其实从扁平化闭包的定义其实不难看出,只需要用标量名加上当前context来表示就行了,在这一点上和原本的k-CFA其实没有什么区别。纯粹只是这篇论文直接内联了这个函数的实现罢了,因为这里的语义实在是很简单。

还是来看之前的例子吧

(^1(^2(^3\lambda x. ^6x) (^4\lambda y. ^7y)) (^5\lambda z .^8z))
求值顺序为
1 \rightsquigarrow 2 \rightsquigarrow 3 \rightsquigarrow 4 \rightsquigarrow 6 \rightsquigarrow 7 \rightsquigarrow halt
m-CFA中context的变化如下:

  1. []
  2. []
  3. []
  4. []
  5. [2]
  6. [1]
  7. []

不难发现,m-CFA在最后是从1中返回的,而k-CFA是从2中返回的。所以这种算法追踪的是最顶上的几个调用栈。
从敏感程度上来说,k-CFA的context变化是要远多于m-CFA的,所以他也更加敏感,但是问题是,在扁平化闭包的语义当中,拷贝本身也就意味着丢失了这个值真实生成位置的信息,而过度的调用栈敏感程度,会导致算法的精度快速下降。虽然不难证明, 在使用了扁平化闭包以后,分析k-CFA算法的时间复杂度会下降到多项式时间但是这种精度的丢失就有点得不偿失了。

因此综合上来说在扁平化闭包语义中m-CFA是更加优秀的, 这种分析在对面向对象的语言中被大量的应用,在之后的2011年Yannis根据扁平化闭包的思想,在Doop这一针对Java的指针分析框架中加入了被称为对象敏感度的新精度衡量方式^5.这直接使得较高精度的分析算法在面向对象语言中至少有一定的可行性了。

5. CFA中精度丢失与状态爆炸

本来这篇博客到这里已经差不多了,主流的两种CFA的方式已经介绍完了,但是在研究算法极端测试用例以及复杂度分析的时候我发现了下面的两个例子,也真正的让我加深了对CFA的理解,还是想在这里分享给大家。

首先第一个例子来自于David Van Horn的分析k-CFA的论文^6,也是他dissertation的主要部分。他原本用的那个语法比较不严谨,我用scheme的语法来简单的重写一下这个例子。

((lambda (f) 
    (let ([a (f #t)]
          [b (f #t)]) 
      b))
 (lambda (z)
    ((lambda (x) x) (if z z #f))))

这个例子看上去似乎没有什么太特别的地方,但是如果你仔细手推一遍这段代码的运行过程就会发现DVH设计这个例子的时候的心思所在。这个例子最核心的地方就在于函数(lambda (z) ...)被绑定到f之后调用了两次。如果你对scheme/lisp语言比较熟悉,应该会不难计算出这个表达是最终的结果是#t, 因为内部(if z z #f)是一个永真式,不论是f的输入是真还是假,最后的结果都必然是真。

但是我们在CFA算法中设计的抽象解释器会给我们什么样的运行结果?

0-CFA是精度最低的CFA算法,也就是完全不记录任何的调用点信息,在AAM式的抽象解释器中来说就是new/tick函数永远返回空。我们来看一下在这种精度下抽象解释器的执行情况。

当函数f被调用时,在两个f的调用点,#t, #f两个值会被分别在各种的调用空间中绑定到变量z上。此时我们的alloc函数会对这个变量进行地址分配,但是如果你仔细阅读和带入规则就会发现他们的地址是相同的\langle z,[] \rangle.在进入(if z z #f)的时候,z的值同时是真和假,最终结果会变成计算这个表达式的真值表。也就是说0CFA算法在这里发生了精度不够的情况,而这种不够的结果是灾难性的,因为他会直接让抽象解释器的状态发生指数爆炸,原因很简单,如果你把(if z z #f)改成更多z的表达式比如(or z1 z2 z3 z4 ....)如果每一个变量都有复数个值,那么最终得到的是指数个不同的运行结果。

如果是1-CFA呢?

照样没用,因为(if z z #f) 还被作用到了一个(lambda (x) x)上这个call是个没有意思的冗余call,只是平白无故的把callsite加一。这个identity函数在这里被称为padding,这个例子中至少要2以上的CFA才能保持精度。

DVH原本的例子

这个例子其实对扁平化闭包带来的影响会更加的大,这里大量的额外callsite放大了变量复制带来的精度丢失,在这里就暂时不展开讲了。

上面的分析告诉我们,精度越高速度越慢是一个大体上的规律但是并不是一定的,低精度也意味着容易发生状态爆炸,从而使抽象解释器陷入大量无意义的近似计算中。

Reference

  1. Cousot, P., & Cousot, R. (1992). Abstract interpretation frameworks. Journal of logic and computation, 2(4), 511-547.
  2. Van Horn, D., & Might, M. (2010, September). Abstracting abstract machines. In Proceedings of the 15th ACM SIGPLAN international conference on Functional programming (pp. 51-62).
  3. Shivers, O. G. (1991). Control-flow analysis of higher-order languages or taming lambda. Carnegie Mellon University.
  4. Might, M., Smaragdakis, Y., & Van Horn, D. (2010, June). Resolving and exploiting the k-CFA paradox: illuminating functional vs. object-oriented program analysis. In Proceedings of the 31st ACM SIGPLAN Conference on Programming Language Design and Implementation (pp. 305-315).
  5. Smaragdakis, Y., Bravenboer, M., & Lhoták, O. (2011, January). Pick your contexts well: understanding object-sensitivity. In Proceedings of the 38th annual ACM SIGPLAN-SIGACT symposium on Principles of programming languages (pp. 17-30).
  6. Van Horn, D., & Mairson, H. G. (2008). Deciding k CFA is complete for EXPTIME. ACM Sigplan Notices, 43(9), 275-282.
最后编辑于
©著作权归作者所有,转载或内容合作请联系作者
  • 序言:七十年代末,一起剥皮案震惊了整个滨河市,随后出现的几起案子,更是在滨河造成了极大的恐慌,老刑警刘岩,带你破解...
    沈念sama阅读 203,547评论 6 477
  • 序言:滨河连续发生了三起死亡事件,死亡现场离奇诡异,居然都是意外死亡,警方通过查阅死者的电脑和手机,发现死者居然都...
    沈念sama阅读 85,399评论 2 381
  • 文/潘晓璐 我一进店门,熙熙楼的掌柜王于贵愁眉苦脸地迎上来,“玉大人,你说我怎么就摊上这事。” “怎么了?”我有些...
    开封第一讲书人阅读 150,428评论 0 337
  • 文/不坏的土叔 我叫张陵,是天一观的道长。 经常有香客问我,道长,这世上最难降的妖魔是什么? 我笑而不...
    开封第一讲书人阅读 54,599评论 1 274
  • 正文 为了忘掉前任,我火速办了婚礼,结果婚礼上,老公的妹妹穿的比我还像新娘。我一直安慰自己,他们只是感情好,可当我...
    茶点故事阅读 63,612评论 5 365
  • 文/花漫 我一把揭开白布。 她就那样静静地躺着,像睡着了一般。 火红的嫁衣衬着肌肤如雪。 梳的纹丝不乱的头发上,一...
    开封第一讲书人阅读 48,577评论 1 281
  • 那天,我揣着相机与录音,去河边找鬼。 笑死,一个胖子当着我的面吹牛,可吹牛的内容都是我干的。 我是一名探鬼主播,决...
    沈念sama阅读 37,941评论 3 395
  • 文/苍兰香墨 我猛地睁开眼,长吁一口气:“原来是场噩梦啊……” “哼!你这毒妇竟也来了?” 一声冷哼从身侧响起,我...
    开封第一讲书人阅读 36,603评论 0 258
  • 序言:老挝万荣一对情侣失踪,失踪者是张志新(化名)和其女友刘颖,没想到半个月后,有当地人在树林里发现了一具尸体,经...
    沈念sama阅读 40,852评论 1 297
  • 正文 独居荒郊野岭守林人离奇死亡,尸身上长有42处带血的脓包…… 初始之章·张勋 以下内容为张勋视角 年9月15日...
    茶点故事阅读 35,605评论 2 321
  • 正文 我和宋清朗相恋三年,在试婚纱的时候发现自己被绿了。 大学时的朋友给我发了我未婚夫和他白月光在一起吃饭的照片。...
    茶点故事阅读 37,693评论 1 329
  • 序言:一个原本活蹦乱跳的男人离奇死亡,死状恐怖,灵堂内的尸体忽然破棺而出,到底是诈尸还是另有隐情,我是刑警宁泽,带...
    沈念sama阅读 33,375评论 4 318
  • 正文 年R本政府宣布,位于F岛的核电站,受9级特大地震影响,放射性物质发生泄漏。R本人自食恶果不足惜,却给世界环境...
    茶点故事阅读 38,955评论 3 307
  • 文/蒙蒙 一、第九天 我趴在偏房一处隐蔽的房顶上张望。 院中可真热闹,春花似锦、人声如沸。这庄子的主人今日做“春日...
    开封第一讲书人阅读 29,936评论 0 19
  • 文/苍兰香墨 我抬头看了看天上的太阳。三九已至,却和暖如春,着一层夹袄步出监牢的瞬间,已是汗流浃背。 一阵脚步声响...
    开封第一讲书人阅读 31,172评论 1 259
  • 我被黑心中介骗来泰国打工, 没想到刚下飞机就差点儿被人妖公主榨干…… 1. 我叫王不留,地道东北人。 一个月前我还...
    沈念sama阅读 43,970评论 2 349
  • 正文 我出身青楼,却偏偏与公主长得像,于是被迫代替她去往敌国和亲。 传闻我的和亲对象是个残疾皇子,可洞房花烛夜当晚...
    茶点故事阅读 42,414评论 2 342

推荐阅读更多精彩内容