一种判定具有非数据类型的字符串操作程序路径可行性的方法
A Decision Procedure for Path Feasibility of String Manipulating Programs with Integer Data Type
摘要：
字符串广泛用于程序中，特别是Web应用程序中。字符串数据类型自然出现在字符串操作程序中，并且经常用于引用字符串的长度或位置。字符串操作程序的分析和测试可以表述为路径可行性问题：给定一个符号执行路径，是否存在对输入的赋值，从而产生实现该路径的具体执行？这样的问题可以自然地重新表述为字符串约束求解问题。虽然最先进的字符串约束求解器通常提供对字符串和整数数据类型的支持，但它们主要采用没有完整性保证的解析法。在本文中，我们提出了一类字符串操作程序，其中不仅包括广泛的字符串操作，如串联，replaceAll，反向，有限的转换器，但也涉及整数数据类型，如长度，indexof，和子串的决策过程。据我们所知，这是目前已知的最具表现力的字符串约束语言之一。我们的决策过程是基于一个变种的成本寄存器自动机。我们实施的决策过程，从而产生一个新的解决方案OSTRICH+。我们在广泛的现有和新的基准上评估OSTRICH+的性能。实验结果表明，OSTRICH+是第一个字符串决策程序能够处理有限的传感器和整数约束，而其整体性能是最先进的字符串约束求解器相媲美。
英文摘要：
Strings are widely used in programs, especially in web applications. Integer data type occurs naturally in string-manipulating programs, and is frequently used to refer to lengths of, or positions in, strings. Analysis and testing of string-manipulating programs can be formulated as the path feasibility problem: given a symbolic execution path, does there exist an assignment to the inputs that yields a concrete execution that realizes this path? Such a problem can naturally be reformulated as a string constraint solving problem. Although state-of-the-art string constraint solvers usually provide support for both string and integer data types, they mainly resort to heuristics without completeness guarantees. In this paper, we propose a decision procedure for a class of string-manipulating programs which includes not only a wide range of string operations such as concatenation, replaceAll, reverse, and finite transducers, but also those involving the integer data-type such as length, indexof, and substring. To the best of our knowledge, this represents one of the most expressive string constraint languages that is currently known to be decidable. Our decision procedure is based on a variant of cost register automata. We implement the decision procedure, giving rise to a new solver OSTRICH+. We evaluate the performance of OSTRICH+ on a wide range of existing and new benchmarks. The experimental results show that OSTRICH+ is the first string decision procedure capable of tackling finite transducers and integer constraints, whilst its overall performance is comparable with the state-of-the-art string constraint solvers.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
