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

洪伟疆; 刘怡君; 陈振邦; 董威; 王戟

doi:10.1631/FITEE.1900213

Your Location：

Home >

Browse articles >

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

常规文章 | Updated：2022-05-19

- 面向MC/DC的符号执行编译优化
- Modified condition/decision coverage (MC/DC) oriented compiler optimization for symbolic execution
- 信息与电子工程前沿（英文） 2020年21卷第9期页码：1267-1284
- Affiliations：
  
  College of Computer, National University of Defense Technology, Changsha 410073, China
  State Key Laboratory of High Performance Computing, National University of Defense Technology, Changsha 410073, China
- Author bio：
  
  [ "", "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" ]
  [ "Wei DONG, E-mail: wdong@nudt.edu.cn" ]
  [ "", "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, E-mail: wj@nudt.edu.cn" ]
- Funds：
  
  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)
- DOI：10.1631/FITEE.1900213
  中图分类号： TP311.5
- 收稿：2019-04-26，
  
  修回：2020-;3-16，
  
  网络出版：2020-06-26，
  
  纸质出版：2020-09
- Accepted：
Scan QR Code
洪伟疆, 刘怡君, 陈振邦, 等. 面向MC/DC的符号执行编译优化[J]. 信息与电子工程前沿（英文）, 2020,21(9):1267-1284.

Wei-jiang HONG, Yi-jun LIU, Zhen-bang CHEN, et al. Modified condition/decision coverage (MC/DC) oriented compiler optimization for symbolic execution[J]. Frontiers of Information Technology & Electronic Engineering, 2020, 21(9): 1267-1284.
洪伟疆, 刘怡君, 陈振邦, 等. 面向MC/DC的符号执行编译优化[J]. 信息与电子工程前沿（英文）, 2020,21(9):1267-1284. DOI： 10.1631/FITEE.1900213.

Wei-jiang HONG, Yi-jun LIU, Zhen-bang CHEN, et al. Modified condition/decision coverage (MC/DC) oriented compiler optimization for symbolic execution[J]. Frontiers of Information Technology & Electronic Engineering, 2020, 21(9): 1267-1284. DOI： 10.1631/FITEE.1900213.

摘要

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

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.

关键词

Keywords

references

F Agakov , , , E Bonilla , , , J Cavazos , , , 等 . . Using machine learning to focus iterative optimization . . Proc Int Symp on Code Generation and Optimization , , 2006 . . p.295 - - 305 . . DOI: 10.1109/cgo.2006.37 http://doi.org/10.1109/cgo.2006.37 . .

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

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

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

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

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

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

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

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

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

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

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

TY Chen , , , SC Cheung , , , SM Yiu . . 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 , , 1998 . . .

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

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

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

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

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

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

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

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

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

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

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

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

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

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

P Godefroid , , , MY Levin , , , D Molnar , , , 等 . . Automated whitebox fuzz testing . . Proc Network and Distributed System Security Symp , , 2008 . . p.151 - - 166 . . . .

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

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

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

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

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

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

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

V Kuznetsov , , , J Kinder , , , S Bucur , , , 等 . . Efficient state merging in symbolic execution . . 33 rd ACM SIGPLAN Conf on Programming Language Design and Implementation , , 2012 . . p.193 - - 204 . . DOI: 10.1145/2345156.2254088 http://doi.org/10.1145/2345156.2254088 . .

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

Y Li , , , Z Su , , , L Wang , , , 等 . . Steering symbolic execution to less traveled paths . . ACM SIGPLAN Not , , 2013 . . 48 ( ( 10 ): ): 19 - - 32 . . DOI: 10.1145/2544173.2509553 http://doi.org/10.1145/2544173.2509553 . .

NP Lopes , , , D Menendez , , , S Nagarakatte , , , 等 . . Provably correct peephole optimizations with alive . . ACM SIGPLAN Not , , 2015 . . 50 ( ( 6 ): ): 22 - - 32 . . DOI: 10.1145/2813885.2737965 http://doi.org/10.1145/2813885.2737965 . .

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

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

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

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

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

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

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

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

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

N Tillmann , , , J de Halleux . . Pex-white box test generation for . . NET. Proc Int Conf on Tests and Proofs , , 2008 . . p.134 - - 153 . . http://www.wanfangdata.com.cn/details/detail.do?_type=perio&id=CC025270529 http://www.wanfangdata.com.cn/details/detail.do?_type=perio&id=CC025270529 , , . .

A Tiwari , , , C Chen , , , J Chame , , , 等 . . A scalable auto-tuning framework for compiler optimization . . Proc IEEE Int Symp on Parallel & Distributed Processing , , 2009 . . p.1 - - 12 . . DOI: 10.1109/ipdps.2009.5161054 http://doi.org/10.1109/ipdps.2009.5161054 . .

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

X Wang , , , J Sun , , , Z Chen , , , 等 . . Towards optimal concolic testing . . Proc 40 th Int Conf on Software Engineering , , 2018 . . p.291 - - 302 . . DOI: 10.1145/3180155.3180177 http://doi.org/10.1145/3180155.3180177 . .

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

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

H Yu , , , Z Chen , , , J Wang , , , 等 . . Symbolic verification of regular properties . . Proc 40 th Int Conf on Software Engineering , , 2018 . . p.871 - - 881 . . DOI: 10.1145/3180155.3180227 http://doi.org/10.1145/3180155.3180227 . .

Y Zhang , , , Z Chen , , , J Wang , , , 等 . . Regular property guided dynamic symbolic execution . . Proc 37 th IEEE Int Conf on Software Engineering , , 2015 . . p.643 - - 653 . . DOI: 10.1109/ICSE.2015.80 http://doi.org/10.1109/ICSE.2015.80 . .

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

浏览量

192

Downloads

CSCD

文章被引用时，请邮件提醒。

Submit

工具集

关联资源

暂无数据