摘要:SMT求解器作为重要的基础软件, 其存在的缺陷可能会导致依赖于它的软件功能失效, 甚至带来安全事故. 然而, 修复SMT求解器缺陷是一个十分耗时的任务, 因为开发者需要花费大量的时间和精力来理解并找到缺陷的根本原因. 虽然已有许多软件缺陷定位方面的研究, 但尚未有系统的工作研究如何自动定位SMT求解器缺陷. 因此, 提出一种基于多源频谱的SMT求解器缺陷定位方法SMTLOC. 首先, 对于给定的SMT求解器缺陷, SMTLOC提出一种枚举算法, 用以对触发该缺陷的公式进行变异, 从而生成一组不触发缺陷, 但与触发缺陷的公式具有相似执行路径的证人公式. 然后, SMTLOC根据证人公式的执行路径以及SMT求解器的源码信息, 提出一种融合覆盖频谱和历史频谱的文件可疑度计算方法, 从而定位可能存在缺陷的文件. 为了验证SMTLOC的有效性, 收集60个SMT求解器缺陷. 实验结果表明, SMTLOC的缺陷定位效果明显优于传统的频谱缺陷定位方法, SMTLOC可以将46.67%的缺陷定位在TOP-5的文件内, 定位效果提升了133.33%.