Synthesis of loop bound functions for loop programs

doi:10.11772/j.issn.1001-9081.2021020221

Journal of Computer Applications ›› 2022, Vol. 42 ›› Issue (2): 565-573.DOI: 10.11772/j.issn.1001-9081.2021020221

• Computer software technology • Previous Articles Next Articles

Synthesis of loop bound functions for loop programs

Wang TAN¹^,², Yi LI¹()

^1.Chongqing Institute of Green and Intelligent Technology，Chinese Academy of Sciences，Chongqing 400714，China
^2.School of Computer Science and Technology，University of Chinese Academy of Sciences，Beijing 101408，China

Received:2021-02-05 Revised:2021-04-12 Accepted:2021-04-13 Online:2022-02-11 Published:2022-02-10
Contact: Yi LI
About author:TAN Wang， born in 1995， M. S. candidate. His research interests include， termination verification for loop programs， machine learning.
LI Yi， born in 1980， Ph. D.， research associate. His research interests include program verification， computer algebra.
Supported by:
National Natural Science Foundation of China(11771421);Chinese Academy of Sciences “Light of the West”, National Key Research and Development Program of China(2020YFA07123000);Natural Science Foundation of Chongqing(cstc2019jcyj-msxmX0638)

循环程序的界函数合成

谭旺¹^,², 李轶¹()

^1.中国科学院重庆绿色智能技术研究院, 重庆 400714
^2.中国科学院大学计算机科学与技术学院, 北京 101408

通讯作者: 李轶
作者简介:谭旺（1995—），男，重庆人，硕士研究生，主要研究方向：循环程序终止性验证、机器学习；
李轶（1980—），男，重庆人，副研究员，博士，CCF会员，主要研究方向：程序验证、计算机代数。
基金资助:
国家自然科学基金资助项目(11771421);中国科学院“西部之光”;国家重点研发计划项目(2020YFA07123000);重庆市自然科学基金资助项目(cstc2019jcyj-msxmX0638)

Abstract

Abstract:

As the mainstream methods of loop program termination analysis，most existing ranking function methods are limited to the solution of linear or polynomial ranking functions. Concerning that the existing ranking function methods cannot prove the termination if there are no corresponding linear or polynomial ranking functions for the loop programs， a new method was proposed to synthesize the loop bound function for the given loop program. The existence of loop bound function of a given loop program implies the termination of this loop function. Firstly， the problem of solving the loop bound functions was transformed into a linear binary classification problem. Once the function’s template was selected， the mapping relationship was established according to the template to construct the training set. After that， the obtained training set was used to obtain the classification hyperplane through Support Vector Machine （SVM） to find the template coefficients， thereby obtaining the candidate loop bound function. Finally， the existing symbol verification tool Redlog was used to verify this candidate loop bound function. Experimental results show that compared with the existing ranking function methods， the proposed method not only can be applied to more loop programs， but also has the obtained loop bound functions more simplified in form than the ranking functions. Specifically， for some loops without linear ranking functions， the corresponding linear loop bound functions can be solved by the proposed method； at the same time， for some loops with only multiphase linear ranking functions， the global linear loop bound functions can be solved by the proposed method.

Key words: program verification, loop program termination, Support Vector Machine (SVM), loop bound function, ranking function

摘要：

作为循环程序终止性分析的主流方法，当前的秩函数方法大多局限于线性或多项式秩函数的求解。针对循环程序若不存在对应的线性或多项式秩函数，现有秩函数方法就无法证明其终止性的问题，提出一个新的方法来合成给定循环程序对应的界函数。对于给定的循环程序，倘若能找到其界函数，则表明该循环程序是可终止的。首先将界函数的求解问题转化为一个线性二分类问题，并在选定界函数模板后，根据模板建立映射关系以构建训练集；然后利用所得训练集通过支持向量机（SVM）获取分类超平面进而求解得到模板系数，从而得到候选的界函数；最后利用现有的符号验证工具Redlog对该候选界函数进行验证。实验结果表明，相较于现有的秩函数方法，所提方法不仅能够应用于更多的循环程序，而且所得界函数在形式上相较于秩函数更加简化。具体表现为，对于某些没有线性秩函数的循环，该方法可以得到其对应的线性界函数；同时，对于某些只有多阶段线性秩函数的循环，该方法可以求解得到全局的线性界函数。

