Bitwise operations make the SMT solver run infinitely

[radumcostache]

Recently I came across a weird issue while using Boogie. I needed to verify something with bitwise operations, and for this I imported the relevant functions from Z3 inside Boogie (to be concise I will address just the bitwise and + the conversion functions):

function {:bvbuiltin "bvand"} bvand_64(x: bv64, y: bv64): bv64;
function {:bvbuiltin "(_ int2bv 64)"} int2bv_64(x: int): bv64;
function {:bvbuiltin "bv2int"} bv2int_64(bv: bv64): int;

And I defined a function that would take two ints and would return the bitwise and of them:

function  bit_and(x: int, y: int): int
{
    bv2int_64(bvand_64(int2bv_64(x), int2bv_64(y)))
}

For convinience, I created two maps one that would map two ints to their maximum and one that would map the two ints to their bitwise_and:

const sum: [int, int] int;
axiom sum == (lambda x, y: int :: x + y);

const andd: [int, int] int;
axiom andd == (lambda x, y: int :: bit_and(x, y));

After this, the verification runs fine for functions that have true postconditions, but for any function that would have some false postcondition, the SMT solver will hang, for example:

procedure test();
    ensures false;

I have to also say that if I leave just one of the consts (andd or sum) it would not hang. Also, if I have the sum and consts for any other non-bitwise operations it doesn't hang, but if I have two bitwise operations it hangs.

[atomb]

This is ultimately caused by Z3 rather than Boogie, I believe. Converting between integers and bit vectors, as implemented in Z3, involves complex non-linear math, which tends to be practical to solve only for very small bit vector sizes. For bit vectors of size 64, it's generally intractable. I suspect that if you were to, say, use bv8, instead, the problem might go away (though I imagine it wouldn't be appropriate for your problem anymore).

The best strategy in general is to avoid converting between integers and bit vectors. Addition is defined on bit vectors, for example, so you can may be able to state your entire problem in terms of bit vectors and avoid integers altogether.

[radumcostache]

@atomb, thank you for your reply and directions. While I agree with you that conversion for SMT solvers is indeed very complex and I should probably avoid it, my issue is not directly with the conversion operation, but with the fact that having both the bitwise and axiom and the sum/any other non-bitwise or bitwise operation would cause Z3 hanging. Moreover, as I said, this happens just for postconditions that prove false and, as you can see in the example that I gave, it can have nothing to do with that particular operation (but if you have ensures true; this runs perfectly fine).

I also agree that the issue is probably caused by Z3, but I opened the issue here because I would first want to exclude an issue with the translation into SMT.

[petemud]

Looks like Boogie lambdas are defined with quantifiers in SMT. Defining them as Z3 lambdas or using as-array would help.

(declare-fun bit_and (Int Int) Int)
(assert
  (forall ((x Int) (y Int))
    (= (bit_and x y) (bv2int (bvand ((_ int2bv 64) x) ((_ int2bv 64) y))))
  )
)
(declare-fun andd () (Array Int Int Int))
(assert
  (forall ((x Int) (y Int)) (= (select andd x y) (bit_and x y)))
  ;(= andd (lambda ((x Int) (y Int)) (bit_and x y)))
  ;(= andd (_ as-array bit_and))
)
(check-sat)
(get-model)

[atomb]

I think @petemud's suggestion is a good one, and that using Z3 lambda for Boogie lambda would be beneficial. I'd have to double check that this is possible in all cases, but it would at least be possible in many.

The reason an issue arises when they're encoded with quantifiers is that, in principle, it may be possible to prove the goal at hand using a contradiction between assumptions. So, although your goal doesn't mention those functions, it could be possible to prove it using some sort of complex reasoning about integer <-> bit vector conversions. The more assumptions exist, and the more operations they use, the harder it is. It isn't possible to prove a contradiction in this case, but it takes an infeasible amount of work for Z3 to confirm that. On top of that, doing complex integer or bit vector math tends to be less efficient (sometimes significantly so) when quantifiers are present.