12-符号执行

定义：将程序中的变量替换为符号值，执行程序以探索所有可能的路径。
- 每个输入变量和一个符号关联
- 每个表达式都是符号表达式
- 程序的路径：以路径约束（一组条件表达式）描述分支处的路径选择
路径敏感 Path-Sensitive：程序中不同的执行路径会被分别分析、分别追踪。
目标：发现程序中的错误、漏洞或不符合预期的行为（如除零错误、越界访问等）。

检查断言：约束求解

$\sigma$ ：记录符号值，如𝝈 = { a -> 𝜶_a ; b -> 𝜶_b ; x -> 1 ; y -> 0 }，在语句执行后改变
$\pi$ ：路径约束，记录分支条件，如𝜋 = { x > 0 ; y < 10 }，初始为true，在每一次分支处改变
检查assert(cond)语句：构造违反条件： $eg cond$ ，如果 $\pi \land \neg cond$ 为假（即在 $\pi$ 条件下不可能发生违反条件），则不会失败

int x = 1, y = 0;
if (a != 0) {
    y = 3 + x;
    if (b == 0) {
        x = 2 * (a + b);
    }
}
assert(x - y != 0);

下一步目标：检查诸如 $\pi \land \neg cond$ 的条件判断式是否成立
使用约束求解器 Constraint Solver 来判断是否满足条件
- 可满足 Satisfiable：存在assert失败的可能性
- 不可满足 Unsatisfiable：assert不会失败
- 未知 Unknown：无法确定是否存在失败可能性（过于复杂，超时）

限制

可拓展性
- Path Explosion：路径数量随着分支和循环的增加而指数级增长
- External Calls：外部函数调用可能导致路径不确定
- Constraint Solving：复杂的约束可能导致求解器无法处理
优化方法
- Path/State Merging：合并相似路径或状态，减少路径数量
  - 引入ite(cond, true_val, false_val)函数，合并相似路径
- Induction for Loops：对循环进行归纳，减少路径数量
  - 把循环内容转化为条件表达式（不一定始终可用）
- Concolic Execution：结合符号执行和具体执行，运行时生成符号值
- Speculative Execution：预测路径，提前执行可能的分支

可满足性 Satisfiability

命题逻辑 Proposition Logic

只涉及命题变量和逻辑运算，不涉及具体变量的运算
真值符号（ $b$ ）： $\top$ 和 $\bot$ （真和假）
命题变量（ $v$ ）： $p$ 、 $q$ 、 $r$ 等
文字（ $l$ ）：原子或其否定
公式（ $F$ ）：
- $l$
- $\lnot F$ （否定）
- $F_1 \lor F_2$ （或）
- $F_1 \land F_2$ （与）
- $F_1 \Rightarrow F_2$ （蕴含）
- $F_1 \Leftrightarrow F_2$ （等价）
可满足 Satisfiable：存在一种真值赋值使得公式为真
有效 Valid：对于所有真值赋值，公式都为真
在命题逻辑中的所有公式 $F$ ， $F$ 有效当且仅当 $\lnot F$ 不可满足

范式 Normal Form

对公式语法的限制，把公式语法规范化为某种接口
有助于简化判定流程

否定范式 Negation Normal Form (NNF)

定义：不允许使用蕴含/等价（ $ightarrow \Leftrightarrow$ ）运算符，只允许对变量取否（ $\lnot$ ），不允许对更复杂的子公式取否
所有的公式都可以转换为 NNF

合取范式 Conjunctive Normal Form (CNF)

定义：合取范式（CNF）是一个公式，由若干“析取项（ $\lor$ ）”之间通过合取（ $\land$ ）连接组成。
- 公式中只允许使用 $\lor$ 、 $\land$ 和 $\lnot$ ，其中：
- $\lnot$ 只能作用于原子命题变量
- 最外层是合取（ $\land$ ）。
- 析取项中不应再包含 $\land$ 。
形式： $(l_1 \lor l_2 \lor \ldots) \land (l_3 \lor \lnot l_4 \lor \ldots) \land \ldots$
所有的公式都可以转换为 CNF

析取范式 Disjunctive Normal Form (DNF)

