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

[Tomas Härdin]

fre 2018-06-22 klockan 19:34 +0000 skrev 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...

I wouldn't demand everyone do this, but I might want it for stuff I
maintain.

/Tomas