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

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

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

CLC Number:

TP311

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

Figures/Tables 9

References 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.

Metrics

Recommended 0

No Suggested Reading articles found!

路径π	当前路径条件φ	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

RichHTML

PDF

Knowledge

Abstract

Cite this article

share this article

Figures/Tables 9

References 15

Related Articles 1

Metrics

Recommended 0