符号执行与SemFix、DirectFix 、Angelix的主要思想

一、符号执行

1.引言

在软件开发的不断演进中，确保代码的可靠性和安全性至关重要。符号执行是一种在过去几十年中逐渐受到关注的技术，用于分析软件，通过探索所有可能的执行路径而不依赖于具体输入。

2.什么是符号执行？

符号执行的核心是一种程序分析技术，起源于20世纪70年代中期，用于检查软件程序在所有可能的使用场景下是否满足特定属性。与传统测试不同，传统测试使用具体输入（如特定的数字或字符串）运行程序并观察其行为，符号执行将输入视为抽象符号。这些符号代表一系列可能的值，并使用约束求解器——如满足模理论（SMT）求解器来确定特定条件（如安全漏洞或bug）是否可以触发。

假设你在测试一个程序，确保它没有绕过身份验证的后门。在具体执行中，你可能会使用随机输入进行测试，但如果后门只在非常特定的条件下激活，你可能会错过关键场景。然而，符号执行可以系统地探索所有可能的路径，使其非常适合发现诸如除零、NULL指针解引用或身份验证绕过等问题。

文章指出，符号执行在过去的四十年中已被整合到数十种工具中，导致软件可靠性方面的突破，尤其是在安全和测试应用中。一个显著的例子是自2008年以来微软在开发过程中的使用，它发现了Windows 7中其他方法未发现的近30%的bug。

3.关键概念

作者介绍了几个使符号执行独特的基础概念：

1. 符号执行与具体执行：在具体执行中，程序使用特定的输入运行，每次只探索一条路径。符号执行则使用符号（如、）来表示输入，从而同时探索多个路径。每条路径都由一条路径约束（布尔公式）和一个符号内存存储（将变量映射到符号表达式）来跟踪。

2. 路径约束与SMT求解器：随着程序的执行，符号引擎构建路径约束，这些约束描述了特定路径被采用的条件。然后，SMT求解器检查这些约束是否可满足，即是否存在具体值可以触发该路径。如果约束不可满足，则丢弃该路径。

3. 正向与反向执行：研究主要关注正向符号执行，从程序的入口点开始向外探索。然而，它也讨论了反向符号执行，从目标点（如错误）开始向后工作，以找到可以到达它的输入。

4.示例

考虑图1中的C代码，假设我们的目标是确定哪些输入会导致函数foobar第8行的断言失败。由于每个4字节输入参数可以有高达2^32个不同的整数值，使用随机生成的输入具体运行函数foobar不太可能恰好找到导致断言失败的输入。通过使用符号（而不是具体值）来评估代码，符号执行克服了这一限制，使得可以对输入类别进行推理，而不仅仅是单一的输入值。

更具体来说，凡是无法通过代码静态分析确定的值，例如函数的实际参数或从流中读取数据的系统调用的结果，都由符号表示。在任何时候，符号执行引擎都会维护一个状态（stmt, σ, π），其中：

• stmt 是下一个要评估的语句。目前，我们假设stmt可以是赋值语句、条件分支或跳转语句。

• σ 是一个符号存储，将程序变量与具体值的表达式或符号值关联起来。

• π 表示路径约束，即一个公式，表达了由于执行中采取的分支而对符号作出的一组假设。在分析开始时，π = true。

根据stmt的不同，符号引擎会以下列方式更改状态：

• 对赋值语句x = e的评估会更新符号存储σ，将x与新的符号表达式关联起来。我们用表示这种关联，其中是通过在当前执行状态的上下文中评估e获得的，可以是涉及符号和具体值的单目或双目运算符的任何表达式。

• 对条件分支的评估会影响路径约束π。符号执行通过创建两个具有路径约束π_true和π_false的执行状态来进行分支，这分别对应于两个分支： 和 ，其中是通过评估e获得的符号表达式。符号执行在这两个状态上独立进行。

• 对跳转语句goto s的评估通过将符号执行推进到语句s来更新执行状态。

函数foobar的符号执行可以有效地表示为一个树，如图2所示。最初（执行状态A），路径约束为true，输入参数a和b与符号值相关联。在第2行初始化局部变量x和y后，符号存储更新，将x和y分别与具体值1和0关联（执行状态B）。第3行包含一个条件分支，执行被分支：根据选择的分支，接下来评估的语句不同，并且对符号作出不同的假设（分别对应执行状态C和D）。在 ≠ 0的分支中，变量y被赋值为x + 3，在状态E中得到，因为在状态C中。通常，算术表达式的评估只是简单地操作符号值。在扩展每个执行状态直到所有分支到达第8行的断言后，我们可以检查哪些输入值（参数a和b）会导致断言失败。通过分析执行状态{D, G, H}，我们可以得出结论，只有状态H会使x - y = 0为真。此时，状态H的路径约束隐式定义了对foobar不安全的输入集。特别是，任何满足以下条件的输入值：

都会导致断言失败。通过调用SMT求解器来解决路径约束，最终可以确定不安全的输入参数实例，在此例中会得出a = 2和b = 0。

5.主要挑战

虽然符号执行非常强大，但它面临几个挑战，限制了其在实际复杂软件中的可扩展性和实用性：

• 内存处理：程序经常使用指针、数组和复杂数据结构。符号引擎必须处理符号地址（不仅是值），这可能导致可能状态数量的爆炸性增长。

• 环境交互：软件与外部系统（如文件系统、库）交互，这可能引入难以符号化建模的副作用。例如，系统调用可能创建文件，从而影响后续执行路径。

• 路径爆炸：程序中的每个分支（如if语句、循环）都可以分叉出新的执行路径。在具有许多分支或循环的程序中，路径数量可能呈指数增长，使得穷尽性探索变得不可行。

• 约束求解：SMT求解器虽然强大，但处理复杂约束（如非线性算术或涉及超越函数的操作）时可能遇到困难。解决这些问题可能计算代价高昂，甚至不可判定。

这些挑战通常迫使在可靠性（找到所有可能的问题）和完整性（避免假阳性）与性能和可扩展性之间进行权衡。

6.创新解决方案

为了解决这些挑战，研究人员开发了一系列复杂技术，调查将这些技术分类并详细解释：

1. 混合符号与具体执行（混合执行）：

   • 动态符号执行（DSE）：这种方法将具体执行（使用实际输入）与符号执行相结合。例如，程序可能使用随机输入运行，符号引擎跟踪约束。为了探索新路径，它否定一个分支条件，并使用SMT求解器找到新的输入。像DART和SAGE这样的工具体现了这一点，SAGE被称为“白盒模糊测试器”，因为它系统但部分地探索了路径。

   • 选择性符号执行：像这样的工具专注于软件堆栈的特定组件，通过交替进行具体和符号执行来平衡深度和广度，从而在保持有意义的分析的同时减少开销。

