Anzeige
Erschienen in:
2017 | OriginalPaper | Buchkapitel
Sound Bit-Precise Numerical Domains
verfasst von : Tushar Sharma, Thomas Reps
Erschienen in: Verification, Model Checking, and Abstract Interpretation
Aktivieren Sie unsere intelligente Suche, um passende Fachinhalte oder Patente zu finden.
Wählen Sie Textabschnitte aus um mit Künstlicher Intelligenz passenden Patente zu finden. powered by
Markieren Sie Textabschnitte, um KI-gestützt weitere passende Inhalte zu finden. powered by
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 (\(\textit{BVSFD}\)) domains. We introduce a framework that takes an abstract domain \(\mathcal {A}\) that is sound with respect to mathematical integers and creates an abstract domain \(\textit{BVS}(\mathcal {A})\) whose operations and abstract transformers are sound with respect to machine integers. We also describe how to create abstract transformers for \(\textit{BVS}(\mathcal {A})\) that are sound with respect to machine arithmetic. The abstract transformers make use of an operation \(\textit{WRAP}(\textit{av}, v)\)—where \(\textit{av} \in \mathcal {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 \(\textit{WRAP}\), we use finite disjunctions of \(\textit{BVS}(\mathcal {A})\) values. The constructor of finite-disjunctive domains, \(\textit{FD}_k(\cdot )\), is parameterized by k, the maximum number of disjunctions allowed.
We instantiate the \(\textit{BVS}(\textit{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\).