Static specification inference using predicate mining

ABSTRACT

The reliability and correctness of complex software systems can be significantly enhanced through well-defined specifications that dictate the use of various units of abstraction (e.g., modules, or procedures). Often times, however, specifications are either missing, imprecise, or simply too complex to encode within a signature, necessitating specification inference. The process of inferring specifications from complex software systems forms the focus of this paper. We describe a static inference mechanism for identifying the preconditions that must hold whenever a procedure is called. These preconditions may reflect both data flow properties (e.g., whenever p is called, variable x must be non-null) as well as control-flow properties (e.g., every call to p must bepreceded by a call to q). We derive these preconditions using a ninter-procedural path-sensitive dataflow analysis that gathers predicates at each program point. We apply mining techniques to these predicates to make specification inference robust to errors. This technique also allows us to derive higher-level specifications that abstract structural similarities among predicates (e.g., procedure p is called immediately after a conditional test that checks whether some variable v is non-null.) We describe an implementation of these techniques, and validate the effectiveness of the approach on a number of large open-source benchmarks. Experimental results confirm that our mining algorithms are efficient, and that the specifications derived are both precise and useful-the implementation discovers several critical, yet previously, undocumented preconditions for well-tested libraries.

REFERENCES

• 1: Rakesh Agrawal , Ramakrishnan Srikant, Fast Algorithms for Mining Association Rules in Large Databases, Proceedings of the 20th International Conference on Very Large Data Bases, p.487-499, September 12-15, 1994
• 2: Rakesh Agrawal , Ramakrishnan Srikant, Mining Sequential Patterns, Proceedings of the Eleventh International Conference on Data Engineering, p.3-14, March 06-10, 1995
• 3: Rajeev Alur , Pavol Černý , P. Madhusudan , Wonhong Nam, Synthesis of interface specifications for Java classes, Proceedings of the 32nd ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.98-109, January 12-14, 2005, Long Beach, California, USA
• 4: Glenn Ammons , Rastislav Bodík , James R. Larus, Mining specifications, Proceedings of the 29th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.4-16, January 16-18, 2002, Portland, Oregon
• 5: Glenn Ammons , David Mandelin , Rastislav Bodík , James R. Larus, Debugging temporal specifications with concept analysis, Proceedings of the ACM SIGPLAN 2003 conference on Programming language design and implementation, June 09-11, 2003, San Diego, California, USA
• 6: Paul Anderson , Thomas Reps , Tim Teitelbaum, Design and Implementation of a Fine-Grained Software Inspection Tool, IEEE Transactions on Software Engineering, v.29 n.8, p.721-733, August 2003 [doi>10.1109/TSE.2003.1223646]
• 7: 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
• 8: Bruno Blanchet, A Computationally Sound Mechanized Prover for Security Protocols, Proceedings of the 2006 IEEE Symposium on Security and Privacy (S&P'06), p.140-154, May 21-24, 2006 [doi>10.1109/SP.2006.1]
• 9: D. Burdick, M. Calimlim, J. Flannick, J. Gehrke, and T. Yiu. Mafia: A performance study of mining maximal frequent itemsets. In Workshop on Frequent Itemset Mining Implementations (FIMI'03), 2003.
• 10: Miguel Castro , Manuel Costa , Tim Harris, Securing software by enforcing data-flow integrity, Proceedings of the 7th conference on USENIX Symposium on Operating Systems Design and Implementation, p.11-11, November 06-08, 2006, Seattle, WA
• 11: Brian Chin , Shane Markstrum , Todd Millstein, Semantic type qualifiers, Proceedings of the 2005 ACM SIGPLAN conference on Programming language design and implementation, June 12-15, 2005, Chicago, IL, USA
• 12: Corinna Cortes , Kathleen Fisher , Daryl Pregibon , Anne Rogers, Hancock: a language for extracting signatures from data streams, Proceedings of the sixth ACM SIGKDD international conference on Knowledge discovery and data mining, p.9-17, August 20-23, 2000, Boston, Massachusetts, United States [doi>10.1145/347090.347094]
• 13: Dawson Engler , David Yu Chen , Seth Hallem , Andy Chou , Benjamin Chelf, Bugs as deviant behavior: a general approach to inferring errors in systems code, Proceedings of the eighteenth ACM symposium on Operating systems principles, October 21-24, 2001, Banff, Alberta, Canada
• 14: Michael D. Ernst , Jake Cockrell , William G. Griswold , David Notkin, Dynamically Discovering Likely Program Invariants to Support Program Evolution, IEEE Transactions on Software Engineering, v.27 n.2, p.99-123, February 2001 [doi>10.1109/32.908957]
• 15: Jeffrey Fischer , Ranjit Jhala , Rupak Majumdar, Joining dataflow with predicates, Proceedings of the 10th European software engineering conference held jointly with 13th ACM SIGSOFT international symposium on Foundations of software engineering, September 05-09, 2005, Lisbon, Portugal
• 16: 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
• 17: Michael Furr , Jeffrey S. Foster, Checking type safety of foreign function calls, Proceedings of the 2005 ACM SIGPLAN conference on Programming language design and implementation, June 12-15, 2005, Chicago, IL, USA
• 18: 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
• 19: Dimitrios Gunopulos , Roni Khardon , Heikki Mannila , Sanjeev Saluja , Hannu Toivonen , Ram Sewak Sharma, Discovering all most specific sentences, ACM Transactions on Database Systems (TODS), v.28 n.2, p.140-174, June 2003 [doi>10.1145/777943.777945]
• 20: Thomas A. Henzinger , Ranjit Jhala , Rupak Majumdar, Permissive interfaces, ACM SIGSOFT Software Engineering Notes, v.30 n.5, September 2005
• 21: G. J. Holzmann. The SPIN Model Checker: Primer and Reference Manual. Addison-Wesley, 2004.
• 22: Ranjit Jhala , Rupak Majumdar, Path slicing, Proceedings of the 2005 ACM SIGPLAN conference on Programming language design and implementation, June 12-15, 2005, Chicago, IL, USA
• 23: Ted Kremenek , Paul Twohey , Godmar Back , Andrew Ng , Dawson Engler, From uncertainty to belief: inferring the specification within, Proceedings of the 7th conference on USENIX Symposium on Operating Systems Design and Implementation, p.12-12, November 06-08, 2006, Seattle, WA
• 24: P. Lam, V. Kuncak, and M. Rinard. Generalized typestate checking for data structure consistency. In VMCAI '05: Proceedings of 6th International Conference on Verification, Model Checking and Abstract Interpretation, pages 430--447, 2005.
• 25: Zhenmin Li , Shan Lu , Suvda Myagmar , Yuanyuan Zhou, CP-Miner: a tool for finding copy-paste and related bugs in operating system code, Proceedings of the 6th conference on Symposium on Opearting Systems Design & Implementation, p.20-20, December 06-08, 2004, San Francisco, CA
• 26: Zhenmin Li , Yuanyuan Zhou, PR-Miner: automatically extracting implicit programming rules and detecting violations in large software code, Proceedings of the 10th European software engineering conference held jointly with 13th ACM SIGSOFT international symposium on Foundations of software engineering, September 05-09, 2005, Lisbon, Portugal
• 27: Ben Liblit , Mayur Naik , Alice X. Zheng , Alex Aiken , Michael I. Jordan, Scalable statistical bug isolation, Proceedings of the 2005 ACM SIGPLAN conference on Programming language design and implementation, June 12-15, 2005, Chicago, IL, USA
• 28: Benjamin Livshits , Thomas Zimmermann, DynaMine: finding common error patterns by mining software revision histories, Proceedings of the 10th European software engineering conference held jointly with 13th ACM SIGSOFT international symposium on Foundations of software engineering, September 05-09, 2005, Lisbon, Portugal
• 29: David Mandelin , Lin Xu , Rastislav Bodík , Doug Kimelman, Jungloid mining: helping to navigate the API jungle, Proceedings of the 2005 ACM SIGPLAN conference on Programming language design and implementation, June 12-15, 2005, Chicago, IL, USA
• 30: Jens Palsberg, Closure analysis in constraint form, ACM Transactions on Programming Languages and Systems (TOPLAS), v.17 n.1, p.47-62, Jan. 1995 [doi>10.1145/200994.201001]
• 31: Murali Krishna Ramanathan , Ananth Grama , Suresh Jagannathan, Path-Sensitive Inference of Function Precedence Protocols, Proceedings of the 29th International Conference on Software Engineering, p.240-250, May 20-26, 2007 [doi>10.1109/ICSE.2007.63]
• 32: Martin Rinard , Cristian Cadar , Daniel Dumitran , Daniel M. Roy , Tudor Leu , William S. Beebee, Jr., Enhancing server availability and security through failure-oblivious computing, Proceedings of the 6th conference on Symposium on Opearting Systems Design & Implementation, p.21-21, December 06-08, 2004, San Francisco, CA
• 33: Olin Grigsby Shivers, Control-flow analysis of higher-order languages of taming lambda, Carnegie Mellon University, Pittsburgh, PA, 1991
• 34: W. Weimer and G. Necula. Mining temporal specifications for error detection. In TACAS '05: Eleventh International Conference on Tools and Algorithms for the Construction and Analysis of Systems, pages 461--476, April 2005.
• 35: John Whaley , Michael C. Martin , Monica S. Lam, Automatic extraction of object-oriented component interfaces, Proceedings of the 2002 ACM SIGSOFT international symposium on Software testing and analysis, July 22-24, 2002, Roma, Italy
• 36: Yichen Xie , Alex Aiken, Scalable error detection using boolean satisfiability, Proceedings of the 32nd ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.351-363, January 12-14, 2005, Long Beach, California, USA
• 37: Guizhen Yang, The complexity of mining maximal frequent itemsets and maximal frequent patterns, Proceedings of the tenth ACM SIGKDD international conference on Knowledge discovery and data mining, August 22-25, 2004, Seattle, WA, USA [doi>10.1145/1014052.1014091]
• 38: Jinlin Yang , David Evans , Deepali Bhardwaj , Thirumalesh Bhat , Manuvir Das, Perracotta: mining temporal API rules from imperfect traces, Proceeding of the 28th international conference on Software engineering, May 20-28, 2006, Shanghai, China [doi>10.1145/1134285.1134325]
• 39: Junfeng Yang , Paul Twohey , Dawson Engler , Madanlal Musuvathi, Using model checking to find serious file system errors, Proceedings of the 6th conference on Symposium on Opearting Systems Design & Implementation, p.19-19, December 06-08, 2004, San Francisco, CA

INDEX TERMS

Primary Classification:
  D. Software
  D.2 SOFTWARE ENGINEERING
      D.2.7 Distribution, Maintenance, and Enhancement
          Subjects: Documentation

Additional Classification:
  D. Software
  D.2 SOFTWARE ENGINEERING
      D.2.4 Software/Program Verification
          Subjects: Statistical methods

  F. Theory of Computation
  F.3 LOGICS AND MEANINGS OF PROGRAMS
      F.3.1 Specifying and Verifying and Reasoning about Programs

General Terms:
Algorithms, Documentation, Verification

Keywords:
preconditions, predicate mining, program analysis, specification inference