Type-based analysis and applications

ABSTRACT

Type-based analysis is an approach to static analysis of programs that has been studied for more than a decade. A type-based analysis assumes that the program type checks, and the analysis takes advantage of that. This paper examines the state of the art of type-based analysis, and it surveys some of the many software tools that use type-based analysis. Most of the surveyed tools use types as discriminators, while most of the theoretical studies use type and effect systems. We conclude that type-based analysis is a promising approach to achieving both provable correctness and good performance with a reasonable effort.

REFERENCES

• 1: Martín Abadi , Anindya Banerjee , Nevin Heintze , Jon G. Riecke, A core calculus of dependency, Proceedings of the 26th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.147-160, January 20-22, 1999, San Antonio, Texas, United States [doi>10.1145/292540.292555]
• 2: Alfred V. Aho , Ravi Sethi , Jeffrey D. Ullman, Compilers: principles, techniques, and tools, Addison-Wesley Longman Publishing Co., Inc., Boston, MA, 1986
• 3: Torben Amtoft, Minimal Thunkification, Proceedings of the Third International Workshop on Static Analysis, p.218-229, September 22-24, 1993
• 4: Andrew W. Appel, Modern compiler implementation in Java, Cambridge University Press, New York, NY, 1997
• 5: David F. Bacon , Peter F. Sweeney, Fast static analysis of C++ virtual function calls, Proceedings of the 11th ACM SIGPLAN conference on Object-oriented programming, systems, languages, and applications, p.324-341, October 06-10, 1996, San Jose, California, United States
• 6: David Francis Bacon. Fast and Effective Optimization of Statically Typed Object-Oriented Languages. PhD thesis, Computer Science Division, University of California, Berkeley, December 1997. Report No. UCB/CSD-98-1017.
• 7: Anindya Banerjee, A modular, polyvariant and type-based closure analysis, Proceedings of the second ACM SIGPLAN international conference on Functional programming, p.1-10, June 09-11, 1997, Amsterdam, The Netherlands
• 8: Lars Birkedal , Mads Tofte , Magnus Vejlstrup, From region inference to von Neumann machines via region representation inference, Proceedings of the 23rd ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.171-183, January 21-24, 1996, St. Petersburg Beach, Florida, United States [doi>10.1145/237721.237771]
• 9: Jan Vitek , Boris Bokowski, Confined types, Proceedings of the 14th ACM SIGPLAN conference on Object-oriented programming, systems, languages, and applications, p.82-96, November 01-05, 1999, Denver, Colorado, United States
• 10: Luca Cardelli. Type systems. In CRC Handbook of Computer Science and Engineering, chapter 103, pages 2208-2236. CRC Press, 1997.
• 11: L. Cardelli , J. Donahue , M. Jordan , B. Kalsow , G. Nelson, The Modula–3 type system, Proceedings of the 16th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.202-212, January 11-13, 1989, Austin, Texas, United States [doi>10.1145/75277.75295]
• 12: James C. Corbett , Matthew B. Dwyer , John Hatcliff , Shawn Laubach , Corina S. Păsăreanu , Robby , Hongjun Zheng, Bandera: extracting finite-state models from Java source code, Proceedings of the 22nd international conference on Software engineering, p.439-448, June 04-11, 2000, Limerick, Ireland [doi>10.1145/337180.337234]
• 13: Jeffrey Dean , David Grove , Craig Chambers, Optimization of Object-Oriented Programs Using Static Class Hierarchy Analysis, Proceedings of the 9th European Conference on Object-Oriented Programming, p.77-101, August 07-11, 1995
• 14: David Detlefs, K. Rustan Leino, Greg Nelson, and James Saxe. Extended static checking. Technical Report 159, Compaq Systems Research Center, 1998.
• 15: Allyn Dimock , Robert Muller , Franklyn Turbak , J. B. Wells, Strongly typed flow-directed representation transformations (extended abstract), Proceedings of the second ACM SIGPLAN international conference on Functional programming, p.11-24, June 09-11, 1997, Amsterdam, The Netherlands
• 16: Amer Diwan , Kathryn S. McKinley , J. Eliot B. Moss, Type-based alias analysis, Proceedings of the ACM SIGPLAN 1998 conference on Programming language design and implementation, p.106-117, June 17-19, 1998, Montreal, Quebec, Canada
• 17: Margaret A. Ellis , Bjarne Stroustrup, The annotated C++ reference manual, Addison-Wesley Longman Publishing Co., Inc., Boston, MA, 1990
• 18: Stephen J. Fink , Kathleen Knobe , Vivek Sarkar, Unified Analysis of Array and Object References in Strongly Typed Languages, Proceedings of the 7th International Symposium on Static Analysis, p.155-174, June 29-July 01, 2000
• 19: Adam Fischbach , John Hannan, Type Systems for Useless-Variable Elimination, Proceedings of the Second Symposium on Programs as Data Objects, p.25-38, May 21-23, 2001
• 20: Cormac Flanagan , Stephen N. Freund, Type-based race detection for Java, Proceedings of the ACM SIGPLAN 2000 conference on Programming language design and implementation, p.219-232, June 18-21, 2000, Vancouver, British Columbia, Canada
• 21: Sanjay Ghemawat , Keith H. Randall , Daniel J. Scales, Field analysis: getting useful and low-cost interprocedural information, Proceedings of the ACM SIGPLAN 2000 conference on Programming language design and implementation, p.334-344, June 18-21, 2000, Vancouver, British Columbia, Canada
• 22: Rajeev Gopal and Stephan R. Schach. Using automatic program decomposition techniques in software maintenance tools. In Proceedings of ICSM'89, International Conference on Software Maintenance, pages 132-141, 1989.
• 23: James Gosling , Bill Joy , Guy L. Steele, The Java Language Specification, Addison-Wesley Longman Publishing Co., Inc., Boston, MA, 1996
• 24: Christian Grothoff , Jens Palsberg , Jan Vitek, Encapsulating objects with confined types, Proceedings of the 16th ACM SIGPLAN conference on Object oriented programming, systems, languages, and applications, p.241-255, October 14-18, 2001, Tampa Bay, FL, USA
• 25: John Hannan. Type systems for closure conversions. In Proceedings of Workshop on Types for Program Analysis, pages 48-62, 1995.
• 26: Nevin Heintze, Control-Flow Analysis and Type Systems, Proceedings of the Second International Symposium on Static Analysis, p.189-206, September 25-27, 1995
• 27: Nevin Heintze , David McAllester, Linear-time subtransitive control flow analysis, Proceedings of the ACM SIGPLAN 1997 conference on Programming language design and implementation, p.261-272, June 16-18, 1997, Las Vegas, Nevada, United States
• 28: Susan Horwitz , Thomas Reps , David Binkley, Interprocedural slicing using dependence graphs, ACM Transactions on Programming Languages and Systems (TOPLAS), v.12 n.1, p.26-60, Jan. 1990 [doi>10.1145/77606.77608]
• 29: Antony L. Hosking , Nathaniel Nystrom , David Whitlock , Quintin Cutts , Amer Diwan, Partial redundancy elimination for access path expressions, Software—Practice & Experience, v.31 n.6, p.577-600, May 2001 [doi>10.1002/spe.371]
• 30: Suresh Jagannathan , Stephen Weeks , Andrew K. Wright, Type-Directed Flow Analysis for Typed Intermediate Languages, Proceedings of the 4th International Symposium on Static Analysis, p.232-249, September 08-10, 1997
• 31: Thomas P. Jensen, Inference of polymorphic and conditional strictness properties, Proceedings of the 25th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.209-221, January 19-21, 1998, San Diego, California, United States [doi>10.1145/268946.268964]
• 32: Pierre Jouvelot , David Gifford, Algebraic reconstruction of types and effects, Proceedings of the 18th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.303-310, January 21-23, 1991, Orlando, Florida, United States [doi>10.1145/99583.99623]
• 33: B. W. Kernighan , D. M. Ritchie, The C programming language, Prentice-Hall, Inc., Upper Saddle River, NJ, 1978
• 34: Naoki Kobayashi, Type-based useless variable elimination, Proceedings of the 2000 ACM SIGPLAN workshop on Partial evaluation and semantics-based program manipulation, p.84-93, January 22-23, 2000, Boston, Massachusetts, United States
• 35: T.-M. Kuo , P. Mishra, On strictness and its analysis, Proceedings of the 14th ACM SIGACT-SIGPLAN symposium on Principles of programming languages, p.144-155, January 21-23, 1987, Munich, West Germany [doi>10.1145/41625.41638]
• 36: Tsung-Min Kuo , Prateek Mishra, Strictness analysis: a new perspective based on type inference, Proceedings of the fourth international conference on Functional programming languages and computer architecture, p.260-272, September 11-13, 1989, Imperial College, London, United Kingdom [doi>10.1145/99370.99390]
• 37: J. M. Lucassen , D. K. Gifford, Polymorphic effect systems, Proceedings of the 15th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.47-57, January 10-13, 1988, San Diego, California, United States [doi>10.1145/73560.73564]
• 38: Robin Milner. A theory of type polymorphism in programming. Journal of Computer and System Sciences, 17:348-375, 1978.
• 39: Robin Milner , Mads Tofte , Robert Harper, The definition of Standard ML, MIT Press, Cambridge, MA, 1990
• 40: Greg Morrisett, Karl Crary, Neal Glew, Dan Grossman, Richard Samuels, Frederick Smith, David Walker, Stephanie Weirich, and Steve Zdancewic. Talx86: A realistic typed assembly language. ACM Workshop on Compiler Support for System Software, May 1999.
• 41: Greg Morrisett , David Walker , Karl Crary , Neal Glew, From system F to typed assembly language, Proceedings of the 25th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.85-97, January 19-21, 1998, San Diego, California, United States [doi>10.1145/268946.268954]
• 42: Christian Mossin, Exact Flow Analysis, Proceedings of the 4th International Symposium on Static Analysis, p.250-264, September 08-10, 1997
• 43: Christian Mossin. Flow Analysis of Typed Higher-Order Languages. PhD thesis, DIKU, University of Copenhagen, 1997.
• 44: Steven S. Muchnick, Advanced compiler design and implementation, Morgan Kaufmann Publishers Inc., San Francisco, CA, 1998
• 45: Greg Nelson, Systems programming with Modula-3, Prentice-Hall, Inc., Upper Saddle River, NJ, 1991
• 46: Flemming Nielson, The Typed lambda-Calculus with First-Class Processes, Proceedings of the Parallel Architectures and Languages Europe, Volume II: Parallel Languages, p.357-373, June 12-16, 1989
• 47: Flemming Nielson , Hanne Riis Nielson, Type and Effect Systems, Correct System Design, Recent Insight and Advances, (to Hans Langmaack on the occasion of his retirement from his professorship at the University of Kiel), p.114-136, January 1999
• 48: Flemming Nielson , Hanne R. Nielson , Chris Hankin, Principles of Program Analysis, Springer-Verlag New York, Inc., Secaucus, NJ, 1999
• 49: H. R. Nielson , F. Nielson, Automatic binding time analysis for a typed &lgr;-calculus, Science of Computer Programming, v.10 n.2, p.139-176, April 1988 [doi>10.1016/0167-6423(88)90025-1]
• 50: Tobias Nipkow , David von Oheimb, Java_light is type-safe—definitely, Proceedings of the 25th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.161-170, January 19-21, 1998, San Diego, California, United States [doi>10.1145/268946.268960]
• 51: Peter Trbik and Jens Palsberg. Trust in the calculus. Journal of Functional Programming, 7(6):557- 591, November 1997. Preliminary version in Proceedings of SAS'95, International Static Analysis Symposium, Springer-Verlag (LNCS 983), pages 314-330, Glasgow, Scotland, September 1995.
• 52: Jens Palsberg, Closure analysis in constraint form, ACM Transactions on Programming Languages and Systems (TOPLAS), v.17 n.1, p.47-62, Jan. 1995 [doi>10.1145/200994.201001]
• 53: Jens Palsberg , Christina Pavlopoulou, From polyvariant flow information to intersection and union types, Proceedings of the 25th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.197-208, January 19-21, 1998, San Diego, California, United States [doi>10.1145/268946.268963]
• 54: Jens Palsberg , Michael I. Schwartzbach, Object-oriented type inference, Conference proceedings on Object-oriented programming systems, languages, and applications, p.146-161, October 06-11, 1991, Phoenix, Arizona, United States
• 55: Jens Palsberg , Michael I. Schwartzbach, Object-oriented type systems, John Wiley and Sons Ltd., Chichester, UK, 1994
• 56: Jakob Rehof , Manuel Fähndrich, Type-base flow analysis: from polymorphic subtyping to CFL-reachability, Proceedings of the 28th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.54-66, January 2001, London, United Kingdom
• 57: Debra J. Richardson, TAOS: Testing with Analysis and Oracle Support, Proceedings of the 1994 ACM SIGSOFT international symposium on Software testing and analysis, p.138-153, August 17-19, 1994, Seattle, Washington, United States [doi>10.1145/186258.187158]
• 58: Zhong Shao , Valery Trifonov, Type-Directed Continuation Allocation, Proceedings of the Second International Workshop on Types in Compilation, p.116-135, March 25-27, 1998
• 59: Olin Grigsby Shivers, Control-flow analysis of higher-order languages of taming lambda, Carnegie Mellon University, Pittsburgh, PA, 1991
• 60: Geoffrey Smith , Dennis Volpano, Secure information flow in a multi-threaded imperative language, Proceedings of the 25th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.355-364, January 19-21, 1998, San Diego, California, United States [doi>10.1145/268946.268975]
• 61: Kirsten Solberg. Annotated Type Systems for Program Analysis. PhD thesis, University ofAarhus, 1995.
• 62: Kirsten Solberg, Hanne Riis Nielson, and Flemming Nielson. Strictness and totality analysis. In Proceedings of SAS'94, International Static Analysis Symposium, pages 408-422. Springer-Verlag (LNCS 864), 1994.
• 63: Kirsten Lackner Solberg, Strictness and Totality Analysis with Conjunction, Proceedings of the 6th International Joint Conference CAAP/FASE on Theory and Practice of Software Development, p.501-515, May 22-26, 1995
• 64: Vijay Sundaresan , Laurie Hendren , Chrislain Razafimahefa , Raja Vallée-Rai , Patrick Lam , Etienne Gagnon , Charles Godin, Practical virtual method call resolution for Java, Proceedings of the 15th ACM SIGPLAN conference on Object-oriented programming, systems, languages, and applications, p.264-280, October 2000, Minneapolis, Minnesota, United States
• 65: Peter F. Sweeney , Frank Tip, Extracting library-based object-oriented applications, Proceedings of the 8th ACM SIGSOFT international symposium on Foundations of software engineering: twenty-first century applications, p.98-107, November 06-10, 2000, San Diego, California, United States
• 66: Jean-Pierre Talpin , Pierre Jouvelot, The type and effect discipline, Information and Computation, v.111 n.2, p.245-296, June 1994 [doi>10.1006/inco.1994.1046]
• 67: Yan Mei Tang , Pierre Jouvelot, Separate Abstract Interpretation for Control-Flow Analysis, Proceedings of the International Conference on Theoretical Aspects of Computer Software, p.224-243, April 19-22, 1994
• 68: Yan Mei Tang , Pierre Jouvelot, Effect systems with subtyping, Proceedings of the 1995 ACM SIGPLAN symposium on Partial evaluation and semantics-based program manipulation, p.45-53, June 21-23, 1995, La Jolla, California, United States [doi>10.1145/215465.215552]
• 69: Peter Thiemann, Formalizing Resourve Allocation in a Compiler, Proceedings of the Second International Workshop on Types in Compilation, p.178-193, March 25-27, 1998
• 70: Frank Tip , Chris Laffra , Peter F. Sweeney , David Streeter, Practical experience with an application extractor for Java, Proceedings of the 14th ACM SIGPLAN conference on Object-oriented programming, systems, languages, and applications, p.292-305, November 01-05, 1999, Denver, Colorado, United States
• 71: Frank Tip , Jens Palsberg, Scalable propagation-based call graph construction algorithms, Proceedings of the 15th ACM SIGPLAN conference on Object-oriented programming, systems, languages, and applications, p.281-293, October 2000, Minneapolis, Minnesota, United States
• 72: Mads Tofte , Jean-Pierre Talpin, Region-based memory management, Information and Computation, v.132 n.2, p.109-176, Feb. 1, 1997 [doi>10.1006/inco.1996.2613]
• 73: Franklyn Turbak, Allyn Dimock, Robert Muller, and J. B. Wells. Compiling with polymorphic and polyvariant ow types. In ACM SIGPLAN Workshop on Types in Compilation, June 1997. http://www.cs.bc.edu/~muller/postscript/tic97.ps.Z.
• 74: Mark Weiser. Program slicing. IEEE Transactions on Software Engineering, 10(4):352-357, July 1984.
• 75: J. B. Wells , Allyn Dimock , Robert Muller , Franklyn Turbak, A calculus with polymorphic and polyvariant flow types, Journal of Functional Programming, v.12 n.3, p.183-227, May 2002 [doi>10.1017/S0956796801004245]
• 76: Andrew K. Wright, Typing references by effect inference, Symposium proceedings on 4th European symposium on programming, p.473-491, January 1992, Rennes, France
• 77: Andrew K. Wright , Matthias Felleisen, A syntactic approach to type soundness, Information and Computation, v.115 n.1, p.38-94, Nov. 15, 1994 [doi>10.1006/inco.1994.1093]
• 78: David A. Wright, A new technique for strictness analysis, Proceedings of the international joint conference on theory and practice of software development on Advances in distributed computing (ADC) and colloquium on combining paradigms for software development (CCPSD): Vol. 2, p.235-258, April 1991, Brighton, United Kingdom

INDEX TERMS

Primary Classification:
  F. Theory of Computation
  F.3 LOGICS AND MEANINGS OF PROGRAMS
      F.3.3 Studies of Program Constructs
          Subjects: Type structure

Additional Classification:
  F. Theory of Computation
  F.3 LOGICS AND MEANINGS OF PROGRAMS
      F.3.2 Semantics of Programming Languages
          Subjects: Program analysis

General Terms:
Algorithms