推荐星级：

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

更新时间：2019-12-24 16:52:48 大小：1M 上传用户：zhiyao6 查看TA发布的资源 标签：循环内界分析 下载积分：1分评价赚积分（如何评价?）打赏收藏评论(0) 举报

资料介绍

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

部分文件列表

文件名	大小
一种符号执行制导的循环内界分析方法.pdf	1M

立即下载

【关注视频号领20积分】【关注公众号立即送20积分】

部分页面预览

（完整内容请下载后查看）

第１１期

电ꢀ

ꢀ

子ꢀ

ꢀ

学ꢀ

ꢀ

报

Ｖｏｌ．４５ꢀ Ｎｏ．１１

Ｎｏｖ．ꢀ ２０１７

２０１７年１１月

ＡＣＴＡＥＬＥＣＴＲＯＮＩＣＡＳＩＮＩＣＡ

一种符号执行制导的

循环内界分析方法

赵祖威^１，２，冯世宁^３，４，汤恩义^１，２，陈ꢀ 鑫^１，李宣东^１，２，潘敏学^１，２，赵ꢀ 晨^１，２

（１．南京大学软件新技术国家重点实验室，江苏南京２１００２３；２．南京大学软件学院，江苏南京２１００９３；

３．南瑞集团公司（国网电力科学研究院），江苏南京２１１１０６；４．国电南瑞科技股份有限公司，江苏南京２１１１０６）

ꢀ ꢀ 摘ꢀ 要：ꢀ 循环是计算机中重要的复杂程序结构．很多应用场景要求静态分析循环可能达到的最大迭代次数，即

循环边界（ＬｏｏｐＢｏｕｎｄ）．对应技术在文献中被称为循环边界分析（ＬｏｏｐＢｏｕｎｄＡｎａｌｙｓｉｓ）．现有的循环边界分析均使用保

守方式进行外界分析，即产生略高于循环边界的近似值．基于这一现状，本文提出了一种自动地循环内界分析方法，产

生略低于循环边界的近似值．当用户综合利用外界与内界分析，能将循环边界值约束到一个统计区间，从而能对分析

结果获得更为完整的认识．本文基于循环条件制导的符号执行（ＳｙｍｂｏｌｉｃＥｘｅｃｕｔｉｏｎ）技术实现了循环内界分析，该技术

的本质在于它能够利用符号执行符号化推导程序执行约束的特点，准确求解循环在程序所有合法输入条件下的边界

值，并由生成的测试用例来保证该边界值一定可达（即保证是循环内界）．本文对符号执行制导技术进行了优化，并在

多组已有研究采用的基准用例集上进行了实例评估，实验结果表明，本文的循环内界分析方法具备准确性和高效性，

可以满足应用需求．

关键词： ꢀ 循环边界分析；符号执行；软件测试

中图分类号： ꢀ ＴＰ３１１ư ５ꢀ ꢀ ꢀ 文献标识码： ꢀ Ａꢀ ꢀ ꢀ 文章编号： ꢀ ０３７２⁃２１１２（２０１７）１１⁃２５８２⁃１１

电子学报ＵＲＬ：ｈｔｔｐ：／／ｗｗｗ．ｅｊｏｕｒｎａｌ．ｏｒｇ．ｃｎꢀ

ＤＯＩ：１０．３９６９／ｊ．ｉｓｓｎ．０３７２⁃２１１２．２０１７．１１．００３

ＡＳｙｍｂｏｌｉｃＥｘｅｃｕｔｉｏｎＧｕｉｄｅｄＩｎｎｅｒ

ＬｏｏｐＢｏｕｎｄＡｎａｌｙｓｉｓ

ＺＨＡＯＺｕ⁃ｗｅｉ^１，２，ＦＥＮＧＳｈｉ⁃ｎｉｎｇ^３，４，ＴＡＮＧＥｎ⁃ｙｉ^１，２

，

ＣＨＥＮＸｉｎ^１，ＬＩＸｕａｎ⁃ｄｏｎｇ^１，２，ＰＡＮＭｉｎ⁃ｘｕｅ^１，２，ＺＨＡＯＣｈｅｎ^１，２

（１．ＳｔａｔｅＫｅｙＬａｂｏｒａｔｏｒｙｆｏｒＮｏｖｅｌＳｏｆｔｗａｒｅＴｅｃｈｎｏｌｏｇｙ，ＮａｎｊｉｎｇＵｎｉｖｅｒｓｉｔｙ，Ｎａｎｊｉｎｇ，Ｊｉａｎｇｓｕ２１００２３，Ｃｈｉｎａ；

