Publishing Service

Polishing & Checking

Frontiers of Information Technology & Electronic Engineering

ISSN 2095-9184 (print), ISSN 2095-9230 (online)

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.

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

Chinese Summary  <27> 面向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);优化推荐;符号执行


Share this article to: More

Go to Contents

References:

<Show All>

Open peer comments: Debate/Discuss/Question/Opinion

<1>

Please provide your name, email address and a comment





DOI:

10.1631/FITEE.1900213

CLC number:

TP311.5

Download Full Text:

Click Here

Downloaded:

2525

Download summary:

<Click Here> 

Downloaded:

1424

Clicked:

4649

Cited:

0

On-line Access:

2020-09-09

Received:

2019-04-26

Revision Accepted:

2019-08-21

Crosschecked:

2020-03-16

Journal of Zhejiang University-SCIENCE, 38 Zheda Road, Hangzhou 310027, China
Tel: +86-571-87952276; Fax: +86-571-87952331; E-mail: jzus@zju.edu.cn
Copyright © 2000~ Journal of Zhejiang University-SCIENCE