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