2. 内存模型：

   • 完全符号内存：将所有内存地址视为符号，使用状态分叉（为每个可能的地址创建新状态）或if-then-else公式（在单个状态中编码多个可能性）。像BITBLAZE和ANGR这样的工具使用这种方法，尽管它可能资源密集。

   • 地址具体化：通过将符号地址固定为具体值来简化问题，从而减少复杂性，但可能错过某些路径（例如DART和CUTE）。

   • 部分内存建模：一种折中方案，其中写入的地址被具体化，但从小地址范围读取时保持符号（例如MAYHEM）。

   • 延迟初始化：推迟初始化复杂数据结构（如链表），直到访问时使用前提条件来修剪无效状态（例如在C++和Java中）。

3. 路径爆炸缓解：

   • 修剪不可实现路径：使用SMT求解器在早期丢弃不可满足约束的路径，这种策略称为急切求值。

   • 函数和循环总结：为重复的代码片段（如函数、循环）创建摘要，以重用结果，减少冗余工作。例如，Proteus总结多路径循环。

   • 状态合并：将相似路径合并为单个状态，使用析取来表示多个结果，而不进行过度近似。这可以减少活跃状态的数量，但增加了求解器的复杂性。

   • 路径包含和等价：使用技术如插值（从不可满足路径中推导属性，以避免类似探索）来识别和跳过冗余路径。

4. 约束求解优化：

   • 延迟约束：推迟解决复杂约束，直到稍后，可能减少求解器负载，但增加了活跃状态的数量。

   • 具体化：使用具体值来简化不可解决的约束，以性能换取一些可靠性。

   • 高级求解器：调查称赞像Z3这样的工具，它支持广泛的理论（如位向量、数组、非线性算术），使其成为现代符号执行器的首选。

7.实际应用

符号执行不仅是理论上的——它正在产生实际的影响。调查突出了其在以下方面的应用：

• 软件测试：生成测试输入以实现高覆盖率，如KLEE和EXE这样的工具，它们为复杂系统自动创建测试用例。

• 安全：检测缓冲区溢出和身份验证绕过等漏洞。DARPA网络大挑战赛（2016年）展示了像ANGR和MAYHEM这样的系统，它们能够实时自动检测并修补漏洞，为数百万奖金而竞争。

• 代码分析：应用包括程序反混淆和动态软件更新，其中符号执行帮助理解和修改代码行为。

一个突出的例子是微软在Windows 7开发中使用符号执行，它发现了其他方法未发现的30%的bug。

8.展望未来

可以通过相关领域引入技术来增强符号执行。包括：

• 分离逻辑：更好地处理基于指针的数据结构。

• 不变式和循环分析：紧凑地捕获循环行为并提高可扩展性。

• 符号计算：更有效地处理非线性约束，可能将SMT求解器和高级数学方法之间的差距填补。

对于开发人员和安全专业人士来说，符号执行是一个改变游戏规则的技术。它提供了对软件行为的更深入洞察，捕获了传统测试可能错过的难以捉摸的bug，并通过探索这些场景来增强安全性。然而，其复杂性意味着它不是万能的——在性能、可靠性和可扩展性之间进行权衡是一个持续的挑战。

二、程序修复的分类与评估

自动化修复方法可分为以下两大类方法，即基于搜索的方法（例如 GenProg、PAR 和 SPR）和基于语义的方法（例如 SemFix、Nopol 和 DirectFix）。基于搜索的修复方法（也称为生成与验证方法）在搜索空间内搜索以生成修复候选，并根据提供的测试组验证该修复候选。同时，基于语义的修复方法通过语义信息（通过符号执行和约束求解）合成修复。GenProg 作为一种突出的基于搜索的修复工具，被证明可以扩展到大型现实世界软件，如 php 和 wireshark。同时，SemFix 作为首个基于语义的修复工具，显示出比 GenProg 在修复能力（修复更多错误程序，成功率更高）和运行时间方面更高效，尽管 SemFix 仅应用于相对较小的程序。此后，在这两种方法中，高质量修复的重要性开始被考虑，从而催生了另一种基于搜索的修复工具 PAR 和基于语义的修复工具 DirectFix 。

当前，自动化程序修复研究考虑了三个属性——可扩展性（应能扩展到大型现实世界程序）、修复能力（应能修复大量缺陷，可能涵盖多种缺陷类别）以及修复质量（应生成对程序更改较少、删除功能较少且更可能被开发者接受的修复）。其中一些属性可能被认为具有一定的定性特征——尽管如此，在构建新的修复方法时考虑这些属性非常重要。例如，基于搜索的修复工具 SPR 生成的修复数量更多（与 GenProg 相比），并且在应用于大型现实世界软件时，生成的修复更常与开发者提供的修复在功能上等价（而不仅仅是通过提供的测试）。与此同时，对于基于语义的方法，低可扩展性一直是主要批评来源，尽管它在高修复能力（例如 SemFix ）和高修复质量（例如 通过对程序进行可证明的最小更改来修复错误程序）方面显示出令人瞩目的成果。

三、SemFix: Program Repair via Semantic Analysis

1.引言

SemFix 由 Nguyen 等人于 2013 年推出，是最早将语义分析应用于自动化程序修复的工具之一。与早期的语法方法（如 GenProg）不同，GenProg 依赖于修改现有代码片段，而 SemFix 旨在使用符号执行和程序合成生成新的修复表达式。其目标是使用测试组修复错误程序，无需形式化规范，解决了遗传编程方法在代码库中缺少正确表达式时的局限性。

2.概述

给定一个错误程序 P 和一个包含至少一个失败测试用例的测试组T，我们的程序修复技术如下工作。首先，我们使用统计故障定位生成一个按语句可疑程度排名的程序语句列表 L。我们的核心程序修复方法随后从最可疑的语句开始逐一扫描语句列表，直到生成成功的修复。对于每个扫描的语句s ，我们的核心程序修复方法尝试通过更改语句s 来修复程序。假设语句s 是失败的根本原因，我们的核心修复方法包括两个主要步骤：1) 首先生成成功修复 s 必须满足的修复约束；2) 尝试使用程序合成解决修复约束。

int is_upward_preferred(int inhibit, int up_sep, int down_sep) {int bias；if (inhibit)bias = down_sep; // 修复：bias = up_sep + 100elsebias = up_sep;if (bias > down_sep)return 1；elsereturn 0;
}

Tcas 代码片段

我们使用示例程序说明我们的技术。这是从 Tcas（空中交通防撞系统）中提取的代码片段。假设 inhibit 只有两个允许值 {0,1}。该程序的预期行为描述如下：is_upward_preferred = (inhibit * 100 + up_sep > down_sep)。用于检查程序正确性的测试集如表 I 所示。测试结果显示该实现有错误，有两个测试失败。为了修复该程序，我们首先使用给定的测试集对错误程序应用 Tarantula 故障定位 。基本上，它按语句的可疑程度以降序排列程序语句。Tarantula 的结果如表 II 所示，是按可疑程度排名的语句列表。由于第 4 行排名最高，我们开始调查是否可以通过更改第 4 行来修复程序。

假设我们想将第 4 行替换为 bias = f(...)，其中 f(...) 由我们的方法确定。第 4 行可访问的变量有四个：inhibit、up_oep、down_oep 和 bias。由于变量 bias 未初始化，我们假设 f(...) 不能使用它。现在假设函数 f 的签名如下：

