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

[Tomas Härdin]

fre 2018-06-22 klockan 14:07 +0000 skrev Eran Kornblau:
> 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.

If you look closely you'll see that check is after subtracting
atom.header_size.

> 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...

You're assuming inlining actually makes the code faster. It's not the
80's anymore.

> 2. this extra statement - 'pos = atom->data + 8 + 4*i;' - 
> 	why for on 'i' when we only care about 'pos'?

It's an attempt at making that code easier to prove. If I can convince
alt-ergo that atom_data[0..(atom_size-1)] is valid and that the code
only touches bytes in that range then the code will pass inspection.
Using end-pos for that ended up with some rather torturous ACSL
annotations.

> 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?

Yeah that's just my attempt at saying "relax, overflow is fine".
Judging by the ACSL manual [1], adding an explicit cast to uint32_t may
be enough.

> 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.

Yeah, but it only ever calls two functions. So calling them explicitly
makes the job of the prover much easier. If it were possible to add
annotations to the function pointer typedef such that assigning from a
pointer to a function that does not fulfill the contract is illegal,
that would be fine. That doesn't seem possible yet.

Of course, for something like struct AVCodec function pointers are
almost unavoidable.

Perhaps when I get a better hang of this I'll try adding annotations to
libavutil, and mxfdec.c. In the end I want less mental burden.

/Tomas

[1] http://frama-c.com/download/acsl_1.13.pdf