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

Hello,

2014-11-04 0:14 GMT+01:00 Gregory Maxwell <gmaxwell at gmail.com>:
>
> 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>
> 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]
>
> frama-c -main secp256k1_fe_mul_inner -lib-entry -wp -wp-timeout 300
> -wp-par 1 -wp-rte a.c
>

First of all, I'd say that for checking potential overflows in this
context, Value Analysis could do the trick at least as easily as WP.
The command line would be like this:

frama-c -main secp256k1_fe_mul_inner -lib-entry -val overflow.c
-context-width 10 -context-valid-pointers -warn-unsigned-overflow

The extra arguments indicate
- that your pointers a and b are valid (-context-valid-pointers)
- that they point to blocks of size 10 (-context-width 10)
- and that you want to be warned when an unsigned arithmetic operation
may overflow (-warn-unsigned-overflow). Indeed, as unsigned overflows
(contrarily to signed overflows) are well defined by the standard, by
default Value do not report alarms on them.

If you launch this command, you'll see a lot of alarms like this:

overflow.c:28:[kernel] warning: unsigned overflow.
                  assert (unsigned long)*(a+0)*(unsigned long)*(b+9) ?
4294967295;

The culprit here is #include <stdint.h>: by default, this will use
your system's headers, which are unlikely to be consistent with
Frama-C's default machdep x86_32. In other words, the typedef you have
in /usr/include/stdint.h for uint64_t will end up in an integral type
interpreted as 32 bit by Frama-C, hence the alarms. In order to have
headers that match your machdep, you have to instruct the external
preprocessor to use Frama-C's standard headers (and if you don't use
the default machdep, you also have to define the appropriate macro as
seen in FRAMAC_SHARE/libc/__fc_machdep.h). This is done in the
following command line:

frama-c -main secp256k1_fe_mul_inner -lib-entry -val overflow.c
-context-width 10 -context-valid-pointers -warn-unsigned-overflow
-cpp-extra-args="-I$(frama-c -print-share-path)/libc"

I agree that this is error-prone. The next version of Frama-C is
likely to use Frama-C's own standard headers, and pass to the
pre-processor the -D option that corresponds to the selected machdep.
This should be less confusing.

Best regards,
-- 
E tutto per oggi, a la prossima volta
Virgile