We use cookies to improve your experience with our site.

对于包含字符串以及字符串函数的程序的自动化约束求解方法

Automated String Constraints Solving for Programs Containing String Manipulation Functions

  • 摘要: 对于各种类型的约束的支持是约束求解器首要指标。在编程语言中,字符串类型经常作为基本的数据类型出现,并且通过字符串库函数进行操作。当以字符串约束作为输入时,大多数约束求解器存在着无法处理复杂的字符串库函数约束或者无法求解混合约束等局限性。这些局限性阻碍了约束求解器在程序分析、自动测试等领域的应用。基于字符数组的数据模型,我们设计了一个包含有限原子操作的约束描述语言,来准确描述常用的字符串操作函数的约束。然后利用一个两步骤的约束求解过程求解转换之后的字符串约束和其他类型的约束:第一,得到关注字符串的字符成员位置约束的部分解,利用此部分解来将字符串约束约简为字符数组约束;第二,利用现成的约束求解器对约简之后的约束进行求解。
    本文所提出的方法在一个自动测试工具中进行了实现,实验结果表明了本方法的有效性,对比试验表明本文所提出的技术相比于同类技术的应用效果有了提升。

     

    Abstract: The ability to solve various constraints is a principal factor of automatic constraint solvers. Most object-oriented languages treat a character string as a primitive data type which is manipulated by string library functions. Most constraint solvers have limitations on their input constraints, such as strong restrictions on the expressiveness of constraints or lack of the ability to solve hybrid constraints. These limitations hinder applying automated constraint solvers on program analysis techniques for programs containing strings and string manipulation functions. We propose an approach to automatically solve program constraints involving strings and string manipulation functions. Based on the character array model, we design a constraint language which contains primitive operations to precisely describe the constraints of commonly used string manipulation functions. The translated string constraints together with numeric constraints are then solved by a twophase test generation procedure:firstly, a partial solution is obtained to satisfy the arithmetic constraints of the position variables, and the solution is utilized to simplify the string constraints into pure character array constraints; secondly, the pure array constraints are solved by an off-the-shelf array-specific theory based constraint solver. We integrate the approach into an automated testing tool to support the generation of string test cases, and then perform experiments. The results of the experiments prove that the integration of the proposed approach promotes the testing coverage of the existing testing tool, and the integrated tool has an advantage of handling specific string manipulation functions compared with an existing string solver.

     

/

返回文章
返回