静态分析：IFDS

2024-05-16

Feasible and Realizable Paths

  • 不可行路径（infeasible path）： CFG 中在程序实际运行时不会执行到的路径
  • 我们希望程序分析结果不会被不可行路径污染，或尽可能少被污染
  • 但是，给定一条路径，确定它是否可行，一般来说是不可判定的
  • 可实现路径（realizable path）： “返回”与相应的”调用”相匹配的执行路径
  • 可实现的路径可能不是可执行的，但不可实现的路径一定不是可执行的。
  • 因为 realizable path 可能是某个 unrealizable path 的后继路径
  • 我们的目标是识别可实现的路径，从而避免沿着不可实现的路径的污染分析污染结果。
  • 使用括号匹配来标识可实现路径（调用点”(“，返回点”)”），但是简单的括号匹配没有办法适应复杂的调用返回情况，所以我们需要 CFL-Reachability

CFL-Reachability（context free language）

定义：只有当路径的边上的标签的连接是指定上下文无关语言中的一个词时，才认为该路径连接了两个节点 A 和 B，或认为从 A 可以到达 B。

部分括号匹配问题可以通过 CFL 来解决，规则是

  • 出现”)”括号则必须要有”(“匹配它，反之则不一定

  • call-site i 的边的标签用（i )i 来表示

  • 其他的边标签用 e 来表示，表示普通边

  • 程序中的一条路径是 realizable path，则这条路径的括号表达一定满足下面的文法

  • image-20240120145503715

Overview of IFDS（通过图可达性来进行程序分析）

  • 定义：I（inter-procedural）F（finite）D（distributive）S（subset problem）
  • 能用 IFDS 进行分析前提：流函数是可分配的 且 域有限
  • IFDS 分析的结果中的路径都是 meet-over-all-realizable-paths（即给出 MRP solution）

MRP（meet-over-all-realizable-paths）

image-20240120150043211

pfp 是某条路径上所有流函数的复合

image-20240120145923982

对于每个节点 n，MRPn 都会提供一个 “meet-over-all-realizable-paths “解决方案，其中 RPaths(start, n) 表示从起始节点到 n 的可实现路径集（路径的单词使用语言 L(realizable)）。

image-20240120150026777

三步走完 IFDS

  • 第一步为程序 P 建立 G*（super-graph），基于要解决的问题定义流函数
  • 第二步应用流函数建立 G#（exploded super-graph）
  • 第三步在 G#上应用 Tabulation 算法解决问题

Super-graph and Flow Functions

super-graph 定义

  • 每个方法建立一个流图
  • 每个方法的流图有唯一的入口节点和出口节点
  • 方法调用拆解为 Callp 和 Retp 节点
  • 有三种边
    • call-to-return-site edge 从 Callp 节点到 Retp 节点
    • call-to-start edge 从 Callp 节点 到被调用方法的头结点
    • exit-to-return-site edge 从 被调用者的尾节点到 Retp 节点
    • image-20240120150733040

flow function 定义

image-20240120150847384

栗子 slide 70 页

image-20240120151047868

Exploded Super-graph and Tabulation Algorithm

Exploded Super-graph（构建）

过程：将 flow function 翻译成一种 representation relation

设 flow function 有 D 个节点，那么 representation relation 是一个图有 2*(D+1)个节点，最多(D+1)^2 条边.

映射过程：image-20240120151349305

image-20240120151628286

回答为什么一定要有(0，0)这条边

  • 在传统的数据流分析中，要查看 data fact a 在程序点 p 是否成立，我们需要在分析结束后检查 a 是否在 OUT[n4] 中。
  • data fact 是通过流函数的组合传播的。在这种情况下，”可达性 “直接从 OUT[n4] 中的最终结果中获取。
  • 对于同样的情况，在 IFDS 中，data fact a 在 p 处是否成立取决于是否存在从 <smain, 0> 到 <n4,a> 的路径，而 “可达性 “是通过连接 “粘贴 “表示关系上的边（找出路径）来检索的。
  • λ S.{a} 表示 a 在 p 处成立，与输入 S 无关；然而，如果没有边 0⟶0，每条边的表示关系就无法连接或 “粘贴 “在一起，就像传统数据流分析中的流函数无法组合在一起一样。因此，IFDS 无法通过这种断开的表示关系生成正确的解决方案。
  • 栗子在 slide 97 页

构建流程：

image-20240120151856055

问一个图中的节点是否可达：找一条从开始节点到目标节点的路径，如果存在 且 函数调用的括号匹配成功，则可达。

Tabulation algorithm（标识出 exploded super-graph 中所有可达节点）

目标：Let n be a program point, data fact d ∈ MRPn, if there is a realizable path in G# from <smain, 0> to <n, d>. (then d’s white circle turns to blue)

算法复杂度：O(E*D^3) edge * domain^3

算法解释我也没听懂，在 slide 144 页

Understanding the Distributivity of IFDS

可分配性：F(x ∧ y) = F(x) ∧ F(y)

判断依据：给定一个语句 S，除了 S 本身，如果我们需要考虑多个输入数据事实来创建正确的输

出，那么这个分析就不是可分配的，不能用 IFDS 来表示。

实例 1-constant propagation（常量传播）

在常量传播中：对于 z = x +y 我们想确定 z 是不是常量需要同时知道 x,y。但是 IFDS 每一次只能处理一个，所以 IFDS 没办法处理常量传播问题

实例 2-Pointer Analysis（指针分析）

要想知道 x,y 是不是指向同一个对象，那么输入得有 x,y，多个输入了，所以指针分析不是可分配的