关键词: 程序验证, 循环程序终止性, 支持向量机, 界函数, 秩函数

CLC Number:

TP311

Wang TAN, Yi LI. Synthesis of loop bound functions for loop programs[J]. Journal of Computer Applications, 2022, 42(2): 565-573.

谭旺, 李轶. 循环程序的界函数合成[J]. 《计算机应用》唯一官方网站, 2022, 42(2): 565-573.

Figures/Tables 6

Fig. 1 Framework of synthesizing loop bound function

Fig. 2 Flowchart of calculating loop bound function for loop program via SVM

Tab. 1 Loops for experiments

编号	表达式
1	$w h i l e (a 1! = a 2) d o i f (a 1 > a 2) a 1' = a 1 - a 2; i f (a 2 > a 1) a 2' = a 2 - a 1$
2	$w h i l e (1 < a 1 < 10) d o a 1' = 2 a 1; a 2' = a 2 + 1$
3	$w h i l e (a 22 + 10 ≤ a 1 + 6 a 2, a 12 + 6 ≤ 4 a 1 + a 2) d o a 1' = a 1 + a 2; a 2' = a 2 - 1$
4	$w h i l e (a 1 + a 2 ≥ 1, a 1 ≤ 3, a 22 ≤ 1) d o a 1' = 5 a 1 - a 12; a 2' = a 22 + a 2$
5	$w h i l e (a 1 > a 22 - a 2) d o a 1' = a 1 + a 2 - 5; a 2' = - a 2$
6	$w h i l e (a 1 ≥ a 2, a 2 ≥ 0) d o a 1' = a 1 - 4 a 22 - 4 a 2 + 3; a 2' = a 2 - 2$
7	$w h i l e (a 1 ≥ 0, a 2 ≥ 0) d o a 1' = a 1 - a 2; a 2' = 2 a 2 + 1$
8	$w h i l e (a 1 ≥ 0, a 2 ≥ a 1) d o a 1' = 3 a 1 - a 2; a 2' = 4 a 1 + 2 a 2 + 3$
9	$w h i l e (a 1 ≥ 1, a 1 - a 2 ≥ 1) d o a 1' = a 1 - 2 a 2; a 2' = 2 a 1 + 4 a 2 + 2$
10	$w h i l e (4 a 1 + a 2 ≥ 1) d o a 1' = - 2 a 1 + 4 a 2; a 2' = 4 a 1$

Tab. 1 Loops for experiments

编号	表达式
1	$w h i l e (a 1! = a 2) d o i f (a 1 > a 2) a 1' = a 1 - a 2; i f (a 2 > a 1) a 2' = a 2 - a 1$
2	$w h i l e (1 < a 1 < 10) d o a 1' = 2 a 1; a 2' = a 2 + 1$
3	$w h i l e (a 22 + 10 ≤ a 1 + 6 a 2, a 12 + 6 ≤ 4 a 1 + a 2) d o a 1' = a 1 + a 2; a 2' = a 2 - 1$
4	$w h i l e (a 1 + a 2 ≥ 1, a 1 ≤ 3, a 22 ≤ 1) d o a 1' = 5 a 1 - a 12; a 2' = a 22 + a 2$
5	$w h i l e (a 1 > a 22 - a 2) d o a 1' = a 1 + a 2 - 5; a 2' = - a 2$
6	$w h i l e (a 1 ≥ a 2, a 2 ≥ 0) d o a 1' = a 1 - 4 a 22 - 4 a 2 + 3; a 2' = a 2 - 2$
7	$w h i l e (a 1 ≥ 0, a 2 ≥ 0) d o a 1' = a 1 - a 2; a 2' = 2 a 2 + 1$
8	$w h i l e (a 1 ≥ 0, a 2 ≥ a 1) d o a 1' = 3 a 1 - a 2; a 2' = 4 a 1 + 2 a 2 + 3$
9	$w h i l e (a 1 ≥ 1, a 1 - a 2 ≥ 1) d o a 1' = a 1 - 2 a 2; a 2' = 2 a 1 + 4 a 2 + 2$
10	$w h i l e (4 a 1 + a 2 ≥ 1) d o a 1' = - 2 a 1 + 4 a 2; a 2' = 4 a 1$

