Modified condition/decision coverage (MC/DC) oriented compiler optimization for symbolic execution

Abstract

Symbolic execution is an effective way of systematically exploring the search space of a program, and is often used for automatic software testing and bug finding. The program to be analyzed is usually compiled into a binary or an intermediate representation, on which symbolic execution is carried out. During this process, compiler optimizations influence the effectiveness and efficiency of symbolic execution. However, to the best of our knowledge, there exists no work on compiler optimization recommendation for symbolic execution with respect to (w.r.t.) modified condition/decision coverage (MC/DC), which is an important testing coverage criterion widely used for mission-critical software. This study describes our use of a state-of-the-art symbolic execution tool to carry out extensive experiments to study the impact of compiler optimizations on symbolic execution w.r.t. MC/DC. The results indicate that instruction combining (IC) optimization is the important and dominant optimization for symbolic execution w.r.t. MC/DC. We designed and implemented a support vector machine based optimization recommendation method w.r.t. IC (denoted as auto). The experiments on two standard benchmarks (Coreutils and NECLA) showed that auto achieves the best MC/DC on 67.47% of Coreutils programs and 78.26% of NECLA programs.

This is a preview of subscription content, log in to check access.

References

  1. Agakov F, Bonilla E, Cavazos J, et al., 2006. Using machine learning to focus iterative optimization. Proc Int Symp on Code Generation and Optimization, p.295–305. https://doi.org/10.1109/cgo.2006.37

  2. Aho AV, Sethi R, Ullman JD, 1986. Compilers: Principles, Techniques, and Tools. Addison-Wesley, Heidelberg, Berlin, Germany.

    Google Scholar 

  3. Ammann P, Offutt J, 2016. Introduction to Software Testing. Cambridge University Press, Cambridge, UK. https://doi.org/10.1017/9781316771273

    Google Scholar 

  4. Barr ET, Clark D, Harman M, et al., 2018. Indexing operators to extend the reach of symbolic execution. https://arxiv.org/abs/1806.10235

  5. Beizer B, 2003. Software Testing Techniques. Dreamtech Press, New Delhi, India.

    Google Scholar 

  6. Bucur S, Ureche V, Zamfir C, et al., 2011. Parallel symbolic execution for automated real-world software testing. Proc 6th Conf on Computer Systems, p.183–198. https://doi.org/10.1145/1966445.1966463

  7. Cadar C, 2015. Targeted program transformations for symbolic execution. Proc 10th Joint Meeting on Foundations of Software Engineering, p.906–909. https://doi.org/10.1145/2786805.2803205

  8. Cadar C, Dunbar D, Engler D, 2008. KLEE: unassisted and automatic generation of high-coverage tests for complex systems programs. Proc 8th USENIX Symp on Operating Systems Design and Implementation, p.209–224.

  9. Chang CC, Lin CJ, 2011. LIBSVM: a library for support vector machines. ACM Trans Intell Syst Technol, 2(3):27. https://doi.org/10.1145/1961189.1961199

    Article  Google Scholar 

  10. Chawla NV, 2005. Data mining for imbalanced datasets: an overview. In: Maimon O, Rokach L (Eds.), Data Mining and Knowledge Discovery. Springer, Boston, USA, p.853–867. https://doi.org/10.1007/0-387-25465-X_40

    Google Scholar 

  11. Chen JJ, Hu WX, Zhang LM, et al., 2018. Learning to accelerate symbolic execution via code transformation. Proc 32nd European Conf on Object-Oriented Programming, Article 6. https://doi.org/10.4230/LIPIcs.ECOOP.2018.6

  12. Chen S, Cowan CFN, Grant PM, 1991. Orthogonal least squares learning algorithm for radial basis function networks. IEEE Trans Neur Netw, 2(2):302–309. https://doi.org/10.1109/72.80341

    Article  Google Scholar 

  13. Chen TY, Cheung SC, Yiu SM, 1998. Metamorphic Testing: a New Approach for Generating Next Test Cases. Technical Report HKUST-CS98–01, Department of Computer Science, Hong Kong University of Science and Technology, Hong Kong, China.

    Google Scholar 

  14. Christakis M, Müller P, Wüstholz V, 2016. Guiding dynamic symbolic execution toward unverified program executions. Proc 38th Int Conf on Software Engineering, p.144–155. https://doi.org/10.1145/2884781.2884843

  15. Converse H, Olivo O, Khurshid S, 2017. Non-semantics-preserving transformations for higher-coverage test generation using symbolic execution. Proc IEEE Int Conf on Software Testing, Verification and Validation, p.241–252. https://doi.org/10.1109/icst.2017.29

  16. Cortes C, Vapnik V, 1995. Support-vector networks. Mach Learn, 20(3):273–297. https://doi.org/10.1007/BF00994018

    MATH  Google Scholar 

  17. Cui HM, Hu G, Wu JY, et al., 2013. Verifying systems rules using rule-directed symbolic execution. Proc 18th Int Conf on Architectural Support for Programming Languages and Operating Systems, p.329–342. https://doi.org/10.1145/2499368.2451152

  18. de Moura L, Bjørner N, 2008. Z3: an efficient SMT solver. Proc 14th Int Conf on Tools and Algorithms for the Construction and Analysis of Systems, p.337–340. https://doi.org/10.1007/978-3-540-78800-3_24

  19. de Moura L, Bjørner N, 2011. Satisfiability modulo theories: introduction and applications. Commun ACM, 54(9): 69–77. https://doi.org/10.1145/1995376.1995394

    Article  Google Scholar 

  20. Dong S, Olivo O, Zhang L, et al., 2015. Studying the influence of standard compiler optimizations on symbolic execution. Proc 26th Int Symp on Software Reliability Engineering, p.205–215. https://doi.org/10.1109/issre.2015.7381814

  21. Dupuy A, Leveson N, 2000. An empirical evaluation of the MC/DC coverage criterion on the HETE-2 satellite software. Proc 19th Digital Avionics Systems Conf, Article 1.B.6. https://doi.org/10.1109/DASC.2000.886883

  22. Duran JW, Ntafos SC, 1984. An evaluation of random testing. IEEE Trans Softw Eng, SE-10(4):438–444. https://doi.org/10.1109/tse.1984.5010257

    Article  Google Scholar 

  23. EUROCAE (European Organisation for Civil Aviation Equipment), 1998. Software Considerations in Airborne Systems and Equipment Certification, RTCA DO-178B. EUROCAE, Paris, France.

    Google Scholar 

  24. Fan WQ, Liang HL, Yang YX, et al., 2009. A novel symbolic execution framework for multi-procedure program analysis. Proc 2nd IEEE Int Conf on Broadband Network & Multimedia Technology, p.858–863. https://doi.org/10.1109/icbnmt.2009.5347802

  25. Fehnker A, Huuck R, Jayet P, et al., 2006. Goanna—a static model checker. Proc Int Workshop on Parallel and Distributed Methods in Verification, p.297–300. https://doi.org/10.1007/978-3-540-70952-7_20

  26. Fewster M, Graham D, 2000. Software Test Automation: Effective Use of Test Execution Tools. Emerald Group Publishing, Bingley, UK. https://doi.org/10.1108/k.2000.29.3.392.5

    Google Scholar 

  27. Godefroid P, Klarlund N, Sen K, 2005. DART: directed automated random testing. Proc ACM SIGPLAN Conf on Programming Language Design and Implementation, p.213–223. https://doi.org/10.1145/1065010.1065036

  28. Godefroid P, Levin MY, Molnar D, et al., 2008. Automated whitebox fuzz testing. Proc Network and Distributed System Security Symp, p.151–166.

  29. Hariri F, Shi A, Converse H, et al., 2016. Evaluating the effects of compiler optimizations on mutation testing at the compiler IR level. Proc 27th Int Symp on Software Reliability Engineering, p.105–115. https://doi.org/10.1109/issre.2016.51

  30. Hayhurst KJ, Veerhusen DS, 2001. A practical tutorial on modified condition/decision coverage. Proc 20th Digital Avionics Systems Conf, Article 1.B.2. https://doi.org/10.1109/dasc.2001.963305

  31. Jia Y, Harman M, 2011. An analysis and survey of the development of mutation testing. IEEE Trans Softw Eng, 37(5):649–678. https://doi.org/10.1109/tse.2010.62

    Article  Google Scholar 

  32. Jia XY, Ghezzi C, Ying S, 2015. Enhancing reuse of constraint solutions to improve symbolic execution. Proc Int Symp on Software Testing and Analysis, p.177–187. https://doi.org/10.1145/2771783.2771806

  33. Joshi HP, Dhanasekaran A, Dutta R, 2015. Impact of software obfuscation on susceptibility to return-oriented programming attacks. Proc 36th Sarnoff Symp, p.161–166. https://doi.org/10.1109/sarnof.2015.7324662

  34. Khurshid S, Päsäreanu CS, Visser W, 2003. Generalized symbolic execution for model checking and testing. Proc Int Conf Tools and Algorithms for the Construction and Analysis of Systems, p.553–568. https://doi.org/10.1007/3-540-36577-x_40

  35. King JC, 1976. Symbolic execution and program testing. Commun ACM, 19(7):385–394. https://doi.org/10.1145/360248.360252

    MathSciNet  Article  Google Scholar 

  36. Kuznetsov V, Kinder J, Bucur S, et al., 2012. Efficient state merging in symbolic execution. 33rd ACM SIGPLAN Conf on Programming Language Design and Implementation, p.193–204. https://doi.org/10.1145/2345156.2254088

  37. Lattner C, Adve VS, 2004. LLVM: a compilation framework for lifelong program analysis & transformation. Proc Int Symp on Code Generation and Optimization, p.75–88. https://doi.org/10.1109/cgo.2004.1281665

  38. Li Y, Su Z, Wang L, et al., 2013. Steering symbolic execution to less traveled paths. ACM SIGPLAN Not, 48(10):19–32. https://doi.org/10.1145/2544173.2509553

    Article  Google Scholar 

  39. Lopes NP, Menendez D, Nagarakatte S, et al., 2015. Provably correct peephole optimizations with alive. ACM SIGPLAN Not, 50(6):22–32. https://doi.org/10.1145/2813885.2737965

    Article  Google Scholar 

  40. Ma KK, Phang KY, Foster JS, et al., 2011. Directed symbolic execution. Proc Int Static Analysis Symp, p.95–111. https://doi.org/10.1007/978-3-642-23702-7_11

  41. McKeeman WM, 1998. Differential testing for software. Dig Techn J, 10(1):100–107.

    Google Scholar 

  42. Pan ZL, Eigenmann R, 2006. Fast and effective orchestration of compiler optimizations for automatic performance tuning. Proc Int Symp on Code Generation and Optimization, p.319–332. https://doi.org/10.1109/cgo.2006.38

  43. Perry DM, Mattavelli A, Zhang X, et al., 2017. Accelerating array constraints in symbolic execution. Proc 26th ACM SIGSOFT Int Symp on Software Testing and Analysis, p.68–78. https://doi.org/10.1145/3092703.3092728

  44. Sen K, Marinov D, Agha G, 2005. CUTE: a concolic unit testing engine for C. Proc 10th European Software Engineering Conf held jointly with 13th ACM SIGSOFT Int Symp on Foundations of Software Engineering, p.263–272. https://doi.org/10.21236/ada482657

  45. Sen K, Necula G, Gong L, et al., 2015. MultiSE: multi-path symbolic execution using value summaries. Proc 10th Joint Meeting on Foundations of Software Engineering, p.842–853. https://doi.org/10.1145/2786805.2786830

  46. Seo H, Kim S, 2014. How we get there: a context-guided search strategy in concolic testing. Proc 22nd ACM SIGSOFT Int Symp on Foundations of Software Engineering, p.413–424. https://doi.org/10.1145/2635868.2635872

  47. Staats M, Päsäreanu C, 2010. Parallel symbolic execution for structural test generation. Proc 19th Int Symp on Software Testing and Analysis, p.183–194. https://doi.org/10.1145/1831708.1831732

  48. Su T, Ke W, Miao W, et al., 2017. A survey on data-flow testing. ACM Comput Surv, 50(1):5. https://doi.org/10.1145/3020266

    Article  Google Scholar 

  49. Tillmann N, de Halleux J, 2008. Pex—white box test generation for. NET. Proc Int Conf on Tests and Proofs, p.134–153. https://doi.org/10.1007/978-3-540-79124-9_10

  50. Tiwari A, Chen C, Chame J, et al., 2009. A scalable autotuning framework for compiler optimization. Proc IEEE Int Symp on Parallel & Distributed Processing, p.1–12. https://doi.org/10.1109/ipdps.2009.5161054

  51. Wagner J, Kuznetsov V, Candea G, 2013. -OVERIFY: optimizing programs for fast verification. 14th USENIX Conf on Hot Topics in Operating Systems, p.1–6.

  52. Wang X, Sun J, Chen Z, et al., 2018. Towards optimal concolic testing. Proc 40th Int Conf on Software Engineering, p.291–302. https://doi.org/10.1145/3180155.3180177

  53. Wong E, Zhang L, Wang S, et al., 2015. DASE: document-assisted symbolic execution for improving automated software testing. Proc 37th IEEE Int Conf on Software Engineering, p.620–631. https://doi.org/10.1109/icse.2015.78

  54. Wong WE, 2001. Mutation Testing for the New Century. Springer, Boston, USA. https://doi.org/10.1007/978-1-4757-5939-6

    Google Scholar 

  55. Yu H, Chen Z, Wang J, et al., 2018. Symbolic verification of regular properties. Proc 40th Int Conf on Software Engineering, p.871–881. https://doi.org/10.1145/3180155.3180227

  56. Zhang Y, Chen Z, Wang J, et al., 2015. Regular property guided dynamic symbolic execution. Proc 37th IEEE Int Conf on Software Engineering, p.643–653. https://doi.org/10.1109/ICSE.2015.80

  57. Zhu H, Hall PA, May JH, 1997. Software unit test coverage and adequacy. ACM Comput Surv, 29(4):366–427. https://doi.org/10.1145/267580.267590

    Article  Google Scholar 

