返回学习路线

同一张控制流图：从数据流事实到安全删除 ​

这份任务将八个条目接成三个可核对的终点：在同一菱形图上求事实并实际变换；把一段三轮循环的乘法移到入口；在SSA图里同时传播常量与控制边。它不要求安装编译器框架，Python标准库就能重放，但每一步都要解释为什么允许改动。

入口与交付 ​

先能回答三个问题：may分析为什么在分支用并集？must分析为什么用交集？φ为什么只读取实际进入边的参数？若还不确定，可依次读单调数据流理路单调数据流分析Monotone dataflow analysis · Monotone framework · Data-flow equations在控制流图上以单调 transfer 和合流方程求解前向或后向程序事实。、控制流图理路控制流图Control-flow graph · Program control-flow graph以基本块或程序点为节点、以可能的执行转移为边表示过程内控制流的有向图。与φ节点理路SSA 的 φ 节点Phi node · Phi function · φ 节点在 SSA 控制流汇合块中按实际进入的前驱边选择对应版本，并以并行方式定义合流值的伪指令。。

固定语言是单线程、过程内局部标量IR，所有使用有定义，数学整数运算不溢出，加法、乘法、比较、复制都纯粹且总定义。观察包含返回值与分支路径；没有内存、调用、异常、poison、输入输出及资源失败。边界反例会明确换模型，不能混入主证明后还沿用原结论。

交付四项：三个数据流边界表；CSE、复制传播、DCE的逐阶段IR；LICM的循环状态及零次反例；SCCP的边集合、值表与两种迁移。证明说明负责全输入保证，有限运行负责检查具体实现。

• 下载可直接运行的检查器
• 下载本轮实际生成的完整结果

运行 Python 3.10 或更高版本：

python foundations-dataflow-optimization-checker.py --out result.json
python -O foundations-dataflow-optimization-checker.py --out result-optimized-mode.json

验收不使用会被 -O 移除的 assert。脚本不联网、不调用LLVM、不测机器码性能，也不把fuel耗尽当作发散证明。菱形解释器明确只支持无环输入，意外出现循环会报错；循环示例有独立的自然数计数执行器。

任务一：同一菱形图，三种问题 ​

输入a、b是整数，p是布尔值。静态赋值按块内位置编号：

E: E.1 x := a+b
   E.2 y := x
   if p goto T else F
T: T.1 u := a+b
   goto J
F: F.1 u := a+b
   goto J
J: J.1 z := a+b
   J.2 dead := z+1
   J.3 r := u+y
   return r

到达定义理路到达定义分析Reaching definitions analysis · 到达定值分析沿控制流保留每个变量可能最近执行的赋值，以入口定义、逐语句杀生与最小不动点建立定义到使用的可靠连接。问值可能来自哪次写入。J入口的完整集合为 {input:a,input:b,input:p,E.1,E.2,T.1,F.1}。其中u的来源有两项，但每次实际运行只选择其中一项。新增一个不可达的U块，里面定义u并跳J，不得污染这个集合。

活跃性理路活跃变量分析Live-variable analysis · Liveness analysis从未来使用逆向传播仍需保存的变量，计算逐指令和块边界活跃集，并把phi的使用限定在相应进入边。问以后可能还读什么。完整边界如下：

可用表达式理路可用表达式分析Available-expression analysis · Available expressions用全路径交集计算已经算过且操作数未改变的表达式，以正确入口、先杀后生和自依赖检查支持安全复用。问每条路是否已算过、操作数是否保持。进入E为空，进入T、F、J均为 {add(a,b)}；J出口另外包含add(z,1)与add(u,y)。把语句换成a:=a+b时，add(a,b)不能生成，因为出口a已经不同。

三张表的含义不可混用。两个到达定义不自动意味着两个数值不同；表达式可用不自动保证结果载体尚在；值不活跃不自动允许删除有副作用的计算。

任务二：逐阶段真正发出代码 ​

第一阶段CSE理路公共子表达式消除Common subexpression elimination · CSE在全路径表达式可用之外验证结果载体仍有效，以支配复用或新临时量接线删除重复计算，同时保留操作语义。用E.1作锚点，将T、F的u赋值和J的z赋值改为读取x。验收证据是：E支配三处，a、b不改写，x也不改写。不要只展示字符串相同。

