Static Analysis: results of FUDcon Lawrence hackfest

[David Malcolm]

On Fri, 2013-01-25 at 13:03 +0000, Daniel P. Berrange wrote:
> On Fri, Jan 25, 2013 at 12:51:13PM +0000, Richard W.M. Jones wrote:
> > On Fri, Jan 25, 2013 at 01:18:43PM +0100, Kamil Dudka wrote:
> > > On Friday, January 25, 2013 09:07:22 Richard W.M. Jones wrote:
> > > > On Thu, Jan 24, 2013 at 02:11:11PM -0700, Jerry James wrote:
> > > > > Note that we also have why and why3 in Fedora, by the way.
> > > > 
> > > > .. and ocaml-cil.
> > > 
> > > CIL can be used as a front-end for a static analysis tool or a C preprocessor 
> > > for static analysis tools that have limited C language parsing capabilities, 
> > > but how are you going to use CIL as a static analysis tool on its own?
> > 
> > Well I did try.  Not, it has to be said, very successfully:
> > 
> > http://people.redhat.com/~rjones/cil-analysis-of-libvirt/
> 
> Based on your work I actually used CIL to validate the correctness of
> mutex locking in libvirt with pretty good success
> 
> https://www.berrange.com/posts/2009/05/15/static-analysis-to-validate-mutex-locking-in-libvirt-using-ocaml-cil/
> 
> the analysis script has bit-rotted since i first wrote it, since
> libvirt locking policy has changed, but it should be possible to
> bring it up2date. It identified a good set of bugs, which I don't
> believe tools like coverity are able todo, because they lack the
> semantic knowledge about intended locking behaviour in this area.
> 
> > This brings me back to an earlier post I made which I still think has
> > an important point to make:
> > 
> > http://lists.fedoraproject.org/pipermail/devel/2012-December/175324.html
> 
> Yep, if I ever have some free time, I have long planned to make
> use of CIL to validate the virError reporting item you mention
> there. It would clear out a large set of bugs that are basically
> impossible to validate any other way than by writing a custom
> static analysis script.

As Kamil points out elsewhere in this thread, what we need are automated
tools that can run on code and emit warnings, without needing human
intervention.  CIL seems like an excellent toolkit for building such
tools, and reading your blog post it sounds like you achieved that.

I like the idea of domain-specific analyzers.  It isn't quite clear to
me at what level your libvirt analysis would work: would you be
analyzing libvirt itself, or all users of the libvirt API across the
distro? (or both?)

What I'm hoping for with the (mock-with-analysis + firehose) approach is
that with either of the above, if you want to write a dedicated analyzer
for, say, users of the libvirt API, then we can add that to the
infrastructure and accept that at first the results are only going to be
of interest to the person writing the libvirt-analyzer: we can have the
metadata and filters in place so that only that person needs to see the
results, until the tool is worth running by default.  (and enough
sandboxing within mock-with-analysis so that if one analyzer goes into
an infinite loop (or whatever) it doesn't interfere with everything else
running to completion- my cpychecker tool occasionally fails, so clearly
I need the proposed results format to capture that).

So yeah, I want to build a pluggable static analysis framework where
we're running the entire distro through a collection of analysis tools
(some of which might be fairly special-purpose, others might be under
development), and presenting the results in some useful fashion.  So far
I've been focusing on test execution and the data model; I hope to look
at results presentation next (I have lots of ideas on that).

Dave