循环程序的界函数合成

Synthesis of loop bound functions for loop programs

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

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.