4.5 过程内指针分析

这一节展示了一个基于约束的规则指针分析说明。下一节将分析扩展到过程间的分析,并且4.7节描述约束解决。

指针类型和约束系统

一个约束系统被定义为为一系列关于指针类型的约束。约束系统的解是一个从指针类型变量到抽象位置集合的替换,使得所有约束都得到满足。

一个指针类型可以是抽象地址集合、一个解引用类型、一个索引类型、一个函数类型和一个类型变量。

对于每一个不是函数类型的对象 o 我们分配一个类型变量;这包含了抽象返回地址对于一个函数。对每一个对象函数类型 f 我们关联是类型参数对应到 f 的参数。对于每一个类型说明者我们都分配一个类型变量。

  • 基础位置
    • 语义:基础位置(如变量名、函数名、标签等)的含义直接为其自身(如 x 的语义是 xfoo 的语义是 foo)。
    • 作用:作为指针类型的原子单元,其他复杂类型基于基础位置构建。
  • 解引用类型
    • 语义:解引用类型的含义是指针 T 所指向的所有对象 o 对应的类型变量 To 的值的并集。
    • 示例:若 T 表示指针 p,其语义为 {x,y}(即 p 可能指向 xy),且 Tx={a}、Ty={b},则 *p 的语义为 {a}∪{b}={a,b}。
    • 作用:将指针的指向集合转换为所指对象的值集合,用于处理解引用操作(如 *p = 1 时确定受影响的对象)。
  • 结构体字段类型
    • 语义:对于结构体类型的指针 T,其字段 i 的含义是 T 所指向的所有结构体对象 o 中,类型为 struct U 的对象对应的字段 U.i 的类型变量值的并集。
    • 示例:若 T 表示结构体指针 ps(指向 s,类型为 struct S),S 的字段 ix,且 Ts={s}、S.x 的类型变量为 T_{S.x} = \{v\},则 ps.x 的语义为 {v}。
    • 作用:处理结构体字段的指针访问,将结构体类型与字段关联起来。
  • 函数类型
    • 语义:函数类型的含义是参数类型 Ti 到返回值类型 T 的映射,即输入参数的语义集合映射到输出返回值的语义集合。
    • 作用:用于分析函数指针的调用行为,确保参数和返回值的类型匹配。
  • 类型变量
    • 语义:类型变量的含义是变量赋值 S 对其绑定的值(如 S(T)={x,y} 表示类型变量 T 被赋值为集合 {x,y})。
    • 作用:通过变量赋值将抽象的类型变量与具体的抽象位置集合关联,实现约束系统的求解。

包含关系的定义

  • 基础情况(抽象位置集合):对于两个抽象位置集合 O1 和 O2,若 O1 是 O2 的超集(O1⊇O2),则称 O1⊇∗O2。

    • 示例:若 O1={x,y},O2={x},则 O1⊇∗O2 成立。
  • 函数类型情况:对于函数类型 (Ti)→T 和 (Ti′)→T′,包含关系要求:

    • 参数类型 Ti 包含 Ti′(协变,Ti⊇∗Ti′);
    • 返回值类型 T′ 包含 T(逆变,T′⊇∗T)。
    • 原因:函数类型的包含关系遵循逆变协变规则,即参数类型更宽松(超集)、返回值类型更严格(子集)时,函数类型可兼容。

约束满足条件

  • 变量赋值S:将类型变量(如 Tp)映射到具体的指针类型(如 {x,y})。
  • 约束 T1⊇T2 的解:当且仅当在变量赋值 S 下,T1 的语义([[T1]]S)通过 ⊇∗ 关系包含 T2 的语义([[T2]]S)。
    • 示例:约束 Tp⊇{x} 的解为 S(Tp)={x,y},因为 {x,y}⊇∗{x} 成立。

定义 4.6 讲的是如何判断一个变量赋值是否能满足指针分析中的约束条件。简单来说,就是看指针可能指向的对象集合之间是否满足 “包含” 关系。(AI生成的)

核心思想:用 “包含关系” 判断解是否合法

  • 对于普通指针指向
    比如,指针 p 可能指向的对象集合是 {A, B},约束要求 p 必须至少指向 A。如果变量赋值后 p 的指向集合包含 A(比如 {A, B}),就满足约束,就像 “大集合包含小集合” 一样。
  • 对于函数指针类型
    假设函数指针的参数类型要求是 “整数指针”,而实际赋值的函数参数类型是 “指针”(更宽泛),这时候参数类型满足 “包含” 关系(整数指针属于指针的一种)。同时,返回值类型要求是 “整数”,实际函数返回值是 “数字”(更严格),这也满足 “包含” 关系。只有参数和返回值都满足这种 “宽包含窄” 或 “严包含松” 的关系时,函数指针的约束才算满足。

