CUTE: a concolic unit testing engine for C

ABSTRACT

In unit testing, a program is decomposed into units which are collections of functions. A part of unit can be tested by generating inputs for a single entry function. The entry function may contain pointer arguments, in which case the inputs to the unit are memory graphs. The paper addresses the problem of automating unit testing with memory graphs as inputs. The approach used builds on previous work combining symbolic and concrete execution, and more specifically, using such a combination to generate test inputs to explore all feasible execution paths. The current work develops a method to represent and track constraints that capture the behavior of a symbolic execution of a unit with memory graphs as inputs. Moreover, an efficient constraint solver is proposed to facilitate incremental generation of such test inputs. Finally, CUTE, a tool implementing the method is described together with the results of applying CUTE to real-world examples of C code.

REFERENCES

• 1: T. Ball. Abstraction-guided test generation: A case study. Technical Report MSR-TR-2003-86, Microsoft Research.
• 2: C. W. Barrett and S. Berezin. CVC Lite: A new implementation of the cooperating validity checker. In Proc. 16th International Conference on Computer Aided Verification, pages 515--518, July 2004.
• 3: Dirk Beyer , Adam J. Chlipala , Rupak Majumdar, Generating Tests from Counterexamples, Proceedings of the 26th International Conference on Software Engineering, p.326-335, May 23-28, 2004
• 4: David L Bird , Carlos Urias Munoz, Automatic generation of random self-checking test cases, IBM Systems Journal, v.22 n.3, p.229-245, 1983
• 5: Chandrasekhar Boyapati , Sarfraz Khurshid , Darko Marinov, Korat: automated testing based on Java predicates, Proceedings of the 2002 ACM SIGSOFT international symposium on Software testing and analysis, July 22-24, 2002, Roma, Italy
• 6: C. Cadar and D. Engler. Execution generated test cases: How to make systems code crash itself. In Proc. of SPIN Workshop, 2005.
• 7: Koen Claessen , John Hughes, QuickCheck: a lightweight tool for random testing of Haskell programs, Proceedings of the fifth ACM SIGPLAN international conference on Functional programming, p.268-279, September 2000
• 8: Christoph Csallner , Yannis Smaragdakis, JCrasher: an automatic robustness tester for Java, Software—Practice & Experience, v.34 n.11, p.1025-1050, September 2004 [doi>10.1002/spe.602]
• 9: Christoph Csallner , Yannis Smaragdakis, Check 'n' crash: combining static checking and testing, Proceedings of the 27th international conference on Software engineering, May 15-21, 2005, St. Louis, MO, USA [doi>10.1145/1062455.1062533]
• 10: J. E. Forrester and B. P. Miller. An Empirical Study of the Robustness of Windows NT Applications Using Random Testing. In Proceedings of the 4th USENIX Windows System Symposium, 2000.
• 11: Patrice Godefroid , Nils Klarlund , Koushik Sen, DART: directed automated random testing, Proceedings of the 2005 ACM SIGPLAN conference on Programming language design and implementation, June 12-15, 2005, Chicago, IL, USA
• 12: Wolfgang Grieskamp , Yuri Gurevich , Wolfram Schulte , Margus Veanes, Generating finite state machines from abstract state machines, Proceedings of the 2002 ACM SIGSOFT international symposium on Software testing and analysis, July 22-24, 2002, Roma, Italy
• 13: Mary Lou Soffa , Aditya P. Mathur , Neelam Gupta, Generating Test Data for Branch Coverage, Proceedings of the 15th IEEE international conference on Automated software engineering, p.219, September 11-15, 2000
• 14: S. Khurshid, C. S. Pasareanu, and W. Visser. Generalized symbolic execution for model checking and testing. In Proc. 9th Int. Conf. on TACAS, pages 553--568, 2003.
• 15: B. Korel. A dynamic Approach of Test Data Generation. In IEEE Conference on Software Maintenance, pages 311--317, November 1990.
• 16: E. Larson and T. Austin. High coverage detection of input-related security faults. In Proc. of the 12th USENIX Security Symposium (Security '03), Aug. 2003.
• 17: lp_solve. http://groups.yahoo.com/group/lp_solve/.
• 18: J. McCarthy and J. Painter. Correctness of a compiler for arithmetic expressions. In Proceedings of Symposia in Applied Mathematics. AMS, 1967.
• 19: George C. Necula , Scott McPeak , Shree Prakash Rahul , Westley Weimer, CIL: Intermediate Language and Tools for Analysis and Transformation of C Programs, Proceedings of the 11th International Conference on Compiler Construction, p.213-228, April 08-12, 2002
• 20: A. Jefferson Offutt , J. Huffman Hayes, A semantic model of program faults, Proceedings of the 1996 ACM SIGSOFT international symposium on Software testing and analysis, p.195-200, January 08-10, 1996, San Diego, California, United States
• 21: C. Pacheco and M. D. Ernst. Eclat: Automatic generation and classification of test inputs. In 19th European Conference Object-Oriented Programming, 2005.
• 22: Parasoft. Jtest manuals version 6.0. Online manual, February 2005. http://www.parasoft.com/.
• 23: Corina S. Pasareanu , Matthew B. Dwyer , Willem Visser, Finding Feasible Counter-examples when Model Checking Abstracted Java Programs, Proceedings of the 7th International Conference on Tools and Algorithms for the Construction and Analysis of Systems, p.284-298, April 02-06, 2001
• 24: K. Sen, D. Marinov, and G. Agha. CUTE: A concolic unit testing engine for C. Technical Report UIUCDCS-R-2005-2597, UIUC, 2005.
• 25: SGLIB. http://xref-tech.com/sglib/main.html.
• 26: Valgrind. http://valgrind.org/.
• 27: Willem Visser , Corina S. Pǎsǎreanu , Sarfraz Khurshid, Test input generation with java PathFinder, Proceedings of the 2004 ACM SIGSOFT international symposium on Software testing and analysis, July 11-14, 2004, Boston, Massachusetts, USA
• 28: Srinivas Visvanathan , Neelam Gupta, Generating Test Data for Functions with Pointer Inputs, Proceedings of the 17th IEEE international conference on Automated software engineering, p.149, September 23-27, 2002
• 29: Tao Xie , Darko Marinov , David Notkin, Rostra: A Framework for Detecting Redundant Object-Oriented Unit Tests, Proceedings of the 19th IEEE international conference on Automated software engineering, p.196-205, September 20-24, 2004 [doi>10.1109/ASE.2004.61]
• 30: T. Xie, D. Marinov, W. Schulte, and D. Notkin. Symstra: A framework for generating object-oriented unit tests using symbolic execution. In Proc. of the Tools and Algorithms for the Construction and Analysis of Systems, 2005.

INDEX TERMS

Primary Classification:
  D. Software
  D.2 SOFTWARE ENGINEERING
      D.2.5 Testing and Debugging

General Terms:
Reliability, Verification

Keywords:
concolic testing, data structure testing, explicit path model-checking, random testing, testing C programs, unit testing