When verifying programs with VCC the interpretation domain for integer variables is mathematical integers. The verification conditions are checked with a SMT solver supporting linear integer arithmetic. There are additional restrictions that made this treatment sound (including generated assertions about overflows).

However it is sometimes required to use non-linear operators or use properties of the 32 or 64 bit U-2 arithmetic that the machine is really using. Fortunately the Z3 SMT solver that we’re using is also equipped with a decision procedure for fixed size bit-vectors with all relevant arithmetic operators (including non-linear ones).

We do not use it in general for performance reasons, but it’s usually OK to use it for proving specific facts about the non-linear operators. It is done using the bv_lemma(prop) construction. The prop is required to be a closed sentence (i.e. it cannot refer to local or global variables or the program, nor the heap). It is first proven using bit-vector decision procedure and then assumed in the integer domain. For example:

#include "vcc.h"

#define MASK ((1 << 2) | (1 << 5))

void foo(unsigned index)
    requires(index < 32)
    unsigned res = 0;

    bv_lemma(forall(unsigned i; ((1 << i) & MASK) <==> i == 2 || i == 5));

    if ((1 << index) & MASK)
        res = 1;

    assert(index == 2 ==> res == 1);
    assert(res == 1 ==> index <= 5);

The tricky part is figuring out what exactly property you need to assert with bv_lemma(...). Note that all operations inside of the bv_lemma(...) are interpreted as unchecked, which means they will only be triggered by the real operation in the code, if those operations are also unchecked. This is not a problem in this case, because there is no difference between checked and unchecked << operator.

Last edited Nov 13, 2009 at 12:05 PM by stobies, version 3


No comments yet.