Improve methods of infeasible path detection by SMT solvers in software testing using reinforcement learning

Document Type : Original Article

Authors

Faculty of Computer Engineering, K.N Toosi University of Technology, Tehran, Iran.

Abstract

Software testing is an important and necessary matter in the development process of any software. Nowadays, an important part of software testing is performed automatically. In automated software testing, there may be obstacles that make the test difficult. One of these obstacles is the infeasible paths in the control flow graph obtained from the source code of the software under test. Infeasible paths are paths that cannot be traversed by any input. The existence of such paths can cause problems in various fields such as test data generation, security and etc., leading to a waste of resources. In order to prevent the mentioned problems, detection of infeasible paths can be very critical. But recognizing these paths in large software can be a time-consuming task due to the large amount of codes and the high number of paths in the control flow graph. In this article, a method is proposed that can increase the infeasible paths detection speed by applying reinforcement learning algorithms. In this method, the speed of the Z3 SMT solver has been increased by using the DQN agent. Z3 is a tool used to check the satisfiability of formulas constructed from the conditions in the control flow graph for detecting infeasible paths. In fact, in this paper, the techniques provided by Z3 are learned using reinforcement learning, and then by selecting and applying these techniques based on the learning performed, the solving speed increases. As the speed of the Z3 tool increases, the speed of all algorithms and methods that use this tool to detect infeasible paths in control flow graphs will also increase. Also, the Z3 tool is applicable in any field where problems can be reduced to the satisfiability of a formula, and improving its performance in those fields can also be effective. The proposed method in this article has been tested on QF_NRA and QF_NIA logics. In the experiments, it is shown that using the proposed method, the speed of the Z3 solver can be increased up to 4.7 times. Furthermore, in the conducted experiments using this method, the speed of Z3 increased by an average of 1.954 times in QF_NRA logic and 1.687 times in QF_NIA logic.

Keywords

Main Subjects

References