int f(int inhibit, int up_sep, int down_sep)

然后，我们找到 f(...) 必须满足的约束，以通过测试集中的所有测试用例。这是通过符号执行实现的。

对于每个执行第 4 行的测试，我们生成一个关于 f(...) 的约束，其满足保证修复后的程序产生预期输出。我们使用表 I 中的第二个测试来解释如何生成这样的约束。图 2 显示了测试 2 的符号执行树，输入向量为 ⟨1,11,110⟩。注意，我们的符号执行不是从程序输入开始。相反，程序以输入 ⟨1,11,110⟩ 具体执行直到第 4 行。然后，变量 bias 的值被替换为符号值 X，并继续进行符号执行。在执行第 7 行的分支时，执行面临两个选择，两个路径都如符号执行树所示执行。由于我们知道输入 ⟨1,11,110⟩的预期返回值应为 1，只有通过第 8 行的路径才能使程序通过。要遵循此路径，路径条件 X>110 应满足。给定第 4 行的程序状态为 (inhibit = 1, up_sep = 11, down_sep = 110)，我们知道 f f 必须满足 f(1,11,110)>110。类似地，我们从测试 1 得到 f(1,0,100)≤100 ，从测试 4 得到 f(1,−20,60)>60。因此，f需要满足的约束是 f(1,11,110)>110∧f(1,0,100)≤100∧f(1,−20,60)>60。我们使用程序合成来解决关于f的约束，以获得具体函数。程序合成需要基本组件（例如常量、“+”、“-”）作为构建函数f的原料。在我们的技术中，这些组件是逐步提供给程序合成的。在第一次尝试中，仅允许使用常量。然而，没有常量函数可以满足上述约束。然后我们允许函数f使用一个 “+”，即f可以采用 var1+c或 var1+var2的形式，其中 var1 ​ 和 var2 ​来{inhibit,up_sep,down_sep}，c 是一个整数常量。合成过程可以找到一个解决方案 f(inhibit,up_sep,down_sep)=up_sep+100 ，这是对图 1 中程序的成功修复。注意，如果使用 “-” 而不是 “+”我们将得到f(inhibit,up_sep,down_sep)=up_sep−(-100) 作为修复。

3.主要贡献

1. SemFix 工具的开发：SemFix 集成了符号执行、约束求解和程序合成来生成修复，标志着向基于语义方法的转变。

2. 提高成功率和效率：评估显示，SemFix 修复的错误程序版本数量是 GenProg 的三倍，对于 GNU Coreutils 错误的平均修复时间为 3.8 分钟，而 GenProg 为 6 分钟。

3. 新表达式的合成：SemFix 可以创建原始代码中不存在的修复表达式，克服了语法方法的关键局限性。

4. 性能优化：它采用了诸如最初使用测试子集和按复杂性递增顺序探索修复的策略，以增强可扩展性。

4.方法

SemFix 的方法结合了三种关键技术：

1. 统计故障定位：使用 Tarantula 技术，SemFix 根据语句在失败与通过测试执行中的频率，排名程序语句包含错误的可能。

   统计故障定位 旨在通过利用错误语句执行与程序失败之间的相关性来定位程序失败的根本原因。根据语句在通过和失败执行中的出现频率，为每个程序语句计算可疑度分数。根据可疑度分数，向用户提供一个按排名排序的语句列表。用户可以从最可疑的语句开始检查排名列表，直到找到失败的根本原因。、

   在本文中，我们采用了 Tarantula技术的可疑度分数。对于语句 s，其可疑度分数 susp(s) 计算如下：(其中 failed(s)表示语句s出现在失败执行中的次数，passed(s) 表示语句s出现在通过执行中的次数。变量 totalfailed表示失败执行的总数，totalpassed表示通过执行的总数。)

   

2. 语句级规范推断：受天使调试（angelic debugging）启发，SemFix 使用符号执行推断错误语句的正确行为。它具体执行程序直到错误语句，然后符号化地用变量替换错误表达式，以推导确保所有测试通过的约束。

3. 程序合成：SemFix 采用基于组件的合成，从基本组件（如常量、算术运算符）构建修复，按复杂性组织。Z3 SMT 求解器和定制的 Perl 合成模块生成满足推导约束的表达式。

5.评估

SEMFIX 从一组测试中推导修复约束，并解决修复约束以生成有效修复。即使修复代码在程序中任何地方都不存在，SEMFIX 也能合成修复。实验结果表明，SEMFIX 能够修复各种类型的错误，并优于基于搜索的程序修复技术。SemFix 在软件工件基础设施存储库（SIR）程序（如 Tcas、Schedule）和带有真实错误的 GNU Coreutils 片段上进行了测试。它在各种错误类型上展示了有效性，包括常量、算术、比较、逻辑以及缺失/冗余代码错误。然而，它在大型程序上存在可扩展性问题，并且在多语句修复或复杂数据类型（如浮点变量）方面遇到了困难。

四、DirectFix: Looking for Simple Program Repairs

1.引言

基于 SemFix，DirectFix 由 Mechtaev 等人于 2015 年提出，专注于生成简单且对开发者友好的补丁。虽然 SemFix 生成了有效的修复，但其补丁有时复杂，降低了可用性。DirectFix 旨在通过整合故障定位和修复生成，创建最小的、可读的修复，确保修复与原始程序结构紧密相似。

2.示例

考虑图1(a)中的程序片段。该程序应在程序结束时，如果满足 x >= y，则返回0；否则返回1。然而，该程序的开发者犯了一个小错误，未考虑 x==y 的情况。这里，图1(b)和图1(c)展示了两种不同的有效修复。注意，前一种修复比后一种更复杂。大多数开发者会更倾向于第二种更简单的修复。据我们所知，现有的修复工具并未考虑修复的简单性。它们在找到一个修复后即停止搜索，无论该修复有多复杂。实际上，图1(b)中的修复类似于 GenProg 生成的修复。GenProg 通过将现有代码嫁接到有错误的程序上尝试修复。因此，GenProg 常常生成对人类开发者来说看似无意义的修复。

与此同时，较新的修复工具 SemFix 似乎比 GenProg 生成的修复更简单（尚未进行用户研究以完全验证这一点，但直观上如此，因为 SemFix [6] 在表达式级别进行修复，而 GenProg 在语句级别进行修复）。然而，SemFix 仍然经常生成比必要更复杂的修复。图2展示了一个这样的例子。给定图2(a)中的有错误程序——前两行被错误地交换，并且缺少等号（=）——SemFix 可以生成图2(b)所示的修复。与图2(c)所示的另一种修复相比，后者修复更简单，尽管它修改了程序的两行（SemFix 无法修改多行）。这两个例子还表明，一个有错误的程序可以通过多种方式修复，生成不同简单程度的修复。

