微信服务号

微信订阅号

2025年5月11日 12:29 星期日
首页 > 过刊浏览>2024年第35卷第7期 >3314-3331. DOI:10.13328/j.cnki.jos.006922
PDF HTML阅读 XML下载 导出引用 引用提醒
SMTLOC: 基于多源频谱的SMT求解器缺陷定位
作者:
作者简介:

王笑爽(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:
  • 摘要
    • | |
  • 访问统计
    • |
  • 参考文献 [47]
    • |
  • 相似文献
    • |
  • 引证文献
    • | |
  • 文章评论
    摘要:

    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%.

    参考文献
    [1] Detlefs D, Nelson G, Saxe JB. Simplify: A theorem prover for program checking. Journal of the ACM, 2005, 52(3): 365–473. [doi: 10.1145/1066100.1066102]
    [2] Cadar C, Dunbar D, Engler DR. KLEE: Unassisted and automatic generation of high-coverage tests for complex systems programs. In: Proc. of the 8th USENIX Conf. on Operating Systems Design and Implementation. San Diego: USENIX Association, 2008. 209–224.
    [3] Godefroid P, Klarlund N, Sen K. DART: Directed automated random testing. In: Proc. of the 2005 ACM SIGPLAN Conf. on Programming Language Design and Implementation. Chicago: ACM, 2005. 213–223.
    [4] Bhargavan K, Bond B, Delignat-Lavaud A, Fournet C, Hawblitzel C, Hritcu C, Ishtiaq S, Kohlweiss M, Leino R, Lorch J, Maillard K, Pang JY, Parno B, Protzenko J, Ramananandro T, Rane A, Rastogi A, Swamy N, Thompson L, Wang P, Zanella-Béguelin S, Zinzindohoué JK. Everest: Towards a verified, drop-in replacement of HTTPS. In: Proc. of the 2nd Summit on Advances in Programming Languages. Asilomar: Schloss Dagstuhl, Leibniz-Zentrum für Informatik, 2017. 1–12.
    [5] Mechtaev S, Yi J, Roychoudhury A. Angelix: Scalable multiline program patch synthesis via symbolic analysis. In: Proc. of the 38th Int’l Conf. on Software Engineering. Austin: IEEE, 2016. 691–701.
    [6] Wiels V, Delmas R, Doose D, Garoche PL, Cazin J, Durrieu G. Formal verification of critical aerospace software. Aerospace Lab, 2012, (4): 1–8.
    [7] de Moura L, Bjørner N. Z3: An efficient SMT solver. In: Proc. of the 14th Int’l Conf. on Tools and Algorithms for the Construction and Analysis of Systems. Budapest: Springer, 2008. 337–340.
    [8] 王赞, 樊向宇, 邹雨果, 陈翔. 一种基于遗传算法的多缺陷定位方法. 软件学报, 2016, 27(4): 879-900. http://www.jos.org.cn/1000-9825/4970.htm
    Wang Z, Fan XY, Zou YG, Chen X. Genetic algorithm based multiple faults localization technique. Ruan Jian Xue Bao/Journal of Software, 2016, 27(4): 879-900 (in Chinese with English abstract). http://www.jos.org.cn/1000-9825/4970.htm
    [9] DiGiuseppe N, Jones JA. On the influence of multiple faults on coverage-based fault localization. In: Proc. of the 2011 Int’l Symp. on Software Testing and Analysis. Toronto: ACM, 2011. 210–220.
    [10] Liblit B, Naik M, Zheng AX, Aiken A, Jordan MI. Scalable statistical bug isolation. ACM SIGPLAN Notices, 2005, 40(6): 15–26. [doi: 10.1145/1064978.1065014]
    [11] Santelices R, Jones JA, Yu YB, Harrold MJ. Lightweight fault-localization using multiple coverage types. In: Proc. of the 31st IEEE Int’l Conf. on Software Engineering. Vancouver: IEEE, 2009. 56–66.
    [12] Xuan JF, Monperrus M. Test case purification for improving fault localization. In: Proc. of the 22nd ACM SIGSOFT Int’l Symp. on Foundations of Software Engineering. Hong Kong: ACM, 2014. 52–63.
    [13] Moon S, Kim Y, Kim M, Yoo S. Ask the mutants: Mutating faulty programs for fault localization. In: Proc. of the 7th IEEE Int’l Conf. on Software Testing, Verification and Validation. Cleveland: IEEE, 2014. 153–162.
    [14] Papadakis M, Le Traon Y. Using mutants to locate “unknown” faults. In: Proc. of the 5th IEEE Int’l Conf. on Software Testing, Verification and Validation. Montreal: IEEE, 2012. 691–700.
    [15] Papadakis M, Le Traon Y. Metallaxis-FL: Mutation-based fault localization. Software Testing, Verification and Reliability, 2015, 25(5–7): 605–628.
    [16] 贺韬, 王欣明, 周晓聪, 李文军, 张震宇, 张成志. 一种基于程序变异的软件错误定位技术. 计算机学报, 2013, 36(11): 2236-2244. [doi: 10.3724/SP.J.1016.2013.02236]
    He T, Wang XM, Zhou XC, Li WJ, Zhang ZY, Cheung SC. A software fault localization technique based on program mutations. Chinese Journal of Computers, 2013, 36(11): 2236-2244 (in Chinese with English abstract). [doi: 10.3724/SP.J.1016.2013.02236]
    [17] 文万志, 李必信, 孙小兵, 刘翠翠. 一种基于层次切片谱的软件错误定位技术. 软件学报, 2013, 24(5): 977-992. http://www.jos.org.cn/1000-9825/4342.htm
    Wen WZ, Li BX, Sun XB, Liu CC. Technique of software fault localization based on hierarchical slicing spectrum. Ruan Jian Xue Bao/Journal of Software, 2013, 24(5): 977-992 (in Chinese with English abstract). http://www.jos.org.cn/1000-9825/4342.htm
    [18] Barbosa H, Barrett C, Brain M, Kremer G, Lachnitt H, Mann M, Mohamed A, Mohamed M, Niemetz A, Nötzli A, Ozdemir A, Preiner M, Reynolds A, Sheng Y, Tinelli C, Zohar Y. cvc5: A versatile and industrial-strength SMT solver. In: Proc. of the 28th Int’l Conf. on Tools and Algorithms for the Construction and Analysis of Systems. Munich: Springer, 2022. 415–442.
    [19] Chen JJ, Han JQ, Sun PY, Zhang LM, Hao D, Zhang L. Compiler bug isolation via effective witness test program generation. In: Proc. of the 27th ACM Joint Meeting on European Software Engineering Conf. and Symp. on the Foundations of Software Engineering. Tallinn: ACM, 2019. 223–234.
    [20] Chen JJ, Ma HY, Zhang LM. Enhanced compiler bug isolation via memoized search. In: Proc. of the 35th IEEE/ACM Int’l Conf. on Automated Software Engineering. Melbourne: IEEE, 2020. 78–89.
    [21] Abreu R, Zoeteweij P, Golsteijn R, van Gemund AJC. A practical evaluation of spectrum-based fault localization. Journal of Systems and Software, 2009, 82(11): 1780–1792. [doi: 10.1016/j.jss.2009.06.035]
    [22] Winterer D, Zhang CY, Su ZD. Validating SMT solvers via semantic fusion. In: Proc. of the 41st ACM SIGPLAN Conf. on Programming Language Design and Implementation. London: ACM, 2020. 718–730.
    [23] Ren ZL, Fan XF, Li XC, Zhou ZD, Jiang H. Multi-objective evolutionary algorithm for string SMT solver testing. In: Proc. of the 8th Int’l Conf. on Dependable Systems and Their Applications (DSA). Yinchuan: IEEE, 2021. 102–113.
    [24] 郭肇强, 周慧聪, 刘释然, 李言辉, 陈林, 周毓明, 徐宝文. 基于信息检索的缺陷定位: 问题、进展与挑战. 软件学报, 2020, 31(9): 2826-2854. http://www.jos.org.cn/1000-9825/6087.htm
    Guo ZQ, Zhou HC, Liu SR, Li YH, Chen L, Zhou YM, Xu BW. Information retrieval based bug localization: Research problem, progress, and challenges. Ruan Jian Xue Bao/Journal of Software, 2020, 31(9): 2826-2854 (in Chinese with English abstract). http://www.jos.org.cn/1000-9825/6087.htm
    [25] Hassan AE. Predicting faults using the complexity of code changes. In: Proc. of the 31st IEEE Int’l Conf. on Software Engineering. Vancouver: IEEE, 2009. 78–88.
    [26] Servant F, Jones JA. History slicing: Assisting code-evolution tasks. In: Proc. of the 20th ACM SIGSOFT Int. Symp. on the Foundations of Software Engineering. North Carolina: ACM, 2012. 43.
    [27] Scott J, Mora F, Ganesh V. BanditFuzz: A reinforcement-learning based performance fuzzer for SMT solvers. In: Proc. of the 12th Int’l Conf. on Software Verification. Los Angeles: Springer, 2020. 68–86.
    [28] Abreu R, Zoeteweij P, van Gemund AJC. On the accuracy of spectrum-based fault localization. In: Testing: Academic and Industrial Conf. Practice and Research Techniques-MUTATION (TAICPART-MUTATION 2007). Windsor: IEEE, 2007. 89–98.
    [29] de Souza HA, Chaim ML, Kon F. Spectrum-based software fault localization: A survey of techniques, advances, and challenges. arXiv:1607.04347, 2016.
    [30] Levenshtein VI. Binary codes capable of correcting deletions, insertions and reversals. Soviet Physics Doklady, 1966, 10(8): 707–710.
    [31] Kuhn HW. The Hungarian method for the assignment problem. Naval research logistics quarterly, 1955, 2(1–2): 83–97.
    [32] Winterer D, Zhang CY, Su ZD. On the unusual effectiveness of type-aware operator mutations for testing SMT solvers. Proceedings of the ACM on Programming Languages, 2020, 4(OOPSLA): 193. [doi: 10.1145/3428261]
    [33] Mansur MN, Christakis M, Wüstholz V, Zhang FY. Detecting critical bugs in SMT solvers using blackbox mutational fuzzing. In: Proc. of the 28th ACM Joint Meeting on European Software Engineering Conf. and Symp. on the Foundations of Software Engineering. ACM, 2020. 701–712.
    [34] Yao PS, Huang HQ, Tang WS, Shi QK, Wu RX, Zhang C. Skeletal approximation enumeration for SMT solver testing. In: Proc. of the 29th ACM Joint Meeting on European Software Engineering Conf. and Symp. on the Foundations of Software Engineering. Athens: ACM, 2021. 1141–1153.
    [35] Le TDB, Lo D, Le Goues C, Grunske L. A learning-to-rank based fault localization approach using likely invariants. In: Proc. of the 25th Int’l Symp. on Software Testing and Analysis. Saarbrücken: ACM, 2016. 177–188.
    [36] Pearson S, Campos J, Just R, Fraser G, Abreu R, Ernst MD, Pang D, Keller B. Evaluating and improving fault localization. In: Proc. of the 39th IEEE/ACM Int’l Conf. on Software Engineering (ICSE). Buenos Aires: IEEE, 2017. 609–620.
    [37] Lou YL, Zhu QH, Dong JH, Li X, Sun ZY, Hao D, Zhang L, Zhang LM. Boosting coverage-based fault localization via graph-based representation learning. In: Proc. of the 29th ACM Joint Meeting on European Software Engineering Conf. and Symp. on the Foundations of Software Engineering. Athens: ACM, 2021. 664–676.
    [38] Wen M, Chen JJ, Tian YQ, Wu RX, Hao D, Han S, Cheung SC. Historical spectrum based fault localization. IEEE Transactions on Software Engineering, 2021, 47(11): 2348–2368. [doi: 10.1109/TSE.2019.2948158]
    [39] Blotsky D, Mora F, Berzish M, Zheng YH, Kabir I, Ganesh V. StringFuzz: A fuzzer for string solvers. In: Proc. of the 30th Int’l Conf. on Computer Aided Verification. Oxford: Springer, 2018. 45–51.
    [40] Brummayer R, Biere A. Fuzzing and delta-debugging SMT solvers. In: Proc. of the 7th Int’l Workshop on Satisfiability Modulo Theories. Montreal: ACM, 2009. 1–5.
    [41] Nagappan N, Zeller A, Zimmermann T, Herzig K, Murphy B. Change bursts as defect predictors. In: Proc. of the 21st IEEE Int’l Symp. on Software Reliability Engineering. San Jose: IEEE, 2010. 309–318.
    [42] Sisman B, Kak AC. Incorporating version histories in information retrieval based bug localization. In: Proc. of the 9th IEEE Working Conf. on Mining Software Repositories (MSR). Zurich: IEEE, 2012. 50–59.
    [43] Wang SW, Lo D. Version history, similar report, and structure: Putting them together for improved bug localization. In: Proc. of the 22nd Int’l Conf. on Program Comprehension. Hyderabad: ACM, 2014. 53–63.
    相似文献
    引证文献
引用本文

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

复制
相关视频

分享
文章指标
  • 点击次数:
  • 下载次数:
  • HTML阅读次数:
  • 引用次数:
历史
  • 收稿日期:2022-08-30
  • 最后修改日期:2022-12-06
  • 在线发布日期: 2023-08-09
  • 出版日期: 2024-07-06
文章二维码
友情链接:中国科学院软件研究所中国计算机学会中国科学院国家自然科学基金委员会CCF数字图书馆Int'l J of Softw Info计算机系统应用
您是第位访问者
版权所有：中国科学院软件研究所 京ICP备05046678号-3
地址：北京市海淀区中关村南四街4号,邮政编码：100190
电话：010-62562563 传真：010-62562533 Email：jos@iscas.ac.cn
技术支持：北京勤云科技发展有限公司

京公网安备 11040202500063号