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

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.

/Tomas

[1] https://frama-c.com/
[2] https://frama-c.com/fc-plugins/eva.html

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

thx

[...]

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.
> 
> /Tomas
> 
> [1] https://frama-c.com/
> [2] https://frama-c.com/fc-plugins/eva.html

I'm all for automated checks, but in my experience they're only worthwhile
if two conditions are met:

* they run automatically on a regular basis
* their output doesn't get boring

One simple way to meet both criteria would be a cron job that runs overnight,
and messages the ML with just the issues that didn't exist in yesterday's run.

Plenty of other ways to do it, but something like that would be a great start.

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

tor 2024-05-16 klockan 13:12 +0100 skrev Andrew Sayers:
> 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.
> > 
> > /Tomas
> > 
> > [1] https://frama-c.com/
> > [2] https://frama-c.com/fc-plugins/eva.html
> 
> I'm all for automated checks, but in my experience they're only
> worthwhile
> if two conditions are met:
> 
> * they run automatically on a regular basis

They could easily be incorporated into FATE or a post-commit hook

> * their output doesn't get boring

The output of Frama-C in general tends to be quite chatty. I've asked a
couple of time for them to add exit codes, for example returning with
zero only if there are no alarms and no unproven proof obligations.
With Eva grepping for " 0 alarms generated by the analysis." is one
way, but that's also quite ugly

/Tomas

On Thu, May 16, 2024 at 02:31:31PM +0200, Tomas Härdin wrote:
> tor 2024-05-16 klockan 13:12 +0100 skrev Andrew Sayers:
> > 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.
> > > 
> > > /Tomas
> > > 
> > > [1] https://frama-c.com/
> > > [2] https://frama-c.com/fc-plugins/eva.html
> > 
> > I'm all for automated checks, but in my experience they're only
> > worthwhile
> > if two conditions are met:
> > 
> > * they run automatically on a regular basis
> 
> They could easily be incorporated into FATE or a post-commit hook

FATE is a good idea, but post-commit hooks break some workflows.
For example, I like to start a test in one window, then put together a commit
in another window.  I can always amend the commit if there's a problem.

The documentation suggests there are some hooks around e-mailing[1],
but I haven't tried them.

> 
> > * their output doesn't get boring
> 
> The output of Frama-C in general tends to be quite chatty. I've asked a
> couple of time for them to add exit codes, for example returning with
> zero only if there are no alarms and no unproven proof obligations.
> With Eva grepping for " 0 alarms generated by the analysis." is one
> way, but that's also quite ugly

Yeah, IMHO the refusal to listen to such reasonable requests is the standard
way for these projects to sabotage themselves.

Diffing against the previous run tends to work a little better than grepping
for a magic word, but still ugly, and you end up having to get rid of line
numbers with `sed` or something.

I find it's easier to put up with such hacks by constantly reminding myself:
No code solution can ever be as ugly as having to do it all by hand.

[1] https://git-scm.com/book/en/v2/Customizing-Git-Git-Hooks#_email_hooks