Full Text:   <1395>

Summary:  <1133>

CLC number: TP311.5

On-line Access: 2020-09-09

Received: 2019-04-26

Revision Accepted: 2019-08-21

Crosschecked: 2020-03-16

Cited: 0

Clicked: 2946

Citations:  Bibtex RefMan EndNote GB/T7714

 ORCID:

Wei-jiang Hong

https://orcid.org/0000-0002-7092-3658

Zhen-bang Chen

https://orcid.org/0000-0003-0874-3231

-   Go to

Article info.
Open peer comments

Frontiers of Information Technology & Electronic Engineering  2020 Vol.21 No.9 P.1267-1284

http://doi.org/10.1631/FITEE.1900213


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


Author(s):  Wei-jiang Hong, Yi-jun Liu, Zhen-bang Chen, Wei Dong, Ji Wang

Affiliation(s):  College of Computer, National University of Defense Technology, Changsha 410073, China; more

Corresponding email(s):   zbchen@nudt.edu.cn, wdong@nudt.edu.cn, wj@nudt.edu.cn

Key Words:  Compiler optimization, Modified condition/decision coverage (MC/DC), Optimization recommendation, Symbolic execution


Share this article to: More |Next Article >>>

Wei-jiang Hong, Yi-jun Liu, Zhen-bang Chen, Wei Dong, Ji Wang. Modified condition/decision coverage (MC/DC) oriented compiler optimization for symbolic execution[J]. Frontiers of Information Technology & Electronic Engineering, 2020, 21(9): 1267-1284.

@article{title="Modified condition/decision coverage (MC/DC) oriented compiler optimization for symbolic execution",
author="Wei-jiang Hong, Yi-jun Liu, Zhen-bang Chen, Wei Dong, Ji Wang",
journal="Frontiers of Information Technology & Electronic Engineering",
volume="21",
number="9",
pages="1267-1284",
year="2020",
publisher="Zhejiang University Press & Springer",
doi="10.1631/FITEE.1900213"
}

%0 Journal Article
%T Modified condition/decision coverage (MC/DC) oriented compiler optimization for symbolic execution
%A Wei-jiang Hong
%A Yi-jun Liu
%A Zhen-bang Chen
%A Wei Dong
%A Ji Wang
%J Frontiers of Information Technology & Electronic Engineering
%V 21
%N 9
%P 1267-1284
%@ 2095-9184
%D 2020
%I Zhejiang University Press & Springer
%DOI 10.1631/FITEE.1900213

TY - JOUR
T1 - Modified condition/decision coverage (MC/DC) oriented compiler optimization for symbolic execution
A1 - Wei-jiang Hong
A1 - Yi-jun Liu
A1 - Zhen-bang Chen
A1 - Wei Dong
A1 - Ji Wang
J0 - Frontiers of Information Technology & Electronic Engineering
VL - 21
IS - 9
SP - 1267
EP - 1284
%@ 2095-9184
Y1 - 2020
PB - Zhejiang University Press & Springer
ER -
DOI - 10.1631/FITEE.1900213


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.

面向MC/DC的符号执行编译优化

洪伟疆1,2,刘怡君1,陈振邦1,董威1,王戟1,2
1国防科技大学计算机学院,中国长沙市,410073
2国防科技大学高性能计算国家重点实验室,中国长沙市,410073

摘要:符号执行是一种系统地探索程序路径空间的有效方式,常用于自动软件测试与错误查找。通常待分析的程序会被编译成二进制或中间表示,在此基础上进行符号执行。在此过程中,编译器的优化选项往往会影响符号执行的有效性和效率。修订条件/判定覆盖(MC/DC)是一种广泛应用于任务关键型软件的重要测试覆盖准则;据我们所知,目前尚未开展面向MC/DC的符号执行编译优化推荐工作。本文采用先进的符号执行工具开展了大量实验,研究编译器优化对使用符号执行以满足程序MC/DC的影响。结果表明,指令组合(IC)优化是符号执行面向MC/DC的关键和主导优化选项。在此基础上,设计并实现了一个基于支持向量机的编译优化推荐方法,在Coreutils和NECLA两个测试集上开展实验。结果表明,所提方法在67.47%的Coreutils程序和78.26%的NECLA程序上取得了最佳MC/DC结果。

关键词:编译优化;修订条件/判定覆盖(MC/DC);优化推荐;符号执行

Darkslateblue:Affiliate; Royal Blue:Author; Turquoise:Article

Reference

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

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

[3]Ammann P, Offutt J, 2016. Introduction to Software Testing. Cambridge University Press, Cambridge, UK.

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

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

[7]Cadar C, 2015. Targeted program transformations for symbolic execution. Proc 10th Joint Meeting on Foundations of Software Engineering, p.906-909.

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

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

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

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

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

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

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

[16]Cortes C, Vapnik V, 1995. Support-vector networks. Mach Learn, 20(3):273-297.

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

[18]de Moura L, Bjorner 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.

[19]de Moura L, Bjorner N, 2011. Satisfiability modulo theories: introduction and applications. Commun ACM, 54(9):69-77.

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

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

[22]Duran JW, Ntafos SC, 1984. An evaluation of random testing. IEEE Trans Softw Eng, SE-10(4):438-444.

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

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

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

[26]Fewster M, Graham D, 2000. Software Test Automation: Effective Use of Test Execution Tools. Emerald Group Publishing, Bingley, UK.

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

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

[30]Hayhurst KJ, Veerhusen DS, 2001. A practical tutorial on modified condition/decision coverage. Proc 20th Digital Avionics Systems Conf, Article 1.B.2.

[31]Jia Y, Harman M, 2011. An analysis and survey of the development of mutation testing. IEEE Trans Softw Eng, 37(5):649-678.

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

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

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

[35]King JC, 1976. Symbolic execution and program testing. Commun ACM, 19(7):385-394.

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

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

[38]Li Y, Su Z, Wang L, et al., 2013. Steering symbolic execution to less traveled paths. ACM SIGPLAN Not, 48(10):19-32.

[39]Lopes NP, Menendez D, Nagarakatte S, et al., 2015. Provably correct peephole optimizations with alive. ACM SIGPLAN Not, 50(6):22-32.

[40]Ma KK, Phang KY, Foster JS, et al., 2011. Directed symbolic execution. Proc Int Static Analysis Symp, p.95-111.

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

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

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

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

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

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

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

[48]Su T, Ke W, Miao W, et al., 2017. A survey on data-flow testing. ACM Comput Surv, 50(1):5.

[49]Tillmann N, de Halleux J, 2008. Pex—white box test generation for .NET. Proc Int Conf on Tests and Proofs, p.134-153.

[50]Tiwari A, Chen C, Chame J, et al., 2009. A scalable auto-tuning framework for compiler optimization. Proc IEEE Int Symp on Parallel & Distributed Processing, p.1-12.

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

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

[54]Wong WE, 2001. Mutation Testing for the New Century. Springer, Boston, USA.

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

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

[57]Zhu H, Hall PA, May JH, 1997. Software unit test coverage and adequacy. ACM Comput Surv, 29(4):366-427.

Open peer comments: Debate/Discuss/Question/Opinion

<1>

Please provide your name, email address and a comment





Journal of Zhejiang University-SCIENCE, 38 Zheda Road, Hangzhou 310027, China
Tel: +86-571-87952783; E-mail: cjzhang@zju.edu.cn
Copyright © 2000 - 2022 Journal of Zhejiang University-SCIENCE