Dynamic inference of likely data preconditions over predicates by tree learning

ABSTRACT

We present a technique to infer likely data preconditions forprocedures written in an imperative programming language. Given a procedure and a set of predicates over its inputs, our technique enumerates different truth assignments to the predicates, deriving test cases from each feasible truth assignment. The predicates themselves are derived automatically using simple heuristics. The enumeration of truth assignments is performed using a propositional SAT solver along with a theory satisfiability checker capable of generating unsatisfiable cores.

For each assignment of truth values, a corresponding set of test cases are generated and executed. Based on the result of the execution, the truth assignment is classified as being safe or buggy. Finally, a decision tree classifier is used to generate a Boolean formula over the input predicates that explains the data obtained from the test cases. The resulting Boolean formula is, in effect, a likely data precondition for the procedure under consideration.

We apply our techniques on a wide variety of functions from the standard C library. Our experiments show that the proposed technique is quite robust. For most cases, it successfully learns a precondition that captures a safe and permissive calling environment.

REFERENCES

• 1: Mithun Acharya , Tao Xie , Jian Pei , Jun Xu, Mining API patterns as partial orders from source code: from usage scenarios to specifications, Proceedings of the the 6th joint meeting of the European software engineering conference and the ACM SIGSOFT symposium on The foundations of software engineering, September 03-07, 2007, Dubrovnik, Croatia [doi>10.1145/1287624.1287630]
• 2: 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
• 3: 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
• 4: Ball, T. A theory of predicate-complete test coverage. In FMCO (2004), pp. 1--22.
• 5: Chandrasekhar Boyapati , Sarfraz Khurshid , Darko Marinov, Korat: automated testing based on Java predicates, ACM SIGSOFT Software Engineering Notes, v.27 n.4, July 2002
• 6: 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]
• 7: Cadar, C., and Engler, D. R. Execution Generated Test Cases: How to make systems code crash itself. In SPIN (2005), vol. 3639 of LNCS, Springer-Verlag, pp. 2--23.
• 8: Patrick Cousot , Radhia Cousot, Abstract interpretation: a unified lattice model for static analysis of programs by construction or approximation of fixpoints, Proceedings of the 4th ACM SIGACT-SIGPLAN symposium on Principles of programming languages, p.238-252, January 17-19, 1977, Los Angeles, California [doi>10.1145/512950.512973]
• 9: Christoph Csallner , Nikolai Tillmann , Yannis Smaragdakis, DySy: dynamic symbolic execution for invariant inference, Proceedings of the 30th international conference on Software engineering, May 10-18, 2008, Leipzig, Germany [doi>10.1145/1368088.1368127]
• 10: 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
• 11: Michael Dean Ernst , David Notkin, Dynamically discovering likely program invariants, University of Washington, 2000
• 12: 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
• 13: Gogate, V., and Dechter, R. A new algorithm for sampling csp solution uniformly at random. In CP'07 (2007).
• 14: Thomas A. Henzinger , Ranjit Jhala , Rupak Majumdar, Permissive interfaces, 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
• 15: Ivančić, F., Yang, Z., Ganai, M. K., Gupta, A., and Ashar, P. F-Soft: Software verification platform. In Computer-Aided Verification (CAV 2005) (2005), vol. 3576 of LNCS, Springer-Verlag, pp. 301--306.
• 16: Daniel Jackson , Mandana Vaziri, Finding bugs with a constraint solver, ACM SIGSOFT Software Engineering Notes, v.25 n.5, p.14-25, Sept. 2000
• 17: Guofei Jiang , Haifeng Chen , Cristian Ungureanu , Kenji Yoshihira, Multi-resolution Abnormal Trace Detection Using Varied-length N-grams and Automata, Proceedings of the Second International Conference on Automatic Computing, p.111-122, June 13-16, 2005 [doi>10.1109/ICAC.2005.42]
• 18: Ted Kremenek , Paul Twohey , Godmar Back , Andrew Ng , Dawson Engler, From uncertainty to belief: inferring the specification within, Proceedings of the 7th symposium on Operating systems design and implementation, November 06-08, 2006, Seattle, Washington
• 19: Benjamin Robert Liblit , Alexander Aiken, Cooperative bug isolation, University of California at Berkeley, Berkeley, CA, 2004
• 20: Rupak Majumdar , Koushik Sen, Hybrid Concolic Testing, Proceedings of the 29th international conference on Software Engineering, p.416-426, May 20-26, 2007 [doi>10.1109/ICSE.2007.41]
• 21: Thomas M. Mitchell, Machine Learning, McGraw-Hill Higher Education, 1997
• 22: 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]
• 23: Moy, Y. Sufficient preconditions for modular assertion checking. In VMCAI'08 (2008), LNCS, Springer-Verlag.
• 24: George C. Necula , Scott McPeak , Westley Weimer, CCured: type-safe retrofitting of legacy code, Proceedings of the 29th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.128-139, January 16-18, 2002, Portland, Oregon
• 25: J. Ross Quinlan, C4.5: programs for machine learning, Morgan Kaufmann Publishers Inc., San Francisco, CA, 1993
• 26: J. R. Quinlan, Induction of Decision Trees, Machine Learning, v.1 n.1, p.81-106 [doi>10.1023/A:1022643204877]
• 27: Murali Krishna Ramanathan , Ananth Grama , Suresh Jagannathan, Static specification inference using predicate mining, Proceedings of the 2007 ACM SIGPLAN conference on Programming language design and implementation, June 10-13, 2007, San Diego, California, USA
• 28: Sriram Sankaranarayanan , Franjo Ivanči , Aarti Gupta, Mining library specifications using inductive logic programming, Proceedings of the 30th international conference on Software engineering, May 10-18, 2008, Leipzig, Germany [doi>10.1145/1368088.1368107]
• 29: Selman, B., Kautz, H., and Cohen, B. Local search strategies for satisfiability testing. DIMACS series on Discrete Mathematics and Theoretical Computer Science 26 (1996).
• 30: Koushik Sen , Darko Marinov , Gul Agha, CUTE: a concolic unit testing engine for C, 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
• 31: Mana Taghdiri , Robert Seater , Daniel Jackson, Lightweight extraction of syntactic specifications, Proceedings of the 14th ACM SIGSOFT international symposium on Foundations of software engineering, November 05-11, 2006, Portland, Oregon, USA [doi>10.1145/1181775.1181809]
• 32: Wei, W., Erenrich, J., and Selman, B. Towards efficient sampling: Exploiting random walk strategies. In AAAI'04 (2004).
• 33: 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
• 34: Yang, J., and Evans, D. Automatically discovering temporal properties for program verification, 2005. TR, Department of Computer Science, University of Virginia.

INDEX TERMS

Primary Classification:
  I. Computing Methodologies
  I.2 ARTIFICIAL INTELLIGENCE
      I.2.6 Learning
          Subjects: Induction

General Terms:
Theory, Verification

Keywords:
decision trees, machine learning, sat, software specification, verification