LARA

Fixed-Width Bitvectors

Bitvector: integer from some finite inteval of length $2^n$

Example: $[0,2^{32}-1]$

Logic on bitvectors.

  • formulas for +.

We can reduce reasoning on bitvectors to reasoning in propositional logic.

Application:

  • exact reasoning about Java integers
  • finding counterexamples for formulas over unbounded integers

Expressing Linear Arithmetic with Given Bounds

Consider formulas in our linear arithmetic language: 

 T ::= K | V | (T + T) | (T - T) | (K * T) | (T / K) | (T % K)
 F ::= (T=T) | (T < T) | (T > T) | (~F) | (F & F) | (F|F)
 V ::= x | y | z | ...
 K ::= 0 | 1 | 2 | ...

Suppose we are given bounds for all integer variables and that they belong to $[0,2^B-1]$.

We present translation from $F$ to equisatisfiable $prop(F)$ in propositional logic. That is,

\begin{equation*} \exists x_1,\ldots,x_n.\ F \end{equation*}

is equivalent to

\begin{equation*} \exists p_1,\ldots,p_m.\ prop(F) \end{equation*}

Where $FV(F)=\{x_1,\ldots,x_n\}$ and $FV(prop(F)) = \{p_1,\ldots,p_m\}$.

For each bounded integer variable $x \in [0,2^B-1]$ we introduce propositional variables corresponding to its binary representation.

The constructions for operations correspond to implementing these operations in hardware circuits:

  • adder for +
  • shift for *
  • comparator for <, =

Example: propositional formula expressing $x + y = z$ when $x,y,z \in [0,2^B-1]$.

Note that subtraction can be expressed using addition, similarly for / and %.

How to express inverse operations for nested terms?

Additional pre-processing is useful. Much more on such encodings we will see later, and can also be found here:

Later we will see how to prove that linear arithmetic holds for all bounds and not just given one.