Journal of Computer Science and Technology ›› 2019, Vol. 34 ›› Issue (3): 670-689.doi: 10.1007/s11390-019-1935-7

Special Issue: Software Systems

• Software Systems • Previous Articles     Next Articles

Unit Test Data Generation for C Using Rule-Directed Symbolic Execution

Ming-Zhe Zhang, Yun-Zhan Gong, Member, CCF, Ya-Wen Wang*, Member, CCF, Da-Hai Jin, Member, CCF   

  1. State Key Laboratory of Networking and Switching Technology, Beijing University of Posts and Telecommunications Beijing 100876, China
  • Received:2018-07-06 Revised:2019-03-19 Online:2019-05-05 Published:2019-05-06
  • Contact: Ya-Wen Wang
  • About author:Ming-Zhe Zhang received his B.E. degree in computer science and technology from Shandong Normal University, Jinan, in 2012. 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 current research interests mainly focus on software testing and program analysis.
  • Supported by:
    This work was supported by the National Natural Science Foundation of China under Grant Nos. U1736110 and 61702044.

Unit testing is widely used in software development. One important activity in unit testing is automatic test data generation. Constraint-based test data generation is a technique for automatic generation of test data, which uses symbolic execution to generate constraints. Unit testing only tests functions instead of the whole program, where individual functions typically have preconditions imposed on their inputs. Conventional symbolic execution cannot detect these preconditions, let alone converting these preconditions into constraints. To overcome these limitations, we propose a novel unit test data generation approach using rule-directed symbolic execution for dealing with functions with missing input preconditions. Rule-directed symbolic execution uses predefined rules to detect preconditions in the individual function, and generates constraints for inputs based on preconditions. We introduce implicit constraints to represent preconditions, and unify implicit constraints and program constraints into integrated constraints. Test data generated based on integrated constraints can explore previously unreachable code and help developers find more functional faults and logical faults. We have implemented our approach in a tool called CTS-IC, and applied it to real-world projects. The experimental results show that rule-directed symbolic execution can find preconditions (implicit constraints) automatically from an individual function. Moreover, the unit test data generated by our approach achieves higher coverage than similar tools and efficiently mitigates missing input preconditions problems in unit testing for individual functions.

Key words: automated unit testing; program constraint; symbolic execution; static analysis;

