论类型感知算子变异在测试SMT求解器中的异常有效性
软件工程
2020-11-13 v4 编程语言
摘要
我们提出了一种类型感知算子变异方法，这是一种简单但异常有效的SMT求解器测试方法。其核心思想是在种子公式中变异符合类型约束的算子，以生成类型正确的变异公式。这些变异公式随后被用作SMT求解器的测试用例。我们在OpFuzz工具中实现了类型感知算子变异，并用它对Z3和CVC4这两个最先进的SMT求解器进行了压力测试。类型感知算子变异异常有效：在使用OpFuzz进行为期一年的广泛测试期间，我们在Z3和CVC4各自的GitHub问题跟踪器上报告了1092个缺陷，其中819个独特缺陷得到确认，685个已确认缺陷被开发者修复。检测到的缺陷高度多样化——我们发现了多种不同类型的缺陷（可靠性缺陷、无效模型缺陷、崩溃等）、逻辑和求解器配置。我们进一步对OpFuzz发现的缺陷进行了深入研究。研究结果表明，OpFuzz发现的缺陷质量很高。其中许多缺陷影响了SMT求解器代码库的核心组件，有些需要开发者进行重大修改才能修复。在OpFuzz发现的819个已确认缺陷中，有184个是可靠性缺陷，即SMT求解器中最关键的缺陷，489个出现在求解器的默认模式下。值得注意的是，OpFuzz在CVC4中发现了27个关键的可靠性缺陷，而CVC4已被证明是一个非常稳定的SMT求解器。
引用
@article{arxiv.2004.08799,
title = {On the Unusual Effectiveness of Type-Aware Operator Mutations for Testing SMT Solvers},
author = {Dominik Winterer and Chengyu Zhang and Zhendong Su},
journal= {arXiv preprint arXiv:2004.08799},
year = {2020}
}