›› 2017, Vol. 32 ›› Issue (6): 1125-1135.doi: 10.1007/s11390-017-1787-y

• Special Section on Software Systems 2017 • Previous Articles     Next Articles

Automated String Constraints Solving for Programs Containing String Manipulation Functions

Xu-Zhou Zhang1, Yun-Zhan Gong1, Member, CCF, Ya-Wen Wang1, Member, CCF, Ying Xing2, Member, CCF, Ming-Zhe Zhang1   

  1. 1 State Key Laboratory of Networking and Switching Technology, Beijing University of Posts and Telecommunications Beijing 100876, China;
    2 Automation School, Beijing University of Posts and Telecommunications, Beijing 100876, China
  • Received:2017-04-27 Revised:2017-09-27 Online:2017-11-05 Published:2017-11-05
  • Contact: 10.1007/s11390-017-1787-y
  • About author:Xu-Zhou Zhang received his B.S.degree in computer science and technology from Huazhong University of Science and Technology,Wuhan,in 2010.He is currently a Ph.D.candidate in the State Key Laboratory of Networking and Switching Technology,Beijing University of Posts and Telecommunications,Beijing.His research interest is program analysis and software testing.
  • Supported by:

    This work was partially supported by the National Natural Science Foundation of China under Grant Nos. 61202080, 61702044, and 61502029.

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.

[1] Zhang D L, Sui J W, Gong Y Z. Large scale software test data generation based on collective constraint and weighted combination method. Tehni?ki Vjesnik, 2017, 24(4):1041-1049.

[2] Zhang Z X, Chen Z Y, Gao R Z, Wong E W, Xu B W. An empirical study on constraint optimization techniques for test generation. Science China Information Sciences, 2017, 60(1):012105

[3] Bjørner N, Tillmann N, Voronkov A. Path feasibility analysis for string-manipulating programs. In Tools and Algorithms for the Construction and Analysis of Systems, Kowalewski S, Philippou A (eds.), Springer, 2009, pp.307-321.

[4] Hooimeijer P, Weimer W. A decision procedure for subset constraints over regular languages. ACM SIGPLAN Notices, 2009, 44(6):188-198.

[5] Tillmann N, de Halleux J. Pex-white box test generation for.NET. In Tests and Proofs, Beckert B, Hähnle R (eds.), Springer, 2008, pp.134-153.

[6] Wang Y W, Xing Y, Gong Y Z, Zhang X Z. Optimized branch and bound for path-wise test data generation. Int. Journal of Computers Communications & Control, 2014, 9(4):497-509.

[7] Liang T Y, Reynolds A, Tinelli C, Barrett C, Deters M. A DPLL(T) theory solver for a theory of strings and regular expressions. In Computer Aided Verification, Biere A, Bloem R (eds.), Springer, 2014, pp.646-662.

[8] van Benthem J, Doets K. Higher-order logic. In Handbook of Philosophical Logic, Gabbay D, Guenthner F (eds.), Springer, 1983, pp.275-329

[9] Khoussainov B, Nies A, Rubin S, Stephan F. Automatic structures:Richness and limitations. In Proc. the 19th Annual IEEE Symp. Logic in Computer Science, July 2004, pp.44-53.

[10] Nieuwenhuis R, Oliveras A, Tinelli C. Solving SAT and SAT modulo theories:From an abstract Davis-PutnamLogemann-Loveland procedure to DPLL(T). Journal of the ACM, 2006, 53(6):937-977.

[11] Kiezun A, Ganesh V, Guo P J, Hooimeijer P, Ernst M D. HAMPI:A solver for string constraints. In Proc. the 18th Int. Symp. Software Testing and Analysis, July 2009, pp.105-116.

[12] Ganesh V, Dill D L. A decision procedure for bit-vectors and arrays. In Computer Aided Verification, Damm W, Hermanns H (eds.), Springer, 2007, pp.519-531.

[13] Saxena P, Akhawe D, Hanna S, Mao F, McCamant S, Song D. A symbolic execution framework for JavaScript. In Proc. IEEE Symp. Security and Privacy, May 2010, pp.513-528.

[14] de Moura L, Bjørner N. Z3:An efficient SMT solver. In Tools and Algorithms for the Construction and Analysis of Systems, Ramakrishnan C R, Rehof J (eds.), Springer, 2008, pp.337-340.

[15] Zheng Y H, Zhang X Y, Ganesh V. Z3-str:A Z3-based string solver for web application analysis. In Proc. the 9th Joint Meeting on Foundations of Software Engineering, August 2013, pp.114-124.

[16] Trinh M T, Chu D H, Jaffar J. S3:A symbolic string solver for vulnerability detection in web applications. In Proc. ACM SIGSAC Conf. Computer and Communications Security, November 2014, pp.1232-1243.

[17] Stump A, Barrett C W, Dill D L. CVC:A cooperating validity checker. In Computer Aided Verification, Brinksma E, Larsen K G (eds.), Springer, 2002, pp.500-504.

[18] Hooimeijer P, Weimer W. Solving string constraints lazily. In Proc. IEEE/ACM Int. Conf. Automated Software Engineering, September 2010, pp.377-386.

[19] Veanes M, de Halleux P, Tillmann N. Rex:Symbolic regular expression explorer. In Proc. the 3rd Int. Conf. Software Testing, Verification and Validation, April 2010, pp.498-507.

[20] Ghosh I, Shafiei N, Li G D, Chiang W F. JST:An automatic test generation tool for industrial Java applications with strings. In Proc. the 35th Int. Conf. Software Engineering, May 2013, pp.992-1001.
No related articles found!
Full text



[1] Gao Qingshi; Zhang Xiang; Yang Shufan; Chen Shuqing;. Vector Computer 757[J]. , 1986, 1(3): 1 -14 .
[2] Shen Li;. Testability Analysis at Switch Level for CMOS Circuits[J]. , 1990, 5(2): 197 -202 .
[3] Han Jianchao; Shi Zhongzhi;. Formalizing Default Reasoning[J]. , 1990, 5(4): 374 -378 .
[4] Huang Zhiyi; Hu Shouren;. Detection of And-Parallelism in Logic Programs[J]. , 1990, 5(4): 379 -387 .
[5] Song Maoqiang; Felix Grimm; Horst Bunke;. A Prototype Expert System for Automatic Generation of Image Processing Programs[J]. , 1991, 6(3): 296 -300 .
[6] Lin Shan;. Using a Student Model to Improve Explanation in an ITS[J]. , 1992, 7(1): 92 -96 .
[7] Harald E. Otto;. UNDO, An Aid for Explorative Learning?[J]. , 1992, 7(3): 226 -236 .
[8] Xu Meirui; Liu Xiaolin;. A VLSI Algorithm for Calculating the Tree to Tree Distance[J]. , 1993, 8(1): 68 -76 .
[9] Gu Junzhong;. Modelling Enterprises with Object-Oriented Paradigm[J]. , 1993, 8(3): 80 -89 .
[10] Huang Guoyong; Li Sanli;. TSP: A Heterogeneous Multiprocessor Supercomputing System Based on i860XP[J]. , 1994, 9(3): 285 -288 .

ISSN 1000-9000(Print)

CN 11-2296/TP

Editorial Board
Author Guidelines
Journal of Computer Science and Technology
Institute of Computing Technology, Chinese Academy of Sciences
P.O. Box 2704, Beijing 100190 P.R. China
E-mail: jcst@ict.ac.cn
  Copyright ©2015 JCST, All Rights Reserved