第二阶段复制传播理路复制传播Copy propagation · Available-copy analysis以可用复制对证明替换点两个变量仍同值，在任一端重定义时失效，并把跨分支的可靠替换与后续死代码删除分开。在J入口同时保留(y,x)、(u,x)，执行z:=x后加入(z,x)，所以改成dead:=x+1、r:=x+x。复制指令此时仍存在。

第三阶段DCE理路死代码消除Dead-code elimination · DCE · Dead assignment elimination删除结果不再需要且计算纯粹总定义的赋值，重新计算需求直至稳定，保留控制流、陷阱、副作用和终止行为。删除dead、z、两份静态u赋值与y，得到：

E: x := a+b
   if p goto T else F
T: goto J
F: goto J
J: r := x+x
   return r

对a=2、b=3、p=false，四个阶段都经过E、F、J并返回10。每次执行的加法次数依次为5、3、3、2；复制次数依次为1、3、3、0。注意源静态赋值有7条，单次路径只执行6条；最终静态与动态赋值都为2条。

检查器枚举a,b∈{-4,…,4}、p∈{false,true}，共162个输入，实际运行四份IR并比较结果与路径。这个枚举没有覆盖全部数学整数；对任意a、b都返回2(a+b)的推导，加上每个变换的逐步保持论证，才支持一般结论。

另把a:=3放E，b:=a+1放后继T，T返回0。要求DCE删除轮数中每轮的删除条数为1、1、0：第一轮删除b，重算活跃性后第二轮删除a，最后一轮确认稳定。

任务三：外提必须经受零次循环 ​

使用循环不变代码外提理路循环不变代码外提Loop-invariant code motion · LICM在单入口自然循环中识别不变操作数，用新鲜临时量把纯总计算放到preheader，并用零次循环检验新增执行的安全性。的程序，i与s从0开始，循环执行t:=ab、s:=s+t、i:=i+1，条件i<n。用新鲜h在preheader算ab，循环内保持t:=h的位置。

取a=2、b=3、n=3，两版循环后的状态都为(1,6)、(2,12)、(3,18)，返回18；乘法3次对1次。n=0时都返回0，但乘法0次对1次，说明代码移动不保证每个输入都减少工作。脚本检查a,b∈{-3,…,3}、n∈{0,…,5}，共294组。

迁移：每轮末尾再写a:=a+1，n=3时源结果27，错误外提结果18。另一模型把运算换成有除零trap的1/d，n=0,d=0时源返回0，错误外提trap。前者违反值不变，后者违反提前求值安全；它们是两项不同的许可。

任务四：让常量与边一起稳定 ​

SCCP理路稀疏条件常量传播Sparse conditional constant propagation · SCCP共同增长可能执行的控制边与SSA值的三层抽象，只在已激活前驱上合流phi，用双工作队列排除假分支并传播常量。的独立SSA输入如下：E定义a=4、b=6、c=(a==4)，真边去T计算t=a+b，假边去F取f=q；J定义v=phi(T:t,F:f)、w=v*2、d=(w==20)，真边R返回w，假边B返回99。

最终已激活边恰为START→E、E→T、T→J、J→R；a=4、b=6、c=true、t=10、v=10、w=20、d=true。输入q为⊤，F中未执行的f仍为⊥。φ只合流已激活入边，不能让F的未知输入污染v。

将E的条件改成未知布尔输入p，再将F改成常量14：两条进入J的边都激活，v、w、d均为⊤，J的两条出口都保留。若F改成10，v仍为10，w=20，d=true，B再次被排除。结果JSON含三种情况的事件轨迹。

本检查器实现分析，没有自动输出清理后的SSA。主例可手工化简为return20，但“分析可证明”与“代码已重写并通过结构验证”是不同交付。SCCP可处理循环的数据流条件，不等于能够判定任意源程序是否终止。

最后四个拒绝理由 ​

1. 把y:=x后的所有y永久改成x：如果x后来改变，就读错旧值
2. 因x死了而删除x:=1/0：在trap语义下改变观察
3. 两分支各算一次表达式，就在汇合读取仅一支定义的u：另一支没有这个载体
4. 队列尚未清空就删除未激活边：后续信息仍可能激活它

验收应能给每项写出具体输入和错误输出，而不只是说“注意边界”。报告里的运行值、变换树和数据流集合均由所附脚本产生；对真实机器整数、别名内存、异常、并发或LLVM语义的保证仍需新模型与新证明。