> 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.
Eran
> [wp] Proved goals: 240 / 340
> Qed: 156 (4ms-16ms-1.2s)
> Alt-Ergo: 84 (28ms-133ms-776ms) (403) (interrupted: 22)
> (unknown: 78)
>
> /Tomas
>
_______________________________________________
ffmpeg-devel mailing list
ffmpeg-devel@ffmpeg.org
http://ffmpeg.org/mailman/listinfo/ffmpeg-devel
