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

Eran Kornblau eran.kornblau at kaltura.com
Fri Jun 22 17:07:52 EEST 2018

> 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://emea01.safelinks.protection.outlook.com/?url=https%3A%2F%2Fframa-c.com%2F&data=02%7C01%7Ceran.kornblau%40kaltura.com%7C41e71cf613e041e2d75908d5d845e373%7C0c503748de3f4e2597e26819d53a42b6%7C0%7C0%7C636652717037149779&sdata=cnGg2SD1mSGhn3qhGR2YRVexfA17%2F6Lrx52mnxPN1nA%3D&reserved=0).
> 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:
First, regarding the if you added, it's redundant - if you look a few lines above, you'll see 'if (atom.size < atom.header_size)'.
atom.header_size is either 8 or 16, it can't be anything else, so atom.size can't be < 8 at this point.

I'll leave it to the maintainers to decide whether this tool is helpful or not, IMHO, all these comments make the 
code less readable, and some of the changes make it less efficient. I don't think this slight reduction of performance 
matters much in the context of faststart, but in other parts of ffmpeg it can be significant.

Few examples to why I think it's less efficient -
1. the change of macros to functions - maybe the compiler will inline them, but maybe it won't...
2. this extra statement - 'pos = atom->data + 8 + 4*i;' - 
	why for on 'i' when we only care about 'pos'?
3. this code - 'current_offset = ((uint64_t)current_offset + (context->moov_atom_size & 0xFFFFFFFF)) & 0xFFFFFFFF;'
	why go through 64 bit when we later cast it to 32 bit?

Other than that, your patch implies that function pointers should not be used, I think that in many cases,
they can be helpful. In this specific case, the function 'parse_atoms' was a generic function for parsing atoms,
after the change, it can't be reused for any other task.


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

More information about the ffmpeg-devel mailing list