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

[Tomas Härdin]

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);
}

I got a bit lazy with the axiom. I think newer versions of Frama-C are
better able to reason about shifts. I'm on version Silicon-20161101. To
validate, put in a file called mini.c and run:

  frama-c -wp -wp-rte -wp-prover z3,cvc4,alt-ergo,qed mini.c

You'll need the frama-c package installed, and all the provers listed.

Curiously, replacing the assignment in the contract with assigns
\nothing doesn't work (should eq. assigning the empty set). Maybe a
newer version of Frama-C fixes this.

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.

The point of all this is that it's possible to specify and verify
whether a function has side effects, that it doesn't write out of
bounds, that it terminates etc. This removes the need for unit tests
(if FFmpeg were to have any)


/Tomas