Verifying code depending on bit vectors

[Mark Tuttle]

Can you give further guidance on how to verify code that depends on bit vectors?  Can you describe something I might implement that would give me more direct access to bit vector support in the underlying solver?

I'm trying to verify the following function that counts the number of leading ones in an unsigned integer.

static size_t countHighBits( uint8_t c )

{

  uint8_t n = c;

  size_t i = 0;

  while( ( n & 0x80U ) != 0U )

  {

    i++;

    n = ( n & 0x7FU ) << 1U;

  }

  return i;

}

Following guidance I received in another question on bit vectors, the best I can do is the following.  It depends on a fixpoint function shift_left that uses the inductive data type for bit vectors to compute the left shift of an integer.  I had to write my own function because the existing shiftleft lemma is not a function that I can use in assertions and it does not limit the result to a fixed bit width.  Run this with `verifast -target 32bit -prover z3v4.5 -shared test.c`.  

#include <stddef.h>

#include <stdint.h>

//@ #include <bitops.gh>

/*@

fixpoint Z take_low_bits(Z bits, int count) {

  switch (bits) {

    case Zsign(bit): return bits;

    case Zdigit(bits0, bit): return

      count <= 0 ?

        take_low_bits(bits0, count-1) :

        Zdigit( take_low_bits(bits0, count-1), bit);

  }

}

fixpoint Z push_low_bits(Z bits, nat count, bool bit) {

  switch (count) {

    case zero: return bits;

    case succ(count0): return Zdigit(push_low_bits(bits, count0, bit), bit);

  }

}

fixpoint uint8_t shift_left(Z bits, int count) {

  return

    int_of_Z(

       take_low_bits(

         push_low_bits(bits, nat_of_int(count), false), 8) );

}

@*/

static size_t countHighBits( uint8_t n )

//@ requires 0 <= n && n <= 0xFFU;

//@ ensures 0 <= result && result <= 8;

{

  size_t i = 0;

  //@ Z z_high_mask = Z_of_uint8(0x80U);

  //@ Z z_low_mask = Z_of_uint8(0x7FU);

  //@ Z z_n0 = Z_of_uint8(n);

  //@ bitand_def(n, z_n0, 0x80U, z_high_mask);

  while( ( n & 0x80U ) != 0U )

    /*@

      invariant 0 <= i && i <= 8U && n == shift_left(z_n0, i);

    @*/

  {

    //@ Z z_n = Z_of_uint8(n);

    //@ bitand_def(n, z_n, 0x7FU, z_low_mask);

    uint8_t low_bits = (uint8_t) (n & 0x7FU);

    //@ shiftleft_def(low_bits, nat_of_int(1));

    n = (uint8_t) (low_bits << 1U);

    //@ z_n = Z_of_uint8(n);

    //@ bitand_def(n, z_n, 0x80U, z_high_mask);

    i++;

  }

  return i;

}

One problem with this solution is that it is slow.  It takes 34 seconds in contrast to small fractions of a second for other functions.  It also requires rewriting the engineer's code to refactor a bit vector expression as a sequence of pairwise bit vector operations.  I think I could do better if I had more direct access to the bit vector support in Z3, and if I could use bit vector expressions in the assertion language.

Thanks!

Mark

[Bart Jacobs]

As for speed: after some experimenting, I discovered that just inserting

//@ switch (i) { case 0: case 1: case 2: case 3: case 4: case 5: case 6: case 7: case 8: }

at the top of the loop body reduces the verification time to a few seconds. Of course, applying this technique in the case of 64-bit ints might not completely solve the performance issue.

As for the other problem you mention: do you mean the need to call these _def lemmas? One solution might be to extend VeriFast so that you can mark a variable as "/*@ bitvector @*/". Then their value would be a term of SMT solver type "bitvector(N)" rather than "int".

Might be a good task for an intern ;-)

--
You received this message because you are subscribed to the Google Groups "VeriFast" group.
To unsubscribe from this group and stop receiving emails from it, send an email to verifast+u...@googlegroups.com.
To view this discussion on the web visit https://groups.google.com/d/msgid/verifast/ad250f0b-0aff-4ed3-8055-991a168ee856n%40googlegroups.com.

[Mark R. Tuttle]

Yes, my first solution included a switch statement giving explicit values for n for each iteration of the loop.  Thanks.

[Bart Jacobs]

On 10/06/2021 13:01, Bart Jacobs wrote:
> As for the other problem you mention: do you mean the need to call
> these _def lemmas? One solution might be to extend VeriFast so that
> you can mark a variable as "/*@ bitvector @*/". Then their value would
> be a term of SMT solver type "bitvector(N)" rather than "int".
>
> Might be a good task for an intern ;-)
>
>

There is a quicker solution: to change VeriFast so that evaluating x &
y, where x and y are of type uint8_t, results in the term bitand(x, y)
plus the equality bitand(x, y) == bitand_uintN(x, y, 8). bitand_uintN(x,
y, 8) can serve as a trigger for an autolemma saying bitand_uintN(x, y,
N) == int_of_Z(Z_and(Z_of_uintN(x, N), Z_of_uintN(y, N))). Lemmas
Z_of_uint8 etc would get an additional postcondition saying result ==
Z_of_uintN(x, 8). I hope to implement this later today.

[Mike Whalen]

Perhaps we could have a tool option that allowed a bitvector representation rather than LIA for integers, globally?  Using comments might require many annotations.  I think the bitvector solvers are pretty good, so performance would be o.k.

Mike

[Mark R. Tuttle]

If this works, the bit operations appearing commonly in the code are are x&y, x|y, x<<y, x>>y.

[bart....@cs.kuleuven.be]

I just pushed a commit so that the following now verifies (in less than a second):

  //@ Z_of_uint8(0x80U);
  //@ Z_of_uint8(0x7FU);

  //@ Z z_n0 = Z_of_uint8(n);

  while( ( n & 0x80U ) != 0 )

    /*@
      invariant 0 <= i && i <= 8U && n == shift_left(z_n0, i);
    @*/
  {

    //@ switch (i) { case 0: case 1: case 2: case 3: case 4: case 5: case 6: case 7: case 8: }

    //@ Z_of_uint8(n);

    uint8_t low_bits = (uint8_t) (n & 0x7FU);

    n = (uint8_t) (low_bits << 1U);

    //@ Z_of_uint8(n);
    i++;
  }

  return i;
}

So, no bitvectors yet, but so far it seems that by inserting Z_of_uint{N} calls in the appropriate places one can get pretty low annotation overhead and pretty good performance without them.

Best,
Bart