通俗例子理解

  • 普通变量约束
    约束条件:“指针 p 必须指向 x”(即 p 的指向集合至少包含 x)。
    如果变量赋值后,p 的指向集合是 {x, y},那么 {x, y} 包含 {x},满足约束;
    如果 p 的指向集合是 {y},不包含 x,就不满足约束。
  • 函数指针约束
    约束条件:“函数指针 fp 必须能接受整数指针参数,并返回整数”。
    • 若 fp 指向函数 foo,其参数是 “指针”(比 “整数指针” 更宽泛),返回值是 “数字”(比 “整数” 更严格)。
    • 参数类型 “指针” 包含 “整数指针”(整数指针是指针的一种),返回值类型 “整数” 包含于 “数字”(整数是数字的一种),因此满足约束。

约束产生

我们给一个基于约束规范的指针说明在之前的章节。

程序的约束是由类型定义约束+声明约束+函数定义约束+目标参数约束

goal parameters(目标参数) 指的是程序入口函数(通常是main函数)的参数。由于这些参数在程序启动时由外部环境传入,其初始值和指向在静态分析中无法确定,因此需要进行保守处理。由于目标参数的初始值未知,其指针抽象必须包含 “Unknown”,以覆盖所有可能的运行时指向。

声明约束

1
2
3
4
5
6
7
8
9
10
11
12
13
若声明为基础类型(如int, float):
生成约束:T_var ⊇ {Unknown}

若声明为指针类型(如int* p):
if 有初始化表达式(如p = &x):
生成地址标签l,约束:T_p ⊇ {l} 且 T_l ⊇ {x}
else:
生成约束:T_p ⊇ {Unknown}

若声明为extern变量(如extern int* ep):
生成约束:T_ep ⊇ {Unknown}

生成结构体类型名S的抽象位置,并为每个字段i生成S.i的抽象位置(无初始约束,仅定义抽象位置)
  • 数组变量视为聚合类型,其指针抽象为a[],表示指向数组内容。

  • 结构体 / 联合体类型本身不直接作为指针目标,其字段的指针抽象通过后续表达式处理。

类型说明约束

类型定义的约束生成(Constraint generation for type definitions) 指的是为程序中定义的类型(如结构体、联合体、枚举)生成相应约束的过程。

结构体类型定义(struct S {…})

  • 约束目标:为结构体类型及其字段建立抽象位置,以便在指针分析中处理结构体指针的解引用和字段访问。
  • 约束规则:
    • 为结构体类型名 S 生成抽象位置 S,表示结构体对象本身的类型。
    • 为每个结构体字段 i 生成抽象位置 S.i,表示该字段的指针目标。
    • 示例:对于 struct S { int x; char* p; },生成抽象位置 S(结构体本身)、S.x(整型字段)、S.p(指针字段)。
  • 约束表达式:无显式包含约束(仅定义抽象位置),字段的指针约束通过后续表达式(如赋值、解引用)生成。

2. 联合体类型定义(union U {…})

  • 约束目标:联合体成员共享内存,需处理指针指向联合体成员时的歧义。
  • 约束规则:
    • 为联合体类型名 U 生成抽象位置 U
    • 为每个联合体成员 i 生成抽象位置 U.i
    • 特殊处理:联合体成员的指针抽象可能重叠,需通过后续表达式约束处理成员访问的不确定性(文档中为简化分析,暂不考虑联合体成员共享的复杂情况,仅生成基础抽象位置)。

3. 枚举类型定义(enum E {…})

  • 约束规则:枚举类型本质为整数,不涉及指针操作,因此不生成任何约束
1
2
3
4
5
6
7
8
9
10
11
12
13
14
若类型定义为结构体 struct S { 字段列表 };:
添加抽象位置 S 到 ALoc;
对每个字段 i in 字段列表:
添加抽象位置 S.i 到 ALoc;
生成空约束(仅定义抽象位置,无包含关系约束);

若类型定义为联合体 union U { 成员列表 };:
添加抽象位置 U 到 ALoc;
对每个成员 i in 成员列表:
添加抽象位置 U.i 到 ALoc;
生成空约束(仅定义抽象位置,无包含关系约束);

若类型定义为枚举 enum E { 枚举值 };:
不生成任何约束和抽象位置(因枚举为整数类型,与指针分析无关);

表达式约束生成

表达式的约束生成(Constraint generation for expressions) 是指针分析的核心步骤之一,用于将程序中的表达式(如赋值、解引用、函数调用等)转换为对应的约束条件,以捕获指针与对象之间的依赖关系。

表达式按操作类型可分为基础表达式(如变量引用、常量)、指针操作表达式(如解引用、地址获取)、类型转换表达式函数调用表达式等,每种表达式对应不同的约束生成规则。

变量引用与常量表达式

  • 变量引用(如x,p):

    • 约束规则:变量的抽象位置即为其自身,生成约束 T_e ⊇ {v}v 为变量名)。
    • 变量 p 的约束为 T_p ⊇ {p}
  • 常量表达式(如 12"string"):
  • 常量无法作为指针目标(除字符串常量),抽象为 Unknown
    • 整数常量 12 生成约束 T_e ⊇ {Unknown};字符串常量 "str" 生成约束 T_e ⊇ {"str"}"str" 为抽象位置)。

