Typestate-like analysis of multiple interacting objects

ABSTRACT

This paper presents a static analysis of typestate-like temporal specifications of groups of interacting objects, which are expressed using tracematches. Whereas typestate expresses a temporal specification of one object, a tracematch state may change due to operations on any of a set of related objects bound by the tracematch. The paper proposes a lattice-based operational semantics equivalent to the original tracematch semantics but better suited to static analysis. The paper defines a static analysis that computes precise local points-to sets and tracks the flow of individual objects, thereby enabling strong updates of the tracematch state. The analysis has been proved sound with respect to the semantics. A context-sensitive version of the analysis has been implemented as instances of the IFDS and IDE algorithms. The analysis was evaluated on tracematches used in earlier work and found to be very precise. Remaining imprecisions could be eliminated with more precise modeling of references from the heap and of exceptional control flow.

REFERENCES

• 1: Chris Allan , Pavel Avgustinov , Aske Simon Christensen , Laurie Hendren , Sascha Kuzins , Ondřej Lhoták , Oege de Moor , Damien Sereni , Ganesh Sittampalam , Julian Tibble, Adding trace matching with free variables to AspectJ, Proceedings of the 20th annual ACM SIGPLAN conference on Object oriented programming, systems, languages, and applications, October 16-20, 2005, San Diego, CA, USA
• 2: P. Avgustinov, A. Christensen, L. Hendren, S. Kuzins, J. Lhoták, O. Lhoták, O. de Moor, D. Sereni, G. Sittampalam, and J. Tibble. abc : An extensible AspectJ compiler. Transactions on Aspect-Oriented Software Development I, pages 293--334. 2006.
• 3: Pavel Avgustinov , Elnar Hajiyev , Neil Ongkingco , Oege de Moor , Damien Sereni , Julian Tibble , Mathieu Verbaere, Semantics of static pointcuts in aspectJ, Proceedings of the 34th annual ACM SIGPLAN-SIGACT symposium on Principles of programming languages, January 17-19, 2007, Nice, France
• 4: Pavel Avgustinov , Julian Tibble , Oege de Moor, Making trace monitors feasible, Proceedings of the 22nd annual ACM SIGPLAN conference on Object oriented programming systems and applications, October 21-25, 2007, Montreal, Quebec, Canada
• 5: Kevin Bierhoff , Jonathan Aldrich, Lightweight object specification with typestates, 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
• 6: Kevin Bierhoff , Jonathan Aldrich, Modular typestate checking of aliased objects, Proceedings of the 22nd annual ACM SIGPLAN conference on Object oriented programming systems and applications, October 21-25, 2007, Montreal, Quebec, Canada
• 7: Stephen M. Blackburn , Robin Garner , Chris Hoffmann , Asjad M. Khang , Kathryn S. McKinley , Rotem Bentzur , Amer Diwan , Daniel Feinberg , Daniel Frampton , Samuel Z. Guyer , Martin Hirzel , Antony Hosking , Maria Jump , Han Lee , J. Eliot B. Moss , B. Moss , Aashish Phansalkar , Darko Stefanović , Thomas VanDrunen , Daniel von Dincklage , Ben Wiedermann, The DaCapo benchmarks: java benchmarking development and analysis, Proceedings of the 21st annual ACM SIGPLAN conference on Object-oriented programming systems, languages, and applications, October 22-26, 2006, Portland, Oregon, USA
• 8: E. Bodden, L. Hendren, and O. Lhoták. A staged static program analysis to improve the performance of runtime monitoring. ECOOP '07: Proceedings of the 21st European Conference on Object-Oriented Programming, pages 525--549, 2007.
• 9: Eric Bodden , Patrick Lam , Laurie Hendren, Finding programming errors earlier by evaluating runtime monitors ahead-of-time, Proceedings of the 16th ACM SIGSOFT International Symposium on Foundations of software engineering, November 09-14, 2008, Atlanta, Georgia [doi>10.1145/1453101.1453109]
• 10: Feng Chen , Grigore Roşu, Mop: an efficient and generic runtime verification framework, Proceedings of the 22nd annual ACM SIGPLAN conference on Object oriented programming systems and applications, October 21-25, 2007, Montreal, Quebec, Canada
• 11: Sigmund Cherem , Radu Rugina, Compile-time deallocation of individual objects, Proceedings of the 5th international symposium on Memory management, June 10-11, 2006, Ottawa, Ontario, Canada [doi>10.1145/1133956.1133975]
• 12: Robert DeLine , Manuel Fähndrich, Enforcing high-level protocols in low-level software, Proceedings of the ACM SIGPLAN 2001 conference on Programming language design and implementation, p.59-69, June 2001, Snowbird, Utah, United States
• 13: R. DeLine and M. Fahndrich. Typestates for objects. ECOOP '04: Proceedings of the 18th European Conference on Object-Oriented Programming, pages 465--490, 2004.
• 14: A. Deutsch. A storeless model of aliasing and its abstractions using finite representations of right--regular equivalence relations. ICCL '92: Proceedings of the 4th IEEE International Conference on Computer Languages, pages 2--13, 1992.
• 15: B. Dufour. Objective quantification of program behaviour using dynamic metrics. Master's thesis, McGill University, 2004.
• 16: Matthew B. Dwyer , Rahul Purandare, Residual dynamic typestate analysis exploiting static analysis: results to reformulate and reduce the cost of dynamic analysis, Proceedings of the twenty-second IEEE/ACM international conference on Automated software engineering, November 05-09, 2007, Atlanta, Georgia, USA [doi>10.1145/1321631.1321651]
• 17: Stephen Fink , Eran Yahav , Nurit Dor , G. Ramalingam , Emmanuel Geay, Effective typestate verification in the presence of aliasing, Proceedings of the 2006 international symposium on Software testing and analysis, July 17-20, 2006, Portland, Maine, USA [doi>10.1145/1146238.1146254]
• 18: Stephen J. Fink , Eran Yahav , Nurit Dor , G. Ramalingam , Emmanuel Geay, Effective typestate verification in the presence of aliasing, ACM Transactions on Software Engineering and Methodology (TOSEM), v.17 n.2, p.1-34, April 2008 [doi>10.1145/1348250.1348255]
• 19: 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
• 20: Simon F. Goldsmith , Robert O'Callahan , Alex Aiken, Relational queries over program traces, Proceedings of the 20th annual ACM SIGPLAN conference on Object oriented programming, systems, languages, and applications, October 16-20, 2005, San Diego, CA, USA
• 21: S. Guyer and C. Lin. Client-driven pointer analysis. SAS '03: Proceedings of the 10th Annual International Static Analysis Symposium, pages 214--236, 2003.
• 22: Samuel Z. Guyer , Calvin Lin, Error checking with client-driven pointer analysis, Science of Computer Programming, v.58 n.1-2, p.83-114, October 2005 [doi>10.1016/j.scico.2005.02.005]
• 23: 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
• 24: 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
• 25: C. Jaspan and J. Aldrich. Checking semantic usage of frameworks. Library Centric Software Design Symposium, 2007.
• 26: C. Jaspan and J. Aldrich. Checking temporal relations between multiple objects. Technical Report CMU-ISR-08-119, Carnegie Mellon University, Dec. 2008.
• 27: H. Jonkers. Abstract storage structures. de Bakker and van Vliet, editors, Algorithmic Languages, pages 321--343, 1981.
• 28: Ond∨rej Lhoták, Comparing call graphs, Proceedings of the 7th ACM SIGPLAN-SIGSOFT workshop on Program analysis for software tools and engineering, p.37-42, June 13-14, 2007, San Diego, California, USA [doi>10.1145/1251535.1251542]
• 29: Michael Martin , Benjamin Livshits , Monica S. Lam, Finding application errors and security flaws using PQL: a program query language, Proceedings of the 20th annual ACM SIGPLAN conference on Object oriented programming, systems, languages, and applications, October 16-20, 2005, San Diego, CA, USA
• 30: N. Naeem and O. Lhoták. Extending typestate analysis to multiple interacting objects. Technical Report CS-2008-04, University of Waterloo, 2008. http://www.cs.uwaterloo.ca/research/tr/2008/CS-2008-04.pdf.
• 31: 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
• 32: Thomas Reps , Susan Horwitz , Mooly Sagiv, Precise interprocedural dataflow analysis via graph reachability, Proceedings of the 22nd ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.49-61, January 23-25, 1995, San Francisco, California, United States [doi>10.1145/199448.199462]
• 33: Mooly Sagiv , Thomas Reps , Susan Horwitz, Precise interprocedural dataflow analysis with applications to constant propagation, Theoretical Computer Science, v.167 n.1-2, p.131-170, Oct. 30, 1996
• 34: Mooly Sagiv , Thomas Reps , Reinhard Wilhelm, Solving shape-analysis problems in languages with destructive updating, ACM Transactions on Programming Languages and Systems (TOPLAS), v.20 n.1, p.1-50, Jan. 1998 [doi>10.1145/271510.271517]
• 35: 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

INDEX TERMS

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

General Terms:
Verification

Keywords:
static analysis, tracematches, typestate