基于变量符号关联分析的程序状态优化方法

doi:10.11959/j.issn.1000-436x.2018094

通信学报 ›› 2018, Vol. 39 ›› Issue (6): 81-88.doi: 10.11959/j.issn.1000-436x.2018094

基于变量符号关联分析的程序状态优化方法

郭曦¹(),王盼²

¹ 华中农业大学信息学院，湖北武汉 430070
² 武汉电力职业技术学院电力工程系，湖北武汉 430079

修回日期:2018-04-02 出版日期:2018-06-01 发布日期:2018-07-09
作者简介:郭曦（1983-），男，湖北鄂州人，博士，华中农业大学副教授、硕士生导师，主要研究方向为软件分析与测试、信息安全等。|王盼（1987-），女，河南济源人，博士，武汉电力职业技术学院讲师，主要研究方向为电力电子变换等。
基金资助:
国家自然科学基金资助项目(61502194);中央高校基本科研业务费专项基金资助项目(2662018JC028)

Program state optimal method based on variable symbolic relation analysis

Xi GUO¹(),Pan WANG²

¹ College of Informatics,Huazhong Agriculture University,Wuhan 430070,China
² Department of Power Engineering,Wuhan Electric Power Technical College,Wuhan 430079,China

Revised:2018-04-02 Online:2018-06-01 Published:2018-07-09
Supported by:
The National Natural Science Foundation of China(61502194);The Central University Basic Business Expenses Special Funding for Scientific Research Projects(2662018JC028)

摘要/Abstract

摘要：

程序分析是主要的程序属性分析方法，在变量依赖关系、路径覆盖率、测试用例约简等方面有广泛的应用，并取得了大量研究成果。目前，程序分析主要以符号执行工具为核心，但是普遍存在路径条件逻辑表达式难以准确生成和约束求解器性能不够高的问题，从而影响程序分析的效果。以提高路径分析精度为目标，首先分析不同执行路径对应的路径条件，并提取公共的符号表达式以提高符号关联分析的精度，然后逆向生成依赖条件逻辑表达式集合，使用依赖关联分析算法以提高路径分析的精度。实验结果表明，所提方法相对于传统的路径分析方法，有更准确的时间复杂度和更高的路径分析精度。

关键词: 程序分析, 符号执行, 约束求解器, 符号分析

Abstract:

Program analysis is the prime method to program property analysis,which is widely used in the domain of parameter dependent relation,path coverage and test case generation,and a lot of progress has been made.Current program analysis is based on the method of symbolic execution,but symbolic execution is usually tackled with the problems of logic expression generation of path condition and low efficiency of constrain solver,which will affect the results of program analysis.Aiming at enhancing the path analysis efficiency,the path conditions of different paths were collected,the common symbolic expression was extracted and the efficiency of symbolic analysis was enhanced,then the logic expression set was generated,the dependent relation algorithm was used to enhance the efficiency of symbolic analysis.Experimental results demonstrate that the proposed method has the advantages of accurate time complexity and better analysis efficiency compare to traditional program analysis method.

Key words: program analysis, symbolic execution, constrain solver, symbolic analysis

中图分类号:

TP311

郭曦,王盼. 基于变量符号关联分析的程序状态优化方法[J]. 通信学报, 2018, 39(6): 81-88.

Xi GUO,Pan WANG. Program state optimal method based on variable symbolic relation analysis[J]. Journal on Communications, 2018, 39(6): 81-88.

图/表 9

图1

表1

图2

图3

表2

图4

表3

图5

表4

参考文献 15

[1]	KUZNETSOV V , KINDER J , BUCUR S ,et al. Efficient state merging in symbolic execution[J]. ACM Sigplan Notices, 2012,47(6): 193-204.
[2]	GODEFROID P , . Compositional dynamic test generation[C]// ACMSigplan-Sigact Symposium on Principles of Programming Languages. 2007: 47-54.
[3]	AVGERINOS T , REBERT A , SANG K C ,et al. Enhancing symbolic execution with veritesting[C]// International Conference on Software Engineering. 2014: 1083-1094.
[4]	GODEFROID P , NORI A V , RAJAMANI S K ,et al. Compositional maymust program analysis:unleashing the power of alternation[C]// ACM Sigplan-Sigact Symposium on Principles of Programming Languages. 2010: 43-56.
[5]	王翀, 吕荫润, 陈力 ,等. SMT 求解技术的发展及最新应用研究综述[J]. 计算机研究与发展, 2017,54(7): 1405-1425.
	WANG C , LYU Y R , CHEN L ,et al. Survey on development of solving methods and state of theart application of satisfiability modulo theories[J]. Journal of Computer Research and Development, 2017,54(7): 1405-1425.
