微信服务号

微信订阅号

2025-5-11- 18
Home > Archive>Volume 35, Issue 7, 2024 >3314-3331. DOI:10.13328/j.cnki.jos.006922
PDF HTML XML Export Cite reminder
SMTLOC: Bug Localization for SMT Solver Based on Multi-source Spectrum
Author:
Affiliation:

Clc Number:

TP311

  • Article
    • | |
  • Metrics
    • |
  • Reference [47]
    • |
  • Related
    • |
  • Cited by
    • | |
  • Comments
    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%.

    Reference
    [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.
    Related
    Cited by
    Comments
    Comments
    分享到微博
    Submit
Get Citation

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

Copy
Share
Article Metrics
  • Abstract:
  • PDF:
  • HTML:
  • Cited by:
History
  • Received:August 30,2022
  • Revised:December 06,2022
  • Online: August 09,2023
  • Published: July 06,2024
Links:Institute of Software, CASChina Computer FederationCASNSFC
You are the first2043811Visitors
Copyright: Institute of Software, Chinese Academy of Sciences Beijing ICP No. 05046678-4
Address：4# South Fourth Street, Zhong Guan Cun, Beijing 100190,Postal Code：100190
Phone：010-62562563 Fax：010-62562533 Email：jos@iscas.ac.cn
Technical Support：Beijing Qinyun Technology Development Co., Ltd.

Beijing Public Network Security No. 11040202500063