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] WP failing to prove a simple absence of RTE unsigned overflow

Probably the same problem as 
http://lists.gforge.inria.fr/pipermail/why-discuss/2014-October/000697.html

You should run fram-c with extra option: -cpp-extra-args="-I$(frama-c 
-print-share-path)/libc"

- Claude

Le 04/11/2014 00:14, Gregory Maxwell a ?crit :
> Greetings, I haven't used frama-c in some time, it's changed quite a
> bit (and I've likely forgotten even more...) and I'm having a hard
> time making progress with it at all this time around.
>
> I'm working on libsecp256k1 a free software cryptographic signature
> library which will be used by the reference Bitcoin software;
> verifying that optimized implementations are exactly correct is
> critical for this application
>
> I'm trying to prove some simple theorems about some inner kernels used
> for field arithmetic.
>
> To start with, I need to first prove that the code is overflow free,
> under assumptions. (I don't just need to do this to make WP happy, its
> required for correctness of the code.
>
> Here is a reduced testcase that I'm trying:
>
> $ cat a.c
> #include <stdint.h>
> /*@ requires \valid(a + (0..9));
>      requires \valid(b + (0..9));
>      requires (a[0] < 1073741824);
>      requires (a[1] < 1073741824);
>      requires (a[2] < 1073741824);
>      requires (a[3] < 1073741824);
>      requires (a[4] < 1073741824);
>      requires (a[5] < 1073741824);
>      requires (a[6] < 1073741824);
>      requires (a[7] < 1073741824);
>      requires (a[8] < 1073741824);
>      requires (a[9] < 67108864);
>      requires (b[0] < 1073741824);
>      requires (b[1] < 1073741824);
>      requires (b[2] < 1073741824);
>      requires (b[3] < 1073741824);
>      requires (b[4] < 1073741824);
>      requires (b[5] < 1073741824);
>      requires (b[6] < 1073741824);
>      requires (b[7] < 1073741824);
>      requires (b[8] < 1073741824);
>      requires (b[9] < 67108864);
> */
> void static inline secp256k1_fe_mul_inner(const uint32_t *a, const
> uint32_t *b, uint32_t *r) {
>      uint64_t d;
>      d  = (uint64_t)a[0] * b[9]
>         + (uint64_t)a[1] * b[8]
>         + (uint64_t)a[2] * b[7]
>         + (uint64_t)a[3] * b[6]
>         + (uint64_t)a[4] * b[5]
>         + (uint64_t)a[5] * b[4]
>         + (uint64_t)a[6] * b[3]
>         + (uint64_t)a[7] * b[2]
>         + (uint64_t)a[8] * b[1]
>         + (uint64_t)a[9] * b[0];
> }
>
> I invoke frama-c with:
>
> frama-c -main secp256k1_fe_mul_inner -lib-entry -wp -wp-timeout 300
> -wp-par 1 -wp-rte a.c
>
> And get some successful proof for memory access, followed by alt-ergo
> returning unknown on the overflow checks:
> [...]
> [wp] [Alt-Ergo] Goal
> typed_secp256k1_fe_mul_inner_assert_rte_mem_access_20 : Valid
> (Qed:1ms) (93ms) (74)
> [wp] [Alt-Ergo] Goal
> typed_secp256k1_fe_mul_inner_assert_rte_unsigned_overflow : Unknown
> (Qed:4ms) (4s)
> [wp] [Alt-Ergo] Goal
> typed_secp256k1_fe_mul_inner_assert_rte_unsigned_overflow_2 : Unknown
> (Qed:5ms) (4s)
>
> This is obviously free of overflows, since  1073741824*1073741824*8 +
> 1073741824*67108864*2 < 2^64
>
> (but the non-reduced code, is less trivial
> http://0bin.net/paste/tTR7910ESfwij7Ib#pZwnZkivigEp+73f4D4yWQpXMaEWCmVFTb4XxE6vRUN
> ... which is why I'm starting with just proving overflows since the
> hand verifiable correctness proof in the comments assumes no
> overflow).
>
> I'm using alt-ergo 0.95.1 and frama-c Neon-20140301
>
> Any suggestions?
> _______________________________________________
> Frama-c-discuss mailing list
> Frama-c-discuss at lists.gforge.inria.fr
> http://lists.gforge.inria.fr/cgi-bin/mailman/listinfo/frama-c-discuss
>

-- 
Claude March?                          | tel: +33 1 72 92 59 69
INRIA Saclay - ?le-de-France           |
Universit? Paris-sud, Bat. 650         | http://www.lri.fr/~marche/
F-91405 ORSAY Cedex                    |