指针解引用表达式(*e)

规则:若表达式 e 是指针(抽象位置为 T_e),则解引用 *e 的抽象结果为 T_e 所指向的对象集合。

  • 约束表达式T_{*e} ⊇ *T_e(即 *e 的类型变量包含 e 所指对象的类型变量值)。
  • 示例:若 p 的约束为 T_p ⊇ {x},则 *p 的约束为 T_{*p} ⊇ T_x(假设 x 是基础类型,T_x ⊇ {Unknown},但作为被指向对象,x 本身是抽象位置)。

地址获取表达式(&e)

规则:对变量 e 取地址生成唯一标签 l,标签 l 的抽象位置包含 e

  • 约束表达式:T_{&e} ⊇ {l}T_l ⊇ {e}
  • 示例&x 生成标签 l1,约束为 T_{l1} ⊇ {x},表示标签 l1 指向 x

类型转换表达式((T)e)

  • 安全转换(如结构体指针转成员指针)
    • 若将结构体指针转换为其首成员指针,生成约束 T_{cast} ⊇ T_e.11 表示首成员)。
    • 示例(int*)&ssstruct S 变量)生成约束 T_{cast} ⊇ S.1(假设 S 的首成员为 int x,则 S.1 = S.x)。
  • 不安全转换(如整数转指针)
    • 抽象为 Unknown,生成约束 T_{cast} ⊇ {Unknown}

函数调用表达式(f(e1,e2))

  • 直接调用(已知函数名)

    • 实参的抽象必须包含于形参的抽象,生成约束 *T_{f} ⊇ (*T_{e1}, *T_{e2}) → T_{f0}f0 为函数返回位置)。
    • 示例foo(p) 生成约束 *T_foo ⊇ (*T_p) → T_{foo0},表示 foo 的参数抽象包含 p 的指向集合,返回值存入 foo0
  • 间接调用(函数指针,如 fp(e)

    • 函数指针 fp 的抽象包含所有可能的函数,生成约束 *T_{fp} ⊇ (*T_e) → T_ll 为调用返回标签)。
    • 示例fp(&x) 生成约束 *T_{fp} ⊇ (*{x}) → T_l,结合 fp 的抽象(如 {foo, bar}),推导 foobar 的参数约束。

赋值表达式(e1=e2)

  • 规则:左值 e1 的抽象必须包含右值 e2 的抽象结果。
    • 约束表达式*T_{e1} ⊇ *T_{e2}
    • 示例p = q 生成约束 T_p ⊇ T_q,即 p 的指向集合包含 q 的指向集合。
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
生成约束:T_v ⊇ {v}

若 e 的类型为指针:
生成约束:T_{*e} ⊇ *T_e

生成唯一标签 l:
生成约束:T_{&e} ⊇ {l} 且 T_l ⊇ {e}

if T 是结构体首成员指针且 e 是结构体指针:
生成约束:T_cast ⊇ T_e.1
else:
生成约束:T_cast ⊇ {Unknown}

生成返回标签 l:
对每个实参 ei:
生成约束:*T_f ⊇ (*T_ei) → T_l
生成约束:T_{调用结果} ⊇ {l}

生成约束:*T_e1 ⊇ *T_e2

语句的约束生成

语句的约束生成(Constraint generation for statements) 是将程序语句(如赋值、循环、函数调用、返回等)转换为指针分析约束的过程。文档中主要关注赋值语句函数调用语句返回语句控制流语句(如循环、分支),每种语句对应不同的约束生成逻辑。

赋值语句(e1=e2)

  • 约束目标:确保左值 e1 的指针抽象包含右值 e2 的指针抽象结果。
  • 约束规则
    • 对于指针类型的赋值(如 p = q),生成约束:*T_{e1} ⊇ *T_{e2}(即左值指向的集合包含右值指向的集合)。
    • 对于解引用赋值(如 *p = &y),生成约束:*T_p ⊇ {&y}(即 p 指向的对象必须包含 &y 的抽象位置)。
  • 示例:
    • 语句 p = &x 生成约束:T_p ⊇ {l}T_l ⊇ {x}l&x 的标签)。
    • 语句 *q = p 生成约束:*T_q ⊇ T_pq 解引用后的指向包含 p 的指向)。

函数调用语句(f(e1,…en))

  • 直接函数调用(如 foo(p)):
    • 实参的抽象必须匹配形参的抽象,生成约束:*T_f ⊇ (*T_{e1}, ..., *T_{en}) → T_{f_0}f_0 是函数 f 的返回位置)。
    • 含义:函数 f 的参数抽象包含所有实参的指向集合,返回值存入 f_0
  • 间接函数调用(如 fp(e)fp 是函数指针):
    • 函数指针 fp 的抽象包含所有可能的目标函数,生成约束:*T_{fp} ⊇ (*T_e) → T_ll 是调用的返回标签)。
  • 示例
    • 语句 foo(p) 生成约束:*T_foo ⊇ (*T_p) → T_{foo_0}
    • 语句 fp(&x) 生成约束:*T_{fp} ⊇ (*{x}) → T_l(假设 &x 的抽象为 {x})。