谨慎选择修复还有一个重要原因：修复后程序的可靠性（即修复后的程序不仅解决了给定测试组中的错误，而且不会引入测试组外测试显示的新错误）因所选修复而异。考虑图3(a)中的有错误程序，它检查字符 c 是否包含在字符串（字符数组）s 中。图3(b)中的表格显示了预期的和实际的输入/输出关系。第一个测试失败，因为在查找与 c 相同的字符时，未扫描字符串 s 的所有字符。注意表格中变量 k 的值并非 s 的长度，而是比长度小1。如前所述，这个有错误的程序存在多种修复方式。图3(c)和图3(d)展示了两种可能的修复——这两种修复都通过了图3(b)中的所有测试。然而，第一个修复（图3(c)）看似危险。如果搜索的字符不是'?'或'!'怎么办？虽然通过选择合适的测试组可以减少修复的潜在危险，但什么是合适的测试组仍是一个尚未彻底解决的重要研究问题。

与此同时，第二个更简单的修复（图3(d)）保留了原始的正确行为，同时纠正了错误行为。这两个修复之间的对比提出了以下假设。这一假设的理由是，简单的修复更可能以更受限的方式修改程序行为。

假设：简单修复比复杂修复更不容易改变原始版本的正确行为。因此，简单修复可能更安全。

现有的测试驱动程序修复工具首先进行故障定位，并在故障定位阶段标记为可疑的程序位置周围搜索修复。因此，寻找最简单修复的直接方法是迭代地在每个可疑程序位置组合生成修复，并选择最简单的修复。然而，显然这种直接方法无法扩展，因为即使是寻找单个修复也常常需要大量时间。为了更高效地找到简单修复（而不明确枚举每个修复候选），我们将程序修复的两个阶段——(i)故障定位和(ii)修复搜索——整合为一个步骤。

3.背景

DirectFix 是一种基于语义的程序修复方法，利用了SMT求解器的最新进展。它将修复问题简化为最大满足问题。特别是，该方法构造了一个逻辑公式，其解决方案对应于修复。我们的编码基于组件合成，并扩展以生成语法上最小的更改并提高可扩展性。

A.预备知识

命题逻辑中的可满足性问题（SAT）是确定给定公式 φ 是否有模型的问题。最大满足性（MaxSAT）是SAT的泛化，其目标是找到满足给定公式最大子句数的模型。可满足性模理论（SMT）是关于给定背景理论的可满足性问题。MaxSMT是SMT上的MaxSAT泛化。部分最大满足性（pMaxSAT）对于一组软子句 s 和一组硬子句 h，是寻找最大子集 s_max 的问题，使得 s_max ∧ h 是可满足的。pMaxSMT是SMT上的pMaxSAT泛化。

DirectFix 利用文献中称为追踪公式的逻辑公式表达程序语义。

定义 1（追踪公式）

确定性程序 P 的追踪公式 TF 是满足以下性质的逻辑公式：给定程序 P 的输入 I，

其中 TF(I, O) 表示追踪公式 TF，其输入变量绑定为 I，输出变量绑定为 O。

B. 基于组件的合成

通过基于组件的合成（CBS）可以自动生成满足给定要求的表达式和程序。这里我们介绍原始的CBS技术，我们的扩展和优化将在第V节中给出。

定义 2
设 v 为变量，V 为变量集且 v ∉ V，F 为运算符集，O 为 {v} ∪ V 上的约束，称为 oracle。基于组件的合成 (v, V, F, O) 是寻找表达式 e 的问题，使得：

• e 使用组件子集 C = V ∪ F 和常量构造；
• O ∧ (v = e) 是可满足的。

该方法通过将称为组件的基本构建块相互连接来构造表达式。组件可以是常量、变量或运算符。组件之间的正确连接使用SMT求解器确定。具体来说，组件的语义、它们之间的连接语义以及 oracle 约束被用来构造一个SMT公式，我们称之为基于组件的编码（CBE）。

CBE 的思想是将表达式视为电路。每个组件有一组输入和一个输出。为了合成所需的表达式，求解器需要找到组件输入和输出之间的正确连接。为了捕获连接信息，为每个输入和输出定义一个称为位置变量的数值变量。位置的含义很简单：输入和输出具有相同位置时即相连。

CBE 定义了组件输入和输出的值与位置之间的关系。对于每个输入和输出，我们引入一个对应其值的变量。我们使用以下符号：对于组件 c，变量 对应其输出的值，变量是其第 k 个输入的值。我们将 c 的输入数量表示为 NI(c)。我们使用函数 L 表示位置变量。例如，组件 c 的第一个输入的位置变量是 L()。图 4 展示了位置变量分配的示例。表达式 x > y 的组件被分配在区间 [0, 3)。变量 x 的输出位置为 0，变量 y 的输出位置为 1，运算符 > 的输出位置为 2。运算符 > 的第一个输入链接到 x，第二个输入链接到 y。假设表达式的输出由变量 v 绑定，即 v = x > y。电路的输出由点标记，并由约束 L() = 2 表示。表达式 x > y 可以通过位置变量的赋值简单重建。我们假设有一个函数 从位置变量的赋值构建表达式。

CBE 包括三类约束：格式正确约束、语义约束和连接约束。格式正确约束 限制位置变量，使得任何满足这些变量的赋值对应于有效结构的表达式。这些约束包括范围约束，将所有组件的输入和输出分配在一个范围内；一致性约束，确保每个组件的输出具有唯一位置；以及无环约束，禁止循环连接。

语义约束 为每个组件定义，指定组件的输入和输出之间的关系。例如，对应于加法运算的组件 c 的语义约束定义为。对应于变量 x 的组件 c 的语义约束定义为。类似地，对应于常量 a 的组件 c 的语义约束定义为。

连接约束 通过组件的语义及其之间的连接捕获要合成的表达式的语义。

定理 1
设 v 为变量，V 为变量集且 v ∉ V，F 为整数运算符集，O 为基于的约束。CBE 的公式 是基于组件的编码，即 以 v, C = V ∪ F 和 φ 的任何模型作为位置变量的赋值，生成基于组件的合成问题 (v, V, F, O) 的解决方案。

描述的 CBE 仅适用于表示对应于单一测试用例的 oracle。如果我们将不同测试用例的输入-输出约束相连，公式显然是不可满足的。为了将此编码扩展到多个测试用例，我们重命名编码公式中的变量，使得每个测试用例使用唯一的变量名。然后，捕获所有给定输入-输出关系的公式是每个测试用例的重命名公式的合取。        

4.概述

为了找到修复，我们首先将给定的错误程序翻译为追踪公式。例如，图 5(b) 展示了函数 foo（图 5(a)）的追踪公式。该函数有错误，其测试 test_foo 失败（为简单起见，此示例使用单个测试）。给定的测试被翻译为以下 oracle 约束：

合取公式 是不可满足的，这反映了测试失败的事实。

我们的目标是确定中哪些表达式需要修改以及如何修改，以便修改后的公式使得 可满足。在我们的示例中，真实修复如下：

本质上，我们的修复方法将程序视为一个电路。为了生成修复，它会切断一些现有连接，并添加新的组件和连接。为了获得最简单（破坏性最小）的修复，我们希望尽可能少地切断连接。我们通过将程序修复问题简化为最大满足性（MaxSAT）问题的一个实例来实现这一点——更具体地说，是部分最大满足模理论（pMaxSMT）问题。

