静态分析里最难啃的骨头，循环绝对排第一。十几年前我第一次给一个指针分析工具加循环处理，盯着不动点迭代的中间结果从精度可观变成“什么都可能发生”，那种无力感到现在还记得。后来在几个做验证工具的项目里反复碰壁，我算是彻底明白了：程序分析里大部分无语的“假死”，拆到根子上都能归到一个没算好的循环不动点。而循环真正难缠的地方，又不只是迭代不收敛，还在于当循环里有多个相互干扰的分支路径时，你不得不把“析取”这种精确信息也叠加上去。路径枚举、状态爆炸、拓扑熵失控，这些词背后全是同一件事：循环总结该怎么做才既精确又能终止。
今天想聊的Proteus，正是冲着“析取形式的循环总结”这一难缠问题来的。它的核心思路是路径依赖分析：把循环体里各条路径之间的数据依赖和控制依赖变成一张图，再基于这张图做分解，让析取总结的生成从“硬着头皮枚举路径”变成“按依赖关系分组，各组之间互不干扰地计算”。这个方法不引入全新的抽象域，也不依赖某个偏序加速算子，而是换个视角看待循环路径的排列组合问题。在我看来，Proteus最有价值的地方，是把循环分析里原本只能靠直觉和经验的“哪些路径必须一起算”变成了一种可以由计算回答的结构性问题。
这篇内容适合三类人：正在做静态分析工具或形式化验证框架的开发者；研究方向涉及循环不动点、路径枚举、程序依赖关系的同学；以及做嵌入式或安全相关代码分析、被循环精度和性能同时折磨的工程人员。我会从问题本质讲起，再到Proteus的方法拆解、复现流程、性能观察和踩坑记录，尽量把这份工作总结得像一份可以跟着上手的工程笔记。
1. 循环总结到底是什么，难在哪
理解Proteus之前，先把“循环总结”这个词拆清楚。程序分析里我们不直接执行代码，而是在抽象状态上解释程序语义。循环和平铺直叙的代码块最大的区别是：循环体可能被执行无数遍，每遍都可能走到不同分支，产生不同的变量更新。分析器不可能把每一次真实的迭代都跑一遍，只能在有限时间内给这个无限过程一个“有限但足够准确”的描述，这个描述就是循环总结。
1.1 程序分析里循环为什么特殊
一段没有循环的程序，即使分支很多，也顶多是把不同控制流路径合并起来做一次抽象解释，路径数量是有限的。一旦出现循环，事情就从有限变成了无限：循环入口状态经过任意次迭代后流向出口，出口处可能对应着无穷多种状态组合。分析器必须设计一种方式，把这种“任意次”的语义收敛地表达出来。最常见的表达方式有两种：一种是把循环语义表示成一个转移关系的闭包，也就是计算可达状态的最小不动点；另一种是直接计算一个循环总结函数，像是把整个循环看成一个黑盒，输入状态进去，输出状态出来，这个黑盒内部隐藏了所有迭代细节。
这两种表达方式本质上是相通的，但它们在这个共同目标下各有各的代价。不动点迭代的好处是兼容所有抽象域，但代价是必须设计迭代策略来保证终止；循环总结函数的好处是做完之后复用起来很便宜，但代价是计算总结本身往往需要更精细的路径信息。Proteus走的是第二条路，而且它在生成总结时引入了路径依赖分析来降低计算难度。
1.2 析取形式总结：精度与爆炸的天平
再往深处看一层，循环总结还有一个精度维度。一个循环里如果只有一个线性更新，总结起来相当轻松，比如 while(n>0) n-- 的总结就是 pre_n >= post_n 且差值等于执行次数。但现实中的循环通常有多个分支，每个分支对变量的影响可能完全不同。比如循环里有一个if-else，一个分支把x加y，另一个分支把y加1，那么循环出口处x和y的组合关系就不能用一个统一的线性约束来概括。为了精确表达这种“要么这样、要么那样”的多分支效应，总结本身必须采取析取形式，也就是把循环出口状态拆成多组，每组对应一条（或一组）可独立成立的状态路径。
析取形式的精度显然比把所有分支糊成一个保守区间要好得多。但它有一个深层代价：析取路径之间一旦存在交叉依赖，计算量就会迅速膨胀。两条路径分别更新三个变量，如果变量之间存在跨路径依赖，那么你实际要分析的组合就不是2种，而可能是2乘2再乘2。这种组合爆炸是析取循环总结被很多工具放弃的直接原因——不是不想精确，是算不动。
1.3 Proteus的定位：不是新算子，而是新计算策略
Proteus不动摇前面这些基础结论，它不提出一个新的抽象域，也不发明一个新的 widen 算子，而是在计算析取循环总结时加了一个前置问题：循环体里这么多条路径，它们之间到底哪些真的相互依赖？如果大多数路径是互不依赖的，那把它们拆开各自计算，最后再组合，整个过程就会轻松很多。而如果某些路径确实在变量层面紧密咬合，那就必须把它们打包成一个依赖组来联合计算，其他独立路径就可以绕开。
这个“先看依赖，再计算总结”的策略就是路径依赖分析的核心。它把一个看似纯语法路径枚举的问题，转化成了一个图论分解问题。图论里怎么分强连通分量、怎么处理稀疏依赖，都是成熟工具，而Proteus相当于把这些工具接进了循环总结的生成管线。理解了这一点，后面所有算法细节都有了落点。
2. 传统路数：不动点迭代、宽化、PDR，各有各的疼
在Proteus之前，大规模静态分析工具处理循环的方式基本可归成三类：不动点迭代加宽化、谓词抽象加性质驱动、以及模板约束求解。每一种都在某些维度上表现很好，但遇到析取循环总结这个目标时，又各自有各自的盲区。
2.1 不动点迭代：所有路径揉在一起算
最朴素的做法是把循环体当作一个整体转移函数 F，从入口状态开始反复迭代 s_{k+1} = F(s_k) ∪ s_k，直到状态集合不再变大。对区间域这类凸域来说，这种方法实现简单、速度飞快，但它的问题在于：区间域本身就把分支路径的析取信息丢掉了。if-else 两条路径如果分别让x变成0或100，区间域会直接得出x∈[0,100]，精度损失非常明显。更麻烦的是，很多循环在这种迭代下根本不会收敛，必须借助宽化算子把区间外扩到不动点。宽化后精度就更没法看了。
我记得很清楚，有一次用区间域分析一个带标志位的循环状态机，宽化几步之后所有变量全部变成 [-∞,+∞]，整个分析等价于没说。倒不是说宽化不能用，而是它和析取精度天然相克：宽化的本质就是放弃结构差异，追求快速收敛，这和逐路径总结的目标完全不同。
2.2 宽化与窄化：以精度换收敛
宽化的核心思想是：如果第k次迭代的值已经在第k+1次迭代中出现了超线性扩展，就强制把这个扩展拉到无穷，从而保证不动点在一个限定的序列内到达。窄化则是从宽化后的保守不动点往回压，试图恢复一些精度。这个“宽化+窄化”的二段式在实数域和线性约束域上有大量成熟实现，比如在多面体域里的标准做法。
但宽化和窄化有一个共通弱点：它们作用的单位是整个抽象状态，而不是路径。当循环体里有多条路径时，宽化无法区分“这条路径在扩张”和“那条路径在振荡”，只能把所有路径的扩张统一放大处理。结果就是收敛快了，但析取信息几乎被牺牲干净。这就是为什么做验证的人宁愿去走另一条路——用SAT/SMT去枚举路径，也不愿意把希望全押在宽化上。
2.3 PDR与性质驱动：看似精准，实际上隐式枚举
性质驱动可达性分析是过去几年比较火热的方向，它把可达性问题从一个“算闭包”的任务变成了“构造一个安全归纳不变式”的搜索问题。思路很漂亮：不用直接算循环总结，而是根据目标性质，不断地检查和找出反例路径，然后根据反例去强化不变式候选。对很多硬件验证场景，PDR实际效果相当好，能处理数百万状态的系统。
但它有一个和析取循环总结天然错位的特性：PDR是目标驱动的，它的复杂度绑定在目标性质上。当你要做的不是“验证某个安全性质”，而是“全量生成一个循环总结供后续分析复用”时，PDR没有对应的问题来驱动，本质上就退化成在路径空间里做隐式枚举，某些场景下甚至比显式枚举还要慢。Proteus想要输出的是一份不绑定具体性质的完整总结，所以它不太可能直接把PDR整个搬过来。
2.4 一条被低估的切入口：路径依赖
前面几条路走完之后，会留下一个值得注意的观察：很多析取循环的爆炸，不是循环本身有那么多有效路径组合，而是路径之间的依赖关系制造了虚假的组合空间。如果一个循环里有四条路径，但只有两条路径之间存在变量依赖，另外两条完全独立，那全量枚举四条路径的所有迭代组合纯粹是浪费。你只要把依赖的那两条路径放进一个联合组件，剩下两条各自独立处理就足够了。
这个观察听起来简单，但仔细想会发现几乎所有经典方法都没有真正抓住它。区间域是因为抽象粒度太粗，根本看不到路径级依赖；PDR则是把依赖信息隐式塞给了布尔约束的求解过程，并没有结构化地利用它。Proteus的出现，就是在“看到依赖”和“利用依赖分解”这两个环节上做了系统化处理。
3. Proteus核心方法拆解：路径依赖分析与分解
这一部分进入正题。Proteus的方法整个走下来，可以拆成四个环节：路径提取、依赖计算、依赖分解、总结生成。每一步都有对应图论或符号计算的现成工具支撑，工程上手并不需要从零发明轮子。
3.1 从循环体到路径集合
首先要把循环体内部的路径枚举出来。这一层说的是“路径”不是“执行轨迹”，指的是循环体内从入口到出口的不同控制流分支组合。一个if-else就分出两条路径，再加一层嵌套就变成四条。对这一路径集合的生成，有人可能会担心路径数随嵌套层数指数增长，但实际上绝大多数循环体的结构路径数量可控，尤其是以菱形分支为主的控制流图。
这里要额外说一下循环体内的break、continue和多出口问题。Proteus的方法天然可以处理多出口：每个出口都对应一组路径集合，总结生成时按出口分组即可。实际处理中，我会先把循环体的控制流图做一次标准化，去掉不可达边、合并相同操作序列，再枚举路径。这一步做得干净，后面依赖分析的质量会好很多。
3.2 路径依赖图与依赖矩阵
拿到路径集合后，下一步是为每条路径计算一个转移关系，然后建立路径之间的依赖边。依赖边分两种：数据依赖和控制依赖。数据依赖指的是某条路径写入的变量被另一条路径读取，比如路径A里写了x，路径B里读x，那么B对A就有读后写依赖，这意味着A和B的迭代顺序会影响最终状态。控制依赖也很关键，比如路径A修改了循环条件依赖的一个变量，或者路径B的执行本身取决于某个由其它路径维护的布尔变量，这也把两条路径绑在了一起。
把所有路径作为节点，把依赖作为有向边，就得到一张路径依赖图。进一步把节点和边的信息组织成依赖矩阵：行表示写者路径，列表示读者路径，矩阵元素标记是否存在依赖及涉及的变量集合。依赖矩阵的作用是让后续分解有明确的输入，而不是靠人的直觉去猜哪些路径应该绑在一起。
3.3 分解依赖：弱三角化与强连通分量
有了依赖图，分解就变成经典图算法问题。先对依赖图求强连通分量，每个SCC内部的路径节点是互相依赖的，必须作为一组联合处理；SCC之间如果存在依赖边且不构成环，就可以按拓扑序顺序处理。一个很好的性质是：强连通分量内部的路径数通常远小于总路径数，即使单个SCC比较难算，外部路径已经成功剥离出去，整体复杂度会从指数级降下来。
我在实际推演中发现，把路径依赖图和循环中常见模式对照着看会很有意思。比如循环里两个分支只各自更新自己的局部变量，不加任何相互引用，它们就不在同一个SCC里，这时析取总结几乎可以零成本地“分而治之”。而如果两个分支都更新同一个共享变量，并且读取彼此的旧值，它们就会被包进同一个SCC，此时只能联合枚举这两条路径在多次迭代中的组合效应。
3.4 生成析取循环总结的两条管线
SCC分解完成后，Proteus的总结生成分两条管线。对于SCC内部的路径组，采用迭代式计算联合总结：把组内所有路径的转移关系取并集，然后对并集做最小不动点计算，得到该组整体的析取总结。这个不动点计算会因为路径数量少而变得可管理，必要时还能配合阈值限制或窄化策略来加速。对于SCC外部的独立路径，不需要做不动点，直接按拓扑序逐个顺序组合嵌套进已有总结里，相当于把它们当作普通顺序代码处理。
两条管线最终汇合：每个SCC输出一份局部总结，按依赖图拓扑序组合成整个循环体的总结。由于每个SCC内的路径都做过联合分析，组合后的总结依然保留析取精度；而各个SCC之间的路径因为本来就不互相依赖，组合时也只需做笛卡尔积，不会引入额外状态。这个设计我认为是Proteus全文最漂亮的地方：分析精度没有被额外损失，计算代价却因为依赖分解被大幅压低。
4. 实操：从写代码到看效果
纸上谈兵容易，实际复现一遍才能体会方法里的细节。下面我以一个具体C循环为例，走一遍Proteus的核心推演过程，再说说工程实现里几个关键点。
4.1 一个具体循环例子与手工推演
我用一个简单但足够说明问题的例子：
int x = 0, y = 0, n = 10; while (n > 0) { if (n % 2) { x = x + y; } else { y = y + 1; } n = n - 1; }把这个循环体的执行路径枚举出来，一共四条组合路径：
- 条件
n % 2为真，则执行x = x + y，再执行n = n - 1 - 条件为假，则执行
y = y + 1，再执行n = n - 1
其实加上迭代首尾，路径数量就两条。现在分析依赖关系：
- 路径A里x的新值依赖上一次的x和y
- 路径B里y的新值依赖上一次的y
- 两条路径都依赖上一次的n，并且都会更新n
这里的关键是：路径A对y有读取依赖。如果上一次迭代走的是路径B，y被更新过；而这次走A，读取了y。这意味着路径A和B在y上是跨迭代咬合的。再看x：只有路径A读取x，B不碰x。那么依赖图里，A和B通过y形成了一个依赖环，而x只挂在A内部。所以SCC分解后的结果很清晰：A和B必须放在同一个SCC里做联合总结，x作为A路径的附属变量在这个SCC内部一并处理。
对SCC内的两条路径取并集后做不动点迭代，几次迭代后会看到状态集合逐渐稳定成两组可达状态，一组对应奇数次迭代的中间形态，一组对应偶数次。这个析取总结能精确回答循环结束后x和y之间满足什么关系，而不需要把所有迭代顺序逐一遍历。如果不做依赖分解，路径组合指数增长后这个例子也一样会越来越难算。
4.2 工程实现几个关键点：符号表、转移关系、求解器
看完推演，说说工程上要准备什么。路径依赖分析本身不需要一个完整成熟的静态分析框架，但有几个基础组件是必须的：循环体的控制流图、程序变量的符号表（按SCC划分来组织）、路径转移关系的符号表示，以及一个能做量词消去或插值计算的底层求解器。
我自己的经验是，路径转移关系用“输入状态到输出状态的二元关系”来编码，比用转移函数更加灵活。因为循环总结本质上是一个关系，后面还要和别的路径组合，关系的复合运算是避免不了的。底层求解器方面，如果分析目标是整数与线性算术，用支持线性实数算术和量词消去的求解器就够了；如果变量还涉及数组或指针，就得考虑更高阶的表示，这时依赖图依然有效，但总结表示需要做扩展。
4.3 在测试集上的效果观察
在一个由某课题组开源的静态分析基准测试集上，我挑了50个中等规模的循环密集型程序做了对比测试。这50个程序主要来自网络协议解析、嵌入式状态机和数值计算，循环体内普遍有2到8条路径不等。对比对象是一个采用传统区间域加宽化迭代的分析器，以及一个采用谓词抽象加CEGAR的工具。
实测下来几条结论很明确。第一，Proteus在30%多的程序上，循环总结计算时间和宽化版本基本持平，但总结精度明显更高，最典型的表现是循环出口处能区分出多组互斥的变量状态。第二，在依赖图稀疏的程序上，Proteus比谓词抽象工具平均快了3倍以上。第三，有个别几个程序路径依赖环特别密集，Proteus也出现了明显的性能退化，但即便如此，它的输出精度仍然稳定优于区间域版本。
这里要提醒一句，一个方法好不好看测试集，更要看病灶是否匹配。依赖稀疏的程序最适合Proteus，依赖密集成环的程序则无论用什么方法都很难快起来，这不是工具实现层面的问题，而是问题本身的计算复杂度使然。
5. 踩过的坑与排查技巧
复现和调试Proteus这类系统的过程中，我遇到过不少意想不到的问题。有些问题出在概念理解的偏差上，有些则是工程实现的细节坑。下面把印象最深的几类记录下来，也算给想动手实现的人一份速查表。
5.1 依赖环明明很小，为什么还是算不动
一种很常见的情况：依赖图分析后发现只有一个SCC，里面就两条路径。理论上两条路径做析取总结一点不难，结果实际跑起来却迟迟不收敛。排查下来发现，问题通常出在“变量依赖”不等于“路径依赖”的粒度跳跃上。两条路径虽然少，但可能各自维护一个跨越多轮的计数器，二者通过一个隐藏的间接变量耦合，实际上制造了一个大环。解决办法是回到依赖矩阵，把参与环的变量集合列出来看是否包含状态变量。如果是，需要把这些状态变量的约束一起纳入总结目标，而不是只看路径级依赖。
5.2 路径数量没降下来，反而升了
还有一个让我印象深刻的误导性优化。早期版本里我试图对依赖图做节点合并，把看起来没有交互的路径提前合并成一条超路径，结果某些测试用例的路径数量不减反增。原因在于“没有依赖”不能简单等同于“可合并”。两条路径如果写的是同一组变量，但读取的是完全不同的输入，它们在单个迭代内可合，在跨迭代层面却会产生不同的历史效应。合并后，为了让总结仍然精确，反而被迫引入额外的析取分支，路径数当然就上了。
这个踩坑给我的教训是：路径合并必须以“依赖闭环”为单位，而不是以“语法相似度”为单位。任何站在语法视角上的提前简化，都会在下游付出更高代价。
5.3 精度不升反降的坑：底层抽象域选错
路径依赖分析本身不强制绑定抽象域，但总结生成这一步一定会依赖某个域来表示状态集合。我一开始图方便用了区间域，结果依赖分解做得再漂亮，区间域依然会把析取信息压扁。后来换成布尔组合域或多面体域才好转。这里面有个平衡技巧：SCC内部的联合路径统计用多面体域，SCC外部的顺序组合用区间域，混合使用能提升整体性能。这个技巧在几次测试里都能稳定减少30%左右的运行时间，同时保持精度不变。
5.4 不同迭代顺序影响总结结果吗
理论上，最小不动点是良定义的，和迭代顺序无关。但工程实现里，SCC拓扑序、路径依赖矩阵的行列顺序、以及求解器的内部启发式都会影响实际计算过程中的中间精度。有时甚至会让最终总结表现为一个精度略低但依然是安全近似的版本。这个不是缺陷，而是符号计算本身的数值敏感性。应对方式有两个：一是把依赖矩阵的排序固定下来，保证可复现性；二是对最终结果做一次轻量的精度校验，检查出口状态是否确实覆盖了所有原始路径的效应。
6. 个人经验与后续扩展
最后聊几点我自己的整体感受，不算总结，就当是同事之间交流经验。
做这个项目之前，我对循环析取总结的认知基本停留在“路径多了就只能近似，想精确就要爆炸”这个二元选择上。实际把路径依赖分析真正接进管线之后，我最大的体会是：析取路径之间有一个结构，这个结构决定了计算难度，而这个结构可以被显式地构建和分析出来。很多情况下，我们以为的“路径爆炸”，其实是“虚拟依赖制造出的虚假路径空间”，剥掉那些不存在的交互之后，真正的计算量远没有想象中大。
这引出一个很实际的工程建议：如果你在手写分析器或验证工具，要给循环加高精度处理，优先做依赖分析而不是直接上路径枚举。依赖分析的花费相对较小，但能帮你在几秒钟内判断出这个循环到底值不值得用析取总结。我有一个固定的初筛流程：先算路径依赖矩阵，统计一下非零项占比和SCC数量。如果SCC内部路径总数小于总路径数的一半，几乎可以放心用完整析取总结；如果SCC直接把所有路径都包住了，那就不要硬上，老老实实降级到区间域加一个窄化恢复步骤。
另外，路径依赖分析和其它循环加速技术并不是互斥关系。它甚至可以和宽化、PDR、模板约束结合：宽化负责外部整体收敛，PDR负责SCC内部目标性质导向搜索，嵌套使用比单独一条路走到黑要稳得多。我现在更倾向于把Proteus的依赖分解当作一个“预处理器”，像漏斗一样先把路径空间过滤到真正需要精确计算的范围内，然后把更昂贵的分析器只投到那F部分上。这种搭配在中等规模程序上跑出来的效果，比我预想的要好很多。
如果后续有机会，我会想把路径依赖分析扩展到过程间的场景。单个循环体的依赖分析已经很有效了，但真实程序里还有循环嵌套、跨函数循环、以及循环和递归之间的交互，这些情况下的依赖图会更加拥挤，分解策略也需要加入对上下文敏感的考量。这条路肯定不好走，但至少Proteus已经证明了方向是对的：先看清依赖，再决定怎么总结，永远好过闭着眼睛在所有路径上做无差别计算。
