SubPoh hedra: a family of numerical abstract domains for the (more) scalable inference of linear inequalities

摘要

We introduce SubPolyhedra (SubPoly), a new family of numerical abstract domains to infer and propagate linear inequalities. The key insight is that the reduced product of linear equalities and intervals produces powerful yet scalable analyses. Abstract domains in SubPoly are as expressive as Polyhedra, but they drop some of the deductive power to achieve scalability. The cost/precision ratio of abstract domains in the SubPoly family can be fine-tuned according to the precision one wants to retain at join points, and the algorithm used to infer the tighter bounds on intervals. We implemented SubPoly on the top of Clousot, ageneric abstract interpreter for .Net. Clousot with SubPoly analyzes very large and complex code bases in few minutes. SubPoly can efficiently capture linear inequalities among hundreds of variables, a result well beyond the state-of-the-art implementations of Polyhedra.