为了基于部分最大满足模理论（pMaxSMT）生成修复，我们构造了一个称为修复条件的公式。给定追踪公式 ，修复条件定义如下：

上述公式 在语义上与 等价。唯一的区别在于，我们用新的变量 替换了中的右值表达式，同时在 函数中保留了每个 与其代表的表达式之间的等价关系（例如，v1 = x1 > y1）。该函数将其参数表达式组件化为电路形式，遵循基于组件合成的思想。

为了获得最简单（破坏性最小）的修复，我们使用了部分最大满足模理论（pMaxSMT）求解器。在 pMaxSMT 中，公式被分为硬子句（必须满足的子句）和软子句（不必满足的子句）。在硬子句中，我们包含表达组件语义和 oracle 数据的子句。同时，通过软子句，我们约束程序表达式的结构。例如，我们为表达式 x>y 构造了结构约束，如下所示，这基本上等价于图4中的电路图：

在上述约束中，我们将表达式的输出与一个新的变量 v 绑定，即 v = x > y。如所示，该约束指定了表达式组件之间的连接以及其输出绑定。在将 分成如上所述的硬子句和软子句后，我们将 输入到 pMaxSMT 求解器中。然后，求解器会移除一些结构约束（如果需要），并返回一个对应于修复的模型。

图6展示了求解器如何通过使用额外的组件 ≥ 修改表达式 x > y 以修复程序。具体来说，它移除了 > 的输出与 v 的输入之间的一个连接，对应于结构约束，并添加了三个新连接：(i) x 的输出与 ≥ 的第一个输入之间的连接，(ii) y 的输出与 ≥ 的第二个输入之间的连接，以及 (iii) ≥ 的输出与绑定变量 v 之间的连接。这些新连接通过使用修复条件的模型（即位置变量的值）获得。

我们注意到，通过寻找一个最大化满足子句数量的模型，我们有效地同时切断和添加连接。换句话说，我们同时进行故障定位和修复生成。

5.主要贡献

1. 整合故障定位与修复：DirectFix 将这两个步骤合并为单一过程，提高效率并确保始终考虑简单性。

2. 用于最小修复的部分最大满足（MaxSAT）：它使用部分最大满足（MaxSAT）结合 SMT 求解，生成尽可能简单的修复，保留原始代码结构。

3. 增强修复质量：与 SemFix 相比，DirectFix 生成了更简单的修复，回归错误更少，56% 的修复与真实情况等同，89% 修改了相同的程序位置。

4. 实证验证：在 98 个错误 SIR 程序和 9 个 GNU Coreutils 错误上进行评估，DirectFix 实现了平均 AST 差异为 2.26，表明变化最小。

6.方法

DirectFix 采用基于测试驱动的方法，使用测试组指导修复。其方法包括：

1. 基于语义的修复：错误程序被翻译成逻辑“跟踪公式”，捕捉其在给定输入和输出的行为，使用 VCC 和 Boogie 等工具。

2. 部分 MaxSMT 公式化：修复问题被建模为部分 MaxSMT 问题，硬约束确保符合测试组，软约束最小化对原始代码的更改。

3. 基于组件的合成：使用组件（如变量、运算符）像电路一样连接进行修复合成，Z3 SMT 求解器确定有效排列。

4. 优化：组件共享和分隔符变量等技术防止无效连接，增强可扩展性。

7.评估

DirectFix 在 98 个错误 SIR 程序版本和 9 个真实 GNU Coreutils 错误上进行了评估。它在简单性和安全性方面优于 SemFix，生成的修复具有更少的意外副作用。其整合故障定位和修复生成减少了枚举所有可能修复的需要，提高了效率。

五、Angelix: Scalable Multiline Program Patch Synthesis via Symbolic Analysis

1.引言

由 Mechtaev 等人于 2016 年提出，Angelix 解决了 SemFix 和 DirectFix 的可扩展性局限性，特别是在大型软件和多位置错误方面。早期工具专注于单语句修复，而 Angelix 旨在处理高达 2814 KLoC 的程序中的复杂、相互依赖的错误，例如 Wireshark 和 PHP，包括 Heartbleed 漏洞。

2.示例

图1展示了为修复coreutils漏洞13627所做的代码更改。在有漏洞的版本中，调用xzalloc（第4行）分配内存块会导致段错误。修复方法包括在调用xzalloc之前添加一个if条件语句（第5行）。只有当变量max_range_endpoint具有非零值时，修复后的版本才会调用xzalloc。此外，修复还需要移除现有的if语句（第1-2行）。如果不移除该if语句，max_range_endpoint会被eol_range_start的非零值覆盖（第2行），从而导致新的if条件语句“if (max_range_endpoint)”无法成功阻止有问题的xzalloc调用。

这个简单的示例展示了修复多个错误位置的多行修复的复杂性。关键难点在于，一个位置的更改可能会影响后续程序执行的修复。更概念化地说，给定有漏洞程序的修复空间会随着每个错误位置的程序更改而不断变化。当前最先进的基于搜索的修复算法，如SPR（也称为生成-验证方法），仅限于修复单一位置。目前尚不清楚如何扩展基于搜索的修复算法以修复如图1a所示的多个位置的错误，同时保持其效率。与此同时，在基于语义的修复方法中，如SemFix 和DirectFix ，DirectFix已支持多位置修复。本质上，DirectFix保留了程序的所有语义信息（以逻辑公式形式），这使得跟踪修复空间的变化成为可能。因此，SemFix更具可扩展性，适用于单行修复，而DirectFix虽然可扩展性较低，但能生成多行修复。

在本文中，我们讨论了基于语义的修复如何在保持修复多位置能力的同时实现可扩展性。图1b-1d高层次展示了我们的修复算法如何从示例中生成修复。图1d中显示的生成修复在功能上等同于开发者提供的修复，尽管存在表面上的差异。修复的第一部分，“if (0)”（第1行），使第2行的语句被跳过，这在功能上等同于移除相应的语句。修复的第二部分，“if (!(max_range_endpoint == 0))”，在功能上也等同于开发者提供的修复，即“if (max_range_endpoint)”。这里的表面差异仅源于我们当前使用的基于组件的合成算法实现。

我们的修复算法从将原始有漏洞程序转换为功能等价的程序开始，如图所示。

图1b展示了我们在每个未受保护的赋值语句前添加一个if条件语句“if (1)”的过程（这是我们当前使用的启发式方法）。随后，我们的修复算法将用户配置的n个最可疑的表达式（基于统计错误定位的结果选择）替换为符号变量，如图1c所示，其中条件表达式和赋值的右侧被替换为符号变量。修复算法的用户可以配置可符号化的可疑表达式的数量和类型，这些表达式包括条件表达式、赋值的右侧以及函数参数。我们的修复算法继续对图1c中的程序执行符号执行，使用提供的测试用例收集修复给定有漏洞程序所需的语义信息。利用提取的语义信息，我们合成了修复表达式。为了合成修复，我们使用了基于MaxSMT的组件化补丁合成算法，如我们之前的工作所述。这导致生成的修复与原始程序非常接近，因为原始有漏洞表达式的结构被最大程度地保留。由此生成的小型补丁可以带来多种好处，例如提高补丁的可维护性（简单补丁比复杂补丁更容易理解）和降低回归风险（简单补丁相比复杂补丁更不容易改变正确行为）。

