--- layout: fc_discuss_archives title: Message 3 from Frama-C-discuss on September 2015 ---
[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[Frama-c-discuss] Simple loop, overflow and bounds



Hi,

Le 02/09/2015 22:10, Kurt Roeckx a écrit :
> Hi,
>
> I'm looking at frama-c to see what I can do with it to, so I ran
> it against some code to see what comes out of it.  The following
> is based on a much larger real file, but I think this already
> shows the kind of questions I have.
>
> I started with the file:
> void foo()
> {
>      unsigned int X[16];
>      int i;
>
>      for (i = 0; i < 16; i++)
>      {
>          X[i] = 0;
>      }
>
>      for (i = 16; i < 64; i += 8)
>      {
>          X[((i+0)+1) & 0x0f]++;
>      }
> }
>
> (This function of course makes little sense.)
>
> I run:
> frama-c-gui -wp -wp-rte -wp-proof alt-ergo <file>
>
> Which will then show me:
> void foo(void)
> {
>    unsigned int X[16];
>    int i;
>    i = 0;
>    while (i < 16) {
>      /*@ assert rte: index_bound: 0 <= i; */
>      /*@ assert rte: index_bound: i < 16; */
>      X[i] = (unsigned int)0;
>      /*@ assert rte: signed_overflow: i+1 <= 2147483647; */
>      i ++;
>    }
>    i = 16;
>    while (i < 64) {
>      /*@ assert rte: index_bound: 0 <= (int)((int)((int)(i+0)+1)&0x0f); */
>      /*@ assert rte: index_bound: (int)((int)((int)(i+0)+1)&0x0f) < 16; */
>      /*@ assert rte: signed_overflow: (int)(i+0)+1 <= 2147483647; */
>      /*@ assert rte: signed_overflow: i+0 <= 2147483647; */
>      /*@ assert
>          rte: unsigned_overflow:
>            X[(int)((int)((int)(i+0)+1)&0x0f)]+1 <= 4294967295;
>      */
>      (X[((i + 0) + 1) & 0x0f]) ++;
>      /*@ assert rte: signed_overflow: i+8 <= 2147483647; */
>      i += 8;
>    }
>    return;
> }
>
> And it show me:
> [wp] 9 goals scheduled
> [wp] [Qed] Goal typed_foo_assert_rte_index_bound_2 : Valid
> [wp] [Alt-Ergo] Goal typed_foo_assert_rte_signed_overflow : Valid (16ms) (5)
> [wp] [Alt-Ergo] Goal typed_foo_assert_rte_index_bound : Unknown (400ms)
> [wp] [Alt-Ergo] Goal typed_foo_assert_rte_signed_overflow_3 : Valid (28ms) (13)
> [wp] [Alt-Ergo] Goal typed_foo_assert_rte_signed_overflow_2 : Valid (32ms) (47)
> [wp] [Alt-Ergo] Goal typed_foo_assert_rte_signed_overflow_4 : Valid (28ms) (21)
> [wp] [Alt-Ergo] Goal typed_foo_assert_rte_index_bound_4 : Unknown (1.4s)
> [wp] [Alt-Ergo] Goal typed_foo_assert_rte_index_bound_3 : Unknown (1.5s)
> [wp] [Alt-Ergo] Goal typed_foo_assert_rte_unsigned_overflow : Unknown (961ms)
> [wp] Proved goals:    5 / 9
>       Qed:             1
>       Alt-Ergo:        4  (16ms-32ms) (47) (unknown: 4)
>
>
> So I have a some questions about this:
> For some reason it can't prove any of the index_bound ones,
> except for the 2nd. (i < 16).  If I look at the code, they all
> seem fairly easy to figure out (for me), since i always has
> a clear limit of the values it's going to have.
>
> Does this require me add things like loop invariants, or something
> else?  If I add the following before my first for loop it makes
> that whole first loop valid:
> /*@ loop invariant 0 <= i <= 16; */
Yes, loop invariants are required by deductive proofs.
> This all seems to be done by Qed in this case, not alt-ergo.
> Why can't alt-ergo figure this out?  Is this some shortcomming in
> the file that is generated for alt-ergo?
Qed is mainly a simplifier. Proof obligation are simplified by Qed 
before the export to external provers.
> Doing the same for the second loop, but then using the following
> doesn't seem to help at all:
> /*@ loop invariant 16 <= i <= 64; */
The loop invariant is not proved by WP, because it seems to weak.
Perhaps, something is missing about the fact that "i" is a 8 multiple 
(unchecked).
> It seems to be unable to prove that, and so the signed overflow checks
> that used to be surely_valid are probably turned into the valid_under_hyp
> because of that.
>
> I'm not sure why it can't prove the 3rd index_bound.  The only
> reason I can think of why it would fail is that it might for some
> reason think i could be negative.  So I turned it into an unsigned
> int, then get to see:
>
> /*@ assert
>          rte: index_bound:
>            (unsigned int)((unsigned int)((unsigned int)(i+(unsigned int)0)+(unsigned int)1)&(unsigned int)0x0f)
>            < 16;
>      */
>
> And it still unknown, while that should be true for all unsigned integers.
Next public version of Frama-C should be able to prove this assertion.
Axiomatics about bitwise operations have been improved since the last 
public release of Frama-C (current non-free version of WP plugin prove 
it - checked).

> Currently a last question is if there is a way to turn off the
> unsigned overflow check it adds?  I have code that code actually
> relies on the overflow behaviour of unsigned integers.

The only way I see (unchecked) could be to add the same assertion into 
your code with a particular tag.
//@ assert TheTag: ... ;
and add WP plugins to prove all properties exception the one having 
TheTag (-wp-prop="-TheTag").
The proof of the one coming from the RTE will rely on it.

Next, loop invariants about X[i] values have to be given.
> Kurt

Patrick.