IDE 值环境分析框架

IFDS的边 $x\to y$ 只说x上的事实会影响y；IDE还能说“原值不变地传过去”“无条件变成3”或“两个来源合流后不再是常量”。这样不用把“x等于3”“x等于4”分别扩成不同事实，只保留事实x，再把值放在格里。

一条摘要记录输入输出之间的函数关系。调用同一过程时，传入3可得3、传入4可得4；不会因为过程曾被两种输入调用，就立即把每个调用的返回都混成未知。

复制常量传播 ​

取平坦常量格

$\mathrm{\perp }$表示尚无值贡献，整数k表示恰为k，$\mathrm{\top }$表示可能不是唯一常量。不同整数的合流为 $\mathrm{\top }$，$\mathrm{\perp }\bigsqcup k=k$。程序点是否可达另行跟踪；不可达点不能因一条常量赋值就凭空变为可达。

语句 y=x 给边 $x\to y$ 标恒等函数，并删除旧y到新y的保持边；其他变量保持。语句 y=3 则从零事实向y提供常量3。对

x = 3
y = x
z = identity(y)

x通过恒等边传到y，identity的匹配摘要再把y传到z，最终z=3。把第一句换成分支 x=3 或 x=4，合流后得到 $3\bigsqcup 4=\mathrm{\top }$，之后复制仍保持 $\mathrm{\top }$；IDE没有声称忽略了分支就仍能恢复一个确定整数。

摘要合流必须仍能表示 ​

考虑一个过程：一条分支令输出等于输入，另一条令输出为3。它的摘要不是简单的“恒等或常量3”二选一，而是函数

输入3时输出仍为3；输入4时为 $\mathrm{\top }$。若摘要表示只能存恒等函数或常量函数，它便不闭合，必须扩充表示或采用可靠近似。

对只含复制与整数字面量的简单语言，可使用恒等、各常量函数、$h_k(v)=v\bigsqcup k$，以及恒底/恒顶等有限形式，并按复合和合流化简。比如 $h_3\circ h_4$ 恒为 $\mathrm{\top }$，$h_3\circ {\mathrm{const}}_3$ 恒为3。字面量集合固定后，这个函数族的表示和操作可以保持紧凑。加入更复杂算术时，要重新证明所选函数族的闭包和复杂度。

普通常量传播未必分配 ​

两条路径分别到达环境 $(x,y)=(1,2)$ 和 $(2,1)$，随后计算 z=x+y。逐路径计算都得z=3，所以路径结果的合流仍为3；但先把两环境逐变量合流，会得到x=y=$\mathrm{\top }$，再计算则z=$\mathrm{\top }$。

因此普通双变量算术转移不满足所需分配律。复制常量传播干脆把这类复合表达式结果保守地置为未知，从而落入可处理的分配子类。原始IDE研究也处理某些单变量线性常量传播，但这不等于任意关系型数值分析都能直接使用同一框架。

第一阶段把IFDS的路径边从“存在/不存在”改成摘要函数：普通边在已有摘要后复合；同一端点对的不同摘要逐点合流；调用与返回通过匹配的被调摘要连接。第二阶段再把程序入口的初值沿这些摘要求出各程序点的具体抽象值。将关系计算与初值求值分开，可以让摘要被不同调用输入复用。

正确性依赖两个分配：程序转移对环境合流分配，边函数的表示能忠实完成路径复合与路径合流。由合法路径分解可证明摘要覆盖所有且仅有模型允许的调用返回路径，再把函数应用到初值，得到该模型的MVP值。

设原过程间图有 $E$ 条边、$N$ 个程序点，$d=|D|$。在边函数表示及操作为常数成本、相关高度为常数等标准条件下，把额外零事实计入后，经典 IDE 的传播时间与 IFDS 同阶，为 $O(E(d+1{)}^3)$；输入读取与程序点初始化的 $O(N+E)$ 成本另计。这样也覆盖 $D=\varnothing$ 的情形；当 $d\ge 1$ 时，传播界可简写为惯用的 $O(E{d}^3)$。若值域高度、函数大小或求解成本随输入增长，都需明确计入；只看到公式有 $E$ 和 $d$ 就把昂贵 SMT 函数标签当常数是不成立的。

IDE适合把布尔依赖升级为有值信息，例如复制常量、某些线性传播或受限数值属性。它与指针包含分析公理库Andersen 包含式指针分析Andersen pointer analysis · Inclusion-based points-to analysis地址获取、复制、解引用读写如何生成只增的points-to包含约束。也不能直接互换：解引用常把“指针可能到哪里”与“那里存了什么”组合起来，未必具有IDE要求的分配结构。

练习与解答 ​

给过程摘要 $h_3(v)=v\bigsqcup 3$，分别求输入 $\mathrm{\perp },3,4,\mathrm{\top }$ 的输出，并说明它为何不是恒等函数也不是常量函数。答案依次为 $3,3,\mathrm{\top },\mathrm{\top }$。输入4说明它不恒等，输入3与4的不同结果说明它不恒定。

再比较先合流再执行双变量加法与先逐路径执行。上述 $(1,2)$、$(2,1)$ 已构成反例；验收应写出两条计算链的不同结果，而不是仅说“关系丢失了”。