3.预备知识

3.1简洁的修复语义签名

为了合成修复补丁，我们的修复算法收集以下程序语义信息：

1. 测试通过路径：首先，我们需要确定每个测试是否存在一条程序路径，使测试通过。修复算法通过受控符号执行检测此类路径——“受控”指的是通过安装符号变量（例如示例中的α、β和γ）控制探索的执行路径。在图1c的程序示例中，符号执行在第1行（if (α)）和第4行（if (γ)）的if条件语句处探索不同路径。如果未检测到测试通过路径，我们将用户配置的下一个n个可疑表达式设为符号变量，并重复该过程以寻找测试通过路径。

2. 天使值(angelic values)：如果检测到通过已安装符号的测试通过路径π，则意味着存在使测试通过的每个符号的具体值。作为第二部分语义信息，我们使用约束求解器推断这些值（称为天使值）。

3. 天使状态(angelic state))：最后，我们需要知道测试通过路径中每个已安装符号处的程序状态（称为天使状态）。例如，为了在图1d的第4行合成修复表达式 !(max_range_endpoint == 0)，需要知道变量max_range_endpoint的值。我们的修复算法收集每个符号安装位置处可见程序变量的值，这些变量在合成修复表达式时用作合成成分。

以下展示了当提供两个测试（t1和t2）时，我们示例的语义签名。

前述语义签名——我们称之为“天使森林”（如定义3所述）——简洁地捕捉了合成修复所需的三部分语义信息：

1. 测试通过路径：首先，天使森林编码了使测试t1通过的两个执行路径（π1和π2），表示为t1 : {π1, π2}。类似地，测试t2也可以通过两条执行路径π3和π4。注意，图1d中建议的修复在测试t1中遵循路径π1，在t2中遵循路径π3。

2. 符号的具体值：其次，每个符号的具体值在每个测试通过路径中被标注。例如，在路径π1中，符号α和γ的值应为False，表示为。符号β的具体值未出现，因为在路径π1中未执行图1c中的语句max_range_endpoint = β。而在路径π2中，所有三个符号的值均出现，表示为。

3. 天使状态：最后，天使状态σi提供用于修复合成的变量值信息。同一变量在不同路径上可能具有不同值，因此每个符号实例与自己的天使状态相关联。在我们的coreutils示例中，σ2(max_range_endpoint)为零，因此建议的修复表达式!(max_range_endpoint == 0)返回γ的具体值False，如路径π1中指定。

3.2可扩展性的原因

我们的修复方法能够处理像Wireshark（2814千行代码）这样的大型程序，并生成多位置修复。以下是我们的修复方法具有可扩展性的几个原因：

1. 轻量级语义签名：我们使用轻量级语义签名进行程序合成。与DirectFix 同样支持多位置修复）使用的语义签名相比，我们的语义签名更为简洁。DirectFix的语义签名本质上是整个程序的语义，维护程序中每个表达式的关系，因此随着程序规模的增加，其语义签名变得更冗长和复杂。需要注意的是，语义签名是修复合成的规范，合成的修复必须遵循提供的语义签名，如我们的示例所示。我们的轻量级语义签名减轻了修复合成器的负担，从而提高了修复合成的效率。

2. 受控符号执行：我们的修复算法使用受控符号执行，仅针对选定的少量可疑表达式，而不是通常的符号输入。通过这种受控符号执行，我们仅探索涉及这些可疑表达式的有限可行执行路径。此外，我们最初仅对测试组的一个子集执行符号执行，以减少运行时间。只有当某些剩余测试在合成的修复下失败时，我们才会对这些失败测试进行额外的符号执行。

3. 基于天使森林的修复合成：我们的修复算法仅在存在天使森林（修复的语义签名）时才启动修复合成。如果选定的n个可疑位置没有天使森林，则表明无法通过更改这些位置修复错误。符号执行通过仅探索可行执行路径，高效地找到天使森林（或证明其不存在）。如果没有天使森林，我们的修复算法不会浪费资源去尝试合成修复。

我们注意到，上述每项技术都是对我们和其他人先前工作的改进或扩展。如前所述，我们新颖的、与程序规模无关的轻量级语义签名是对之前工作DirectFix 中使用的重量级语义签名的改进。我们还提到，受控符号执行首次在我们的先前工作SemFix 中引入，尽管当时仅在一个位置安装符号，因此无法实现多位置修复。此外，我们忽略修复不可行的可疑位置的修复策略与Nopol 和SPR 有相似之处。但Nopol和SPR目前无法修复多位置错误。此外，由于Nopol和SPR的语义签名较弱，无法捕捉多个程序位置之间的依赖关系，多位置修复对它们来说在根本上具有挑战性。我们新颖的语义签名与现有技术的独特组合实现了可扩展的多位置错误修复。

4.背景

我们使用部分最大可满足性模理论（Partial MaxSMT）的技术和工具来实现修复算法。部分MaxSMT针对两组子句（软子句和硬子句）的问题，旨在找到一个变量赋值，使所有硬子句得到满足，并尽可能满足最多数量的软子句。

为了合成补丁，我们采用了基于组件的修复合成算法（CBRS），这是基于组件的程序合成在程序修复中的推广。在CBRS中，一个组件可以是变量、常量或在给定背景理论中定义的基于组件和操作的项；例如，1、x、(∗1 + ∗2) 和 (if ∗1 then ∗2 else ∗3)，其中∗i表示组件的输入。一个表达式通过连接多个组件形成。例如，图2显示表达式x > y由以下三个组件连接形成：(∗1 > ∗2)、x 和 y。每个组件c有一个输出和一个或多个输入。我们用NI(c)表示组件c的输入数量。为了表示组件之间的连接，组件的输入和输出与称为位置变量的独特变量相关联。例如，输入与其位置变量相关联，输出与相关联。只有当一个组件的位置变量与另一个组件的位置变量具有相同值时，这两个组件才被认为是有连接的。

为了确保合成的表达式是格式正确的，CBRS施加了一个格式正确约束，其中C表示所有可用组件的集合：

在此，范围约束确保所有组件的输入和输出在合法范围内，一致性约束保证每个组件的输出具有唯一的位置，循环约束禁止循环连接。CBRS还为每个组件施加语义约束，以及连接约束，用于将位置变量与其对应的组件连接起来。连接约束定义如下：

最后，结构约束捕捉原始有漏洞程序的结构。例如，对于表达式 x + y，结构约束定义为：

为了使用CBRS为有漏洞程序合成补丁，结构约束作为软约束传递给部分MaxSMT求解器，其余约束作为硬约束传递。然后，求解器找到一个满足合成规范且在语法上与原始有漏洞程序最接近的新程序。

5.关键技术

我们的修复方法包括以下四个步骤：(1) 程序转换，(2) 错误定位，(3) 提取修复约束，(4) 补丁合成。