２．ＳｏｆｔｗａｒｅＩｎｓｔｉｔｕｔｅ，ＮａｎｊｉｎｇＵｎｉｖｅｒｓｉｔｙ，Ｎａｎｊｉｎｇ，Ｊｉａｎｇｓｕ２１００９３，Ｃｈｉｎａ；

３．ＮＡＲＩＧｒｏｕｐＣｏｒｐｏｒａｔｉｏｎ（ＳｔａｔｅＧｒｉｄＥｌｅｃｔｒｉｃＰｏｗｅｒＲｅｓｅａｒｃｈＩｎｓｔｉｔｕｔｅ），Ｎａｎｊｉｎｇ，Ｊｉａｎｇｓｕ２１１１０６，Ｃｈｉｎａ；

４．ＮＡＲＩＴｅｃｈｎｏｌｏｇｙＣｏ．，Ｌｔｄ．，Ｎａｎｊｉｎｇ，Ｊｉａｎｇｓｕ２１１１０６）

Ａｂｓｔｒａｃｔ：ꢀ Ｌｏｏｐｉｓａｎｉｍｐｏｒｔａｎｔｐｒｏｇｒａｍｓｔｒｕｃｔｕｒｅｉｎｃｏｍｐｕｔｅｒ．Ｍａｎｙａｐｐｌｉｃａｔｉｏｎｓｎｅｅｄｔｏｅｓｔｉｍａｔｅｔｈｅｍａｘｉｍｕｍｉｔｅｒ⁃

ａｔｉｏｎｎｕｍｂｅｒｏｆｌｏｏｐｓｉｎｐｒｏｇｒａｍｓｂｙｌｏｏｐｂｏｕｎｄａｎａｌｙｓｉｓ．Ｅｘｉｓｔｉｎｇｌｏｏｐｂｏｕｎｄａｎａｌｙｓｉｓｕｓｅｓｃｏｎｓｅｒｖａｔｉｖｅｍｅｔｈｏｄｓｔｏｄｅｒｉｖｅ

ｏｕｔｅｒｌｏｏｐｂｏｕｎｄｓ，ｗｈｉｃｈｅｓｔｉｍａｔｅｓｔｈｅｂｏｕｎｄｓｈｉｇｈｅｒｔｈａｎｔｈｅｒｅａｌｏｎｅｓ．Ｉｎｔｈｉｓｐａｐｅｒ，ｗｅｐｒｏｐｏｓｅａｎａｕｔｏｍａｔｉｃｉｎｎｅｒｂｏｕｎｄ

ａｎａｌｙｓｉｓ，ｗｈｉｃｈｇｅｎｅｒａｔｅｓｂｏｕｎｄｓｓｌｉｇｈｔｌｙｌｏｗｅｒｔｈａｎｔｈｅｒｅａｌｏｎｅｓ．Ｗｈｅｎｕｓｅｒｓｃｏｍｂｉｎｅｔｈｅｉｎｎｅｒｂｏｕｎｄａｎａｌｙｓｉｓｗｉｔｈｔｒａｄｉ⁃

ｔｉｏｎａｌｏｕｔｅｒｂｏｕｎｄａｎａｌｙｓｉｓ，ｔｈｅｙｃａｎｒｅｓｔｒｉｃｔｅｖｅｒｙｒｅａｌｌｏｏｐｂｏｕｎｄｉｎａｎｉｎｔｅｒｖａｌａｎｄｇｅｔｍｏｒｅｉｎｆｏｒｍａｔｉｏｎａｂｏｕｔｔｈｅｌｏｏｐｓ．

Ｗｅｉｍｐｌｅｍｅｎｔｔｈｅｉｎｎｅｒｂｏｕｎｄａｎａｌｙｓｉｓｂｙａｓｃｏｐｅ⁃ｃｏｎｄｉｔｉｏｎｇｕｉｄｅｄｓｙｍｂｏｌｉｃｅｘｅｃｕｔｉｏｎ．Ｔｈｅｉｎｓｉｇｈｔｏｆｏｕｒｔｅｃｈｎｉｑｕｅｉｓｔｈａｔ

ｗｈｅｎｓｙｍｂｏｌｉｃｅｘｅｃｕｔｉｏｎｓｕｂｓｔｉｔｕｔｅｓｐｒｏｇｒａｍｉｎｐｕｔｓｂｙｓｙｍｂｏｌｓｉｎｉｔｓｄｅｒｉｖａｔｉｏｎ，ｉｔｇｅｎｅｒａｔｅｓｌｏｏｐｂｏｕｎｄｓｆｏｒａｌｌｖａｌｉｄｉｎｐｕｔｓ

