> -----Original Message-----
> From: ffmpeg-devel [mailto:ffmpeg-devel-boun...@ffmpeg.org] On Behalf Of 
> Tomas Härdin
> Sent: Friday, June 22, 2018 5:51 PM
> To: FFmpeg development discussions and patches <ffmpeg-devel@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@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
_______________________________________________
ffmpeg-devel mailing list
ffmpeg-devel@ffmpeg.org
http://ffmpeg.org/mailman/listinfo/ffmpeg-devel

Reply via email to