Frama-C-discuss mailing list archives

This page gathers the archives of the old Frama-C-discuss archives, that was hosted by Inria's gforge before its demise at the end of 2020. To search for mails newer than September 2020, please visit the page of the new mailing list on Renater.

[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.