Write a Blog >>
VMCAI 2017
Sun 15 - Tue 17 January 2017
co-located with POPL 2017
Mon 16 Jan 2017 10:30 - 11:00 at Amphitheater 44 - Numerical domains Chair(s): Laure Gonnord

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 Domains(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 abstract operations 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 \in 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, FD_k(.), is parametrized by k, the maximum number of disjunctions allowed.

We instantiate the BVS(FD_k) 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.

slides (bitprecisevmcai17.pdf)916KiB

Mon 16 Jan