ch9.2-12

期末周完全按照重点整理的笔记，比较草率

符号执行

符号执行是一种经典的路径敏感分析技术，它通过枚举并分析程序的每一条路径来实现程序分析。

符号执行作为一种重要的形式化方法和软件分析技术，采用抽象符号代替程序变量，程序计算的输出被表示为输入符号值的函数，根据程序的语义，遍历程序的执行空间。其在软件测试和程序验证中发挥着重要作用，并可以应用于程序漏洞和脆弱性的检测中。

𝝈: 符号存储，把每个程序变量映射到一个符号表达式
𝝅:路径约束，记录当前执行路径上所有条件的组合，初始为 true（表示还没有任何限制）
- 例如：执行到 if (x > 0) 的“真分支”时，会加上约束 x > 0，更新为 𝝅 = 𝝅 ∧ (x > 0)
- 遇到断言 assert(…)，就构造其取反条件
- 是否存在解（satisfiable）

考虑两种到达assert的情况，分别计算check内容（𝝅带入式子），第二种情况a=2, b=0时，x = 4, y = 4 ⇒ x - y = 0，断言x - y != 0不成立，触发断言失败 ⇒ 程序出错（bug）

约束求解（Constraint Solving） 是一种在给定条件（约束）下寻找变量的解的技术

限制:

路径爆炸（Path Explosion）：

符号执行会尝试遍历程序的每个条件分支，路径数量随着分支数量指数增长，导致计算量迅速变得不可控。
外部调用（External Calls）：

程序中调用外部库函数或系统API时，符号执行难以模拟其内部逻辑，影响准确性。
约束求解（Constraint Solving）：

符号执行需要用约束求解器来判断路径条件的可行性，但复杂的约束可能导致求解困难，影响执行效率。

优化:

为了克服这些限制，研究人员提出了多种优化技术，目的是让符号执行更实用：

路径/状态合并（Path/State Merging）：

把多个相似的执行路径合并成一个状态，减少需要跟踪的路径数量，缓解路径爆炸。
循环归纳（Induction for Loops）：

用数学归纳方法分析循环，不必每次迭代都展开符号执行，减少执行次数。
混合符号执行（Concolic Execution）：

结合具体执行（concrete execution）和符号执行，利用具体输入来限制符号路径数量，提高效率。
推测执行（Speculative Execution）：

先猜测可能的执行路径，减少无谓计算。

路径合并
使用 ite 函数（if-then-else）表达式，把两个路径的结果合并成一个表达式：

减少循环

求解路径约束

命题逻辑（Propositional Logic）
- 基础逻辑系统，使用布尔变量和逻辑运算符（如与、或、非）表示问题。
- 可满足性问题（SAT）：判断命题逻辑公式是否存在一组变量赋值使其为真。
  - DPLL算法：经典的SAT求解算法，通过回溯和剪枝搜索解。
  - CDCL算法（冲突驱动子句学习）：现代SAT求解器的核心，通过学习和冲突分析优化搜索效率。
一阶逻辑（First Order Logic）
- 扩展命题逻辑，引入量词（∀、∃）、谓词和函数，表达能力更强。
可满足性模理论（SMT, Satisfiability Modulo Theories）
- 结合SAT求解器和特定理论（如算术、数组、位向量等），解决一阶逻辑公式的可满足性问题。
- 例如，判断“x + y = 5 ∧ x > 3”是否有解。
位向量理论（The Bit Vector Theory）
- SMT中的一种理论，用于处理固定长度的二进制位运算（如硬件验证、加密算法）。

命题逻辑（Propositional Logic, PL）

命题逻辑是最简单的逻辑系统，仅处理原子命题（不可再分的陈述）及其组合。其语法规则如下：

(1) 真值符号（Truth Symbols）

⊤（表示“真”，True）
⊥（表示“假”，False）

(2) 命题变量（Propositional Variables）

用符号表示原子命题，例如：p, q, r, …
例如：p = "今天下雨"，q = "地面是湿的"

