<html>
<head>
<meta http-equiv="Content-Type" content="text/html; charset=utf-8">
</head>
<body text="#000000" bgcolor="#FFFFFF">
<p><font size="+1">Thank you for the updates!<br>
<br>
I looked through the project report of using Z3 to remove false
positives. It is very promising. It's already in Clang 7.<br>
<br>
But my problem is finding specific bugs that the static analyzer
cannot find. For example, integer overflow which involves
multiple symbols in an expression. I guess that the current
static analyzer cannot handle this because Z3 only takes
findings of the analyzer. The analyzer does not handle multiple
symbols, so Z3 has no chance to see the entire expression even
though Z3 can process multiple symbols.<br>
<br>
I can rephrase this to taint propagation and integer expression
by saying that an expression involving a tainted value is likely
to cause integer overflow. What is the best way to implement
this checker if I use this strategy? I've noticed that there is
a taint propagation checker but haven't figured out how to use
it in another checker. Is there any example code that uses it?<br>
<br>
Another thought of combining the static analysis and Z3 is
developing another static analyzer which doesn't use symbolic
execution, just abstract interpretation. It'll be more scalable
but probably cause many false positives, then use the current Z3
integration to remove false positives. If I'll go this route,
where should I start with?<br>
<br>
</font></p>
<pre class="moz-signature" cols="72">Thanks,
Lou
</pre>
<div class="moz-cite-prefix">On 09/13/2018 05:31 PM, Artem Dergachev
wrote:<br>
</div>
<blockquote type="cite"
cite="mid:8c53dc57-7cad-4bf4-b94c-936e515b5393@gmail.com">
<meta http-equiv="Content-Type" content="text/html; charset=utf-8">
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"
moz-do-not-send="true">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" moz-do-not-send="true">cfe-dev@lists.llvm.org</a>
<a class="moz-txt-link-freetext" href="http://lists.llvm.org/cgi-bin/mailman/listinfo/cfe-dev" moz-do-not-send="true">http://lists.llvm.org/cgi-bin/mailman/listinfo/cfe-dev</a>
</pre>
</blockquote>
<br>
</blockquote>
<br>
</body>
</html>