[FFmpeg-devel] frama-c:ify qt-faststart.c, proof-of-concept (kinda)

[Tomas Härdin]

Hi

I've recently been looking at formal proof systems for minimizing bugs.
One common example is SPARK, which is an Ada variant which uses
contracts, guaranteed termination and lack of dynamic allocation to
make reasoning about SPARK programs much easier. This allows automatic
checking for things like overflows, out-of-bounds access and so on. A
great thing for code quality.

There is something similar for C called Frama-C (https://frama-c.com/).
It allows you to add contracts to functions and then attempts to prove
that the functions fulfill said contracts. Like SPARK it is also
possible to check for things like out-of-bounds accesses or
over/underflow. So I spent a few days going over qt-faststart.c (then
yet again after the recent patch), adding ACSL annotations here and
there, and rewriting parts of it to make the job of alt-ergo/why3/coq
much easier. It's far from done, roughly 29% of goals are yet to be
proven. But the purpose is to raise discussion rather than provide a
perfect solution.

I'd also like to know if anyone else on here has fiddled with frama-c,
and might know how one could make this part of the test system. For
example, I'd like a plot of % proved goals over time and the ability to
fail a build if a file that was 100% proved suddenly no longer is.

Doing this for a large project like FFmpeg is a serious undertaking,
but something I feel should really be done for all C projects. In my
case this is motivated by the recent cargo cult discussion about checks
in mxfdec.c, which an automated prover could take care of. There are of
course many more cases.

Patch attached. One thing I discovered is that all atom parsers expect
at least 8 bytes of atom data, so I was able to add contracts and
checks for that. Here's what "frama-c -wp -wp-rte qt-faststart.c" says
about it right now:

    [wp] Proved goals:  240 / 340
         Qed:           156  (4ms-16ms-1.2s)
         Alt-Ergo:       84  (28ms-133ms-776ms) (403) (interrupted: 22) (unknown: 78)

/Tomas
-------------- next part --------------
A non-text attachment was scrubbed...
Name: 0001-frama-c-ify-qt-faststart.c.patch
Type: text/x-patch
Size: 16192 bytes
Desc: not available
URL: <http://ffmpeg.org/pipermail/ffmpeg-devel/attachments/20180622/6be5ec3d/attachment.bin>