Towards Satisfiability Modulo Parametric Bit-vectors

Abstract

Many SMT solvers implement efficient SAT-based procedures for solving fixed-size bit-vector formulas. These techniques, however, cannot be used directly to reason about bit-vectors of symbolic bit-width. To address this shortcoming, we propose a translation from bit-vector formulas with parametric bit-width to formulas in a logic supported by SMT solvers that includes non-linear integer arithmetic, uninterpreted functions, and universal quantification. While this logic is undecidable, our approach can still solve many formulas that arise in practice by capitalizing on advances in SMT solving for non-linear arithmetic and universally quantified formulas. We provide several case studies in which we have applied this approach with promising results, including the bit-width independent verification of invertibility conditions, compiler optimizations, and bit-vector rewrite rules.

1 Introduction

Satisfiability Modulo Theories (SMT) solving for the theory of fixed-size bit-vectors has received a lot of interest in recent years. Many applications rely on bit-precise reasoning as provided by SMT solvers, and the number of solvers that participate in the corresponding divisions of the annual SMT competition is high and increasing. Although the satisfiability problem in this domain is theoretically difficult (e.g., [19]), bit-vector solvers are in practice highly efficient and typically implement SAT-based procedures.

Reasoning about fixed-size, i.e., fixed-width, bit-vectors suffices for many applications. For instance, in hardware verification the size of a circuit is usually known in advance. In software verification, machine integers are treated as fixed-width bit-vectors, with the width depending on the underlying architecture. Correspondingly, current solving approaches in SMT rely on this restriction and, as a consequence, cannot reason about parametric circuits or machine integers of arbitrary size. This is a serious limitation when proving properties that are bit-width independent, or when reasoning about machine integers of a fixed but large size. For example, in smart contract languages such as Solidity [33], 256-bit integers are widely used as addresses.

The current state of the art for solving bit-vector formulas involves a technique called bit-blasting [20], an eager translation to propositional logic. However, it does not scale well for larger bit-widths, in particular in the presence of operations that have a complex definition at the propositional level, such as multiplication. To address this limitation, we propose a general method for reasoning about bit-vector formulas with parametric bit-width. The essence of our method is to replace the translation from fixed-size bit-vectors to propositional logic with a translation to a quantified fragment of the combined theory of integer arithmetic and uninterpreted functions. We obtain a fully automated verification process by capitalizing on recent advances in SMT solving for these theories.

The reliability of our approach depends on the correctness of the SMT solvers in use. Interactive theorem provers, or proof assistants, such as Isabelle and Coq  [10, 25], on the other hand, target applications where trust is of higher importance than automation, although substantial progress towards increasing the latter has been made in recent years [5]. Our long-term goal is an efficient automated framework for proving bit-width independent properties within a trusted proof assistant, which requires both a formalization of such properties in the language of the proof assistant and the development of efficient automated techniques to reason about these properties. Our encoding techniques make the latter feasible.

Translating a formula from the theory of parametric-width bit-vectors to the theory of integer arithmetic is not straightforward. This is due to the fact that the semantics of bit-vector operations of bit-width n are most naturally expressed using exponentiation terms $2^n$. Most SMT solvers, however, do not support unrestricted exponentiation for integer arithmetic. Further, operators such as bitwise ${ and}$ and ${ or}$ do not have a natural representation in integer arithmetic. While they are definable in the theory of integer arithmetic using $\beta$-function encodings (e.g., [15]), such a translation is expensive as it requires an encoding of sequences into natural numbers. Instead, we introduce an uninterpreted function (UF) for each of these problematic operators and axiomatize them with quantified formulas, which shifts some of the reasoning burden from arithmetic to UF reasoning. We consider two alternative axiomatization approaches: a complete one relying on induction, and a partial (hand-crafted) one that can be understood as an under-approximation of the original problem.

To evaluate the potential of our approach, we examine three case studies that arise from real applications where reasoning about bit-width independent properties is essential. Niemetz et al. [23] introduced the notion of invertibility condition for bit-vector operators, and defined a large number of such conditions which they then used in a new procedure for quantified bit-vector formulas. Because of the fixed-size setting, the correctness of those conditions was only checked for specific range of bit-widths: from 1 to 65. As a first case study, we consider here the bit-width independent verification of those invertibility conditions, which Niemetz et al. [23] left to future work. As a second case study, we examine the bit-width independent verification of compiler optimizations in LLVM. For that, we use the Alive tool [22], which generates verification conditions for such optimizations in the theory of fixed-size bit-vectors. Proving the correctness of these optimizations for arbitrary bit-widths would ensure their correctness for any language or underlying architecture rather than just for specific ones. As a third case study, we consider the bit-width independent verification of rewrite rules for the theory of fixed-size bit-vectors. SMT solvers for this theory heavily rely on such rules to simplify the input. Verifying their correctness is essential and is typically done by hand, which is both tedious and error-prone.

To summarize, this paper makes the following contributions.

• In Sect. 4, we study complete and incomplete encodings of bit-vector formulas with parametric bit-width into integer arithmetic.

• In Sect. 5, we evaluate the effectiveness of these encodings in three case studies.

• As part of the first case study, we introduce conditional inverses for bit-vector constraints, thus augmenting the work of [23] with concrete parametric solutions.

Table 1 Considered bit-vector operators with SMT-LIB 2 syntax

1.1 Related Work

Bit-width independent bit-vector formulas were studied by Picora [27], who introduced a formal language for bit-vectors of parametric width, together with semantics and a decision procedure. The language we use here is a simplified variant of that language. A unification-based algorithm for bit-vectors of symbolic lengths is discussed by Bjørner and Picora in [4]. Bit-width independent formulas are related to parametric Boolean functions and circuits. An inductive approach for reasoning about such formalisms was developed by Gupta and Fisher [16, 17] by considering a Boolean function for the base case of a circuit and another one for its inductive step. Reasoning about equivalence of such circuits can be embedded in Picora’s formal framework of [27]. Our technique is based on a translation of parametric bit-vectors to integers. For the case of fixed-width bit-vectors, translations of arithmetic bit-vector operations to integers have been studied, e.g., in [6, 7, 36].

2 Preliminaries

We briefly review the usual notions and terminology of many-sorted first-order logic with equality. See [15, 34] for more detailed information.

Let $S$ be a set of sort symbols, and for every sort ${\sigma \in S}$, let $X _{\sigma }$ be an infinite set of variables of sort $\sigma$. We assume that sets $X _{\sigma }$ are pairwise disjoint and define $X$ as the union of sets $X _{\sigma }$. A signature $\varSigma$ consists of a set $\varSigma ^s \!\subseteq S$ of sort symbols and a set $\varSigma ^f$ of function symbols. Arities of function symbols are defined in the usual many-sorted way. Constants are treated as nullary functions. We assume that every signature $\varSigma$ includes a Boolean sort Bool and two constant symbols $\top$ (true) and $\bot$ (false) of sort Bool. Furthermore, we assume that $\varSigma$ has an equality symbol $\approx$ of arity $\sigma \times \sigma \rightarrow \textsf {Bool}$ for each sort $\sigma \in \varSigma ^s$. We call predicate symbol any function symbol whose return sort is Bool. We use the usual definitions of well-sorted terms, literals, and formulas as terms of sort Bool, and refer to them as $\varSigma$-terms, $\varSigma$-literals, and $\varSigma$-formulas, respectively. We include the if–then–else operator $\mathrm{ite}({\_},{\_},{\_})$ of arity $\textsf {Bool} \times \sigma \times \sigma \rightarrow \sigma$ for each $\sigma \in \varSigma ^s$.

We define $\varvec{x} = (x_1, ..., x_n)$ as a tuple of variables and write $Q\varvec{x} \varphi$ with $Q \in \{ \forall , \exists \}$ for a quantified formula $Qx_1 \cdots Qx_n \varphi$. For a $\varSigma$-term s, we denote the free variables of s (defined as usual) as $\mathrm{FV}(s)$ and use $s[\varvec{x} ]$ to denote that the free variables of s occur in $\varvec{x}$; if $\varSigma$-terms $\varvec{t} = (t_1, ..., t_n)$ is a tuple of terms we write $s[\varvec{t} ]$ for the term obtained from s by simultaneously replacing each occurrence of $x_i$ in s by $t_i$. A $\varSigma$-interpretation ${\mathcal {I}}$ maps: each sort $\sigma \in \varSigma ^s$ to a distinct non-empty set of values $\sigma ^{{\mathcal {I}}}$ (the domain of $\sigma$ in ${\mathcal {I}}$); each variable $x \in X _{\sigma }$ to an element ${x^{\mathcal {I}} \in \sigma ^{{\mathcal {I}}}}$; and each function symbol $f^{\sigma _1 \cdots \sigma _n \sigma } \in \varSigma ^f$ to a total function $f^{\mathcal {I}} \!\!: \sigma _1^{\mathcal {I}} \times ... \times \sigma _n^{\mathcal {I}} \rightarrow \sigma ^{{\mathcal {I}}}$ if $n > 0$, and to an element in $\sigma ^{{\mathcal {I}}}$ if $n = 0$. We use the usual inductive definition of a satisfiability relation $\models$ between $\varSigma$-interpretations and $\varSigma$-formulas. Given a $\varSigma$-interpretation ${\mathcal {I}}$ and a sub-signature $\varSigma '$ of $\varSigma$, the reduct of ${\mathcal {I}}$ to $\varSigma '$ is obtained from ${\mathcal {I}}$ by restricting it to the sorts and symbols of $\varSigma '$.

A theory T is a pair $(\varSigma , {I})$, where $\varSigma$ is a signature and ${I}$ is a non-empty class of $\varSigma$-interpretations that is closed under variable reassignment, i.e., if interpretation ${\mathcal {I}} '$ only differs from an ${\mathcal {I}} \in {I}$ in how it interprets variables, then also ${{\mathcal {I}} '\in {I}}$. Moreover, each interpretation in ${I}$ interprets $\approx$ as the identity relation and Bool as the two-element set $\{\top ^{\mathcal {I}}, \bot ^{\mathcal {I}} \}$ and interprets a term of the form $\mathrm{ite}({c},{s},{t})$ as $s^{\mathcal {I}}$ if $c^{\mathcal {I}} = \top ^{\mathcal {I}}$ and as $t^{\mathcal {I}}$ otherwise. A $\varSigma$-formula $\varphi$ is T-satisfiable (resp. T-unsatisfiable) if it is satisfied by some (resp. no) interpretation in ${I}$; it is T-valid if it is satisfied by all interpretations in ${I}$. We will sometimes omit T when the theory is understood from context.

