论文部分内容阅读
字符串是很多编程语言都包含的数据类型，而且字符串在实际程序中被广泛使用，比如web应用程序。字符串约束求解是对操作字符串的程序进行静态分析与验证的基础。目前主流的字符串约束求解器比如CVC4和Z3-str等一般支持对含有字符串连接函数、正则表达式、以及字符串长度的约束的求解。但这些字符串约束语言还远远满足不了对操作字符串的程序进行分析与验证的需要。这方面的一个例子是replaceAll函数。虽然replaceAll函数是web应用程序中常用的字符串操作，但由于replaceAll函数本身的递归特性，目前主流的字符串约束求解器对replaceAll函数要么不支持，要么只是提供启发式算法来求解。因此缺乏针对含有replaceAll函数的字符串约束的可靠完备的判定算法以及求解器。 本论文聚焦在对含有replaceAll函数的字符串约束的求解上。一般来讲，replaceAll函数含有三个参数:第一个参数是主体串(subject)，第二个参数是形式上为字符串或正则表达式的模式(pattern)，第三个参数是替代串(replacement)。replaceAll函数的直观意思是将主体串中模式的所有出现都换为替代串。Lin和Barceló在POPL2016文章中证明了含有replaceAll函数和正规表达式的字符串约束的可满足性问题是不可判定的。他们还以对操作字符串的程序进行符号执行为背景提出了字符串约束的直线子集（straight-line fragment）的概念。本论文对含有replaceAll函数和正规表达式的字符串约束的直线子集（记为SL[replaceAll]）的可满足性问题进行了全面的探讨。具体来讲，本论文的贡献如下: -证明了如果模式参数允许为字符串变量，则SL[replaceAll]的可满足性问题是不可判定的; -证明了如果模式参数为正规表达式，则SL[replaceAll]的可满足性问题可以在指数空间内判定，而且，该判定算法基于自动机构造，具有模块化的优点，易于实现; -我们在Z3的基础上实现了本论文中提出的判定算法，开发了原型工具Z3-replaceAll，进行了实例研究，展示了提出的判定算法的实际可行性。