上下文敏感的过程间分析

过程内分析把信息沿后继边传走就够了。跨函数后，一条出口边还承诺“我属于哪次尚未完成的调用”。如果把这层配对丢掉，就像把两次电话的回答接给错误的来电者。

调用图公理库调用图构造Call graph construction · Static call graph不知道运行时接收者或函数指针时，怎样可靠地列出可能的被调函数。决定有哪些可能的被调函数；上下文敏感分析决定这些调用的事实如何传入、怎样回到对应调用者。目标集合精确不代表返回已经匹配，反之亦然。

同一个恒等函数也会被分析“串线” ​

考虑纯函数 identity(z){ return z; }，以及

a = identity(0)       // c1，返回到r1
b = identity(1)       // c2，返回到r2
assert(a == 0 && b == 1)

真实执行分别把0交给a、1交给b。若只为identity入口保存一个抽象状态，参数z可能被合并为“0或1”；出口的统一结果再流到两个返回点，分析可能无法证明断言。

更明显的假路径是：从 $c_1$ 进入identity，却沿 ${\mathrm{return}}_{c_2}$ 到 $r_2$。图上可达，调用栈却含 $c_1$，所以该返回不合法。最精确的过程内常量传播也无法修复一条从模型层就接错的返回边。

调用串如何区分，又如何合并 ​

长度1的调用串把identity的两次入口分别记为 $\kappa =[c_1]$ 与 $[c_2]$，于是得到z=0和z=1两份状态。分析递归调用链 $c_1,d,d,d,\dots$ 时，只保留最近一个调用点会使多层上下文都映到 $[d]$，因此状态仍有限。

截断不是把栈简单弹一次就能求逆。例如长度1上下文 $[d]$ 可能来自 $[c_1]$ 压d，也可能来自 $[c_2]$ 压d。返回时必须把结果传给所有与该抽象进入关系相容的调用者，或显式记录调用关联；直接删掉d并假装得到了唯一旧上下文，会漏掉行为。

长度k的调用串有至多 $1+c+\cdots +c^k$ 种，其中c是调用点数。固定k保证有限，不保证增加k总能消除特定伪路径；更深的相同调用后缀仍会合并。

摘要可以不逐个复制所有调用上下文 ​

对identity，入口到出口摘要就是函数 $\mathrm{Summary}(s)=s$，精确保存输入值与输出值的关系。调用处分别应用它：0映到0，1映到1。若只把摘要存成“出口可能是0或1”的集合，就已经丢掉这种输入输出关联。

对于有全局状态的过程，摘要要描述可能影响的全局量；对堆写入，还要接入别名信息。递归使摘要互相依赖，需要求解不动点。单调数据流分析公理库单调数据流分析Monotone dataflow analysis · Monotone framework · Data-flow equations在控制流图上以单调 transfer 和合流方程求解前向或后向程序事实。提供迭代骨架，具体摘要的表示决定是否有限、能否高效合成。

应区分三个精度维度。流敏感性按程序点保留顺序；上下文敏感性区分调用环境；路径敏感性保留足以区别分支条件的信息。一个分析可以上下文敏感但流不敏感，也可以在每个函数内很精确却把所有调用者合并。

即便只合流调用返回合法路径，仍可能包含不可行分支。例如先判断x>0，随后在没有改变x时又走x≤0分支，这是一条调用返回配对正确、但数值条件矛盾的图路径。因此“对所有合法过程间路径精确”不能写成“对真实程序执行精确”。

对一般有限抽象域，复制每个 $[v,\kappa ]$ 状态可直接得到有限方程系统；成本至少乘以上下文数量，格高度和单次转移成本仍需另计。某些分配性问题可用摘要关系而不枚举所有调用串，IFDS公理库IFDS 图可达分析框架IFDS · Interprocedural finite distributive subset problems哪些集合数据流问题能化成有限事实图上的匹配调用返回可达性。与IDE公理库IDE 值环境分析框架IDE · Interprocedural distributive environment problems每个事实还携带常量等格值时，怎样在路径上组合边函数并在路径间合流。便沿这条路计算匹配调用返回的路径结果。

单元任务入口：识别三种不同的伪告警 ​

给一个有两次identity调用、一个共享指针和一处分支的程序，先画出调用点配对，再标出三种不确定性：错误返回边、指针may-alias、多条分支合流。只有第一种能仅靠调用返回匹配解决；第二种需要指针抽象，第三种需要更强的路径条件。

对本页程序，验收解答必须给出 $c_1{\mathrm{return}}_{c_2}$ 非法的栈证据，并列出identity摘要如何分别作用于0和1。若只是画两份函数副本，却没有说明递归时如何截断或复用，分析模型仍不完整。