An Abstract Domain to Infer Symbolic Ranges over Nonnegative Parameters

AbstractThe value range information of program variables is useful in many applications such as compiler optimization and program analysis. In the framework of abstract interpretation, the interval abstract domain infers numerical bounds for each program variable. However, in certain applications such as automatic parallelization, symbolic ranges are often desired. In this paper, we present a new numerical abstract domain, namely the abstract domain of parametric ranges, to infer symbolic ranges over nonnegative parameters for each program variable. The new domain is designed based on the insight that in certain contexts, program procedures often have nonnegative parameters, such as the length of an input list and the size of an input array. The domain of parametric ranges seeks to infer the lower and upper bounds for each program variable where each bound is a linear expression over nonnegative parameters. The time and memory complexity of the domain operations of parametric ranges is O(nm) where n is the number of program variables and m is the number of nonnegative parameters. On this basis, we show the application of parametric ranges to infer symbolic ranges of the sizes of list segments in programs manipulating singly-linked lists. Finally, we show preliminary experimental results