Re: [FFmpeg-devel] frama-c:ify qt-faststart.c, proof-of-concept (kinda)
fre 2018-06-22 klockan 23:12 +0200 skrev Michael Niedermayer:
> On Fri, Jun 22, 2018 at 04:51:09PM +0200, Tomas Härdin wrote:
> > fre 2018-06-22 klockan 14:07 + 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.
>
> Until someone tests it, both claims are assumtations.
> The date on the calender surely is not a good argument though even though it
> has a somewhat "authorative" vibe to it.
>
> Personally i prefer inline/always inline functions over macros when they are
> equally fast though ...
>
> Speaking about the date. I would have thought the need to manually annotate
> the
> code for analyzers was a thing more for the past and for academia. But quite
> possibly i have missed something ...
It's common in industries where you need to guarantee that a piece of
code will never crash. Aerospace comes to mind.
> If you compare the time it takes a human to anotate a piece of code (some of
> this anotation itself may be incorrect) and subsequently a analyzer to find
> bugs.
> To the alternative
> of a human manually reviewing the code line by line and a analyzer running
> over
> the code which does not need anotations
>
> which finds more bugs ?
> The question matters, because i think we want the maximum return for the time
> that
> is invested
The point is to let the machine automatically catch when certain
assumptions are violated, since mistakes happen. You are correct that
it can take considerable time though. I wouldn't insist on anyone else
doing it, this is mostly for my own sanity. And of course if the
contracts are wrong then you're screwed. Just like if ones assumptions
of what a function does are wrong.
As an example of just how wordy these annotations can get, I've
attached binary_search_tree_proved.c from [1]. It's 8 lines of code and
over 100 lines of annotations. But it does prove correct.
To cap off this post, I'll link to what I've said on the 'ol blogaroo
about Ada/SPARK: http://härdin.se/blog/2018/01/20/trying-out-ada-spark/
/Tomas
[1] https://bts.frama-c.com/dokuwiki/lib/exe/fetch.php?media=mantis:fra
ma-c:tutorial:lifo-2014:solutions.tar.gz
struct tree { int data;
struct tree* left;
struct tree* right; };
/*@ inductive reachable{L}(struct tree* t1, struct tree* t2) {
case single: \forall struct tree* t; reachable(t,t);
case transl: \forall struct tree* t1,*t2; reachable(t1->left,t2) ==>
reachable(t1,t2);
case transr: \forall struct tree* t1, *t2;
reachable(t1->right,t2) ==> reachable(t1,t2);
}
*/
/*@ lemma reachable_trans_l:
\forall struct tree *t1, *t2;
reachable(t1,t2) && \valid(t2) ==> reachable(t1, t2->left);
*/
/*@ lemma reachable_trans_r:
\forall struct tree *t1, *t2;
reachable(t1,t2) && \valid(t2) ==> reachable(t1, t2->right);
*/
/*@ predicate well_formed{L}(struct tree* t) =
\forall struct tree* t1; reachable(t,t1) ==>
\valid(t1) || t1 == (struct tree*)0;
*/
/*@ predicate contains{L}(struct tree* t, int data) =
\valid(t) &&
\exists struct tree* t1; \valid(t1) && reachable(t,t1) && t1->data == data;
*/
/*@ inductive sorted_tree{L}(struct tree* t) {
case empty{L}: sorted_tree((struct tree*)0);
case full{L}: \forall struct tree* t; well_formed(t) &&
\valid(t) && sorted_tree(t->left) && sorted_tree(t->right) &&
(\forall struct tree* t1; reachable(t->left, t1) ==> t->data >= t1->data) &&
(\forall struct tree* t1; reachable(t->right, t1) ==> t->data <= t1->data) ==>
sorted_tree(t);
}
*/
/*@ lemma sorted_tree_projl:
\forall struct tree* t, *t1;
sorted_tree(t) && \valid(t) && \valid(t1) && reachable(t->left,t1) ==>
t1->data <= t->data;
*/
/*@ lemma sorted_tree_projr:
\forall struct tree* t, *t1;
sorted_tree(t) && \valid(t) && \valid(t1) && reachable(t->right,t1) ==>
t1->data >= t->data;
*/
/*@ lemma sorted_children:
\forall struct tree* t;
\valid(t) && sorted_tree(t) ==> sorted_tree(t->left) && sorted_tree(t->right);
*/
/* @ lemma reachable_choice{L}:
\forall struct tree* t, *t1;
\valid(t) && \valid(t1) && well_formed(t)
Re: [FFmpeg-devel] frama-c:ify qt-faststart.c, proof-of-concept (kinda)
fre 2018-06-22 klockan 19:34 + skrev Eran Kornblau: > > -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 > .org> > > Subject: Re: [FFmpeg-devel] frama-c:ify qt-faststart.c, proof-of- > > concept (kinda) > > > > > fre 2018-06-22 klockan 14:07 + 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 & 0x)) & 0x;' > > > 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 ___ ffmpeg-devel mailing list ffmpeg-devel@ffmpeg.org http://ffmpeg.org/mailman/listinfo/ffmpeg-devel
Re: [FFmpeg-devel] [FFmpeg-cvslog] lavf/amr: Make the heuristic for auto-detection even stricter.
On Thu, Jun 21, 2018 at 10:09:14PM +, Carl Eugen Hoyos wrote: > ffmpeg | branch: master | Carl Eugen Hoyos | Fri Jun 22 > 00:08:13 2018 +0200| [40b7e6071815fc416a4efc5dc1616f5460a3aacb] | committer: > Carl Eugen Hoyos > > lavf/amr: Make the heuristic for auto-detection even stricter. > > Fixes ticket #7270. > > > http://git.videolan.org/gitweb.cgi/ffmpeg.git/?a=commit;h=40b7e6071815fc416a4efc5dc1616f5460a3aacb > --- > > libavformat/amr.c | 6 +++--- > 1 file changed, 3 insertions(+), 3 deletions(-) > > diff --git a/libavformat/amr.c b/libavformat/amr.c > index f954803d46..6cc06bceac 100644 > --- a/libavformat/amr.c > +++ b/libavformat/amr.c > @@ -201,7 +201,7 @@ static int amrnb_probe(AVProbeData *p) > i++; > } > } > -if (valid > 100 && valid > invalid) > +if (valid > 100 && valid >> 4 > invalid) > return AVPROBE_SCORE_EXTENSION / 2 + 1; > return 0; > } > @@ -258,8 +258,8 @@ static int amrwb_probe(AVProbeData *p) > i++; > } > } > -if (valid > 100 && valid > invalid) > -return AVPROBE_SCORE_EXTENSION / 2 - 1; > +if (valid > 100 && valid >> 4 > invalid) > +return AVPROBE_SCORE_EXTENSION / 2 + 1; This breaks detecting the h263 file: https://samples.ffmpeg.org/V-codecs/h263/h263-raw/messenger.h263 [...] -- Michael GnuPG fingerprint: 9FF2128B147EF6730BADF133611EC787040B0FAB It is what and why we do it that matters, not just one of them. signature.asc Description: PGP signature ___ ffmpeg-devel mailing list ffmpeg-devel@ffmpeg.org http://ffmpeg.org/mailman/listinfo/ffmpeg-devel
Re: [FFmpeg-devel] frama-c:ify qt-faststart.c, proof-of-concept (kinda)
On Sat, Jun 23, 2018 at 11:40:52AM +0200, Tomas Härdin wrote: > fre 2018-06-22 klockan 23:12 +0200 skrev Michael Niedermayer: > > On Fri, Jun 22, 2018 at 04:51:09PM +0200, Tomas Härdin wrote: > > > fre 2018-06-22 klockan 14:07 + 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. > > > > Until someone tests it, both claims are assumtations. > > The date on the calender surely is not a good argument though even though it > > has a somewhat "authorative" vibe to it. > > > > Personally i prefer inline/always inline functions over macros when they are > > equally fast though ... > > > > Speaking about the date. I would have thought the need to manually annotate > > the > > code for analyzers was a thing more for the past and for academia. But quite > > possibly i have missed something ... > > It's common in industries where you need to guarantee that a piece of > code will never crash. Aerospace comes to mind. If you want to make FFmpeg reach Aerospace / Medicine like levels of bug-free-ness, that is welcome. Thanks [...] -- Michael GnuPG fingerprint: 9FF2128B147EF6730BADF133611EC787040B0FAB Asymptotically faster algorithms should always be preferred if you have asymptotical amounts of data signature.asc Description: PGP signature ___ ffmpeg-devel mailing list ffmpeg-devel@ffmpeg.org http://ffmpeg.org/mailman/listinfo/ffmpeg-devel
Re: [FFmpeg-devel] [PATCH][ticket #5522] lavc/cfhd: interlaced frame decoding added
Hi
On Tue, May 22, 2018 at 09:10:21PM +0530, Gagandeep Singh wrote:
> ticket #5522 output of given samples significantly improved
> ---
> libavcodec/cfhd.c | 181
> +++---
> libavcodec/cfhd.h | 9 +++
> 2 files changed, 155 insertions(+), 35 deletions(-)
>
> diff --git a/libavcodec/cfhd.c b/libavcodec/cfhd.c
> index 7ceb803595..051d210355 100644
> --- a/libavcodec/cfhd.c
> +++ b/libavcodec/cfhd.c
> @@ -49,12 +49,15 @@ enum CFHDParam {
> SubbandNumber= 48,
> Quantization = 53,
> ChannelNumber= 62,
> +SampleFlags = 68,
> BitsPerComponent = 101,
> ChannelWidth = 104,
> ChannelHeight= 105,
> PrescaleShift= 109,
> };
>
> +
> +
> static av_cold int cfhd_init(AVCodecContext *avctx)
> {
> CFHDContext *s = avctx->priv_data;
> @@ -72,6 +75,13 @@ static void init_plane_defaults(CFHDContext *s)
> s->subband_num_actual = 0;
> }
>
> +static void init_peak_table_defaults(CFHDContext *s)
> +{
> +s->peak.level = 0;
> +s->peak.offset = 0;
> +s->peak.base = NULL;
> +}
> +
> static void init_frame_defaults(CFHDContext *s)
> {
> s->coded_width = 0;
> @@ -86,15 +96,44 @@ static void init_frame_defaults(CFHDContext *s)
> s->wavelet_depth = 3;
> s->pshift= 1;
> s->codebook = 0;
> +s->difference_coding = 0;
> +s->progressive = 0;
> init_plane_defaults(s);
> +init_peak_table_defaults(s);
> }
>
> /* TODO: merge with VLC tables or use LUT */
> -static inline int dequant_and_decompand(int level, int quantisation)
> +static inline int dequant_and_decompand(int level, int quantisation, int
> codebook)
> +{
> +if (codebook == 0 || codebook == 1) {
> +int64_t abslevel = abs(level);
> +if (level < 264)
> +return (abslevel + ((768 * abslevel * abslevel * abslevel) /
> (255 * 255 * 255))) *
> + FFSIGN(level) * quantisation;
> +else
> +return level * quantisation;
> +} else
> +return level * quantisation;
> +}
> +
> +static inline void difference_coding(int16_t *band, int width, int height)
> +{
> +
> +int i,j;
> +for (i = 0; i < height; i++) {
> +for (j = 1; j < width; j++) {
> + band[j] += band[j-1];
> +}
> +band += width;
> +}
> +}
> +
> +static inline void peak_table(int16_t *band, Peak *peak, int length)
> {
> -int64_t abslevel = abs(level);
> -return (abslevel + ((768 * abslevel * abslevel * abslevel) / (255 * 255
> * 255))) *
> - FFSIGN(level) * quantisation;
> +int i;
> +for (i = 0; i < length; i++)
> +if (abs(band[i]) > peak->level)
> +band[i] = *(peak->base++);
This directly reads from the bytestream cast to int16.
This is likely wrong for bigendian
> }
>
> static inline void process_alpha(int16_t *alpha, int width)
> @@ -154,6 +193,18 @@ static inline void filter(int16_t *output, ptrdiff_t
> out_stride,
> }
> }
>
> +static inline void interlaced_vertical_filter(int16_t *output, int16_t *low,
> int16_t *high,
> + int width, int linesize, int plane)
> +{
> +int i;
> +int16_t even, odd;
> +for (i = 0; i < width; i++) {
> +even = (low[i] - high[i])/2;
> +odd = (low[i] + high[i])/2;
> +output[i]= av_clip_uintp2(even, 10);
> +output[i + linesize] = av_clip_uintp2(odd, 10);
> +}
> +}
> static void horiz_filter(int16_t *output, int16_t *low, int16_t *high,
> int width)
> {
> @@ -295,6 +346,9 @@ static int cfhd_decode(AVCodecContext *avctx, void *data,
> int *got_frame,
> uint16_t data = bytestream2_get_be16(&gb);
> if (abs_tag8 >= 0x60 && abs_tag8 <= 0x6f) {
> av_log(avctx, AV_LOG_DEBUG, "large len %x\n", ((tagu & 0xff) <<
> 16) | data);
> +} else if (tag == SampleFlags) {
> +av_log(avctx, AV_LOG_DEBUG, "Progressive?%"PRIu16"\n", data);
> +s->progressive = data & 0x0001;
> } else if (tag == ImageWidth) {
> av_log(avctx, AV_LOG_DEBUG, "Width %"PRIu16"\n", data);
> s->coded_width = data;
> @@ -393,6 +447,8 @@ static int cfhd_decode(AVCodecContext *avctx, void *data,
> int *got_frame,
> }
> av_log(avctx, AV_LOG_DEBUG, "Transform-type? %"PRIu16"\n", data);
> } else if (abstag >= 0x4000 && abstag <= 0x40ff) {
> +if (abstag == 0x4001)
> +s->peak.level = 0;
> av_log(avctx, AV_LOG_DEBUG, "Small chunk length %d %s\n", data *
> 4, tag < 0 ? "optional" : "required");
> bytestream2_skipu(&gb, data * 4);
> } else if (tag == 23) {
> @@ -450,7 +506,8 @@ static int cfhd_decode(AVCodecContext *avctx, void *data,
> int *got_frame,
> s->codebook = data;
> av_log(avctx, AV_LOG_DEBUG, "Codebook %i\n", s
[FFmpeg-devel] [PATCH 1/3] avcodec/magicyuv: Check bits left in flags&1 branch
Fixes: Timeout
Fixes:
8690/clusterfuzz-testcase-minimized-ffmpeg_AV_CODEC_ID_MAGICYUV_fuzzer-6542020913922048
Found-by: continuous fuzzing process
https://github.com/google/oss-fuzz/tree/master/projects/ffmpeg
Signed-off-by: Michael Niedermayer
---
libavcodec/magicyuv.c | 4
1 file changed, 4 insertions(+)
diff --git a/libavcodec/magicyuv.c b/libavcodec/magicyuv.c
index 9c6e1ba1b1..1a129c2619 100644
--- a/libavcodec/magicyuv.c
+++ b/libavcodec/magicyuv.c
@@ -240,6 +240,8 @@ static int magy_decode_slice10(AVCodecContext *avctx, void
*tdata,
dst = (uint16_t *)p->data[i] + j * sheight * stride;
if (flags & 1) {
+if (get_bits_left(&gb) < bps * width * height)
+return AVERROR_INVALIDDATA;
for (k = 0; k < height; k++) {
for (x = 0; x < width; x++)
dst[x] = get_bits(&gb, bps);
@@ -368,6 +370,8 @@ static int magy_decode_slice(AVCodecContext *avctx, void
*tdata,
dst = p->data[i] + j * sheight * stride;
if (flags & 1) {
+if (get_bits_left(&gb) < 8* width * height)
+return AVERROR_INVALIDDATA;
for (k = 0; k < height; k++) {
for (x = 0; x < width; x++)
dst[x] = get_bits(&gb, 8);
--
2.18.0
___
ffmpeg-devel mailing list
ffmpeg-devel@ffmpeg.org
http://ffmpeg.org/mailman/listinfo/ffmpeg-devel
[FFmpeg-devel] [PATCH 3/3] libavcodec/vp8: Do not compute line pointers per pixel in fade()
72->60 seconds
Testcase:
8680/clusterfuzz-testcase-minimized-ffmpeg_AV_CODEC_ID_VP7_fuzzer-5861504418054144
Signed-off-by: Michael Niedermayer
---
libavcodec/vp8.c | 6 --
1 file changed, 4 insertions(+), 2 deletions(-)
diff --git a/libavcodec/vp8.c b/libavcodec/vp8.c
index f6120aa67e..a06692c476 100644
--- a/libavcodec/vp8.c
+++ b/libavcodec/vp8.c
@@ -492,9 +492,11 @@ static void fade(uint8_t *dst, ptrdiff_t dst_linesize,
{
int i, j;
for (j = 0; j < height; j++) {
+const uint8_t *src2 = src + j * src_linesize;
+uint8_t *dst2 = dst + j * dst_linesize;
for (i = 0; i < width; i++) {
-uint8_t y = src[j * src_linesize + i];
-dst[j * dst_linesize + i] = av_clip_uint8(y + ((y * beta) >> 8) +
alpha);
+uint8_t y = src2[i];
+dst2[i] = av_clip_uint8(y + ((y * beta) >> 8) + alpha);
}
}
}
--
2.18.0
___
ffmpeg-devel mailing list
ffmpeg-devel@ffmpeg.org
http://ffmpeg.org/mailman/listinfo/ffmpeg-devel
[FFmpeg-devel] [PATCH 2/3] avcodec/vp8: Check bitstream input in vp7_fade_frame() before time consuming operation
Signed-off-by: Michael Niedermayer
---
libavcodec/vp8.c | 3 +++
1 file changed, 3 insertions(+)
diff --git a/libavcodec/vp8.c b/libavcodec/vp8.c
index 62b9f8bc2d..f6120aa67e 100644
--- a/libavcodec/vp8.c
+++ b/libavcodec/vp8.c
@@ -505,6 +505,9 @@ static int vp7_fade_frame(VP8Context *s, VP56RangeCoder *c)
int beta = (int8_t) vp8_rac_get_uint(c, 8);
int ret;
+if (c->end <= c->buffer && c->bits >= 0)
+return AVERROR_INVALIDDATA;
+
if (!s->keyframe && (alpha || beta)) {
int width = s->mb_width * 16;
int height = s->mb_height * 16;
--
2.18.0
___
ffmpeg-devel mailing list
ffmpeg-devel@ffmpeg.org
http://ffmpeg.org/mailman/listinfo/ffmpeg-devel