The theory $T_{\mathrm{BV}} = (\varSigma _{\mathrm{BV}}, {I} _{\mathrm{BV}})$ of fixed-size bit-vectors as defined in the SMT-LIB 2 standard [3] consists of the class of interpretations ${I} _{\mathrm{BV}}$ and signature $\varSigma _{\mathrm{BV}}$, which includes a unique sort for each positive integer n (representing the bit-vector width), denoted here as $\sigma _{[n]}$. We consider a restricted set of bit-vector function and predicate symbols (or bit-vector operators) as listed in Table 1. The selection of operators in this set is arbitrary but complete in the sense that it suffices to express all bit-vector operators defined in SMT-LIB 2. For a given positive integer n, the domain ${\sigma _{[n]}}^{{\mathcal {I}}}$ of sort $\sigma _{[n]}$ in ${\mathcal {I}}$ is the set of all bit-vectors of size n. We assume that $\varSigma _{\mathrm{BV}}$ includes all bit-vector constants of sort $\sigma _{[n]}$ for each n, represented as bit-strings. However, to simplify the notation we will sometimes denote them by the corresponding natural number in $\{0, \ldots , 2^{n-1}\}$. All interpretations ${\mathcal {I}} \in {I} _{\mathrm{BV}}$ are identical except for the value they assign to variables. They interpret sort and function symbols as specified in SMT-LIB 2. In particular, all function symbols (of non-zero arity) in $\varSigma ^f _{\mathrm{BV}}$ are overloaded for every $\sigma _{[n]} \! \in \varSigma ^s _{\mathrm{BV}}$. We denote a $\varSigma _{\mathrm{BV}}$-term (or bit-vector term) t of width n as ${t}_{[{n}]}$ when we want to specify its bit-width explicitly.

The SMT-LIB 2 definition of division by zero is worth mentioning. The expression $s\hbox {div}^{\mathrm{BV}}0$ is defined as evaluating to a bit-vector with the same bit-width as s with all bits set to 1. Similarly, expression ${s}\hbox {mod}^{\mathrm{BV}}{0}$ is defined as evaluating to s. Details on these semantics and their justification are given in the latest version of the SMT-LIB 2 standard.

We refer to the ith bit of $t_{[n]}$ as t[i] with $0\le i < n$. We interpret t[0] as the least significant bit (LSB), and $t[n-1]$ as the most significant bit (MSB), and denote bit ranges over k from index j down to i as t[j : i]. The unsigned interpretation of a bit-vector $t_{[n]}$ as a natural number is given by ${\left[ {t}\right] }_{\mathbb {N}} = \varSigma _{i=0}^{n-1}{t}\left[ {i}\right] \cdot 2^i$, and its signed interpretation as an integer is given by ${\left[ {t}\right] }_{\mathbb {Z}} =-{t}\left[ {n-1}\right] \cdot 2^{n-1}+{\left[ {{t}[{n-2}:{0}]^{\mathrm{BV}}}\right] }_{\mathbb {N}}$.

The theory $T_{\mathrm{IA}} = (\varSigma _{\mathrm{IA}}, {I} _{\mathrm{IA}})$ of integer arithmetic is also defined as in the SMT-LIB 2 standard. The signature $\varSigma _{\mathrm{IA}}$ includes a single sort $\textsf {Int}$, function and predicate symbols $\left\{ {+, -, \cdot , \div ,\,\mathrm{mod}\,, |{\_}|, <, \le , >, \ge }\right\}$, and a constant symbol for every non-negative integer value. We further extend $\varSigma _{\mathrm{IA}}$ to include exponentiation, denoted in the usual way as $a^b$. Unlike in the theory of bit-vectors, $\div$ and $\,\mathrm{mod}\,$ are partial functions, as they are not defined when their second argument is 0. Their semantics in this case is left unspecified in the SMT-LIB 2 standard, and they are thus treated as uninterpreted functions. Hence, ${I} _{\mathrm{IA}}$ is the set of all $\varSigma _{\mathrm{IA}}$-interpretations ${\mathcal {I}}$ that interpret the arithmetic operators as the usual integer operators, and differ only for the values they assign to variables and to $\div$ and $\,\mathrm{mod}\,$ when their second argument is zero. For a set $\mathcal {F}$ of function symbols whose arities have the form $\textsf {Int} \times \cdots \times \textsf {Int} \rightarrow \textsf {Int}$, we write $T_{\mathrm {UF}\mathrm{IA} } ^{\mathcal {F}}$ to denote the (combined) theory of uninterpreted functions of $\mathcal {F}$ with integer arithmetic. Its signature $\varSigma _{\mathrm {UF}\mathrm{IA} } ^{\mathcal {F}}$ is the union of the signature of $T_{\mathrm{IA}}$ with a disjoint signature containing the set $\mathcal {F}$ of function symbols, called uninterpreted functions. $T_{\mathrm {UF}\mathrm{IA} } ^{\mathcal {F}}$ consists of all $\varSigma _{\mathrm {UF}\mathrm{IA} } ^{\mathcal {F}}$-interpretations whose reduct to the signature $\varSigma _{\mathrm{IA}}$ is an interpretation of $T_{\mathrm{IA}}$.

3 Parametric Bit-Vector Formulas

We are interested in reasoning about (classes of) $\varSigma _{\mathrm{BV}}$-formulas that hold independently from the specific width of the sorts assigned to their variables or terms. We formalize the notion of parametric $\varSigma _{\mathrm{BV}}$-formulas in the following.

We fix two disjoint sets $X^{*}$ and $Z^*$ of variable and constant symbols, respectively, of a new bit-vector sort of undetermined bit-width. The bit-width is provided by the first component of a separate function pair $\omega = (\omega ^b, \omega ^N)$ which maps symbols ${\mathsf {x} \in X^{*} \cup Z^*}$ to $\varSigma _{\mathrm{IA}}$-terms without $\div$ and $\,\mathrm{mod}\,$. These operators (which we did not encounter in mappings $\omega$ of practical problems) are easily expressible by introducing more variables and using multiplication and addition, without having to deal with issues like division by zero. We refer to $\omega ^b(\mathsf {x})$ as the symbolic bit-width assigned by $\omega$ to $\mathsf {x}$. The second component of $\omega$ is a map $\omega ^N$ from symbols $\mathsf {z} \in Z^*$ to $\varSigma _{\mathrm{IA}}$-terms without $\div$ and $\,\mathrm{mod}\,$. We call $\omega ^N\!(\mathsf {z})$ the symbolic value assigned by $\omega$ to $\mathsf {z}$. Let $\varvec{v} =\mathrm{FV}(\omega )$ be the set of free (integer) variables occurring in the range of either $\omega ^b$ or $\omega ^N$. We say that $\omega$ is admissible if for every interpretation ${\mathcal {I}} \in {I} _{\mathrm{IA}}$ that interprets each variable in $\varvec{v}$ as a positive integer, and for every $\mathsf {x} \in X^{*} \cup Z^*$, ${\mathcal {I}}$ also interprets $\omega ^b(\mathsf {x})$ as a positive integer.

Let t be a term (possibly a formula), built from the function symbols of $\varSigma _{\mathrm{BV}}$ and $X^{*} \cup Z^*$, ignoring their sorts. We refer to t as a parametric $\varSigma _{\mathrm{BV}}$-term (formula). One can interpret t as a class of fixed-size bit-vector terms as follows. For each symbol $\mathsf {x} \in X^{*}$ and integer $n>0$, we associate a unique variable $x_n$ of (fixed) bit-vector sort $\sigma _{[n]}$. Given an admissible $\omega$ with $\varvec{v} =\mathrm{FV}(\omega )$ and an interpretation ${\mathcal {I}}$ that maps each variable in $\varvec{v}$ to a positive integer, let ${t}|_{{\omega }[{{\mathcal {I}}}]}$ be the result of replacing all symbols $\mathsf {x} \in X^{*}$ in t by the corresponding bit-vector variable ${x}_{[{k}]}$ and all symbols $\mathsf {x} \in Z^*$ in t by the bit-vector constant of sort $\sigma _{[k]}$ corresponding to $\omega ^N\!(\mathsf {x}) ^{\mathcal {I}} \,\mathrm{mod}\,2^k$, where in both cases k is $\omega ^b(\mathsf {x}) ^{\mathcal {I}}$. We say that t is well-sorted under $\omega$ if $\omega$ is admissible and ${t}|_{{\omega }[{{\mathcal {I}}}]}$ is a well-sorted $\varSigma _{\mathrm{BV}}$-term for all ${\mathcal {I}}$ that map variables in $\varvec{v}$ to positive integers. Note that in the most general case, well-sortedness and admissibility conditions may include non-linear multiplication and even exponentiation, which makes the problem of determining them undecidable. As we shall see in Sect. 5, however, there are interesting benchmarks that occur in practice and induce very simple conditions that can be trivial to check.

Example 1

Let $X^{*}$ be the set $\{ \mathsf {x} \}$ and $Z^*$ be the set $\{ \mathsf {z} _0, \mathsf {z} _1 \}$, where $\omega ^N\!(\mathsf {z} _0) = 0$ and $\omega ^N\!(\mathsf {z} _1) = 1$. Let $\varphi$ be the formula ${({\mathsf {x}}\, +^{\mathrm{BV}}{\mathsf {x}})}\, +^{\mathrm{BV}}{\mathsf {z} _1} \not \approx \mathsf {z} _0$. We have that $\varphi$ is well-sorted under $(\omega ^b, \omega ^N)$ with $\omega ^b = \{ \mathsf {x} \mapsto a, \mathsf {z} _0 \mapsto a, \mathsf {z} _1 \mapsto a \}$ or $\omega ^b = \{ \mathsf {x} \mapsto 3, \mathsf {z} _0 \mapsto 3, \mathsf {z} _1 \mapsto 3 \}$. It is not well-sorted when $\omega ^b = \{ \mathsf {x} \mapsto a_1, \mathsf {z} _0 \mapsto a_1, \mathsf {z} _1 \mapsto a_2 \}$ since ${\varphi }|_{{\omega }[{{\mathcal {I}}}]}$ is not a well-sorted $\varSigma _{\mathrm{BV}}$-formula whenever $a_1^{\mathcal {I}} \not = a_2^{\mathcal {I}}$. Note that an $\omega$ where $\omega ^b(\mathsf {x}) = a_1 - a_2$ is not admissible, since $(a_1 - a_2)^{\mathcal {I}} \le 0$ is possible even when $a_1^{\mathcal {I}} > 0$ and $a_2^{\mathcal {I}} > 0$.

Notice that symbolic constants such as the maximum unsigned constant of a symbolic length w can be represented by introducing $\mathsf {z} \in Z^*$ with $\omega ^b(\mathsf {z}) = w$ and $\omega ^N\!(\mathsf {z}) = 2^w-1$. Furthermore, recall that signature $\varSigma _{\mathrm{BV}}$ includes the (postfix) bit-vector extract operator ${}[{u}:{l}]^{\mathrm{BV}}$ whose name is parameterized by two natural numbers u and l. We do not lift the above definitions to handle extract operations. This is for simplicity and comes at no loss of expressive power, since constraints involving extract can be equivalently expressed using constraints involving concatenation. For example, showing that every instance of a constraint $s \approx {t}[{u}:{l}]^{\mathrm{BV}}$ is satisfiable, where $0< l \le u < n-1$, is equivalent to showing that $\forall y_1 \forall y_2 \forall y_3 (t \approx { y_1 } \circ ^{\mathrm{BV}}{ ({ y_2 } \circ ^{\mathrm{BV}}{ y_3 }) } \Rightarrow s \approx y_2)$ is satisfiable where $y_1, y_2, y_3$ are fresh variables of sort $\sigma _{[n-1-u]}$, $\sigma _{[u-l+1]}$, $\sigma _{[l]}$, respectively. We may reason about a formula involving a symbolic range $\{l, \ldots , u\}$ of t by considering a parametric bit-vector formula that encodes a formula of the latter form, where the appropriate symbolic bit-widths are assigned to symbols introduced for $y_1, y_2, y_3$.

