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