[1] Li B, Vendome C, Linares-Vásquez M, Poshyvanyk D, Kraft N A. Automatically documenting unit test cases. In Proc. IEEE International Conference on the Software Testing, Verification and Validation, April 2016, pp.341-352.
[2] Lam W, Srisakaokul S, Bassett B, Mahdian P, Xie T, Tillmann N, de Halleux J. Parameterized unit testing in the open source wild. Technical Report, IDEALS, 2015., Dec. 2018.
[3] Zhang B, Hill E, Clause J. Towards automatically generating descriptive names for unit tests. In Proc. the 31st IEEE/ACM International Conference on Automated Software Engineering, September 2016, pp.625-636.
[4] Yoshida H, Tokumoto S, Prasad M R, Ghosh I, Uehara T. FSX:Fine-grained incremental unit test generation for C/C++ programs. In Proc. the 25th International Symposium on Software Testing and Analysis, July 2016, pp.106- 117.
[5] DeMilli R A, Offutt A J. Constraint-based automatic test data generation. IEEE Transactions on Software Engineering, 1991, 17(9):900-910.
[6] Boonstoppel P, Cadar C, Engler D. RWset:Attacking path explosion in constraint-based test generation. In Proc. the 14th International Conference on Tools and Algorithms for the Construction and Analysis of Systems, March 2008, pp.351-366.
[7] Boyer R S, Elspas B, Levitt K N. SELECT - A formal system for testing and debugging programs by symbolic execution. ACM SIGPLAN Notices, 1975, 10(6):234-245.
[8] Cadar C, Sen K. Symbolic execution for software testing:Three decades later. Communications of the ACM, 2013, 56(2):82-90.
[9] Cadar C, Dunbar D, Engler D R. KLEE:Unassisted and automatic generation of high-coverage tests for complex systems programs. In Proc. the 8th USENIX Symposium on Operating Systems Design and Implementation, December 2008, pp.209-224.
[10] Ganesh V, Dill D L. A decision procedure for bit-vectors and arrays. In Proc. the 19th International Conference on Computer Aided Verification, July 2007, pp.519-531.
[11] de Moura L, Bjørner N. Z3:An efficient SMT solver. In Proc. the 14th International Conference on Tools and Algorithms for the Construction and Analysis of Systems, March 2008, pp.337-340.
[12] Tillmann N, de Halleux J. Pex-white box test generation for.NET. In Proc. the 2nd International Conference on Tests and Proofs, April 2008, pp.134-153.
[13] Cadar C, Ganesh V, Pawlowski P M, Dill D L, Engler D R. EXE:Automatically generating inputs of death. ACM Transactions on Information and System Security, 2008, 12(2):Article No. 10.
[14] Engler D R, Dunbar D. Under-constrained execution:Making automatic code destruction easy and scalable. In Proc. the 2007 ACM/SIGSOFT International Symposium on Software Testing and Analysis, July 2007, pp.1-4.
[15] Burnim J, Sen K. Heuristics for scalable dynamic test generation. In Proc. the 23rd IEEE/ACM International Conference on Automated Software Engineering, September 2008, pp.443-446.
[16] Hutchins M, Foster H, Goradia T, Ostrand T. Experiments of the effectiveness of dataflow- and controlflow-based test adequacy criteria. In Proc. the 16th International Conference on Software Engineering, May 1994, pp.191-200.
[17] Xing Y, Gong Y Z, Wang Y W, Zhang X Z. Branch and bound framework for automatic test case generation. SCIENTIA SINICA Informationis, 2014, 44(10):1345-1360.
[18] Kernighan B W, Ritchie D M. The C Programming Language (2nd edition). Prentice hall, 1988.
[19] Zhang X Z, Gong Y Z, Wang Y W, Xing Y, Zhang M Z. Automated string constraints solving for programs containing string manipulation functions. Journal of Computer Science and Technology, 2017, 32(6):1125-1135.
[20] Aho A V, Sethi R, Ullman J D. Compilers:Principles, Techniques, and Tools. Addison-Wesley, 1986.
[21] Lin M X, Chen Y L, Yu K, Wu G S. Lazy symbolic execution for test data generation. IET Software, 2011, 5(2):132-141.
[22] Li G, Ghosh I. Lazy symbolic execution through abstraction and sub-space search. In Proc. the 9th International Haifa Verification Conference on Hardware and Software:Verification and Testing, November 2013, pp.295-310.
[23] Brack-Bernsen L, Hunger H. On the "Atypical Astronomical Cuneiform Text E":A mean-value scheme for predicting lunar latitude. Archiv fur Orientforschung, 2005, 51:96-107.
[24] Arcuri A, Iqbal M Z, Briand L. Formal analysis of the effectiveness and predictability of random testing. In Proc. the 19th International Symposium on Software Testing and Analysis, July 2010, pp.219-230.
[25] Sen K, Marinov D, Agha G. Cute:A concolic unit testing engine for C. In Proc. the 10th European Software Engineering Conference, September 2005, pp.263-272.
[26] Godefroid P, Levin M Y, Molnar D. SAGE:Whitebox fuzzing for security testing. Communications of the ACM, 2012, 55(3):40-44.
[27] Yoshida H, Li G, Kamiya T, Ghosh I, Rajan S, Tokumoto S, Munakata K, Uehara T. KLOVER:Automatic test generation for C and C++ programs, using symbolic execution. IEEE Software, 2017, 34(5):30-37.
[28] Ramos D A, Engler D R. Under-constrained symbolic execution:Correctness checking for real code. In Proc. the 24th USENIX Security Symposium, August 2015, pp.49-64.
[29] Nori A V, Rajamani S K. An empirical study of optimizations in YOGI. In Proc. the 32nd ACM/IEEE International Conference on Software Engineering, Volume 1, May 2010, pp.355-364.
[30] Zhang D, Liu D, Lei Y, Kung D, Csallner C, Wang W. Detecting vulnerabilities in C programs using trace-based testing. In Proc. the 2010 IEEE/IFIP International Conference on Dependable Systems Networks, June 2010, pp.241-250.
[31] Li H, Kim T, Bat-Erdene M, Lee H. Software vulnerability detection using backward trace analysis and symbolic execution. In Proc. the 2013 International Conference on Availability, Reliability and Security, September 2013, pp.446-454.
[32] Kim Y, Kim Y, Kim T, Lee G, Jang Y, Kim M. Automated unit testing of large industrial embedded software using concolic testing. In Proc. the 28th IEEE/ACM International Conference on Automated Software Engineering, November 2013, pp.519-528.
[1] Gen Zhang, Peng-Fei Wang, Tai Yue, Xu Zhou, Kai Lu. MEBS: Uncovering Memory Life-Cycle Bugs in Operating System Kernels [J]. Journal of Computer Science and Technology, 2021, 36(6): 1248-1268.
[2] Jung-Been Lee, Taek Lee, Hoh Peter In. Topic Modeling Based Warning Prioritization from Change Sets of Software Repository [J]. Journal of Computer Science and Technology, 2020, 35(6): 1461-1479.
[3] Feng-Juan Gao, Yu Wang, Lin-Zhang Wang, Zijiang Yang, Xuan-Dong Li. Automatic Buffer Overflow Warning Validation [J]. Journal of Computer Science and Technology, 2020, 35(6): 1406-1427.
[4] Gökçer Peynirci, Mete Eminaǧaoǧlu, Korhan Karabulut. Feature Selection for Malware Detection on the Android Platform Based on Differences of IDF Values [J]. Journal of Computer Science and Technology, 2020, 35(4): 946-962.
[5] Ling-Yun Situ, Student Member, CCF, Lin-Zhang Wang, Distinguished Member, CCF, Yang Liu, Member, ACM, IEEE, Bing Mao, Xuan-Dong Li, Fellow, CCF. Automatic Detection and Repair Recommendation for Missing Checks [J]. Journal of Computer Science and Technology, 2019, 34(5): 972-992.
[6] Ji Wang, Senior Member, CCF, Xiao-Dong Ma, Wei Dong, Hou-Feng Xu, and Wan-Wei Liu, Member, CCF. Demand-Driven Memory Leak Detection Based on Flow- and Context-Sensitive Pointer Analysis [J]. , 2009, 24(2): 347-356.
[7] ZHANG WenHui . Combining Static Analysis and Case-Based Search Space Partitioning for Reducing Peak Memory in Model Checking [J]. , 2003, 18(6): 0-0.
[8] LIAO Husheng;. An Action Analysis for Combining Partial Evaluation [J]. , 2000, 15(2): 196-201.
[9] Qu Yuzhong; Wang Zhijian; Xu Jiafu;. Denotational Semantics of a Simple Model of Eiffel [J]. , 1995, 10(3): 214-226.
[10] Liu Zongtian; Chen Fuan;. Research on Decompiling Technology [J]. , 1994, 9(4): 311-319.
Full text