For every admissible $\omega$, we extend $\omega$ to bit-vector terms t that are well sorted under $\omega$ so that ${t}|_{{\omega }[{{\mathcal {I}}}]}$ has sort $\sigma _{[\omega ^b(t) ^{{\mathcal {I}}}]}$ for all interpretations ${\mathcal {I}}$ that map variables in $\mathrm{FV}(\omega )$ to positive integers. Intuitively, $\omega (t)$ is computed recursively by computing $\omega$ for each immediate subterm of t and then applying the typing rules of the operators in $\varSigma _{\mathrm{BV}}$. The formal definition of $\omega ^b$ is by induction on terms. The base cases are already defined. $\omega ^b(\diamond t) =\omega ^b(t)$ for $\diamond \in \left\{ {-^{\mathrm{BV}},\sim ^{\mathrm{BV}}}\right\}$. For the binary operators of Table 1 (except for extraction which can be eliminated as described above), we set $\omega ^b(\diamond (t_{1},t_{2})) =\omega ^b(t_{2})$ if $\diamond$ is not $\circ ^{\mathrm{BV}}$. For concatenation, $\omega ^b({t_{1}} \circ ^{\mathrm{BV}}{t_{2}}) =\omega ^b(t_{1}) +\omega ^b(t_{2})$. In turn, $\omega ^N$ is extended to complex terms by evaluating them according to the semantics given by the SMT-LIB 2 standard. For example, $\omega ^N\!({t_{1}}\, +^{\mathrm{BV}}{t_{2}})$ is $\omega ^N\!(t_{1}) + \omega ^N\!(t_{2}) \,\mathrm{mod}\,2^{\omega ^b(t_{2})}$.

Finally, we extend the notion of validity to parametric bit-vector formulas. Given a formula $\varphi$ well sorted under $\omega$, we say $\varphi$ is $T_{\mathrm{BV}}$-valid under $\omega$ if ${\varphi }|_{{\omega }[{{\mathcal {I}}}]}$ is $T_{\mathrm{BV}}$-valid for all ${\mathcal {I}}$ that map variables in $\mathrm{FV}(\omega )$ to positive integers.

4 Encoding Parametric Bit-Vector Formulas in SMT

Current SMT solvers do not support reasoning about parametric bit-vector formulas. In this section, we present a technique for encoding such formulas into formulas involving non-linear integer arithmetic, uninterpreted functions, and universal quantifiers. In SMT-LIB parlance, these are formulas in the UFNIA logic. Given a quantifier-free formula $\varphi$ that is well-sorted under some mapping $\omega$, we describe this encoding in terms of a translation $\mathcal {T}$, which returns a formula $\psi$ that is valid in the theory of uninterpreted functions with integer arithmetic only if $\varphi$ is $T_{\mathrm{BV}}$-valid under $\omega$. We describe several variations on this translation and discuss their relative strengths and weaknesses.

4.1 Introducing the Encoding

4.1.1 Overall Approach

At a high level, our translation produces an implication whose antecedent requires the integer variables to be in the correct ranges (e.g., $k>0$ for every bit-width variable k), and whose conclusion is the result of converting each (parametric) bit-vector term of bit-width k to an integer term. Operations on parametric bit-vector terms are converted to operations on the integers modulo $2^k$, where k can be a symbolic (i.e., uninterpreted) constant. We first introduce uninterpreted functions that will be used in our translation. Note that SMT solvers may not support the full set of functions in our extended signature $\varSigma _{\mathrm{IA}}$, since they typically do not support exponentiation. Our translation, however, requires a limited form of exponentiation. Therefore, we introduce an uninterpreted function symbol $\textsf {pow2}$ of arity $\textsf {Int} \rightarrow \textsf {Int}$, whose intended semantics is the function $\lambda x.2^x$ when the argument x is non-negative. Second, for each (non-predicate) n-ary function ${f}^{\mathrm{BV}}$ (with $n > 0$) of arity $\sigma _1 \times \cdots \times \sigma _n \rightarrow \sigma$ in the signature of fixed-size bit-vectors $\varSigma _{\mathrm{BV}}$ (excluding bit-vector extraction), we introduce an uninterpreted function ${f}^{{{\mathbb {N}}}}$ of arity $\textsf {Int} \times \textsf {Int} \times \cdots \times \textsf {Int} \rightarrow \textsf {Int}$, where the extra argument is used to specify the bit-width. For example, for ${+}^{{\mathrm{BV}}}$ with arity $\sigma _{[n]} \times \sigma _{[n]} \rightarrow \sigma _{[n]}$, we introduce ${+}^{{{\mathbb {N}}}}$ of arity $\textsf {Int} \times \textsf {Int} \times \textsf {Int} \rightarrow \textsf {Int}$. In its intended semantics, this function adds the second and third arguments, both integers, and returns the result modulo $2^k$, where k is the first argument. The signature $\varSigma _{\mathrm{BV}}$ contains one function, bit-vector concatenation $\circ ^{\mathrm{BV}}$, whose two arguments may have different sorts. For this case, the first argument of ${\circ }^{{{\mathbb {N}}}}$ indicates the bit-width of the third argument, i.e., ${\circ }^{{{\mathbb {N}}}} ({k},{x},{y})$ is interpreted as the concatenation of x and y, where y is an integer that encodes a bit-vector of bit-width k; the bit-width for x is not specified by an argument, as it is not needed for the elimination of this operator we perform later. We introduce uninterpreted functions for each bit-vector predicate symbol in a similar fashion. For instance, ${\ge _u}^{{{\mathbb {N}}}}$ has arity $\textsf {Int} \times \textsf {Int} \times \textsf {Int} \rightarrow \textsf {Bool}$ and encodes whether its second argument is greater than or equal to its third argument when these two arguments are interpreted as unsigned bit-vector values whose bit-width is given by its first argument. Most of these uninterpreted functions are eliminated as described below. However, $\textsf {pow2}$, ${{ \& }^{{{\mathbb {N}}}}}$, ${\mid }^{{{\mathbb {N}}}}$ and ${\oplus }^{{{\mathbb {N}}}}$ are not eliminated. Depending on the variation of the encoding, our translation may introduce quantified formulas that fully axiomatize the behavior of these remaining uninterpreted functions or add (quantified) lemmas that state some key properties about them, or both.

Fig. 1

Translation $\mathcal {T} _A$ for parametric bit-vector formulas, parameterized by axiomatization mode A

4.1.2 Translation Function

Figure 1 defines our translation function $\mathcal {T} _A$, which is parameterized by an axiomatization mode A. Given an input formula $\varphi$ that is well-sorted under $\omega$, it returns the implication whose antecedent is an axiomatization formula $\mathrm{AX}_{A} (\varphi ,\sigma )$ and whose conclusion is the result of converting $\varphi$ to its encoded version via the conversion function $\textsc {Conv}$. The former is dependent upon the axiomatization mode A which we discuss later. We assume without loss of generality that $\varphi$ contains no applications of bit-vector extract, which can be eliminated as described in the previous section, nor does it contain concrete bit-vector constants, since these can be equivalently represented by introducing a symbol in $Z^*$ with the appropriate concrete mappings in $\omega ^b$ and $\omega ^N$. For simplicity, we present only the case where $\varphi$ is quantifier-free. Quantifiers can be handled in the expected way: every bound bit-vector variable is replaced with a bound integer variable. The needed range-constraints are then added conjunctively to the matrix of an existential quantifier, and as a premise of an implication in the case of a universal quantifier.¹

In the translation, we use an auxiliary function $\textsc {Conv}$ which converts parametric bit-vector expressions into integer expressions with uninterpreted functions. Parametric bit-vector variables $\mathsf {x}$ (that is, symbols from $X^{*}$) are replaced by unique integer variables of sort $\textsf {Int}$, where we assume a mapping $\chi$ that maintains this correspondence and is such that the range of $\chi$ does not include any variable occurring in $\mathrm{FV}(\omega )$. Parametric bit-vector constants $\mathsf {z}$ (that is, symbols from set $Z^*$) are replaced by the term $\omega ^N\!(\mathsf {z}) \,\mathrm{mod}\,\textsf {pow2} (\omega ^b(\mathsf {z}))$. Observe that the ranges of the maps in $\omega$ may contain arbitrary $\varSigma _{\mathrm{IA}}$-symbols (other than $\div$ and $\,\mathrm{mod}\,$). In practice, however, our translation handles only cases where these terms contain symbols supported by the SMT solver, as well as terms of the form $2^t$, which we assume are replaced by $\textsf {pow2} (t)$ during this translation. For instance, if $\omega ^b(\mathsf {z}) =w+v$ and $\omega ^N\!(\mathsf {z}) = 2^w-1$, then $\textsc {Conv} (z,\omega )$ returns $(\textsf {pow2} (w)-1) \,\mathrm{mod}\,\textsf {pow2} (w+v)$.

Equalities are processed by $\textsc {Conv}$ by recursively running the translation on both sides. The next case handles applications of symbols from the signature $\varSigma _{\mathrm{BV}}$, where symbols ${f}^{\mathrm{BV}}$ are replaced with the corresponding uninterpreted function ${f}^{{{\mathbb {N}}}}$. The first argument of ${f}^{{{\mathbb {N}}}}$ is $\omega ^b(t_n)$, indicating the symbolic bit-width of the last argument of ${f}^{\mathrm{BV}}$. The remaining arguments are obtained by recursively calling $\textsc {Conv}$ on $t_1, \ldots , t_n$. In all cases, $\omega ^b(t_n)$ corresponds to the bit-width that the uninterpreted function ${f}^{{{\mathbb {N}}}}$ expects, based on its intended semantics (the bit-width of the second argument for bit-vector concatenation, or of an arbitrary argument for all other function and predicate symbols). Finally, $\textsc {Conv}$ applies homomorphically to all terms whose top symbol is a Boolean connective.

$\textsc {Conv}$ runs the auxiliary conversion function $\textsc {Elim}$ on all applications of uninterpreted functions ${f}^{{{\mathbb {N}}}}$ introduced during the conversion. $\textsc {Elim}$ eliminates a majority of functions corresponding to bit-vector operators as these functions are equivalently expressed using integer arithmetic and $\textsf {pow2}$. Specifically, the ternary addition operation ${+}^{{{\mathbb {N}}}}$, which represents addition of two bit-vectors with their width k specified as the first argument, is translated to integer addition modulo $\textsf {pow2} (k)$. The translation of subtraction ${-}^{{{\mathbb {N}}}}$ and multiplication ${\cdot }^{{{\mathbb {N}}}}$ applications is similar. For the division and remainder operations $\hbox {div}^{{\mathbb {N}}}$ and $\hbox {mod}^{{\mathbb {N}}}$, $\textsc {Conv}$ handles the special case where the second argument is zero, consistently with the semantics of bit-vectors operators in the SMT-LIB 2 standard. The integer operators corresponding to unary (arithmetic) negation and bitwise negation can be eliminated in a straightforward way. The semantics of various bitwise shift operators can be defined arithmetically using division and multiplication with $\textsf {pow2} (k)$. Arithmetic shift right $\mathop {{>>_a}^{{{\mathbb {N}}}}}$ can be defined in terms of other bit-vector operators and hence can be eliminated based on this definition. Concatenation can be eliminated by multiplying its first argument x by $\textsf {pow2} (k)$ (recall that k is the bit-width of the second argument y) which has the effect of shifting x left by k bits, as expected. The unsigned relation symbols can be directly converted to the corresponding integer relation. For the elimination of signed relation symbols we use an auxiliary helper $\textsf {uts}$ (unsigned to signed), also defined in Fig. 1, which returns the interpretation of its argument when seen as a signed value. The definition of $\textsf {uts}$ can be derived based on the semantics of signed and unsigned bit-vector values in the SMT-LIB 2 standard. Based on this definition, we have that integers v and u that encode bit-vectors of bit-width k, satisfy ${<_s}^{{{\mathbb {N}}}} (k, u, v)$ if and only if they satisfy $\textsf {uts} _{k}(u) <\textsf {uts} _{k}(v)$.

