Ⅰ Invariant-based Program Repair
- 引用:Al-Bataineh O I. Invariant-based Program Repair[J]. arXiv preprint arXiv:2312.16652, 2023.
0 摘要
-
本论文描述了一种 基于程序中ivariants概念的正式通用的自动化程序修复框架。
-
在上述框架中,动态分析缺陷程序的运行踪迹,推断出特征
和 ,其中 表示可能不变量(良好模式)的集合,这些不变量是运行成功所需的,而 表示可能可疑不变量(错误模式),导致瑕疵程序中的错误。 -
随后,利用严格的程序分析技术来对这些规范进行精炼,这些技术还可以引导修复过程生成可用补丁,随后评估这些补丁的正确性
-
通过开发一种基于invariants的高效修复bug的修复系统,我们展示了使用invariants在APR中的实用性
-
初步分析证明,基于不变量的APR在处理bug的性能方面是有效的,能够生成 确保程序效率提升且不对其功能产生不利影响的补丁
-
KeyWord:
- Automated program repair
- Invariant learning and refinement
- Patch overfitting
- Program verifier
- CPAChecker
- Performance bug
1 介绍
- Automated program repair (APR) 最近引起了很大的关注,其通过自动生成 瑕疵程序的补丁来显著减少手动调试工作。 现代化的修复工具已经被证明在修复许多实际程序中的错误方面是有效的.然而自动生成的补丁质量不佳[11],仍然是软件从业者采用自动化程序修复的主要障碍
问题
当前APR工具自动生成的补丁质量较低的主要原因是缺乏预期行为的规范。大多数程序修复系统依赖于测试行为作为正确性标准,因为软件开发者没有明确提供正式规范。因此,当前的APR方法产生的补丁可能是合理的,但仍然在部署前进行手动检查。因此,目前无法保证生成的补丁通常是正确的,并且不会引入新的错误。
解决方法
- 程序验证技术使开发人员能够在部署之前证明程序的正确性。
- 支持这项技术的关键之一是推断程序invarant,一个作为程序的抽象规范的逻辑表示。开发人员可以通过程序不变量显著受益,以确定修改代码必须要保留的程序属性。
- 不幸的是,这些invariants通常在代码中确实,导致了不严格的APR方法(如动态APR)占据主导地位;以及众所周知的补丁过拟合问题
- 我们认为,通过使用测试用例和基于可达性的分析技术,可以获得准确的invarants集合,用于生成高质量的补丁,即 CPAChecker
[3] and PathFinder [15]之类的程序验证工具可用于优化生成invariants的过程- 首先,我们使用测试用例来分析程序的运行轨迹推断invariant集合,随后,使用程序验证器对这些候选就行优化以获得更准确的invariants。目标是推断出两个规范
表示成功运行需要的良好模式集合 表示导致目标错误的不良模式集合
- 首先,我们使用测试用例来分析程序的运行轨迹推断invariant集合,随后,使用程序验证器对这些候选就行优化以获得更准确的invariants。目标是推断出两个规范
- 基于invariant的APR提供了两个关键优点
-
- 将APR导向潜在可行的补丁
-
- 使得可以使用程序验证器对合理的补丁惊醒正式验证
-
Viability of Invariant-based APR 可行性分析
- 程序invariant在多个应用中展现了效率,如程序理解,错误定位和形式验证。
- invariant之所以高效,是因为功能正确性与程序的最终结构相关,而不是特定的实现。 因此,他们可以帮助抽象出许多具体的执行步骤,从而极大的减少了理解补丁正确性所需的工作量。
- 事实上,那些尝试修复一个没有形式规范的错误没有文档的程序(即未经过深思编写的程序)的开发人员可以发现,基于不变量的APR对他们的修复工作很有帮助。
- 成熟的自动不变量检测工具如Daikon[4]和实用的软件验证工具如CPAChecker和PathFinder的可用性使基于不变量的程序修复技术成为可能。
- 乍一看,使用软件验证工具来优化不变量似乎成本太高,然而由于软件验证的巨大进步[2],实际上,基于invariant的验证变得非常高效。
- 特别是,软件分析框架CPAChecker,支持多种可达性分析,已经被有效地用于验证多达50k行的C程序的各种可达性查询。这使得可达性分析成为一种有前途的技术,可以用来显著减少补丁的过拟合问题并产生高质量补丁
2 基于invariant的APR框架
- 本节将使用程序invariant的概念重新阐释APR问题。
- 然后,我们描述了如何分析无故障运行的执行跟踪,推断出程序预期行为的可能规范,以及分析有故障运行的执行跟踪,推断出可能导致故障行为的可疑不变量。再进一步进行前,然我们介绍一些定义
Definition 1 (fault-free vs fault runs)
- 令
为一个bug程序, 是 的运行集合, 是程序P的预期行为属性。 我们定义一个运行 是一个成功的运行(i.e. fault-free run)当 ,否则, 是一个失败的运行(i.e. fault run),当
根据定义1我们可以注意到,通过分析从无故障运行中提取的信息,可以推断出程序预期行为的行为规范。 类似的,通过分析故障运行中的执行信息,可以推断出导致错误的错误invariant。 这是因为无故障运行表示保持程序invariant的运行,而有故障的运行表示违反某些程序invariant的运行。
Definition 2 (Invariant-based APR problem)
-
令
为一个包含bug 的程序 并且 为一个测试套件, 表示通过的测试而 表示失败的测试。 令 表示动态invariant推断工具如Daikon, 表示程序验证工具如CPAChcker,基于invariant的APR过程包含以下步骤: -
- Invariant 提取:使用
生成程序 的初始invariant集合
- Invariant 提取:使用
-
- Invariant 精炼:使用
精炼集合 产生规范 和 。 这可以通过在程序感兴趣的位置断言不变量,并使用任何生成的反例来对其进行精炼来完成。
- Invariant 精炼:使用
-
- 错误定位:通过分析
和 ,计算可能产生有效补丁的可疑语句列表
- 错误定位:通过分析
-
- 补丁生成:构造代码,纠正错误的不变量,同时保持程序其它的不变量,通过使用类似搜索或基于语义的补丁生成过程来执行
-
- 补丁验证:使用
验证生成的补丁的正确性
- 补丁验证:使用
-
-
根据正在修复的bug类型和分析程序的结构,不同的程序位置可能与属性
和 相关联。 示例包括不同函数的前置条件和后置条件,或者某些程序的循环不变量。 需要注意,根据定义2描述的基于不变量的APR过程的前两个步骤对于增加生成的补丁精度是必要的,该过程的实际修复步骤,即3-5步,可以正式陈述如下: - 上式中,
是基于不变量的错误定位, 是使用测试套件进行补丁生成和验证过程 表示使用验证工具V进行正式补丁验证的过程。 - 如果未找到合理的补丁,或者找到的补丁是不正确的,则修复过程返回失败。
- 如果合理的补丁通过了工具V执行的验证步骤,该过程将返回一个补丁
-
接下来讨论如何通过分析使用通过和失败的测试运行程序P产生规范
和 ,对无故障和有故障运行的分析产生了以下模式 -
,只是用成功运行推断不变量,这些不变量表示程序 的预期行为
-
,使用失败运行推断不变量,注意到 可能同时包含好的和坏的模式,这取决于目标错误如何影响 的不同功能。
-
, 与错误相关的违反不变量的集合
-
-
将推断的不变量分类和区分为好的和坏的模式是很重要的,特别是在处理有多个功能要求的程序时。
- 这将有助于在修改代码时确定要维持的期望不变量集合和要修复的冲突的不变量集合。
- 同时也将帮助识别与分析bug相关的不变量集合
-
推断出的
和 的准确性很大程度上取决于所使用不变量推断工具的准确性和不变量精炼过程的准确性,通过可达性分析增加程序行为的覆盖范围,可以增加 和 为真的可能性
Definition 3 (Patch validation in invariant-based APR)
-
令
为一个包括 bug 的程序, 是一个包含至少一个失败测试和一个正确测试的测试套件。 假设 是一个合理的补丁使得 通过了 中的所有测试用例。 补丁 的有效性可以按照以下形式进行检查 其中, 工具的响应取决于正在检查的程序是否满足或违反了规范 -
为了提高对生成补丁有效性的信心,我们选择针对
和 进行验证。 然而,为了降低调用验证器 的成本,我们打算实施一个三步的补丁验证方法,首先使用测试套件,然后在使用程序验证器,生成合理的补丁是通过使用测试用例在第一步完成的,第二步设计对合理补丁针对不良模式集合(属性 )进行检查,通过前两步的补丁在第三步针对良好模式集合(属性 )进行检查
3 使用invariant的APR修复 Performance Bugs
- 性能bug是导致系统性能显著下降的编程错误。经验表明,许多广泛使用的商业软件都存在性能问题[13,6,10].
- 因此,这里需要开发一个严格的性能错误修复框架,确保在不影响功能的情况下提高效率。
- 与功能错误相比,性能错误的一个独特特征是性能错误不会影响程序的功能性(即程序在语义上是正确的,但效率低下),因此可以使用不变量推断工具自动推断程序的与其行为
- 本节描述了一个针对性能错误的基于不变量的APR系统,并演示了如何通过生成可以确保提高效率而不牺牲功能性的补丁来处理性能错误
3.1 针对性能bug的基于不变量的修复框架
-
在本节,我们描述解决性能bug的基于不变量的修复框架,框架主要包含以下部分
-
- 通过测试集:包含使程序运行快速的测试用例。
-
- 失败测试集:包含导致程序运行缓慢的测试用例。
-
- 运行时监视器:用于跟踪程序的执行时间,并区分快速运行和缓慢运行。
-
- 自动不变量推断工具(例如Daikon或CPAChecker)和自动不变量验证工具(例如PVS、Z3求解器或CPAChecker)。
-
-
接下来讨论如何定义通过测试和失败测试的概念,以及针对性能错误,生成和验证补丁的过程
针对性能错误的通过和失败测试
- 性能错误在运行时不会产生debug信息:不会产生崩溃,异常或不正确的结果。 因此我们使用一个含有预定义定时器的运行时监视器来重新定义通过和失败测试的概念
- 我们将导致快速运行的测试用例视为通过测试,而导致缓慢运行的测试用例视为失败测试。
- 一个修复方案,可以将缓慢运行转换为快速运行,同时保持原程序的期望行为,有效的修复
针对性能错误的补丁生成策略
- 因为我们处理的是语义上正确但效率底下的程序,因此通常可以通过重构原始程序的基本组件来创建程序的高效版本。
- 我们的初步分析表明,遗传修复工具(如GenProg)在处理性能错误方面是有效的。这表明,通过相对简单的更改,可以修复具有性能错误的程序。例如,可以使用遗传修复工具使用的移动,交换,删除和插入等变异操作符来修复各种性能错误
- 因此,我们的目标是将我们的修复框架和基于遗传的补丁生成工具结合起来
针对性能错误的补丁验证
- 需要注意的是,不变量推断工具也可以用于推导与程序非功能属性相关的。这可以通过向被修复的程序添加额外的非功能变量来实现。
- 假设我们有一个程序
带有一组变量 ,其中包含一个性能错误。 我们需要检查为程序 生成的补丁是否修理了性能错误,同时没有引入新的功能错误。为此,我们需要生成并验证与程序效率属性相关的断言,如下所述 -
- 添加一个新变量值
, 其值不会影响 的行为。正在处理的性能错误的类型决定了如何使用 来模拟程序的效率。然而,对于我们考虑的循环程序, 的作用像一个计数器,每次迭代增加一次,换句话说,这是循环迭代次数作为效率的模型
- 添加一个新变量值
-
- 使用不变量推断工具
来推断原始版本和补丁版本的不变量上的数量,分别表示为 ,前者表示 涉及变量 的程序 的不变量集合
- 使用不变量推断工具
-
- 比较
和 中的 数值 断言,确定补丁版本是否比原始版本更有效率
- 比较
-
- 为简单起见,我们假设我们处理的程序只有一个循环。然而,分析程序中的循环数量决定了需要多少个额外变量,因此,不变量推断工具
用于推断关于 的不变量,然后我们区分以下类型的断言 -
: 与程序功能相关的断言
-
:与程序效率相关的断言
-
- 使用生成的断言,可以用以下方法检测补丁的有效性
其中是一个bool操作来检查给定的不变量集合是否语义相同, 是一个bool操作来检查与修补版本相关的谓词中的上界是否小于与原始程序相关的谓词中的上界。 - 我们现在描述两种正式的程序,使用可用的程序验证工具验证合理补丁的有效性
-
- Daikon-PVS:在这个补丁验证过程中,Daikon用于生成和程序
功能和效率相关的断言。 如果 (即与功能属性相关的断言)不相同,则可能需要检查这些集合中的谓词之间的等价和蕴含关系,以确定 和 是否在语义上等价。通过查询定理证明器 ,可以完成这项任务。
- Daikon-PVS:在这个补丁验证过程中,Daikon用于生成和程序
-
- CPAChecker-PVS:CPACheck的一个有趣特性是它以GraphML格式产生正确性证明,并且在这些证明中,可以分析程序的不变量。可以利用这个特性生成原始程序和相应的合理程序的不变量集合。如果两个程序的不变量集合不相同,则可能需要调用 PVS来检查这两个不变量集合之间的等价和蕴含关系。
-
3.2 使用基于不变量的APR修复现实世界的性能bug
- 本节,我们将展示基于不变量的APR可以用于解决现实世界的性能bug。处于空间的原因,我们只考虑一个有趣的性能bug的实例,如下代码。这个bug是基于真实事件Apache的一个真实缺陷,也被其它研究人员研究过
int found = -1;
while ( found < 0 ) {
// Check if string source [] contains target []
char first = target [0];
int max = sourceLen - targetLen ;
for (int i = 0; i <= max; i++) {
// Look for first character .
if ( source [i] != first) {
while (++i <= max && source[i] != first );
}
// Found first character
if (i <= max) {
int j = i + 1;
int end = j + targetLen - 1;
for (int k=1; j<end && source [j]== target[k]; j++, k ++);
if (j == end) {
/* Found whole string target . */
found = i;
break;
}
}
}
// append another character ; try again
source [ sourceLen ++] = getchar ();
}
对程序分析
- 该程序旨在确定给定的(目标)字符串是否包含在另一个(源)字符串中。如果在源字符串中找到了目标字符串,程序设置变量
found
设置为目标字符串的第一个字符的索引。 - 但是,该程序存在一个很大的性能缺陷:
- 当目标字符串位于源字符串的开头时,运行速度很快;
- 当字符串接近源字符串末尾时,运行速度缓慢,这是因为有大量冗余计算的增加,错误在于for循环控制的循环变量i的初始化语句在第6行应该放在主while循环外,就在变量
found
初始化之后
3.3 结果和分析
- 为了处理3.2中的性能bug,我们选择了两种APR工具,这两种工具都是修复C代码的通用修复工具,可以用于修复一系列程序错误,包括循环程序错误
- 基于搜索的GenProg[7]
- 基于语义的FAnglix[16]
- GenProg成功生成了一个合理的补丁,但FAnglix没有。
- 为了避免原始程序中的重复计算,GenProg将变量i的初始化语句移动到了第6行for循环之外,即修补版本的程序以变量i的初始化语句开始,此时生成的补丁同构了测试用例,因为i不再每次循环接收新字符时被设置为0
- 为了检查GenProg生成的合理补丁的有效性,我们使用了工具Daikon,比较了原始程序和合理补丁版本的功能和效率断言。 Daikon生成了与功能变量相关的相同不变量集合(即,原始版本和修补版本都有与程序变量相关的相同不变量),这表明补丁保持了原始程序的功能行为
代码分析
- 代码中包含了4个的循环
- 第2行的while循环
- 第6行的for循环
- 第9行的while循环
- 第15行的for循环
- 为了评估原始程序和修补程序的效率,需要计算迭代次数的上界,因为补丁不会通过添加或删除操作修改任何循环的逻辑,即在两个程序中,四个循环的每次迭代都涉及相同数量的操作,因此,我为每个循环添加四个迭代计数器(cnt2,cnt6,cnt9,cnt15)来模拟每个循环的效率。 在分析缺陷和修补版本的效率断言中,我们得出以下观察结果
- 对于有缺陷和修补版本中的cnt2,cnt15生成的不变量时相同的,这表明补丁不会影响第2,15行循环的迭代次数
- cnt9只在缺陷版本中递增,并且cnt9<=500499,修补版本不再使用第9行的while循环是一个重大的改进
- Daikon为有缺陷版本生成了不变量cnt6<=1001,而修补版本生成了不变量cnt6<=501,这表明修补版本的第6行循环的迭代次数比原始代码中少了50%
- 上述发现,以及原始版本和修补版本的衍生功能断言时相同的事实,增强了我们对GenProg工具生成补丁有效性的信心
4 相关工作
APR中过拟合问题
- 目前已有多种解决方法来缓解APR中的过度拟合问题
- 例如符号规范推断[8]
- 基于机器学习的补丁优先级排序[1]
- 基于模糊测试的测试套件增强[5]和合成路径探索[12]
- 这些措施依赖于有限的不完整的测试用例,不能保证补丁的普遍正确性。
- 与基于生成测试输入的方法相比面积与不变量的APR在修改代码时自动生成并精炼需要保持的不变量即需要修复的问题不变量,这使得该方法比现有修复方法更可靠。
- 现在通用的APR工具依赖于符号执行或合成执行来发现反例并生成修复补丁[9,12],然而这些修复方法需要手动检查生成的补丁是否正确或与开发者的补丁相同,这可能存在错误。 基于不变量的APR使得可以应用自动化验证技术来缓解过拟合问题,并通过与开发者补丁相比较来正式和系统地检查生成的补丁的准确性
解决性能错误
- 目前已经进行了许多尝试,使用动态,静态,混合分析方法来检测和修复程序中的性能错误[13,6,10]。
- [10]对性能错误进行了实证调查,并提出了一个用于识别它们的效率规则。
- [13]中,使用动态-静态分析技术,开发了几种修复策略来识别和解决性能问题。
- 然而我们的方法与先前的研究不同之处在于,它是一种更通用和精确的技术,利用程序不变量来解决循环程序的性能问题,并产生可靠的补丁。因为系统不变量,原始程序的效率可以系统的和修补版本进行比较
5 结论 和 未来工作
结论
- 我们描述了一个基于程序不变量概念的新型自动程序修复(APR)系统。
- 基于不变量的APR有望处理比其它APR方法更广泛的错误,并生成更可靠的补丁,这是由于基于不变量的修复系统依赖于更强的正确性指标,而不是测试套件。
- 我们通过开发了一个针对性能缺陷的不变量修复系统来展示APR中利用不变量的实用性。 初步结果现实,基于不变量的APR可以帮助生成高质量的补丁,这些补丁可以确保程序效率提高而不会对其功能产生不利影响。
未来工作
- 为了完善此处开始的基于不变量的APR研究,我们确定了以下未来工作的关键方向
- 首先,我们的主要目的是进行深入的实证分析,以确定基于不变量的APR在处理程序中功能性和非功能性缺陷方面的表现如何,这还涉及评估当前可访问的不变量推断和验证工具
- 准确的不变量生成是确保基于不变量的APR生成的补丁有效性的关键,我们推测可达性分析可以帮助解决这个复杂的计算任务,我们的目标是将基于不变量的APR与支持不变量生成和精炼的程序验证工具(如CPAChecker和PathFinder)相结合
Ⅱ Invalidator: Automated Patch Correctness Assessment Via Semantic and Syntactic Reasoning
- 引用:Le-Cong T, Luong D M, Le X B D, et al. Invalidator: Automated patch correctness assessment via semantic and syntactic reasoning[J]. IEEE Transactions on Software Engineering, 2023.
- CCF A TSE
- 链接
4.1 介绍a
- 本论文介绍名为INVALIDATOR的新技术,它结合了语义和语法推理来自动评估由自动程序修复(APR)技术生成的补丁的正确性。
- 利用程序不变量推理程序的语义属性
- 使用预训练语言模型捕捉程序语法,该模型从大量代码语料库中学习语言语义。
- 与其他自动化补丁正确性评估(APAC)技术类似,INVALIDATOR利用APR修补过的程序与真实正确程序之间的行为差异来确定补丁的正确性。然而
- 例如DIFFTGEN [65]、PATCHSIM [66]或RANDOOP [18]、[46]。这些技术生成新测试以增强当前测试套件,其中每个测试生成一个执行,执行次数与生成测试用例成正比
- INVALIDATOR仅使用当前测试套件,并推断出自然泛化超出测试套件的程序不变量,程序不变量的泛化运行INVALIDATOR高效且在语义上推理程序的正确性,此外,INVALIDATOR融入语法推理来增强其有效性,进一步增强语义推理
4.2 工作流程
-
- 基于语义的分类器:
- 由两个高级直观概念构成
- a. 程序不变量在错误版本和正确版本都保持不变,可以作为程序的正确规范
- b. 只在错误版本存在但在正确版本不存在的程序不变量可能表示程序的错误规范
- 如果自动生成的不定违反了正确的规范或保留了错误的规范,INVALIDATOR会判断过拟合
- INVALIDATOR首先使用DAIKON根据原始测试套件自动推断每个程序的可能不变式。然后,INVALIDATOR构造正确和错误的规范集合,这些规范作为被测程序的近似规范。根据推断出的规范,如果从机器修补的程序中推断出的不变式违反了正确的规范或保留了错误的规范,INVALIDATOR就会判断补丁过拟合。
-
- 基于语法的分类器
- 在基于不变式的规范推断无法确定过拟合补丁的情况下,INVALIDATOR进一步通过机器生成的补丁与其错误版本和正确版本之间的语言语义差异来识别过拟合补丁。
- 具体使用使用预训练的语言模型,即CODEBERT,从每个程序的源代码中提取源语法特征。然后,INVALIDATOR通过一系列比较函数(例如,减法或相似度)来衡量差异。最后,INVALIDATOR使用从标记数据训练的模型来估计基于语法接近度的机器生成补丁是否过拟合的可能性。
4.3 主要内容
-
在本文中,我们使用Daikon[7]——一个流行的用于挖掘可能不变式的工具,作为我们的动态不变式推断技术。Daikon观察程序的执行轨迹,并将它们与一组模板进行匹配,以推断出在所有或大多数执行中成立的可能不变式。Daikon可以从多达311个模板的大型集合中(参见Daikon手册文档1的细节),检测出广泛概括超出用于产生执行轨迹的测试套件的各种不变式[49]。
-
APR技术的作者通常通过以下两种方式评估补丁的正确性:
- (1) 使用与修复时所用测试套件不同的独立测试套件来测试生成补丁的泛化能力;
- (2) 通过与真实情况进行比较的手动检查来评估APR生成的补丁。
-
Le等人表明,通过独立测试套件进行的自动验证不如手动验证有效,但使用手动验证存在人为偏见的潜在风险。此外,手动验证需要重复且昂贵的任务,而自动验证可以弥补这一点。
Mesbah A, Van Deursen A, Roest D. Invariant-based automatic testing of modern web applications[J]. IEEE Transactions on Software Engineering, 2011, 38(1): 35-53.