(3) 文字（Literals）

一个命题变量或其否定，例如：
- p（正文字）
- ¬p（负文字，表示“非p”）

(4) 公式（Formulas）

通过逻辑运算符组合文字或子公式，递归定义如下：

原子公式：单个文字（如 p 或 ¬q）。
复合公式：
- ¬F：否定（非），例如 ¬p。
- F ∨ F：析取（或），例如 p ∨ q。
- F ∧ F：合取（与），例如 p ∧ q。
- F ⇒ F：蕴含（如果…则…），例如 p ⇒ q（若p为真，则q为真）。
- F ⟺ F：等价（当且仅当），例如 p ⟺ q（p和q同真同假）。

(5) 语义（Semantics）

语义定义了公式的“真假”如何被解释：

每个命题变量通过赋值（Assignment）被赋予真值（⊤ 或 ⊥）。
复合公式的真值由运算符的语义规则决定：
- ¬p 为真 ⇔ p 为假。
- p ∨ q 为真 ⇔ p 或 q 至少一个为真。
- p ∧ q 为真 ⇔ p 和 q 同时为真。
- p ⇒ q 为假 ⇔ p 为真且 q 为假 （其他情况为真）。
- p ⟺ q 为真 ⇔ p 和 q 真值相同。

(6) 合法句子（Well-Formed Formulas, WFFs） 必须严格遵循语法规则。以下是合法的例子：

⊥（假）
⊤ ∧ ⊥（真与假）
p ∨ q（p 或 q）

而 p and q 是非法的，因为命题逻辑中必须使用标准逻辑符号（如 ∧ 代替 “and”）。

(7) 其他

范式（Normal Forms）

定义：范式是对逻辑公式语法形状的限制，通过统一结构来简化分析或计算（如可满足性判定）。
作用：
- 结构化搜索空间（例如，限制运算符的嵌套方式）。
- 简化决策过程（如SAT求解器常要求输入为特定范式）。

否定范式（NNF）

NNF是一种范式，其语法规则如下：

允许的符号：
- 真值符号：⊤（真）、⊥（假）。
- 命题变量：p, q, r, …。
- 文字（Literals）：原子命题或其否定（如 p 或 ¬p），但不允许对复合公式直接否定（如 ¬(p ∧ q) 需转换）。
允许的运算符：
- 仅限 ∧（与）、∨（或）。
- 不允许 ⇒（蕴含）、⟺（等价）、以及对复合公式的 ¬。
公式构造规则：
- 原子公式：文字（如 p 或 ¬q）。
- 复合公式：通过 ∧ 或 ∨ 组合子公式（如 p ∨ (¬q ∧ r)）。

通过以下步骤消除 ⇒、⟺ 和移动 ¬：

消去蕴含和等价：
- A ⇒ B → ¬A ∨ B
- A ⟺ B → (¬A ∨ B) ∧ (A ∨ ¬B)
德摩根律（De Morgan’s Laws）：
- ¬(A ∧ B) → ¬A ∨ ¬B
- ¬(A ∨ B) → ¬A ∧ ¬B
双重否定律：
- ¬¬A → A

示例：

将 ¬(p ⇒ (q ∧ ¬r)) 转换为NNF：

消去蕴含：¬(¬p ∨ (q ∧ ¬r))
德摩根律：p ∧ ¬(q ∧ ¬r)
德摩根律：p ∧ (¬q ∨ r)（最终NNF形式）

NNF的充分性定理

对于命题逻辑中的任意公式 FF，存在一个等价的否定范式（NNF）公式。

析取范式（Disjunctive Normal Form, DNF）

DNF 的充分性定理

对于命题逻辑中的任意公式 FF，存在一个等价的 DNF 公式。

DNF 的局限性： DNF 转换可能导致公式体积指数级增长。

合取范式（Conjunctive Normal Form, CNF）

CNF 的充分性定理

对于命题逻辑中的任意公式 FF，存在一个等价的 CNF 公式。