Tab. 2 Experimental parameters and template coefficients

编号	界函数模板	负类点	模板系数
1	$w 1 ⋅ a 1 + w 2 ⋅ a 2 + w 3$	（0，0，1）	（2，2，2）
2	$w 1 ⋅ a 1 + w 2$	（10，1）	（10，0）
3	$w 1 ⋅ a 1 + w 2 ⋅ a 2 + w 3$	（-1，-1，1）	（1，1，1）
4	$w 1 ⋅ a 1 + w 2 ⋅ a 2 + w 3$	（0，0，1）	（3.34，3.32，1）
5	$w 1 ⋅ a 1 + w 2 ⋅ a 2 + w 3$	（-1，0.5，1）	（2，2，1）
6	$w 1 ⋅ a 1 + w 2 ⋅ a 2 + w 3$	（0，0，1）	（3，5，4）
7	$w 1 ⋅ a 1 + w 2 ⋅ a 2 + w 3$	（-1，-1，1）	（2，2，4）
8	$w 1 ⋅ a 1 + w 2 ⋅ a 2 + w 3$	（-1，-1，1）	（3，3，9）
9	$w 1 ⋅ a 1 + w 2 ⋅ a 2 + w 3$	（-1，-1，1）	（3，2，16）
10	$w 1 ⋅ (a 1 + 1) 2 + w 2 ⋅ (a 2 + 1) 2 + w 3$	（0，0，1）	（6，6，25）

Tab. 2 Experimental parameters and template coefficients

编号	界函数模板	负类点	模板系数
1	$w 1 ⋅ a 1 + w 2 ⋅ a 2 + w 3$	（0，0，1）	（2，2，2）
2	$w 1 ⋅ a 1 + w 2$	（10，1）	（10，0）
3	$w 1 ⋅ a 1 + w 2 ⋅ a 2 + w 3$	（-1，-1，1）	（1，1，1）
4	$w 1 ⋅ a 1 + w 2 ⋅ a 2 + w 3$	（0，0，1）	（3.34，3.32，1）
5	$w 1 ⋅ a 1 + w 2 ⋅ a 2 + w 3$	（-1，0.5，1）	（2，2，1）
6	$w 1 ⋅ a 1 + w 2 ⋅ a 2 + w 3$	（0，0，1）	（3，5，4）
7	$w 1 ⋅ a 1 + w 2 ⋅ a 2 + w 3$	（-1，-1，1）	（2，2，4）
8	$w 1 ⋅ a 1 + w 2 ⋅ a 2 + w 3$	（-1，-1，1）	（3，3，9）
9	$w 1 ⋅ a 1 + w 2 ⋅ a 2 + w 3$	（-1，-1，1）	（3，2，16）
10	$w 1 ⋅ (a 1 + 1) 2 + w 2 ⋅ (a 2 + 1) 2 + w 3$	（0，0，1）	（6，6，25）

Tab. 3 Feasibility comparison of different methods

编号	基于QE 秩函数合成	基于SVM 秩函数合成	多阶段线性秩函数合成	本文方法
1	成功	成功	失败	成功
2	成功	成功	成功	成功
3	失败	成功	失败	成功
4	失败	成功	失败	成功
5	失败	成功	失败	成功
6	失败	成功	失败	成功
7	失败	失败	成功	成功
8	失败	失败	成功	成功
9	失败	失败	成功	成功
10	失败	失败	失败	成功