[6]	TORLAK E , BODIK R . A lightweight symbolic virtual machine for solver-aided host languages[J]. ACM SIGPLAN Notices, 2014,49(6): 530-541.
[7]	VISSER W , REANU C S , NEK R . Test input generation for Java containers using state matching[C]// International Symposium on Software Testing and Analysis. 2006: 37-48.
[8]	CHAKRABARTI A , GODEFROID P . Software partitioning for effective automated unit testing[C]// ACM ＆ IEEE International Conference on Embedded Software. 2006: 262-271.
[9]	SHARIR M , PNUELI A . Two approaches to interprocedural dataflow analysis[M]. Englewood: Prentice-HallPress, 1981: 189-234.
[10]	REPS T , HORWITZ S , SAGIV M . Precise interprocedural dataflow analysis via graph reachability[C]// ACM Sigplan-Sigact Symposium on Principles of Programming Languages. 1995: 49-61.
[11]	PENG T , PADUA D . Gated SSA-based demand driven symbolic analysis for parallelizing compilers[C]// International Conference on Supercomputing. 1995: 414-423.
[12]	SEN K , NECULA G , GONG L ,et al. MultiSE:multi-path symbolic execution using value summaries[C]// The 10th Joint Meeting on Foundations of Software Engineering. 2015: 842-853.
[13]	QI D W , NGUYEN H , ROYCHOUDHURY A . Path exploration based on symbolic output[J]// ACM Transactions on Software Engineering and Methodology, 2011,22(4): 278-288.
[14]	王伟光, 曾庆凯, 孙浩 . 面向危险操作的动态符号执行方法[J]. 软件学报, 2016,27(5): 1230-1245.
	WANG W G , ZENG Q K , SUN H . Dynamic symbolic execution method oriented to critical operation[J]. Journal of Software, 2016,27(5): 1230-1245.
[15]	BANG L , AYDIN A , BULTAN T . Automatically computing path complexity of programs[C]// Joint Meeting on Foundations of Software Engineering. 2015: 61-72.

路径π	当前路径条件φ	x	y	z
1,2,3,6,8	φ₁=2x₀≤3∧z₀≤2	2x₀	y₀	z₀
1,2,3,6,7,8	φ₂=2x₀≤3∧z₀>2	2x₀	z₀–1	z₀
1,2,3,4,6,8	φ₃=2x₀>3∧y₀≠2∧z₀≤2	2x₀	y₀	z₀
1,2,3,4,6,7,8	φ₄=2x₀>3∧y₀≠2∧z₀>2	2x₀	z₀–1	z₀
1,2,3,4,5,6,7,8	φ₅=2x₀>3∧y₀=2	2x₀	1.5	2.5

步骤	输入	路径	依赖条件
1)	{x=6,y=2,z=2}	p_1,t,p_2,f,p_3,t]	?(x+y>10)
2)	{x=6,y=5,z=2}	p_1,t,p_2,t,p_3,t]	(x?y>0)∧(x+y>10)
3)	{x=6,y=2,z=2}	p_1,t,p_2,f,p_3,t]	?(x+y>10)
4)	{x=2,y=6,z=2}	p_1,f,p_2,f,p_3,t]	?(x+y>10)

测试集	基本特征				状态合并		符号执行
测试集	规模/行	执行时间/s	符号签名均值/个	符号签名共享度	合并数量/个	传统方法合并率	加速比	传统方法可行路径百分比	约束求解器平均调用次数/个
用例1	72	21.2	5.5	4.4	209	100.0%	1.2	76.5%	3.8
用例2	91	13.0	3.6	6.5	181	100.0%	5.2	65.2%	1.3
用例3	207	29.9	4.7	6.4	224	53.3%	5.2	86.5%	2.6
用例4	435	37.5	2.5	7.1	324	76.7%	4.8	61.6%	1.7
用例5	591	31.7	2.6	15.5	280	43.1%	2.0	67.7%	1.8
用例6	744	57.2	5.7	20.3	363	37.6%	3.3	85.8%	2.1
用例7	1 329	86.3	5.5	18.6	408	51.3%	2.4	73.6%	1.6

对比项	顺序分支	嵌套分支	顺序循环	嵌套循环
圈复杂度	K+1	K+1	K+1	K+1
NPATH复杂度	2^K	K+1	2^K	K+1
本文方法	2^K	K+1	Θ(n^K)	Θ(bⁿ)

基于变量符号关联分析的程序状态优化方法

Program state optimal method based on variable symbolic relation analysis

在线阅读

PDF下载

可视化

摘要/Abstract

引用本文

使用本文

图/表 9

参考文献 15

相关文章 1

Metrics

推荐阅读 0