Expressive and Efficient Memory Representation for Bounded Model Checking of C programs
Abstract
Ensuring memory safety in programs has been an important yet difficult topic of research. Most static analysis approaches rely on the theory of arrays to model memory
access. The limitation of the theory of arrays in terms of scalability and compatibility
with SAT/SMT solvers is well-known, and there has been many attempts at optimizing
either the theory itself or memory encodings based on theory of arrays.
In this thesis, we demonstrate that existing arrays-based memory encodings miss potential optimization opportunities by omitting language specific properties such as alignment and pointer arithmetic in C. We present SeaM, a new memory representation for C programs built around a more expressive First-order Theory: the Theory of Memory.
We show that by preserving more C language specific rules and properties, the Theory
of Memory allows for more thorough optimization methods during eager rewriting of sequences of stores. We introduce two such optimization methods in this thesis. First, we over-approximate pointer comparison with an abstract interpretation-like approach called AddressRangeMap. Second, we compress sequences of stores with Store-Map for faster
address offset look-ups.
The new memory representation is implemented in SeaBmc, a new BMC tool for
LLVM. We evaluate our approach on real-world bounded model checking tasks from the
aws-c-common library and Sv-Comp benchmarks and compare it against two existing
memory representations in SeaBmc. Our results show that SeaM outperforms the theory
of array based representation and is comparable with the λ based representation.
Collections
Cite this version of the work
Xiang Zhou
(2022).
Expressive and Efficient Memory Representation for Bounded Model Checking of C programs. UWSpace.
http://hdl.handle.net/10012/18953
Other formats