关于类型感知算子突变对测试SMT求解器的异常有效性
On the Unusual Effectiveness of Type-Aware Operator Mutations for Testing SMT Solvers
摘要：
我们提出了类型感知算子变异，一个简单的，但异常有效的方法来测试SMT求解器。其关键思想是在种子公式中对符合类型的运算符进行变异，以生成良好类型的变异公式。这些突变的公式，然后用作SMT求解器的测试用例。我们在OpFuzz工具中实现了类型感知的操作符变异，并使用它对两个最先进的SMT求解器Z3和CVC 4进行了压力测试。类型感知的操作符突变异常有效：在一年的OpFuzz广泛测试中，我们在Z3和CVC 4的GitHub问题跟踪器上报告了1，092个错误，其中819个独特的错误得到了确认，685个确认的错误被开发人员修复。检测到的错误是高度多样化的-我们发现了许多不同类型的错误（健全错误，无效模型错误，崩溃等），逻辑和求解器配置。我们进一步对OpFuzz发现的bug进行了深入研究。研究结果表明，OpFuzz发现的错误质量较高。其中许多影响SMT求解器代码库的核心组件，并且一些需要开发人员进行重大更改来修复。在OpFuzz发现的819个确认的bug中，184个是SMT求解器中最关键的bug，489个是求解器的默认模式。值得注意的是，OpFuzz在CVC 4中发现了27个关键的可靠性错误，这已经被证明是一个非常稳定的SMT解决方案。
英文摘要：
We propose type-aware operator mutation, a simple, but unusually effective approach for testing SMT solvers. The key idea is to mutate operators of conforming types within the seed formulas to generate well-typed mutant formulas. These mutant formulas are then used as the test cases for SMT solvers. We realized type-aware operator mutation within the OpFuzz tool and used it to stress-test Z3 and CVC4, two state-of-the-art SMT solvers. Type-aware operator mutations are unusually effective: During one year of extensive testing with OpFuzz, we reported 1,092 bugs on Z3's and CVC4's respective GitHub issue trackers, out of which 819 unique bugs were confirmed and 685 of the confirmed bugs were fixed by the developers. The detected bugs are highly diverse -- we found bugs of many different types (soundness bugs, invalid model bugs, crashes, etc.), logics and solver configurations. We have further conducted an in-depth study of the bugs found by OpFuzz. The study results show that the bugs found by OpFuzz are of high quality. Many of them affect core components of the SMT solvers' codebases, and some required major changes for the developers to fix. Among the 819 confirmed bugs found by OpFuzz, 184 were soundness bugs, the most critical bugs in SMT solvers, and 489 were in the default modes of the solvers. Notably, OpFuzz found 27 critical soundness bugs in CVC4, which has proved to be a very stable SMT solver.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
