[FFmpeg-devel] [RFC] Value analysis with Frama-C's Eva plugin (and an UB fix)

[Tomas Härdin]

ons 2024-05-15 klockan 23:29 +0200 skrev Michael Niedermayer:
> On Wed, May 15, 2024 at 09:39:43PM +0200, Tomas Härdin wrote:
> > Hi
> > 
> > So as I said in the coverity thread it would be good if we could
> > get at
> > least part of the codebase covered using formal tools. To this
> > effect I
> > sat down for an hour just now and gave libavutil/common.h a go with
> > Frama-C's Eva plugin [1;2]. This plugin performs value analysis,
> > which
> > is a much simpler analysis compared to say the weakest predicate
> > (WP)
> > plugin.
> > 
> > Going through the functions from top to bottom it only took until
> > av_clipl_int32_c() to find my first UB, a patch for which is
> > attached.
> > Thus my harping on this has born at least some fruit.
> > 
> > To run the analysis implemented in this set of patches (all of
> > which
> > I've attached here because I don't want to bother writing six
> > follow-up
> > email), first install frama-c using opam. I'm using 28.0~beta
> > (Nickel).
> > Then run "make verify" in libavutil/ and Eva should tell you that
> > 33%
> > of functions are covered and 100% of statements in those functions
> > are
> > covered, with zero alarms.
> > 
> > If the project isn't interested in this then I'll probably continue
> > fiddling with it on my own mostly as exercise. But I suspect it
> > will
> > bear even more fruit in time.
> 
> i think this is cool, especially considering
> 
> 
> >  common.h |    4 ++--
> >  1 file changed, 2 insertions(+), 2 deletions(-)
> > e451a7cd9a600ece22a6ee85ad7ed0c16349a411  0006-lavu-common.h-Fix-
> > UB-in-av_clipl_int32_c.patch
> > From 8a535878b9f1f87ca20d5e626f2c4c098b1c948e Mon Sep 17 00:00:00
> > 2001
> > From: =?UTF-8?q?Tomas=20H=C3=A4rdin?= <git at haerdin.se>
> > Date: Wed, 15 May 2024 21:03:47 +0200
> > Subject: [PATCH 6/7] lavu/common.h: Fix UB in av_clipl_int32_c()
> > 
> > ---
> >  libavutil/common.h | 4 ++--
> >  1 file changed, 2 insertions(+), 2 deletions(-)
> > 
> > diff --git a/libavutil/common.h b/libavutil/common.h
> > index d81131f8ad..0521ebbfc5 100644
> > --- a/libavutil/common.h
> > +++ b/libavutil/common.h
> > @@ -258,8 +258,8 @@ static av_always_inline av_const int16_t
> > av_clip_int16_c(int a)
> >   */
> >  static av_always_inline av_const int32_t av_clipl_int32_c(int64_t
> > a)
> >  {
> > -    if ((a+0x80000000u) & ~UINT64_C(0xFFFFFFFF)) return
> > (int32_t)((a>>63) ^ 0x7FFFFFFF);
> > -    else                                         return
> > (int32_t)a;
> > +    if ((a+UINT64_C(0x80000000)) & ~UINT64_C(0xFFFFFFFF)) return
> > (int32_t)((a>>63) ^ 0x7FFFFFFF);
> > +    else                                                  return
> > (int32_t)a;
> >  }
> 
> it already found something
> 
> the av_clipl_int32_c patch LGTM

Yeah I'll push that patch later today or so if there are no objections.
I'll probably keep the rest of them in a fork of my own for now,
especially since I'm still learning more about Eva. For example, the
ACSL contracts I added to av_log2*() might not actually be necessary

/Tomas