--- layout: fc_discuss_archives title: Message 72 from Frama-C-discuss on August 2013 ---
[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[Frama-c-discuss] Proving a simple property on bitshift with WP



Hello Virgile,

2013/8/29 Virgile Prevosto <virgile.prevosto at m4x.org>:
> I'm afraid that WP tries to play it a bit too smart here: if you look
> at the generated goal, you'll see that the values of the m[i] have
> been const-folded, so that you have m[0] == 128, m[1] == 64, etc. It
> makes the assert on m[0] trivial, but
> the assert on m[bit] much more complicated, as the prover somehow has
> to revert back the transformation. Since we're dealing with a bitwise
> rather than an arithmetic operation, I'm not sure that there's an easy
> way to have alt-ergo prove that.

Argh!! Thank you for the explanation!

I found an overkill way to prove the property by building it manually
and putting it as requirement of the function of interest (see below).
I also need to call WP with -wp-model "Typed,int".

Even if now everything is proved, this is ugly and much less readable
than the original program. :-(

I also thought of combining Value analysis and WP to do the same kind
of thing as below program, but using Value to prove the property on
the static version of m[]. Unfortunately, Value seems unable to reason
on \forall quantifier and I see no other way to express the property.

A third approach would be to attach a global invariant to the static m
(and still require the property at f() entrance):
 global invariant my_m:
       \forall integer i; 0 <= i  < 8 ==> m[i] == (1 << (7-i));
Unfortunately, WP does not seem to support it (and probably would have
the same issue to prove it).

====

unsigned char m[8];

/*@ requires n >= 0;
    requires \forall integer i; 0 <= i  < 8 ==> m[i] == (1 << (7-i));
 */
int f(int n)
{
  int size, bit;

  size = 8;
  bit = n%size;
  //@ assert 0 <= bit <= 7;

  //@ assert m[0] == ((unsigned char)(1 << 7));
  //@ assert m[bit] == ((unsigned char)1 << (7-(n%8)));

  return 0;
}

int main(int n)
{
  int i;

  if (n < 0) return -1;

  /*@ loop invariant 0 <= i <= 8;
      loop invariant \forall integer j; 0 <= j < i ==> m[j] == (1 << (7-j));
      loop invariant n >= 0;
   */
  for (i=0; i<8; i++) {
    m[i] = (1 << (7-i));
  }
  //@ assert \forall integer i; 0 <= i  < 8 ==> m[i] == (1 << (7-i));

  f(n);
  return 0;
}
====

Best regards,
david