[cfe-dev] static analyzer status?

[Lou Wynn via cfe-dev]

Thank you for the updates!

I looked through the project report of using Z3 to remove false
positives. It is very promising. It's already in Clang 7.

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.

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?

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?

Thanks,
Lou

On 09/13/2018 05:31 PM, Artem Dergachev wrote:
> 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/423b14b0/attachment.html>