Example 2

As an example of our translation, let $\varphi ={({\mathsf {x}}\, +^{\mathrm{BV}}{\mathsf {x}})}\, +^{\mathrm{BV}}{\mathsf {z} _1} \not \approx \mathsf {z} _0$, $\omega ^N\!(\mathsf {z} _0) =0$, $\omega ^N\!(\mathsf {z} _1) =1$, and $\omega ^b(\mathsf {x}) =\omega ^b(\mathsf {z} _0) =\omega ^b(\mathsf {z} _1) =a$ from Example 1. Then, the result of $\textsc {Conv} (\varphi , (\omega ^b,\omega ^N))$ is

$$\begin{aligned} \textsc {Elim} ({+}^{{{\mathbb {N}}}} ({a},{\textsc {Elim} ({+}^{{{\mathbb {N}}}} ({a},{\chi (\mathsf {x})},{\chi (\mathsf {x})}))},{1\,\mathrm{mod}\,\textsf {pow2} (a)}))\not \approx 0 \,\mathrm{mod}\,\textsf {pow2} (a) \ . \end{aligned}$$

After applying $\textsc {Elim}$ and simplifying, we get $(\chi (\mathsf {x}) + \chi (\mathsf {x}) + 1) \,\mathrm{mod}\,\textsf {pow2} (a) \not \approx 0$.

Thanks to the application of $\textsc {Elim}$, we have that all formulas generated by $\textsc {Conv}$ contain only uninterpreted function symbols in the set $\mathcal {F} =\{ \textsf {pow2},{{ \& }^{{{\mathbb {N}}}}},{\mid }^{{{\mathbb {N}}}},{\oplus }^{{{\mathbb {N}}}} \}$. Thus, we restrict our attention to these symbols only in our axiomatization $\mathrm{AX}_{A}$, described next. From now on we denote $T_{\mathrm {UF}\mathrm{IA} } ^{\mathcal {F}}$ by $T_{\mathrm {UF}\mathrm{IA} }$.

Table 2 Full axiomatization of $\textsf {pow2}$, ${{ \& }^{{{\mathbb {N}}}}}$, ${\mid }^{{{\mathbb {N}}}}$, and ${\oplus }^{{{\mathbb {N}}}}$

Table 3 Partial axiomatization of $\textsf {pow2}$, ${{ \& }^{{{\mathbb {N}}}}}$, and ${\oplus }^{{{\mathbb {N}}}}$

4.1.3 Axiomatization Modes

We consider four different axiomatization modes A, which we call full, partial, comb, and qf (quantifier-free). These induce four different translations, namely: $\mathcal {T} _{\textit{full}}$, $\mathcal {T} _{\partial }$, $\mathcal {T} _{\textit{comb}}$, and $\mathcal {T} _{\textit{qf}}$. For each of these modes, we define $\mathrm{AX}_{A} (\varphi ,\omega )$ as the conjunction:11

$$ \begin{aligned} \bigwedge _{x \in \mathrm{FV}(\varphi )} \!\!\!\!0 \le \chi (x) < \textsf {pow2} (\omega ^b(x)) \wedge \left( \,\,\bigwedge _{w \in \mathrm{FV}(\omega )}\!\!\!\! w > 0\right) \wedge \mathrm{AX}_{A}^{\textsf {pow2}} \wedge \mathrm{AX}_{A}^{{{ \& }^{{{\mathbb {N}}}}}} \wedge \mathrm{AX}_{A}^{{\mid }^{{{\mathbb {N}}}}} \wedge \mathrm{AX}_{A}^{{\oplus }^{{{\mathbb {N}}}}} \end{aligned}$$

The first conjunction states that all integer variables introduced for parametric bit-vector variables $\mathsf {x}$ reside in the range specified by their bit-width. The second conjunction states that all free variables in $\omega$ (denoting bit-widths) are positive. The remaining four conjuncts denote the axiomatizations for the four uninterpreted functions that may occur in the output of the conversion function. The definitions of these formulas are given in Tables 2 and 3 for axiomatizations full and partial respectively. For each axiom, i, j, k denote bit-widths and x, y denote integers that encode bit-vectors of size k. We assume guards on all quantified formulas (omitted for brevity) that constrain i, j, k to be positive and x, y to be in the range $\{0, \ldots , \textsf {pow2} (k)-1\}$. Each table entry lists a set of formulas (interpreted conjunctively) that state properties about the intended semantics of these operators. The formulas for axiomatization mode full assert the intended semantics of these operators, whereas those for partial assert several properties of them. Axiomatization comb asserts both, and mode qf takes only the formulas in axiomatization partial that are quantifier-free. In particular, $\mathrm{AX}_{\textit{qf}}^{\textsf {pow2}}$ corresponds to the base cases listed in partial, and $\mathrm{AX}_{\textit{qf}}^{\diamond }$ for the other operators is simply $\top$. The partial axiomatization of these operations mainly includes natural properties of them. For example, we include some base cases for each operation, and also the ranges of its inputs and output. For some proofs, these are sufficient. For operators ${{ \& }^{{{\mathbb {N}}}}}$, ${\mid }^{{{\mathbb {N}}}}$ and ${\oplus }^{{{\mathbb {N}}}}$ we also include behavior for specific cases, e.g., ${{ \& }^{{{\mathbb {N}}}}} ({k},{a},{0})=0$ and its variants. Other axioms (e.g., “never even”) were added after analyzing specific benchmarks to identify sufficient axioms for their proofs.

4.2 Correctness

Our translation satisfies the following key properties.

Theorem 1

Let $\varphi$ be a parametric bit-vector formula that is well-sorted under $\omega$ and has no occurrences of operator bit-vector extract or concrete bit-vector constants. Then, the following hold.

• 1. $\varphi$ is $T_{\mathrm{BV}}$-valid under $\omega$ if and only if $\mathcal {T} _{\textit{full}} ({\varphi , \omega })$ is $T_{\mathrm {UF}\mathrm{IA} }$-valid.

• 2. $\varphi$ is $T_{\mathrm{BV}}$-valid under $\omega$ if and only if $\mathcal {T} _{\textit{comb}} ({\varphi , \omega })$ is $T_{\mathrm {UF}\mathrm{IA} }$-valid.

• 3. $\varphi$ is $T_{\mathrm{BV}}$-valid under $\omega$ if $\mathcal {T} _{\partial } ({\varphi , \omega })$ is $T_{\mathrm {UF}\mathrm{IA} }$-valid.

• 4. $\varphi$ is $T_{\mathrm{BV}}$-valid under $\omega$ if $\mathcal {T} _{\textit{qf}} ({\varphi , \omega })$ is $T_{\mathrm {UF}\mathrm{IA} }$-valid.

We prove Theorem 1 in the remainder of this section. We start with a proof of the first property described in the theorem, and then use this property in order to prove the others.

4.2.1 Proof of Property 1

The essence of the proof is to elevate the translation function described in Fig. 1 and Table 2 from formulas to interpretations. We start with the following definition that introduces this translation.

Definition 1

Given an interpretation ${\mathcal {J}}$ of $T_{\mathrm{IA}}$ that interprets the variables in $\varvec{v} =\mathrm{FV}(\omega )$ as positive integers, and an interpretation ${\mathcal {I}}$ of $T_{\mathrm{BV}}$, we define a corresponding interpretation ${{\mathcal {I}}}{{\mathbb {N}}}$ of $T_{\mathrm {UF}\mathrm{IA} }$ as follows:

• $\diamond ^{{{\mathcal {I}}}{{\mathbb {N}}}}$ is set to satisfy $\mathrm{AX}_{\diamond }^{\textit{full}}$ for any $\diamond \in \left\{ {\textsf {pow2},{{ \& }^{{{\mathbb {N}}}}},{\mid }^{{{\mathbb {N}}}},{\oplus }^{{{\mathbb {N}}}}}\right\}$

• $v^{{{\mathcal {I}}}{{\mathbb {N}}}}=v^{{\mathcal {J}}}$ for every $v\in \varvec{v}$

• $\chi (x)^{{{\mathcal {I}}}{{\mathbb {N}}}}={\left[ {({x}_{[{c}]})^{{\mathcal {I}}}}\right] }_{\mathbb {N}}$, where $c=\omega ^b(x) ^{{\mathcal {J}}}$ for any $x\in X^{*}$

We will show that this translation between interpretations preserves satisfiability. The following lemmas will be useful for this purpose.

Lemma 1

Let ${\mathcal {I}}$ be an interpretation of $T_{\mathrm {UF}\mathrm{IA} }$ that satisfies $\mathrm{AX}_{\textit{full}}^{\textsf {pow2}}$. Let a be a bit-vector constant of bit-width k and $n={\left[ {a}\right] }_{\mathbb {N}}$. Then:

• 1. Over natural numbers, $\textsf {pow2} ^{{\mathcal {I}}}$ is identical to $\lambda x.2^{x}$.

  In addition, ${\mathcal {I}}$ satisfies the following formulas:

• 2. ${\left[ {{i} \circ ^{\mathrm{BV}}{a}}\right] }_{\mathbb {N}}\approx \textsf {pow2} (k) \cdot i+{\left[ {a}\right] }_{\mathbb {N}}$ for any $i\in \left\{ {0,1}\right\}$.

• 3. $n \,\mathrm{mod}\,\textsf {pow2} (k-1) \approx {\left[ {{a}[{k-2}:{0}]^{\mathrm{BV}}}\right] }_{\mathbb {N}}$

• 4. $n \div 2 \approx {\left[ {{a}[{k-1}:{1}]^{\mathrm{BV}}}\right] }_{\mathbb {N}}$

• 5. ${\textsf {ex} _{{i}}({n})}^{{\mathcal {I}}}={a}\left[ {i}\right]$, with $\textsf {ex} _{{i}}({n})$ as $(n \div \textsf {pow2} (i)) \!\,\mathrm{mod}\,2\,$ for every $\,0\le i\le k-1$.

Proof