Tab. 4 Comparison of experimental results in functional forms

编号	基于QE 秩函数合成	基于SVM 秩函数合成	多阶段线性秩函数合成	本文方法
1	线性	线性	无法合成	线性
2	线性	线性	线性	线性
3	无法合成	线性	无法合成	线性
4	无法合成	线性	无法合成	线性
5	无法合成	非线性	无法合成	线性
6	无法合成	非线性	无法合成	线性
7	无法合成	无法合成	多阶段线性	线性
8	无法合成	无法合成	多阶段线性	线性
9	无法合成	无法合成	多阶段线性	线性
10	无法合成	无法合成	无法合成	非线性

References 32

1	COUSOT P， COUSOT R. An abstract interpretation framework for termination ［C］// Proceedings of the 39th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages. New York： ACM， 2012： 245-258. 10.1145/2103656.2103687
2	LEE S C， JONES N D， BEN-AMRAM A M. The size-change principle for program termination ［C］// Proceedings of the 28th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages. New York： ACM， 2001： 81-92. 10.1145/360204.360210
3	LEIKE J， HEIZMANN M. Geometric nontermination arguments ［C］// Proceedings of the 2018 International Conference on Tools and Algorithms for the Construction and Analysis of Systems， LNCS10806. Cham： Springer， 2018： 266-283.
4	BRAVERMAN M. Termination of integer linear programs ［C］// Proceedings of the 2006 International Conference on Computer Aided Verification， LNCS4144. Berlin： Springer， 2006： 372-385.
5	TIWARI A. Termination of linear programs ［C］// Proceedings of the 2004 International Conference on Computer Aided Verification， LNCS3114. Berlin： Springer， 2004： 70-82.
6	TURING A M. On computable numbers， with an application to the Entscheidungsproblem［J］. Proceedings of the London Mathematical Society， 1937， s2-41（1）： 230-265. 10.1112/plms/s2-42.1.230
7	CHEN Y F， HEIZMANN M， LENGÁL O， et al. Advanced automata-based algorithms for program termination checking ［C］// Proceedings of the 39th ACM SIGPLAN Conference on Programming Language Design and Implementation. New York： ACM， 2018： 135-150. 10.1145/3192366.3192405
8	FEDYUKOVICH G， ZHANG Y L， GUPTA A. Syntax-guided termination analysis ［C］// Proceedings of the 2018 International Conference on Computer Aided Verification， LNCS10981. Cham： Springer， 2018： 124-143.
9	LI Y. Witness to non-termination of linear programs［J］. Theoretical Computer Science， 2017， 681： 75-100. 10.1016/j.tcs.2017.03.036
10	BAGNARA R， MESNARD F. Eventual linear ranking functions ［C］// Proceedings of the 15th International Symposium on Principles and Practice of Declarative Programming. New York： ACM， 2013： 229-238. 10.1145/2505879.2505884
11	BEN-AMRAM A M， GENAIM S. Ranking functions for linear-constraint loops［J］. Journal of the ACM， 2014， 61（4）： No.26. 10.1145/2629488
12	BEN-AMRAM A M， GENAIM S. On multiphase-linear ranking functions ［C］// Proceedings of the 2017 International Conference on Computer Aided Verification， LNCS10427. Cham： Springer， 2017： 601-620.
13	LEIKE J， HEIZMANN M. Ranking templates for linear loops ［C］// Proceedings of the 2014 International Conference on Tools and Algorithms for the Construction and Analysis of Systems， LNCS8413. Berlin： Springer， 2014： 172-186. 10.2168/lmcs-11(1:16)2015
14	LI Y， ZHU G， FENG Y. The l-depth eventual linear ranking functions for single-path linear constraint loops ［C］// Proceedings of the 10th International Symposium on Theoretical Aspects of Software Engineering. Piscataway： IEEE， 2016： 30-37. 10.1109/tase.2016.8
15	CHEN Y H， XIA B C， YANG L， et al. Discovering non-linear ranking functions by solving semi-algebraic systems ［C］// Proceedings of the 2007 International Colloquium on Theoretical Aspects of Computing， LNCS4711. Berlin： Springer， 2007： 34-49.
16	SHEN L Y， WU M， YANG Z F， et al. Generating exact nonlinear ranking functions by symbolic-numeric hybrid method［J］. Journal of Systems Science and Complexity， 2013， 26（2）： 291-301. 10.1007/s11424-013-1004-1
17	YUAN Y， LI Y. Ranking function detection via SVM： a more general method［J］. IEEE Access， 2019， 7： 9971-9979. 10.1109/access.2018.2890692
18	KOVÁCS L. Automated invariant generation by algebraic techniques for imperative program verification in Theorema［D］. Linz： Johannes Kepler University Linz， 2007： 43-75.
19	GULWANI S， JAIN S， KOSKINEN E. Control-flow refinement and progress invariants for bound analysis ［C］// Proceedings of the 30th ACM SIGPLAN Conference on Programming Languages Design and Implementation. New York： ACM， 2009： 375-385. 10.1145/1542476.1542518
20	GULWANI S， MEHRA K K， CHILIMBI T. SPEED： precise and efficient static estimation of program computational complexity ［C］// Proceedings of the 36th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages. New York： ACM， 2009： 127-139. 10.1145/1594834.1480898
21	NORI A V， SHARMA R. Termination proofs from tests ［C］// Proceedings of the 9th Joint Meeting on Foundations of Software Engineering. New York： ACM， 2013： 246-256. 10.1145/2491411.2491413
22	邢建英.程序验证关键技术研究［D］.长沙：国防科学技术大学， 2011： 63-75.
	XING J Y. Study on program verification［D］. Changsha： National University of Defense Technology， 2011： 63-75.
