程序切片 | Codeboy's Blog

形式陈述

准则先于删除

程序切片要先说清楚保留什么。本页沿用程序依赖图的无循环结构化整数语言，并固定末尾 return r 为观察准则 $c$ 。全部表达式纯粹且总定义，原程序每条路径的读取都有定义；无异常、堆、外部 I/O 和并发。目标是对每个输入 $a$ 保持

\operatorname{return}(P,a)=\operatorname{return}(P_c,a).

输入接口保留，其他局部变量的最终值不在观察中。由于两程序都无循环且操作总定义，终止在这个模型里自动成立；这里没有给一般含循环程序证明终止等价。

在依赖图上，从 $K_0=\{c\}$ 开始反复加入所有指向已选节点的数据或控制前驱：

K_{i+1}=K_i\cup\{u:\exists v\in K_i,\ (u,v)\in E_d\cup E_c\}.

有限图上得到最小反向闭包 $K$ 。把不在 $K$ 的赋值换成 skip；保留所选判断及其原分支结构。若一个判断及两边全部语句都不在 $K$ ，可将整个条件语句删成 skip。最后去掉顺序组合中的空语句，得到可执行切片。

本页只对结构化语法这样重建。不能从任意 CFG 删除节点后随意连接剩余边，也不能把选出的语句按编号重新拼成无条件列表。

何以保持返回值

对相同输入，把原执行与切片执行中的保留节点对应。每个保留判断的读取来源都在数据反向闭包中；因此其变量取值与原执行相同，分支选择相同。每个保留赋值的操作数也相同，赋值结果随之相同。

关键是“最近写入”不会被偷偷换掉。如果原路径上某次赋值给一个保留读取供值，到达定义边就把它纳入 $K$ 。决定这次赋值是否执行的外层判断又经控制前驱闭包被保留。没有相关后代的删除分支只执行被删赋值，不改变下一个保留读取所需的值。按结构化命令和执行顺序归纳，最终保留的 return r 得到同一值。[1]

这是给定模型下的观察保持结论，不是对所有变量、执行时间或外部行为的全等价声明。

直觉

问返回值，不问所有工作

前页程序先计算 a=x+1、junk=y*y、r=0；随后在 x>0 时根据 y==a 将 r 改成1或2，最后更新 junk 并返回 r。只问返回值时，junk 的两次计算可以一起去掉。

但不能只沿变量名 r 找赋值。r:=1 是否发生取决于两个判断，第二个判断又读取 a，所以 a:=x+1 也必须留下。数据依赖解释“值从哪里来”，控制依赖解释“为何恰好走到这个赋值”。

例子与边界

从9逆向走到稳定

以9号 return r 为起点，闭包逐步为

轮次	新加入的节点	理由
0	9	观察准则
1	3、6、7	三个可能到达的 `r` 定义
2	5	决定6或7执行
3	1、4、0	5读 `a,y`，受4控制；输入0提供 `y`
后续	无	1与4所需的 `x` 已由0提供

闭包为 $\{0,1,3,4,5,6,7,9\}$ 。输入0保留，九个原语句节点中保留七个、删除2和8，得到

text

a := x + 1
r := 0
if x > 0:
    if y == a:
        r := 1
    else:
        r := 2
return r

输入 $(0,0)$ 返回0， $(1,2)$ 返回1， $(1,0)$ 返回2。下载复算在 $[-2,2]^2$ 的25组输入上逐项比较原程序和切片；正文的结构归纳才承担所有数学整数输入的结论，有限测试不替代它。

静态与动态的量词不同

这个静态切片服务全部输入。若仅观察输入 $(0,0)$ 的一次实际轨迹，4为假，6和7都没有执行。围绕该次执行得到的动态切片可以更小，但它只承担这次输入及所选观察的保持责任；把这种结果拿去处理 $(1,2)$ ，可能错误返回0。

本页不实现一般动态切片。仅说明两类任务的区别：静态切片的依赖来自所有可能路径，动态切片还带指定输入和执行实例。静态切片通常也不最小：保守不可行路径会多留节点，代数恒等或两个分支同值等语义化简又可能继续缩小程序。

三个不能越过的边界

如果省去控制边，仅保留 r:=0; r:=1; r:=2; return r，会把本来互斥的赋值顺序执行，任何输入都返回2。反向可达性给出节点集合，语法重建仍是正确性的一部分。

如果被删除的2号赋值改成 junk:=1/y，而语言把除零定义为异常，则 $y=0$ 时原程序报错、切片可能返回。它违反本页总定义假设；若要保留异常，应把异常结果加入观察并补充依赖，而非继续套用当前定理。

如果在返回前放入不影响 r 的无限循环，删除它可能让原本不返回的程序返回。只看终止轨迹上的值和要求保留发散是不同规格；含循环切片必须另给其终止或发散处理规则。[1的原始讨论也明确限定所研究的终止轨迹。]

推论与应用

闭包成本与反例接口

图已建好时，用反向邻接表和队列实现闭包：节点首次发现就标记，每个节点最多出队一次，每条相关反向边最多扫描一次。包含建立反向表和遍历原语法的成本，时间为 $O(|V|+|E_d|+|E_c|+L)$ ，空间为 $O(|V|+|E_d|+|E_c|+L)$ ； $L$ 为源语法大小。不能把前页的依赖分析成本也声称为线性闭包的一部分。

若外部检查规格为 return != 1，切片保留的返回函数相同，所以原程序与切片拥有相同的失败输入集合。符号执行可以在更小程序上求出 $(1,2)$ ，再回到原程序重放；这给删减、搜索与证据建立了明确接口。

迁移练习：把第8行改为 r:=junk 后重新求切片。保留输入0、2、8、9即可，1、3、4、5、6、7都不再影响最终返回；切片返回 $y^2$ 。如果沿用旧切片并只追加8，会读未定义的 junk，直接暴露“修改代码后必须重新分析”的责任。

参考资料

[1] Mark Weiser，Program Slicing，IEEE Transactions on Software Engineering SE-10(4)，1984，352–357页；352–354页定义状态轨迹投影、切片准则及数据/控制相关计算。本文固定唯一返回准则与必停结构化片段，证明的是该观察的保持，不声称求得语义最小切片。

[2] Jeanne Ferrante、Karl J. Ottenstein、Joe D. Warren，The Program Dependence Graph and Its Use in Optimization，ACM TOPLAS 9(3)，1987，§3的统一依赖表示；本页使用其数据与控制来源思想进行反向闭包。

形式陈述 ​

准则先于删除 ​

何以保持返回值 ​

问返回值，不问所有工作 ​

从9逆向走到稳定 ​

静态与动态的量词不同 ​

三个不能越过的边界 ​

闭包成本与反例接口 ​

反向链接