返回语句(return e)

  • 约束目标:函数的返回值抽象必须包含返回表达式 e 的抽象结果。
  • 约束规则:生成约束:T_{f_0} ⊇ *T_e(函数返回位置 f_0 的抽象包含表达式 e 的指向集合)。
  • 示例:语句 return p 生成约束:T_{f_0} ⊇ T_p(返回值的指向集合包含 p 的指向)。

控制流语句(循环、分支)

  • 流不敏感分析:文档中的分析是流不敏感的,因此循环和分支语句不生成额外约束,而是将不同分支的约束合并。
  • 示例if (cond) p = &x; else p = &y; 生成约束:T_p ⊇ {x, y}(合并两个分支的指向集合)。
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
若语句为 e1 = e2:
生成约束:*T_e1 ⊇ *T_e2
若 e2 是地址表达式(如 &x):
生成标签 l,约束:T_{e2} ⊇ {l} 且 T_l ⊇ {x}

若语句为 f(e1, ..., en):
生成返回标签 l:
对每个实参 ei:
生成约束:*T_f ⊇ (*T_ei) → T_l
生成约束:T_{调用结果} ⊇ {l}

若语句为 return e:
生成约束:T_{f_0} ⊇ *T_e (f_0 是当前函数的返回位置)

// 流不敏感分析中,合并所有分支的约束
对每个分支中的语句生成约束,合并结果(如 T_p 包含所有分支的指向集合)

完备性和可靠性

  1. 可靠性(Soundness)

    • 分析结果必须保守地覆盖程序运行时的所有可能指针指向,即任何实际指向的对象都包含在分析结果中。

    • 通俗理解:分析不会遗漏可能的指针指向,确保安全性(不会因低估指向导致错误优化)。

  2. 完备性(Completeness)

    • 分析结果应尽可能精确地捕获所有可能的指针指向,即分析结果中的每个指向都是实际可能发生的。
    • 通俗理解:分析结果中没有 “虚假” 指向(Spurious Points-to),但在实际中,由于流不敏感等近似,完备性通常难以完全满足。

4.6 过程间指针分析

过程内分析在前几章分析中牺牲了精确性在函数调用:所有的函数调用被合并了。注意一个下面的函数例子:

1
2
3
int *inc_ptr(int *q){
return q+1;
}

这里应该有两个函数调用’inc_ptr(a)’和’inc_ptr(b)’当a和b都是指针时。过程内分析将调用合并,并声称对inc ptr的调用会产生一个指向ab的指针。

有很多调用’inc_ptr’虚假的指向信息被传播到不相关的调用点,降低了分析的精确度。这节弥补这个问题通过将分析扩展到过程间,或者是上下文敏感的指针分析。

分离函数上下文

过程间分析的简单方法是在过程内分析之前对函数进行文本复制。函数调用从不同的上下文被拷贝,调用点依次改变。从北也许会指数级增加程序的大小,从而也会使生成的约束系统规模呈指数级增长。

函数文本复制的问题在于,由于约束数量的增加,分析速度会变慢;更糟糕的是拷贝也许是没有用的:拷贝函数也许会被用到相同的上下文,以致于并没有增加精确度。理想来说,克隆函数应该给予分析的结果,这样只有从复制中获益的函数才会被实际复制。

上下文分离经由静态调用图

该小节主要介绍如何利用静态调用图(Static-Call Graph, SCG)实现过程间指针分析的上下文分离,以提升分析精度,同时避免函数复制带来的指数级复杂度问题。

静态调用图作用

  • 定义:静态调用图是一个映射函数 SCG: CallLabel × Variant → Id × Variant,用于将调用站点封闭函数的变体编号映射到目标函数名及其变体编号
  • 目的:通过为不同调用上下文的函数生成唯一变体(Variant),区分函数在不同调用场景下的行为,避免将所有调用合并分析(如过程内分析的 “粘性” 处理),从而减少伪指针信息的传播。

函数变体与约束系统扩展

  • 函数变体:每个函数根据其调用上下文被划分为多个变体(如 f^0, f^1, ..., f^n),其中 0 通常作为摘要变体(Summary Variant),用于处理间接调用或无法区分的上下文,其他变体对应具体调用场景。
  • 约束系统扩展
    • 为每个函数变体生成独立的约束系统,但通过共享结构避免重复计算。
    • 例如,函数 f 的参数和局部变量在不同变体中表示为向量形式(如 T_p = <T_p^0, T_p^1, T_p^2>),分别对应摘要上下文和具体调用上下文。

