Some Efficient Algorithms for the Tightest UTVPI Polyhedral Over-Approximation Problem

Many static analysis problems involve solving mathematical data-flow equations over numerical abstract domains. Convex polyhedra is one such abstract domain that is widely used to precisely capture affine relationships among program variables. However, the majority of the analysis problems based on convex polyhedral domains fail to scale for large problem sizes due to the high-complexity/exponential nature of operations defined over them (such as Feasibility, Optimization). The Unit-Two-Variable-Per-Inequality (UTVPI) Polyhedra (also called Octagons) has been proven to be a very useful abstract domain; due to its improved worst-case polynomial time complexity, as well as ease of implementation. In this paper, we present two new algorithms that compute the tightest UTVPI Over-Approximation (OA) of a given convex polyhedron by relying on elementary polyhedral operations. Our algorithms improve over the OA algorithm that is implemented in the state-of-the-art libraries. Our first algorithm is based on linear programming (LP); our second algorithm is based on Fourier-Motzkin elimination (projections) combined with only rotation operations. Both algorithms exploit the Octagonal nature of the OA that they aim to obtain; so, they are highly simple in nature (in theory as well as implementation), simple to reason about correctness and optimality, and also easy to implement. We implemented our two algorithms in the Integer Set Library (ISL), an open-source polyhedral compilation library. Though our work is preliminary, we believe that our algorithms will be useful in static analysis as well as polyhedral compilation applications like iterative optimization, codegeneration, cache miss calculation, and transitive closure