The first property follows from the standard inductive definition of the exponentiation function. The next three properties follow from the definition of ${\left[ {\cdot }\right] }_{\mathbb {N}}$. For the last property, we use induction on k. If $k=1$ then we must have $i=0$. In this case, $n\in \left\{ {0,1}\right\}$ and $\textsf {ex} _{{i}}({n}) ^{{\mathcal {I}}}=n ={\left[ {{a}\left[ {0}\right] }\right] }_{\mathbb {N}}$. Suppose $k>1$. If $i=0$, then this is shown similarly to the base case. Otherwise, ${a}\left[ {i}\right]$ corresponds to the bit in index $i-1$ of the bit-vector ${a}[{k-1}:{1}]^{\mathrm{BV}}$. By the induction hypothesis and previous items of this lemma, the latter is equal to $\textsf {ex} _{{i-1}}({{\left[ {{a}[{k-1}:{1}]^{\mathrm{BV}}}\right] }_{\mathbb {N}}}) ^{{\mathcal {I}}} =\textsf {ex} _{{i-1}}({{\left[ {a}\right] }_{\mathbb {N}} \div 2}) ^{{\mathcal {I}}}= \textsf {ex} _{{i}}({n}) ^{{\mathcal {I}}}$. $\square$

In the following lemma, we show that the full axiomatization indeed captures (over the natural numbers) the intended meaning of the bitwise operators.

Lemma 2

Let a and b be bit-vector constants of bit-width k, operator $\diamond \in \left\{ { \& ,\mid ,\oplus }\right\}$, and ${\mathcal {I}}$ an interpretation of $T_{\mathrm {UF}\mathrm{IA} }$ that satisfies $\mathrm{AX}_{\textit{full}}^{\textsf {pow2}} \wedge \mathrm{AX}_{\textit{full}}^{\diamond }$. Then ${\mathcal {I}}$ satisfies ${{\left[ {a{\diamond }^{\mathrm{BV}} b}\right] }_{\mathbb {N}}} \approx {{\diamond }^{{{\mathbb {N}}}}(k,{\left[ {a}\right] }_{\mathbb {N}},{\left[ {b}\right] }_{\mathbb {N}})}$.

Proof

We prove the lemma for the case where $\diamond$ is & by induction on k. The other cases are shown similarly. If $k=1$, then by Lemma 1, we have $({\left[ {{a} { \& }^{\mathrm{BV}}{b}}\right] }_{\mathbb {N}})^{{\mathcal {I}}} ={\left[ {\min (a,b)}\right] }_{\mathbb {N}}=\min (a,b)={{ \& }^{{{\mathbb {N}}}}} ({1},{{\left[ {a}\right] }_{\mathbb {N}}},{{\left[ {b}\right] }_{\mathbb {N}}})$. Now, suppose $k>1$. Then,

$$ \begin{aligned}&{{ \& }^{{{\mathbb {N}}}}} ({k},{{\left[ {a}\right] }_{\mathbb {N}}},{{\left[ {b}\right] }_{\mathbb {N}}})^{{\mathcal {I}}} \\&\quad =({{ \& }^{{{\mathbb {N}}}}} ({k-1},{{\left[ {a}\right] }_{\mathbb {N}} \,\mathrm{mod}\,\textsf {pow2} (k-1)},{{\left[ {b}\right] }_{\mathbb {N}} \,\mathrm{mod}\,\textsf {pow2} (k-1)})\\&\qquad +\,\,\textsf {pow2} (k-1) \cdot \min (\textsf {ex} _{{k-1}}({a}), \textsf {ex} _{{k-1}}({b})))^{{\mathcal {I}}} \end{aligned}$$

By Lemma 1, we have that

$$ \begin{aligned} \min (\textsf {ex} _{{k-1}}({a}), \textsf {ex} _{{k-1}}({b})) ={\left[ {{{a}\left[ {k-1}\right] } { \& }^{\mathrm{BV}}{{b}\left[ {k-1}\right] }}\right] }_{\mathbb {N}} \end{aligned}$$

By the induction hypothesis and Lemma 1, we obtain that ${{ \& }^{{{\mathbb {N}}}}} ({k},{{\left[ {a}\right] }_{\mathbb {N}}},{{\left[ {b}\right] }_{\mathbb {N}}})$ is equal in ${\mathcal {I}}$ to

$$ \begin{aligned} {\left[ {{{a}[{k-2}:{0}]^{\mathrm{BV}}} { \& }^{\mathrm{BV}}{{b}[{k-2}:{0}]^{\mathrm{BV}}}}\right] }_{\mathbb {N}} +\textsf {pow2} (k-1) \cdot {\left[ {{{a}\left[ {k-1}\right] } { \& }^{\mathrm{BV}}{{b}\left[ {k-1}\right] }}\right] }_{\mathbb {N}} \end{aligned}$$

which by Lemma 1 is equal in ${\mathcal {I}}$ to

$$ \begin{aligned} {\left[ {{({{a}\left[ {k-1}\right] } { \& }^{\mathrm{BV}}{{b}\left[ {k-1}\right] })} \circ ^{\mathrm{BV}}{({{a}[{k-2}:{0}]^{\mathrm{BV}}} { \& }^{\mathrm{BV}}{{a}[{k-2}:{0}]^{\mathrm{BV}}})}}\right] }_{\mathbb {N}} ={\left[ {{a} { \& }^{\mathrm{BV}}{b}}\right] }_{\mathbb {N}} \end{aligned}$$

$\square$

Now, we present the main lemma of the proof. It establishes a tight correspondence between the translation of Fig. 1 and Table 2 for formulas, and that of Definition 1 for interpretations.

Lemma 3

${\textsc {Conv} (t,\omega )}^{{{\mathcal {I}}}{{\mathbb {N}}}}={\left[ {({{t}|_{{\omega }[{{\mathcal {J}}}]}})^{{\mathcal {I}}}}\right] }_{\mathbb {N}}$ for any parametric $\varSigma _{\mathrm{BV}}$-term t, interpretation ${\mathcal {I}}$ of $T_{\mathrm{BV}}$, and ${\mathcal {J}}$ as in Definition 1.

Proof

First, notice that for any $x\in X^{*} \cup Z^*$ we have that $\omega ^b(x) ^{{{\mathcal {I}}}{{\mathbb {N}}}}=\omega ^b(x) ^{{\mathcal {J}}}$ and $\omega ^N\!(x) ^{{{\mathcal {I}}}{{\mathbb {N}}}}=\omega ^N\!(x) ^{{\mathcal {J}}}$. Using induction, the same holds for any parametric $\varSigma _{\mathrm{BV}}$-term t. We prove the lemma by induction on t.

• If t is x for some $x\in X^{*}$: follows from the definition of ${{\mathcal {I}}}{{\mathbb {N}}}$ for this case.

• If t is z for some $z\in Z^*$:

  $$\begin{aligned}&{\textsc {Conv} (t,\omega )}^{{{\mathcal {I}}}{{\mathbb {N}}}}\\&\quad =(\omega ^N\!(z) \,\mathrm{mod}\,\textsf {pow2} (\omega ^b(z)))^{{{\mathcal {I}}}{{\mathbb {N}}}}\\&\quad =\omega ^N\!(z) ^{{\mathcal {J}}} \,\mathrm{mod}\,\textsf {pow2} (\omega ^b(z) ^{{\mathcal {J}}}) \end{aligned}$$

  In turn, ${z}|_{{\omega }[{{\mathcal {J}}}]}$ is the bit-vector constant of width $k=\omega ^b(z) ^{{\mathcal {J}}}$ whose integer value is $\omega ^N\!(z) ^{{\mathcal {J}}}\,\mathrm{mod}\,2^{k}$.

• If t is constructed from an operator other than ${ \& }^{\mathrm{BV}}$, ${|}^{\mathrm{BV}}$, $\oplus ^{\mathrm{BV}}$, then this follows by the semantics of the various operators as defined in the SMT-LIB 2 standard. We explicitly show the case where $t={t_{1}}\, +^{\mathrm{BV}}{t_{2}}$. In this case,

  $$\begin{aligned} {\textsc {Conv} (t,\omega )}=(\textsc {Conv} (t_{1},\omega ) + \textsc {Conv} (t_{2}, \omega )) \,\mathrm{mod}\,\textsf {pow2} (\omega ^b(t_{2})), \end{aligned}$$

  which by Lemma 1, is interpreted in ${{\mathcal {I}}}{{\mathbb {N}}}$ as

  $$\begin{aligned} ((\textsc {Conv} (t_{1},\omega ))^{{{\mathcal {I}}}{{\mathbb {N}}}} + (\textsc {Conv} (t_{2}, \omega ))^{{{\mathcal {I}}}{{\mathbb {N}}}}) \,\mathrm{mod}\,2^k \end{aligned}$$

  for $k=\omega ^b(t_{2}) ^{{\mathcal {J}}}$. By the induction hypothesis, the latter is equal to

  $$\begin{aligned} ({\left[ {{{t_{1}}|_{{\omega }[{{\mathcal {J}}}]}}^{{\mathcal {I}}}}\right] }_{\mathbb {N}} +{\left[ {{{t_{2}}|_{{\omega }[{{\mathcal {J}}}]}}^{{\mathcal {I}}}}\right] }_{\mathbb {N}}) \,\mathrm{mod}\,2^k, \end{aligned}$$

  which by the semantics of ${+}^{{\mathrm{BV}}}$ as defined in the SMT-LIB 2 standard, is equal to ${\left[ {({({t_{1}}\, +^{\mathrm{BV}}{t_{2}})}|_{{\omega }[{{\mathcal {J}}}]})^{{\mathcal {I}}}}\right] }_{\mathbb {N}}$.

• The operators ${ \& }^{\mathrm{BV}}$, ${|}^{\mathrm{BV}}$ and $\oplus ^{\mathrm{BV}}$ rely on Lemma 2, rather than on the SMT-LIB 2 standard. We explicitly show the case where $t={t_{1}} { \& }^{\mathrm{BV}}{t_{2}}$. In this case,

  $$ \begin{aligned} {\textsc {Conv} (t,\omega )}^{{{\mathcal {I}}}{{\mathbb {N}}}}= ({{ \& }^{{{\mathbb {N}}}}} (\omega ^b(t_{2}), \textsc {Conv} (t_{1},\omega ),\textsc {Conv} (t_{2}, \omega )))^{{{\mathcal {I}}}{{\mathbb {N}}}}, \end{aligned}$$

  which by the induction hypothesis, is equal to

  $$ \begin{aligned} ({{ \& }^{{{\mathbb {N}}}}} (\omega ^b(t_{2}), {\left[ {{{t_{1}}|_{{\omega }[{{\mathcal {J}}}]}}^{{\mathcal {I}}}}\right] }_{\mathbb {N}}, {\left[ {{{t_{2}}|_{{\omega }[{{\mathcal {J}}}]}}^{{\mathcal {I}}}}\right] }_{\mathbb {N}}))^{{{\mathcal {I}}}{{\mathbb {N}}}} \end{aligned}$$

  By Lemma 2, we obtain ${\left[ {({({t_{1}} { \& }^{\mathrm{BV}}{t_{1}})}|_{{\omega }[{{\mathcal {J}}}]})^{{\mathcal {I}}}}\right] }_{\mathbb {N}}$.

$\square$

Using Lemma 3, we prove the correctness of the translation between interpretations:

Lemma 4

${\mathcal {I}}$ satisfies ${\varphi }|_{{\omega }[{{\mathcal {J}}}]}$ iff ${{\mathcal {I}}}{{\mathbb {N}}}$ satisfies $\mathcal {T} _{\textit{full}} ({\varphi ,\omega })$.

Proof

By induction on $\varphi$. We explicitly prove two base cases. The remaining cases are proved similarly. Further, the induction steps (for formulas composed using the logical connectives), follow directly from the induction hypothesis.