[1] P. Ammann and J. Offutt, Introduction to Software Testing. Cambridge, U.K.: Cambridge Univ. Press, 2016, doi: 10.1017/9781316771273.
[2] B. Beizer, Software Testing Techniques. New York, NY, USA: Van Nostrand Reinhold, 1990.
[3] H. Farzaneh, S. Bakhshayeshi, R. Ebrahimi Atani, and A. Shahbahrami, “A survey on test data generation techniques based on Mutation Testing,” Soft Comput. J., vol. 2, no. 1, pp. 72-85, 2013, dor: 20.1001.1.23223707.1392.2.1.61.5 [In Persian].
[4] Y.-W. Wang, Y. Xing, and X.-Z. Zhang, “A method of path feasibility judgment based on symbolic execution and range analysis,” Int. J. Future Gener. Commun. Netw., vol. 7, no. 3, pp. 205-212, 2014, doi: 10.14257/ijfgcn.2014.7.3.19.
[5] H. Zhu, D. Jin, Y. Gong, Y. Xing, and M. Zhou, “Detecting interprocedural infeasible paths based on unsatisfiable path constraint patterns,” IEEE Access, vol. 7, pp. 15040-15055, 2019, doi: 10.1109/ACCESS.2019.2894593.
[6] S. Jiang et al., “An approach for detecting infeasible paths based on a SMT solver,” IEEE Access, vol. 7, pp. 69058-69069, 2019, doi: 10.1109/ACCESS.2019.2918558.
[7] L. de Moura and N. Bjorner, “Z3: An efficient SMT solver,” in Proc. Int. Conf. Tools Algorithms Constr. Anal. Syst., 2008, pp. 337-340, doi: 10.1007/978-3-540-78800-3_24.
[8] C. Barrett and C. Tinelli, “Satisfiability modulo theories,” in Handbook of Model Checking, Springer, 2018, pp. 305-343, doi: 10.1007/978-3-319-10575-8_11.
[9] M. Balunovic, P. Bielik, and M. Vechev, “Learning to solve SMT formulas,” Adv. Neural Inf. Process. Syst., vol. 31, 2018.
[10] S. Anand, P. Godefroid, and N. Tillmann, “Demand-driven compositional symbolic execution,” in Proc. Int. Conf. Tools Algorithms Constr. Anal. Syst., 2008, pp. 367-381, doi: 10.1007/978-3-540-78800-3_28.
[11] J. Scott, F. Mora, and V. Ganesh, “BanditFuzz: Fuzzing SMT solvers with reinforcement learning,” University of Waterloo, Waterloo Research, 2020.
[12] S. Jeon and J. Moon, “Dr. PathFinder: Hybrid fuzzing with deep reinforcement concolic execution toward deeper path-first search,” Neural Comput. Appl., vol. 34, pp. 10731-10750, 2022, doi: 10.1007/s00521-022-07008-8.
[13] M. Hajibaba and S. Parsa, “Software Fault Localization using Cross Entropy and N-gram Models,” Soft Comput. J., vol. 2, no. 1, pp. 44-59, 2013, dor: 20.1001.1.23223707.1392.2.1.59.3 [In Persian].
[14] S. Ding, H.B.K. Tan, and K.P. Liu, “A survey of infeasible path detection,” in Proc. 7th Int. Conf. Eval. Novel Approaches Softw. Eng. (ENASE), 2012, pp. 43-52.
[15] S. Jang, H.-Y. Kim, Y.-H. Choi, and T.-M. Chung, “A study of advanced hybrid execution using reverse traversal,” in Proc. 2011 Int. Conf. Inf. Manag. Innov. Manag. Ind. Eng., vol. 2, 2011, pp. 557-559, doi: 10.1109/ICIII.2011.278.
[16] H. Ghorbani Moghadam, B. Jamasb, and H. Dehdashti Jahromi, “Review on security requirements in the software production process,” Soft Comput. J., vol. 10, no. 2, pp. 72-83, 2022, doi: 10.22052/scj.2022.242857.0 [In Persian]
[17] B. Barhoush and I. Alsmadi, “Infeasible paths detection using static analysis,” Res. Bull. Jordan ACM, vol. 2, no. 3, pp. 120-126, 2013.
[18] N. Malevris, D. Yates, and A. Veevers, “Predictive metric for likely feasibility of program paths,” Inf. Softw. Technol., vol. 32, no. 2, pp. 115-118, 1990, doi: 10.1016/0950-5849(90)90110-D.
[19] D. Yates and N. Malevris, “Reducing the effects of infeasible paths in branch testing,” ACM SIGSOFT Softw. Eng. Notes, vol. 14, no. 8, pp. 48-54, 1989, doi: 10.1145/75309.75315.
[20] SMT-LIB, Accessed: Feb. 6, 2022, [Online]. Available: https://smtlib.cs.uiowa.edu/.
[21] R.S. Sutton and A.G. Barto, Reinforcement Learning: An Introduction. London, U.K.: The MIT Press, 2018.
[22] E.J. Weyuker, “The applicability of program schema results to programs,” Int. J. Comput. Inf. Sci., vol. 8, no. 5, pp. 387-403, 1979, doi: 10.1007/BF00995175.
[23] D. Gong and X. Yao, “Automatic detection of infeasible paths in software testing,” IET Softw., vol. 4, no. 5, pp. 361-370, 2010, doi: 10.1049/iet-sen.2009.0092.
[24] D. Kundu, M. Sarma, and D. Samanta, “A UML model-based approach to detect infeasible paths,” J. Syst. Softw., vol. 107, pp. 71-92, 2015, doi: 10.1016/j.jss.2015.05.007.
[25] G. Brockman, V. Cheung, L. Pettersson, J. Schneider, J. Schulman, J. Tang and W. Zaremba, “OpenAI Gym,” arXiv preprint, arXiv:1606.01540, 2016.
[26] V. Mnih et al., “Human-level control through deep reinforcement learning,” Nature, vol. 518, pp. 529-533, 2015, doi: 10.1038/nature14236.
Soft Computing Journal
Volume 13, Issue 2 - Serial Number 26
February 2025
Pages 170-199

Files

History

  • Receive Date: 11 September 2023
  • Revise Date: 27 November 2023
  • Accept Date: 16 January 2024

Share

How to cite

Statistics