Loop invariant could not be verified.

Apr 15, 2011 at 2:16 PM

A very basic and simple loop invariant but still I am not be debug why VCC is able to verify the loop invariant of the function given below. 'Loop body invariant doesn't verifies'

What could be the possible point i am missing here.

============================================

bool bitmap_contains (const struct bitmap *b, size_t start, size_t cnt, bool value)

requires(b!=NULL)

requires((start + cnt )<= b->bit_cnt)

requires(wrapped(b))

ensures(!result <==> forall(size_t k;k>=0 && k<cnt;bitmap_test(b,start+k)!=value))

ensures(result <==> exists(size_t k;k>=0 && k<cnt;bitmap_test(b,start+k)==value))

{

size_t i, idx;

for (i = 0; i < cnt; i++)

      invariant(i>=0 && i<=cnt)

      invariant(forall(size_t k; k>=0 && k<i; ((b->bits[elem_idx (start+k)] & bit_mask (start+k)) != 0) != value))             // NOT able to verify it ??

      invariant(start+i<=b->bit_cnt)

      {

       idx=start+i;          

       if (((b->bits[elem_idx (idx)] & bit_mask (idx)) != 0) == value)

        return true;

   }

assert(forall(size_t k;k>=0 && k<cnt; bitmap_test(b,start+k)!=value));

return false;

}

 

====================

 

Coordinator
Apr 15, 2011 at 6:23 PM

Hi,

  could you add the missing function and type definitions for inspection?

  Best, Mark

Apr 15, 2011 at 6:57 PM

typedef unsigned long size_t; //__int32

typedef unsigned long elem_type; //__int32

#define ELEM_BITS (sizeof (elem_type) * CHAR_BIT)    //CHAR_BIT:= 8 ELEM_BITS=4*8=32

struct bitmap
  {
    size_t bit_cnt;     /* Number of bits. */
    elem_type *bits;    /* Elements that represent bits. */
    invariant(keeps(as_array(bits,(bit_cnt+ELEM_BITS-1)/ELEM_BITS)))
    invariant(bit_cnt>0
           && is_malloc_root(this)          // if i want to free bitmap
           && is_malloc_root(as_array(bits, bit_cnt)) // if i want free bits array
            )
  };


/* Returns the index of the element that contains the bit
   numbered BIT_IDX. */
ispure static inline size_t elem_idx (size_t bit_idx)
    returns(bit_idx/ELEM_BITS)
{
    assert(ELEM_BITS>0);
  return bit_idx / ELEM_BITS;
}


/* Returns the index of the element that contains the bit
   numbered BIT_IDX. */
ispure static inline size_t elem_idx (size_t bit_idx)
    returns(bit_idx/ELEM_BITS)
{
    assert(ELEM_BITS>0);
  return bit_idx / ELEM_BITS;
}


/* Returns an elem_type where only the bit corresponding to
   BIT_IDX is turned on. */
ispure static inline elem_type
    bit_mask (size_t bit_idx)
    returns( (elem_type) (1 << (bit_idx % ELEM_BITS)))
{
  return (elem_type) 1 << (bit_idx % ELEM_BITS);
}

 

Coordinator
Apr 16, 2011 at 9:54 AM

Hi,

  this is a "triggering problem", related to VCC's underlying handling of quantifiers. In this case, VCC / the underlying prover Z3 only find a trigger (also called "pattern") for the quantified variable "k" involving arithmetic (start + k), which are not handled too well. The warning below indicates this (it can be seen in the VCC output window in VS):

Prover warning: using arith. in pattern (quantifier id: d2540611.54:17), the weight was increased to 5 (this value can be modified using PI_ARITH_WEIGHT=).
Prover warning: using arith. in pattern (quantifier id: d2540611.54:17), the weight was increased to 5 (this value can be modified using PI_ARITH_WEIGHT=).

  The problem is quite similar to this one: http://vcc.codeplex.com/discussions/251335. It should possible to fix it using manual triggers or restructuring the quantifiers. In this case, the "/oaf" (operators as functions) also helps, which to some extent improves the triggering on arithmetic situation. Pasted below is the example I've worked with.

  HTH, Mark

//`/oaf
#include <vcc.h>

typedef unsigned long size_t; //__int32

typedef unsigned long elem_type; //__int32

#define NULL ((void*)0)

#define CHAR_BIT (8)

#define ELEM_BITS (sizeof (elem_type) * CHAR_BIT)    //CHAR_BIT:= 8 ELEM_BITS=4*8=32

struct bitmap
  {
    size_t bit_cnt;     /* Number of bits. */
    elem_type *bits;    /* Elements that represent bits. */
    invariant(keeps(as_array(bits,(bit_cnt+ELEM_BITS-1)/ELEM_BITS)))
    invariant(bit_cnt>0
           && is_malloc_root(this)          // if i want to free bitmap 
           && 1 /* TODO: not admissible, wrong size: is_malloc_root(as_array(bits, bit_cnt)) */ // if i want free bits array
            ) 
  };


/* Returns the index of the element that contains the bit
   numbered BIT_IDX. */
ispure static inline size_t elem_idx (size_t bit_idx) 
    returns(bit_idx/ELEM_BITS)
{
    assert(ELEM_BITS>0);
  return bit_idx / ELEM_BITS;
}


/* Returns an elem_type where only the bit corresponding to
   BIT_IDX is turned on. */
ispure static inline elem_type 
    bit_mask (size_t bit_idx) 
    returns( (elem_type) (1 << (bit_idx % ELEM_BITS)))
{
  return (elem_type) 1 << (bit_idx % ELEM_BITS);
}

bool bitmap_contains (const struct bitmap *b, size_t start, size_t cnt, bool value)
  requires(b!=NULL)
  requires((start + cnt )<= b->bit_cnt)
  requires(wrapped(b))
  // TODO missing definitions:
  //ensures(!result <==> forall(size_t k;k>=0 && k<cnt;bitmap_test(b,start+k)!=value))
  //ensures(result <==> exists(size_t k;k>=0 && k<cnt;bitmap_test(b,start+k)==value))
{
  size_t i, idx;
  for (i = 0; i < cnt; i++)
    invariant(i>=0 && i<=cnt)
    invariant(forall(size_t k; k>=0 && k<i; ((b->bits[elem_idx (start+k)] & bit_mask (start+k)) != 0) != value))
    invariant(start+i<=b->bit_cnt)
  {
    idx=start+i;          
    if (((b->bits[elem_idx (idx)] & bit_mask (idx)) != 0) == value)
      return true;
  }
  // TODO missing definitions:
  //assert(forall(size_t k;k>=0 && k<cnt; bitmap_test(b,start+k)!=value));
  return false;
}
 
/*`
Verification of bitmap#adm succeeded.
Verification of elem_idx succeeded.
Verification of bit_mask succeeded.
Verification of bitmap_contains succeeded.
`*/

Apr 18, 2011 at 5:58 PM

Thank you mark,

that really helped.