小袁的秘密基地
  • 🙌🏻Hi there!
  • 🧑🏻‍💻学习碎片
    • Golang
    • Java
    • Python
    • C++
    • Rust
    • 计算机网络
    • 操作系统与 Linux
    • 数据存储
    • 消息队列
    • 分布式系统
    • 云原生与 DevOps
    • 网络安全
    • 数据结构与算法
    • 业务场景
  • 🧑🏻‍🏫系统性学习
    • Go 底层设计
    • Go 高手技法
    • K8s 入门实战
    • 分布式系统典型实例
    • 数据密集型应用系统设计
    • 常见设计模式总结
    • 程序数据流静态分析指北
    • MySQL 实战技巧
    • ElasticSearch 101
  • 📝Leetcode
    • 二分查找
    • 动态规划
    • 哈希表
    • 双指针
    • 数学
    • 数据结构
    • DFS
    • BFS
    • 位运算
    • 模拟
    • 剑指 Offer
    • Go CodeTop 题解
  • 🫥CQUPT
    • 算法设计与分析
    • 计算机组织与结构
    • 计算机图形学
    • 大数据导论
由 GitBook 提供支持
在本页
  • Introduction
  • 莱斯定理(Rice's Theorem)
  • Sound & Complete
  • Abstraction & Over-approximation
  • Intermediate Representation
  • Compiler
  • AST vs. IR
  • 3-Address Code(3AC)
  • Static Single Assignment(SSA)
  • Control Flow Analysis
  • Data Flow Analysis
  • Notations for Constraints
  • Applications
  1. 系统性学习

程序数据流静态分析指北

上一页常见设计模式总结下一页MySQL 实战技巧

最后更新于1个月前

本文整理自南京大学(NJU)《软件分析》,包含 Intro、IR、应用三部分。

Introduction

莱斯定理(Rice's Theorem)

"Any non-trivial property of the behavior of programs in a r.e. language is undecidable"

不存在 Perfect static analysis

Sound & Complete

Sound
Truth
Complete

Overapproximate

All possible true program behaviors

Underapproximate

报告范围 Sound 会更多,为了保证程序可靠,会尽可能多地报 bug,但是可能存在误报。Complete 为了确保不“冤枉”程序,会保证所报的 bug 均是确切的 bug,从而导致漏报。

几乎所有的静态分析都是 Sound,如图:

图中仅分析了蓝色路径会得到错误的结论 —— Safe Cast,而 Sound 需要考虑到所有的情况进而得到 Not Safe Cast 的结论。

Useful Static Analysis —— 在 Sound 的前提下,精度与速度间进行有效平衡。

Abstraction & Over-approximation

​ abstraction 是把具体域映射成抽象域。e.g. 抽象域可以包括:

+、−、0、⊤(unknown),⊥(undefined)+、 -、 0、 \top\text{(unknown)}, \bot\text{(undefined)}+、−、0、⊤(unknown),⊥(undefined)

,over-approximation 再对抽象域进行运算关系 (transfer functions) 与控制流 (control flow) 的近似。

Intermediate Representation

Compiler

AST vs. IR

// do i = i + 1; while (a[i] < v)

IR 三地址码
1: i = i + 1
2: t1 = a[i]
3: if t1 < v goto 1
AST
IR

高级并贴合 grammar structure

低级并接近汇编

依赖不同的编程语言

和其他语言无关

缺乏控制流信息 e.g.不能清晰看出循环

包含控制流信息

3-Address Code(3AC)

右侧只能有一个操作符,e.g.

c = a + b + 3 => t1 = a + b; c = t1 + 3;

地址(Address)可以由以下部分组成:

  • Name: a, b, c

  • Constant: 3

  • Compiler-generated temporary: t1

常见的三地址码形式

x = y bop z
x = uop y
x = y
goto L
if x goto L
if x rop y goto L

/**
x, y, z: addresses
bop: binary arithmetic or logical operation
uop: unary operation (minus, negation, casting)
L: a label to represent a program location
rop: relational operator (>, <, ==, >=, <=, etc.)
goto L: unconditional jump
if … goto L: conditional jump
**/

Static Single Assignment(SSA)

  • Give each definition a fresh name

  • Propagate fresh name to subsequent uses

  • Every variable has exactly one definition

// 3AC
p = a + b
q = p - c
p = q * d
p = e - p
q = p + q

// SSA
p1 = a + b
q1 = p1 - c
p2 = q1 * d
p3 = e - p2
q2 = p3 + q1

Control Flow Analysis

  • Usually refer to building Control Flow Graph (CFG)

  • CFG serves as the basic structure for static analysis

  • The node in CFG can be an individual 3-address instruction, or (usually) a Basic Block (BB)

Basic Blocks(BB)

Basic blocks (BB) are maximal sequences of consecutive three-address instructions with the properties that.

  • 入口为第一个指令

  • 出口为最后一个指令

禁止中途进出

Control Flow Graphs(CFG)

  • The nodes of CFG are basic blocks

  • There is an edge from block A to block B if and only if

    • There is a conditional or unconditional jump from the end of A to the beginning of B

    • B immediately follows A in the original order of instructions and A does not end in an unconditional jump

  • It is normal to replace the jumps to instruction labels by jumps to basic blocks

Data Flow Analysis

How Data Flows on CFG

Data-flow analysis is to find a solution to a set of safe-approximation-directed constraints on the IN[s]’s and OUT[s]’s, for all statements.

  • constraints based on semantics of statements (transfer functions)

  • constraints based on the flows of control

Notations for Constraints

Transfer Function

Control Flow

Applications

Reaching Definitions Analysis

基本概念

  • 假定 x 有定义 d (definition),如果存在一个路径,从紧随 d 的点到达某点 p,并且此路径上面没有 x 的其他定义点,则称 x 的定义 d 到达 (reaching) p。

  • 如果在这条路径上有对 x 的其它定义,我们说变量 x 的这个定义 d 被杀死 (killed) 了

在实践中这个算法可以用来检测未定义的变量:e.g. 每一个变量 v 在 CFG 入口会有一个虚拟定义(dummy definition),虚拟定义 v 到达使用 v 的某点 p 时,那么 v 可能会在定义前被使用。

Transfer Function & Control Flow

Algorithm

OUT[entry] = NULL;
for (each basic block B(排除 entry)) {
	OUT[B] = NULL;
}
while (changes to any OUT occur) {
	for (each basic block B(排除 entry)) {
		IN[B] = Union(所有前驱 OUT[P]);
		OUT[B] = gen(B) Union (IN[B] - kill(B));
	}
}

e.g.

  • 首先让所有 BB 和入口的 OUT 为空。因为你不知道 BB 中有哪些 D(definition)。

  • 当任意 OUT 发生变化,则分析出的定值可能需要继续往下流动,所需要修改各 BB 的 IN 和 OUT。

  • 先处理 IN,然后再根据转移方程完成更新 OUT。

  • 在转移方程中,kill 与 gen 相关的 bit 不会因为 IN 的改变而发生改变,而其它 bit 又是通过对前驱 OUT 取并得到的,因此其它 bit 不会发生 1 => 0 的情况。所以,OUT 是不断增长的,而且有上界,因此算法最后必然会停止。

  • 因为 OUT 没有变化,不会导致任何的 IN 发生变化,因此 OUT 不变可以作为终止条件。我们称之为程序到达了不动点(Fixed Point)

Live Variables Analysis

基本概念

  • 变量 x 在程序点 p 上的值是否会在某条从 p 出发的路径中使用

  • 变量 x 在 p 上活跃,当且仅存在一条从 p 开始的路径,该路径的末端使用了 x,且路径上没有对 x 进行覆盖。

在被使用前,v 没有被重新定义过,即没有被 kill 过。

这个算法可以用于寄存器分配。

Transfer Function & Control Flow

Algorithm

IN[exit] = NULL;
for (each basic block B(排除 exit)) {
	IN[B] = NULL;
}
while (changes to any IN occur) {
	for (each basic block B(排除 exit)) {
		OUT[B] = Union(所有后继 IN[S]);
		IN[B] = use(B) Union (OUT[B] - def(B));
	}
}

e.g.

  • 考虑 BB 及其后继 S。若 S 中,变量 v 被使用,那么我们就把 v 放到 S 的 IN 中,交给 BB 来分析。

  • 在一个 BB 中,若变量 v 被使用,那么我们需要添加到我们的 IN 里。而如果 v 被定义,那么在其之上的语句中,v 都是一个非活跃变量,因为没有语句再需要使用它。

  • 对于转移方程,IN 是从后继 OUT 中删去重新赋值的变量,然后并上使用过的变量。在同一个 BB 中,变量 v 的 def 先于 use ,那么实际上效果和没有 use 是一样的。

Available Expressions Analysis

基本概念

  • x + y 在 p 点可用的条件:从流图入口结点到达 p 的每条路径都对 x + y 求了值,且在最后一次求值之后再没有对 x 或 y 赋值

如果一个表达式上次计算的值到这次仍然可用,我们就能直接利用其中值,而不用进行再次的计算。

Transfer Function & Control Flow

Algorithm

OUT[entry] = NULL;
for (each basic block B(排除 entry)) {
	OUT[B] = ALL;
}
while (changes to any OUT occur) {
	for (each basic block B(排除 entry)) {
		IN[B] = Merge(所有前驱 OUT[P]);
		OUT[B] = gen(B) Union (IN[B] - kill(B));
	}
}

e.g.

一开始确实无任何表达式可用,因此被初始化为空集是自然的。其它 BB 的 OUT 被初始化为全集是因为当 CFG 存在环时,一个空的初始化值,会让取交集阶段直接把第一次迭代的 IN 设置成 0,无法进行正确的判定了。

Analysis Comparison

Reaching Definitions
Live Variables
Available Expressions

Domain

Definitions

Variables

Expressions

Direction

Forward

Backward

Forward

May/Must

May

May

Must

Boundary

OUT[Entry] = NULL

IN[Exit] = NULL

OUT[Entry] = NULL

Initialization

OUT[B] = NULL

IN[B] = NULL

OUT[B] = ALL

Transfer Function

OUT = gen() Union (IN - kill())

OUT = gen() Union (IN - kill())

OUT = gen() Union (IN - kill())

Meet

Union

Union

Merge

🧑🏻‍🏫
南京大学 Static Program Analysis