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

Hi !

Instead of writing the ?assembly? by hand, you should have a look to the machine-integer model of WP.
Using option ?-wp-model +cint? (+nat is the default, Cf. WP manual), all machine integer operations are converted into a Z-operation followed by an appropriate modulo operator.
For instance, provided 'int a,b ;' expression (a+b) would be interpreted as 'to_sint32 (a+b)?.

By the way, I must notice that WP + RTE is not the best way to check for absence of runtime errors. You should use Value for this purpose.
L.


Le 26 nov. 2014 ? 01:43, Mansour Moufid <mansourmoufid at gmail.com> a ?crit :

> On Mon, 3 Nov 2014 23:14:32 +0000
> Gregory Maxwell <gmaxwell at gmail.com> wrote:
> 
>> 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 have attempted to do something similar with the reference Curve25519
> implementation.
> 
> The strategy I found works well with the WP plugin is to break down
> complex arithmetic expressions into basic functions, kind of like you
> would write assembly.
> 
> So your example code would look like this:
> 
>    #include <stdint.h>
>    /*@ 
>        ensures \result == a * b;
>     */
>    static inline uint64_t
>    _uint32_mul(const uint32_t a, const uint32_t b)
>    {
>        return (uint64_t) a * (uint64_t) b;
>    }
>    /*@ 
>        requires a <= UINT64_MAX / 2;
>        requires b <= UINT64_MAX / 2;
>        ensures \result == a + b;
>     */
>    static inline uint64_t
>    _uint64_sum(const uint64_t a, const uint64_t b)
>    {
>        return a + b;
>    }
>    /*@ 
>        requires a <= UINT64_MAX / 10;
>        requires b <= UINT64_MAX / 10;
>        requires c <= UINT64_MAX / 10;
>        requires d <= UINT64_MAX / 10;
>        requires e <= UINT64_MAX / 10;
>        requires f <= UINT64_MAX / 10;
>        requires g <= UINT64_MAX / 10;
>        requires h <= UINT64_MAX / 10;
>        requires i <= UINT64_MAX / 10;
>        requires j <= UINT64_MAX / 10;
>        ensures \result == a + b + c + d + e + f + g + h + i + j;
>     */
>    static inline uint64_t
>    _uint64_sum_10(const uint64_t a, const uint64_t b,
>        const uint64_t c, const uint64_t d,
>        const uint64_t e, const uint64_t f,
>        const uint64_t g, const uint64_t h,
>        const uint64_t i, const uint64_t j)
>    {
>        return (_uint64_sum(a,
>                _uint64_sum(b,
>                _uint64_sum(c,
>                _uint64_sum(d,
>                _uint64_sum(e,
>                _uint64_sum(f,
>                _uint64_sum(g,
>                _uint64_sum(h,
>                _uint64_sum(i,j))))))))));
>    }
>    /*@ 
>        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);
>    */
>    static inline void
>    secp256k1_fe_mul_inner(const uint32_t a[10], const uint32_t b[10])
>    {
>        uint64_t d;
>        d = _uint64_sum_10(
>                _uint32_mul(a[0], b[9]),
>                _uint32_mul(a[1], b[8]),
>                _uint32_mul(a[2], b[7]),
>                _uint32_mul(a[3], b[6]),
>                _uint32_mul(a[4], b[5]),
>                _uint32_mul(a[5], b[4]),
>                _uint32_mul(a[6], b[3]),
>                _uint32_mul(a[7], b[2]),
>                _uint32_mul(a[8], b[1]),
>                _uint32_mul(a[9], b[0])
>            );
>    }
> 
> Check it with the WP and RTE plugins:
> 
>    $ frama-c -machdep $(uname -m) -pp-annot -wp -wp-rte \
>        -wp-prop @ensures,unsigned_overflow a.c 
>    ...
>    [wp] Proved goals:    7 / 7
>         Qed:             3  (4ms-32ms)
>         Alt-Ergo:        4  (76ms-80ms) (13)
> 
> It works, but it's very verbose.  You may find that the value analysis
> plugin is less tedious, I don't know.
> 
> Best of luck.
> 
> Mansour
> _______________________________________________
> 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

-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.gforge.inria.fr/pipermail/frama-c-discuss/attachments/20141126/35b297b6/attachment-0001.html>