在程序分析这块摸爬滚打久了你会发现一个特别扎心的现象处理十个以内的函数调用大家都问题不大一旦遇到带复杂路径的循环很多工具瞬间就从“可靠分析”退化成“猜谜游戏”。我一度重度依赖抽象解释和枚举展开去处理循环结果不是false alarm满天飞就是分析器跑着跑着直接不终止。后来接触了Proteus系统“通过路径依赖分析计算析取形式的循环总结”的思路才算把这条路上的坑看明白。这篇内容想做的就是把析取形式的循环总结disjunctive loop summary和路径依赖分析path dependency analysis放在一起拆一拆适合正在做静态分析、符号执行、或者是被循环造成误报困扰的同行参考也适合想理解“为什么一句循环总结那么难求”的研究生和技术爱好者。我会尽量用我们在实际调试某个跨平台代码扫描系统时遇到的场景来讲不绕弯子。1. 为什么循环总结不能靠“把循环展开几遍”来解决1.1 循环总结到底是什么又在解决哪一类痛点循环总结简单说就是把一段循环从“执行前的状态”映射到“执行后的状态”的一个抽象关系或者是一个精炼后的不变式集合。听起来很好理解但真正做程序分析的人都知道循环是分析器最大的死穴。一次循环退出后程序状态到底怎么变化路径不同、迭代次数不同结果截然不同。拿一个典型的指针遍历来说循环里出现了条件分支一边更新结构体的某个字段另一边走另一个逻辑。把循环展开几次原则上能看到一条局部轨迹的轮廓但真实程序的循环往往有几百几千次迭代。你不可能把几十个展开副本全部枚举完。这就是经典的“无限路径”困境。抽象解释的做法是用一个不动点迭代去逼近用一个抽象值域把所有路径合并成一个“过近似”听起来很优雅但它丢掉的东西恰恰是析取总结想要保住的——“每类路径到底是什么条件下走的”。1.2 合取形式的不变式为什么报错时特别苍白我举个例子一段循环内部有两条明显互斥的路径一条路径里x严格递增另一条路径里x被重置为0。传统的抽象域如区间域或八边形域最终会得到一个合取的不变式比如x 0。这句话没有错但它完全没告诉你x在哪类路径下会变成0在哪类路径下会保持生长。这对做缓冲区分析的坏影响很明显。给循环做上下文摘要时调用方若看到x 0只能采取最保守的策略而析取形式的总结能把状态空间划分为“轨道”每条轨道保留资格条件。于是后面的分析可以区分“进来之前的标志位不同导致循环内行驶路径完全不同”这样的关键事实。Proteus的核心目标就是在合理的算力下拿到这种析取总结而不是简单粗暴地丢一个过近似的不变式跑完全程。我觉得这里必须强调一个反直觉的点析取不是表达越细越好而是要根据路径依赖关系决定什么该析取、什么该合并。如果对每一条迭代轨迹都单独保留状态数会指数爆炸但如果完全合并得到的就是合取不变式等于没做。路径依赖分析就是来解决“以什么标准切分状态”这个问题的。2. 路径依赖分析的关键前提先把“状态”按路径资格分好组2.1 从一个带条件分支的循环看状态分组的必然性我们先看一段我非常常用的测试片段int i 0; int flag nondet(); while (i n) { if (flag 0) { a[i] 1; i 2; } else { a[i] 0; i 1; } }这段循环很简单但如果你只用区间域去分析i最终的范围最多得到一个“上界约等于n”的粗糙结论。你看不出i在哪条路径下更快到达上界也看不出数组不同位置写入的值和flag的依赖关系。路径依赖分析的做法是先抽出一条条“路径片段”。所谓路径片段不仅包括循环体内部的基本块序列还包括触发这条序列的路径条件。上面这段循环里最重要的路径条件就是flag 0。由于flag在循环外就可能被符号化分析器需要建立一条依赖链循环头是否能执行 → 依赖i n→ 循环内走真分支还是假分支 → 依赖flag 0。把这两条路径分离然后分别跟踪各自的变量转移关系得到的就是类似这样的析取总结在flag 0的路径类里i每次增加2在flag 0的路径类里i每次增加1。这样的总结在后续调用点非常有用——比“i 最终不小于 0 且不大于 n”有意义得多。2.2 路径依赖分析与符号执行、抽象解释的区别符号执行也能得到析取式路径摘要但它是把程序完整地路径枚举出来。一旦循环里嵌套循环符号执行就要处理路径约束的指数增长。抽象解释是在另一边它用一个抽象域做宽度优先的合并精度低但能保证终止。路径依赖分析恰好落在两者中间它基于控制流的“轨道”划分来切分状态空间并对轨道内部做抽象解释或符号转移。换句话说它在精度保证和可终止性之间找了一个工程可接受的折中点。我看到很多分析器实现到一半就放弃了原因是路径分组策略太粗或者太细。太粗等于退回合取域太细则符号约束数量爆炸。Proteus这类系统真正有价值的部分就是一套成体系的“该分组到哪一层、什么时候合并”的算法。2.3 一个生活化的类比航班航路图你可以把路径依赖分析想象成规划航路图一条航线从A到Z中间经停很多机场。如果只告诉你“这个航班最终到达Z”确实没错但你无法判断它在哪个中转站遇到了延误。析取式总结更像是把航线按天气条件切分晴天走北线雷雨走南线。路径依赖分析做的是先把“天气”这个决定性变量识别出来再分别评估南北两条线路的到达时间区间。这样你后续做延误分析或流量调度时才不用假设每条航线都走最坏情况的雷雨路径。程序分析也是这样调用循环总结的外部代码不需要用最悲观的状态去对接而可以根据调用点时实际的分支条件选一条更精确的轨道来对接。3. 从路径条件抽取到轨道划分Proteus风格的核心工作流3.1 第一步控制流图预处理与路径切片实际开始计算之前要先把循环边界和控制流图处理干净。以LLVM IR为例第一步是规范化循环识别出循环头、退出块、回边。然后对循环体内部的所有基本块跑一次路径切片。路径切片不是简单的“去掉不相关语句”而是要保留所有影响循环转移关系的条件。比如上节例子里flag 0影响循环体选择哪条路但这段代码写在循环外切片的时候很容易被当成普通的赋初值语句剪掉。我的经验是切片必须沿着“控制依赖”回溯而不仅仅是数据依赖。flag虽然没在循环内被修改但它通过控制流影响a[i]的写入和i的增量因此它必须作为一条路径资格被保留。这个阶段输出的是一组路径片段。每个路径片段形如片段 ID: P1 入口条件: flag 0 更新: a[i] 1; i i 2 循环继续条件: i n路径片段是后续析取总结的最小单元。有人说直接按基本块路径二分会爆炸其实不会因为程序正常写出来的循环内部有效路径数量通常很有限关键要抓住“真正的分叉点”而不是每个算术比较都当分叉。3.2 第二步构建路径依赖关系而不是直接算不变式拿到路径片段后不能急着交给抽象解释去跑不动点。得先做一件事构建路径依赖关系图。这个图回答的中心问题是“哪些路径资格条件互相影响”考虑一个更复杂的例子while (k 100) { if (k % 2 0) { x 2; } else { y 1; } k; }这里的路径资格条件是k % 2 0和k % 2 ! 0。但k自己也在循环内更新所以这两条路径资格不是静态的而是随着循环迭代不断切换。路径依赖分析要把“k的奇偶性”作为循环归纳变量去处理然后判断对于奇偶路径变量变化规律是什么。在做依赖分析时有个必须强调的工程细节依赖一定要闭包。k的变化可能导致x或y的变化而x、y又可能影响循环退出条件。如果在做依赖闭包时不追踪k对自身奇偶性的影响很容易把路径资格条件错误地当成常量最终总结精度严重受损。3.3 第三步按轨道运行抽象解释或符号转移路径依赖图建好后下一步是把状态空间划分成若干“轨道”。每条轨道对应于一组固定的路径资格组合。上面奇偶性例子可以划分成“偶迭代轨道”和“奇迭代轨道”分别跟踪x、y的变化。轨道内部可以用区间域跑不动点。比如轨道P1偶数迭代循环执行约50次x 2执行了约50次那么x的增长区间是[0, 100]轨道P2奇数迭代y增长约50次。最后把两个轨道合起来得到析取总结轨道 T1: (k % 2 0), x ∈ [0,100], y 不变 轨道 T2: (k % 2 ! 0), y ∈ [0,50], x 不变有人问为什么不直接对x和y分别算区间再并起来因为分别算区间后你丢失了“x增长时y不动”这种关联信息。析取总结的价值不是只算区间而是要生成一个“处处带着条件的关系式”。3.4 第四步反例引导的收敛与细化轨道划分之后还有一个关键的闭环检验当前析取总结对后续分析是否足够。如果分析下游代码发现还需要区分更多路径系统会根据失败的反例自动往更细的轨道切。比如某次下游分析要求知道“当 flag 大于2 时i 的步长是否为2”原有的“flag0”轨道就太粗必须进一步切分。这一步其实是绝大多数开源分析器做得最差的地方。很多实现跑完一遍就收工不会主动去构造反例。Proteus风格的系统会在生成循环总结后用一个小型的符号执行器去验证总结的保真度挑几条代表性路径让符号执行器跑真实路径再和总结预测的结果对比。不一致就说明轨道切分或转移函数有问题需要反哺到第二步。4. 跑通一个小例子从C片段到析取循环总结的完整流程4.1 示例程序和它的分析目标我们来完整推演一遍。基础代码int flag read(); int x 0; while (x 10) { if (flag 0) { x x 2; } else { x x 1; } }分析目标是生成一个循环总结供其他函数多次调用这个循环时使用。注意flag在循环内不被修改所以这是一个非常典型的“路径资格随调用环境变化”的场景。如果调用点环境是flag positive那么循环实际上只走增量2分支循环大概执行5次退出如果调用点环境flag nonpositive增量1分支大概执行10次退出。一个理想的析取总结应当把这两条轨道分开调用方可以根据自己的flag取值选择轨道而不必把两种情况都算进去。4.2 控制流简化与路径资格提取第一步把flag 0从循环条件里单独抽出来。它虽是外层条件但直接控制循环体内路径。此时路径依赖分析建立一条依赖循环头退出条件x 10依赖xx的增量依赖flag 0。于是形成一个简单但完整链路。如果用合取域区间分析最终得到x ∈ [0,10]。这结论合法保留但对调用点帮助有限到底循环执行几次如果是递增2分支执行5次递增1分支执行10次。从“x ∈ [0,10]”不能可靠推出循环迭代次数。析取总结的目标则是分别给出两个轨道并在轨道上标注退出条件。4.3 轨道划分与不动点迭代轨道划分后分别跑一个小型值域分析。轨道T1的路径条件是flag 0转移关系是x x 2循环退出条件是x 10。区间迭代很快收敛初始x 0反复应用x x 2且要求x 10最坏情况下循环执行5次退出。轨道T2的条件是flag 0转移关系x x 1最坏执行10次退出。两个轨道合起来得到如下总结轨道路径条件循环退出时 x 状态迭代次数上界T1flag 0x ∈ [10, 11]5T2flag 0x ∈ [10, 10]10这个表格比单个区间x ∈ [0,10]信息量大了不少。至少在数值分析时调用方可以根据实际flag的正负选择一个精确的循环次数上界而不是两侧同时估满。4.4 下游分析如何受益继续往下接函数后面有while(...) { ... }或者一个memcpy边界检查。如果只拿到x ∈ [0,10]缓冲区边界分析必须考虑 x 从0到10所有可能且迭代次数上下界耦合但拿到轨道T1和T2后可以精确地知道“当 flag 0 时这段循环最多跑5次x 约为10”因此后续数组下标都是在安全范围内。这就是析取总结在真实代码分析里的价值。它不是一种炫技的表达而是能让下游分析真正减少误报的“基建”。5. 状态爆炸与不终止跑析取总结最容易踩的几个坑5.1 坑一路径资格条件太多轨道数量指数级增长最常见的翻车场景是循环里连续出现三四个独立条件路径依赖分析老老实实建了一条完整依赖每个条件都二分于是轨道数量瞬间变成2^k。当k 8时256条轨道已经很难跑k 20时直接退出。我处理过的一个模拟项目X中有一段权限校验循环里面每个分支都用type 1 || type 2之类的多重条件做判断。直接建轨道组合数轻松上百。应对策略是“代价引导合并”先跑一遍每条轨道的转移关系和变量转移强度把那些转移关系完全相同或高度相似的轨道合并成一组。比如flag 0和flag 10如果对变量更新的效果完全一样就不要当成两条轨道。实际操作中我一般设置两个参数最大轨道数比如64条和合并阈值。当轨道数超限时优先合并那些“路径条件互斥且变更行为一致”的轨道而不是随机丢弃。5.2 坑二迭代不终止尤其是嵌套循环外层循环内有一个内层循环内外层各自有不同的路径条件时路径依赖分析很容易挂掉。原因在于内层路径资格往往依赖外层变量而外层变量又在内层循环中被修改这导致依赖循环。如果不加保护分析器在构建路径依赖闭包时会出现环。在Proteus这类系统里一般会对路径依赖图做“分层”把不变量层如全局变量、循环外常量和内层归纳层分开。凡是在闭包中出现回边且没有归纳变量支撑的直接退化为合取域处理。这个方法不完美但能让分析器保持终止性同时保住绝大多数真正有用的析取信息。5.3 坑三符号约束求解太慢卡在Z3这类求解器上生成轨道后经常需要判断两条轨道的可满足性比如判断某个反例对应的路径条件是否真的存在。这会频繁调用SMT求解器。一旦遇到非线性约束等待时间就相当长。我见过一个案例某个循环的路径条件里出现了乘法flag * k threshold求解器在判断路径存在性时跑了几分钟没返回。这个问题的应对是路径依赖分析阶段不要把SMT求解当成主力只在关键的路径条件可满足性验证时用。更宽泛的轨道探索用轻量的线性近似即可。5.4 坑四阈值设得太紧导致析取总结退化成合取很多人担心状态爆炸就把合并阈值设置得很激进结果却把有效轨道全部合并掉了。比如flag 0和flag 0两条路径变量更新方向完全相反但因为合并阈值设置的比较“贪心”分析器把它们合并成一个区间总结精度大幅下降。这里有个我试了多次后觉得合理的经验优先按“变量变更关系”而不是“状态空间数量”来决定析取。如果两条路径对相同变量的更新函数完全一致哪怕路径条件不同也值得合并如果更新函数方向相反或改变不同变量即使只差一点点也要保留分离。以更新结构为准不以路径个数为准。6. 和现有循环推断工具的取舍什么时候该用析取总结什么时候不必6.1 合取式循环不变式的适用场景必须承认析取式总结不是万能的。如果循环体是简单的累加器比如sum arr[i]一个普通的线性约束或区间不变式就够用了。用析取总结反而增加开销对下游分析没有明显改善。我在处理一个数值积分模块时循环内只有一个更新操作路径条件也不多。直接用区间域跑一个迭代就收敛了析取根本没有用武之地。所以这不是一个“越精确越好”的问题而是一个“精度收益是否值得额外开销”的问题。6.2 什么场景下只有析取总结能解决问题有两个典型场景非析取不可。第一个是循环内路径改变的是控制流走向且路径选择依赖于后续退出条件。比如前面说的flag片段如果没有轨道分离下游几乎不可能准确推断迭代次数。第二个是多阶段循环前半个循环用一种更新后半个循环用另一种更新而且切换点依赖循环内条件。这类循环在协议解析和状态机模拟里很常见合取域几乎无力应对。6.3 代价对比从工程角度看要不要上析取我自己实操下来一个基于路径依赖分析的循环总结系统单循环分析时间往往比传统区间分析慢几十倍。但它们不是替代关系更像是一套分析流水线里的先后关系普通函数用快速抽象域遇到被高频调用且内含多路径的循环再升级到析取路径依赖分析。在这个流水线里最重要的是“启动标准”。我自己的经验是两条其一循环体内部至少有两个互相排斥的有效分支其二这个循环所在函数在调用图中被引用超过一定次数。两者都满足才推进到析取计算否则一律用合取域。下面是某模拟项目X中做的对比可以直观感受一下分析模式单循环耗时对下游误报率影响可扩展性纯区间域约1ms误报率高约30%好路径依赖析取约20-50ms误报率降至约6%需要控制轨道数纯路径枚举分钟级甚至不终止误报率最低差这些数字不一定代表所有场景但方向是对的析取总结的精度收益非常显著但你必须管住轨道数量和终止性。7. 关于轨道划分策略与实际代码调试的一些心得7.1 以“更新结构”为准划分轨道在真正调试模拟项目X的循环分析器时我最开始是按路径条件完全展开轨道的效果很差。后来改成动态判断每条路径映射先提取对变量的“更新效果签名”完全相同的才归并。举个例子两个分支分别是if (a 0) { x 2; }和if (b 0) { x 2; }虽然路径条件不同但更新效果都是x 2那就当一条轨道处理。等下游分析需要追踪a和b的差异时才重新细分。这个思路对内存和多路条件特别有效可以让轨道数控制在个位数同时不丢失关键信息。7.2 验证总结不要只验证“成立性”还要验证“充分性”很多做循环总结的人只关心最后的不变式是否正确也就是“成立性”所有真实执行路径的结果都在总结范围内。但析取总结还有一个更隐蔽的问题——“充分性”总结是否足够精确让下游分析拿到后能做出更准确的判断。打个比方循环结束后x真的永远是正数但你给下游的总结是x 0虽然正确却因为太弱下游分析没法判断另一段代码中x是否可能为0从而被迫走保守分支。生成总结后我的经验是做一次“可满足性抽查”构造几个下游判定条件看总结能否给出一致结论。看到某个assert在真实运行时一定不会触发但总结却说“可能触发”那就说明总结精度不够得重新轨道切分。7.3 和插桩测试结合形成半自动验证闭环纯形式化验证成本高纯测试又覆盖不全。我现在的做法是把析取总结的预测和实际插桩运行做对比。选几百组随机的flag和n组合插桩记录真实循环的退出次数和关键变量终值再和总结预测的轨道范围比对。一旦发现偏差就从偏差组反推是哪条路径片段漏了或转移关系错了。这个方法有点土但非常有效。它不依赖复杂的证明框架只要被测循环能跑起来就能快速定位问题。8. 扩展方向路径依赖分析在更大代码库中的整合思路如果只是针对单循环建立析取总结就好比只给一栋楼做了消防通道规划。真正要落地需要把不同循环的总结挂到函数摘要之上并在调用点做轨道匹配。我在一个跨平台代码扫描Demo里试过一种分层方法函数A的循环得到轨道T1、T2在函数A出口处根据T1、T2分别生成函数摘要。调用函数B时看见调用点实际条件更贴近T2就直接以T2作为进入A时的初始状态不再重复分析A内部的其他轨道。这相当于“按需展开析取”既保留了路径依赖信息又避免把整套析取空间全部撒出去。这个思路的代价是函数摘要不再是单一关系式而是一个带路径条件标签的析取集合。做下游分析时不能简单地“拿一个状态跑一遍摘要”而要遍历可匹配的轨道。幸好轨道数量通常可控实测中大多数公有函数摘要也就三到五条轨道。另外如果把路径依赖分析和指针分析结合还能追踪一些“结构体字段之间的关系”。比如循环里有if (p-kind A)路径资格不只是一个标量条件而是p-kind的取值。此时析取总结可以输出类似“kindA的轨道上next指针字段始终非空”的更有用的关系。这比单纯区间分析实用许多。我目前在这个方向上的实践还没完全跑顺但已经能看到收益。在模拟项目X的一个模块里加入结构体字段路径资格后原先由于字段状态不确定导致的误报下降了将近一半分析时间只上升了约10%。9. 最后说说我自己对析取循环总结的真实体会说实话我刚接触路径依赖分析时一度觉得析取总结不过是一种表达风格把合取域打散成多个子域而已。真正动手修正一版循环分析器后才发现最大的坑根本不是表达方式而是“什么时候析取、什么时候合并”这个度。切得太细轨道几何级增长分析器老态龙钟切得太粗高高举起轻轻放下还得靠下游兜底析取的价值又体现不出来。后来在一次针对嵌套循环的状态爆炸排查里我试着把“更新函数相同”作为归并标准轨道数从68条下降到了7条下游误报率反而基本没变。那次之后我才算真正理解析取式总结的意义不是尽量多地保留路径而是在路径资格条件真正影响变量变化关系时把这种影响关系原样保留下来。条件再多只要不影响转移函数大可以放心合成一条轨道。目前我维护的循环分析流程基本默认对高频调用函数开启路径依赖分析并设定轨道合并阈值。跑了几轮真实代码后整体误报率稳定在一个可接受范围分析时间也在可控区间。如果你也被“循环总结太粗、下游分析被迫往最坏情况猜”这个问题困扰我建议手上准备一个能快速验证“总结充分性”的插桩工具别只对着证明器纠结。先在小规模真实执行上下手把轨道分组标准调顺再上大代码库整个流程会顺滑很多。