--- layout: fc_discuss_archives title: Message 46 from Frama-C-discuss on November 2014 ---
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>