• If $\varphi$ has the form $t_{1}=t_{2}$, then $I\models {\varphi }|_{{\omega }[{{\mathcal {J}}}]}$ iff ${t_{1}}|_{{\omega }[{{\mathcal {J}}}]} ^{{\mathcal {I}}}={t_{2}}|_{{\omega }[{{\mathcal {J}}}]} ^{{\mathcal {I}}}$ iff ${\left[ {{t_{1}}|_{{\omega }[{{\mathcal {J}}}]} ^{{\mathcal {I}}}}\right] }_{\mathbb {N}}={\left[ {{t_{2}}|_{{\omega }[{{\mathcal {J}}}]} ^{{\mathcal {I}}}}\right] }_{\mathbb {N}}$ iff (Lemma 3) $\textsc {Conv} (t_{1},\omega )^{{{\mathcal {I}}}{{\mathbb {N}}}}=\textsc {Conv} (t_{2},\omega )^{{{\mathcal {I}}}{{\mathbb {N}}}}$ iff ${{\mathcal {I}}}{{\mathbb {N}}}\models \textsc {Conv} (t_{1},\omega )=\textsc {Conv} (t_{2},\omega )$ iff ${{\mathcal {I}}}{{\mathbb {N}}}\models \mathcal {T} _{\textit{full}} ({t_{1}=t_{2},\omega })$.

• If $\varphi$ has the form ${t_{1}}\, {<_{\mathrm{s}}}^{ {\mathrm{BV}}}{t_{2}}$, then recall that the SMT-LIB 2 semantics of ${x}\, {<_{\mathrm{s}}}^{ {\mathrm{BV}}}{y}$ are given by the formula $({x}[{k-1}:{k-1}]^{\mathrm{BV}} =1\wedge {y}[{k-1}:{k-1}]^{\mathrm{BV}} =0)\vee ({x}[{k-1}:{k-1}]^{\mathrm{BV}} ={y}[{k-1}:{k-1}]^{\mathrm{BV}} \wedge {x}\, {<_{\mathrm{u}}}^{ {\mathrm{BV}}}{y})$. It is easy to see that this condition is equivalent to ${\left[ {x}\right] }_{\mathbb {Z}}<{\left[ {y}\right] }_{\mathbb {Z}}$. Thus, in this case, we have that $I\models {\varphi }|_{{\omega }[{{\mathcal {J}}}]}$ iff

  $$\begin{aligned} (*)~{\left[ {{t_{1}}|_{{\omega }[{{\mathcal {J}}}]} ^{{\mathcal {I}}}}\right] }_{\mathbb {Z}} <{\left[ {{t_{2}}|_{{\omega }[{{\mathcal {J}}}]} ^{{\mathcal {I}}}}\right] }_{\mathbb {Z}}. \end{aligned}$$

  Now, for any term t, $\textsf {uts} _{k}({\left[ {({t}|_{{\omega }[{{\mathcal {J}}}]})^{{\mathcal {I}}}}\right] }_{\mathbb {N}}) = {\left[ {({t}|_{{\omega }[{{\mathcal {J}}}]})^{{\mathcal {I}}}}\right] }_{\mathbb {Z}}$ for every parametric bit-vector term t with $k=\omega ^b(t)$. Indeed, let $v={t}|_{{\omega }[{{\mathcal {J}}}]} ^{{\mathcal {I}}}$. Then, ${\left[ {v}\right] }_{\mathbb {N}}=2^{k-1}\cdot {v}\left[ {k-1}\right] +{\left[ {{v}[{k-2}:{0}]^{\mathrm{BV}}}\right] }_{\mathbb {N}}$ and ${\left[ {v}\right] }_{\mathbb {Z}}=-2^{k-1}\cdot {v}\left[ {k-1}\right] +{\left[ {{v}[{k-2}:{0}]^{\mathrm{BV}}}\right] }_{\mathbb {N}}$. Adding these two equations and simplifying, we get ${\left[ {v}\right] }_{\mathbb {Z}}=2\cdot {\left[ {{v}[{k-2}:{0}]^{\mathrm{BV}}}\right] }_{\mathbb {N}}-{\left[ {v}\right] }_{\mathbb {N}}={\left[ {v}\right] }_{\mathbb {N}}\,\mathrm{mod}\,2^{k-1}-{\left[ {v}\right] }_{\mathbb {N}}= \textsf {uts} _{k}({\left[ {v}\right] }_{\mathbb {N}})$. Hence, condition $(*)$ above holds iff $\textsf {uts} _{k}({\left[ {{{t_{1}}|_{{\omega }[{{\mathcal {J}}}]} ^{{\mathcal {I}}}}}\right] }_{\mathbb {N}}) < \textsf {uts} _{k}({\left[ {{{t_{2}}|_{{\omega }[{{\mathcal {J}}}]} ^{{\mathcal {I}}}}}\right] }_{\mathbb {N}})$, with $k=\omega ^b(t_{1}) ^{{\mathcal {J}}}$ iff (by Lemma 3) $\textsf {uts} _{k}(\textsc {Conv} (t_{1},\omega )^{{{\mathcal {I}}}{{\mathbb {N}}}}) < \textsf {uts} _{k}(\textsc {Conv} (t_{2},\omega )^{{{\mathcal {I}}}{{\mathbb {N}}}})$ iff ${{\mathcal {I}}}{{\mathbb {N}}}\models \mathcal {T} _{\textit{full}} ({\varphi ,\omega })$.

$\square$

Finally, we can collect all the pieces and prove the correctness of the full translation between formulas.

Proof of Property 1 of Theorem 1

$(\Leftarrow )$::

Suppose $\varphi$ is not $T_{\mathrm{BV}}$-valid under $\omega$. Then there exists a $T_{\mathrm{IA}}$-interpretation ${\mathcal {J}}$ that maps variables in $\varvec{v}$ to positive integers such that ${\varphi }|_{{\omega }[{{\mathcal {J}}}]}$ is not $T_{\mathrm{BV}}$-valid. Hence, there exists an interpretation ${\mathcal {I}}$ of $T_{\mathrm{BV}}$ such that ${\mathcal {I}} \not \models {\varphi }|_{{\omega }[{{\mathcal {J}}}]}$. By Lemma 4, the constructed interpretation ${{\mathcal {I}}}{{\mathbb {N}}}$ of $T_{\mathrm {UF}\mathrm{IA} }$ does not satisfy $\mathcal {T} _{\textit{full}} ({\varphi ,\omega })$. Hence, $\mathcal {T} _{\textit{full}} ({\varphi ,\omega })$ is not $T_{\mathrm {UF}\mathrm{IA} }$-valid.

$(\Rightarrow )$::

Suppose $\mathcal {T} _{\textit{full}} ({\varphi ,\omega })$ is not $T_{\mathrm {UF}\mathrm{IA} }$-valid. Then there exists an interpretation ${\mathcal {I}}$ of $T_{\mathrm {UF}\mathrm{IA} }$ such that ${\mathcal {I}} \not \models \mathcal {T} _{\textit{full}} ({\varphi ,\omega })$. We define a $\mathrm{IA}$-interpretation ${\mathcal {J}}$ such that ${\varphi }|_{{\omega }[{{\mathcal {J}}}]}$ is not $T_{\mathrm{BV}}$-valid, by setting $x^{{\mathcal {J}}}=x^{{\mathcal {I}}}$ for each $x\in \mathrm{FV}(\omega )$. Translation $\mathcal {T} _{\textit{full}} ({\varphi ,\omega })$ is an implication whose left size is a conjunction whose first two conjuncts are: $\bigwedge _{x \in \mathrm{FV}(\varphi )} 0 \le \chi (x) < \textsf {pow2} (\omega ^b(x))$ (denoted A) and $\bigwedge _{w \in \mathrm{FV}(\omega )}w > 0$ (denoted B). Notice that ${\mathcal {J}}$ maps the variables in $\mathrm{FV}(\omega )$ to positive integers, as ${\mathcal {I}} \models B$. To show that ${\varphi }|_{{\omega }[{{\mathcal {J}}}]}$ is not $T_{\mathrm{BV}}$-valid, we define a $T_{\mathrm{BV}}$-interpretation ${{\mathcal {I}}}{\mathrm{BV}}$ by setting ${x}_{[{c}]} ^{{{\mathcal {I}}}{\mathrm{BV}}}={{\left[ {\chi (x)^{{\mathcal {I}}}}\right] }_{\mathbb {N}}}_{k}^{-1}$, where $c=\omega ^b(x) ^{{\mathcal {J}}}$ and ${{\left[ {.}\right] }_{\mathbb {N}}}_{.}^{-1}$ can be considered as an “inverse” of ${\left[ {.}\right] }_{\mathbb {N}}$. Concretely, if $0\le y < 2^{k}$, then there is a unique bit-vector x with minimal width such that ${\left[ {x}\right] }_{\mathbb {N}}=y$. If this minimal width is at most k, then ${{\left[ {y}\right] }_{\mathbb {N}}}_{k}^{-1}$ is that bit-vector, padded with zeros to width k. Otherwise, ${{\left[ {y}\right] }_{\mathbb {N}}}_{k}^{-1}$ is undefined. In the case of ${\mathcal {I}}$ above, every usage of ${{\left[ {.}\right] }_{\mathbb {N}}}_{.}^{-1}$ is defined, thanks to the fact that ${\mathcal {I}} \models A$. It can be easily shown that ${{{\mathcal {I}}}{\mathrm{BV}}}{{\mathbb {N}}}={\mathcal {I}}$. By Lemma 4, since ${\mathcal {I}} \not \models \mathcal {T} _{\textit{full}} ({\varphi ,\omega })$, we have that ${{\mathcal {I}}}{\mathrm{BV}}\not \models {\varphi }|_{{\omega }[{{\mathcal {J}}}]}$.

$\square$

4.2.2 Proof of Properties 2–4

The rest of the properties follow from Property 1 by showing that the axioms in Table 3 are valid in every interpretation of $T_{\mathrm {UF}\mathrm{IA} }$ that satisfies $\mathrm{AX}_{\textit{full}} (\varphi ,\omega )$.

