下推控制流分析 | Codeboy's Blog

形式陈述

下推控制流分析把高阶程序的环境和存储有限化，却保留未设深度上界的调用栈。它从抽象机器出发，将状态写成

(q,\kappa),\qquad q=(e,\hat\rho,\hat\sigma),\qquad \kappa\in\Gamma^*.

表达式e来自有限程序，环境和存储采用有限地址及有限值近似，所以控制状态集Q有限；栈帧集合 $\Gamma$ 也有限，但任意有限栈序列使总配置集合仍可能无限。

选择无第一类续延的传值高阶核心，使一步执行只需有限控制和栈顶：调用可压一帧，返回弹指定帧，尾调用可不改变栈。于是机器成为一个下推系统，转移标记为 $\varepsilon$ 、 $\operatorname{push}\gamma$ 或 $\operatorname{pop}\gamma$ 。

与七元组 PDA 接口对应时，另加永久栈底符号 $Z_0$ ，用 $\kappa Z_0$ 编码这里的帧栈，因而空帧栈对应仅含 $Z_0$ 的栈。所有转移都不读取输入：内部步保留栈顶，push $\gamma$ 把顶符号 $X$ 替换为 $\gamma X$ ，pop $\gamma$ 只把顶端的 $\gamma$ 替换为空串，永不弹出 $Z_0$ 。PDA 的剩余输入始终为空；本分析询问控制状态可达性，不使用终态或空栈接受条件。

分析目标是从初始控制 $q_0$ 和空栈出发，哪些控制状态与哪些调用返回边可经合法栈动作到达。栈的精确性只针对所选抽象控制系统；被合并的数值、闭包环境或堆内容仍可能引入额外行为。

直觉

k-CFA把历史限制在有限上下文中，因此容易让多次调用共享返回信息。下推方法不把整条栈压成有界历史，而用一套有限摘要表示无界嵌套：一段从压帧到匹配弹帧的计算可以整体视为净栈变化为零。

这类似括号语言。push a, push b, pop b, pop a合法；push a, pop b非法。增加递归深度只会增加嵌套层数，不会要求把所有栈逐条列出来。

图中+a表示压入a，−a表示弹出a；虚线B是净栈变化为空的平衡路径摘要，不是新增的程序指令。

例子与边界

相同函数入口，不同返回帧

设程序先计算 u=f(0)，再计算 v=f(1)，两个调用后分别还有不同工作。进入f时分别压入帧 $K_u$ 与 $K_v$ 。若有限值抽象把0和1都概括为“整数”，两次调用可以进入相同控制状态q，但完整配置分别为 $(q,K_u\kappa)$ 与 $(q,K_v\kappa)$ 。

f结束时，只能弹当前栈顶。第一配置返回u后的位置，第二配置返回v后的位置；即使q完全相同，也不产生交叉返回。这正是过程间合法路径在抽象机层面的直接实现。

若f递归调用自身，栈可以成为 $K_rK_rK_rK_u\kappa$ 。算法没有把深度限制为k；返回必须先逐层弹掉 $K_r$ ，才可到达 $K_u$ 的续接位置。

用有限平衡关系代表无限嵌套

定义 $B\subseteq Q\times Q$ ： $(p,q)\in B$ 表示存在一条从p到q、净栈变化为零且不弹出起始层的路径。对显式有限系统，可按规则求最小关系：

$(p,p)\in B$ ，每条内部 $\varepsilon$ 边也加入B
若 $(p,r),(r,q)\in B$ ，加入 $(p,q)$
若 $p\xrightarrow{push\gamma}r$ 、 $(r,s)\in B$ 、 $s\xrightarrow{pop\gamma}q$ ，加入 $(p,q)$

第三条必须匹配同一个帧符号。设有 $p\xrightarrow{push\ a}r$ 、 $r\xrightarrow\varepsilon s$ 、 $s\xrightarrow{pop\ a}t$ ，便得到B(p,t)；若最后是pop b，就不能建立该摘要。

从空栈出发的合法路径末端可能仍有未返回调用。它能分成若干平衡片段和若干尚未匹配的push。因此可从 $q_0$ 开始，沿B摘要与push边传播控制可达性；不能无条件沿pop边传播。对源语言隐式生成控制状态的实现，摘要、可达状态与新转移要交替增长，这就是Dyck状态图工作队列的思想。

推论与应用

终止与证明责任

尽管栈配置无限，B最多只有 $|Q|^2$ 对；摘要规则只添加不删除，因此饱和终止。每条新摘要对应内部步、路径拼接或匹配的一对push/pop，故可靠。反方向按平衡路径的括号嵌套归纳，任意平衡路径都能由这些规则构造，所以摘要完整。

最简单的全扫描饱和可用非常保守的多项式界描述：至多 $|Q|^2$ 次新增轮，每轮扫描关系三元组合以及匹配push/pop规则对。若转移数为d，直接实现界可写为 $O(|Q|^5+|Q|^2d^2)$ ，空间主要为 $O(|Q|^2+d)$ 。专门索引和工作队列能减少大量重复。这些是相对于已经显式列出的控制系统的界，不是相对于源代码自动得到的多项式界。

如果把每一种抽象存储都放进q，Q本身可能随程序大小指数增长。某些PDCFA变体通过统一存储的widening等手段取得源程序规模上的多项式界，同时付出别处精度损失。因此“保留无界栈仍可判定”与“分析整个程序很便宜”是两条不同结论。

栈精确不使所有值都精确

若进入f的两个实参已经在同一抽象地址合并，返回路径虽严格匹配，返回值仍可能混合。下推方法消除的是由错误调用返回配对造成的路径，不能恢复前面主动丢掉的堆或数值区别。

加入第一类续延、可从栈中间恢复的控制对象，或每一步都查看整条栈的操作时，原来“只读栈顶”的下推接口可能失效。抽象GC就需要知道所有续延帧持有的根地址；将它与下推分析结合需额外的栈根摘要或introspective构造，不能直接扫描无界栈后仍宣称使用同一个普通下推系统。

练习与解答

给边 $p\xrightarrow{push\ a}r$ 、 $r\xrightarrow{push\ b}s$ 、 $s\xrightarrow{pop\ b}t$ 、 $t\xrightarrow{pop\ a}u$ ，求B(p,u)。先由恒等摘要B(s,s)和中间push/pop得到B(r,t)，再用外层push/pop得到B(p,u)。若把第三条改成pop a，内层配对失败，不能形成同一摘要。

验收须给出内外两次构造，并解释为什么不需要枚举运行栈深度。把四条边忽略标签后做普通传递闭包，无法通过这一检查。

参考资料

Christopher Earl, Matthew Might, David Van Horn, “Pushdown Control-Flow Analysis of Higher-Order Programs”, Scheme, 2010，§§4–6：CESK到下推系统；§§7–8：Dyck状态图；§9：通过widening获得多项式版本
J. Ian Johnson et al., “Pushdown Flow Analysis with Abstract Garbage Collection”, JFP 24(2–3), 2014，§1.1：整栈根信息与普通下推接口的冲突

形式陈述 ​

相同函数入口，不同返回帧 ​

用有限平衡关系代表无限嵌套 ​

终止与证明责任 ​

栈精确不使所有值都精确 ​

练习与解答 ​