This project is read-only.

bit operation and array initialization

Apr 12, 2011 at 2:57 AM

typedef unsigned char U8;

U8 OSMap[8] = {0x01,0x02,0x04,0x08,0x10,0x20,0x40,0x80};
U8 OSTaskRdyBitmap[8] = {0};
U8 OSTaskRdyIndex = 0;
#define get_bit(x, i) (x << (7 - i)) >> 7

void SetBitMap(U32 prio) requires(prio < 64) requires(thread_local(as_array(OSMap, 8))) ensures(get_bit(OSTaskRdyIndex, prio / 8) == 1) ensures(get_bit(OSTaskRdyBitmap[prio / 8], prio % 8) == 1) writes(&OSTaskRdyIndex) writes(as_array(OSTaskRdyBitmap, 8)) { unsigned int x,y; y = prio>>3; OSTaskRdyIndex |= OSMap[y]; x = prio - (y * (1<<3)); OSTaskRdyBitmap[y] |= OSMap[x]; return; }

VCC reports that "unhandled initializer" at first.

Then I remove the initializer and add a new require: "forall (unsigned int i; i < 8 ==> OSMap[i] == 1 << i)"

typedef unsigned char U8;

U8 OSMap[8];
U8 OSTaskRdyBitmap[8];
U8 OSTaskRdyIndex = 0;
#define get_bit(x, i) (x << (7 - i)) >> 7

void SetBitMap(U32 prio)
requires(prio < 64)
requires(thread_local(as_array(OSMap, 8)))
requires (forall (unsigned int i; i < 8 ==> OSMap[i] == 1 << i))
ensures(get_bit(OSTaskRdyIndex, prio / 8) == 1)
ensures(get_bit(OSTaskRdyBitmap[prio / 8], prio % 8) == 1)
writes(&OSTaskRdyIndex)
writes(as_array(OSTaskRdyBitmap, 8))
{
unsigned int x,y;

y = prio>>3;
OSTaskRdyIndex |= OSMap[y];
x = prio - (y * (1<<3));
OSTaskRdyBitmap[y] |= OSMap[x];
return;
}

VCC reports succeeded.
But it's not useful. Because even when I change the post-condition to "ensures(get_bit(OSTaskRdyBitmap[prio / 8], prio % 8) == 2)", it still reports succeeded...
Do I introduce some contradictions in the pre-condition?
Apr 13, 2011 at 9:42 PM

Hi,

  indeed, there's a contradiction, not related to the initializer: "as_array(x,n)" can't be used for global arrays "x[n]" of primitive element type, which are internally embedded in a different type, leading to the contradiction. This is mentioned in passing on http://vcc.codeplex.com/wikipage?title=Globals&referringTitle=Documentation; the documentation / internal representation situation is however not ideal.

  The right way to require thread-locality here is using "requires(is_thread_local_array(x,n))" or "requires(thread_local(gemb(x + 0)))", both for "OSMap" and "OSTaskRdyBitmap".

  HTH, Mark

Apr 14, 2011 at 8:41 AM

Now I change it to is_thread_local_array and remove the array initilization. But VCC still reports succeed for any post-condition....

 

typedef unsigned char U8;

U8 OSMap[8];
U8 OSTaskRdyBitmap[8];
U8 OSTaskRdyIndex = 0;
#define get_bit(x, i) (x << (7 - i)) >> 7

void SetBitMap(U32 prio)
	requires(prio < 64)
        requires(is_thread_local_array(OSMap, 8))
        requires(is_thread_local_array(OSTaskRdyBitmap, 8))
        requires (forall (unsigned int i; i < 8 ==> OSMap[i] == 1 << i))
	ensures(get_bit(OSTaskRdyIndex, prio / 8) == 1)
	ensures(get_bit(OSTaskRdyBitmap[prio / 8], prio % 8) == 1)
        writes(&OSTaskRdyIndex)
	writes(as_array(OSTaskRdyBitmap, 8))
{
	unsigned int x,y;

	y = prio>>3;
	OSTaskRdyIndex |= OSMap[y];
	x = prio - (y * (1<<3));
	OSTaskRdyBitmap[y] |= OSMap[x];
	return;
}
Are there still some contradictions in the pre-conditions?

Apr 14, 2011 at 8:58 AM

Yes, sorry, the writes clauses has to be changed as well:

#include <vcc.h>

typedef unsigned char U8;
typedef unsigned __int32 U32;

U8 OSMap[8];
U8 OSTaskRdyBitmap[8];
U8 OSTaskRdyIndex = 0;
#define get_bit(x, i) (x << (7 - i)) >> 7

void SetBitMap(U32 prio)
	requires(prio < 64)
        requires(is_thread_local_array(OSMap, 8))
        requires(is_thread_local_array(OSTaskRdyBitmap, 8))
        requires (forall (unsigned int i; i < 8 ==> OSMap[i] == 1 << i))
	ensures(get_bit(OSTaskRdyIndex, prio / 8) == 1)
	ensures(get_bit(OSTaskRdyBitmap[prio / 8], prio % 8) == 1)
        writes(&OSTaskRdyIndex)
	writes(array_range(OSTaskRdyBitmap,8))
{
	unsigned int x,y;

	y = prio>>3;
	OSTaskRdyIndex |= OSMap[y];
	x = prio - (y * (1<<3));
	OSTaskRdyBitmap[y] |= OSMap[x];
	return;
}

Now you get a failing postcondition, which I didn't investigate (I guess you need some bitvector lemmas).

Best, Mark 

Apr 14, 2011 at 9:20 AM

now I change it to "writes (array_range(OSTaskRdyBitmap, 8))". And VCC reports that "Error    1    Post condition '(OSTaskRdyIndex << (7 - prio / 8)) >> 7 == 1' did not verify. "

May I add some bv_lemma?

This is a bit-map to specify scheduling. The array OSMap is used as mask. The array OSTaskRdyBitmap contains 8 element and each element is a char, of which length is 8-bits. Every bit denotes a task.

The function SetBitMap sets the "prio" by setting the j th bit in OSTaskRdyBitmap[i] to 1, where i is prio/8 and j is prio%8.

Apr 14, 2011 at 12:17 PM

Right, you need BV lemmas. Here's an example for a simpler function:

#include <vcc.h>

#define BITMASK(i) (1 << (i))
#define BIT(a,i) ((a) & BITMASK(i))

unsigned set_bit(unsigned a, unsigned i)
  requires(i < 32)
  ensures(BIT(result, i))
  ensures(forall(unsigned j; j != i; BIT(result, j) == BIT(a, j)))
{
  bv_lemma(forall(unsigned a, i, j; i != j; BIT(a, j) == BIT(a | BITMASK(i), j)));
  return a | BITMASK(i);
}

/*`
Verification of set_bit succeeded.
Verification of set_bit#bv_lemma#0 succeeded.
`*/