1. 程序转换：在第一步，我们执行保留语义的程序转换，以扩展修复算法能够处理的缺陷类别。例如，我们在第2节中展示了在每个未受保护的语句前添加“if (1)”。我们的修复框架对添加更多保留语义的程序转换方案是透明的。

2. 错误定位：在第二步，我们执行统计错误定位。我们使用Jaccard公式 ，被认为是最有效的自动程序修复方法。由于我们的修复算法修改的是有漏洞的表达式，我们在表达式级别而非语句级别应用Jaccard公式。

3. 提取修复约束：最后两步将基于语义的修复方法与基于搜索的修复方法（如GenProg和SPR）区分开来。基于语义的方法通常通过符号执行从待修复程序中提取修复约束。这一修复约束作为指导程序合成的规范，从而可以合成满足修复约束的补丁。

4. 补丁合成：我们修复方法的关键创新在于我们提出了一种新的轻量级修复约束，我们称之为“天使森林”（angelic forest）。天使森林的大小与待修复程序的规模无关，这是我们修复方法具有可扩展性的主要原因。尽管天使森林简单，但它包含足够的语义信息以支持多位置错误修复。以下，我们基于天使值（定义1）和天使路径（定义2）正式定义天使森林（定义3）。

定义1（天使值 ）：设P为程序，t为失败的测试用例，e为程序表达式，为其在t的执行跟踪中的第k次出现。天使值α是指在t的执行跟踪中将表达式替换为α，使程序P通过测试t。

定义2（天使路径）：设E为程序P的一组程序表达式，t为P的测试用例。天使路径π(t, E)是一组三元组(, v, σ)，其中是测试t的执行跟踪中出现的表达式e ∈ E的第k个实例，v是的天使值，σ : Variables → Values表示位置的天使状态，是位置处可见变量到其值的映射。对于天使路径π(t, E)中的三元组(, v, σ)，满足以下性质：将天使路径中的所有替换为其对应的天使值v，使得(1) 程序P通过测试t，(2) e_k位置的可见变量x具有值σ(x)。

定义3（天使森林）：设E为程序P的一组程序表达式，t为P的测试用例。测试t的天使森林是天使路径的集合。

A.天使森林提取

我们通过受控的自定义符号执行提取天使森林——“受控”指的是，我们不是以符号输入启动符号执行，而是在基于统计错误定位结果选择的少量可疑程序位置安装符号，以控制符号执行期间探索的执行路径。算法1展示了如何提取天使森林。通过执行受控符号执行，生成一对路径条件pc和程序的实际输出（第3行）。给定测试中可用的预期输出，我们通过约束求解器找到的模型（即第6行的模型M）。该模型用于提取天使路径，并随后扩展天使森林（第7行）。回顾一下，天使森林是一组天使路径的集合，每个天使路径是一组三元组，包含可疑表达式的实例、其天使值（应返回以通过测试的值）以及处天使状态σ，即位置处可见变量到其值的映射。

由于传统符号执行既不能为选定的可疑表达式安装符号，也不能维护可疑表达式的天使状态，我们扩展了传统符号执行，如算法2所述。在我们的自定义符号执行中，通过将每个可疑表达式实例的值替换为新符号来安装符号（第7行）。如果给定的不是可疑表达式，我们的自定义符号执行以与传统符号执行相同的方式评估（第10行）。此外，我们通过增强路径条件来维护可疑表达式的天使状态（第4行）。对于（可疑表达式e的第k个实例）位置的每个可见变量x，我们用扩展路径条件，其中表示上下文中的变量x，表示符号执行期间评估的x的具体/符号值。通过约束求解器解决增强后的路径条件，生成天使森林。我们在KLEE 之上实现了自定义符号执行。

B.补丁合成

一旦获得天使森林，我们将其作为合成规范输入到修复合成器中。具体来说，合成的修复在执行时会为每个测试遵循一条天使路径，从而使所有测试通过。在这些天使路径中，每个修复的表达式返回其对应天使路径中指定的天使值。

我们的修复合成器是基于组件的修复合成（CBRS）的实现。CBRS将程序视为由变量和操作符等基本组件构成的电路。例如，图2的电路图展示了程序表达式x > y的电路，盒子和线分别表示组件和连接。CBRS的目标是给定原始有漏洞程序、组件以及待合成程序的规范，搜索满足以下条件的组件间连接：(1) 满足给定的规范；(2) 与原始有漏洞程序的连接差异最小。例如，考虑有漏洞的表达式x ≥ y，图2的表格显示了该表达式的预期规范，CBRS将变量x和y与组件‘≥’的连接修改为与组件‘>’的连接，因为x > y满足给定规范。

CBRS的规范以算法1提取的天使森林形式提供。表1展示了一个天使森林的示例。为简单起见，此示例仅考虑一个可疑表达式e（扩展到多个表达式是直接的）。表格的前两列分别显示路径ID和e的实例ID。在该示例中，路径1执行表达式e两次（即k为1或2），而路径2仅执行e一次。天使森林包括两个可见程序变量x和y，作为可疑位置的程序状态。这些变量的值显示在和列中。表示（e的第k个实例）上下文中的变量x。最后一列“Angelic”显示的天使值。

CBRS使用约束求解器搜索组件间的连接。对于示例天使森林，我们生成以下约束：

对于天使森林（每个天使路径是一组三元组(, v, σ)），我们生成以下约束：

其中，v是的天使值，dom(σ)表示σ的定义域，即位置处可见变量到其值的映射。

可能存在多个满足给定修复约束的补丁。在这种情况下，CBRS使用MaxSMT求解器找到需要最少更改的补丁。最大程度保留原始源代码的能力有两个重要原因：

1. 开发者偏好：我们假设开发者更倾向于最小补丁。最小补丁更容易验证，且与更复杂的补丁相比，它们更不容易改变原始程序的正确行为。

2. 错误定位与修复：在为多个可疑表达式合成修复时，基于MaxSMT的修复同时作为错误定位，即修复算法同时确定哪些表达式需要修改以及如何修改。如果没有这一特性，合成器将始终修改所有可疑表达式，导致多位置修复由于补丁复杂性而不切实际。

这种合成方式提供的修复质量高于SPR。

6.优化

为了控制符号执行的会话数量，我们采用以下迭代方法：

1. 初始测试子集：从提供可疑位置最高覆盖率的测试组小子集开始。

2. 天使森林推断与补丁合成：为该子集推断天使森林并合成补丁。

3. 回归测试：如果生成的补丁在整个测试组中引发回归，则将反例测试添加到测试子集中。

4. 迭代重复：重复上述步骤，直到所有测试用例通过。

运行时间优势：与基于搜索的方法（如GenProg和SPR）相比，基于语义的方法具有显著优势。基于搜索的方法由于修复尝试次数多，需要频繁重建和重新测试待修复软件。而我们的基于语义的方法通常在一次或少量尝试中找到修复，重建和重新测试的成本显著降低。

类型优化：在C语言中，由于类型强制转换和缺乏独立的布尔类型，区分程序表达式的类型较为困难。然而，精确的类型信息可以提高合成正确修复的概率并改善合成性能。为此，我们分析可疑表达式和可见变量的使用情况，收集类型约束。然后，利用这些类型约束推断程序表达式和变量的更精确类型。例如，我们为用作if条件的表达式分配布尔类型。

