Complete Decision Procedure for the Theory of Bounded Pointer Arithmetic
Rafael Faritovich Sadykov, Mikhail Usamovich Mandrykin · Programming and Computer Software · 2022
Abstract The process of developing C programs is quite often prone to errors associated with the use of pointer arithmetic and operations on memory addresses. Hence, the need for various automated program verification tools arises. One of the techniques frequently employed by these tools is invocation of suitable decision procedures implemented within existing SMT solvers. However, both the SMT standard and the majority of existing SMT solvers lack relevant logics (combinations of logical theories) for the direct and precise modeling of the semantics of pointer operations in C. A possible way to support these logics is to implement them in an SMT solver. However, this approach can be time-consuming (as it requires modifying the source code of the solver), inflexible (because introducing any changes to the signature or semantics of the theory can be unreasonably hard), and limited (every solver has to be supported individually). Another way is to design and implement custom quantifier instantiation strategies. These strategies can then be used to translate formulas in selected theory combinations into formulas in well-supported decidable logics, e.g., QF_UFLIA. In this paper, we present an instantiation procedure for translating formulas in the theory of bounded pointer arithmetic into the QF_UFLIA logic. We formally prove the soundness and completeness of our instantiation procedure in Isabelle/HOL. The paper also presents an informal description of this proof for the proposed procedure. The theory of bounded pointer arithmetic itself is formulated based on known errors associated with the use of pointer arithmetic operations in C, as well as based on the semantics of these operations specified in the C standard. Similar procedure can also be defined for a practically relevant fragment of the theory of bit vectors (monotone propositional combinations of equalities between bitwise expressions). Our approach is sufficient to derive efficient decision procedures, implemented as Isabelle/HOL proof methods, for several decidable logical theories used in C program verification by relying on the existing capabilities of well-known SMT solvers (e.g., Z3), as well as on the proof reconstruction capabilities of the Isabelle/HOL proof assistant.