The axioms of $\textsf {pow2}$ easily follow from simple properties of exponentiation. As for the bitwise logical operators, we explicitly prove the validity of “difference” for ${{ \& }^{{{\mathbb {N}}}}}$. The rest are shown similarly. Let $k>0$, $0\le x,y,z < 2^{k}$, and let ${\mathcal {I}}$ be an interpretation of $T_{\mathrm {UF}\mathrm{IA} }$ that satisfies $\mathrm{AX}_{\textit{full}} (\varphi ,\omega )$. Note that k, x, y and z are integer constants, and are therefore interpreted as themselves in ${\mathcal {I}}$. Let a, b and c be bit-vectors of width k such that $x={\left[ {a}\right] }_{\mathbb {N}}$, $y={\left[ {b}\right] }_{\mathbb {N}}$ and $z={\left[ {c}\right] }_{\mathbb {N}}$. Suppose ${\mathcal {I}}$ satisfies $x\not \approx y$. Then $a\not \approx b$, and so there exists some $0\le i\le k-1$ such that ${{a}\left[ {i}\right] } \not \approx {{b}\left[ {i}\right] }$. First, suppose ${a}\left[ {i}\right] =0$. Then ${b}\left[ {i}\right] =1$ and ${({a} { \& }^{\mathrm{BV}}{c})}\left[ {i}\right] =0$, and hence, ${{a} { \& }^{\mathrm{BV}}{c}} \not \approx {b}$. This means that ${{\left[ {{a} { \& }^{\mathrm{BV}}{c}}\right] }_{\mathbb {N}}} \not \approx {{\left[ {b}\right] }_{\mathbb {N}}}$, and thus, by Lemma 2, we have that ${\mathcal {I}}$ satisfies ${{{{ \& }^{{{\mathbb {N}}}}} ({k},{x},{z})}} \not \approx {y}$. Otherwise, ${a}\left[ {i}\right] =1$ and ${b}\left[ {i}\right] =0$. If ${{a} { \& }^{\mathrm{BV}}{c}} \approx {b}$ then ${c}\left[ {i}\right] =0$, which means that ${({b} { \& }^{\mathrm{BV}}{c})}\left[ {i}\right] =0$ and so ${{b} { \& }^{\mathrm{BV}}{c}} \not \approx {a}$. This means that ${{\left[ {{b} { \& }^{\mathrm{BV}}{c}}\right] }_{\mathbb {N}}} \not \approx {{\left[ {a}\right] }_{\mathbb {N}}}$, and thus by Lemma 2, we have that ${\mathcal {I}}$ satisfies ${{{{ \& }^{{{\mathbb {N}}}}} ({k},{y},{z})}} \not \approx {x}$. $\square$

5 Case Studies

We apply the techniques from Sect. 4 to three case studies:

• 1. the verification of invertibility conditions from Niemetz et al. [23];

• 2. the verification of compiler optimizations as generated by Alive [22]; and

• 3. the verification of rewrite rules that are used in SMT solvers.

For these case studies, we consider a set of verification conditions that originally use fixed-size bit-vectors, and exclude formulas involving multiple bit-widths. This restriction simplifies the implementation but is interesting enough as each case study includes many verification conditions of this sort. Generalizing the framework beyond this restriction is technical but straightforward, and is left for future work. In essence, such an extension amounts to including the well-sortedness conditions of the underlying mappings $\omega$ in the translated benchmarks (e.g., equalities between bit-width variables that are associated with parametric bit-vector variables that occur under the same operator). For the case studies that we consider here, such extra constraints are trivial.

For each formula $\phi$, we first produce a parametric version $\varphi$ by replacing each variable in $\phi$ by a fresh $\mathsf {x} \in X^{*}$ and each (concrete) bit-vector constant by a fresh $\mathsf {z} \in Z^*$. We define $\omega ^b(\mathsf {x}) =\omega ^b(\mathsf {z}) = k$ for a fresh integer variable k and let $\omega ^N\!(\mathsf {z})$ be the integer value corresponding to the bit-vector constant it replaced. We then define $\omega =(\omega ^b, \omega ^N)$ and invoke our translation from Sect. 4 on the parametric bit-vector formula $\varphi$. If the resulting formula is valid, the original verification condition holds independently of the original bit-width. In each case study, we report on the success rates of determining the validity of these formulas for axiomatization modes full, partial, comb, and qf. Overall, axiomatization mode comb yields the best results.

All experiments described below require an SMT solver with support for the SMT-LIB 2 logic UFNIA. We used all three participants in the UFNIA division of the 2018 SMT competition: CVC4  [2] (GitHub master 6eb492f6), Z3  [12] (version 4.8.4), and Vampire [18] (GitHub master d0ea236). Z3 and CVC4 use various strategies and techniques for quantifier instantiation including E-matching [11], and enumerative [29] and conflict-based [32] instantiation. For non-linear integer arithmetic, CVC4 uses an approach based on incremental linearization [8, 9, 31]. Vampire is a superposition-based theorem prover for first-order logic based on the AVATAR framework [35], which has been extended to support some theories, including integer arithmetic [28]. We performed all experiments on a cluster with Intel Xeon E5-2637 CPUs with 3.5 GHz and 32 GB of memory. We imposed a time limit of 300 seconds (wallclock) and a memory limit of 4GB for each solver/benchmark pair.² We consider a bit-width independent property to be proved if at least one solver proved it for at least one of the axiomatization modes. The solving time reported does not include the (negligible) translation time, as the translation for all benchmarks was performed before running the experiments on the translated benchmarks.³

5.1 Verifying Invertibility Conditions

Niemetz et al. [23] present a technique for solving quantified bit-vector formulas that utilizes invertibility conditions to generate symbolic instantiations. Intuitively, an invertibility condition $\phi _{\mathrm{c}}$ for a literal $\ell [x]$ is the exact condition under which $\ell [x]$ has a solution for x, i.e., $\phi _{\mathrm{c}} \Leftrightarrow \exists x.\ell [x]$ is $T_{\mathrm{BV}}$-valid. For example, consider bit-vector literal ${x} { \& }^{\mathrm{BV}}{s} \approx t$ with $x \not \in \mathrm{FV}(s) \cup \mathrm{FV}(t)$; then, the invertibility condition for x is ${t} { \& }^{\mathrm{BV}}{s} \approx {t}$. The authors define invertibility conditions for a representative set of literals having a single occurrence of x that involve the bit-vector operators listed in Table 1, excluding extraction, as the invertibility condition for the latter is trivially $\top$. A considerable number of these conditions were determined by leveraging Syntax-Guided Synthesis (SyGuS) techniques [1]. The authors further verified the correctness of all conditions for bit-widths 1 to 65. However, a bit-width-independent proof of correctness of these conditions was left to future work. In the following, we apply the techniques of Sect. 4 to tackle this problem. Note that for this case study, we exclude operators involving multiple bit-widths, namely bit-vector extraction and concatenation. For the former, all invertibility conditions are $\top$, and for the latter it is easy to produce a hand-written parametric proof of correctness of its invertibility conditions.

5.1.1 Proving Invertibility Conditions

Let $\ell [x]$ be a bit-vector literal of the form $\diamond x \bowtie t$ or $x \diamond s \bowtie t$ (dually, $s \diamond x \bowtie t$), with operators $\diamond$ and relations $\bowtie$ as defined in Table 1. To prove the correctness of an invertibility condition $\phi _{\mathrm{c}}$ for x independent of the bit-width, we have to prove the validity of the formula:

$$\begin{aligned} \phi _{\mathrm{c}} \Leftrightarrow \exists x . \ell [x], \end{aligned}$$

(1)

where occurrences of the variables s and t are implicitly universally quantified. We then want to prove that Eq. (1) is $T_{\mathrm{BV}}$-valid under $\omega$. Considering the two directions of Eq. (1) separately, we get:

$$\begin{aligned} \exists x . \ell [x,s,t]\Rightarrow \phi _{\mathrm{c}} [s,t] \end{aligned}$$

(rtl)

and

$$\begin{aligned} \phi _{\mathrm{c}} [s,t]\Rightarrow \exists x . \ell [x,s,t]. \end{aligned}$$

(ltr)

The validity of (rtl) is equivalent to the unsatisfiability of the quantifier-free formula:

$$\begin{aligned} \ell [x,s,t]\wedge \lnot \phi _{\mathrm{c}} [s,t]. \end{aligned}$$