Download references

Acknowledgements

We thank Jun-jie CHEN and Dan HAO with Peking University for supporting the empirical comparison with LEO.

Author information

Affiliations

Authors

Contributions

Wei-jiang HONG and Yi-jun LIU designed the research. Zhen-bang CHEN guided the research. Wei-jiang HONG and Zhen-bang CHEN drafted the manuscript. Wei DONG helped organize the manuscript. Ji WANG polished the paper. Wei-jiang HONG and Zhen-bang CHEN finalized the paper.

Corresponding author

Correspondence to Zhen-bang Chen.

Additional information

Compliance with ethics guidelines

Wei-jiang HONG, Yi-jun LIU, Zhen-bang CHEN, Wei DONG, and Ji WANG declare that they have no conflict of interest.

Project supported by the National Key R&D Program of China (No. 2017YFB1001802) and the National Natural Science Foundation of China (Nos. 61472440, 61632015, 61690203, and 61532007)

Zhen-bang CHEN received his BS degree and PhD degree in Computer Science in 2002 and 2009, respectively, from the College of Computer, National University of Defense Technology, Changsha, China. He is now an associate professor at the College of Computer, National University of Defense Technology, China. His research interests include program analysis, formal methods, and their applications.

Ji WANG received his BS degree and PhD degree in Computer Science in 1987 and 1995, respectively, from the College of Computer, National University of Defense Technology, Changsha, China. He is now a full professor at the State Key Laboratory of High Performance Computing, National University of Defense Technology, China. He is an executive associate editor-in-chief of Frontiers of Information Technology & Electronic Engineering. His research interests include formal methods and software engineering.

Rights and permissions

Reprints and Permissions

About this article

Verify currency and authenticity via CrossMark

Cite this article

Hong, W., Liu, Y., Chen, Z. et al. Modified condition/decision coverage (MC/DC) oriented compiler optimization for symbolic execution. Front Inform Technol Electron Eng (2020). https://doi.org/10.1631/FITEE.1900213

Download citation

Key words

  • Compiler optimization
  • Modified condition/decision coverage (MC/DC)
  • Optimization recommendation
  • Symbolic execution

CLC number

  • TP311.5