AI helps you reading Science

AI generates interpretation videos

AI extracts and analyses the key points of the paper to generate videos automatically


pub
Go Generating

AI Traceability

AI parses the academic lineage of this thesis


Master Reading Tree
Generate MRT

AI Insight

AI extracts a summary of this paper


Weibo:
This paper addresses the challenge of typestate verification, with acceptable precision, for real-world Java programs

Effective typestate verification in the presence of aliasing

ACM Transactions on Software Engineering and Methodology, no. 2 (2008): ArticleNo.9-ArticleNo.9

Cited by: 252|Views164
EI

Abstract

This article addresses the challenge of sound typestate verification, with acceptable precision, for real-world Java programs. We present a novel framework for verification of typestate properties, including several new techniques to precisely treat aliases without undue performance costs. In particular, we present a flow-sensitive, conte...More

Code:

Data:

0
Introduction
  • Checking if programs satisfy specified safety properties can help identify defects early in the development cycle, increasing productivity, reducing development costs, and improving quality and reliability.

    Typestate [32] is an elegant framework for specifying a class of temporal safety properties.
  • Checking if programs satisfy specified safety properties can help identify defects early in the development cycle, increasing productivity, reducing development costs, and improving quality and reliability.
  • Typestate can express the property that a Java program should not read data from java.net.Socket until the socket is connected.
  • This paper addresses the challenge of typestate verification, with acceptable precision, for real-world Java programs.
  • The authors focus on sound verification; if the verifier reports no problem, the program is guaranteed to satisfy the desired proper-
Highlights
  • Checking if programs satisfy specified safety properties can help identify defects early in the development cycle, increasing productivity, reducing development costs, and improving quality and reliability.

    Typestate [32] is an elegant framework for specifying a class of temporal safety properties
  • This paper addresses the challenge of typestate verification, with acceptable precision, for real-world Java programs
  • The pointer analysis relies on an SSA register-transfer language representation of each method, which gives a measure of flow-sensitivity for points-to sets of local variables [20]
  • When an object is created by a reflective call, the analysis assumes that the object will be cast to a declared type before being accessed. The analysis tracks these flows, and infers the type of object created by newInstance based on the declared type of relevant casts. We believe that this approximation is accurate for the vast majority of reflective factory methods in Java programs
  • The results show that our combination of techniques is relatively successful and efficient at verifying these typestate properties
  • Since our goal in this paper is the successful verification of typestate properties, we have deliberately chosen a set of mature benchmarks
Methods
  • Bytecode Stmts Contexts

    6.2 Sparsification

    To make the analysis scale, the authors rely on a lightweight sparsification[28] optimization prior to solving the IFDS problem.
  • The authors first consult the flow-insensitive points-to graph to conservatively determine all program variables that may appear in access-paths of depth at most k, which point to typestate objects of interest for a given property.
  • The authors prune the call graph to include only those nodes from which some relevant node is reachable, since the other nodes cannot modify the IFDS solution.
  • This pruning is particular important for the LocalFocus verifier.
  • Exploiting the pruning, the LocalFocus verifier can avoid making conservative assumptions for every method call, greatly increasing its precision
Results
  • 6.1 Implementation

    The preliminary flow-insensitive pointer analysis provides a mostly context-insensitive field-sensitive Andersen’s analysis [3], enhanced with a selective object sensitivity policy [26] to disambiguate contents of Java collection classes and I/O stream containers.
  • The pointer analysis names each context-sensitive allocation site as an instance key, and builds the call graph on-the-fly.
  • For these experiments, the authors configure the analysis to ignore some system libraries such as java.awt and javax.swing, which generally do not have side effects that affect the typestate properties of interest.
Conclusion
  • The results show that the combination of techniques is relatively successful and efficient at verifying these typestate properties.
  • The specJVM98 code’s use of PrintStream accounts for 241 of the 365 warnings reported.
  • These are all false positives, stemming from a few lines of code in the specJVM98 harness.
  • This program stores a PrintStream object in a static field Context.out, and uses the object ubiquitously throughout the various benchmarks.
  • The particular idiom by which the program caches the PrintStream object in a static field defeats the focus heuristics, leading to a loss of precision
Tables
  • Table1: Transfer functions for statements indicating how an incoming tuple o, unique, typestate, APmust, May, APmustNot is transformed, where pt(e) is the set of instance keys pointed-to by e in the flow-insensitive solution, v ∈ VarId. mayAlias(e1, e2) iff pointer analysis indicates e1 and e2 may point to the same instance key
  • Table2: Call graph characteristics for benchmarks
  • Table3: Typestate properties
  • Table4: Findings for the most precise (staged) solver across all benchmarks and typestate properties. Each entry in the table shows the number of warnings as a fraction of the number of PPFs, for each benchmark/property combination