可满足性等价

Tseitin Transformation

Tseitin变换是一种将任意命题逻辑公式高效转换为CNF（合取范式）的方法，通过引入辅助变量避免经典CNF转换中的指数级规模膨胀。其核心特点是：

保持可满足性（Equisatisfiable）：新生成的CNF公式与原公式的可满足性一致（但未必逻辑等价）。
线性规模增长：转换后的CNF公式规模最多是原公式的常数倍。

SAT问题

流程：

DPLL算法

DPLL（Davis-Putnam-Logemann-Loveland）算法是一种经典的回溯搜索算法，用于解决命题逻辑公式的可满足性问题（SAT）。其核心思想是通过**决策（Decision）和传播（Propagation）**逐步缩小搜索空间，最终找到满足公式的赋值或证明其不可满足。

bool DPLL(F, I) {
    if (F == false) return UNSAT;  // 公式为假，无解
    if (F == true)  return SAT;    // 公式为真，当前解释有效
    p = choose(F);                 // 选择一个未赋值的变量 p
    if (DPLL(F[p→true], I[p→true]) == SAT) return SAT;  // 尝试 p=true
    return DPLL(F[p→false], I[p→false]);                // 回溯尝试 p=false
}

例子：

冲突驱动子句学习（CDCL）

核心思想

CDCL是DPLL算法的增强版，通过动态学习冲突子句来避免重复搜索无效路径，显著提升SAT求解效率。其核心改进在于：

冲突分析：当赋值导致矛盾时，分析冲突原因并生成新的子句（称为学习子句）。
非时序回溯：根据学习子句直接跳转到冲突的根源层级，而非简单回溯。

关键步骤

决策（Decision）：选择未赋值的变量并赋值（如 x1=1）。
传播（Propagation）：通过单元传播推导其他变量的值。
冲突检测：若发现某个子句无法满足（如 x∧¬x），触发冲突分析。
学习子句生成：从冲突中提取新的子句加入CNF。
回溯（Backjumping）：根据学习子句跳转到早期决策点，避免无效搜索。

为什么学习子句有效？

剪枝搜索空间：新子句阻止未来出现相同的冲突组合（如 x0=0∧x1=1x0=0∧x1=1）。
指导回溯：避免逐层回溯，直接跳转到关键决策点。

CDCL vs DPLL

特性	DPLL	CDCL
回溯方式	时序回溯（逐层撤销）	非时序回溯（跳转到冲突根源）
学习能力	无	动态生成学习子句
效率	较低（可能重复搜索）	高（通过学习避免冗余）

比特向量理论（Theory of Bit Vectors）

1. 理论定义

作用：为一阶逻辑提供固定长度二进制数的语义（如32位整数）。
核心操作：
- 逻辑运算：按位与（∧）、或（∨）、非（¬）。
- 比较运算：有符号小于（slt）、无符号小于（ult）。
- 算术运算：加减乘除、位移等。

可满足性模理论（SMT）

1. SMT求解流程

针对一阶逻辑公式+理论（如比特向量），SMT求解器分三步处理：

步骤1：词级预处理（Word-Level Preprocessing）

目标：简化公式，应用理论特定的推理规则。
操作：
- 常量传播、等式链合并。
- 示例：x + 1 = y ∧ y = 2 → x = 1。

步骤2：比特爆破（Bit-Blasting）

目标：将高阶公式转换为等价的命题逻辑公式（PL）。
操作：
- 将比特向量变量拆解为单个比特（如32位整数→32个布尔变量）。
- 将算术/逻辑操作转换为布尔电路。
- 示例：a[3:0] + b[3:0] → 生成4位加法器的布尔约束。

步骤3：DPLL/CDCL求解

目标：调用SAT求解器（如DPLL或CDCL）处理生成的布尔公式。
关键点：
- 结合理论求解器（如比特向量理论）验证中间赋值的合法性。

2. 为什么需要SMT？

