Re: [Qemu-devel] QEMU versus Facebook's Infer static analysis tool

[Stefan Hajnoczi]

On Sat, Nov 14, 2015 at 09:53:44PM +0000, Peter Maydell wrote:
> So I tried out Facebook's Infer static analysis tool (http://fbinfer.com/)
> on QEMU this evening, just to see whether it would be able to handle our
> codebase and if it would report anything interesting.
> 
> The good news is it was easy enough to install and didn't fall over;
> all you have to do to run it is (a) configure; (b) run "infer -- make -j4"
> in the build directory.
> 
> The bad news is that it really doesn't get on with our QOM cast macros.
> It produces over a thousand false positives for code like
>     CadenceUARTState *s = CADENCE_UART(dev);
>     s->r[R_CR] = 0x00000128;
> where as far as I can tell it thinks that 's' could be NULL when
> deferenced because:
>  * the QOM cast macro has an internal call to object_dynamic_cast_assert()
>  * object_dynamic_cast_assert() handles being passed NULL (it returns NULL
>    if the input is NULL), so it includes tests for 'obj != NULL'
>  * infer assumes that this test implies that obj could be NULL in this
>    code path
> 
> That's a shame, because it would have been nice to include another
> kind of static analysis in what we run on QEMU (especially since
> the coverity tests are "only runs every so often when we do a build"),
> and the ability to do incremental analysis would have meant you could
> include it in day to day workflow much more easily.
> 
> In summary: worth keeping an eye on to see if it improves, but for
> now I figured I'd just post this email to the list to save anybody
> else running through the same process to come to the same conclusion.

Is it possible to send feedback to the fbinfer team?  Maybe they are
willing to solve the issue.  From your description it seems like the
tool's NULL analysis is too shallow and not useful due to the false
positives.

Stefan

signature.asc
Description: PGP signature