(rtl')

Eliminating the quantifier in (ltr) is much trickier. It typically amounts to finding a symbolic value for x such that $\ell [x,s,t]$ holds provided that $\phi _{\mathrm{c}} [s,t]$ holds. We refer to such a symbolic value as a conditional inverse.

5.1.2 Conditional Inverses

Given an invertibility condition $\phi _{\mathrm{c}}$ for x in bit-vector literal $\ell [x]$, we say that a term $\alpha _{\mathrm{c}}$ is a conditional inverse for x if $\phi _{\mathrm{c}} \Rightarrow \ell [\alpha _{\mathrm{c}} ]$ is $T_{\mathrm{BV}}$-valid. For example, in literal ${({x}\, {|}^{\mathrm{BV}}{s})}\, {\le _{\mathrm{u}}}^{ {\mathrm{BV}}}{t}$, the term s itself is a conditional inverse for x: given that there exists some x such that ${({x}\, {|}^{\mathrm{BV}}{s})}\, {\le _{\mathrm{u}}}^{ {\mathrm{BV}}}{t}$, we have that $({s}\, {|}^{\mathrm{BV}}{s}){\le _{\mathrm{u}}}^{ {\mathrm{BV}}}t$. When a conditional inverse $\alpha _{\mathrm{c}}$ for x is found, we may replace (ltr) by:

$$\begin{aligned} \phi _{\mathrm{c}} \Rightarrow \ell [\alpha _{\mathrm{c}} ] \end{aligned}$$

(ltr')

Clearly, (ltr’) implies (ltr). However, the converse may not hold, i.e., there may be models that falsifiy (ltr’) without falsifying (ltr). Notice that if the invertibility condition for x is $\top$, the conditional inverse is in fact unconditional. The problem of finding a conditional inverse for a bit-vector literal $x \diamond s \bowtie t$ (dually, $s \diamond x \bowtie t$) can be defined as a SyGuS problem by asking whether the (second-order) formula $\exists C\forall s\forall t. \phi _{\mathrm{c}} \Rightarrow C(s,t) \diamond s \bowtie t$ is satisfiable, where C is a binary function symbol. If such a function C is found, then it is in fact a conditional inverse for x in $\ell [x]$. We synthesized conditional inverses for x in $\ell [x]$ for bit-width 4 with variants of the grammars used in [23] to synthesize invertibility conditions. For each grammar, we generated 160 SyGuS problems, one for each combination of bit-vector operator and relation from Table 1 except for extraction and concatenation, counting commutative cases only once. We used the SyGuS solver CVC4SY  [30] to solve these problems, and out of 160, we were able to synthesize candidate conditional inverses for 143 invertibility conditions. For 12 out of these 143, we found that the synthesized terms were not conditional inverses for every bit-width by checking (ltr’) for bit-widths up to 64.

Tables 4 and 5 list all verified conditional inverses that we found. Note that we omitted superscript BV from all bit-vector symbols for better readability. The synthesized conditional inverses are useful for bit-width independent verification of the correctness of the invertibility conditions. In addition, they are interesting in their own right: they provide more constructive information about bit-vector literals by showing a concrete term for a general solution, which is an improvement compared to [23], where a formula that states the existence of such a solution was synthesized, without necessarily showing how to construct such a solution. We plan to study the affect of these more specific solutions in the context of quantifier instantiation, and to compare it to the technique of [23].

Table 4 Conditional inverses for relations $\bowtie$ in $\left\{ {{{} \approx {}}, {{} \not \approx {}}, <_u, \le _u, >_{u}, \ge _u}\right\}$

Table 5 Conditional inverses for relations $\bowtie$ in $\left\{ {<_s, \le _s, >_s, \ge _s}\right\}$

5.1.3 Results

Table 6 summaries the results of verifying invertibility conditions. For each invertibility condition, it states whether it was fully proved, only one direction of it was proved, or none of the directions were proved. Table 7 provides detailed information on the results for the axiomatization modes full, partial, and qf discussed in Sect. 4.

Table 6 Invertibility conditions verification

We use $\rightarrow$and $\leftarrow$to indicate that only direction left-to-right (ltr or ltr’) or right-to-left (rtl’) were proved, and $\checkmark$ and ✕to indicate that both or none of the directions were proved. Additionally, we use $\rightarrow _{\alpha _{\mathrm{c}}}$ (resp. $\rightarrow _{\mathrm{no}\,\alpha _{\mathrm{c}}}$) to indicate that for direction left-to-right, formula (ltr’) (resp. (ltr)) was proved with (resp. without) plugging in a conditional inverse.

Overall, out of 160 invertibility conditions, we were able to fully prove 110, and for 19 (resp. 17) conditions we were able to prove only direction rtl’ (resp. ltr’). For direction right-to-left, 129 formulas (rtl’) overall were successfully proved to be unsatisfiable. Out of these 129, 32 formulas were actually trivial since the invertibility condition $\phi _{\mathrm{c}}$ was $\top$. For direction left-to-right, overall, 127 formulas were proved successfully, and out of these, 102 (resp. 94) were proved using (resp. not using) a conditional inverse. Furthermore, 33 formulas could only be proved when using a conditional inverse. Thus, using conditional inverses was helpful for proving the correctness of invertibility conditions. Interestingly, the opposite was also observed: 11 invertibility conditions for which conditional inverses were found, were not proven using conditional inverses, but were proven without them. This could be explained by the fact that even though conditional inverses eliminate a quantifier (thus making the problem easier), they produce a stronger formula, as (ltr’) implies (ltr) (thus making the problem harder).

Considering the different axiomatization modes, overall, with 104 fully proved and only 17 unproved instances, axiomatization comb performed best. Interestingly, even though axiomatization qf only includes some of the base cases of axiomatization partial, it still performs well. This may be due to the fact that in many cases, the correctness of the invertibility condition does not rely on any particular property of the operators involved. For example, the invertibility condition $\phi _{\mathrm{c}}$ for literal ${{x} { \& }^{\mathrm{BV}}{s}} \approx {t}$ is ${{t} { \& }^{\mathrm{BV}}{s}} \approx {t}$. Proving the correctness of $\phi _{\mathrm{c}}$ amounts to coming up with the right substitution for x without relying on any particular axiomatization of ${{ \& }^{{{\mathbb {N}}}}}$. In contrast, the invertibility condition $\phi _{\mathrm{c}}$ for literal ${{x} { \& }^{\mathrm{BV}}{s}} \not \approx {t}$ is ${t} \not \approx {0} \vee {s} \not \approx {0}$. Proving the correctness of $\phi _{\mathrm{c}}$ relies on axioms regarding ${ \& }^{\mathrm{BV}}$ and $\sim ^{\mathrm{BV}}$. Specifically, we have found that from axiomatization partial, it suffices to keep “min” and “idempotence” to prove $\phi _{\mathrm{c}}$ in that case.

The project of verifying invertibility conditions for arbitrary bit-widths was recently extended by Ekici et al. [14], where a representative subset consisting of 11 invertibility conditions out of the 50 that were not proven by our approach were proven semi-automatically using the Coq proof assistant, building on a library for SMT-LIB 2 bit-vectors previously developed by Ekici et al. [13].

Table 7 Invertibility condition verification using axiomatization modes comb, full, partial, and qf

5.2 Verifying Alive Optimizations

Lopes et al. [22] introduces Alive, a tool for proving the correctness of compiler peephole optimizations. Alive has a high-level language for specifying optimizations. The tool takes as input a description of an optimization in this high-level language and then automatically verifies that applying the optimization to an arbitrary piece of source code produces optimized target code that is equivalent under a given precondition. It can also automatically translate verified optimizations into C++ code that can be linked into LLVM  [21]. For each optimization, Alive generates four constraints that encode the following properties, assuming that the precondition of the optimization holds:

• 1. Memory Source and Target yield the same state of memory after execution.

• 2. Definedness The target is well-defined whenever the source is.

• 3. Poison The target produces so-called poison values (caused by LLVM ’s $nsw$, $nuw$, and $exact$ attributes) only when the source does.

• 4. Equivalence Source and target yield the same result after execution.

From these verification tasks, Alive can generate benchmarks in SMT-LIB 2 format in the theory of fixed-size bit-vectors, with and without quantifiers. For each task, types are instantiated with all possible valid type assignments (for integer types up to a default bound of 64 bits). In the following, we apply our techniques from Sect. 4 to prove Alive verification tasks independently from the bit-width. For this, as in Lopes et al. [22], we consider the set of optimizations from the $instcombine$ optimization pass of LLVM, provided as Alive translations (433 total).⁴ Of these 433 optimizations, 113 are dependent on a specific bit-width; thus, we focus on the remaining 320. We further exclude optimizations that do not comply with the following criteria:

• In each generated SMT-LIB 2 file, only a single bit-width is used.

• All SMT-LIB 2 files generated for a property (instantiated for all possible valid type assignments) must be identical modulo the bit-width (excluding, e.g., bit-width dependent constants other than 0, 1 and (un)signed min/max).

As a useful exception to the first criterion, we included instances where all terms of bit-width 1 can be interpreted as Booleans. Overall, we consider bit-width independent verification conditions 1–4 for 180 out of 320 optimizations. None of these include memory operations or poison values, and only some have definedness constraints (and those are simple). We thus only consider the equivalence verification conditions for these 180 optimizations.

5.2.1 Results

Table 8 summarizes the results of verifying the equivalence constraints for the selected 180 optimizations from the instcombine LLVM optimization pass. The first column lists all families with the number of bit-width independent optimizations per family (320 total). The second column indicates how many in each family were in the set of 180 considered optimizations, and the remaining columns show how many of those considered were proved with each axiomatization mode.

Table 8 Alive optimizations verification using axiomatizations comb, full, partial and qf

Overall, out of 180 equivalence verification conditions, we were able to prove 88. Our techniques were most successful for the AndOrXor family. This is not surprising, since many verification conditions of this family require only Boolean reasoning and basic properties of ordering relations that are already included in the theory $T_{\mathrm{IA}}$. For example, given bit-vector term a and bit-vector constants $C_1$ and $C_2$, optimization AndOrXor:979 from instcombine essentially rewrites $({a}\, {<_{\mathrm{s}}}^{ {\mathrm{BV}}}{C_1} \wedge {a}\, {<_{\mathrm{s}}}^{ {\mathrm{BV}}}{C_2})$ to ${a}\, {<_{\mathrm{s}}}^{ {\mathrm{BV}}}{C_1}$, provided that precondition ${C_{1}}\, {<_{\mathrm{s}}}^{ {\mathrm{BV}}}{C_{2}}$ holds. To prove its correctness, it suffices to apply the transitivity of $<_{\mathrm{s}}^{\mathrm{BV}}$ with Boolean reasoning. The same holds when lifting this equivalence to the integers, deducing the transitivity of ${<_s}^{{{\mathbb {N}}}}$ from that of the builtin < relation of $T_{\mathrm{IA}}$.

None of the 9 instances from the Shifts family were proven. These instances are more complicated than others, since they combine bitwise and arithmetical operations and thus rely on the axiomatization of these operators. Solving the instances from the Shifts family is an interesting challenge for future work. Adding specialized axioms to axiomatization partial is one promising approach.

Interestingly, for this case study, the results from the different axiomatization modes are very similar. This can again be explained by the fact that many optimizations rely on properties of the integers that are already included in $T_{\mathrm{IA}}$, without requiring any particular property of functions $\textsf {pow2}$, ${{ \& }^{{{\mathbb {N}}}}} {}$, ${\mid }^{{{\mathbb {N}}}} {}$ and ${\oplus }^{{{\mathbb {N}}}}$ (as in the above example).

Note that we have also tried using our approach for proving the equivalence verification conditions for up to a bit-width of 64. This was done by adding an assertion of the form $0 < k \le 64$ for the bit-width variable k. However, all optimizations that were proven correct this way were already proven correct for arbitrary bit-widths, which suggests that this restriction did not make the input problem easier for the solvers.

5.3 BV Rewriting

SMT solvers for the theory of fixed-size bit-vectors heavily rely on rewriting to reduce the size of the input formula prior to solving the problem. Since these rewrite rules are usually implemented independently of the bit-width, verifying that they hold for any bit-width is crucial for the soundness of the solver. For this case study, we used a feature of the SyGuS solver in CVC4 that allows us to enumerate equivalent bit-vector terms/formulas (rewrite candidates) for a certain bit-width up to a certain term depth (nesting level of operators) [26]. We generated 1575 pairs of equivalent bit-vector terms of depth three and 431 equivalent pairs of formulas of depth two for bit-width 4 and translated them to integer problems with axiomatization modes full, partial, qf, and comb, resulting in $6300+1724 = 8024$ benchmarks in total. Since rewrites that have been proved correct can be used to further axiomatize the integer translation, we collected all proven rewrites after each run, added them as axioms to the initial problems and reran the experiments. This was repeated until we reached a fixpoint, i.e., no further rewrites were proved. With this approach, we were able to prove 409 out of the 431 formula equivalences (94%) by reaching a fixpoint at the first iteration. For the equivalent terms, we initially proved 878 out of the 1575 equivalences, which increased to 935 (59%) after adding all axioms from the first run, reaching a fixpoint after two iterations.

5.4 Summary

Summarizing these three case studies, Table 9 shows the percentage of problems that were proved by the various solver in each case study. Numbers in parenthesis denote the total number of SMT-LIB 2 benchmarks used in each case (including all encodings). Rows 1–3 show the percentage of problems proved by each solver, row 4 shows the percentage of problems proved by all three solvers, and row 5 shows the percentage of problems that were proved by at least one solver, which corresponds to the success rate of the virtual best solver.

Table 9 Summary of solvers performance on all generated SMT-LIB 2 benchmarks

6 Conclusion and Further Research

We have studied several translations from bit-vector formulas with parametric bit-width to the theories of integer arithmetic and uninterpreted functions. The translations differ in the way that the operator $2^{(\_)}$ and bitwise logical operators are axiomatized, namely, fully (using their recursive definition) or partially (using some of their key properties). Our empirical results show that state-of-the-art SMT solvers are capable of solving the translated formulas for various benchmarks that originate from the verification of invertibility conditions, LLVM optimizations, and rewriting rules for fixed-size bit-vectors.

In future research, we plan to investigate an implementation of our translation in a proof assistant such as Coq, for which a bit-vector library was recently developed [13], and supports the formalization of bit-width independent properties. A verified translation to integers can open a path to automating proofs for such properties in Coq. This will require also supporting proofs in the SMT solver for non-linear arithmetic and quantifiers. We also plan to explore satisfiable benchmarks and to consider lazy variants of the proposed translations. In such a setting, a partitioning of the input problem into sub-problems can be beneficial, as for each part, only the axioms that relate to the operators that occur in it will be considered. Something similar can be done with the bounds on the variables that occur in each part. In such an approach, we can sometimes avoid the introduction of quantifiers (which currently are always introduced, by adding all the axioms, even if the original formula is quantifier-free). This has potential in improving performance, and can also help with Nelson-Oppen style combination with other theories. Finally, we are experimenting with solving fixed-width (i.e., non-parametric) bit-vector formulas using a similar translation to integers. The main difference, though, is that in such a case, quantification is not needed. For exponentiation, the exponent is always a numeral when the original formula has only fixed-width bit-vectors. For the bitwise operators, their corresponding axiom schemas can be instantiated lazily or eagerly. Since the bit-width is known, this can be done in a complete manner.