SMTLOC: 基于多源频谱的SMT求解器缺陷定位
CSTR:
作者:
作者单位:

作者简介:

王笑爽(1998-),女,硕士生,主要研究领域为软件测试,缺陷定位;周志德(1990-),男,博士,CCF专业会员,主要研究领域为智能软件工程,可信编译,深度学习优化;李晓晨(1989-),男,博士,副教授,CCF专业会员,主要研究领域为演化计算,智能软件工程,开源软件工程;江贺(1980-),男,博士,教授,博士生导师,CCF杰出会员,主要研究领域为智能软件工程,工业软件测试;任志磊(1984-),男,博士,教授,博士生导师,CCF专业会员,主要研究领域为演化计算,算法自动构造,数据挖掘,软件大数据分析

通讯作者:

任志磊, E-mail: zren@dlut.edu.cn

中图分类号:

TP311

基金项目:

南京航空航天大学科研基地创新(理工类)项目(NJ2020022); 国家自然科学基金(62072068, 62032004); 国家重点研发计划(2018YFB1003900)


SMTLOC: Bug Localization for SMT Solver Based on Multi-source Spectrum
Author:
Affiliation:

Fund Project:

  • 摘要
  • |
  • 图/表
  • |
  • 访问统计
  • |
  • 参考文献
  • |
  • 相似文献
  • |
  • 引证文献
  • |
  • 资源附件
  • |
  • 文章评论
    摘要:

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

    Abstract:

    SMT solver is an important system software. Therefore, bugs in the SMT solver may lead to the function failure of software relying on it and even bring security incidents. However, fixing bugs in the SMT solver is time-consuming because developers need to spend a lot of effort in understanding and finding the root cause of the bugs. Although many studies on software bug localization have been proposed, there is no systematic work to automatically locate bugs in the SMT solver. Therefore, this study proposes a bug localization method for the SMT solver based on multi-source spectrums, namely SMTLOC. First, for a given bug in the SMT solver, SMTLOC proposes an enumeration-based algorithm to mutate the formula that triggers the bug by generating a set of witness formulas that will not trigger the bug but has a similar execution trace with the formula that triggers the corresponding bug. Then, according to the execution trace of the witness formulas and the source code information of the SMT solver, SMTLOC develops a technique based on the coverage spectrum and historical spectrum to calculate the suspiciousness of files, thus locating the files that contain the bug. In order to evaluate the effectiveness of SMTLOC, 60 bugs in the SMT solver are collected. Experimental results show that SMTLOC is superior to the traditional spectrum bug localization method and can locate 46.67% of the bugs in TOP-5 files, and the localization effect is improved by 133.33%.

    参考文献
    相似文献
    引证文献
引用本文

王笑爽,周志德,李晓晨,江贺,任志磊. SMTLOC: 基于多源频谱的SMT求解器缺陷定位.软件学报,2024,35(7):3314-3331

复制
分享
文章指标
  • 点击次数:
  • 下载次数:
  • HTML阅读次数:
  • 引用次数:
历史
  • 收稿日期:2022-08-30
  • 最后修改日期:2022-12-06
  • 录用日期:
  • 在线发布日期: 2023-08-09
  • 出版日期: 2024-07-06
文章二维码
您是第位访问者
版权所有:中国科学院软件研究所 京ICP备05046678号-3
地址:北京市海淀区中关村南四街4号,邮政编码:100190
电话:010-62562563 传真:010-62562533 Email:jos@iscas.ac.cn
技术支持:北京勤云科技发展有限公司

京公网安备 11040202500063号