定义：析取范式（DNF）是一个公式，由若干“合取项（ $\land$ ）”之间通过析取（ $\lor$ ）连接组成。
- 公式中只允许使用 $\lor$ 、 $\land$ 和 $\lnot$ ，其中：
- $\lnot$ 只能作用于原子命题变量
- 最外层是析取（ $\lor$ ）。
- 合取项中不应再包含 $\lor$ 。
形式： $(l_1 \land l_2 \land \ldots) \lor (l_3 \land \lnot l_4 \land \ldots) \lor \ldots$
所有的公式都可以转换为 DNF

Tseitin Transformation

同时可满足性 Equisatisfiability

定义：两个公式 $F_1$ 和 $F_2$ 是同时可满足的，当且仅当 $F_1$ 可满足等价于 $F_2$ 可满足
- 说人话：两个公式要么都是可满足的，要么都是不可满足的
对于任意公式 $F$ ，可以构造一个同时可满足的 CNF 范式公式 $F'$ ，且 $F'$ 的大小倍数是常数级别的

具体实现

建立语法树，把每一个叶子节点对应的表达式 $F_i$ 替换为一个新的变量 $x_i$
根节点 $F_1$ 转换为 $x_1 \land (x_1 \Leftrightarrow F_1)$
随后在式子后面加上 $\land (x_i \Leftrightarrow F_i)$ ，直到所有的叶子节点都被替换
通过下面大一离散课的知识，把所有的 $\Leftrightarrow$ 和 $ightarrow$ 替换为 CNF 形式的合取范式

离散课回忆

原始逻辑形式

用与/或/非表示

$A \Rightarrow B$

$\lnot A \lor B$

$A \Leftrightarrow B$

$(A \lor \lnot B) \land (\lnot A \lor B)$

SAT 问题

找到是否存在能让 $F$ 为真的变量赋值
解决方法
- 通过 Tseitin Transformation 转换为 CNF
- 使用 DPLL 算法（Davis-Putnam-Logemann-Loveland）

DPLL 算法

选择一个变量 $v$ ，赋值为真/假
传播这个变量的值
优化
- $(a_0 \lor a_1 \lor \ldots \lor a_n \lor c) \land (b_0 \lor b_1 \lor \ldots \lor b_m \lor \lnot c)$ 可转化为 $(a_0 \lor a_1 \lor \ldots \lor a_n \lor b_0 \lor b_1 \lor \ldots \lor b_m)$

bool DPLL (F, I) {
  if (F == false) return UNSAT;
  if (F == true) return SAT;
  
  p = choose(F);
  bool ret = DPLL(F[pàtrue], I[pàtrue])
  if (ret == SAT) return SAT;
  
  return DPLL(F[pàfalse], I[pà false]);
}

CDCL 算法

Conflict-Driven Clause Learning
从矛盾中学习，优化算法速度
略，来不及复习了

一阶逻辑 First-Order Logic (FOL)

定义：由对象（objects）和它们之间的关系（relations）构成的逻辑系统，可以表达“某个对象”、“对象之间的关系”和“对象上的函数”等更复杂结构。
- 对象符号： $a, b, c, \ldots$ ，表示具体的对象或个体。
- $n$ -元谓词： $p(t_1, t_2, \ldots, t_n)$ ，输入 $n$ 个对象，输出一个真假值（True/False）。
- $n$ -元函数： $f(t_1, t_2, \ldots, t_n)$ ，输入 $n$ 个对象，输出一个关系。
- 公式：通过连接词和量词构造的逻辑表达式。
  - $\top$ $\bot$
  - 原子公式 $t$
  - $eg, \lor, \land, \Rightarrow, \Leftrightarrow$
  - $\forall x. F$ $\exists x. F$
Theory of Bit Vectors：所有数据都是有长度的位向量，把运算看作位向量上的逻辑运算，可以将 FOL 转化为 PL

Satisfiability Modulo Theories

词级别处理，在词层面化简逻辑公式
Bit blasting：将公式转换为位向量的形式，把 FOL 转化为 PL
问题转化为 SAT 问题，使用 DPLL 或 CDCL 算法求解

上一页11-数据流分析下一页13-过程间分析

最后更新于1个月前