[1] Liu Mingye; Hong Enyu;. Some Covering Problems and Their Solutions in Automatic Logic Synthesis Systems[J]. , 1986, 1(2): 83 -92 .
[2] Chen Shihua;. On the Structure of (Weak) Inverses of an (Weakly) Invertible Finite Automaton[J]. , 1986, 1(3): 92 -100 .
[3] Gao Qingshi; Zhang Xiang; Yang Shufan; Chen Shuqing;. Vector Computer 757[J]. , 1986, 1(3): 1 -14 .
[4] Chen Zhaoxiong; Gao Qingshi;. A Substitution Based Model for the Implementation of PROLOG——The Design and Implementation of LPROLOG[J]. , 1986, 1(4): 17 -26 .
[5] Huang Heyan;. A Parallel Implementation Model of HPARLOG[J]. , 1986, 1(4): 27 -38 .
[6] Min Yinghua; Han Zhide;. A Built-in Test Pattern Generator[J]. , 1986, 1(4): 62 -74 .
[7] Tang Tonggao; Zhao Zhaokeng;. Stack Method in Program Semantics[J]. , 1987, 2(1): 51 -63 .
[8] Min Yinghua;. Easy Test Generation PLAs[J]. , 1987, 2(1): 72 -80 .
[9] Zhu Hong;. Some Mathematical Properties of the Functional Programming Language FP[J]. , 1987, 2(3): 202 -216 .
[10] Li Minghui;. CAD System of Microprogrammed Digital Systems[J]. , 1987, 2(3): 226 -235 .

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
  Copyright ©2015 JCST, All Rights Reserved