ａｎｄｇｅｎｅｒａｔｅｓｃｏｒｒｅｓｐｏｎｄｉｎｇｔｅｓｔｃａｓｅｓｔｈａｔｍａｋｅｔｈｅｉｎｎｅｒｂｏｕｎｄｓｆｅａｓｉｂｌｅ．Ｗｅｏｐｔｉｍｉｚｅｔｈｅｔｅｃｈｎｉｑｕｅａｎｄｅｖａｌｕａｔｅｉｔｏｎｓｅｖ⁃

ｅｒａｌｂｅｎｃｈｍａｒｋｓ．Ｔｈｅｒｅｓｕｌｔｓｓｈｏｗｔｈａｔｔｈｅａｎａｌｙｓｉｓｉｓｐｒｅｃｉｓｅａｎｄｅｆｆｉｃｉｅｎｔ．

Ｋｅｙｗｏｒｄｓ：ꢀ ｌｏｏｐｂｏｕｎｄａｎａｌｙｓｉｓ；ｓｙｍｂｏｌｉｃｅｘｅｃｕｔｉｏｎ；ｓｏｆｔｗａｒｅｔｅｓｔｉｎｇ

收稿日期：２０１６⁃０７⁃２５；修回日期：２０１６⁃１２⁃１６；责任编辑：马兰英

基金项目：国家自然科学基金（Ｎｏ．６１４０２２２２，Ｎｏ．６１６３２０１５）；国家重点研发计划（Ｎｏ．２０１６ＹＦＢ１０００８０２）；教育部高等学校博士学科点专项科研基

金（Ｎｏ．２０１１００９１１２００５８）；江苏省产学研项目（Ｎｏ．ＢＹ２０１４１２６⁃０３）

第ꢀ １１ꢀ 期

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

２５８３

程序输入定义成可代表任意值的符号，并沿程序的控

制流推导各中间变量的关系性质．当程序中存在多条路

径时，符号执行会创建多个执行状态来追踪各路径下

的变量关系，并记录各路径的条件约束．最终，利用约束

求解器（ＣｏｎｓｔｒａｉｎｔＳｏｌｖｅｒ）来获得覆盖特定路径的测试

输入．本文通过制导符号执行过程使其能够高效地推导

各循环达到最大迭代目标路径的约束条件，从而实现

循环内界的自动分析．同样，我们也能生成该约束条件

对应的测试用例，以覆盖循环的最大迭代路径，供进一

步分析与测试．

本文基于开源符号执行平台ＫＬＥＥ^［９］实现了自动

循环内界分析，并在多组已有研究采用的基准用例集

上进行了实例评估．实验结果显示本文的循环内界分析

方法是准确和高效的，能满足大多数的应用需求．

１ꢀ 引言

ꢀ ꢀ 循环是计算机中重要的复杂程序结构．许多应用场

景要求静态分析循环可能达到的最大迭代次数，文献

中称之为循环边界（ＬｏｏｐＢｏｕｎｄ），而对应的计算方法被

称为循环边界分析（ＬｏｏｐＢｏｕｎｄＡｎａｌｙｓｉｓ）^{［１～３］}．循环边界

的使用场景有：在程序优化中作为各代码段对全局性

能影响的依据；在程序影响分析中用于进一步分析循

环中代码的影响范围；在实时系统分析中用于估测系

统各任务的最坏情况执行时间；检测触发条件较为苛

刻、需要深入循环才会发生的软件缺陷等等．

现有的循环边界分析方法均为外界分析^{［１，４］}，这些

方法采用较保守的策略，在不能准确分析时保证分析

值一定大于实际循环边界值，因此我们称这样的分析

值为循环外界（ＯｕｔｅｒＢｏｕｎｄ）．这类外界分析方法特别适

用于保证实时任务安全性的分析场景，即保证实时系

统中循环的实际最大迭代次数一定不超出分析值．然

而，外界分析方法并不能测算当前的分析值离实际的

边界值有多远，当外界分析方法不够准确时，会因为系

统预留了过多的计算资源而造成浪费^{［２～４］}．基于这一现

状，本文提出一种循环内界的自动分析方法（Ｉｎｎｅｒ

ＢｏｕｎｄＡｎａｌｙｓｉｓ）．该方法尽可能准确地获得循环实际能

达到的边界值，即注重边界值的可达性．在不能准确分

析循环边界的条件下，内界分析得到略小于实际边界

的分析值．该方法的意义在于，当用户综合利用外界分