23	BERDINE J， CHAWDHARY A， COOK B， et al. Variance analyses from invariance analyses ［C］// Proceedings of the 34th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages. New York： ACM， 2007： 211-224. 10.1145/1190216.1190249
24	CHAWDHARY A， COOK B， GULWANI S， et al. Ranking abstractions ［C］// Proceedings of the 2008 International Conference on European Symposium on Programming. Cham： Springer， 2008： 148-162. 10.1007/978-3-540-78739-6_13
25	TSITOVICH A， SHARYGINA N， WINTERSTEIGER C M， et al. Loop summarization and termination analysis ［C］// Proceedings of the 2011 International Conference on Tools and Algorithms for the Construction and Analysis of Systems. Cham： Springer， 2011： 81-95. 10.1007/978-3-642-19835-9_9
26	KROENING D， SHARYGINA N， TSITOVICH A， et al. Termination analysis with compositional transition invariants ［C］// Proceedings of the 2010 International Conference on Computer Aided Verification， LNCS6174. Berlin： Springer， 2010： 89-103.
27	PODELSKI A， RYBALCHENKO A. Transition invariants ［C］// Proceedings of the 19th Annual IEEE Symposium on Logic in Computer Science. Piscataway： IEEE， 2004： 32-41. 10.1109/lics.2004.1319598
28	PEDREGOSA F， VAROQUAUX G， GRAMFORT A， et al. Scikit-learn： machine learning in Python［J］. Journal of Machine Learning Research， 2011， 12： 2825-2830. 10.3389/fninf.2014.00014
29	GULWANI S. SPEED： symbolic complexity bound analysis ［C］// Proceedings of the 2009 International Conference on Computer Aided Verification， LNCS5643. Berlin： Springer， 2009： 51-62.
30	VAPNIK V N， CHERVONENKIS A Y. A note on one class of perceptrons［J］. Automation and Remote Control， 1964， 25（1）： 103-109.
31	VAPNIK V N. Statistical learning theory［J］. Encyclopedia of the Sciences of Learning， 1998， 41（4）： 3185-3185.
32	周志华.机器学习［M］.北京：清华大学出版社， 2016： 121-124. 10.21436/inbom.12382432
	ZHOU Z H. Machine Learning［M］. Beijing： Tsinghua University Press， 2016： 121-124. 10.21436/inbom.12382432

