Widening 与 Narrowing

Widening 的两项责任 ​

在抽象域公理库抽象域Abstract domain · Domain of abstract properties用带精度次序和合流运算的抽象元素表示具体状态集合，为可靠静态近似提供语义空间。 $(A,⊑)$ 上，二元操作 $\mathrm{\nabla }:A\times A\to A$ 是 widening，若至少满足上界性

$$x⊑x\mathrm{\nabla }y,y⊑x\mathrm{\nabla }y,$$

并且对任意上升链 $x_0⊑x_1⊑\cdots$，序列

$$y_0=x_0,y_{n+1}=y_n\mathrm{\nabla }{x}_{n+1}$$

在有限步后稳定。不同教材给出等价或更一般的序列式定义，核心都是“结果保持可靠上界”和“加速序列最终稳定”。

Widening 通常不是格 join，不要求结合、交换、幂等或单调公理库偏序集上的单调映射Monotone map on posets · Order-preserving map · Isotone map在偏序之间保持次序的映射，以及它作为单调算子参与不动点迭代时的基本结构。。擅自依赖这些代数律会让 worklist 次序变化时出现未经证明的结果。

区间上界跳跃 ​

经典区间 widening 对 $[l_0,u_0]$ 与新值 $[l_1,u_1]$ 定义

$$[l_0,u_0]\mathrm{\nabla }[l_1,u_1]=[l^{\prime },u^{\prime }],$$

其中若 $l_1<l_0$ 则 $l^{\prime }=-\mathrm{\infty }$，否则 $l^{\prime }=l_0$；若 $u_1>u_0$ 则 $u^{\prime }=+\mathrm{\infty }$，否则 $u^{\prime }=u_0$。

循环 x:=0; while (...) x:=x+1 的普通 join 迭代产生

$$[0,0],[0,1],[0,2],\dots$$

永不有限稳定。首次增长时 widening 可从 $[0,0]$ 与 $[0,1]$ 跳到 $[0,+\mathrm{\infty }]$，下一轮保持不变。

这个结果可靠却很粗。它不是“猜测真实上界无穷”，而是主动放弃不断移动的有限上界，以保证分析终止。

放置点与延迟策略 ​

不必在每个控制流节点都 widening。常见策略只在循环头或反馈边使用，使无环区域仍以精确 join 传播。选取覆盖每个循环的 widening points 是终止证明的一部分。

可以先做若干普通迭代，再启用 widening；或采用 thresholds，只允许边界跳到程序常量 $10,100$ 后再到无穷。它们常提高精度，却需证明任何无限增长最终仍会越过有限阈值并稳定。

迭代次序会影响结果。两个语义等价的 CFG 排序可能触发不同 widening 时机，因此工程报告应说明策略，不把输出当成唯一最小解。

Narrowing 恢复精度 ​

得到后不动点 $y$ 后，可用 narrowing $\mathrm{△}$ 生成下降序列

$$z_0=y,z_{n+1}=z_n\mathrm{△}{F}^{\mathrm{\#}}(z_n),$$

要求在不低于所需具体解的前提下收紧，并在所考虑下降序列上终止。区间 narrowing 常把无穷端点替换为 transfer 计算出的有限端点。

若循环实际条件是 x<100，widening 得 $[0,+\mathrm{\infty }]$ 后，guard 与一次或数次 narrowing 可能收紧到 $[0,100]$。narrowing 不保证回到最小不动点，也不能恢复 widening 丢掉的所有关系信息。

没有可靠上界就开始下降可能漏状态。顺序必须先获得 post-fixpoint，再在保真条件下改进；把 narrowing 当任意“优化结果”的后处理没有证明依据。

失败边界 ​

若所谓 widening 只返回第二个参数 $y$，它在上升链上是上界，却可能沿 $[0,n]$ 永不稳定，因此不是 widening。若返回第一个参数 $x$，会稳定但未必覆盖新状态，也不可靠。

过早 widening 到 $\mathrm{\top }$ 会让分析快速终止，却产生大量假警报。过度延迟则可能耗尽资源。终止保证与实际精度是需要测量的权衡，不靠更换循环常数的伪例证明。

并非所有有限高度域都需要 widening：普通单调迭代已会稳定。加入 widening 只会引入额外不确定性，违背最小必要机制。

对嵌套循环，外层和内层 widening point 的调度会互相影响。内层尚未稳定就把粗结果送到外层，可能触发不可逆的无穷边界；完全求稳内层又可能重复昂贵计算。局部 WTO 等策略用控制流的嵌套结构规定更新次序，但每种策略仍需证明所有反馈环最终经过 widening 点。

参考资料

• Patrick Cousot and Radhia Cousot, “Abstract Interpretation: A Unified Lattice Model for Static Analysis,” POPL, 1977, pp. 238–252。
• Patrick Cousot and Radhia Cousot, “Comparing the Galois Connection and Widening/Narrowing Approaches,” PLILP, Springer, 1992, pp. 269–295。
• Xavier Rival and Kwangkeun Yi, Introduction to Static Analysis, MIT Press, 2020, Ch. 10。