Program Analysis Using Symbolic RangesSriram Sankaranarayanan , Franjo Ivancic, and Aarti Gupta |
|
Interval analysis seeks static lower and upper bounds on the values of
program variables. These bounds are useful, especially for inferring
invariants to prove buffer overflow checks. In practice, however,
intervals by themselves are inadequate as invariants due to the lack
of relational information among the variables.
In this paper, we present a technique for deriving symbolic bounds on the variable values. We study a restricted class of polyhedra whose constraints are stratified with respect to some variable ordering provided by the user, or chosen heuristically. We define a notion of normalization for such constraints and demonstrate polynomial time domain operations on the resulting domain of symbolic range constraints. The abstract domain is intended to complement widely used domains such as intervals and octagons for use in buffer overflow analysis. Finally, we study the impact of our analysis on commercial software using an overflow analyzer for the C language.
|
| ps pdf |
| Static Analysis Symposium (SAS 2007), volume 4634 of Lecture Notes in Computer Science, pp. 366-383, Springer-Verlag. |
| Copyright (C) Springer-Verlag. Copy has been made available online for personal use only. Do not redistribute without permission. |