BOXES: A Symbolic Abstract Domain of Boxes

Arie Gurfinkel, Sagar Chaki, Proceedings of the 17th International Static Analysis Symposium (SAS), page 287-303, September 14-16, 2010.

Abstract: Numeric abstract domains are widely used in program analyses. The simplest numeric domains over-approximate disjunction by an imprecise join, typically yielding path-insensitive analyses. This problem is addressed by disjunctive completions, such as finite powersets, which provide exact disjunction. However, developing correct and efficient disjunctive completions is challenging. First, there must be an efficient way to represent and manipulate abstract values. The simple approach of using ``sets of base abstract values'' is often not scalable. Second, while a widening must strike the right balance between precision and the rate of convergence, it is notoriously hard to get correct. In this paper, we present an implementation of the BOXES abstract domain -- a disjunctive completion of the well-known BOX (or Intervals) domain. An element of BOXES is a finite union of boxes, i.e., expressible as a propositional formula over upper- and lower-bounds constraints. Our implementation is symbolic, and weds the strengths of Binary Decision Diagrams (BDDs) and BOX. The complexity of the operations (meet, join, transfer functions, and widening) is linear in the size of the operands. Empirical evaluation indicates that the performance of BOXES is superior to other existing disjunctive completions of BOX with comparable expressiveness.

PDF