Download tables as Excel
Related work
  • Many existing verification frameworks (e.g., [11, 4, 8]) use a two-phased approach, performing points-to analysis as a preceding phase, followed by typestate checking. This approach only supports weak updates as discussed in Sec. 3.3.

    The current version of ESP [13] uses an integrated approach, recording must and may alias information in a flow-sensitive manner. They observe that the may set becomes polluted and expensive to maintain, and even hint toward maintaining a must-not set as a possible future solution. In contrast, our approach adds must-not and also introduces the notions of uniqueness and focus, and uses staging to achieve increased scalability and precision.

    DeLine and Fahndrich [12] present a type system for typestate properties for objects. Their system guarantees that a program that typechecks has no typestate violations, and provides a modular, sound checker for object-oriented programs. To handle aliasing, they employ the adoption and focus operations to a linear type system, as described in [15]. With these operations, the type checker can assume must-alias properties for a limited program scope, and thus apply strong updates allowing typestate transitions. Our approach can prove correctness of a more general class of programs, since a context-sensitive analysis can accept programs for which an expression cannot be assigned a unique type at a given program point. Furthermore, our focus operation generates facts that can flow across arbitrary program scopes, in contrast to the limited program scope handled by [15]. On the other hand, our approach is non-modular and thus more expensive.
