Calculating sized types

ABSTRACT

Many program optimisations and analyses, such as array-bound checking, termination analysis, etc, depend on knowing the size of a function's input and output. However, size information can be difficult to compute. Firstly, accurate size computation requires detecting size relation between different inputs of a function. Secondly, different optimisations and analyses may require slightly different size information, and thus slightly different computation. Literature in size computation has mainly concentrated on size checking, instead of inferencing. In this paper, we provide a generic framework on which different size variants can be expressed and computed. We also describe an effective algorithm for inferring, instead of checking, size information. Size information are expressed in terms of Presburger formulae, and our algorithm utilises the Omega Calculator to compute as exact a size information as possible, within the linear arithmetic capability.

REFERENCES

• 1: A. Bossi , N. Cocco , M. Fabris, Typed norms, Symposium proceedings on 4th European symposium on programming, p.73-92, January 1992, Rennes, France
• 2: Alexander Brodsky , Yehoshua Sagiv, Inference of inequality constraints in logic programs (extended abstracts), Proceedings of the tenth ACM SIGACT-SIGMOD-SIGART symposium on Principles of database systems, p.227-240, May 29-31, 1991, Denver, Colorado, United States [doi>10.1145/113413.113434]
• 3: Wei-Ngan Chin , Masami Hagiya, A bounds inference method for vector-based memoization, Proceedings of the second ACM SIGPLAN international conference on Functional programming, p.176-187, June 09-11, 1997, Amsterdam, The Netherlands
• 4: W.N. Chin and S.C. Khoo. Calculating sized types. In Technical Report, DISCS, NUS, December 1999.
• 5: Patrick Cousot , Nicolas Halbwachs, Automatic discovery of linear restraints among variables of a program, Proceedings of the 5th ACM SIGACT-SIGPLAN symposium on Principles of programming languages, p.84-96, January 23-25, 1978, Tucson, Arizona [doi>10.1145/512760.512770]
• 6: D. De Schreye and S Decorte. Termination of logic programs: The never-ending story.Journal of Logic Programming, 19/20:199-260, 1994.
• 7: Arne J. Glenstrup , Neil D. Jones, BTA Algorithms to Ensure Termination of Off-Line Partial Evaluation, Proceedings of the Second International Andrei Ershov Memorial Conference on Perspectives of System Informatics, p.273-284, June 25-28, 1996
• 8: Carsten Kehler Holst, Finiteness analysis, Proceedings of the 5th ACM conference on Functional programming languages and computer architecture, p.473-495, June 1991, Cambridge, Massachusetts, United States
• 9: John Hughes , Lars Pareto , Amr Sabry, Proving the correctness of reactive systems using sized types, Proceedings of the 23rd ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.410-423, January 21-24, 1996, St. Petersburg Beach, Florida, United States [doi>10.1145/237721.240882]
• 10: P. Kelly, V. Maslov, W. Pugh, E. Rosser, T. Shpeisman, and D. Wonnacott. The omega library version 1.1.0 interface guide. Technical report, University of Maryland, College Park, November 1996. http : //www. cs. umd. edu/pro j ects/omega.
• 11: Wayne Kelly , William Pugh , Evan Rosser , Tatiana Shpeisman, Transitive closure of infinite graphs and its applications, University of Maryland at College Park, College Park, MD, 1994
• 12: Lutz Plümer, Termination proofs for logic programs, Springer-Verlag New York, Inc., New York, NY, 1990
• 13: William Pugh, A practical algorithm for exact array dependence analysis, Communications of the ACM, v.35 n.8, p.102-114, Aug. 1992 [doi>10.1145/135226.135233]
• 14: Kirack Sohn , Allen Van Gelder, Termination detection in logic programs using argument sizes (extended abstract), Proceedings of the tenth ACM SIGACT-SIGMOD-SIGART symposium on Principles of database systems, p.216-226, May 29-31, 1991, Denver, Colorado, United States [doi>10.1145/113413.113433]
• 15: Chris Speirs , Zoltan Somogyi , Harald Søndergaard, Termination Analysis for Mercury, Proceedings of the 4th International Symposium on Static Analysis, p.160-171, September 08-10, 1997
• 16: Jeffrey D. Ullman , Allen Van Gelder, Efficient tests for top-down termination of logical rules, Journal of the ACM (JACM), v.35 n.2, p.345-373, April 1988 [doi>10.1145/42282.42285]
• 17: Hongwei Xi , Frank Pfenning, Eliminating array bound checking through dependent types, Proceedings of the ACM SIGPLAN 1998 conference on Programming language design and implementation, p.249-257, June 17-19, 1998, Montreal, Quebec, Canada
• 18: Hongwei Xi , Frank Pfenning, Dependent types in practical programming, Proceedings of the 26th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.214-227, January 20-22, 1999, San Antonio, Texas, United States [doi>10.1145/292540.292560]

INDEX TERMS

Primary Classification:
  F. Theory of Computation
  F.3 LOGICS AND MEANINGS OF PROGRAMS

Additional Classification:
  D. Software
  D.3 PROGRAMMING LANGUAGES

General Terms:
Design, Languages, Verification