[1]	Min SUN, Qian CHENG, Xining DING. CBAM-CGRU-SVM based malware detection method for Android [J]. Journal of Computer Applications, 2024, 44(5): 1539-1545.
[2]	Enbao QIAO, Xiangyang GAO, Jun CHENG. Self-recovery adaptive Monte Carlo localization algorithm based on support vector machine [J]. Journal of Computer Applications, 2024, 44(10): 3246-3251.
[3]	Xueyu HUANG, Huaiyu HE, Huimin LIN, Jinshui CHEN. Classification and recognition method of copper alloy metallograph based on feature aggregation [J]. Journal of Computer Applications, 2023, 43(8): 2593-2601.
[4]	Lei YANG, Hongdong ZHAO, Kuaikuai YU. End-to-end speech emotion recognition based on multi-head attention [J]. Journal of Computer Applications, 2022, 42(6): 1869-1875.
[5]	Zhen QU, Kunting LI, Zhixi FENG. Remote sensing image scene classification based on effective channel attention [J]. Journal of Computer Applications, 2022, 42(5): 1431-1439.
[6]	Guifang QIAO, Shouming HOU, Yanyan LIU. Facial expression recognition algorithm based on combination of improved convolutional neural network and support vector machine [J]. Journal of Computer Applications, 2022, 42(4): 1253-1259.
[7]	Qian GE, Guangbin ZHANG, Xiaofeng ZHANG. Automatic feature selection algorithm based on interaction of ReliefF with maximum information coefficient and SVM [J]. Journal of Computer Applications, 2022, 42(10): 3046-3053.
[8]	Hongfei JIA, Xi LIU, Yu WANG, Hongbing XIAO, Suxia XING. Application of 3DPCANet in image classification of functional magnetic resonance imaging for Alzheimer’s disease [J]. Journal of Computer Applications, 2022, 42(1): 310-315.
[9]	JIA Heming, JIANG Zichao, LI Yao, SUN Kangjian. Simultaneous feature selection optimization based on improved spotted hyena optimizer algorithm [J]. Journal of Computer Applications, 2021, 41(5): 1290-1298.
[10]	YUAN Qianqian, DENG Hongmin, WANG Xiaohang. Citrus disease and insect pest area segmentation based on superpixel fast fuzzy C-means clustering and support vector machine [J]. Journal of Computer Applications, 2021, 41(2): 563-570.
[11]	Hongliang CAO, Ying ZHANG, Bin WU, Fanyu LI, Xubo NA. Prediction method of liver transplantation complications based on transfer component analysis and support vector machine [J]. Journal of Computer Applications, 2021, 41(12): 3608-3613.
[12]	Kai LI, Jie LI. Structure-fuzzy multi-class support vector machine algorithm based on pinball loss [J]. Journal of Computer Applications, 2021, 41(11): 3104-3112.
[13]	TONG Lin, GUAN Zheng. Fuzzy granulation prediction of traffic flow based on improved whale optimization support vector machine [J]. Journal of Computer Applications, 2021, 41(10): 2919-2927.
[14]	ZHANG Jianming, SHI Yuanhao, XU Zhengyi, WEI Jianming. Adaptive UWB/PDR fusion positioning algorithm based on error prediction [J]. Journal of Computer Applications, 2020, 40(6): 1755-1762.
[15]	WANG Yang, ZHAO Hongdong. Human activity recognition based on improved particle swarm optimization-support vector machine and context-awareness [J]. Journal of Computer Applications, 2020, 40(3): 665-671.

Synthesis of loop bound functions for loop programs

循环程序的界函数合成

RichHTML

PDF

Knowledge

Abstract

Cite this article

share this article

Figures/Tables 6

References 32

Related Articles 15

Recommended Articles

Metrics