示例说明

  • 程序场景:假设有函数 dinc 两次调用 inc_ptr,而 dinc 自身又被 main 调用两次。
  • 静态调用图结构:
    • main 中的两次 dinc 调用生成 dinc^1dinc^2 变体。
    • 每个 dinc 变体调用 inc_ptr 时,生成 inc_ptr^1, inc_ptr^2, inc_ptr^3, inc_ptr^4 四个变体(因 dinc 有两个变体,每个可能生成多个 inc_ptr 变体)。
  • 约束系统优化:
    • 不同变体的约束系统通过向量索引关联(如 T_{inc_ptr}^i 对应第 i 个调用上下文的参数约束),而非独立生成完整约束,减少冗余。

变体向量约束

该小节主要介绍如何通过变体向量(Variant Vectors)扩展约束系统,以支持过程间(Inter-procedural)指针分析的上下文敏感性。核心内容围绕约束条件的向量表示变量与表达式的向量分配,以及如何通过向量运算解决跨上下文的指针传播问题

扩展约束系统的定义

  • 基本概念:将传统的单变量约束扩展为向量形式,每个分量对应函数的一个变体(Variant)。例如,若函数有 n 个变体,则约束表示为 Tn⊇Un,其中 T 和 U 是指针类型向量。

  • 向量元素含义

    • 向量长度由函数变体数量决定(通常为 n+1,包含一个摘要变体 0 和 n 个具体变体)。
    • 摘要变体(如 T0)表示所有上下文的合并信息,具体变体(如 T1,T2)对应特定调用上下文的信息。

变量与表达式的向量分配

  • 对象关联向量:每个程序对象(如变量、函数参数、堆分配标签)关联一个类型变量向量。例如:
    • 局部变量 p 在函数的 n 个变体中表示为 ,其中 是第 i 个变体中 p 的类型变量。
    • 全局变量因无上下文区分,向量所有分量相同。
  • 表达式向量约束:表达式的约束通过向量分量逐一应用。例如,赋值表达式 p=&x 生成约束 (具体变体)和 (摘要变体)。

向量约束的求解规则

  • 分量独立求解:向量约束的每个分量按传统约束规则独立求解,但需满足摘要变体的包容性,即对所有 i≥1。这确保摘要变体包含所有具体变体的信息。
  • 函数调用约束:当调用函数 g 的第 k 个变体时,实际参数的变体 i 与形式参数的变体 k 需满足约束

过程间约束生成

该小节主要介绍如何在过程间(Inter-procedural)指针分析中生成约束系统,通过扩展静态调用图(SCG)和变体向量(Variant Vector)技术,实现对函数调用上下文的敏感分析。核心内容包括函数变体的约束生成规则调用站点与目标函数的参数映射,以及间接调用和返回值的处理方式

约束生成基本框架

输入假设:程序包含一个静态调用图 SCG,其中每个调用站点 l 和调用上下文变体 i 唯一映射到目标函数 g 的变体 k,即 SCG(l,i)=⟨g,k⟩。

约束系统构成:过程间约束系统由函数内约束(如变量声明、表达式)和跨函数调用约束(如参数传递、返回值)共同组成。

函数变体的约束生成规则

  • 局部变量与参数
    • 对于函数 fn 个变体,其局部变量 v 和参数 x 对应向量,其中:
      • 是摘要变体,包含所有上下文的合并信息;
      • 是第 i 个具体变体的类型变量。
    • 约束示例:声明 int *p = &x 生成 (具体变体)和 (摘要变体)。
  • 全局变量:全局变量无上下文区分,其向量所有分量相同

函数调用的约束生成

直接调用

当调用函数 时(l 为调用站点标签),假设当前函数变体为 i,目标函数变体为 k=SCG(l,i),则生成以下约束:

  1. 参数传递:实际参数 的变体 i 约束目标函数 g 的参数 的变体 k

  2. 返回值约束:调用的返回值抽象位置需包含目标函数返回位置 的信息

间接调用

对于通过指针调用的表达式,由于无法确定具体目标函数,使用摘要变体 0 合并所有可能的调用上下文:即所有变体的返回值均指向摘要位置,不区分具体上下文。

变体向量的摘要约束

包容性约束:为确保摘要变体包含所有具体变体的信息,对每个变量向量添加约束

跨函数摘要传播:当函数 f 调用函数 g 时,f 的摘要变体需吸收 g 的所有具体变体信息,避免信息丢失。

提高的命名约定

该小节主要介绍过程间指针分析中针对堆分配对象的命名优化策略,通过改进抽象位置的命名规则,提升对动态内存分配场景的分析精度。核心内容包括堆对象的标签化处理调用站点唯一性的利用,以及该策略与传统方法的对比优势

堆分配对象的传统分析局限

传统过程内分析将同一函数中多次调用 alloc()(如 malloc)分配的堆对象合并为单一抽象位置(如 l),导致不同调用分配的对象被错误关联。

  • 示例:若函数 f 两次调用 alloc() 分配互不相关的对象,传统分析会将两者均表示为 l,导致指针指向信息混合。

后果:伪指针信息传播至无关代码路径,降低分析精度(如误判两个独立堆对象存在别名)。

