Nomair A. Naeem
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.
- C. Allan, P. Avgustinov, A. Christensen, L. Hendren, S. Kuzins, O. Lhoták, O. de Moor, D. Sereni, G. Sittampalam, and J. Tibble. Adding trace matching with free variables to AspectJ. OOPSLA '05: Proceedings of the 20th ACM SIGPLAN Conference on Object Oriented Programming Systems and Applications, pages 345--364, 2005. Google Scholar
Digital Library
- 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. Google ScholarDigital Library
- P. Avgustinov, E. Hajiyev, N. Ongkingco, O. de Moor, D. Sereni, J. Tibble, and M. Verbaere. Semantics of static pointcuts in AspectJ. POPL '07: Proceedings of the 34th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, pages 11--23, 2007. Google ScholarDigital Library
- P. Avgustinov, J. Tibble, and O. de Moor. Making trace monitors feasible. OOPSLA '07: Proceedings of the 22nd ACM SIGPLAN Conference on Object Oriented Programming Systems and Applications, pages 589--608, 2007. Google ScholarDigital Library
- K. Bierhoff and J. Aldrich. Lightweight object specification with typestates. ESEC/FSE 2005: Proceedings of the Joint 10th European Software Engineering Conference (ESEC) and the 13th ACM SIGSOFT Symposium on the Foundations of Software Engineering (FSE-13), pages 217--226, 2005. Google ScholarDigital Library
- K. Bierhoff and J. Aldrich. Modular typestate checking of aliased objects. OOPSLA '07: Proceedings of the 22nd ACM SIGPLAN Conference on Object Oriented Programming Systems and Applications, pages 301--320, 2007. Google ScholarDigital Library
- S. Blackburn, R. Garner, C. Hoffman, A. Khan, K. McKinley, R. Bentzur, A. Diwan, D. Feinberg, D. Frampton, S. Guyer, M. Hirzel, A. Hosking, M. Jump, H. Lee, E. Moss, A. Phansalkar, D. Stefanović, T. VanDrunen, D. von Dincklage, and B. Wiedermann. The DaCapo benchmarks: Java benchmarking development and analysis. OOPSLA '06: Proceedings of the 21st ACM SIGPLAN Conference on Object Oriented Programming Systems and Applications, 2006. Google ScholarDigital Library
- 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. Google ScholarDigital Library
- E. Bodden, P. Lam, and L. Hendren. Finding programming errors earlier by evaluating runtime monitors ahead-of-time. FSE 2008: ACM SIGSOFT International Symposium on the Foundations of Software Engineering, Nov. 2008. Google ScholarDigital Library
- F. Chen and G. Roşu. Mop: an efficient and generic runtime verification framework. OOPSLA '07: Proceedings of the 22nd ACM SIGPLAN Conference on Object Oriented Programming Systems and Applications, pages 569--588, 2007. Google ScholarDigital Library
- S. Cherem and R. Rugina. Compile--time deallocation of individual objects. ISMM '06: Proceedings of the 2006 International Symposium on Memory Management, pages 138--149, 2006. Google ScholarDigital Library
- R. DeLine and M. Fahndrich. Enforcing high-level protocols in low-level software. PLDI '01: Proceedings of the 2001 ACM SIGPLAN Conference on Programming Language Design and Implementation, pages 59--69, 2001. Google ScholarDigital Library
- R. DeLine and M. Fahndrich. Typestates for objects. ECOOP '04: Proceedings of the 18th European Conference on Object-Oriented Programming, pages 465--490, 2004.Google ScholarCross Ref
- 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.Google ScholarCross Ref
- B. Dufour. Objective quantification of program behaviour using dynamic metrics. Master's thesis, McGill University, 2004.Google Scholar
- M. B. Dwyer and R. Purandare. Residual dynamic typestate analysis: exploiting static analysis results to reformulate and reduce the cost of dynamic analysis. ASE '07: Proceedings of the twenty-second IEEE/ACM International Conference on Automated Software Engineering, pages 124--133, New York, NY, USA, 2007. ACM. Google ScholarDigital Library
- S. Fink, E. Yahav, N. Dor, G. Ramalingam, and E. Geay. Effective typestate verification in the presence of aliasing. ISSTA '06: Proceedings of the International Symposium on Software Testing and Analysis, pages 133--144, 2006. Google ScholarDigital Library
- S. J. Fink, E. Yahav, N. Dor, G. Ramalingam, and E. Geay. Effective typestate verification in the presence of aliasing. ACM Trans. Softw. Eng. Methodol., 17(2):1--34, 2008. Google ScholarDigital Library
- J. Foster, T. Terauchi, and A. Aiken. Flow--sensitive type qualifiers. PLDI '02: Proceedings of the 2002 ACM SIGPLAN Conference on Programming Language Design and Implementation, pages 1--12, 2002. Google ScholarDigital Library
- S. Goldsmith, R. O'Callahan, and A. Aiken. Relational queries over program traces. OOPSLA '05: Proceedings of the 20th ACM SIGPLAN Conference on Object Oriented Programming Systems and Applications, pages 385--402, 2005. Google ScholarDigital Library
- S. Guyer and C. Lin. Client-driven pointer analysis. SAS '03: Proceedings of the 10th Annual International Static Analysis Symposium, pages 214--236, 2003. Google ScholarDigital Library
- S. Guyer and C. Lin. Error checking with client-driven pointer analysis. Sci. Comput. Program., 58(1--2):83--114, 2005. Google ScholarDigital Library
- B. Hackett and R. Rugina. Region-based shape analysis with tracked locations. POPL '05: Proceedings of the 32nd ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, pages 310--323, 2005. Google ScholarDigital Library
- S. Hallem, B. Chelf, Y. Xie, and D. Engler. A system and language for building system-specific, static analyses. PLDI '02: Proceedings of the 2002 ACM SIGPLAN Conference on Programming Language Design and Implementation, pages 69--82, 2002. Google ScholarDigital Library
- C. Jaspan and J. Aldrich. Checking semantic usage of frameworks. Library Centric Software Design Symposium, 2007. Google ScholarDigital Library
- C. Jaspan and J. Aldrich. Checking temporal relations between multiple objects. Technical Report CMU-ISR-08-119, Carnegie Mellon University, Dec. 2008.Google ScholarCross Ref
- H. Jonkers. Abstract storage structures. de Bakker and van Vliet, editors, Algorithmic Languages, pages 321--343, 1981.Google Scholar
- O. Lhoták. Comparing call graphs. PASTE '07: Proceedings of the 7th ACM SIGPLAN-SIGSOFT Workshop on Program Analysis for Software Tools and Engineering, pages 37--42, 2007. Google ScholarDigital Library
- M. Martin, B. Livshits, and M. S. Lam. Finding application errors and security flaws using PQL: a program query language. OOPSLA '05: Proceedings of the 20th ACM SIGPLAN Conference on Object Oriented Programming Systems and Applications, pages 365--383, 2005. Google ScholarDigital Library
- 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.Google Scholar
- G. Ramalingam, A. Warshavsky, J. Field, D. Goyal, and M. Sagiv. Deriving specialized program analyses for certifying component-client conformance. PLDI '02: Proceedings of the 2002 ACM SIGPLAN Conference on Programming Language Design and Implementation, pages 83--94, 2002. Google ScholarDigital Library
- T. Reps, S. Horwitz, and M. Sagiv. Precise interprocedural dataflow analysis via graph reachability. POPL '95: Proceedings of the 22nd ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, pages 49--61, 1995. Google ScholarDigital Library
- M. Sagiv, T. Reps, and S. Horwitz. Precise interprocedural dataflow analysis with applications to constant propagation. Theoretical Computer Science, 167(1--2):131--170, 1996. Google ScholarDigital Library
- M. Sagiv, T. Reps, and R. Wilhelm. Solving shape--analysis problems in languages with destructive updating. ACM TOPLAS, 20(1):1--50, Jan. 1998. Google ScholarDigital Library
- R. E. Strom and S. Yemini. Typestate: A programming language concept for enhancing software reliability. IEEE Trans. Softw. Eng., 12(1):157--171, 1986. Google ScholarDigital Library
Index Terms
- Typestate-like analysis of multiple interacting objects
Recommendations
Typestate-like analysis of multiple interacting objects
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 ...
The Clara framework for hybrid typestate analysis
A typestate property describes which operations are available on an object or a group of inter-related objects, depending on this object's or group's internal state, the typestate. Researchers in the field of static analysis have devised static program ...
Validating temporal properties of interacting objects
OOPSLA Companion '08: Companion to the 23rd ACM SIGPLAN conference on Object-oriented programming systems languages and applicationsFor a single object, many programming errors can be detected by specifying the undesirable sequence of events using typestate. However, since objects interact with one another, defining temporal specifications only for a single object is too ...
Comments