直接FOL求解困难：一阶逻辑本身不可判定（无通用算法）。
理论加持：通过限制域（如整数、比特向量），使问题可判定。

Andersen & Steensgaard Algorithm

两种算法均可建模为有向图的传递闭包问题：

Andersen’s Alg. as Graph Closure

指令调度

为什么编译器很重要？

硬件只能执行已经被取指（fetched）的指令
硬件用于缓存需要等待的操作的空间是有限的
编译器可以将相互独立的操作放得更近一些，以便更好地利用硬件资源

指令调度（instruction scheduling） 是一种代码优化手段，常见于优化编译器，其主要功能在于通过加强指令层级的并行运行，使得程序在拥有指令流水线的中央处理器上能够高效运行。换句话说，此手段力求以不改变程序运算结果的方式，完成以下任务：通过重组指令的运行顺序，减少或阻止流水线停顿的发生;阻止非法操作（即未定义行为）的产生，例如涉及流水线时序、非互锁资源的等等操作。其中流水线停顿主要由结构型冒险（受处理器的资源所限）、数据型冒险以及控制流型冒险导致。

数据型冒险：当前指令的执行依赖与上一条指令执行的结果。数据冒险可能产生数据流依赖。
结构型冒险：多条指令同时访问处理器的同一个硬件单元的时候，由于缺少相应的资源，导致结构型冒险
控制型冒险：存在分支跳转，不确定下一条要执行的指令，导致其产生的控制型冒险

为什么要指令调度： 更好利用处理器并行性，指令重排将并行度高的指令排在一起（加上上面定义里的）

目前数据流依赖关系主要有以下三种：

假设第一条执行的指令为I1，下一条执行的指令为I2

True（flow）dependence：是真正的数据流依赖，也叫流依赖，即RAW（Read After Write），指令I2的输入，需要等到指令I1的输出
Anti-dependence：反依赖，即WAR（Write After Read），指令I2需要用到I1指令的数据或者覆盖I1指令
Output dependence：输出依赖，WAW（Write After Write），指令I1与指令I2同时写一块内存，指令I1和指令I2之间可能存在使用指令I1的其他指令

当前输出依赖和反依赖均可称为假依赖。真依赖是绝对不能改变指令之间的执行顺序，但是假依赖的话，一般可以通过寄存器重命名或者变量重命名的方式，来解决依赖关系，从而使其有机会改变指令之间的执行顺序：

依赖关系图：节点是指令，边是真依赖

表调度（List Scheduling）

表调度是一种贪心+启发式方法，用以调度基本块中的各个指令操作，是基本块中指令调度的最常见方法。

表调度的基本思想：

维护一个用来存储已经准备执行的指令的ready列表和一个正在执行指令的active列表，ready列表的构建主要基于数据依赖约束和硬件资源信息；根据调度算法以周期为单位来执行具体的指令调度，包括从列表中选择及调度指令，更新列表信息。

基本的表调度算法大致分为以下三步：

根据指令间依赖，建立依赖关系图。
根据当前指令节点到根节点的长度以及指令的latency，计算每个指令的优先级。
不断选择一个指令，并调度它，a. 使用两个队列维护ready的指令和正在执行的active的指令；b. 在每个周期：选择一个满足条件的ready的指令并调度它，更新ready队列；检查active的指令是否执行完毕，更新active列表

假设LD/ST 3 cycles; MUL 2 cycles; ADD 1 cycle：

如果一个指令节点上面的节点仍在active里（即图中颜色较淡的节点），且没有其他可选择的指令时nop。

本文作者：RyoCY
本文链接：https://squirrelune.github.io/cn/2025Spring-%E7%BC%96%E8%AF%91%E5%8E%9F%E7%90%86/%E7%BC%96%E8%AF%91%E5%8E%9F%E7%90%8607/
许可协议： 除特殊声明外，本站博文均采用 CC BY-NC-SA 3.0 CN 许可协议，转载请注明出处！

编译原理07