7.主要贡献

1. 大型程序的可扩展性：Angelix 与基于搜索的工具（如 GenProg 和 SPR）在可扩展性上相当，有效处理大型现实世界软件。

2. 多位置错误修复：它可以修复多个依赖的错误位置，这是许多早期工具缺乏的能力。

3. 高质量修复：Angelix 生成的修复通常在功能上等同于开发者补丁，减少了删除功能的“看似合理”修复。

4. 天使森林约束：一种新颖的轻量级修复约束“天使森林”，实现高效的多行补丁合成，不随程序大小扩展。

8.方法

Angelix 的方法包括：

1. 语义保留变换：它应用变换（例如，在未受保护的语句前添加“if (1)”），扩展可修复缺陷的范围，同时保留语义。

2. 统计故障定位：使用 Jaccard 公式。

3. 约束的符号执行：受控符号执行提取“天使森林”，一个轻量级的语义签名，指导合成，不随程序大小扩展。

4. 高效合成：仅在存在天使森林时启动合成，避免不必要的计算。

9.评估

在 GenProg ICSE2012 基准和 CoREBench 上测试，Angelix 修复了 32 个缺陷中的 28 个，其中 10 个在功能上等同于开发者修复。在 Wireshark 和 PHP 等程序上的实验，运行在 Intel Xeon E5-2660 CPU 上，设置 12 小时超时，显示平均修复时间为 32 分钟，展示了可扩展性。

六、比较与对比

方面	SemFix (2013)	DirectFix (2015)	Angelix (2016)
焦点	单语句语义修复	简单、开发者友好的修复	可扩展、多位置修复
故障定位	统计（Tarantula）	与修复生成整合	统计（Jaccard，表达式级别）
修复技术	符号执行，基于组件的合成	部分 MaxSMT，基于组件的合成	天使森林，受控符号执行
可扩展性	受大型程序限制	有所改善但仍有限	处理高达 2814 KLoC
错误类型	单语句错误	单语句错误	多位置、相互依赖错误
修复质量	有效但复杂补丁	更简单，回归错误更少	通常等同于开发者补丁
评估	SIR，GNU Coreutils	SIR，GNU Coreutils	GenProg 基准，CoREBench

共同点：所有三种工具都使用语义分析和程序合成，依赖测试组指导修复。它们利用 Z3 等 SMT 求解器，生成正确的修复。

差异与演变

1. SemFix奠定了基于语义的修复基础，引入了符号执行和合成，但局限于单语句修复，面临可扩展性问题。Semfix 的方法基于符号执行，具体过程为：首先用实际输入具体执行程序，直到到达疑似错误的语句；然后，将该语句的输出视为符号变量，从此处开始符号执行，探索不同程序路径。这种方法使用 KLEE 符号执行引擎，探索与潜在缺陷直接相关的变量路径条件和符号输出，形成修复约束。Semfix 的符号执行是全面的，不限制路径探索，适合处理复杂程序。Semfix 使用基于组件的程序合成，通过符号执行生成修复约束后，构建表达式。组件包括常量、算术运算符（如 +、-）和比较运算符，按复杂性分层。合成过程从简单组件（如常量）开始，逐步增加复杂性（如逻辑运算符），使用 SMT 求解器解决约束。最终输出是替换错误语句的表达式，确保程序通过所有测试。

2. DirectFix改进了 SemFix，优先考虑简单性，整合故障定位和修复，使用部分 MaxSAT 最小化更改，但仍局限于单语句修复。Directfix 也使用基于组件的程序合成，但结合部分 MaxSAT 求解，专注于最小化程序结构变化。首先将程序翻译为逻辑公式，捕获程序语义。然后将修复问题转化为部分 MaxSMT 问题，硬约束必须满足，软约束优先满足以减少变化。使用 SMT 求解器找到模型，生成修复表达式，确保最小 AST 节点差异。Directfix 通过故障定位和修复生成一体化步骤，产生简单修复

3. Angelix解决了可扩展性和多位置错误问题，引入天使森林以实现大型程序的高效合成，标志着重大进步。Angelix 引入“控制符号执行”，更注重效率。它仅选择几个通过故障定位识别的可疑表达式，探索有限的可行执行路径。初始阶段仅使用测试组的子集进行符号执行，以减少运行时间；如果合成的修复未能通过剩余测试，则进行额外符号执行。Angelix 的“天使森林”修复约束通过这种轻量级符号执行提取，独立于程序大小，增强了可扩展性。这种方法特别适合处理大规模程序，如 wireshark 和 php。Angelix 的程序生成以“天使森林”为指导，这种轻量级修复约束通过控制符号执行提取。合成修复为无副作用/函数调用的表达式，包括布尔、算术、关系运算符，可用变量和常量，支持多位置修复。合成过程高效，因“天使森林”独立于程序大小，减少了合成器的负担。

4. Semfix 和 Angelix 都使用符号执行，但它们的实现有显著差异。Semfix 从错误语句开始，采用全面的符号执行，探索所有可能的程序路径，以生成修复约束。相比之下，Angelix 使用“控制符号执行”，仅关注几个可疑表达式，并限制路径探索，以提高效率。这种方法使 Angelix 更适合处理大规模程序。

七、结论

SemFix、DirectFix 和 Angelix代表了自动化程序修复领域的进步，同时我们可以看到符号执行在其中发挥的重要作用。SemFix 开创了基于语义的技术，DirectFix 增强了修复的简单性和质量，Angelix 实现了可扩展性和多位置修复能力。它们共同展示了自动化修复转变软件开发的潜力，尽管处理复杂数据类型和确保全面测试组的挑战依然存在。

八、BibTex

@article{baldoni2018survey,title={A survey of symbolic execution techniques},author={Baldoni, Roberto and Coppa, Emilio and D’elia, Daniele Cono and Demetrescu, Camil and Finocchi, Irene},journal={ACM Computing Surveys (CSUR)},volume={51},number={3},pages={1--39},year={2018},publisher={ACM New York, NY, USA}
}

@inproceedings{nguyen2013semfix,title={Semfix: Program repair via semantic analysis},author={Nguyen, Hoang Duong Thien and Qi, Dawei and Roychoudhury, Abhik and Chandra, Satish},booktitle={2013 35th International Conference on Software Engineering (ICSE)},pages={772--781},year={2013},organization={IEEE}
}

@inproceedings{mechtaev2015directfix,title={Directfix: Looking for simple program repairs},author={Mechtaev, Sergey and Yi, Jooyong and Roychoudhury, Abhik},booktitle={2015 IEEE/ACM 37th IEEE International Conference on Software Engineering},volume={1},pages={448--458},year={2015},organization={IEEE}
}

@inproceedings{mechtaev2016angelix,title={Angelix: Scalable multiline program patch synthesis via symbolic analysis},author={Mechtaev, Sergey and Yi, Jooyong and Roychoudhury, Abhik},booktitle={Proceedings of the 38th international conference on software engineering},pages={691--701},year={2016}
}