Sound bit-precise numerical domains

Abstract

This paper tackles the challenge of creating a numerical abstract domain that can identify affine-inequality invariants while handling overflow in arithmetic operations over bit-vector data-types. The paper describes the design and implementation of a class of new abstract domains, called the Bit-Vector-Sound, Finite-Disjunctive (BVSFD) domains. We introduce a framework that takes an abstract domain A that is sound with respect to mathematical integers and creates an abstract domain BVS(A) whose operations and abstract transformers are sound with respect to machine integers. We also describe how to create abstract transformers for BVS(A) that are sound with respect to machine arithmetic. The abstract transformers make use of an operation WRAP(av, v)—where av ∈ A and v is a set of program variables—which performs wraparound in av for the variables in v. To reduce the loss of precision from WRAP, we use finite disjunctions of BVS(A) values. The constructor of finite-disjunctive domains, FDk(·), is parameterized by k, the maximum number of disjunctions allowed. We instantiate the BVS(FDk) framework using the abstract domain of polyhedra and octagons. Our experiments show that the analysis can prove 25% of the assertions in the SVCOMP loop benchmarks with k = 6, and 88% of the array-bounds checks in the SVCOMP array benchmarks with k = 4.