[cfe-dev] static analyzer status?

[Artem Dergachev via cfe-dev]

There were slight improvements, but our ad-hoc constraint solver quickly 
becomes unmaintainable (algorithmic complexity exponentially explodes) 
while we try to squeeze more features into it.

There was also an attempt to use Z3, i.e. a full-featured theorem 
prover, instead of our ad-hoc solver. Z3 supports everything, but makes 
the analyzer significantly slower (imagine 10x-20x). This is very 
experimental and was never supported, because it seems to be a dead end 
due to a huge performance hit.

Finally, last GSoC there was an attempt to use both constraint solvers: 
use ad-hoc solver during analysis (to quickly eliminate infeasible paths 
and report bugs), and then cross-check with Z3 only when the actual bug 
report is emitted. This fixes the problem when it comes to eliminating 
false positives, but it doesn't allow the analyzer to find new classes 
of bugs. This completely avoids any performance problems and looks very 
promising, and while this is still not officially supported, we'll 
probably be looking more into this to see if we'll be able to ship this 
somehow, probably with a different SMT or SAT solver if we run into 
problems with Z3. See 
http://lists.llvm.org/pipermail/cfe-dev/2018-August/058912.html for more 
details.

So if your main problem is false positives there's much more hope to see 
a solution available soon-ish than if your main problem is being able to 
find these specific bugs.

On 9/13/18 3:00 PM, Lou Wynn via cfe-dev wrote:
>
> Hi,
>
> I have watched the Building a Checker in 24 Hours slide 
> (http://llvm.org/devmtg/2012-11/Zaks-Rose-Checker24Hours.pdf). It 
> mentioned that one limitation of the Constraint Solver is that it 
> can't handle multiple symbols (page 83). The talk was given in 2012. 
> I'm wondering if this limitation has been removed now in 2018.
>
> -- 
> Thanks,
> Lou
>
> _______________________________________________
> cfe-dev mailing list
> cfe-dev at lists.llvm.org
> http://lists.llvm.org/cgi-bin/mailman/listinfo/cfe-dev

-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.llvm.org/pipermail/cfe-dev/attachments/20180913/1b383085/attachment.html>