
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 postcondition to "ensures(get_bit(OSTaskRdyBitmap[prio / 8], prio % 8) == 2)", it still reports succeeded... Do I introduce some contradictions in the precondition?


Coordinator
Apr 13, 2011 at 8: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 threadlocality here is using "requires(is_thread_local_array(x,n))" or "requires(thread_local(gemb(x + 0)))", both for "OSMap" and "OSTaskRdyBitmap".
HTH, Mark



Now I change it to is_thread_local_array and remove the array initilization. But VCC still reports succeed for any postcondition....
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 preconditions?


Coordinator
Apr 14, 2011 at 7: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



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 bitmap 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 8bits. 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.


Coordinator
Apr 14, 2011 at 11:17 AM

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.
`*/

