Skip to main content
Log in

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

  • Published:
Frontiers of Information Technology & Electronic Engineering Aims and scope Submit manuscript

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 via an institution to check access.

Access this article

Price excludes VAT (USA)
Tax calculation will be finalised during checkout.

Instant access to the full article PDF.

Institutional subscriptions

Similar content being viewed by others

References

Download references

Acknowledgements

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

Author information

Authors and Affiliations

Authors

Corresponding author

Correspondence to Zhen-bang Chen.

Additional information

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)

Contributors

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.

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.

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

Check for updates. Verify currency and authenticity via CrossMark

Cite this article

Hong, Wj., Liu, Yj., Chen, Zb. et al. Modified condition/decision coverage (MC/DC) oriented compiler optimization for symbolic execution. Front Inform Technol Electron Eng 21, 1267–1284 (2020). https://doi.org/10.1631/FITEE.1900213

Download citation

  • Received:

  • Accepted:

  • Published:

  • Issue Date:

  • DOI: https://doi.org/10.1631/FITEE.1900213

Key words

CLC number

Navigation