Deriving object typestates in the presence of inter-object references

ABSTRACT

We are interested in static analysis of Java classes with the goal of discovering the preconditions under which a certain program point within a method may be reached, taking into account the effects of previous method calls on an object of that class. The information pertinent to this computation is represented as the object's typestate, which is a finite set of relevant predicates that abstract the object's actual state. The execution of a method depends on an object's current typestate as well as other input parameters; the object may transition to a different typestate during the method's execution.It is common for objects to contain references to other ob-jects. In such cases, an object's behavior may depend on, in addition to its own state, the state of objects it has a refer-ence to. The main contribution of this paper is to discover relevant object typestates, as well as transitions between typestates, in the presence of inter-object references. Our analysis first performs a combined predicate discovery and predicate abstraction to derive "boolean" versions of Java classes given as input. It then uses abstract interpretation to compute the typestate transitions caused by method calls. A novel aspect of this work is that a set of Java classes is analyzed in isolation, without any client program being pro-vided. To do this, the analysis simulates all possible client's actions via a synthetic heap, all of whose interesting config-urations are explored by our analysis.The information we compute can be put to use in several ways. It can be used in checking whether a given client code erroneously uses a set of Java classes in a way that can throw an exception. It can also be used in creating test drivers for Java classes in order to exercise all relevant code paths in the corresponding methods.

REFERENCES

• 1: http://www.eclipse.org/, 2004.
• 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: Thomas Ball , Rupak Majumdar , Todd Millstein , Sriram K. Rajamani, Automatic predicate abstraction of C programs, Proceedings of the ACM SIGPLAN 2001 conference on Programming language design and implementation, p.203-213, June 2001, Snowbird, Utah, United States
• 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: Jong-Deok Choi , Manish Gupta , Mauricio Serrano , Vugranam C. Sreedhar , Sam Midkiff, Escape analysis for Java, Proceedings of the 14th ACM SIGPLAN conference on Object-oriented programming, systems, languages, and applications, p.1-19, November 01-05, 1999, Denver, Colorado, United States
• 6: Edmund M. Clarke , Orna Grumberg , Somesh Jha , Yuan Lu , Helmut Veith, Counterexample-Guided Abstraction Refinement, Proceedings of the 12th International Conference on Computer Aided Verification, p.154-169, July 15-19, 2000
• 7: Satyaki Das , David L. Dill, Counter-Example Based Predicate Discovery in Predicate Abstraction, Proceedings of the 4th International Conference on Formal Methods in Computer-Aided Design, p.19-32, November 06-08, 2002
• 8: R. DeLine and M. Fahndrich. Typestates for objects, 2004.
• 9: Brian Demsky , Martin Rinard, Role-based exploration of object-oriented programs, Proceedings of the 24th International Conference on Software Engineering, May 19-25, 2002, Orlando, Florida [doi>10.1145/581339.581379]
• 10: 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
• 11: Patrick Lam , Viktor Kuncak , Martin Rinard, Generalized typestate checking using set interfaces and pluggable analyses, ACM SIGPLAN Notices, v.39 n.3, March 2004 [doi>10.1145/981009.981016]
• 12: Tal Lev-Ami , Shmuel Sagiv, TVLA: A System for Implementing Static Analyses, Proceedings of the 7th International Symposium on Static Analysis, p.280-301, June 29-July 01, 2000
• 13: A. Loginov, T. Reps, and M. Sagiv. Abstraction refinement for 3-valued-logic analysis. Technical report, University of Wisconsin, Madison, WI, April 2004.
• 14: Mangala Gowri Nanda , S. Ramesh, Pointer analysis of multithreaded Java programs, Proceedings of the 2003 ACM symposium on Applied computing, March 09-12, 2003, Melbourne, Florida [doi>10.1145/952532.952741]
• 15: G. Ramalingam , Alex Warshavsky , John Field , Deepak Goyal , Mooly Sagiv, Deriving specialized program analyses for certifying component-client conformance, Proceedings of the ACM SIGPLAN 2002 Conference on Programming language design and implementation, June 17-19, 2002, Berlin, Germany
• 16: Mooly Sagiv , Thomas Reps , Reinhard Wilhelm, Parametric shape analysis via 3-valued logic, ACM Transactions on Programming Languages and Systems (TOPLAS), v.24 n.3, p.217-298, May 2002 [doi>10.1145/514188.514190]
• 17: R E Strom , S Yemini, Typestate: A programming language concept for enhancing software reliability, IEEE Transactions on Software Engineering, v.12 n.1, p.157-171, Jan. 1986
• 18: 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

INDEX TERMS

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

General Terms:
Languages, Verification

Keywords:
Java, alias analysis, heap analysis, interface specification, predicate abstraction