Saturn: A scalable framework for error detection using Boolean satisfiability

ABSTRACT

This article presents Saturn, a general framework for building precise and scalable static error detection systems. Saturn exploits recent advances in Boolean satisfiability (SAT) solvers and is path sensitive, precise down to the bit level, and models pointers and heap data. Our approach is also highly scalable, which we achieve using two techniques. First, for each program function, several optimizations compress the size of the Boolean formulas that model the control flow and data flow and the heap locations accessed by a function. Second, summaries in the spirit of type signatures are computed for each function, allowing interprocedural analysis without a dramatic increase in the size of the Boolean constraints to be solved.

We have experimentally validated our approach by conducting two case studies involving a Linux lock checker and a memory leak checker. Results from the experiments show that our system scales well, parallelizes well, and finds more errors with fewer false positives than previous static error detection systems.

REFERENCES

• 1: Alfred V. Aho , Ravi Sethi , Jeffrey D. Ullman, Compilers: principles, techniques, and tools, Addison-Wesley Longman Publishing Co., Inc., Boston, MA, 1986
• 2: Alex Aiken , Jeffrey S. Foster , John Kodumal , Tachio Terauchi, Checking and inferring local non-aliasing, Proceedings of the ACM SIGPLAN 2003 conference on Programming language design and implementation, June 09-11, 2003, San Diego, California, USA
• 3: Ball, T., Cook, B., Levin, V., and Rajamani, S. 2004. SLAM and Static Driver Verifier: Technology transfer of formal methods inside Microsoft. In Proceedings of Fourth International Conference on Integrated Formal Methods. Springer, Berlin, Germany.
• 4: Thomas Ball , Sriram K. Rajamani, Automatically validating temporal safety properties of interfaces, Proceedings of the 8th international SPIN workshop on Model checking of software, p.103-122, May 2001, Toronto, Ontario, Canada
• 5: Randal E. Bryant, Graph-Based Algorithms for Boolean Function Manipulation, IEEE Transactions on Computers, v.35 n.8, p.677-691, August 1986 [doi>10.1109/TC.1986.1676819]
• 6: William R. Bush , Jonathan D. Pincus , David J. Sielaff, A static analyzer for finding dynamic programming errors, Software—Practice & Experience, v.30 n.7, p.775-802, June 2000 [doi>10.1002/(SICI)1097-024X(200006)30:7<775::AID-SPE309>3.0.CO;2-H]
• 7: Matthias Hauswirth , Trishul M. Chilimbi, Low-overhead memory leak detection using adaptive statistical profiling, Proceedings of the 11th international conference on Architectural support for programming languages and operating systems, October 07-13, 2004, Boston, MA, USA
• 8: Andy Chow Chou , Dawson Engler, Static analysis for bug finding in systems software, Stanford University, Stanford, CA, 2003
• 9: Clarke, E., Kroening, D., and Lerda, F. 2004a. A tool for checking ANSI-C programs. In Tools and Algorithms for the Construction and Analysis of Systems (TACAS), K. Jensen and A. Podelski, Eds. Lecture Notes in Computer Science, vol. 2988. Springer, Berlin, Germany, 168--176.
• 10: Edmund Clarke , Daniel Kroening , Natasha Sharygina , Karen Yorav, Predicate Abstraction of ANSI-C Programs Using SAT, Formal Methods in System Design, v.25 n.2-3, p.105-127, September-November 2004 [doi>10.1023/B:FORM.0000040025.89719.f3]
• 11: Manuvir Das , Sorin Lerner , Mark Seigle, ESP: path-sensitive program verification in polynomial time, Proceedings of the ACM SIGPLAN 2002 Conference on Programming language design and implementation, June 17-19, 2002, Berlin, Germany
• 12: Maryam Emami , Rakesh Ghiya , Laurie J. Hendren, Context-sensitive interprocedural points-to analysis in the presence of function pointers, Proceedings of the ACM SIGPLAN 1994 conference on Programming language design and implementation, p.242-256, June 20-24, 1994, Orlando, Florida, United States
• 13: Dawson Engler , Benjamin Chelf , Andy Chou , Seth Hallem, Checking system rules using system-specific, programmer-written compiler extensions, Proceedings of the 4th conference on Symposium on Operating System Design & Implementation, p.1-1, October 22-25, 2000, San Diego, California
• 14: David Evans, Static detection of dynamic memory errors, Proceedings of the ACM SIGPLAN 1996 conference on Programming language design and implementation, p.44-53, May 21-24, 1996, Philadelphia, Pennsylvania, United States
• 15: Jeffrey S. Foster , Tachio Terauchi , Alex Aiken, Flow-sensitive type qualifiers, Proceedings of the ACM SIGPLAN 2002 Conference on Programming language design and implementation, June 17-19, 2002, Berlin, Germany
• 16: Hackett, B. and Aiken, A. 2005. How is aliasing used in systems software? Tech. rep. Stanford University, Stanford, CA.
• 17: Brian Hackett , Radu Rugina, Region-based shape analysis with tracked locations, Proceedings of the 32nd ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.310-323, January 12-14, 2005, Long Beach, California, USA
• 18: Seth Hallem , Benjamin Chelf , Yichen Xie , Dawson Engler, A system and language for building system-specific, static analyses, Proceedings of the ACM SIGPLAN 2002 Conference on Programming language design and implementation, June 17-19, 2002, Berlin, Germany
• 19: Hastings, R. and Joyce, B. 1992. Purify: Fast detection of memory leaks and access errors. In Proceedings of the Winter USENIX Conference.
• 20: David L. Heine , Monica S. Lam, A practical flow-sensitive and context-sensitive C and C++ memory leak detector, Proceedings of the ACM SIGPLAN 2003 conference on Programming language design and implementation, June 09-11, 2003, San Diego, California, USA
• 21: Thomas A. Henzinger , Ranjit Jhala , Rupak Majumdar , Grégoire Sutre, Lazy abstraction, Proceedings of the 29th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.58-70, January 16-18, 2002, Portland, Oregon
• 22: Henzinger, T. A., Jhala, R., Majumdar, R., and Sutre, G. 2003. Software verification with Blast. In Proceedings of the SPIN 2003 Workshop on Model Checking Software. Lecture Notes in Computer Science, vol. 2648. Springer, Berlin, Germany, 235--239.
• 23: Daniel Jackson , Mandana Vaziri, Finding bugs with a constraint solver, Proceedings of the 2000 ACM SIGSOFT international symposium on Software testing and analysis, p.14-25, August 21-24, 2000, Portland, Oregon, United States
• 24: Khurshid, S., Pasareanu, C., and Visser, W. 2003. Generalized symbolic execution for model checking and testing. In Proceedings of the 9th International Conference on Tools and Algorithms for the Construction and Analysis of Systems. Springer, Berlin, Germany.
• 25: Edmund Clarke , Daniel Kroening , Karen Yorav, Behavioral consistency of C and verilog programs using bounded model checking, Proceedings of the 40th conference on Design automation, June 02-06, 2003, Anaheim, CA, USA [doi>10.1145/775832.775928]
• 26: William Landi , Barbara G. Ryder, A safe approximate algorithm for interprocedural aliasing, Proceedings of the ACM SIGPLAN 1992 conference on Programming language design and implementation, p.235-248, June 15-19, 1992, San Francisco, California, United States
• 27: Donglin Liang , Mary Jean Harrold, Efficient Computation of Parameterized Pointer Information for Interprocedural Analyses, Proceedings of the 8th International Symposium on Static Analysis, p.279-298, July 16-18, 2001
• 28: Matthew W. Moskewicz , Conor F. Madigan , Ying Zhao , Lintao Zhang , Sharad Malik, Chaff: engineering an efficient SAT solver, Proceedings of the 38th conference on Design automation, p.530-535, June 2001, Las Vegas, Nevada, United States [doi>10.1145/378239.379017]
• 29: Erik Ruf, Effective synchronization removal for Java, Proceedings of the ACM SIGPLAN 2000 conference on Programming language design and implementation, p.208-218, June 18-21, 2000, Vancouver, British Columbia, Canada
• 30: John Whaley , Martin Rinard, Compositional pointer and escape analysis for Java programs, Proceedings of the 14th ACM SIGPLAN conference on Object-oriented programming, systems, languages, and applications, p.187-206, November 01-05, 1999, Denver, Colorado, United States
• 31: Robert P. Wilson , Monica S. Lam, Efficient context-sensitive pointer analysis for C programs, Proceedings of the ACM SIGPLAN 1995 conference on Programming language design and implementation, p.1-12, June 18-21, 1995, La Jolla, California, United States
• 32: Xie, Y. and Chou, A. 2002. Path sensitive analysis using Boolean satisfiability. Tech. rep. Stanford University, Stanford, CA.
• 33: Lintao Zhang , Conor F. Madigan , Matthew H. Moskewicz , Sharad Malik, Efficient conflict driven learning in a boolean satisfiability solver, Proceedings of the 2001 IEEE/ACM international conference on Computer-aided design, November 04-08, 2001, San Jose, California

INDEX TERMS

Primary Classification:
  D. Software
  D.2 SOFTWARE ENGINEERING
      D.2.4 Software/Program Verification

Additional Classification:
  D. Software
  D.2 SOFTWARE ENGINEERING
      D.2.3 Coding Tools and Techniques
      D.2.5 Testing and Debugging

General Terms:
Algorithms, Experimentation, Languages, Verification

Keywords:
Boolean satisfiability, Program analysis, error detection