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

[Andrew Sayers]

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