Universal symbolic execution and its application to likely data structure invariant generation

ABSTRACT

Local data structure invariants are asserted over a bounded fragment of a data structure around a distinguished node M of the data structure. An example of such an invariant for a sorted doubly linked list is "for all nodes M of the list, if M ≠ null and M.next ≠ null, then M.next.prev = M and M.value ≤ M.next.value." It has been shown that such local invariants are both natural and sufficient for describing a large class of data structures. This paper explores a novel technique, called Krystal, to infer likely local data structure invariants using a variant of symbolic execution, called universal symbolic execution. Universal symbolic execution is like traditional symbolic execution except the fact that we create a fresh symbolic variable for every read of a lvalue that has no mapping in the symbolic state rather than creating a symbolic variable only for inputs. This helps universal symbolic execution to symbolically track data flow for all memory locations along an execution even if input values do not flow directly into those memory locations. We have implemented our algorithm and applied it to several data structure implementations in Java. Our experimental results show that we can infer many interesting local invariants for these data structures.

REFERENCES

• 1: 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
• 2: Glenn Ammons , Rastislav Bodík , James R. Larus, Mining specifications, ACM SIGPLAN Notices, v.37 n.1, p.4-16, Jan. 2002
• 3: L. A. Clarke, A System to Generate Test Data and Symbolically Execute Programs, IEEE Transactions on Software Engineering, v.2 n.3, p.215-222, May 1976 [doi>10.1109/TSE.1976.233817]
• 4: P. David Coward, Symbolic execution systems—a review, Software Engineering Journal, v.3 n.6, p.229-239, Nov. 1988
• 5: 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]
• 6: B. Dutertre and L. M. de Moura. A fast linear-arithmetic solver for dpll(t). In Computer Aided Verification, volume 4144 of LNCS, pages 81--94, 2006.
• 7: 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]
• 8: Michael D. Ernst , Adam Czeisler , William G. Griswold , David Notkin, Quickly detecting relevant program invariants, Proceedings of the 22nd international conference on Software engineering, p.449-458, June 04-11, 2000, Limerick, Ireland [doi>10.1145/337180.337240]
• 9: M. D. Ernst, W. G. Griswold, Y. Kataokay, and D. Notkin. Dynamically discovering program invariants involving collections. In TR UW-CSE-99-11-02, University of Washington, 2000.
• 10: Cormac Flanagan , K. Rustan M. Leino , Mark Lillibridge , Greg Nelson , James B. Saxe , Raymie Stata, Extended static checking for Java, Proceedings of the ACM SIGPLAN 2002 Conference on Programming language design and implementation, June 17-19, 2002, Berlin, Germany
• 11: Cormac Flanagan , K. Rustan M. Leino, Houdini, an Annotation Assistant for ESC/Java, Proceedings of the International Symposium of Formal Methods Europe on Formal Methods for Increasing Software Productivity, p.500-517, March 12-16, 2001
• 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: Sudheendra Hangal , Monica S. Lam, Tracking down software bugs using automatic anomaly detection, Proceedings of the 24th International Conference on Software Engineering, May 19-25, 2002, Orlando, Florida [doi>10.1145/581339.581377]
• 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: James C. King, Symbolic execution and program testing, Communications of the ACM, v.19 n.7, p.385-394, July 1976 [doi>10.1145/360248.360252]
• 16: Gareth Lee , John Morris , Kris Parker , Gary A. Bundell , Peng Lam, Using symbolic execution to guide test generation: Research Articles, Software Testing, Verification & Reliability, v.15 n.1, p.41-61, March 2005 [doi>10.1002/stvr.v15:1]
• 17: F. Logozzo. Automatic inference of class invariants. In Proceedings of the 5th International Conference on Verification, Model Checking and Abstract Interpretation (VMCAI '04), January 2004.
• 18: M. Z. Malik, A. Pervaiz, , and S. Khurshid. Generating representation invariants of structurally complex data. In TACAS, pages 34--49, 2007.
• 19: S. McPeak and G. C. Necula. Data structure specifications via local equality axioms. In Proceedings of Computer Aided Verification (CAV), pages 476--490, 2005.
• 20: John C. Mitchell, Foundations of programming languages, MIT Press, Cambridge, MA, 1996
• 21: K. Sen, D. Marinov, and G. Agha. CUTE: A concolic unit testing engine for C. Technical Report UIUCDCS-R-2005-2597, UIUC, 2005.
• 22: 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
• 23: Mana Taghdiri , Daniel Jackson, Inferring specifications to detect errors in code, Automated Software Engineering, v.14 n.1, p.87-121, March 2007 [doi>10.1007/s10515-006-0005-x]
• 24: N. Tillmann, F. Chen, and W. Schulte. Discovering likely method specifications. In ICFEM, pages 717--736, 2006.
• 25: Raja Vallée-Rai , Phong Co , Etienne Gagnon , Laurie Hendren , Patrick Lam , Vijay Sundaresan, Soot - a Java bytecode optimization framework, Proceedings of the 1999 conference of the Centre for Advanced Studies on Collaborative research, p.13, November 08-11, 1999, Mississauga, Ontario, Canada
• 26: 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
• 27: 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
• 28: 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
• 29: T. Xie, D. Marinov, W. Schulte, and D. Notkin. Symstra: A framework for generating object-oriented unit tests using symbolic execution. In Procs. of TACAS, 2005.
• 30: Jinlin Yang , David Evans, Dynamically inferring temporal properties, Proceedings of the 5th ACM SIGPLAN-SIGSOFT workshop on Program analysis for software tools and engineering, June 07-08, 2004, Washington DC, USA [doi>10.1145/996821.996832]

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.5 Testing and Debugging
          Subjects: Symbolic execution

General Terms:
Design, Documentation, Reliability

Keywords:
dynamic analysis, execution traces, logical inference, program invariants, symbolic execution