Reference
  • A. Aiken, J. S. Foster, J. Kodumal, and T. Terauchi. Checking and inferring local non-aliasing. ACM SIGPLAN Notices, 38(5):129–140, May 2003. In Conference on Programming Language Design and Implementation (PLDI).
    Google ScholarLocate open access versionFindings
  • R. Alur, P. Cerny, P. Madhusudan, and W. Nam. Synthesis of interface specifications for java classes. SIGPLAN Not., 40(1):98–109, 2005.
    Google ScholarLocate open access versionFindings
  • L. O. Andersen. Program Analysis and Specialization for the C Programming Language. PhD thesis, DIKU, Univ. of Copenhagen, May 1994. (DIKU report 94/19).
    Google ScholarFindings
  • T. Ball, R. Majumdar, T. Millstein, and S. Rajamani. Automatic predicate abstraction of C programs. In Proc. ACM Conf. on Programming Language Design and Implementation, pages 203–213, June 2001.
    Google ScholarLocate open access versionFindings
  • T. Ball and S. K. Rajamani. The Slam project: debugging system software via static analysis. ACM SIGPLAN Notices, 37(1):1–3, Jan. 2002.
    Google ScholarLocate open access versionFindings
  • D. R. Chase, M. Wegman, and F. K. Zadeck. Analysis of pointers and structures. ACM SIGPLAN Notices, 25(6):296–310, June 1990. In PLDI.
    Google ScholarLocate open access versionFindings
  • J.-D. Choi, M. Burke, and P. Carini. Efficient flow-sensitive interprocedural computation of pointer-induced aliases and side effects. In POPL 93, pages 232–245, 1993.
    Google ScholarLocate open access versionFindings
  • J. Corbett, M. Dwyer, J. Hatcliff, C. Pasareanu, Robby, S. Laubach, and H. Zheng. Bandera: Extracting finite-state models from Java source code. In Proc. Intl. Conf. on Software Eng., pages 439–448, June 2000.
    Google ScholarLocate open access versionFindings
  • P. Cousot and R. Cousot. Systematic design of program analysis frameworks. In Proc. ACM Symp. on Principles of Programming Languages, pages 269–282, New York, NY, 197ACM Press.
    Google ScholarLocate open access versionFindings
  • M. Das. Unification-based pointer analysis with directional assignments. ACM SIGPLAN Notices, 35(5):35–46, May 2000. In Conference on Programming Language Design and Implementation (PLDI).
    Google ScholarLocate open access versionFindings
  • M. Das, S. Lerner, and M. Seigle. ESP: path-sensitive program verification in polynomial time. ACM SIGPLAN Notices, 37(5):57–68, May 2002. In Conference on Programming Language Design and Implementation (PLDI).
    Google ScholarLocate open access versionFindings
  • R. DeLine and M. Fahndrich. Typestates for objects. In 18th European Conference on Object-Oriented Programming (ECOOP), volume 3086 of LNCS, June 2004.
    Google ScholarLocate open access versionFindings
  • N. Dor, S. Adams, M. Das, and Z. Yang. Software validation via scalable path-sensitive value flow analysis. In ISSTA, pages 12–22, 2004.
    Google ScholarLocate open access versionFindings
  • M. Emami, R. Ghiya, and L. J. Hendren. Context-sensitive interprocedural points-to analysis in the presence of function pointers. ACM SIGPLAN Notices, 29(6):242–256, June 1994. In Conference on Programming Language Design and Implementation (PLDI).
    Google ScholarLocate open access versionFindings
  • M. Fahndrich and R. DeLine. Adoption and focus: practical linear types for imperative programming. ACM SIGPLAN Notices, 37(5):13–24, May 2002. In Conference on Programming Language Design and Implementation (PLDI).
    Google ScholarLocate open access versionFindings
  • J. Field, D. Goyal, G. Ramalingam, and E. Yahav. Typestate verification: Abstraction techniques and complexity results. In Proc. of Static Analysis Symposium (SAS’03), volume 2694 of LNCS, pages 439–462. Springer, June 2003.
    Google ScholarLocate open access versionFindings
  • S. Fink, J. Dolby, and L. Colby. Semi-automatic J2EE transaction configuration. Technical Report RC23326, IBM, 2004.
    Google ScholarFindings
  • R. Gupta. Optimizing array bound checks using flow analysis. ACM Lett. Program. Lang. Syst., 2(1-4):135–150, 1993.
    Google ScholarLocate open access versionFindings
  • S. Guyer and C. Lin. Client-driven pointer analysis. In Proc. of SAS’03, volume 2694 of LNCS, pages 214–236, June 2003.
    Google ScholarLocate open access versionFindings
  • R. Hasti and S. Horwitz. Using static single assignment form to improve flow-insensitive pointer analysis. ACM SIGPLAN Notices, 33(5):97–105, May 1998. In Conference on Programming Language Design and Implementation (PLDI).
    Google ScholarLocate open access versionFindings
  • N. Heintze and O. Tardieu. Ultra-fast aliasing analysis using CLA: A million lines of C code in a second. ACM SIGPLAN Notices, 36(5):254–263, May 2001. In Conference on Programming Language Design and Implementation (PLDI).
    Google ScholarLocate open access versionFindings
  • T. A. Henzinger, R. Jhala, R. Majumdar, and G. Sutre. Lazy abstraction. In Symposium on Principles of Programming Languages, pages 58–70, 2002.
    Google ScholarLocate open access versionFindings
  • W. Landi and B. G. Ryder. A safe approximate algorithm for interprocedural aliasing. ACM SIGPLAN Notices, 27(7):235–248, July 1992. In Conference on Programming Language Design and Implementation (PLDI).
    Google ScholarLocate open access versionFindings
  • O. Lhotak and L. Hendren. Scaling Java points-to analysis using SPARK. In 12th International Conference on Compiler Construction (CC), volume 2622 of LNCS, pages 153–169, Apr. 2003.
    Google ScholarLocate open access versionFindings
  • B. Livshits, J. Whaley, and M. S. Lam. Reflection analysis for java. In Proceedings of Programming Languages and Systems: Third Asian Symposium, APLAS 2005, November 2005.
    Google ScholarLocate open access versionFindings
  • A. Milanova, A. Rountev, and B. G. Ryder. Parameterized object sensitivity for points-to analysis for java. ACM Trans. Softw. Eng. Methodol., 14(1):1–41, 2005.
    Google ScholarLocate open access versionFindings
  • J. Plevyak and A. A. Chien. Precise concrete type inference for object-oriented languages. ACM SIGPLAN Notices, 29(10):324–324, Oct. 1994. In Conference on Object-Oriented Programming Systems, Languages, and Applications (OOPSLA).
    Google ScholarLocate open access versionFindings
  • G. Ramalingam. On sparse evaluation representations. Theor. Comput. Sci., 277(1-2):119–147, 2002.
    Google ScholarLocate open access versionFindings
  • T. Reps, S. Horwitz, and M. Sagiv. Precise interprocedural dataflow analysis via graph reachability. In Conference record of POPL ’95, 22nd ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, pages 49–61, New York, NY, USA, 1995. ACM Press.
    Google ScholarLocate open access versionFindings
  • M. Sagiv, T. Reps, and R. Wilhelm. Parametric shape analysis via 3-valued logic. In Proc. ACM Symp. on Principles of Programming Languages, pages 105–118, 1999.
    Google ScholarLocate open access versionFindings
  • M. Sagiv, T. Reps, and R. Wilhelm. Parametric shape analysis via 3-valued logic. Transactions on Programming Languages and Systems (TOPLAS), 24(3):217–298, May 2002.
    Google ScholarLocate open access versionFindings
  • R. E. Strom and S. Yemini. Typestate: A programming language concept for enhancing software reliability. IEEE Trans. Software Eng., 12(1):157–171, 1986.
    Google ScholarLocate open access versionFindings
  • J. Whaley, M. Martin, and M. Lam. Automatic extraction of object-oriented component interfaces. In Proceedings of the International Symposium on Software Testing and Analysis, July 2002.
    Google ScholarLocate open access versionFindings
  • R. P. Wilson and M. S. Lam. Efficient context-sensitive pointer analysis for C programs. ACM SIGPLAN Notices, 30(6):1–12, June 1995. In Conference on Programming Language Design and Implementation (PLDI).
    Google ScholarLocate open access versionFindings
  • E. Yahav and G. Ramalingam. Verifying safety properties using separation and heterogeneous abstractions. In Proceedings of the ACM SIGPLAN 2004 conference on Programming language design and implementation, pages 25–34. ACM Press, 2004.
    Google ScholarLocate open access versionFindings
Your rating :
0

 

Tags
Comments
数据免责声明
页面数据均来自互联网公开来源、合作出版商和通过AI技术自动分析结果,我们不对页面数据的有效性、准确性、正确性、可靠性、完整性和及时性做出任何承诺和保证。若有疑问,可以通过电子邮件方式联系我们:report@aminer.cn
小科