What is the fastest way to deal with intExp and BitVecExp?

[andre-sapientai]

We are modeling our numbers as intExp, but when we are treating some bitwise operations, we convert to BitVecExp using mkInt2BV.

Then we use some bitwise operation, like mkBVAND, mkBVOR, mkBVXOR, mkBVSHL, mkBVASHR and mkBVLSHR.

And at the end we convert back to intExpr, using mkBV2Int.

But we notice that mkBV2Int is very slow.

Do we have a way to do that using intExpr directly? Or some another way to be faster?

Thanks

[ThomasHaas]

We had a similar issue when model checking C programs with bit operations.
Even just a single conversion from integers to bit-vectors (Int2BV) could make an otherwise trivial problem unsolvable.
We observed slow-downs of several orders of magnitude.

The following can help to tackle the issue:

• (1) Some special bit operations can be replaced by integer one's: for example x << k ---> x * 2^k (assuming no overflow, and k constant), x & 2^k ---> x mod 2^k (assuming k constant). This type of translation works well if you do verification of compiled programs and the compiler added some optimizations that converted arithmetic to bit-vector operations (like replacing multiplication by shifts).
• (2) Just use bit-vectors everywhere as soon as you need to use them somewhere. This is what we ended up doing because (1) worked only in very specific cases. The rule-of-thumb is that mixing theories should be avoided if possible.
• (3) The conversion BV2Int should be a lot faster than Int2BV. If the BV operations happen "early", that is, they depend only on a very few other values, then it is possible to encode only those dependencies as BV and convert the final result to an integer for the remaining encoding.
  I give some pseudo-code to demonstrate this:

// Pseudo C-code
int a = ...;
int b = f(a);
int c = a & b; // Only bit-operation
int d = g(c)
// ....
int y = ...
int z = h(y)

this can be converted to

bv a = ...; // Now bv
bv b = f(a); // Now bv
int c = BV2Int(a & b); // Only bit-operation converted to int
int d = g(c) // Only ints from here onwards
// ....
int y = ...
int z = h(y)

This way only the necessary parts are encoded via bit-vectors. If there are many BV operations or they have deep dependency chains, then doing full BV encoding (2) might be better.
IIRC, this approach is/was used by the Smack tool. Unfortunately, I don't remember the concrete paper where the approach is explained (in the context of model checking programs).