析和内界分析时，可以获得实际边界的范围区间，从而

对分析结果有更为完整的认识．例如，用户可以明确某

循环边界的具体范围介于内界４９５和外界５１１之间，并

获得该循环达到４９５次迭代的测试用例．

２ꢀ 符号执行

ꢀ ꢀ 符号执行（ＳｙｍｂｏｌｉｃＥｘｅｃｕｔｉｏｎ）是一项近年来广受

关注的^{［７～１４］}软件测试自动生成技术，它的基本思想是：

将程序输入定义成表示任意值的符号，并由此推导程

序各中间数据和执行结果．因此，各变量值在符号执行

中均被表示成了输入符号的表达式．符号执行通过创建

执行状态来记录程序中不同执行路径下各变量的符号

表达式．当符号推导遇到一个条件分支时，符号执行平

台会从当前执行状态中复制出一个新的执行状态，并

在新状态中记录条件为假的分支条件约束，而当前的

执行状态会被记录为条件为真的分支条件约束而继续

推导．最终当某一执行状态的推导到达程序出口时，符

号执行平台通过约束求解器求解当前状态的总条件约

束，并生成覆盖对应路径的测试用例．本节通过一个具

体的例子来说明这一过程，如图１所示．

本文基于循环条件制导的符号执行（ＳｙｍｂｏｌｉｃＥｘｅ⁃

ｃｕｔｉｏｎ）技术来实现循环内界分析．符号执行技术^{［５～８］}

将

ꢀ ꢀ 图１（ａ）给出了一段带循环的示例程序，它的控制

流（ＣｏｎｔｒｏｌＦｌｏｗ）如图１（ｂ）所示．在图１（ａ）中ｍａｉｎ函

数的入口处，符号执行平台将输入变量ｘ和ｙ表示为可

代表任意值的符号，并建立符号执行的第一个执行状

态ｓ_０．符号执行中每个执行状态ｓ由５个信息域（ｐｃ，ｃｖ，

ｓｖ，ｅｘ，ｃ）组成，具体包括：（１）程序计数器ｓư ｐｃ，记录了

执行状态ｓ的当前执行位置；（２）所有非符号变量的具

体值ｓư ｃｖ，记录了各具体变量到值的映射，例如图１（ａ）

中变量ｎ被赋值为５；（３）程序中的符号值ｓư ｓｖ，记录了

符号变量到符号表达式的映射，例如示例程序中的变

量ｘ和ｙ在程序入口处被初始化，映射为表示任意值的

符号；（４）符号操作表达式ｓư ｅｘ，记录程序中符号变量

间的关系；（５）当前路径的符号约束ｓư ｃ，记录覆盖当前

路径须满足的条件，例如示例程序中的ｘ＜ｎ．对于每一

个执行状态ｓ，符号执行由ｓư ｐｃ获得该状态的下一条指

令，并由该指令推导更新ｓ中其它各信息域的值．Ｋｉｎｇ

等人的工作^［６］定义了这一推导过程，在本文中，我们将其

封装为ｓ的成员函数ｓư ｓｙｍｂｏｌｉｃＥｘｅｃｕｔｉｏｎ（），它的返回值

为经过当前指令更新的状态集．特别地，当ｓ在推导过

程中遇到条件分支（例如ｉｆｂｔｈｅｎＳｅｌｓｅＳ’）时，它会产

生含有不同路径约束的新状态，返回状态集｛ｓ_ｔ，ｓ_ｆ｝．这

里状态ｓ_ｔ和ｓ_ｆ分别记录了ｔｒｕｅ分支和ｆａｌｓｅ分支对应的

执行状态，即ｓ ư ｃｓư ｃ∧ｂ和ｓ ư ｃｓư ｃ∧┐ｂ，而ｓ和ｓ

←

ｔ

ｆ

ｔ

ｆ

中的其他信息皆从原状态ｓ中拷贝．为节省内存，本文方

法将状态ｓ_ｔ各信息域直接更新到原状态ｓ里而仅新建状

态ｓ_ｆ，我们也称新建的状态为ｓ’，从而把这一过程定义为

｛ｓ，ｓ’｝ｓư ｆｏｒｋＥｘｅｃｕｔｉｏｎ（）．因此，仅当符号执行遇到条件

←

分支时执行状态的数量才会增加．

全部评论(0)

暂无评论

评论赚积分>>

上传资源上传优质资源有赏金

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

资料介绍

部分文件列表

部分页面预览

相关下载

全部评论(0)

热门标签

最新上传

热门下载

推荐下载

专栏首页