[FFmpeg-devel] [PATCH] avutil: add av_memcpy() to avoid undefined behavior with NULL, NULL, 0

[Michael Niedermayer]

On Sat, Jul 06, 2019 at 02:34:34PM +0200, Tomas Härdin wrote:
> lör 2019-07-06 klockan 00:08 +0200 skrev Michael Niedermayer:
> > As we are already off topic, heres an example to test static
> > analysis, does this trigger undefined behavior by executing the memcpy
> > for some user input ?
> > 
> > void f(unsigned bigint a) {
> >     bigint i;
> >     for (i = 2; (((bigint)1 << a) + 1) % i; i++)
> >         ;
> >     if (a > 20 && i > ((bigint)1 << a))
> >         memcpy(NULL, NULL, 0);
> > }
> > 
> > i know its a lame example but just to remind that static analysis has
> > limitations. (your mail sounds a bit like static analysis could replace
> > everything ...)
> 
> That is acually perfectly legal since the intersection between
> [NULL,NULL) and [NULL,NULL) is empty and thus they do not overlap.
> Here's an example that validates:
> 
> #include <stdint.h>
> #include <string.h>
> 
> /*@ axiomatic Foo {
>     axiom Bar: \forall integer a;
>       0 <= a <= 62 ==>
>         1 <= (1<<a) <= (1<<62);
>     }
>  */
> 
> /*@ requires 0 <= a <= 62;
>     assigns ((char*)NULL)[0..-1];
>  */
> void f(uint64_t a) {
>     int64_t i = 2;
>     int64_t a2 = (1LL << a) + 1;
>     /*@ loop invariant 2 <= i <= a2;
>         loop assigns i;
>      */
>     for (; a2 % i; i++)
>         ;
>     //@ assert a2 % i == 0;
>     if (a > 20 && i > ((int64_t)1 << a))
>         memcpy(NULL, NULL, 0);
> }

this code is wrong.
Imagine this was real code, and to make it fit in the static
analyzer one changes it like this

why is it worng ?
the range should not have a upper bound of 62 in fact there is no
reason to run this function with input below 1LL<<33 that is not
33 that is 1LL<<33

also you can restrict a to powers of 2 if you like
thats
for (b = 33; ; b++)
    f((bigint)1<<b);
    
can the analyzer help check this ?
I am pretty sure its not UB below, and i suspect its not UB for most values 
above but iam really curious and like to know for sure.


[...]

> If you change the memcpy() to copy n=1 bytes then the verification
> fails, as expected. It also fails if let src and dst equal to the same
> valid memory area, because of overlap.

are you saying that code which never executes causes failure of the
analyzer because if it did execute it would be wrong ?

[...]

Thanks

-- 
Michael     GnuPG fingerprint: 9FF2128B147EF6730BADF133611EC787040B0FAB

Never trust a computer, one day, it may think you are the virus. -- Compn
-------------- next part --------------
A non-text attachment was scrubbed...
Name: signature.asc
Type: application/pgp-signature
Size: 181 bytes
Desc: not available
URL: <http://ffmpeg.org/pipermail/ffmpeg-devel/attachments/20190706/d988e371/attachment.sig>