电子学报 ›› 2017, Vol. 45 ›› Issue (11): 2582-2592.DOI: 10.3969/j.issn.0372-2112.2017.11.003

• 学术论文 • 上一篇    下一篇

一种符号执行制导的循环内界分析方法

赵祖威1,2, 冯世宁3,4, 汤恩义1,2, 陈鑫1, 李宣东1,2, 潘敏学1,2, 赵晨1,2   

  1. 1. 南京大学软件新技术国家重点实验室, 江苏南京 210023;
    2. 南京大学软件学院, 江苏南京 210093;
    3. 南瑞集团公司(国网电力科学研究院), 江苏南京 211106;
    4. 国电南瑞科技股份有限公司, 江苏南京 211106
  • 收稿日期:2016-07-25 修回日期:2016-12-16 出版日期:2017-11-25
    • 通讯作者:
    • 汤恩义
    • 作者简介:
    • 赵祖威,男,1992年10月出生,江苏南通人.2015年本科毕业于南京大学软件学院.现为南京大学软件学院硕士研究生,主要研究方向为静态程序分析,软件测试;冯世宁,女,1986年11月出生,江苏南京人.2008年、2011年分别在东南大学、国网电力科学研究院获学士、硕士学位.现为南瑞集团(国网电力科学研究院)工程师,从事系统仿真,电力电子自动化等领域的研究.
    • 基金资助:
    • 国家自然科学基金 (No.61402222,No.61632015); 国家重点研发计划 (No.2016YFB1000802); 教育部高等学校博士学科点专项科研基金 (No.20110091120058); 江苏省产学研项目 (No.BY2014126-03)

A Symbolic Execution Guided Inner Loop Bound Analysis

ZHAO Zu-wei1,2, FENG Shi-ning3,4, TANG En-yi1,2, CHEN Xin1, LI Xuan-dong1,2, PAN Min-xue1,2, ZHAO Chen1,2   

  1. 1. State Key Laboratory for Novel Software Technology, Nanjing University, Nanjing, Jiangsu 210023, China;
    2. Software Institute, Nanjing University, Nanjing, Jiangsu 210093, China;
    3. NARI Group Corporation(State Grid Electric Power Research Institute), Nanjing, Jiangsu 211106, China;
    4. NARI Technology Co., Ltd., Nanjing, Jiangsu 211106
  • Received:2016-07-25 Revised:2016-12-16 Online:2017-11-25 Published:2017-11-25
    • Supported by:
    • National Natural Science Foundation of China (No.61402222, No.61632015); National Key Research and Development Program of China (No.2016YFB1000802); Research Fund for the Doctoral Program of Higher Education of Ministry of Education of China (No.20110091120058); Industry-University-research Project of Jiangsu Province (No.BY2014126-03)

摘要: 循环是计算机中重要的复杂程序结构.很多应用场景要求静态分析循环可能达到的最大迭代次数,即循环边界(Loop Bound).对应技术在文献中被称为循环边界分析(Loop Bound Analysis).现有的循环边界分析均使用保守方式进行外界分析,即产生略高于循环边界的近似值.基于这一现状,本文提出了一种自动地循环内界分析方法,产生略低于循环边界的近似值.当用户综合利用外界与内界分析,能将循环边界值约束到一个统计区间,从而能对分析结果获得更为完整的认识.本文基于循环条件制导的符号执行(Symbolic Execution)技术实现了循环内界分析,该技术的本质在于它能够利用符号执行符号化推导程序执行约束的特点,准确求解循环在程序所有合法输入条件下的边界值,并由生成的测试用例来保证该边界值一定可达(即保证是循环内界).本文对符号执行制导技术进行了优化,并在多组已有研究采用的基准用例集上进行了实例评估,实验结果表明,本文的循环内界分析方法具备准确性和高效性,可以满足应用需求.

关键词: 循环边界分析, 符号执行, 软件测试

Abstract: Loop is an important program structure in computer.Many applications need to estimate the maximum iteration number of loops in programs by loop bound analysis.Existing loop bound analysis uses conservative methods to derive outer loop bounds,which estimates the bounds higher than the real ones.In this paper,we propose an automatic inner bound analysis,which generates bounds slightly lower than the real ones.When users combine the inner bound analysis with traditional outer bound analysis,they can restrict every real loop bound in an interval and get more information about the loops.We implement the inner bound analysis by a scope-condition guided symbolic execution.The insight of our technique is that when symbolic execution substitutes program inputs by symbols in its derivation,it generates loop bounds for all valid inputs and generates corresponding test cases that make the inner bounds feasible.We optimize the technique and evaluate it on several benchmarks.The results show that the analysis is precise and efficient.

Key words: loop bound analysis, symbolic execution, software testing

中图分类号: