<html>
<head>
<meta http-equiv="Content-Type" content="text/html; charset=UTF-8">
</head>
<body text="#000000" bgcolor="#FFFFFF">
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.<br>
<br>
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.<br>
<br>
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
<a class="moz-txt-link-freetext" href="http://lists.llvm.org/pipermail/cfe-dev/2018-August/058912.html">http://lists.llvm.org/pipermail/cfe-dev/2018-August/058912.html</a> for
more details.<br>
<br>
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.<br>
<br>
<div class="moz-cite-prefix">On 9/13/18 3:00 PM, Lou Wynn via
cfe-dev wrote:<br>
</div>
<blockquote type="cite"
cite="mid:d443daa5-3cc3-ed27-8a1e-dda62c8d3d1b@gmail.com">
<meta http-equiv="content-type" content="text/html; charset=UTF-8">
<p><font size="+1">Hi,</font></p>
<p><font size="+1">I have watched the Building a Checker in 24
Hours slide (<a class="moz-txt-link-freetext"
href="http://llvm.org/devmtg/2012-11/Zaks-Rose-Checker24Hours.pdf"
moz-do-not-send="true">http://llvm.org/devmtg/2012-11/Zaks-Rose-Checker24Hours.pdf</a>).
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.</font><br>
</p>
<pre class="moz-signature" cols="72">--
Thanks,
Lou
</pre>
<br>
<fieldset class="mimeAttachmentHeader"></fieldset>
<pre class="moz-quote-pre" wrap="">_______________________________________________
cfe-dev mailing list
<a class="moz-txt-link-abbreviated" href="mailto:cfe-dev@lists.llvm.org">cfe-dev@lists.llvm.org</a>
<a class="moz-txt-link-freetext" href="http://lists.llvm.org/cgi-bin/mailman/listinfo/cfe-dev">http://lists.llvm.org/cgi-bin/mailman/listinfo/cfe-dev</a>
</pre>
</blockquote>
<br>
</body>
</html>