基于调用站点的标签化命名

  • 核心思想:为每个 alloc() 调用站点分配唯一标签(如 l^i),其中 i 表示调用该站点的上下文变体编号。同一函数的不同调用站点或不同变体的相同站点均生成不同标签,确保堆对象的唯一性。

  • 标签生成规则

    • alloc() 调用位于函数 f 的第 k 个变体,则其分配的堆对象标签为 l^k
    • 全局或静态调用的 alloc() 标签为 l^0(摘要变体)。
  • 约束表示:分配语句 p = alloc() 生成约束 具体变体 k)和 (摘要变体),确保不同上下文的堆对象在向量分量中分离。

约束解决

本节介绍了一组用于约束系统的保持解的重写规则。我们证明,重复应用这些重写规则可使系统转化为易于找到解的形式。我们认为这个方案是最小的。

为了简单起见,我们只关注过程内约束在这一章。对过程间系统的扩展很直接:类型对按组件方式处理。注意相同的类型变量总是出现在约束的两侧。 实际上,约束会用类型向量的长度进行标注。

重写规则

该小节主要介绍约束系统的重写规则,通过一系列保持解不变的变换将复杂约束简化为易于求解的形式,从而实现指针分析的自动化推导。核心内容包括类型规范化规则传播规则的定义与作用,以及这些规则如何逐步将约束系统转换为可直接求解的规范形式。

重写规则的目标与分类

  • 核心目标:将约束系统中的复杂表达式(如结构体访问、指针解引用、函数类型)逐步拆解为基础约束(如 T ⊇ {o}T1 ⊇ T2),以便通过迭代算法求解最小解。
  • 规则分类
    • 类型规范化规则(Type Normalization Rules):处理结构体、指针解引用、函数类型等复杂结构。
    • 传播规则(Propagation Rules):将推导得到的抽象位置信息传播到相关约束中,消除变量依赖。

类型规范化规则

用于将复杂类型约束转换为基础形式,具体包括:

