Sound Bit-Precise Numerical Domains
Tushar Sharma and Thomas Reps
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.
(Click here to access the paper:
PDF;
(c) Springer-Verlag.)
University of Wisconsin