Grid domains for analysing software

摘要

Static analysis is the determination of correct though approximate information about the be- haviour of a system, this approach is used to detect and locate programming errors or to certify the absence of such bugs. Abstract interpretation is a static program analysis method that uses abstract domains to provide a convenient but approximate representation of the accumulated in- formation during the evaluation of a program. The focus of this thesis is to investigate numerical abstract domains that capture the distribution or patterns of values the program properties can take. There has already been a considerable amount of research into numerical abstract domains and a wide variety of such domains have been specified each providing a different degree of pre- cision and efficiency. For instance the domain of convex polyhedra is precise but has exponential complexity while the interval or box domain is much less precise but has linear complexity. Note that these domains do not capture the distribution information which is the focus of this thesis. In the first part of this thesis we introduce the domain of grids. This domain interprets the patterns of distribution of the values that the program properties can take. The complete grid domain can interpret the relationships which hold between variables or properties in a program. There are two representations that form the two components of a double description method similar to that provided for convex polyhedra. This thesis gives algorithms and methods for computing canonical forms, conversion between the descriptions and the main abstract operations needed for software analysis, such as comparison, intersection, join, difference, affine image and pre-image. Also included is a widening operation and we show that all of these operations have polynomial complexity. In the second part of this thesis we consider the partially reduced product of two numerical domains. The partially reduced product allows a choice of interaction between the component domains ranging from “do nothing” required by the direct product to a total reduction required by the reduced product. We consider the partially reduced product where the components are those of the grid domain with either the convex polyhedra domain or one of its sub-domains, specifi- cally the boxes, bounded difference shapes and octagon domains. The “weakly tight product” is introduced, an operation that ensures each constraint of the polyhedral representation intersects a point of the grid, and the “tight product”, which ensures each constraint of the polyhedral rep- resentation intersects a point of the grid-polyhedron. We provide an algorithm to compute the weakly tight product and show for what circumstances this algorithm achieves stronger results, so that the resulting grid-polyhedron is either a tight or a reduced product. Methods for test- ing if a grid-polyhedron is empty as well as several useful operations on grid-polyhedra are also described.