规则1.a 结构体字段访问

  • 约束形式T ⊇ {s}.i(访问结构体 s 的字段 i

  • 转换:若 s 的类型为 struct S,则替换为 T ⊇ T_{S.i},其中 T_{S.i} 是结构体字段 i 的类型变量。

  • 作用:将结构体字段访问转换为对字段类型变量的直接约束。

规则1.b 指针解引用

  • 约束形式T ⊇ *{o}(解引用指针 o
  • 转换:替换为 T ⊇ T_o,其中 T_o 是指针 o 指向的对象的类型变量。
  • 作用:将指针解引用转换为对目标对象类型的约束。

规则1.c 反向指针解引用

  • 约束形式*{o} ⊇ T(指针 o 指向的对象包含 T 的值)
  • 转换:替换为 T_o ⊇ T,直接约束指针 o 的目标类型。

规则1.d 函数类型约束

  • 约束形式(T_i) → T ⊇ (T_i') → T'(函数类型包含关系)
  • 转换:拆分为参数类型反向包含 T_i ⊇ T_i' 和返回值类型正向包含 T' ⊇ T
  • 作用:将函数类型的包含关系分解为参数与返回值的独立约束。

传播规则

用于将已推导的抽象位置信息传播到其他约束中,消除变量间的依赖,具体包括:

规则2.a 基础传播

  • 约束形式T1 ⊇ T2
  • 操作:若 T2 包含抽象位置 o(即 o ∈ Collect(T2, C)),则添加 T1 ⊇ {o}
  • 作用:将类型变量间的包含关系转换为具体抽象位置的包含关系。

规则2.b 结构体字段传播

  • 约束形式T1 ⊇ T2.i
  • 操作:若 T2 包含结构体对象 s(即 s ∈ Collect(T2, C)),则添加 T1 ⊇ {s}.i
  • 作用:将结构体字段的约束传播到具体对象的字段访问。

规则2.c 指针解引用传播

  • 约束形式T1 ⊇ *T2
  • 操作:若 T2 包含指针对象 o(即 o ∈ Collect(T2, C)),则添加 T1 ⊇ *{o}
  • 作用:将指针解引用的约束传播到具体指针变量。

规则 2.d:反向指针解引用传播

  • 约束形式*T1 ⊇ T2
  • 操作:若 T1 包含指针对象 o(即 o ∈ Collect(T1, C)),则添加 *{o} ⊇ T2
  • 作用:将指针指向对象的约束传播到具体指针变量。

辅助函数:Collect(T,C)

Collect(T, C) 返回约束系统 C 中类型变量 T 所包含的所有抽象位置集合,通过递归遍历约束推导得出。

  • C 包含 T ⊇ {o},则 o ∈ Collect(T, C)
  • C 包含 T ⊇ T'o ∈ Collect(T', C),则 o ∈ Collect(T, C)

用于提取类型变量中已确定的抽象位置,为传播规则提供依据,确保约束推导的完整性。

规则的性质

  • 解保持性(Solution-Preserving):所有重写规则均不改变约束系统的解集,即应用规则后的系统与原系统等价。
  • 终止性(Termination):规则的应用次数有限(因抽象位置集合有限),最终可将约束系统转换为规范形式(仅包含 T ⊇ {o} 形式的基础约束)。
  • 最小解导向:通过规则推导的约束逐步逼近最小解,确保最终解为满足所有约束的最精确结果。

最小解决

该小节主要介绍如何通过重写规则将约束系统化简为规范形式,并从中提取最小解(Minimal Solution),确保指针分析结果在满足安全性的前提下达到最高精度。核心内容包括规范形式的定义最小解的构造方法,以及其与程序实际指针行为的关系。

约束系统的规范形式

定义:经过重写规则(4.7.1 节)的穷尽应用后,约束系统转化为仅包含基础约束的形式,即:

  • 所有约束均为 T ⊇ {o} 的形式,其中 T 是类型变量,o 是抽象位置(如变量名、结构体字段、堆分配标签等)。
  • 不存在复杂约束(如结构体访问、指针解引用、函数类型等)。

关键性质

  • 唯一性:规范形式是唯一的,与重写顺序无关。
  • 可解性:规范形式直接对应类型变量与抽象位置的包含关系,可直接用于构造解。

最小解的构造方法

三步法流程

  1. 重写至规范形式:应用重写规则将原始约束系统 C 转换为规范形式 C'',其中仅包含 T ⊇ {o} 类型的约束。
  2. 提取包含关系:对于每个类型变量 T,收集其在 C'' 中所有包含的抽象位置,构成集合 Collect(T, C'')Collect(T, C'') = { o | T ⊇ {o} ∈ C'' }
  3. 定义 substitution:构造解 S 为类型变量到抽象位置集合的映射,即:S(T)=Collect(T,C′′) 该映射确保每个类型变量 T 被赋值为其在规范形式中包含的所有抽象位置的并集。

最小解的性质

  • 安全性(Safety)
    S 满足原始约束系统的所有条件,即对于任意约束 T1 ⊇ T2,有 S(T1)⊇S(T2)。
    • 这确保分析结果不会遗漏任何可能的指针指向关系,符合 “may point-to” 分析的安全定义(4.4 节)。
  • 最小性(Minimality)
    S 是所有可能解中最精确的,即不存在其他解 S' 满足 S′(T)⊆S(T) 对所有 T 成立且至少有一个 T 严格包含于 S(T)
    • 最小解避免了过度近似,确保分析结果尽可能精确。
  • 构造正确性
    通过数学归纳法可证明,重写规则的穷尽应用能正确推导出所有必要的包含关系,因此 S 是唯一的最小解。

4. 与程序实际行为的关系

  • 抽象与具体的映射
    • 抽象位置 o 对应程序中的具体内存位置(如变量地址、堆块)。
    • 最小解 S 中的集合 S(T) 是程序运行时指针 T 可能指向的所有具体位置的安全抽象(即实际指向的位置集合是 S(T) 的子集)。
  • 处理不确定性
    • 对于无法确定的指针(如经过类型转换或外部函数返回的指针),最小解将其映射到 {Unknown},确保保守处理。
    • 例如,p = (int*)0xabcd 会被抽象为 S(T_p) = {Unknown}

算法部分

在本节中,我们概述一种用于指针分析的算法。算法很想传统的迭代固定指针解决者。更进一步,我们描述一个更方便的表示方法。

表示方法

我们为程序中的每个声明符关联一个指针类型。对于没有声明符的抽象位置,我们创建一个。一个对象通过指向相应声明符的指针进行唯一标识。因此,约束 被表示为 ,这可以在常数时间内被写为

我们为每个类型变量T关联一个声明符(指针)集合T.incl。此外,为每个类型变量假定一个布尔标记T.upd。字段T.incl会随着T包含的对象集合逐步更新。标记T.upd用于指示自 “上次检查” 以来集合是否发生了变化。

迭代约束解决

约束从 可以被提前标准化到 在约束产生的时间,并且因此在解决过程中没有存在。详细的约束产生对用户函数调用。

迭代过程

  • 基础约束 T1 ⊇ {o}:直接将对象 o 添加到 T1.incl 中。例如,p = &x 对应约束 T_p ⊇ {x},则 T_p.incl 包含 x
  • 指针解引用约束 T1 ⊇ *T2
    • T2.incl 包含对象 o(表示 T2 指向 o),则将 o 指向的对象集合(即 T_o.incl)添加到 T1.incl 中。
    • 例如,*q = &y 对应 T_p ⊇ {y}(假设 q 指向 p),则 T_p.incl 包含 y()。
  • 结构体字段约束 T1 ⊇ T2.i:若 T2.incl 包含结构体对象 s,则将 s 的字段 i 对应的类型变量(如 S.i)添加到 T1.incl 中。
  • 函数调用约束 *T0 ⊇ (*T1) → T_result:处理函数指针调用时,根据参数类型和返回值类型更新相关集合。

关键数据结构

  • T.incl:存储类型变量 T 目前指向的所有对象集合(如 {x, y})。
  • T.upd:布尔标记,记录 incl 集合是否在本次迭代中被更新,用于控制迭代终止。
  • clist:约束列表,按类型分类(如赋值约束、解引用约束等),便于遍历处理。

注意指针解引用的情况。如果对 “Unknown” 执行解引用操作,算法将终止并输出 “最坏情况” 消息。例如,在赋值语句p = *q的情况下(其中q被近似为 Unknown),该分析会得出 “最坏情况” 结果。实际上,出现在赋值语句左侧的约束会被 “标记”,且只有这些约束会导致算法终止。

正确性

复杂度

Algorithm 4.1 的时间复杂度是多项式级的,与程序中的声明数量(如变量、函数、结构体等)成线性或多项式关系,而非指数级。

4.9 实验

我们在C-Mix系统实现了一个指针分析。该分析与本章中介绍的分析类似,但在两个方面存在差异:它使用了一个代表显著降低了约束的数量,并且它为指针类型的所有间接寻址计算摘要信息。

前置降低了分析的运行时间,后者增加了时间。请注意,本章的分析仅计算指针首次间接寻址的左值;其他间接寻址必须通过检查指针可能指向的对象来计算。

维护所有间接寻址的摘要信息的值依赖于分析的使用。例如,有了针对所有间接寻址的摘要信息,第 6 章的副作用分析无需在每个间接寻址节点处对指针进行摘要;这在指针分析时完成。另一方面,无用信息也许会积累。我们怀疑本章的分析在实践中更具可行性,但在撰写本文时尚无实证依据支持这一点。

我们已将该分析应用于一些测试程序。所有实验均在一台配备 64 兆内存的 Sun SparcStation II 工作站上进行。结果如下所示。有关程序的描述,请参考第 9 章。

如下所示,该分析速度很快。不过需要强调的是,这些程序均未大量使用指针。尽管如此,我们认为本章的分析在实际应用中仍会展现出相当的运行时间。推断信息的质量良好,即指针得到了准确的近似(在流不敏感的范围内)。平均而言,一个指针的指向集合较小。

:上述报告的约束数量看似不合理!关键在于,生成的大多数超集约束可通过等式求解。所有这些约束均已预先归一化,因此约束系统基本仅包含涉及指针的赋值(调用)约束。

面向程序点的指针分析

本章分析是流不敏感的:它产生了整个函数体的摘要。这提高了效率降低了精确度,如左侧(人为设计的)函数所示。

这个分析忽略了分支和从一个分支可能影响到另一个分支的信息。在这个例子中,精确度的损失体现在指向信息传播到两个调用中。

右边的例子说明了缺乏程序点特定信息。一个程序点特定分析会记录下p会指向x在第一次调用中,并且指向y在第二次调用中。在这一节中我们会关注程序点特定,流敏感指针分析基于约束解决。

程序点是序列点

目标是计算指针抽象对于每一程序点,奖指针映射到对象可能指向的特定程序点的集合。通常来说,通常,程序点被定义为 “两条语句之间的位置”,但在 C 语言中,这一概念与顺序点一致。在一个顺序点中,所有的在前一个点和当前点之间的所有副作用均应已完成。举个例子,存储已经更新了,随后的副作用还没有发生。此外,一个对象最多只能被访问一次以确定其值。最后,访问一个对象应仅用于确定要存储的值。顺序点被定义在Annex C of 标准[ISO 1990]。

在接下来,我们为了简化起见忽略表达式中顺序点,并且使用转换如果S是语句,那么m是在S之前的程序,n是在程序之后的。举个例子,一个顺序语句中,我们有

基于程序点约束的程序分析

这一节简要概括了基于约束或者是基于集合命令式语言的程序分析,Heintze发展的。

对于每一个程序点m,分配一个类型变量向量代表抽象存储。

相应的约束系统与4.5节介绍的相似。但是,传播抽象状态需要额外的约束在程序点之间。举个例子,在程序点4,变量假定了相同的值与,因为它没更新。

约束系统可以被解决通过图42的重写规则解决,但是不幸的是分析不能解决多级指针。

为什么Heintze的基于集合分析失败了

注意如下的程序片段:

在程序点 3 和 4 之间的赋值更新了抽象位置 p,但 “p” 在表达式 “*q = &y” 中并未在语法上出现。产生约束

有两个错误。首先,要通过状态传播的值并非由表达式从语法上给出,举个例子,p在两个程序点3和4之间更新。间接赋值的约束未关联到具体程序点,无法明确确定应更新哪个变量的类型变量。

为了解决第二个问题,可通过为约束附加程序点信息来解决。第一个问题更复杂。未被更新的变量依赖于的解决。由于程序中的循环和自我依赖,也许会依赖于程序点 3 和 4 传播的变量。目前,我们尚未找到解决该问题的有效方法。