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

[Eran Kornblau]

> -----Original Message-----
> From: ffmpeg-devel [mailto:ffmpeg-devel-bounces at ffmpeg.org] On Behalf Of Tomas Härdin
> Sent: Friday, June 22, 2018 5:51 PM
> To: FFmpeg development discussions and patches <ffmpeg-devel at ffmpeg.org>
> Subject: Re: [FFmpeg-devel] frama-c:ify qt-faststart.c, proof-of-concept (kinda)
> 
> > 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.
> 
You're right, I missed that, but now that I see it - it's not redundant, it's just wrong.
It's perfectly ok for an arbitrary atom to have size smaller than 8 bytes (frma is, for example, 
only 4 bytes), it's not ok for the two specific atoms that we're parsing - stco & co64. 
The validation of size >= 8 already existed in all branches that required it 
(parse_atoms / update_stco_offsets / update_co64_offsets)

> > 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.
> 
Sounds a bit problematic to me to demand that everyone here learn all this stuff now, 
but again, it's not my call...

> > 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] https://emea01.safelinks.protection.outlook.com/?url=http%3A%2F%2Fframa-c.com%2Fdownload%2Facsl_1.13.pdf&data=02%7C01%7Ceran.kornblau%40kaltura.com%7Ce74b7daf0c4846621a6e08d5d84fa248%7C0c503748de3f4e2597e26819d53a42b6%7C0%7C1%7C636652758896295662&sdata=CjOaX1Uvl%2FsvYLmL6Pdvm2yg8RFNZ%2BcJUTJ11hyu4c8%3D&reserved=0
> _______________________________________________
> ffmpeg-devel mailing list
> ffmpeg-devel at ffmpeg.org
> https://emea01.safelinks.protection.outlook.com/?url=http%3A%2F%2Fffmpeg.org%2Fmailman%2Flistinfo%2Fffmpeg-devel&data=02%7C01%7Ceran.kornblau%40kaltura.com%7Ce74b7daf0c4846621a6e08d5d84fa248%7C0c503748de3f4e2597e26819d53a42b6%7C0%7C1%7C636652758896295662&sdata=HhRDsQBrzYopJhMPb7xuVtlo99ka9btAbcnE8091Yu8%3D&reserved=0
> 

Eran